Merge pull request #13 from maxkurze1/directly_typed_parsing

A couple of improvements for directly typed parsing

coq/CPS.v

@@ -211,13 +211,13 @@ Section CPS.
                        k (Some (l, (sigma fn) v, Gamma))
                      | None => k None
                      end)
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         fun k =>
           interp_args'_cps (@cps) args
                            (fun res =>
                               match res with
                               | Some (l, argvals, Gamma) =>
-                                cps body (fun res =>
+                                cps fn.(int_body) (fun res =>
                                             match res with
                                             | Some (l, v, _) =>
                                               k (Some (l, v, Gamma))

coq/CompactSemantics.v

@@ -133,9 +133,9 @@ Section Interp.
       | ExternalCall fn arg1 => fun Gamma =>
         let/opt3 action_log, arg1, Gamma := interp_action Gamma sched_log action_log arg1 in
         Some (action_log, sigma fn arg1, Gamma)
-      | InternalCall name args body => fun Gamma =>
+      | InternalCall fn args => fun Gamma =>
         let/opt3 action_log, results, Gamma := interp_args' (@interp_action) Gamma sched_log action_log args in
-        let/opt3 action_log, v, _ := interp_action results sched_log action_log body in
+        let/opt3 action_log, v, _ := interp_action results sched_log action_log fn.(int_body) in
         Some (action_log, v, Gamma)
       | APos _ a => fun Gamma =>
         interp_action Gamma sched_log action_log a

coq/Desugaring.v

@@ -33,7 +33,7 @@ Section Desugaring.
     | UBinop fn arg1 arg2 => UBinop fn (d arg1) (d arg2)
     | UExternalCall fn arg => UExternalCall (fSigma fn) (d arg)
     | UInternalCall fn args =>
-      UInternalCall (map_intf_body d fn) (List.map d args)
+      UInternalCall (map_uintf_body d fn) (List.map d args)
     | UAPos p e => UAPos p (d e)
     | USugar s => desugar pos fR fSigma s
     end
@@ -77,7 +77,7 @@ Section Desugaring.
            SyntaxMacros.uswitch (d var) (d default) branches
          | UCallModule fR' fSigma' fn args =>
            let df body := desugar_action' pos (fun r => fR (fR' r)) (fun fn => fSigma (fSigma' fn)) body in
-           UInternalCall (map_intf_body df fn) (List.map d args)
+           UInternalCall (map_uintf_body df fn) (List.map d args)
          end.
 
   Definition desugar_action (pos: pos_t) (a: uaction reg_t ext_fn_t)

coq/Frontend.v

@@ -80,8 +80,8 @@ Notation rule := (rule pos_t var_t fn_name_t).
 
 Notation scheduler := (scheduler pos_t _).
 
-Notation UInternalFunction reg_t ext_fn_t := (InternalFunction var_t fn_name_t (uaction reg_t ext_fn_t)).
-Notation InternalFunction R Sigma sig tau := (InternalFunction var_t fn_name_t (action R Sigma sig tau)).
+Notation UInternalFunction reg_t ext_fn_t := (UInternalFunction pos_t var_t fn_name_t reg_t ext_fn_t).
+Notation InternalFunction R Sigma sig tau := (InternalFunction pos_t var_t fn_name_t R Sigma sig tau).
 
 Notation register_update_circuitry R Sigma := (register_update_circuitry _ R Sigma ContextEnv).
 
@@ -213,7 +213,7 @@ Notation tc_rule R Sigma ua :=
   (tc_action R Sigma (@List.nil (var_t * type)) unit_t ua) (only parsing).
 
 Notation tc_function R Sigma uf :=
-  (tc_action R Sigma (int_argspec uf) (int_retSig uf) (int_body uf)) (only parsing).
+  (tc_action R Sigma (uint_argspec uf) (uint_retType uf) (uint_body uf)) (only parsing).
 
 Ltac _arg_type R :=
   match type of R with

coq/Lowering.v

@@ -130,10 +130,10 @@ Section Lowering.
         lower_binop fn (l a1) (l a2)
       | TypedSyntax.ExternalCall fn a =>
         LoweredSyntax.ExternalCall fn (l a)
-      | TypedSyntax.InternalCall fn args body =>
+      | TypedSyntax.InternalCall fn args =>
         SyntaxMacros.InternalCall
           (lower_args' (@lower_action) args)
-          (l body)
+          (l fn.(int_body))
       | TypedSyntax.APos p a =>
         LoweredSyntax.APos p (l a)
       end.

coq/Parsing.v

@@ -131,17 +131,11 @@ Notation "a '[' b ':+' c ']'" := (UBinop (UBits2 (UIndexedSlice c)) a b) (in cus
 Notation "'`' a '`'" := ( a) (in custom koika at level 99, a constr at level 99).
 
 Notation "'fun' nm args ':' ret '=>' body" :=
-  {| int_name := nm%string;
-     int_argspec := args;
-     int_retSig := ret;
-     int_body := body |}
-    (in custom koika at level 99, nm custom koika_var at level 0, args custom koika_types, ret constr at level 0, body custom koika at level 99, format "'[v' 'fun'  nm  args  ':'  ret  '=>' '/' body ']'").
+  (Build_UInternalFunction' nm%string args ret body)
+    (in custom koika at level 99, nm custom koika_var at level 0, args custom koika_types, ret constr at level 0, body custom koika at level 99, right associativity, format "'[v' 'fun'  nm  args  ':'  ret  '=>' '/' body ']'").
 Notation "'fun' nm '()' ':' ret '=>' body" :=
-  {| int_name := nm%string;
-     int_argspec := nil;
-     int_retSig := ret;
-     int_body := body |}
-    (in custom koika at level 99, nm custom koika_var at level 0, ret constr at level 0, body custom koika at level 99, format "'[v' 'fun'  nm  '()'   ':'  ret  '=>' '/' body ']'").
+  (Build_UInternalFunction' nm%string nil ret body)
+    (in custom koika at level 99, nm custom koika_var at level 0, ret constr at level 0, body custom koika at level 99, right associativity, format "'[v' 'fun'  nm  '()'   ':'  ret  '=>' '/' body ']'").
 
 (* Deprecated *)
 Notation "'call' instance method args" :=
@@ -268,10 +262,6 @@ Module Type Tests.
   (* Notation "'{&' a '&}'" := (a) (a custom koika_types at level 200). *)
   (* Definition test_21 := {& "yoyo" : bits_t 2 &}. *)
   (* Definition test_22 := {& "yoyo" : bits_t 2 , "yoyo" : bits_t 2  &}. *)
-  Definition test_23 : InternalFunction string string (uaction reg_t) := {{ fun test (arg1 : (bits_t 3)) (arg2 : bits_t 2) : bits_t 4 => magic }}.
-  Definition test_24 : nat -> InternalFunction string string (uaction reg_t) :=  (fun sz => {{ fun test (arg1 : bits_t sz) (arg1 : bits_t sz) : bits_t sz  => magic}}).
-  Definition test_25 : nat -> InternalFunction string string (uaction reg_t) := (fun sz => {{fun test (arg1 : bits_t sz ) : bits_t sz => let oo := magic >> magic in magic}}).
-  Definition test_26 : nat -> InternalFunction string string (uaction reg_t) := (fun sz => {{ fun test () : bits_t sz  => magic }}).
   Definition test_27 : uaction reg_t :=
     {{
         (if (!read0(data0)) then
@@ -283,6 +273,12 @@ Module Type Tests.
            read0(data0));
         fail
     }}.
+  Notation UInternalFunction :=
+    (UInternalFunction pos_t string string reg_t ext_fn_t).
+  Definition test_23 : UInternalFunction := {{ fun test (arg1 : (bits_t 3)) (arg2 : bits_t 2) : bits_t 4 => magic }}.
+  Definition test_24 : nat -> UInternalFunction :=  (fun sz => {{ fun test (arg1 : bits_t sz) (arg1 : bits_t sz) : bits_t sz  => magic}}).
+  Definition test_25 : nat -> UInternalFunction := (fun sz => {{fun test (arg1 : bits_t sz ) : bits_t sz => let oo := magic >> magic in magic}}).
+  Definition test_26 : nat -> UInternalFunction := (fun sz => {{ fun test () : bits_t sz  => magic }}).
   Definition test_28 : uaction reg_t :=  {{
                                              match var with
                                              | magic => magic

coq/Syntax.v

@@ -20,7 +20,7 @@ Section Syntax.
   | UUnop (ufn1: PrimUntyped.ufn1) (arg1: uaction)
   | UBinop (ufn2: PrimUntyped.ufn2) (arg1: uaction) (arg2: uaction)
   | UExternalCall (ufn: ext_fn_t) (arg: uaction)
-  | UInternalCall (ufn: InternalFunction var_t fn_name_t uaction) (args: list uaction)
+  | UInternalCall (ufn: UInternalFunction' var_t fn_name_t uaction) (args: list uaction)
   | UAPos (p: pos_t) (e: uaction)
   | USugar (s: usugar)
   with usugar {reg_t ext_fn_t} :=
@@ -40,7 +40,7 @@ Section Syntax.
   | UCallModule {module_reg_t module_ext_fn_t: Type}
                 (fR: module_reg_t -> reg_t)
                 (fSigma: @Lift module_ext_fn_t ext_fn_t)
-                (fn: InternalFunction var_t fn_name_t (@uaction module_reg_t module_ext_fn_t))
+                (fn: UInternalFunction' var_t fn_name_t (@uaction module_reg_t module_ext_fn_t))
                 (args: list uaction).
 
   Inductive scheduler :=
@@ -54,3 +54,8 @@ Arguments Lift: clear implicits.
 Arguments usugar : clear implicits.
 Arguments uaction : clear implicits.
 Arguments scheduler : clear implicits.
+
+Notation UInternalFunction pos_t var_t fn_name_t reg_t ext_fn_t :=
+  (UInternalFunction'
+     var_t fn_name_t
+     (uaction pos_t var_t fn_name_t reg_t ext_fn_t)).

coq/SyntaxFunctions.v

@@ -40,7 +40,7 @@ Section SyntaxFunctions.
         | UExternalCall ufn arg =>
           UExternalCall ufn (r 0 arg)
         | UInternalCall ufn arg =>
-          let ufn := map_intf_body (r 0) ufn in
+          let ufn := map_uintf_body (r 0) ufn in
           let args := snd (foldi (fun n a args => (r n a :: args)) 1 [] arg) in
           UInternalCall ufn args
         | UAPos _ e => (r 0 e)
@@ -78,7 +78,7 @@ Section SyntaxFunctions.
                  foldi (fun n a elements => (r n a) :: elements) 0 [] elements in
              UArrayInit tau elements
            | UCallModule fR fSigma ufn args =>
-             let ufn := map_intf_body (r 0) ufn in
+             let ufn := map_uintf_body (r 0) ufn in
              let args := snd (foldi (fun n a args => (r n a :: args)) 1 [] args) in
              UCallModule fR fSigma ufn args
            end.
@@ -154,11 +154,11 @@ Section SyntaxFunctions.
               let '(f, arg) := pe 0 arg in
               (f, UExternalCall ufn arg)
             | UInternalCall ufn args =>
-              let '(fbody, body) := pe 0 ufn.(int_body) in
+              let '(fbody, body) := pe 0 ufn.(uint_body) in
               let ufn :=
                   if fbody then
                     (* Only unfold the body if the error is in it *)
-                    map_intf_body (fun _ => body) ufn
+                    map_uintf_body (fun _ => body) ufn
                   else ufn in
               let '(n, (fargs, args)) :=
                   foldi (fun n arg '(fargs, args) =>
@@ -228,10 +228,10 @@ Section SyntaxFunctions.
                        0 ([], []) fields in
              (ffields, UStructInit sig fields)
            | UCallModule fR fSigma ufn args =>
-              let '(fbody, body) := pe 0 ufn.(int_body) in
+              let '(fbody, body) := pe 0 ufn.(uint_body) in
               let ufn :=
                   if fbody then (* Only unfold the body if the error is in it *)
-                    map_intf_body (fun _ => body) ufn
+                    map_uintf_body (fun _ => body) ufn
                   else ufn in
               let '(n, (fargs, args)) :=
                   foldi (fun n arg '(fargs, args) =>
@@ -267,7 +267,7 @@ Section SyntaxFunctions.
            | UInternalCall ufn args =>
              List.fold_left
                (fun acc arg => acc + uaction_size arg)
-               args (uaction_size ufn.(int_body))
+               args (uaction_size ufn.(uint_body))
            | UAPos p e => uaction_size e
            | USugar s => usugar_size s
            | _ => 0
@@ -301,7 +301,7 @@ Section SyntaxFunctions.
                 | UCallModule fR fSigma fn args =>
                   List.fold_left
                     (fun acc arg => acc + uaction_size arg)
-                    args (uaction_size fn.(int_body))
+                    args (uaction_size fn.(uint_body))
                 | _ => 0
                 end)%N.
   End TermSize.

coq/SyntaxMacros.v

@@ -146,47 +146,44 @@ Module Display.
     Context {pos_t reg_t ext_fn_t: Type}.
 
     Notation uaction := (uaction pos_t var_t fn_name_t reg_t ext_fn_t).
+    Notation intfun := (UInternalFunction pos_t var_t fn_name_t reg_t ext_fn_t).
 
     Inductive field : Type :=
     | Str (s: string)
     | Value (tau: type).
 
-    Notation intfun := (InternalFunction var_t fn_name_t uaction).
-
-    Definition empty_printer : InternalFunction var_t fn_name_t uaction :=
-      {| int_name := "print";
-         int_argspec := [];
-         int_retSig := unit_t;
-         int_body := USugar USkip |}.
+    Definition empty_printer : intfun :=
+      {| uint_name := "print";
+         uint_argspec := [];
+         uint_retType := unit_t;
+         uint_body := USugar USkip |}.
 
     Definition display_utf8 s : uaction :=
       UUnop (UDisplay (UDisplayUtf8)) (USugar (UConstString s)).
 
-    Definition nl_printer : InternalFunction var_t fn_name_t uaction :=
-      {| int_name := "print_nl";
-         int_argspec := [];
-         int_retSig := unit_t;
-         int_body := display_utf8 "\n" |}.
+    Definition nl_printer : intfun :=
+      {| uint_name := "print_nl";
+         uint_argspec := [];
+         uint_retType := unit_t;
+         uint_body := display_utf8 "\n" |}.
 
     Definition extend_printer f (offset: nat) (printer: intfun) : intfun :=
       let opts :=
           {| display_newline := false; display_strings := false; display_style := dFull |} in
       let display_value arg :=
           UUnop (UDisplay (UDisplayValue opts)) (UVar arg) in
-      let '(Build_InternalFunction int_name int_argspec int_retSig int_body) :=
-          printer in
       match f with
       | Str s =>
-        {| int_name := int_name;
-           int_argspec := int_argspec;
-           int_retSig := int_retSig;
-           int_body := (USeq (display_utf8 s) int_body) |}
+        {| uint_name    := printer.(uint_name);
+           uint_argspec := printer.(uint_argspec);
+           uint_retType  := printer.(uint_retType);
+           uint_body    := (USeq (display_utf8 s) printer.(uint_body)) |}
       | Value tau =>
         let arg := String.append "arg" (show offset) in
-        {| int_name := int_name;
-           int_argspec := (arg, tau) :: int_argspec;
-           int_retSig := unit_t;
-           int_body := (USeq (display_value arg) int_body) |}
+        {| uint_name    := printer.(uint_name);
+           uint_argspec := (arg, tau) :: printer.(uint_argspec);
+           uint_retType  := unit_t;
+           uint_body    := (USeq (display_value arg) printer.(uint_body)) |}
       end.
 
     Fixpoint make_printer (offset: nat) (fstring: list field) : intfun :=

coq/TypeInference.v

@@ -146,12 +146,15 @@ Section TypeInference.
         let/res tc_args := result_list_map (type_action pos sig) args in
         let arg_positions := List.map (actpos pos) args in
         let tc_args_w_pos := List.combine arg_positions tc_args in
-        let/res args_ctx := assert_argtypes e fn.(int_name) pos (List.rev fn.(int_argspec)) (List.rev tc_args_w_pos) in
+        let/res args_ctx := assert_argtypes e fn.(uint_name) pos (List.rev fn.(uint_argspec)) (List.rev tc_args_w_pos) in
 
-        let/res fn_body' := type_action (actpos pos fn.(int_body)) (List.rev fn.(int_argspec)) fn.(int_body) in
-        let/res fn_body' := cast_action (actpos pos fn.(int_body)) fn.(int_retSig) (``fn_body') in
+        let/res fn_body' := type_action (actpos pos fn.(uint_body)) (List.rev fn.(uint_argspec)) fn.(uint_body) in
+        let/res fn_body' := cast_action (actpos pos fn.(uint_body)) fn.(uint_retType) (``fn_body') in
 
-        Success (EX (TypedSyntax.InternalCall fn.(int_name) args_ctx fn_body'))
+        Success (EX (TypedSyntax.InternalCall {|
+          int_name := fn.(uint_name);
+          int_body := fn_body';
+        |} args_ctx))
       | UUnop fn arg1 =>
         let pos1 := actpos pos arg1 in
         let/res arg1' := type_action pos sig arg1 in