Remove the 'r type variable from the ty type definition

1 files changed, 54 insertions, 64 deletions

diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index e0c4703b..cdcea2cc 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -149,7 +149,7 @@ let eval_assertion_concrete (config : C.config) (assertion : A.assertion) :
   let eval_assert cf (v : V.typed_value) : m_fun =
    fun ctx ->
     match v.value with
-    | Literal (Bool b) ->
+    | VLiteral (VBool b) ->
         (* Branch *)
         if b = assertion.expected then cf Unit ctx else cf Panic ctx
     | _ ->
@@ -172,26 +172,26 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
   (* Evaluate the assertion *)
   let eval_assert cf (v : V.typed_value) : m_fun =
    fun ctx ->
-    assert (v.ty = T.Literal PV.Bool);
+    assert (v.ty = T.TLiteral PV.TBool);
     (* We make a choice here: we could completely decouple the concrete and
      * symbolic executions here but choose not to. In the case where we
      * know the concrete value of the boolean we test, we use this value
      * even if we are in symbolic mode. Note that this case should be
      * extremely rare... *)
     match v.value with
-    | Literal (Bool _) ->
+    | VLiteral (VBool _) ->
         (* Delegate to the concrete evaluation function *)
         eval_assertion_concrete config assertion cf ctx
     | Symbolic sv ->
         assert (config.mode = C.SymbolicMode);
-        assert (sv.V.sv_ty = T.Literal PV.Bool);
+        assert (sv.V.sv_ty = T.TLiteral PV.TBool);
         (* We continue the execution as if the test had succeeded, and thus
          * perform the symbolic expansion: sv ~~> true.
          * We will of course synthesize an assertion in the generated code
          * (see below). *)
         let ctx =
           apply_symbolic_expansion_non_borrow config sv
-            (V.SeLiteral (PV.Bool true)) ctx
+            (V.SeLiteral (PV.VBool true)) ctx
         in
         (* Continue *)
         let expr = cf Unit ctx in
@@ -232,7 +232,7 @@ let set_discriminant (config : C.config) (p : E.place)
   let update_value cf (v : V.typed_value) : m_fun =
    fun ctx ->
     match (v.V.ty, v.V.value) with
-    | T.Adt ((T.AdtId _ as type_id), generics), V.Adt av -> (
+    | T.TAdt ((T.AdtId _ as type_id), generics), V.VAdt av -> (
         (* There are two situations:
            - either the discriminant is already the proper one (in which case we
              don't do anything)
@@ -254,7 +254,7 @@ let set_discriminant (config : C.config) (p : E.place)
                 | _ -> raise (Failure "Unreachable")
               in
               assign_to_place config bottom_v p (cf Unit) ctx)
-    | T.Adt ((T.AdtId _ as type_id), generics), V.Bottom ->
+    | T.TAdt ((T.AdtId _ as type_id), generics), V.Bottom ->
         let bottom_v =
           match type_id with
           | T.AdtId def_id ->
@@ -273,8 +273,8 @@ let set_discriminant (config : C.config) (p : E.place)
          * setting a discriminant should only be used to initialize a value,
          * or reset an already initialized value, really. *)
         raise (Failure "Unexpected value")
-    | _, (V.Adt _ | V.Bottom) -> raise (Failure "Inconsistent state")
-    | _, (V.Literal _ | V.Borrow _ | V.Loan _) ->
+    | _, (V.VAdt _ | V.Bottom) -> raise (Failure "Inconsistent state")
+    | _, (V.VLiteral _ | V.Borrow _ | V.Loan _) ->
         raise (Failure "Unexpected value")
   in
   (* Compose and apply *)
@@ -282,7 +282,7 @@ let set_discriminant (config : C.config) (p : E.place)
 
 (** Push a frame delimiter in the context's environment *)
 let ctx_push_frame (ctx : C.eval_ctx) : C.eval_ctx =
-  { ctx with env = Frame :: ctx.env }
+  { ctx with env = EFrame :: ctx.env }
 
 (** Push a frame delimiter in the context's environment *)
 let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx)
@@ -291,7 +291,7 @@ let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx)
     instantiation of an assumed function.
  *)
 let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id)
-    (generics : T.egeneric_args) : T.ety =
+    (generics : T.generic_args) : T.ety =
   assert (generics.trait_refs = []);
   (* [Box::free] has a special treatment *)
   match fid with
@@ -305,17 +305,16 @@ let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id)
       let sg = Assumed.get_assumed_fun_sig fid in
       (* Instantiate the return type  *)
       (* There shouldn't be any reference to Self *)
-      let tr_self : T.erased_region T.trait_instance_id =
-        T.UnknownTrait __FUNCTION__
-      in
+      let tr_self : T.trait_instance_id = T.UnknownTrait __FUNCTION__ in
+      let generics = Subst.generic_args_erase_regions generics in
       let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
-        Subst.make_esubst_from_generics sg.generics generics tr_self
+        Subst.make_subst_from_generics sg.generics generics tr_self
       in
       let ty =
         Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
           sg.output
       in
-      Assoc.ctx_normalize_ety ctx ty
+      Assoc.ctx_normalize_erase_ty ctx ty
 
 let move_return_value (config : C.config) (pop_return_value : bool)
     (cf : V.typed_value option -> m_fun) : m_fun =
@@ -337,12 +336,12 @@ let pop_frame (config : C.config) (pop_return_value : bool)
   let rec list_locals env =
     match env with
     | [] -> raise (Failure "Inconsistent environment")
-    | C.Abs _ :: env -> list_locals env
-    | C.Var (DummyBinder _, _) :: env -> list_locals env
-    | C.Var (VarBinder var, _) :: env ->
+    | C.EAbs _ :: env -> list_locals env
+    | C.EBinding (BDummy _, _) :: env -> list_locals env
+    | C.EBinding (BVar var, _) :: env ->
         let locals = list_locals env in
         if var.index <> ret_vid then var.index :: locals else locals
-    | C.Frame :: _ -> []
+    | C.EFrame :: _ -> []
   in
   let locals : E.VarId.id list = list_locals ctx.env in
   (* Debug *)
@@ -392,11 +391,11 @@ let pop_frame (config : C.config) (pop_return_value : bool)
   let rec pop env =
     match env with
     | [] -> raise (Failure "Inconsistent environment")
-    | C.Abs abs :: env -> C.Abs abs :: pop env
-    | C.Var (_, v) :: env ->
+    | C.EAbs abs :: env -> C.EAbs abs :: pop env
+    | C.EBinding (_, v) :: env ->
         let vid = C.fresh_dummy_var_id () in
-        C.Var (C.DummyBinder vid, v) :: pop env
-    | C.Frame :: env -> (* Stop here *) env
+        C.EBinding (C.BDummy vid, v) :: pop env
+    | C.EFrame :: env -> (* Stop here *) env
   in
   let cf_pop cf (ret_value : V.typed_value option) : m_fun =
    fun ctx ->
@@ -416,7 +415,7 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
   comp cf_pop cf_assign
 
 (** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
+let eval_box_new_concrete (config : C.config) (generics : T.generic_args) :
     cm_fun =
  fun cf ctx ->
   (* Check and retrieve the arguments *)
@@ -426,9 +425,9 @@ let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
   | ( [],
       [ boxed_ty ],
       [],
-      Var (VarBinder input_var, input_value)
-      :: Var (_ret_var, _)
-      :: C.Frame :: _ ) ->
+      EBinding (BVar input_var, input_value)
+      :: EBinding (_ret_var, _)
+      :: C.EFrame :: _ ) ->
       (* Required type checking *)
       assert (input_value.V.ty = boxed_ty);
 
@@ -441,9 +440,9 @@ let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
       let cf_create cf (moved_input_value : V.typed_value) : m_fun =
         (* Create the box value *)
         let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in
-        let box_ty = T.Adt (T.Assumed T.Box, generics) in
+        let box_ty = T.TAdt (T.TAssumed T.TBox, generics) in
         let box_v =
-          V.Adt { variant_id = None; field_values = [ moved_input_value ] }
+          V.VAdt { variant_id = None; field_values = [ moved_input_value ] }
         in
         let box_v = mk_typed_value box_ty box_v in
 
@@ -478,7 +477,7 @@ let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
     It thus updates the box value (by calling {!drop_value}) and updates
     the destination (by setting it to [()]).
 *)
-let eval_box_free (config : C.config) (generics : T.egeneric_args)
+let eval_box_free (config : C.config) (generics : T.generic_args)
     (args : E.operand list) (dest : E.place) : cm_fun =
  fun cf ctx ->
   match (generics.regions, generics.types, generics.const_generics, args) with
@@ -657,7 +656,7 @@ let create_push_abstractions_from_abs_region_groups
     (* Add the avalues to the abstraction *)
     let abs = { abs with avalues } in
     (* Insert the abstraction in the context *)
-    let ctx = { ctx with env = Abs abs :: ctx.env } in
+    let ctx = { ctx with env = EAbs abs :: ctx.env } in
     (* Return *)
     ctx
   in
@@ -768,7 +767,7 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id)
       (* Treat the evaluation of the global as a call to the global body (without arguments) *)
       let func =
         {
-          E.func = FunId (Regular global.body_id);
+          E.func = FunId (FRegular global.body_id);
           generics = TypesUtils.mk_empty_generic_args;
           trait_and_method_generic_args = None;
         }
@@ -779,9 +778,8 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id)
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
        * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
-      let sval =
-        mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty)
-      in
+      assert (ty_no_regions global.ty);
+      let sval = mk_fresh_symbolic_value V.Global global.ty in
       let cc =
         assign_to_place config (mk_typed_value_from_symbolic_value sval) dest
       in
@@ -810,7 +808,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
         let cf_if (cf : st_m_fun) (op_v : V.typed_value) : m_fun =
          fun ctx ->
           match op_v.value with
-          | V.Literal (PV.Bool b) ->
+          | V.VLiteral (PV.VBool b) ->
               (* Evaluate the if and the branch body *)
               let cf_branch cf : m_fun =
                 (* Branch *)
@@ -838,7 +836,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
         let cf_switch (cf : st_m_fun) (op_v : V.typed_value) : m_fun =
          fun ctx ->
           match op_v.value with
-          | V.Literal (PV.Scalar sv) ->
+          | V.VLiteral (PV.VScalar sv) ->
               (* Evaluate the branch *)
               let cf_eval_branch cf =
                 (* Sanity check *)
@@ -893,7 +891,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
           let p_v = value_strip_shared_loans p_v in
           (* Match *)
           match p_v.value with
-          | V.Adt adt -> (
+          | V.VAdt adt -> (
               (* Evaluate the discriminant *)
               let dv = Option.get adt.variant_id in
               (* Find the branch, evaluate and continue *)
@@ -931,9 +929,9 @@ and eval_function_call_concrete (config : C.config) (call : A.call) : st_cm_fun
     =
  fun cf ctx ->
   match call.func.func with
-  | FunId (Regular fid) ->
+  | FunId (FRegular fid) ->
       eval_transparent_function_call_concrete config fid call cf ctx
-  | FunId (Assumed fid) ->
+  | FunId (FAssumed fid) ->
       (* Continue - note that we do as if the function call has been successful,
        * by giving {!Unit} to the continuation, because we place us in the case
        * where we haven't panicked. Of course, the translation needs to take the
@@ -944,9 +942,9 @@ and eval_function_call_concrete (config : C.config) (call : A.call) : st_cm_fun
 and eval_function_call_symbolic (config : C.config) (call : A.call) : st_cm_fun
     =
   match call.func.func with
-  | FunId (Regular _) | TraitMethod _ ->
+  | FunId (FRegular _) | TraitMethod _ ->
       eval_transparent_function_call_symbolic config call
-  | FunId (Assumed fid) -> eval_assumed_function_call_symbolic config fid call
+  | FunId (FAssumed fid) -> eval_assumed_function_call_symbolic config fid call
 
 (** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
 and eval_transparent_function_call_concrete (config : C.config)
@@ -975,7 +973,7 @@ and eval_transparent_function_call_concrete (config : C.config)
     (* There shouldn't be any reference to Self *)
     let tr_self = T.UnknownTrait __FUNCTION__ in
     let subst =
-      Subst.make_esubst_from_generics def.A.signature.generics generics tr_self
+      Subst.make_subst_from_generics def.A.signature.generics generics tr_self
     in
     let locals, body_st = Subst.fun_body_substitute_in_body subst body in
 
@@ -1106,13 +1104,13 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
   *)
   let func, generics, def, inst_sg =
     match call.func.func with
-    | FunId (Regular fid) ->
+    | FunId (FRegular fid) ->
         let def = C.ctx_lookup_fun_decl ctx fid in
         log#ldebug
           (lazy
             ("fun call:\n- call: " ^ call_to_string ctx call
            ^ "\n- call.generics:\n"
-            ^ egeneric_args_to_string ctx call.func.generics
+            ^ PA.generic_args_to_string ctx call.func.generics
             ^ "\n- def.signature:\n"
             ^ fun_sig_to_string ctx def.A.signature));
         let tr_self = T.UnknownTrait __FUNCTION__ in
@@ -1120,7 +1118,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
           instantiate_fun_sig ctx call.func.generics tr_self def.A.signature
         in
         (call.func.func, call.func.generics, def, inst_sg)
-    | FunId (Assumed _) ->
+    | FunId (FAssumed _) ->
         (* Unreachable: must be a transparent function *)
         raise (Failure "Unreachable")
     | TraitMethod (trait_ref, method_name, _) -> (
@@ -1128,9 +1126,9 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
           (lazy
             ("trait method call:\n- call: " ^ call_to_string ctx call
            ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n"
-            ^ egeneric_args_to_string ctx call.func.generics
+            ^ PA.generic_args_to_string ctx call.func.generics
             ^ "\n- trait and method generics:\n"
-            ^ egeneric_args_to_string ctx
+            ^ PA.generic_args_to_string ctx
                 (Option.get call.func.trait_and_method_generic_args)));
         (* When instantiating, we need to group the generics for the trait ref
            and the method *)
@@ -1155,9 +1153,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
                 (* This is a required method *)
                 let method_def = C.ctx_lookup_fun_decl ctx id in
                 (* Instantiate *)
-                let tr_self =
-                  T.TraitRef (etrait_ref_no_regions_to_gr_trait_ref trait_ref)
-                in
+                let tr_self = T.TraitRef trait_ref in
                 let inst_sg =
                   instantiate_fun_sig ctx generics tr_self
                     method_def.A.signature
@@ -1168,7 +1164,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
                    which implements the method. In order to do this properly,
                    we also need to update the generics.
                 *)
-                let func = E.FunId (Regular id) in
+                let func = E.FunId (FRegular id) in
                 (func, generics, method_def, inst_sg)
             | None ->
                 (* If not found, lookup the methods provided by the trait *declaration*
@@ -1210,13 +1206,11 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
                   (lazy
                     ("provided method call:" ^ "\n- method name: " ^ method_name
                    ^ "\n- all_generics:\n"
-                    ^ egeneric_args_to_string ctx all_generics
+                    ^ PA.generic_args_to_string ctx all_generics
                     ^ "\n- parent params info: "
                     ^ Print.option_to_string A.show_params_info
                         method_def.signature.parent_params_info));
-                let tr_self =
-                  T.TraitRef (etrait_ref_no_regions_to_gr_trait_ref trait_ref)
-                in
+                let tr_self = T.TraitRef trait_ref in
                 let inst_sg =
                   instantiate_fun_sig ctx all_generics tr_self
                     method_def.A.signature
@@ -1243,10 +1237,6 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
             log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def));
             (* Instantiate *)
             let tr_self = T.TraitRef trait_ref in
-            let tr_self =
-              TypesUtils.etrait_instance_id_no_regions_to_gr_trait_instance_id
-                tr_self
-            in
             let inst_sg =
               instantiate_fun_sig ctx generics tr_self method_def.A.signature
             in
@@ -1271,7 +1261,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call)
  *)
 and eval_function_call_symbolic_from_inst_sig (config : C.config)
     (fid : A.fun_id_or_trait_method_ref) (inst_sg : A.inst_fun_sig)
-    (generics : T.egeneric_args) (args : E.operand list) (dest : E.place) :
+    (generics : T.generic_args) (args : E.operand list) (dest : E.place) :
     st_cm_fun =
  fun cf ctx ->
   log#ldebug
@@ -1281,7 +1271,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
       ^ "\n- inst_sg:\n"
       ^ inst_fun_sig_to_string ctx inst_sg
       ^ "\n- call.generics:\n"
-      ^ egeneric_args_to_string ctx generics
+      ^ PA.generic_args_to_string ctx generics
       ^ "\n- args:\n"
       ^ String.concat ", " (List.map (operand_to_string ctx) args)
       ^ "\n- dest:\n" ^ place_to_string ctx dest));
@@ -1454,7 +1444,7 @@ and eval_assumed_function_call_symbolic (config : C.config)
       in
 
       (* Evaluate the function call *)
-      eval_function_call_symbolic_from_inst_sig config (FunId (Assumed fid))
+      eval_function_call_symbolic_from_inst_sig config (FunId (FAssumed fid))
         inst_sig generics args dest cf ctx
 
 (** Evaluate a statement seen as a function body *)