Perform some renamings

10 files changed, 76 insertions, 83 deletions

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 19e17260..e00a4e53 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -872,12 +872,11 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       (* Top-level qualifier *)
       match qualif.id with
       | Func fun_id ->
-          extract_function_call ctx fmt inside fun_id qualif.type_params args
+          extract_function_call ctx fmt inside fun_id qualif.type_args args
       | AdtCons adt_cons_id ->
-          extract_adt_cons ctx fmt inside adt_cons_id qualif.type_params args
+          extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args args
       | Proj proj ->
-          extract_field_projector ctx fmt inside app proj qualif.type_params
-            args)
+          extract_field_projector ctx fmt inside app proj qualif.type_args args)
   | _ ->
       (* "Regular" expression *)
       (* Open parentheses *)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index c3331de5..e8e9c6c4 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -994,18 +994,18 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
   *)
   match call.func with
   | A.Regular fid ->
-      eval_local_function_call config fid call.region_params call.type_params
+      eval_local_function_call config fid call.region_args call.type_args
         call.args call.dest
   | A.Assumed fid ->
-      eval_non_local_function_call config fid call.region_params
-        call.type_params call.args call.dest
+      eval_non_local_function_call config fid call.region_args call.type_args
+        call.args call.dest
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
 and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
-    (region_params : T.erased_region list) (type_params : T.ety list)
+    (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
-  assert (region_params = []);
+  assert (region_args = []);
 
   (* Retrieve the (correctly instantiated) body *)
   let def = C.ctx_lookup_fun_decl ctx fid in
@@ -1022,7 +1022,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
   let tsubst =
     Subst.make_type_subst
       (List.map (fun v -> v.T.index) def.A.signature.type_params)
-      type_params
+      type_args
   in
   let locals, body_st = Subst.fun_body_substitute_in_body tsubst body in
 
@@ -1080,7 +1080,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
 
 (** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
 and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
-    (region_params : T.erased_region list) (type_params : T.ety list)
+    (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
   (* Retrieve the (correctly instantiated) signature *)
@@ -1088,12 +1088,12 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
   let sg = def.A.signature in
   (* Instantiate the signature and introduce fresh abstraction and region ids
    * while doing so *)
-  let inst_sg = instantiate_fun_sig type_params sg in
+  let inst_sg = instantiate_fun_sig type_args sg in
   (* Sanity check *)
   assert (List.length args = List.length def.A.signature.inputs);
   (* Evaluate the function call *)
   eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg
-    region_params type_params args dest cf ctx
+    region_args type_args args dest cf ctx
 
 (** Evaluate a function call in symbolic mode by using the function signature.
 
@@ -1102,10 +1102,10 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
  *)
 and eval_function_call_symbolic_from_inst_sig (config : C.config)
     (fid : A.fun_id) (inst_sg : A.inst_fun_sig)
-    (region_params : T.erased_region list) (type_params : T.ety list)
+    (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
-  assert (region_params = []);
+  assert (region_args = []);
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.A.output in
   let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in
@@ -1169,7 +1169,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
 
     (* Synthesize the symbolic AST *)
     let abs_ids = List.map (fun rg -> rg.T.id) inst_sg.regions_hierarchy in
-    S.synthesize_regular_function_call fid call_id abs_ids type_params args
+    S.synthesize_regular_function_call fid call_id abs_ids type_args args
       args_places ret_spc dest_place expr
   in
   let cc = comp cc cf_call in
@@ -1185,8 +1185,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
 
 (** Evaluate a non-local function call in symbolic mode *)
 and eval_non_local_function_call_symbolic (config : C.config)
-    (fid : A.assumed_fun_id) (region_params : T.erased_region list)
-    (type_params : T.ety list) (args : E.operand list) (dest : E.place) :
+    (fid : A.assumed_fun_id) (region_args : T.erased_region list)
+    (type_args : T.ety list) (args : E.operand list) (dest : E.place) :
     st_cm_fun =
  fun cf ctx ->
   (* Sanity check: make sure the type parameters don't contain regions -
@@ -1194,7 +1194,7 @@ and eval_non_local_function_call_symbolic (config : C.config)
   assert (
     List.for_all
       (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty))
-      type_params);
+      type_args);
 
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
@@ -1205,7 +1205,7 @@ and eval_non_local_function_call_symbolic (config : C.config)
   | A.BoxFree ->
       (* Degenerate case: box_free - note that this is not really a function
        * call: no need to call a "synthesize_..." function *)
-      eval_box_free config region_params type_params args dest (cf Unit) ctx
+      eval_box_free config region_args type_args args dest (cf Unit) ctx
   | _ ->
       (* "Normal" case: not box_free *)
       (* In symbolic mode, the behaviour of a function call is completely defined
@@ -1216,55 +1216,53 @@ and eval_non_local_function_call_symbolic (config : C.config)
         | A.BoxFree ->
             (* should have been treated above *)
             raise (Failure "Unreachable")
-        | _ -> instantiate_fun_sig type_params (Assumed.get_assumed_sig fid)
+        | _ -> instantiate_fun_sig type_args (Assumed.get_assumed_sig fid)
       in
 
       (* Evaluate the function call *)
       eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig
-        region_params type_params args dest cf ctx
+        region_args type_args args dest cf ctx
 
 (** Evaluate a non-local (i.e, assumed) function call such as `Box::deref`
     (auxiliary helper for [eval_statement]) *)
 and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
-    (region_params : T.erased_region list) (type_params : T.ety list)
+    (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
  fun cf ctx ->
   (* Debug *)
   log#ldebug
     (lazy
-      (let type_params =
-         "["
-         ^ String.concat ", " (List.map (ety_to_string ctx) type_params)
-         ^ "]"
+      (let type_args =
+         "[" ^ String.concat ", " (List.map (ety_to_string ctx) type_args) ^ "]"
        in
        let args =
          "[" ^ String.concat ", " (List.map (operand_to_string ctx) args) ^ "]"
        in
        let dest = place_to_string ctx dest in
        "eval_non_local_function_call:\n- fid:" ^ A.show_assumed_fun_id fid
-       ^ "\n- type_params: " ^ type_params ^ "\n- args: " ^ args ^ "\n- dest: "
+       ^ "\n- type_args: " ^ type_args ^ "\n- args: " ^ args ^ "\n- dest: "
        ^ dest));
 
   match config.mode with
   | C.ConcreteMode ->
-      eval_non_local_function_call_concrete config fid region_params type_params
+      eval_non_local_function_call_concrete config fid region_args type_args
         args dest (cf Unit) ctx
   | C.SymbolicMode ->
-      eval_non_local_function_call_symbolic config fid region_params type_params
+      eval_non_local_function_call_symbolic config fid region_args type_args
         args dest cf ctx
 
 (** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
     [eval_statement]) *)
 and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
-    (region_params : T.erased_region list) (type_params : T.ety list)
+    (region_args : T.erased_region list) (type_args : T.ety list)
     (args : E.operand list) (dest : E.place) : st_cm_fun =
   match config.mode with
   | ConcreteMode ->
-      eval_local_function_call_concrete config fid region_params type_params
-        args dest
+      eval_local_function_call_concrete config fid region_args type_args args
+        dest
   | SymbolicMode ->
-      eval_local_function_call_symbolic config fid region_params type_params
-        args dest
+      eval_local_function_call_symbolic config fid region_args type_args args
+        dest
 
 (** Evaluate a statement seen as a function body (auxiliary helper for
     [eval_statement]) *)
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index 6e77cadb..d35cd5d8 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -65,8 +65,8 @@ type inst_fun_sig = {
 
 type call = {
   func : fun_id;
-  region_params : erased_region list;
-  type_params : ety list;
+  region_args : erased_region list;
+  type_args : ety list;
   args : operand list;
   dest : place;
 }
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 7604ec2b..75e9cbf7 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -532,17 +532,17 @@ let call_of_json (js : json) : (A.call, string) result =
     | `Assoc
         [
           ("func", func);
-          ("region_params", region_params);
-          ("type_params", type_params);
+          ("region_args", region_args);
+          ("type_args", type_args);
           ("args", args);
           ("dest", dest);
         ] ->
         let* func = fun_id_of_json func in
-        let* region_params = list_of_json erased_region_of_json region_params in
-        let* type_params = list_of_json ety_of_json type_params in
+        let* region_args = list_of_json erased_region_of_json region_args in
+        let* type_args = list_of_json ety_of_json type_args in
         let* args = list_of_json operand_of_json args in
         let* dest = place_of_json dest in
-        Ok { A.func; region_params; type_params; args; dest }
+        Ok { A.func; region_args; type_args; args; dest }
     | _ -> Error "")
 
 let rec statement_of_json (js : json) : (A.statement, string) result =
diff --git a/src/Print.ml b/src/Print.ml
index 98e9dd74..fedc4122 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -953,41 +953,41 @@ module LlbcAst = struct
         else indent ^ "assert(¬" ^ cond ^ ")"
     | A.Call call ->
         let ty_fmt = ast_to_etype_formatter fmt in
-        let params =
-          if List.length call.A.type_params > 0 then
+        let t_params =
+          if List.length call.A.type_args > 0 then
             "<"
             ^ String.concat ","
-                (List.map (PT.ty_to_string ty_fmt) call.A.type_params)
+                (List.map (PT.ty_to_string ty_fmt) call.A.type_args)
             ^ ">"
           else ""
         in
         let args = List.map (operand_to_string fmt) call.A.args in
         let args = "(" ^ String.concat ", " args ^ ")" in
-        let name_params =
+        let name_args =
           match call.A.func with
-          | A.Regular fid -> fmt.fun_decl_id_to_string fid ^ params
+          | A.Regular fid -> fmt.fun_decl_id_to_string fid ^ t_params
           | A.Assumed fid -> (
               match fid with
-              | A.Replace -> "core::mem::replace" ^ params
-              | A.BoxNew -> "alloc::boxed::Box" ^ params ^ "::new"
+              | A.Replace -> "core::mem::replace" ^ t_params
+              | A.BoxNew -> "alloc::boxed::Box" ^ t_params ^ "::new"
               | A.BoxDeref ->
-                  "core::ops::deref::Deref<Box" ^ params ^ ">::deref"
+                  "core::ops::deref::Deref<Box" ^ t_params ^ ">::deref"
               | A.BoxDerefMut ->
-                  "core::ops::deref::DerefMut" ^ params ^ "::deref_mut"
-              | A.BoxFree -> "alloc::alloc::box_free" ^ params
-              | A.VecNew -> "alloc::vec::Vec" ^ params ^ "::new"
-              | A.VecPush -> "alloc::vec::Vec" ^ params ^ "::push"
-              | A.VecInsert -> "alloc::vec::Vec" ^ params ^ "::insert"
-              | A.VecLen -> "alloc::vec::Vec" ^ params ^ "::len"
+                  "core::ops::deref::DerefMut" ^ t_params ^ "::deref_mut"
+              | A.BoxFree -> "alloc::alloc::box_free" ^ t_params
+              | A.VecNew -> "alloc::vec::Vec" ^ t_params ^ "::new"
+              | A.VecPush -> "alloc::vec::Vec" ^ t_params ^ "::push"
+              | A.VecInsert -> "alloc::vec::Vec" ^ t_params ^ "::insert"
+              | A.VecLen -> "alloc::vec::Vec" ^ t_params ^ "::len"
               | A.VecIndex ->
-                  "core::ops::index::Index<alloc::vec::Vec" ^ params
+                  "core::ops::index::Index<alloc::vec::Vec" ^ t_params
                   ^ ">::index"
               | A.VecIndexMut ->
-                  "core::ops::index::IndexMut<alloc::vec::Vec" ^ params
+                  "core::ops::index::IndexMut<alloc::vec::Vec" ^ t_params
                   ^ ">::index_mut")
         in
         let dest = place_to_string fmt call.A.dest in
-        indent ^ dest ^ " := move " ^ name_params ^ args
+        indent ^ dest ^ " := move " ^ name_args ^ args
     | A.Panic -> indent ^ "panic"
     | A.Return -> indent ^ "return"
     | A.Break i -> indent ^ "break " ^ string_of_int i
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index e40a7b8b..b29f6e70 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -516,7 +516,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
         in
         (* Convert the type instantiation *)
         let ty_fmt = ast_to_type_formatter fmt in
-        let tys = List.map (ty_to_string ty_fmt) qualif.type_params in
+        let tys = List.map (ty_to_string ty_fmt) qualif.type_args in
         (* *)
         (qualif_s, tys)
     | _ ->
diff --git a/src/Pure.ml b/src/Pure.ml
index 05f7e199..3798c555 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -373,11 +373,7 @@ type qualif_id =
   | Proj of proj_kind  (** Field projector *)
 [@@deriving show]
 
-type qualif = {
-  id : qualif_id;
-  type_params : ty list; (* TODO: rename to type_args *)
-}
-[@@deriving show]
+type qualif = { id : qualif_id; type_args : ty list } [@@deriving show]
 (** An instantiated qualified.
 
     Note that for now we have a clear separation between types and expressions,
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 0d941079..96d84fb1 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -260,7 +260,7 @@ let opt_destruct_function_call (e : texpression) :
   | None -> None
   | Some (qualif, args) -> (
       match qualif.id with
-      | Func fun_id -> Some (fun_id, qualif.type_params, args)
+      | Func fun_id -> Some (fun_id, qualif.type_args, args)
       | _ -> None)
 
 let opt_destruct_result (ty : ty) : ty option =
@@ -344,7 +344,7 @@ let unit_ty : ty = Adt (Tuple, [])
 (** TODO: rename to "mk_unit_texpression" *)
 let unit_rvalue : texpression =
   let id = AdtCons { adt_id = Tuple; variant_id = None } in
-  let qualif = { id; type_params = [] } in
+  let qualif = { id; type_args = [] } in
   let e = Qualif qualif in
   let ty = unit_ty in
   { e; ty }
@@ -395,7 +395,7 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
       let ty = mk_arrows tys ty in
       (* Construct the tuple constructor qualifier *)
       let id = AdtCons { adt_id = Tuple; variant_id = None } in
-      let qualif = { id; type_params = tys } in
+      let qualif = { id; type_args = tys } in
       (* Put everything together *)
       let cons = { e = Qualif qualif; ty } in
       mk_apps cons vl
@@ -423,7 +423,7 @@ let mk_result_fail_rvalue (ty : ty) : texpression =
   let id =
     AdtCons { adt_id = Assumed Result; variant_id = Some result_fail_id }
   in
-  let qualif = { id; type_params = type_args } in
+  let qualif = { id; type_args } in
   let cons_e = Qualif qualif in
   let cons_ty = ty in
   let cons = { e = cons_e; ty = cons_ty } in
@@ -436,7 +436,7 @@ let mk_result_return_rvalue (v : texpression) : texpression =
   let id =
     AdtCons { adt_id = Assumed Result; variant_id = Some result_return_id }
   in
-  let qualif = { id; type_params = type_args } in
+  let qualif = { id; type_args } in
   let cons_e = Qualif qualif in
   let cons_ty = mk_arrow v.ty ty in
   let cons = { e = cons_e; ty = cons_ty } in
@@ -597,7 +597,7 @@ module TypeCheck = struct
             let variant_id = None in
             let expected_field_tys =
               get_adt_field_types ctx.type_decls adt_id variant_id
-                qualif.type_params
+                qualif.type_args
             in
             let expected_field_ty = FieldId.nth expected_field_tys field_id in
             let _adt_ty, field_ty = destruct_arrow e.ty in
@@ -607,7 +607,7 @@ module TypeCheck = struct
             (* TODO: we might also want to check the out type *)
             let expected_field_tys =
               get_adt_field_types ctx.type_decls id.adt_id id.variant_id
-                qualif.type_params
+                qualif.type_args
             in
             let field_tys, _ = destruct_arrows e.ty in
             assert (expected_field_tys = field_tys))
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 81f6985b..7cb0e8c2 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -262,15 +262,15 @@ let assertion_substitute (tsubst : T.TypeVarId.id -> T.ety) (a : A.assertion) :
 let call_substitute (tsubst : T.TypeVarId.id -> T.ety) (call : A.call) : A.call
     =
   let rsubst x = x in
-  let type_params = List.map (ty_substitute rsubst tsubst) call.A.type_params in
+  let type_args = List.map (ty_substitute rsubst tsubst) call.A.type_args in
   let args = List.map (operand_substitute tsubst) call.A.args in
   let dest = place_substitute tsubst call.A.dest in
   (* Putting all the paramters on purpose: we want to get a compiler error if
      something moves - we may add a field on which we need to apply a substitution *)
   {
     func = call.A.func;
-    region_params = call.A.region_params;
-    A.type_params;
+    region_args = call.A.region_args;
+    A.type_args;
     args;
     dest;
   }
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index e8f37f1e..64b3929f 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -648,7 +648,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (v : V.typed_value) :
             in
             (* Create the constructor *)
             let qualif_id = AdtCons { adt_id; variant_id = av.variant_id } in
-            let qualif = { id = qualif_id; type_params = type_args } in
+            let qualif = { id = qualif_id; type_args } in
             let cons_e = Qualif qualif in
             let field_tys =
               List.map (fun (v : texpression) -> v.ty) field_values
@@ -1088,7 +1088,7 @@ and translate_return (config : config) (opt_v : V.typed_value option)
 and translate_function_call (config : config) (call : S.call) (e : S.expression)
     (ctx : bs_ctx) : texpression =
   (* Translate the function call *)
-  let type_params = List.map (ctx_translate_fwd_ty ctx) call.type_params in
+  let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
   let args = List.map (typed_value_to_texpression ctx) call.args in
   let args_mplaces = List.map translate_opt_mplace call.args_places in
   let dest_mplace = translate_opt_mplace call.dest_place in
@@ -1127,7 +1127,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
       (List.combine args args_mplaces)
   in
   let dest_v = mk_typed_pattern_from_var dest dest_mplace in
-  let func = { id = Func fun_id; type_params } in
+  let func = { id = Func fun_id; type_args } in
   let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
   let ret_ty = mk_function_ret_ty config monadic state_monad dest_v.ty in
   let func_ty = mk_arrows input_tys ret_ty in
@@ -1197,7 +1197,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
   | V.FunCall ->
       let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
       let call = call_info.forward in
-      let type_params = List.map (ctx_translate_fwd_ty ctx) call.type_params in
+      let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
       (* Retrive the orignal call and the parent abstractions *)
       let forward, backwards = get_abs_ancestors ctx abs in
       (* Retrieve the values consumed when we called the forward function and
@@ -1232,7 +1232,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
       in
 
       let inst_sg =
-        get_instantiated_fun_sig fun_id (Some abs.back_id) type_params ctx
+        get_instantiated_fun_sig fun_id (Some abs.back_id) type_args ctx
       in
       List.iter
         (fun (x, ty) -> assert ((x : texpression).ty = ty))
@@ -1262,7 +1262,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
       let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
       let ret_ty = mk_function_ret_ty config monadic state_monad output.ty in
       let func_ty = mk_arrows input_tys ret_ty in
-      let func = { id = Func func; type_params } in
+      let func = { id = Func func; type_args } in
       let func = { e = Qualif func; ty = func_ty } in
       let call = mk_apps func args in
       (* **Optimization**:
@@ -1401,7 +1401,7 @@ and translate_expansion (config : config) (p : S.mplace option)
                  * field.
                  * We use the [dest] variable in order not to have to recompute
                  * the type of the result of the projection... *)
-                let adt_id, type_params =
+                let adt_id, type_args =
                   match scrutinee.ty with
                   | Adt (adt_id, tys) -> (adt_id, tys)
                   | _ -> raise (Failure "Unreachable")
@@ -1409,7 +1409,7 @@ and translate_expansion (config : config) (p : S.mplace option)
                 let gen_field_proj (field_id : FieldId.id) (dest : var) :
                     texpression =
                   let proj_kind = { adt_id; field_id } in
-                  let qualif = { id = Proj proj_kind; type_params } in
+                  let qualif = { id = Proj proj_kind; type_args } in
                   let proj_e = Qualif qualif in
                   let proj_ty = mk_arrow scrutinee.ty dest.ty in
                   let proj = { e = proj_e; ty = proj_ty } in