refactor(syntax): rename 'retSig' to 'retType'

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

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.
 

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);

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} :=

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 "@]@ |}.@]"
 

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

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
   }
 

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 =

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 ->