From 86e559bd4622b2e43d1e73bb0dc60cf70287d572 Mon Sep 17 00:00:00 2001
From: Max Kurze <Max.Kurze@mailbox.tu-dresden.de>
Date: Sat, 9 Nov 2024 22:15:50 +0100
Subject: [PATCH 1/4] test(parsing): fix test case

---
 coq/TypedParsing.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq/TypedParsing.v b/coq/TypedParsing.v
index 561fe184..7fcbc5c8 100644
--- a/coq/TypedParsing.v
+++ b/coq/TypedParsing.v
@@ -538,7 +538,7 @@ Module Type Tests2.
   Program Definition test_lit : _action (tau := bits_t 5) := (Seq (Write P0 data0 <{ Ob~1~1~0~0~1 }>) (Const (tau := bits_t _) (Bits.of_N ltac:(let x := eval cbv in ((len "01100") * 1) in exact x) (bin_string_to_N "01100")))).
   Fail Next Obligation.
   Definition test_20 : _action := <{ |0b"11001100"| [ Ob~0~0~0 :+ 3 ] }>.
-  Definition test_23 : function R Sigma := <{ fun test (arg1 : (bits_t 3)) (arg2 : bits_t 2) : bits_t 4 => pass }>.
+  Definition test_23 : function R Sigma := <{ fun test (arg1 : (bits_t 3)) (arg2 : bits_t 2) : unit_t => pass }>.
   Definition test_24 (sz : nat) : function R Sigma := <{ fun test (arg1 : bits_t sz) (arg1 : bits_t sz) : bits_t sz  => fail(sz)}>.
   Definition test_25 (sz : nat) : function R Sigma := <{fun test (arg1 : bits_t sz ) : bits_t sz => let oo := fail(sz) >> fail(sz) in oo}>.
   Definition test_26 (sz : nat) : function R Sigma := <{ fun test () : bits_t sz  => fail(sz) }>.

From 354fe3743fc83ffc6fc8ea2db5cfca67e434685b Mon Sep 17 00:00:00 2001
From: Max Kurze <Max.Kurze@mailbox.tu-dresden.de>
Date: Sat, 9 Nov 2024 12:11:28 +0100
Subject: [PATCH 2/4] refactor(syntax): un-reverse function argspec

For some reason the arguments list of functions was stored in reverse in
the AST. I couldn't figure out a reason for it, so I decided to rather
save it as is.
---
 coq/TypedParsing.v          | 8 ++++----
 coq/TypedSyntax.v           | 4 ++--
 coq/TypedSyntaxProperties.v | 2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/coq/TypedParsing.v b/coq/TypedParsing.v
index 7fcbc5c8..fac0dcf3 100644
--- a/coq/TypedParsing.v
+++ b/coq/TypedParsing.v
@@ -270,15 +270,15 @@ Fixpoint lift_reg
 
 
 Notation "fn args" :=
-  (InternalCall (tau := fn.(int_retSig)) (argspec := rev fn.(int_argspec)) fn.(int_name) args fn.(int_body))
+  (InternalCall (tau := fn.(int_retSig)) (argspec := fn.(int_argspec)) fn.(int_name) args fn.(int_body))
     (in custom koika_t at level 1, fn constr at level 0 , args custom koika_t_args at level 99, only parsing).
 
 Notation "instance  '.(' fn ')' args" :=
-  (InternalCall (tau := fn.(int_retSig)) (argspec := rev fn.(int_argspec)) fn.(int_name) args (lift_reg (exist _ instance (fun _ => eq_refl)) fn.(int_body)))
+  (InternalCall (tau := fn.(int_retSig)) (argspec := fn.(int_argspec)) fn.(int_name) args (lift_reg (exist _ instance (fun _ => eq_refl)) fn.(int_body)))
     (in custom koika_t at level 1, instance constr at level 0, fn constr, args custom koika_t_args at level 99).
 
 Notation "'{' fn '}' args" :=
-  (InternalCall (tau := fn.(int_retSig)) (argspec := rev fn.(int_argspec)) fn.(int_name) args fn.(int_body))
+  (InternalCall (tau := fn.(int_retSig)) (argspec := fn.(int_argspec)) fn.(int_name) args fn.(int_body))
     (in custom koika_t at level 1, fn constr at level 200 , args custom koika_t_args at level 99, only parsing).
 
 Notation "'extcall' method '(' arg ')'" := (ExternalCall method arg) (in custom koika_t at level 98, method constr at level 0, arg custom koika_t).
@@ -728,4 +728,4 @@ Module Type Tests2.
   Definition num_test_constr_2 := |0b"0110"|     : bits _.
   Definition num_test_constr_3 := |"c0ffee":h|   : bits _.
   Definition num_test_constr_4 := |0x"deadbeef"| : bits _.
-End Tests2.
\ No newline at end of file
+End Tests2.
diff --git a/coq/TypedSyntax.v b/coq/TypedSyntax.v
index 7451ce76..d2c5152c 100644
--- a/coq/TypedSyntax.v
+++ b/coq/TypedSyntax.v
@@ -48,8 +48,8 @@ Section Syntax.
   | InternalCall {sig tau}
                  (fn : fn_name_t)
                  {argspec : tsig var_t}
-                 (args: context (fun k_tau => action sig (snd k_tau)) (List.rev argspec))
-                 (body : action (List.rev argspec) tau)
+                 (args: context (fun k_tau => action sig (snd k_tau)) argspec)
+                 (body : action argspec tau)
     : action sig tau
   | APos {sig tau} (pos: pos_t) (a: action sig tau)
     : action sig tau.
diff --git a/coq/TypedSyntaxProperties.v b/coq/TypedSyntaxProperties.v
index 5905e4b3..dc218918 100644
--- a/coq/TypedSyntaxProperties.v
+++ b/coq/TypedSyntaxProperties.v
@@ -74,7 +74,7 @@ Section TypedSyntaxProperties.
       generalize dependent Gamma.
       generalize dependent sched_log.
       generalize dependent action_log.
-      generalize dependent (rev argspec); clear argspec.
+      generalize dependent (argspec).
       fix IHargs 2; destruct args; cbn; intros;
         repeat dec_step. }
 

From f04056d47c44e80cb8b04045b2827031707b31c6 Mon Sep 17 00:00:00 2001
From: Max Kurze <Max.Kurze@mailbox.tu-dresden.de>
Date: Tue, 22 Oct 2024 14:22:04 +0200
Subject: [PATCH 3/4] refactor(syntax): change InternalFunction definition
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

As already done by Clément Pit-Claudel, this commit adapts the internal
function definition in order to deduplicate information that is
currently available on the term and type level. This includes the
argument specification (which is also the body's signature) and the
retSig (which is also the body's tau).
---
 coq/CPS.v                      |  4 +--
 coq/CompactSemantics.v         |  4 +--
 coq/Desugaring.v               |  4 +--
 coq/Frontend.v                 |  6 ++--
 coq/Lowering.v                 |  4 +--
 coq/Parsing.v                  | 24 +++++++---------
 coq/Syntax.v                   |  9 ++++--
 coq/SyntaxFunctions.v          | 16 +++++------
 coq/SyntaxMacros.v             | 41 +++++++++++++---------------
 coq/TypeInference.v            | 11 +++++---
 coq/TypedParsing.v             | 50 +++++++++++++++++++++++-----------
 coq/TypedSemantics.v           |  4 +--
 coq/TypedSyntax.v              |  7 +++--
 coq/TypedSyntaxFunctions.v     | 36 ++++++++++++------------
 coq/TypedSyntaxProperties.v    | 10 +++----
 coq/Types.v                    | 33 +++++++++++++---------
 ocaml/backends/coq.ml          | 22 +++++++--------
 ocaml/backends/cpp.ml          | 38 +++++++++++++-------------
 ocaml/common/common.ml         | 10 +++----
 ocaml/cuttlebone/cuttlebone.ml | 22 +++++++--------
 ocaml/frontends/lv.ml          | 14 +++++-----
 21 files changed, 199 insertions(+), 170 deletions(-)

diff --git a/coq/CPS.v b/coq/CPS.v
index b5f4352b..1c6ed129 100644
--- a/coq/CPS.v
+++ b/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))
diff --git a/coq/CompactSemantics.v b/coq/CompactSemantics.v
index 84646f79..e94c7e25 100644
--- a/coq/CompactSemantics.v
+++ b/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
diff --git a/coq/Desugaring.v b/coq/Desugaring.v
index a8238c60..4f80331a 100644
--- a/coq/Desugaring.v
+++ b/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)
diff --git a/coq/Frontend.v b/coq/Frontend.v
index 5e7ebcca..cafa9b6d 100644
--- a/coq/Frontend.v
+++ b/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_retSig uf) (uint_body uf)) (only parsing).
 
 Ltac _arg_type R :=
   match type of R with
diff --git a/coq/Lowering.v b/coq/Lowering.v
index 9db55922..d931fe8d 100644
--- a/coq/Lowering.v
+++ b/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.
diff --git a/coq/Parsing.v b/coq/Parsing.v
index 0ddf20af..4217b5c2 100644
--- a/coq/Parsing.v
+++ b/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
diff --git a/coq/Syntax.v b/coq/Syntax.v
index c44b4d87..c0f9f070 100644
--- a/coq/Syntax.v
+++ b/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)).
diff --git a/coq/SyntaxFunctions.v b/coq/SyntaxFunctions.v
index a64065ba..a52c330c 100644
--- a/coq/SyntaxFunctions.v
+++ b/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.
diff --git a/coq/SyntaxMacros.v b/coq/SyntaxMacros.v
index 112bebd4..ad789545 100644
--- a/coq/SyntaxMacros.v
+++ b/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_retSig := 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_retSig := 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_retSig  := printer.(uint_retSig);
+           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_retSig  := unit_t;
+           uint_argspec := (arg, tau) :: printer.(uint_argspec);
+           uint_body    := (USeq (display_value arg) printer.(uint_body)) |}
       end.
 
     Fixpoint make_printer (offset: nat) (fstring: list field) : intfun :=
diff --git a/coq/TypeInference.v b/coq/TypeInference.v
index 7c4f474c..426d391d 100644
--- a/coq/TypeInference.v
+++ b/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_retSig) (``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
diff --git a/coq/TypedParsing.v b/coq/TypedParsing.v
index fac0dcf3..45495fc2 100644
--- a/coq/TypedParsing.v
+++ b/coq/TypedParsing.v
@@ -42,7 +42,7 @@ Definition function
   {tau sig reg_t ext_fn_t}
   (R : reg_t -> type)
   (Sigma: ext_fn_t -> ExternalSignature) :=
-    Types.InternalFunction var_t fn_name_t
+    Types.InternalFunction' fn_name_t
       (TypedSyntax.action pos_t var_t fn_name_t R Sigma sig tau).
 
 Notation "'<{' e '}>'" := (e) (e custom koika_t at level 200).
@@ -199,17 +199,31 @@ Declare Custom Entry koika_t_types_binder.
 Notation "'(' x ':' y ')'" := (x%string, (y : type)) (in custom koika_t_types_binder at level 60, x custom koika_t_var at level 0, y constr at level 12 ).
 Notation "a  ..  b" := (cons a ..  (cons b nil) ..)  (in custom koika_t_types at level 95, a custom koika_t_types_binder , b custom koika_t_types_binder, right associativity).
 
+(* We want to tell the typechecker that the body of the function
+ * should have the function's arguments in its context (sig).
+ *
+ * However, using a type hint where R Sigma are kept implicit
+ * like:
+ * ```
+ * Definition some_act : action R Sigma :=
+ * <{ ... }>: action' (sig := ...) _ _.
+ * ```
+ * does not work since coq is then trying to infer R and Sigma from
+ * the body term instead of the outer definition.
+ *
+ * To tell coq to infer it from the definition we need
+ * bidirectionality hints and thus we need a seperate function.
+ *)
+Local Definition refine_sig_tau sig tau {reg_t ext_fn_t}
+  {R : reg_t -> type} {Sigma : ext_fn_t -> ExternalSignature}
+  (a : action' R Sigma (tau := tau) (sig := sig)) : action' R Sigma := a.
+Arguments refine_sig_tau sig tau {reg_t ext_fn_t} {R Sigma} & a : assert.
+
 Notation "'fun' nm args ':' ret '=>' body" :=
-  ({| int_name := nm%string;
-     int_argspec := args;
-     int_retSig := ret;
-     int_body := body |} : function (sig := args) _ _)
+  (Build_InternalFunction' nm%string (refine_sig_tau args ret body))
     (in custom koika_t at level 99, nm custom koika_t_var at level 0, args custom koika_t_types, ret constr at level 0, body custom koika_t at level 99, 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 |} : function (sig := nil) _ _)
+  (Build_InternalFunction' nm%string (refine_sig_tau nil ret body))
     (in custom koika_t at level 99, nm custom koika_t_var at level 0, ret constr at level 0, body custom koika_t at level 99, format "'[v' 'fun'  nm  '()'   ':'  ret  '=>' '/' body ']'").
 
 (* Koika_args *)
@@ -261,24 +275,28 @@ Fixpoint lift_reg
     | Unop fn arg => Unop fn (lift_reg lift arg)
     | Binop fn arg1 arg2 => Binop fn (lift_reg lift arg1) (lift_reg lift arg2)
     | ExternalCall fn arg => ExternalCall fn (lift_reg lift arg)
-    | InternalCall fn args body =>
-      InternalCall fn (rew List.map_id _ in
+    | InternalCall fn args =>
+      InternalCall {| int_name := fn.(int_name);
+        int_body := (lift_reg lift fn.(int_body)) |}
+      (rew List.map_id _ in
       @cmap _ _ _ (fun k_tau => action' (tau := (snd k_tau)) sR Sigma)
-        id (fun _ => lift_reg lift) _ args) (lift_reg lift body)
+        id (fun _ => lift_reg lift) _ args)
     | APos pos a => APos pos (lift_reg lift a)
     end.
 
-
 Notation "fn args" :=
-  (InternalCall (tau := fn.(int_retSig)) (argspec := fn.(int_argspec)) fn.(int_name) args fn.(int_body))
+  (InternalCall fn args)
     (in custom koika_t at level 1, fn constr at level 0 , args custom koika_t_args at level 99, only parsing).
 
 Notation "instance  '.(' fn ')' args" :=
-  (InternalCall (tau := fn.(int_retSig)) (argspec := fn.(int_argspec)) fn.(int_name) args (lift_reg (exist _ instance (fun _ => eq_refl)) fn.(int_body)))
+  (InternalCall {|
+    int_name := fn.(int_name);
+    int_body := (lift_reg (exist _ instance (fun _ => eq_refl)) fn.(int_body))
+    |} args)
     (in custom koika_t at level 1, instance constr at level 0, fn constr, args custom koika_t_args at level 99).
 
 Notation "'{' fn '}' args" :=
-  (InternalCall (tau := fn.(int_retSig)) (argspec := fn.(int_argspec)) fn.(int_name) args fn.(int_body))
+  (InternalCall fn args)
     (in custom koika_t at level 1, fn constr at level 200 , args custom koika_t_args at level 99, only parsing).
 
 Notation "'extcall' method '(' arg ')'" := (ExternalCall method arg) (in custom koika_t at level 98, method constr at level 0, arg custom koika_t).
diff --git a/coq/TypedSemantics.v b/coq/TypedSemantics.v
index 14a33e6f..65c3c370 100644
--- a/coq/TypedSemantics.v
+++ b/coq/TypedSemantics.v
@@ -110,9 +110,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
diff --git a/coq/TypedSyntax.v b/coq/TypedSyntax.v
index d2c5152c..b3b55692 100644
--- a/coq/TypedSyntax.v
+++ b/coq/TypedSyntax.v
@@ -46,10 +46,10 @@ Section Syntax.
                  (arg: action sig (arg1Sig (Sigma fn)))
     : action sig (retSig (Sigma fn))
   | InternalCall {sig tau}
-                 (fn : fn_name_t)
+                 (* TODO -- why does this list need to be reversed?? *)
                  {argspec : tsig var_t}
+                 (fn : InternalFunction' fn_name_t (action argspec tau))
                  (args: context (fun k_tau => action sig (snd k_tau)) argspec)
-                 (body : action argspec tau)
     : action sig tau
   | APos {sig tau} (pos: pos_t) (a: action sig tau)
     : action sig tau.
@@ -59,3 +59,6 @@ End Syntax.
 
 Arguments action pos_t var_t fn_name_t {reg_t ext_fn_t} R Sigma sig tau : assert.
 Arguments rule pos_t var_t fn_name_t {reg_t ext_fn_t} R Sigma : assert.
+
+Notation InternalFunction pos_t var_t fn_name_t R Sigma sig tau :=
+  (InternalFunction' fn_name_t (action pos_t var_t fn_name_t R Sigma sig tau)).
diff --git a/coq/TypedSyntaxFunctions.v b/coq/TypedSyntaxFunctions.v
index cae779af..ca6b647f 100644
--- a/coq/TypedSyntaxFunctions.v
+++ b/coq/TypedSyntaxFunctions.v
@@ -44,9 +44,9 @@ Section TypedSyntaxFunctions.
       | Unop fn arg1 => action_footprint' acc arg1
       | Binop fn arg1 arg2 => action_footprint' (action_footprint' acc arg1) arg2
       | ExternalCall fn arg => action_footprint' acc arg
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         let acc := cfoldr (fun _ _ arg acc => action_footprint' acc arg) args acc in
-        action_footprint' acc body
+        action_footprint' acc fn.(int_body)
       | APos _ a => action_footprint' acc a
       end.
 
@@ -255,7 +255,7 @@ Section TypedSyntaxFunctions.
       | ExternalCall fn arg =>
         let '(env, arg) := annotate_action_register_histories env arg in
         (env, ExternalCall fn arg)
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         let '(env, args) :=
             cfoldr (fun sg k arg cont =>
                       fun env =>
@@ -263,8 +263,8 @@ Section TypedSyntaxFunctions.
                         let '(env, args) := cont env in
                         (env, CtxCons k arg args)) args
                    (fun env => (env, CtxEmpty)) env in
-        let '(env, body) := annotate_action_register_histories env body in
-        (env, InternalCall fn args body)
+        let '(env, body) := annotate_action_register_histories env fn.(int_body) in
+        (env, InternalCall {| int_name := fn.(int_name); int_body := body |} args)
       | APos pos a =>
         let '(env, a) := annotate_action_register_histories env a in
         (env, APos (PosAnnot pos) a)
@@ -393,9 +393,9 @@ Section TypedSyntaxFunctions.
       | Unop fn arg1 => rule_max_log_size arg1
       | Binop fn arg1 arg2 => rule_max_log_size arg1 + rule_max_log_size arg2
       | ExternalCall fn arg => rule_max_log_size arg
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         cfoldl (fun k arg acc => acc + rule_max_log_size arg) args 0
-        + rule_max_log_size body
+        + rule_max_log_size fn.(int_body)
       | APos pos a => rule_max_log_size a
       end.
   End StaticAnalysis.
@@ -418,9 +418,9 @@ Section TypedSyntaxFunctions.
       | Unop fn a => existsb_subterm f a
       | Binop fn a1 a2 => existsb_subterm f a1 || existsb_subterm f a2
       | ExternalCall fn arg => existsb_subterm f arg
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         cfoldl (fun k arg acc => acc || existsb_subterm f arg) args false
-        || existsb_subterm f body
+        || existsb_subterm f fn.(int_body)
       | APos _ a => existsb_subterm f a
       end.
 
@@ -457,9 +457,9 @@ Section TypedSyntaxFunctions.
     | Unop fn arg1 => is_pure arg1
     | Binop fn arg1 arg2 => is_pure arg1 && is_pure arg2
     | ExternalCall fn arg => false
-    | InternalCall fn args body =>
+    | InternalCall fn args =>
       cfoldr (fun _ k arg acc => acc && is_pure arg) args true
-      && is_pure body
+      && is_pure fn.(int_body)
     | APos pos a => is_pure a
     end.
 
@@ -477,7 +477,7 @@ Section TypedSyntaxFunctions.
     | Unop fn arg1 => false
     | Binop fn arg1 arg2 => false
     | ExternalCall fn arg => false
-    | InternalCall fn args body => returns_zero body
+    | InternalCall fn args => returns_zero fn.(int_body)
     | APos pos a => returns_zero a
     end.
 
@@ -495,7 +495,7 @@ Section TypedSyntaxFunctions.
     | @Unop _ _ _ _ _ _ _ _ fn _ => Some (PrimSignatures.Sigma1 fn).(retSig)
     | @Binop _ _ _ _ _ _ _ _ fn _ _ => Some (PrimSignatures.Sigma2 fn).(retSig)
     | @ExternalCall _ _ _ _ _ _ _ _ _ _ => None
-    | @InternalCall _ _ _ _ _ _ _ _ tau _ _ _ _ => Some tau
+    | @InternalCall _ _ _ _ _ _ _ _ tau _ _ _ => Some tau
     | @APos _ _ _ _ _ _ _ _ tau _ _ => Some tau
     end.
 
@@ -521,7 +521,7 @@ Section TypedSyntaxFunctions.
       let/opt r2 := interp_arithmetic arg2 in
       Some (PrimSpecs.sigma2 fn r1 r2)
     | ExternalCall fn arg => None
-    | InternalCall fn args body => None
+    | InternalCall fn args => None
     | APos pos a => interp_arithmetic a
     end.
 
@@ -544,8 +544,8 @@ Section TypedSyntaxFunctions.
            action_size arg1 + action_size arg2
          | ExternalCall ufn arg =>
            action_size arg
-         | InternalCall fn argspec body =>
-           cfoldl (fun _ arg acc => acc + action_size arg) argspec (action_size body)
+         | InternalCall fn argspec =>
+           cfoldl (fun _ arg acc => acc + action_size arg) argspec (action_size fn.(int_body))
          | APos p e => action_size e
          | _ => 0
          end)%N.
@@ -585,9 +585,9 @@ Section TypedSyntaxFunctions.
         find_read1s_after_write1s' acc arg2
       | ExternalCall fn arg =>
         find_read1s_after_write1s' acc arg
-      | InternalCall fn args body =>
+      | InternalCall fn args =>
         let acc := cfoldr (fun _ _ arg acc => find_read1s_after_write1s' acc arg) args acc in
-        find_read1s_after_write1s' acc body
+        find_read1s_after_write1s' acc fn.(int_body)
       | APos _ a => find_read1s_after_write1s' acc a
       end.
 
diff --git a/coq/TypedSyntaxProperties.v b/coq/TypedSyntaxProperties.v
index dc218918..c907be8d 100644
--- a/coq/TypedSyntaxProperties.v
+++ b/coq/TypedSyntaxProperties.v
@@ -45,15 +45,14 @@ Section TypedSyntaxProperties.
     | [ H: Some _ = Some _ |- _ ] => inversion H; subst; clear H
     | _ => solve [intuition eauto 3 using bits_to_N_zero]
     end.
-
-  Lemma returns_zero_correct {sig tau} :
-    forall (a: action sig tau) (Gamma: tcontext sig) (sched_log: Log) (action_log: Log),
+  Fixpoint returns_zero_correct {sig tau} (a: action sig tau) {struct a} :
+    forall (Gamma: tcontext sig) (sched_log: Log) (action_log: Log),
       returns_zero a = true ->
       forall l v G,
         interp_action r sigma Gamma sched_log action_log a = Some (l, v, G) ->
         bits_of_value v = Bits.zeroes (type_sz tau).
   Proof.
-    induction a; repeat dec_step.
+    destruct a; try solve [repeat dec_step].
   Qed.
 
   Lemma is_pure_correct :
@@ -70,7 +69,8 @@ Section TypedSyntaxProperties.
                interp_args r sigma Gamma sched_log action_log args = Some (l', v, G) ->
                l = action_log).
 
-    { clear dependent a; clear t t2 Heqo.
+    { destruct fn as [name a]; clear dependent a.
+      clear t t2 Heqo.
       generalize dependent Gamma.
       generalize dependent sched_log.
       generalize dependent action_log.
diff --git a/coq/Types.v b/coq/Types.v
index 2a56238b..2fb3acc9 100644
--- a/coq/Types.v
+++ b/coq/Types.v
@@ -289,21 +289,28 @@ Definition CExternalSignature := CSig 1.
 Definition tsig var_t := list (var_t * type).
 Definition lsig := list nat.
 
-Record InternalFunction {var_t fn_name_t action: Type} :=
+Record UInternalFunction' {var_t fn_name_t action: Type} :=
+  { uint_name : fn_name_t;
+    uint_argspec : tsig var_t;
+    uint_retSig : type;
+    uint_body : action }.
+Arguments UInternalFunction' : clear implicits.
+Arguments Build_UInternalFunction' {var_t fn_name_t action}
+          uint_name uint_argspec uint_retSig uint_body : assert.
+
+Definition map_uintf_body {var_t fn_name_t action action': Type}
+           (f: action -> action') (fn: UInternalFunction' var_t fn_name_t action) :=
+  {| uint_name := fn.(uint_name);
+     uint_argspec := fn.(uint_argspec);
+     uint_retSig := fn.(uint_retSig);
+     uint_body := f fn.(uint_body) |}.
+
+Record InternalFunction' {fn_name_t action: Type} :=
   { int_name : fn_name_t;
-    int_argspec : tsig var_t;
-    int_retSig : type;
     int_body : action }.
-Arguments InternalFunction : clear implicits.
-Arguments Build_InternalFunction {var_t fn_name_t action}
-          int_name int_argspec int_retSig int_body : assert.
-
-Definition map_intf_body {var_t fn_name_t action action': Type}
-           (f: action -> action') (fn: InternalFunction var_t fn_name_t action) :=
-  {| int_name := fn.(int_name);
-     int_argspec := fn.(int_argspec);
-     int_retSig := fn.(int_retSig);
-     int_body := f fn.(int_body) |}.
+Arguments InternalFunction' : clear implicits.
+Arguments Build_InternalFunction' {fn_name_t action}
+          int_name int_body : assert.
 
 Record arg_sig {var_t} :=
   { arg_name: var_t;
diff --git a/ocaml/backends/coq.ml b/ocaml/backends/coq.ml
index ca167028..02cae9fc 100644
--- a/ocaml/backends/coq.ml
+++ b/ocaml/backends/coq.ml
@@ -143,11 +143,11 @@ let pp_external_sig ppf f =
 let pp_internal_sig_arg ppf (nm, tau) =
   fprintf ppf "@[%a@ :: %a@]" pp_quoted nm (pp_type ~wrap:false) tau
 
-let pp_internal_function ppf (f: _ internal_function) =
+let pp_uinternal_function ppf (f: _ uinternal_function) =
   fprintf ppf "{{{ %a | %a ~> %a }}}"
-    pp_quoted f.int_name
-    (pp_seq (pp_sep " ~> ") pp_internal_sig_arg) f.int_argspec
-    (pp_type ~wrap:false) f.int_retSig
+    pp_quoted f.uint_name
+    (pp_seq (pp_sep " ~> ") pp_internal_sig_arg) f.uint_argspec
+    (pp_type ~wrap:false) f.uint_retSig
 
 let pp_ext_fn_Sigma ppf (extfuns: ffi_signature list) =
   fprintf ppf "@[<hv 2>Definition Sigma (f: ext_fn_t): ExternalSignature :=@ %a@]."
@@ -318,7 +318,7 @@ let rec pp_action print_positions ppf (a: ResolvedAST.uaction locd) =
     | ExternalCall { fn; arg } ->
        pp_app "UExternalCall" "%a@ %a" pp_raw fn.lcnt.ffi_name pp_action arg
     | InternalCall { fn; args } ->
-       pp_app "UInternalCall" "%a@ %a" pp_raw fn.int_name (pp_list pp_action) args
+       pp_app "UInternalCall" "%a@ %a" pp_raw fn.uint_name (pp_list pp_action) args
     | Sugar u -> pp_app "USugar" "%a" pp_sugar u
   and pp_sugar ppf u =
     let pp_app fn fmt = pp_app ppf fn fmt in
@@ -367,13 +367,13 @@ let pp_scheduler print_positions ppf (name, scheduler) =
   fprintf ppf "@[<2>Definition %s_eval (sigma: forall f, Sigma f)@ : Log R ContextEnv :=@ " name;
   fprintf ppf "@[<2>interp_scheduler@ (ContextEnv.(create) r)@ sigma@ rules@ %s@].@]" name
 
-let pp_int_fn ~print_positions ppf (_, { int_name; int_argspec; int_retSig; int_body }) =
+let pp_int_fn ~print_positions ppf (_, { uint_name; uint_argspec; uint_retSig; uint_body }) =
   let p fmt = fprintf ppf fmt in
-  p "@[<v>@[<hv 2>Definition %s {reg_t ext_fn_t} : UInternalFunction reg_t ext_fn_t := {|@ " int_name;
-  p "int_name := %a;@ " pp_quoted int_name;
-  p "int_argspec := %a;@ " (pp_list (pp_pair pp_quoted pp_type_unwrapped)) int_argspec;
-  p "int_retSig := %a;@ " pp_type_unwrapped int_retSig;
-  p "int_body := %a;" (pp_action print_positions) int_body;
+  p "@[<v>@[<hv 2>Definition %s {reg_t ext_fn_t} : UInternalFunction reg_t ext_fn_t := {|@ " uint_name;
+  p "uint_name := %a;@ " pp_quoted uint_name;
+  p "uint_argspec := %a;@ " (pp_list (pp_pair pp_quoted pp_type_unwrapped)) uint_argspec;
+  p "uint_retSig := %a;@ " pp_type_unwrapped uint_retSig;
+  p "uint_body := %a;" (pp_action print_positions) uint_body;
   p "@]@ |}.@]"
 
 let pp_tc_rules ppf (rules: (string * _) list) =
diff --git a/ocaml/backends/cpp.ml b/ocaml/backends/cpp.ml
index 3100ca61..cb9c23d1 100644
--- a/ocaml/backends/cpp.ml
+++ b/ocaml/backends/cpp.ml
@@ -1114,11 +1114,11 @@ them before writing to the registers.\n"
         let bindings, body = loop pos [] action in
         List.rev bindings, body in
 
-      let package_intfun fn argspec tau body =
-        { Extr.int_name = hpp.cpp_fn_names fn;
-          Extr.int_argspec = argspec;
-          Extr.int_retSig = tau;
-          Extr.int_body = body } in
+      let package_intfun fn argspec tau =
+        { Extr.uint_name = hpp.cpp_fn_names fn.Extr.int_name;
+          Extr.uint_argspec = argspec;
+          Extr.uint_retSig = tau;
+          Extr.uint_body = fn.Extr.int_body } in
 
       (* Table mapping function objects to unique names.  This is reset for each
          rules, because each implementation of a function is specific to one
@@ -1126,8 +1126,8 @@ them before writing to the registers.\n"
          to invoke a rule-specific reset function *)
       let internal_functions = Hashtbl.create 20 in
 
-      let lookup_intfun fn argspec tau body =
-        let intf = package_intfun fn argspec tau body in
+      let lookup_intfun fn argspec tau =
+        let intf = package_intfun fn argspec tau in
         intf, Hashtbl.find_opt internal_functions intf in
 
       let rec p_action
@@ -1229,8 +1229,8 @@ them before writing to the registers.\n"
            (* See ‘Read’ case for why returning just ImpureExpr isn't safe *)
            let expr = cpp_ext_funcall ffi.ffi_name kind (must_value a) in
            p_assign_impure target (ImpureExpr expr)
-        | Extr.InternalCall (_, tau, fn, argspec, rev_args, body) ->
-           let fn_name = match snd (lookup_intfun fn argspec tau body) with
+        | Extr.InternalCall (_, tau, argspec, fn, rev_args) ->
+           let fn_name = match snd (lookup_intfun fn argspec tau) with
              | Some fn -> fn
              | None -> assert false in
            let args = Extr.cfoldl (fun (argname, tau) arg argstrs ->
@@ -1314,15 +1314,15 @@ them before writing to the registers.\n"
             else
               loop (counter + 1) in
           loop 0 in
-        let register_intfun pos fn argspec tau body =
+        let register_intfun pos fn argspec tau =
           assert_no_duplicates ~descr:"argument list"
             (List.map (fun (v, _) -> hpp.cpp_var_names v) argspec);
-          match lookup_intfun fn argspec tau body with
+          match lookup_intfun fn argspec tau with
           | _, Some _ -> ()
           | intf, None ->
-             let nm = ensure_fresh (hpp.cpp_fn_names fn) in
+             let nm = ensure_fresh (hpp.cpp_fn_names fn.Extr.int_name) in
              fns := (pos, nm, intf) :: !fns;
-             Hashtbl.add internal_functions intf nm in
+             Hashtbl.add internal_functions intf nm; in
         let rec loop pos = function
           | Extr.Fail _
             | Extr.Var _
@@ -1343,10 +1343,10 @@ them before writing to the registers.\n"
              loop pos c;
              loop pos tbr;
              loop pos fbr
-          | Extr.InternalCall (_, tau, fn, argspec, rev_args, body) ->
-             register_intfun pos fn argspec tau body;
+          | Extr.InternalCall (_, tau, argspec, fn, rev_args) ->
+             register_intfun pos fn argspec tau;
              Extr.cfoldr (fun _ _ arg () -> loop pos arg) argspec rev_args ();
-             loop pos body in
+             loop pos fn.Extr.int_body in
         loop pos action;
         List.rev !fns in
 
@@ -1354,14 +1354,14 @@ them before writing to the registers.\n"
         let sp_arg (nm, tau) =
           let tau = Cuttlebone.Util.typ_of_extr_type tau in
           sprintf "%s %s" (cpp_type_of_type tau) (hpp.cpp_var_names nm) in
-        let ret_tau = Cuttlebone.Util.typ_of_extr_type intf.Extr.int_retSig in
+        let ret_tau = Cuttlebone.Util.typ_of_extr_type intf.Extr.uint_retSig in
         let ret_type = cpp_type_of_type ret_tau in
         let ret_arg = sprintf "%s %s" ret_type "&_ret" in
-        let args = String.concat ", " @@ name :: ret_arg :: List.map sp_arg intf.Extr.int_argspec in
+        let args = String.concat ", " @@ name :: ret_arg :: List.map sp_arg intf.Extr.uint_argspec in
         p "DECL_FN(%s, %s)" name ret_type;
         p_special_fn "FN" ~args (fun () ->
             let target = VarTarget { tau = ret_tau; declared = true; name = "_ret" } in
-            p_assign_and_ignore target (p_action true pos target intf.int_body);
+            p_assign_and_ignore target (p_action true pos target intf.uint_body);
             p "return true;") in
 
       p "#define RULE_NAME %s" rule_name_unprefixed;
diff --git a/ocaml/common/common.ml b/ocaml/common/common.ml
index f15ec920..0f9710db 100644
--- a/ocaml/common/common.ml
+++ b/ocaml/common/common.ml
@@ -250,11 +250,11 @@ let locd_make lpos lcnt =
 let locd_of_pair (pos, x) =
   locd_make pos x
 
-type 'action internal_function = {
-    int_name: string;
-    int_argspec: (string * typ) list;
-    int_retSig: typ;
-    int_body: 'action
+type 'action uinternal_function = {
+    uint_name: string;
+    uint_argspec: (string * typ) list;
+    uint_retSig: typ;
+    uint_body: 'action
   }
 
 let with_output_to_file fname (f: out_channel -> 'a -> unit) (data: 'a) =
diff --git a/ocaml/cuttlebone/cuttlebone.ml b/ocaml/cuttlebone/cuttlebone.ml
index ce3fb940..9c0f8fc0 100644
--- a/ocaml/cuttlebone/cuttlebone.ml
+++ b/ocaml/cuttlebone/cuttlebone.ml
@@ -92,17 +92,17 @@ module Util = struct
     Extr.{ argSigs = Extr.vect_of_list [extr_type_of_typ ffi_argtype];
           retSig = extr_type_of_typ ffi_rettype }
 
-  let extr_intfun_of_intfun fbody (fsig: _ Common.internal_function) =
-    { Extr.int_name = fsig.int_name;
-      Extr.int_argspec = List.map (fun (nm, tau) -> nm, extr_type_of_typ tau) fsig.int_argspec;
-      Extr.int_retSig = extr_type_of_typ fsig.int_retSig;
-      Extr.int_body = fbody fsig.int_body }
-
-  let intfun_of_extr_intfun fbody (fsig: _ Extr.internalFunction) =
-    { int_name = fsig.int_name;
-      int_argspec = List.map (fun (nm, tau) -> nm, typ_of_extr_type tau) fsig.int_argspec;
-      int_retSig = typ_of_extr_type fsig.int_retSig;
-      int_body = fbody fsig.int_body }
+  let extr_uintfun_of_uintfun fbody (fsig: _ Common.uinternal_function) =
+    { Extr.uint_name = fsig.uint_name;
+      Extr.uint_argspec = List.map (fun (nm, tau) -> nm, extr_type_of_typ tau) fsig.uint_argspec;
+      Extr.uint_retSig = extr_type_of_typ fsig.uint_retSig;
+      Extr.uint_body = fbody fsig.uint_body }
+
+  let uintfun_of_extr_uintfun fbody (fsig: _ Extr.uInternalFunction') =
+    { uint_name = fsig.uint_name;
+      uint_argspec = List.map (fun (nm, tau) -> nm, typ_of_extr_type tau) fsig.uint_argspec;
+      uint_retSig = typ_of_extr_type fsig.uint_retSig;
+      uint_body = fbody fsig.uint_body }
 
   let extr_type_to_string tau =
     typ_to_string (typ_of_extr_type tau)
diff --git a/ocaml/frontends/lv.ml b/ocaml/frontends/lv.ml
index cad77351..44287c97 100644
--- a/ocaml/frontends/lv.ml
+++ b/ocaml/frontends/lv.ml
@@ -83,7 +83,7 @@ module ResolvedAST = struct
     | Unop of { fn: (Extr.PrimUntyped.ufn1) locd; arg: uaction locd }
     | Binop of { fn: (Extr.PrimUntyped.ufn2) locd; a1: uaction locd; a2: uaction locd }
     | ExternalCall of { fn: ffi_signature locd; arg: uaction locd }
-    | InternalCall of { fn: uaction locd internal_function; args: uaction locd list }
+    | InternalCall of { fn: uaction locd uinternal_function; args: uaction locd list }
     | Sugar of usugar
   and usugar =
     | AstError
@@ -116,7 +116,7 @@ module ResolvedAST = struct
        | ExternalCall { fn; arg } -> UExternalCall (fn.lcnt, translate_action arg)
        | InternalCall { fn; args } ->
           UInternalCall
-            (Util.extr_intfun_of_intfun translate_action fn,
+            (Util.extr_uintfun_of_uintfun translate_action fn,
              List.map translate_action args)
        | Sugar u ->
           Extr.USugar
@@ -198,7 +198,7 @@ type unresolved_unit = {
 type resolved_extfun = ffi_signature
 
 type resolved_defun =
-  ResolvedAST.uaction locd internal_function
+  ResolvedAST.uaction locd uinternal_function
 
 type resolved_fn =
   | FnExternal of ffi_signature
@@ -1605,10 +1605,10 @@ let resolve_fn_decl types fns { ufn_name; ufn_signature; ufn_rettype; ufn_body }
    match ufn_body with
    | InternalUfn body ->
       let body = resolve_action types fns [] body in
-      InternalDecl { int_name = ufn_name.lcnt;
-                     int_retSig = rettype;
-                     int_argspec = args;
-                     int_body = body }
+      InternalDecl { uint_name = ufn_name.lcnt;
+                     uint_retSig = rettype;
+                     uint_argspec = args;
+                     uint_body = body }
    | ExternalUfn ->
       let unit_t = Bits_t 0 in
       let ffi_argtype = match List.map snd args with

From 58373fc674c9973199efbfd323173ccb412ca534 Mon Sep 17 00:00:00 2001
From: Max Kurze <Max.Kurze@mailbox.tu-dresden.de>
Date: Sat, 9 Nov 2024 13:43:42 +0100
Subject: [PATCH 4/4] refactor(syntax): rename 'retSig' to 'retType'

---
 coq/Frontend.v                 | 2 +-
 coq/SyntaxMacros.v             | 8 ++++----
 coq/TypeInference.v            | 2 +-
 coq/Types.v                    | 6 +++---
 ocaml/backends/coq.ml          | 6 +++---
 ocaml/backends/cpp.ml          | 4 ++--
 ocaml/common/common.ml         | 2 +-
 ocaml/cuttlebone/cuttlebone.ml | 4 ++--
 ocaml/frontends/lv.ml          | 2 +-
 9 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/coq/Frontend.v b/coq/Frontend.v
index cafa9b6d..d99b063b 100644
--- a/coq/Frontend.v
+++ b/coq/Frontend.v
@@ -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 (uint_argspec uf) (uint_retSig uf) (uint_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
diff --git a/coq/SyntaxMacros.v b/coq/SyntaxMacros.v
index ad789545..e1f407ac 100644
--- a/coq/SyntaxMacros.v
+++ b/coq/SyntaxMacros.v
@@ -155,7 +155,7 @@ Module Display.
     Definition empty_printer : intfun :=
       {| uint_name := "print";
          uint_argspec := [];
-         uint_retSig := unit_t;
+         uint_retType := unit_t;
          uint_body := USugar USkip |}.
 
     Definition display_utf8 s : uaction :=
@@ -164,7 +164,7 @@ Module Display.
     Definition nl_printer : intfun :=
       {| uint_name := "print_nl";
          uint_argspec := [];
-         uint_retSig := unit_t;
+         uint_retType := unit_t;
          uint_body := display_utf8 "\n" |}.
 
     Definition extend_printer f (offset: nat) (printer: intfun) : intfun :=
@@ -176,13 +176,13 @@ Module Display.
       | Str s =>
         {| uint_name    := printer.(uint_name);
            uint_argspec := printer.(uint_argspec);
-           uint_retSig  := printer.(uint_retSig);
+           uint_retType  := printer.(uint_retType);
            uint_body    := (USeq (display_utf8 s) printer.(uint_body)) |}
       | Value tau =>
         let arg := String.append "arg" (show offset) in
         {| uint_name    := printer.(uint_name);
-           uint_retSig  := unit_t;
            uint_argspec := (arg, tau) :: printer.(uint_argspec);
+           uint_retType  := unit_t;
            uint_body    := (USeq (display_value arg) printer.(uint_body)) |}
       end.
 
diff --git a/coq/TypeInference.v b/coq/TypeInference.v
index 426d391d..b9cc650c 100644
--- a/coq/TypeInference.v
+++ b/coq/TypeInference.v
@@ -149,7 +149,7 @@ Section TypeInference.
         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.(uint_body)) (List.rev fn.(uint_argspec)) fn.(uint_body) in
-        let/res fn_body' := cast_action (actpos pos fn.(uint_body)) fn.(uint_retSig) (``fn_body') in
+        let/res fn_body' := cast_action (actpos pos fn.(uint_body)) fn.(uint_retType) (``fn_body') in
 
         Success (EX (TypedSyntax.InternalCall {|
           int_name := fn.(uint_name);
diff --git a/coq/Types.v b/coq/Types.v
index 2fb3acc9..092a5c2e 100644
--- a/coq/Types.v
+++ b/coq/Types.v
@@ -292,17 +292,17 @@ Definition lsig := list nat.
 Record UInternalFunction' {var_t fn_name_t action: Type} :=
   { uint_name : fn_name_t;
     uint_argspec : tsig var_t;
-    uint_retSig : type;
+    uint_retType : type;
     uint_body : action }.
 Arguments UInternalFunction' : clear implicits.
 Arguments Build_UInternalFunction' {var_t fn_name_t action}
-          uint_name uint_argspec uint_retSig uint_body : assert.
+          uint_name uint_argspec uint_retType uint_body : assert.
 
 Definition map_uintf_body {var_t fn_name_t action action': Type}
            (f: action -> action') (fn: UInternalFunction' var_t fn_name_t action) :=
   {| uint_name := fn.(uint_name);
      uint_argspec := fn.(uint_argspec);
-     uint_retSig := fn.(uint_retSig);
+     uint_retType := fn.(uint_retType);
      uint_body := f fn.(uint_body) |}.
 
 Record InternalFunction' {fn_name_t action: Type} :=
diff --git a/ocaml/backends/coq.ml b/ocaml/backends/coq.ml
index 02cae9fc..686033d3 100644
--- a/ocaml/backends/coq.ml
+++ b/ocaml/backends/coq.ml
@@ -147,7 +147,7 @@ let pp_uinternal_function ppf (f: _ uinternal_function) =
   fprintf ppf "{{{ %a | %a ~> %a }}}"
     pp_quoted f.uint_name
     (pp_seq (pp_sep " ~> ") pp_internal_sig_arg) f.uint_argspec
-    (pp_type ~wrap:false) f.uint_retSig
+    (pp_type ~wrap:false) f.uint_retType
 
 let pp_ext_fn_Sigma ppf (extfuns: ffi_signature list) =
   fprintf ppf "@[<hv 2>Definition Sigma (f: ext_fn_t): ExternalSignature :=@ %a@]."
@@ -367,12 +367,12 @@ let pp_scheduler print_positions ppf (name, scheduler) =
   fprintf ppf "@[<2>Definition %s_eval (sigma: forall f, Sigma f)@ : Log R ContextEnv :=@ " name;
   fprintf ppf "@[<2>interp_scheduler@ (ContextEnv.(create) r)@ sigma@ rules@ %s@].@]" name
 
-let pp_int_fn ~print_positions ppf (_, { uint_name; uint_argspec; uint_retSig; uint_body }) =
+let pp_int_fn ~print_positions ppf (_, { uint_name; uint_argspec; uint_retType; uint_body }) =
   let p fmt = fprintf ppf fmt in
   p "@[<v>@[<hv 2>Definition %s {reg_t ext_fn_t} : UInternalFunction reg_t ext_fn_t := {|@ " uint_name;
   p "uint_name := %a;@ " pp_quoted uint_name;
   p "uint_argspec := %a;@ " (pp_list (pp_pair pp_quoted pp_type_unwrapped)) uint_argspec;
-  p "uint_retSig := %a;@ " pp_type_unwrapped uint_retSig;
+  p "uint_retType := %a;@ " pp_type_unwrapped uint_retType;
   p "uint_body := %a;" (pp_action print_positions) uint_body;
   p "@]@ |}.@]"
 
diff --git a/ocaml/backends/cpp.ml b/ocaml/backends/cpp.ml
index cb9c23d1..66330c44 100644
--- a/ocaml/backends/cpp.ml
+++ b/ocaml/backends/cpp.ml
@@ -1117,7 +1117,7 @@ them before writing to the registers.\n"
       let package_intfun fn argspec tau =
         { Extr.uint_name = hpp.cpp_fn_names fn.Extr.int_name;
           Extr.uint_argspec = argspec;
-          Extr.uint_retSig = tau;
+          Extr.uint_retType = tau;
           Extr.uint_body = fn.Extr.int_body } in
 
       (* Table mapping function objects to unique names.  This is reset for each
@@ -1354,7 +1354,7 @@ them before writing to the registers.\n"
         let sp_arg (nm, tau) =
           let tau = Cuttlebone.Util.typ_of_extr_type tau in
           sprintf "%s %s" (cpp_type_of_type tau) (hpp.cpp_var_names nm) in
-        let ret_tau = Cuttlebone.Util.typ_of_extr_type intf.Extr.uint_retSig in
+        let ret_tau = Cuttlebone.Util.typ_of_extr_type intf.Extr.uint_retType in
         let ret_type = cpp_type_of_type ret_tau in
         let ret_arg = sprintf "%s %s" ret_type "&_ret" in
         let args = String.concat ", " @@ name :: ret_arg :: List.map sp_arg intf.Extr.uint_argspec in
diff --git a/ocaml/common/common.ml b/ocaml/common/common.ml
index 0f9710db..262431e9 100644
--- a/ocaml/common/common.ml
+++ b/ocaml/common/common.ml
@@ -253,7 +253,7 @@ let locd_of_pair (pos, x) =
 type 'action uinternal_function = {
     uint_name: string;
     uint_argspec: (string * typ) list;
-    uint_retSig: typ;
+    uint_retType: typ;
     uint_body: 'action
   }
 
diff --git a/ocaml/cuttlebone/cuttlebone.ml b/ocaml/cuttlebone/cuttlebone.ml
index 9c0f8fc0..e733bb2f 100644
--- a/ocaml/cuttlebone/cuttlebone.ml
+++ b/ocaml/cuttlebone/cuttlebone.ml
@@ -95,13 +95,13 @@ module Util = struct
   let extr_uintfun_of_uintfun fbody (fsig: _ Common.uinternal_function) =
     { Extr.uint_name = fsig.uint_name;
       Extr.uint_argspec = List.map (fun (nm, tau) -> nm, extr_type_of_typ tau) fsig.uint_argspec;
-      Extr.uint_retSig = extr_type_of_typ fsig.uint_retSig;
+      Extr.uint_retType = extr_type_of_typ fsig.uint_retType;
       Extr.uint_body = fbody fsig.uint_body }
 
   let uintfun_of_extr_uintfun fbody (fsig: _ Extr.uInternalFunction') =
     { uint_name = fsig.uint_name;
       uint_argspec = List.map (fun (nm, tau) -> nm, typ_of_extr_type tau) fsig.uint_argspec;
-      uint_retSig = typ_of_extr_type fsig.uint_retSig;
+      uint_retType = typ_of_extr_type fsig.uint_retType;
       uint_body = fbody fsig.uint_body }
 
   let extr_type_to_string tau =
diff --git a/ocaml/frontends/lv.ml b/ocaml/frontends/lv.ml
index 44287c97..59a33394 100644
--- a/ocaml/frontends/lv.ml
+++ b/ocaml/frontends/lv.ml
@@ -1606,7 +1606,7 @@ let resolve_fn_decl types fns { ufn_name; ufn_signature; ufn_rettype; ufn_body }
    | InternalUfn body ->
       let body = resolve_action types fns [] body in
       InternalDecl { uint_name = ufn_name.lcnt;
-                     uint_retSig = rettype;
+                     uint_retType = rettype;
                      uint_argspec = args;
                      uint_body = body }
    | ExternalUfn ->