Merge branch 'main' into son_fixes2

2 files changed, 705 insertions, 604 deletions

diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 045c4484..437b358a 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1,28 +1,24 @@
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module A = LlbcAst
-module L = Logging
+open Types
 open TypesUtils
+open Values
 open ValuesUtils
-module Inv = Invariants
-module S = SynthesizeSymbolic
-open Utils
+open Expressions
+open Contexts
+open LlbcAst
 open Cps
 open InterpreterUtils
 open InterpreterProjectors
 open InterpreterExpansion
 open InterpreterPaths
 open InterpreterExpressions
+module Subst = Substitute
+module S = SynthesizeSymbolic
 
 (** The local logger *)
 let log = L.statements_log
 
 (** Drop a value at a given place - TODO: factorize this with [assign_to_place] *)
-let drop_value (config : C.config) (p : E.place) : cm_fun =
+let drop_value (config : config) (p : place) : cm_fun =
  fun cf ctx ->
   log#ldebug
     (lazy
@@ -36,14 +32,14 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
   (* Prepare the place (by ending the outer loans *at* the place). *)
   let cc = comp cc (prepare_lplace config p) in
   (* Replace the value with {!Bottom} *)
-  let replace cf (v : V.typed_value) ctx =
+  let replace cf (v : typed_value) ctx =
     (* Move the value at destination (that we will overwrite) to a dummy variable
      * to preserve the borrows it may contain *)
     let mv = InterpreterPaths.read_place access p ctx in
-    let dummy_id = C.fresh_dummy_var_id () in
-    let ctx = C.ctx_push_dummy_var ctx dummy_id mv in
+    let dummy_id = fresh_dummy_var_id () in
+    let ctx = ctx_push_dummy_var ctx dummy_id mv in
     (* Update the destination to ⊥ *)
-    let nv = { v with value = V.Bottom } in
+    let nv = { v with value = VBottom } in
     let ctx = write_place access p nv ctx in
     log#ldebug
       (lazy
@@ -55,40 +51,39 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
   comp cc replace cf ctx
 
 (** Push a dummy variable to the environment *)
-let push_dummy_var (vid : C.DummyVarId.id) (v : V.typed_value) : cm_fun =
+let push_dummy_var (vid : DummyVarId.id) (v : typed_value) : cm_fun =
  fun cf ctx ->
-  let ctx = C.ctx_push_dummy_var ctx vid v in
+  let ctx = ctx_push_dummy_var ctx vid v in
   cf ctx
 
 (** Remove a dummy variable from the environment *)
-let remove_dummy_var (vid : C.DummyVarId.id) (cf : V.typed_value -> m_fun) :
-    m_fun =
+let remove_dummy_var (vid : DummyVarId.id) (cf : typed_value -> m_fun) : m_fun =
  fun ctx ->
-  let ctx, v = C.ctx_remove_dummy_var ctx vid in
+  let ctx, v = ctx_remove_dummy_var ctx vid in
   cf v ctx
 
 (** Push an uninitialized variable to the environment *)
-let push_uninitialized_var (var : A.var) : cm_fun =
+let push_uninitialized_var (var : var) : cm_fun =
  fun cf ctx ->
-  let ctx = C.ctx_push_uninitialized_var ctx var in
+  let ctx = ctx_push_uninitialized_var ctx var in
   cf ctx
 
 (** Push a list of uninitialized variables to the environment *)
-let push_uninitialized_vars (vars : A.var list) : cm_fun =
+let push_uninitialized_vars (vars : var list) : cm_fun =
  fun cf ctx ->
-  let ctx = C.ctx_push_uninitialized_vars ctx vars in
+  let ctx = ctx_push_uninitialized_vars ctx vars in
   cf ctx
 
 (** Push a variable to the environment *)
-let push_var (var : A.var) (v : V.typed_value) : cm_fun =
+let push_var (var : var) (v : typed_value) : cm_fun =
  fun cf ctx ->
-  let ctx = C.ctx_push_var ctx var v in
+  let ctx = ctx_push_var ctx var v in
   cf ctx
 
 (** Push a list of variables to the environment *)
-let push_vars (vars : (A.var * V.typed_value) list) : cm_fun =
+let push_vars (vars : (var * typed_value) list) : cm_fun =
  fun cf ctx ->
-  let ctx = C.ctx_push_vars ctx vars in
+  let ctx = ctx_push_vars ctx vars in
   cf ctx
 
 (** Assign a value to a given place.
@@ -98,8 +93,7 @@ let push_vars (vars : (A.var * V.typed_value) list) : cm_fun =
     dummy variable and putting in its destination (after having checked that
     preparing the destination didn't introduce ⊥).
  *)
-let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) :
-    cm_fun =
+let assign_to_place (config : config) (rv : typed_value) (p : place) : cm_fun =
  fun cf ctx ->
   log#ldebug
     (lazy
@@ -108,20 +102,20 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) :
       ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n"
       ^ eval_ctx_to_string ctx));
   (* Push the rvalue to a dummy variable, for bookkeeping *)
-  let rvalue_vid = C.fresh_dummy_var_id () in
+  let rvalue_vid = fresh_dummy_var_id () in
   let cc = push_dummy_var rvalue_vid rv in
   (* Prepare the destination *)
   let cc = comp cc (prepare_lplace config p) in
   (* Retrieve the rvalue from the dummy variable *)
   let cc = comp cc (fun cf _lv -> remove_dummy_var rvalue_vid cf) in
   (* Update the destination *)
-  let move_dest cf (rv : V.typed_value) : m_fun =
+  let move_dest cf (rv : typed_value) : m_fun =
    fun ctx ->
     (* Move the value at destination (that we will overwrite) to a dummy variable
      * to preserve the borrows *)
     let mv = InterpreterPaths.read_place Write p ctx in
-    let dest_vid = C.fresh_dummy_var_id () in
-    let ctx = C.ctx_push_dummy_var ctx dest_vid mv in
+    let dest_vid = fresh_dummy_var_id () in
+    let ctx = ctx_push_dummy_var ctx dest_vid mv in
     (* Write to the destination *)
     (* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
     assert (not (bottom_in_value ctx.ended_regions rv));
@@ -141,15 +135,15 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) :
   comp cc move_dest cf ctx
 
 (** Evaluate an assertion, when the scrutinee is not symbolic *)
-let eval_assertion_concrete (config : C.config) (assertion : A.assertion) :
+let eval_assertion_concrete (config : config) (assertion : assertion) :
     st_cm_fun =
  fun cf ctx ->
   (* There won't be any symbolic expansions: fully evaluate the operand *)
   let eval_op = eval_operand config assertion.cond in
-  let eval_assert cf (v : V.typed_value) : m_fun =
+  let eval_assert cf (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
     | _ ->
@@ -165,33 +159,33 @@ let eval_assertion_concrete (config : C.config) (assertion : A.assertion) :
     a call to [assert ...] then continue in the success branch (and thus
     expand the boolean to [true]).
  *)
-let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
+let eval_assertion (config : config) (assertion : assertion) : st_cm_fun =
  fun cf ctx ->
   (* Evaluate the operand *)
   let eval_op = eval_operand config assertion.cond in
   (* Evaluate the assertion *)
-  let eval_assert cf (v : V.typed_value) : m_fun =
+  let eval_assert cf (v : typed_value) : m_fun =
    fun ctx ->
-    assert (v.ty = T.Literal PV.Bool);
+    assert (v.ty = TLiteral 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);
+    | VSymbolic sv ->
+        assert (config.mode = SymbolicMode);
+        assert (sv.sv_ty = TLiteral 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
+          apply_symbolic_expansion_non_borrow config sv (SeLiteral (VBool true))
+            ctx
         in
         (* Continue *)
         let expr = cf Unit ctx in
@@ -210,31 +204,29 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
     - either the discriminant is already the proper one (in which case we
       don't do anything)
     - or it is not the proper one (because the variant is not the proper
-      one, or the value is actually {!V.Bottom} - this happens when
+      one, or the value is actually {!Bottom} - this happens when
       initializing ADT values), in which case we replace the value with
-      a variant with all its fields set to {!V.Bottom}.
+      a variant with all its fields set to {!Bottom}.
       For instance, something like: [Cons Bottom Bottom].
  *)
-let set_discriminant (config : C.config) (p : E.place)
-    (variant_id : T.VariantId.id) : st_cm_fun =
+let set_discriminant (config : config) (p : place) (variant_id : VariantId.id) :
+    st_cm_fun =
  fun cf ctx ->
   log#ldebug
     (lazy
       ("set_discriminant:" ^ "\n- p: " ^ place_to_string ctx p
      ^ "\n- variant id: "
-      ^ T.VariantId.to_string variant_id
+      ^ VariantId.to_string variant_id
       ^ "\n- initial context:\n" ^ eval_ctx_to_string ctx));
   (* Access the value *)
   let access = Write in
   let cc = update_ctx_along_read_place config access p in
   let cc = comp cc (prepare_lplace config p) in
   (* Update the value *)
-  let update_value cf (v : V.typed_value) : m_fun =
+  let update_value cf (v : typed_value) : m_fun =
    fun ctx ->
-    match (v.V.ty, v.V.value) with
-    | ( T.Adt
-          (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types, cgs),
-        V.Adt av ) -> (
+    match (v.ty, v.value) with
+    | TAdt ((TAdtId _ as type_id), generics), VAdt av -> (
         (* There are two situations:
            - either the discriminant is already the proper one (in which case we
              don't do anything)
@@ -250,33 +242,22 @@ let set_discriminant (config : C.config) (p : E.place)
               (* Replace the value *)
               let bottom_v =
                 match type_id with
-                | T.AdtId def_id ->
-                    compute_expanded_bottom_adt_value
-                      ctx.type_context.type_decls def_id (Some variant_id)
-                      regions types cgs
-                | T.Assumed T.Option ->
-                    assert (regions = []);
-                    compute_expanded_bottom_option_value variant_id
-                      (Collections.List.to_cons_nil types)
+                | TAdtId def_id ->
+                    compute_expanded_bottom_adt_value ctx def_id
+                      (Some variant_id) generics
                 | _ -> raise (Failure "Unreachable")
               in
               assign_to_place config bottom_v p (cf Unit) ctx)
-    | ( T.Adt
-          (((T.AdtId _ | T.Assumed T.Option) as type_id), regions, types, cgs),
-        V.Bottom ) ->
+    | TAdt ((TAdtId _ as type_id), generics), VBottom ->
         let bottom_v =
           match type_id with
-          | T.AdtId def_id ->
-              compute_expanded_bottom_adt_value ctx.type_context.type_decls
-                def_id (Some variant_id) regions types cgs
-          | T.Assumed T.Option ->
-              assert (regions = []);
-              compute_expanded_bottom_option_value variant_id
-                (Collections.List.to_cons_nil types)
+          | TAdtId def_id ->
+              compute_expanded_bottom_adt_value ctx def_id (Some variant_id)
+                generics
           | _ -> raise (Failure "Unreachable")
         in
         assign_to_place config bottom_v p (cf Unit) ctx
-    | _, V.Symbolic _ ->
+    | _, VSymbolic _ ->
         assert (config.mode = SymbolicMode);
         (* This is a bit annoying: in theory we should expand the symbolic value
          * then set the discriminant, because in the case the discriminant is
@@ -286,73 +267,82 @@ 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 _) ->
+    | _, (VAdt _ | VBottom) -> raise (Failure "Inconsistent state")
+    | _, (VLiteral _ | VBorrow _ | VLoan _) ->
         raise (Failure "Unexpected value")
   in
   (* Compose and apply *)
   comp cc update_value cf ctx
 
 (** 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 }
+let ctx_push_frame (ctx : eval_ctx) : eval_ctx =
+  { 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)
 
 (** Small helper: compute the type of the return value for a specific
-    instantiation of a non-local function.
+    instantiation of an assumed function.
  *)
-let get_non_local_function_return_type (fid : A.assumed_fun_id)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (const_generic_params : T.const_generic list) : T.ety =
+let get_assumed_function_return_type (ctx : eval_ctx) (fid : assumed_fun_id)
+    (generics : generic_args) : ety =
+  assert (generics.trait_refs = []);
   (* [Box::free] has a special treatment *)
-  match (fid, region_params, type_params, const_generic_params) with
-  | A.BoxFree, [], [ _ ], [] -> mk_unit_ty
+  match fid with
+  | BoxFree ->
+      assert (generics.regions = []);
+      assert (List.length generics.types = 1);
+      assert (generics.const_generics = []);
+      mk_unit_ty
   | _ ->
       (* Retrieve the function's signature *)
-      let sg = Assumed.get_assumed_sig fid in
+      let sg = Assumed.get_assumed_fun_sig fid in
       (* Instantiate the return type  *)
-      let tsubst = Subst.make_type_subst_from_vars sg.type_params type_params in
-      let cgsubst =
-        Subst.make_const_generic_subst_from_vars sg.const_generic_params
-          const_generic_params
+      (* There shouldn't be any reference to Self *)
+      let tr_self : trait_instance_id = 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_subst_from_generics sg.generics generics tr_self
       in
-      Subst.erase_regions_substitute_types tsubst cgsubst sg.output
+      let ty =
+        Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
+          sg.output
+      in
+      AssociatedTypes.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 =
+let move_return_value (config : config) (pop_return_value : bool)
+    (cf : typed_value option -> m_fun) : m_fun =
  fun ctx ->
   if pop_return_value then
-    let ret_vid = E.VarId.zero in
-    let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in
+    let ret_vid = VarId.zero in
+    let cc = eval_operand config (Move (mk_place_from_var_id ret_vid)) in
     cc (fun v ctx -> cf (Some v) ctx) ctx
   else cf None ctx
 
-let pop_frame (config : C.config) (pop_return_value : bool)
-    (cf : V.typed_value option -> m_fun) : m_fun =
+let pop_frame (config : config) (pop_return_value : bool)
+    (cf : typed_value option -> m_fun) : m_fun =
  fun ctx ->
   (* Debug *)
   log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ctx));
 
   (* List the local variables, but the return variable *)
-  let ret_vid = E.VarId.zero in
+  let ret_vid = VarId.zero in
   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 ->
+    | EAbs _ :: env -> list_locals env
+    | EBinding (BDummy _, _) :: env -> list_locals env
+    | EBinding (BVar var, _) :: env ->
         let locals = list_locals env in
         if var.index <> ret_vid then var.index :: locals else locals
-    | C.Frame :: _ -> []
+    | EFrame :: _ -> []
   in
-  let locals : E.VarId.id list = list_locals ctx.env in
+  let locals : VarId.id list = list_locals ctx.env in
   (* Debug *)
   log#ldebug
     (lazy
       ("pop_frame: locals in which to drop the outer loans: ["
-      ^ String.concat "," (List.map E.VarId.to_string locals)
+      ^ String.concat "," (List.map VarId.to_string locals)
       ^ "]"));
 
   (* Move the return value out of the return variable *)
@@ -367,7 +357,7 @@ let pop_frame (config : C.config) (pop_return_value : bool)
   in
 
   (* Drop the outer *loans* we find in the local variables *)
-  let cf_drop_loans_in_locals cf (ret_value : V.typed_value option) : m_fun =
+  let cf_drop_loans_in_locals cf (ret_value : typed_value option) : m_fun =
     (* Drop the loans *)
     let locals = List.rev locals in
     let cf_drop =
@@ -395,13 +385,13 @@ 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 ->
-        let vid = C.fresh_dummy_var_id () in
-        C.Var (C.DummyBinder vid, v) :: pop env
-    | C.Frame :: env -> (* Stop here *) env
+    | EAbs abs :: env -> EAbs abs :: pop env
+    | EBinding (_, v) :: env ->
+        let vid = fresh_dummy_var_id () in
+        EBinding (BDummy vid, v) :: pop env
+    | EFrame :: env -> (* Stop here *) env
   in
-  let cf_pop cf (ret_value : V.typed_value option) : m_fun =
+  let cf_pop cf (ret_value : typed_value option) : m_fun =
    fun ctx ->
     let env = pop ctx.env in
     let ctx = { ctx with env } in
@@ -411,51 +401,46 @@ let pop_frame (config : C.config) (pop_return_value : bool)
   comp cc cf_pop cf ctx
 
 (** Pop the current frame and assign the returned value to its destination. *)
-let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
+let pop_frame_assign (config : config) (dest : place) : cm_fun =
   let cf_pop = pop_frame config true in
   let cf_assign cf ret_value : m_fun =
     assign_to_place config (Option.get ret_value) dest cf
   in
   comp cf_pop cf_assign
 
-(** Auxiliary function - see {!eval_non_local_function_call} *)
-let eval_replace_concrete (_config : C.config)
-    (_region_params : T.erased_region list) (_type_params : T.ety list)
-    (_cg_params : T.const_generic list) : cm_fun =
- fun _cf _ctx -> raise Unimplemented
-
-(** Auxiliary function - see {!eval_non_local_function_call} *)
-let eval_box_new_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_params : T.const_generic list) : cm_fun =
+(** Auxiliary function - see {!eval_assumed_function_call} *)
+let eval_box_new_concrete (config : config) (generics : generic_args) : cm_fun =
  fun cf ctx ->
   (* Check and retrieve the arguments *)
-  match (region_params, type_params, cg_params, ctx.env) with
+  match
+    (generics.regions, generics.types, generics.const_generics, ctx.env)
+  with
   | ( [],
       [ boxed_ty ],
       [],
-      Var (VarBinder input_var, input_value)
-      :: Var (_ret_var, _)
-      :: C.Frame :: _ ) ->
+      EBinding (BVar input_var, input_value)
+      :: EBinding (_ret_var, _)
+      :: EFrame :: _ ) ->
       (* Required type checking *)
-      assert (input_value.V.ty = boxed_ty);
+      assert (input_value.ty = boxed_ty);
 
       (* Move the input value *)
       let cf_move =
-        eval_operand config (E.Move (mk_place_from_var_id input_var.C.index))
+        eval_operand config (Move (mk_place_from_var_id input_var.index))
       in
 
       (* Create the new box *)
-      let cf_create cf (moved_input_value : V.typed_value) : m_fun =
+      let cf_create cf (moved_input_value : typed_value) : m_fun =
         (* Create the box value *)
-        let box_ty = T.Adt (T.Assumed T.Box, [], [ boxed_ty ], []) in
+        let generics = TypesUtils.mk_generic_args_from_types [ boxed_ty ] in
+        let box_ty = TAdt (TAssumed TBox, generics) in
         let box_v =
-          V.Adt { variant_id = None; field_values = [ moved_input_value ] }
+          VAdt { variant_id = None; field_values = [ moved_input_value ] }
         in
         let box_v = mk_typed_value box_ty box_v in
 
         (* Move this value to the return variable *)
-        let dest = mk_place_from_var_id E.VarId.zero in
+        let dest = mk_place_from_var_id VarId.zero in
         let cf_assign = assign_to_place config box_v dest in
 
         (* Continue *)
@@ -466,71 +451,7 @@ let eval_box_new_concrete (config : C.config)
       comp cf_move cf_create cf ctx
   | _ -> raise (Failure "Inconsistent state")
 
-(** Auxiliary function which factorizes code to evaluate [std::Deref::deref]
-    and [std::DerefMut::deref_mut] - see {!eval_non_local_function_call} *)
-let eval_box_deref_mut_or_shared_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_params : T.const_generic list) (is_mut : bool) : cm_fun =
- fun cf ctx ->
-  (* Check the arguments *)
-  match (region_params, type_params, cg_params, ctx.env) with
-  | ( [],
-      [ boxed_ty ],
-      [],
-      Var (VarBinder input_var, input_value)
-      :: Var (_ret_var, _)
-      :: C.Frame :: _ ) ->
-      (* Required type checking. We must have:
-         - input_value.ty = & (mut) Box<ty>
-         - boxed_ty = ty
-         for some ty
-      *)
-      (let _, input_ty, ref_kind = ty_get_ref input_value.V.ty in
-       assert (match ref_kind with T.Shared -> not is_mut | T.Mut -> is_mut);
-       let input_ty = ty_get_box input_ty in
-       assert (input_ty = boxed_ty));
-
-      (* Borrow the boxed value *)
-      let p =
-        { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] }
-      in
-      let borrow_kind = if is_mut then E.Mut else E.Shared in
-      let rv = E.Ref (p, borrow_kind) in
-      let cf_borrow = eval_rvalue_not_global config rv in
-
-      (* Move the borrow to its destination *)
-      let cf_move cf res : m_fun =
-        match res with
-        | Error EPanic ->
-            (* We can't get there by borrowing a value *)
-            raise (Failure "Unreachable")
-        | Ok borrowed_value ->
-            (* Move and continue *)
-            let destp = mk_place_from_var_id E.VarId.zero in
-            assign_to_place config borrowed_value destp cf
-      in
-
-      (* Compose and apply *)
-      comp cf_borrow cf_move cf ctx
-  | _ -> raise (Failure "Inconsistent state")
-
-(** Auxiliary function - see {!eval_non_local_function_call} *)
-let eval_box_deref_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_params : T.const_generic list) : cm_fun =
-  let is_mut = false in
-  eval_box_deref_mut_or_shared_concrete config region_params type_params
-    cg_params is_mut
-
-(** Auxiliary function - see {!eval_non_local_function_call} *)
-let eval_box_deref_mut_concrete (config : C.config)
-    (region_params : T.erased_region list) (type_params : T.ety list)
-    (cg_params : T.const_generic list) : cm_fun =
-  let is_mut = true in
-  eval_box_deref_mut_or_shared_concrete config region_params type_params
-    cg_params is_mut
-
-(** Auxiliary function - see {!eval_non_local_function_call}.
+(** Auxiliary function - see {!eval_assumed_function_call}.
 
     [Box::free] is not handled the same way as the other assumed functions:
     - in the regular case, whenever we need to evaluate an assumed function,
@@ -549,15 +470,14 @@ let eval_box_deref_mut_concrete (config : C.config)
     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) (region_params : T.erased_region list)
-    (type_params : T.ety list) (cg_params : T.const_generic list)
-    (args : E.operand list) (dest : E.place) : cm_fun =
+let eval_box_free (config : config) (generics : generic_args)
+    (args : operand list) (dest : place) : cm_fun =
  fun cf ctx ->
-  match (region_params, type_params, cg_params, args) with
-  | [], [ boxed_ty ], [], [ E.Move input_box_place ] ->
+  match (generics.regions, generics.types, generics.const_generics, args) with
+  | [], [ boxed_ty ], [], [ Move input_box_place ] ->
       (* Required type checking *)
       let input_box = InterpreterPaths.read_place Write input_box_place ctx in
-      (let input_ty = ty_get_box input_box.V.ty in
+      (let input_ty = ty_get_box input_box.ty in
        assert (input_ty = boxed_ty));
 
       (* Drop the value *)
@@ -570,136 +490,87 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
       cc cf ctx
   | _ -> raise (Failure "Inconsistent state")
 
-(** Auxiliary function - see {!eval_non_local_function_call} *)
-let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
-    (_region_params : T.erased_region list) (_type_params : T.ety list)
-    (_cg_params : T.const_generic list) : cm_fun =
- fun _cf _ctx -> raise Unimplemented
-
 (** Evaluate a non-local function call in concrete mode *)
-let eval_non_local_function_call_concrete (config : C.config)
-    (fid : A.assumed_fun_id) (region_params : T.erased_region list)
-    (type_params : T.ety list) (cg_params : T.const_generic list)
-    (args : E.operand list) (dest : E.place) : cm_fun =
-  (* There are two cases (and this is extremely annoying):
-     - the function is not box_free
-     - the function is box_free
-     See {!eval_box_free}
-  *)
-  match fid with
-  | A.BoxFree ->
-      (* Degenerate case: box_free *)
-      eval_box_free config region_params type_params cg_params args dest
-  | _ ->
-      (* "Normal" case: not box_free *)
-      (* Evaluate the operands *)
-      (*      let ctx, args_vl = eval_operands config ctx args in *)
-      let cf_eval_ops = eval_operands config args in
-
-      (* Evaluate the call
-       *
-       * Style note: at some point we used {!comp_transmit} to
-       * transmit the result of {!eval_operands} above down to {!push_vars}
-       * below, without having to introduce an intermediary function call,
-       * but it made it less clear where the computed values came from,
-       * so we reversed the modifications. *)
-      let cf_eval_call cf (args_vl : V.typed_value list) : m_fun =
-        (* Push the stack frame: we initialize the frame with the return variable,
-           and one variable per input argument *)
-        let cc = push_frame in
-
-        (* Create and push the return variable *)
-        let ret_vid = E.VarId.zero in
-        let ret_ty =
-          get_non_local_function_return_type fid region_params type_params
-            cg_params
-        in
-        let ret_var = mk_var ret_vid (Some "@return") ret_ty in
-        let cc = comp cc (push_uninitialized_var ret_var) in
-
-        (* Create and push the input variables *)
-        let input_vars =
-          E.VarId.mapi_from1
-            (fun id (v : V.typed_value) -> (mk_var id None v.V.ty, v))
-            args_vl
-        in
-        let cc = comp cc (push_vars input_vars) in
-
-        (* "Execute" the function body. As the functions are assumed, here we call
-         * custom functions to perform the proper manipulations: we don't have
-         * access to a body. *)
-        let cf_eval_body : cm_fun =
-          match fid with
-          | A.Replace ->
-              eval_replace_concrete config region_params type_params cg_params
-          | BoxNew ->
-              eval_box_new_concrete config region_params type_params cg_params
-          | BoxDeref ->
-              eval_box_deref_concrete config region_params type_params cg_params
-          | BoxDerefMut ->
-              eval_box_deref_mut_concrete config region_params type_params
-                cg_params
-          | BoxFree ->
-              (* Should have been treated above *) raise (Failure "Unreachable")
-          | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
-              eval_vec_function_concrete config fid region_params type_params
-                cg_params
-          | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
-          | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut
-          | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
-          | SliceSubsliceMut | SliceLen ->
-              raise (Failure "Unimplemented")
-        in
+let eval_assumed_function_call_concrete (config : config) (fid : assumed_fun_id)
+    (call : call) : cm_fun =
+  let args = call.args in
+  let dest = call.dest in
+  match call.func with
+  | FnOpMove _ ->
+      (* Closure case: TODO *)
+      raise (Failure "Closures are not supported yet")
+  | FnOpRegular func -> (
+      let generics = func.generics in
+      (* Sanity check: we don't fully handle the const generic vars environment
+         in concrete mode yet *)
+      assert (generics.const_generics = []);
+      (* There are two cases (and this is extremely annoying):
+         - the function is not box_free
+         - the function is box_free
+         See {!eval_box_free}
+      *)
+      match fid with
+      | BoxFree ->
+          (* Degenerate case: box_free *)
+          eval_box_free config generics args dest
+      | _ ->
+          (* "Normal" case: not box_free *)
+          (* Evaluate the operands *)
+          (*      let ctx, args_vl = eval_operands config ctx args in *)
+          let cf_eval_ops = eval_operands config args in
+
+          (* Evaluate the call
+           *
+           * Style note: at some point we used {!comp_transmit} to
+           * transmit the result of {!eval_operands} above down to {!push_vars}
+           * below, without having to introduce an intermediary function call,
+           * but it made it less clear where the computed values came from,
+           * so we reversed the modifications. *)
+          let cf_eval_call cf (args_vl : typed_value list) : m_fun =
+           fun ctx ->
+            (* Push the stack frame: we initialize the frame with the return variable,
+               and one variable per input argument *)
+            let cc = push_frame in
+
+            (* Create and push the return variable *)
+            let ret_vid = VarId.zero in
+            let ret_ty = get_assumed_function_return_type ctx fid generics in
+            let ret_var = mk_var ret_vid (Some "@return") ret_ty in
+            let cc = comp cc (push_uninitialized_var ret_var) in
+
+            (* Create and push the input variables *)
+            let input_vars =
+              VarId.mapi_from1
+                (fun id (v : typed_value) -> (mk_var id None v.ty, v))
+                args_vl
+            in
+            let cc = comp cc (push_vars input_vars) in
+
+            (* "Execute" the function body. As the functions are assumed, here we call
+             * custom functions to perform the proper manipulations: we don't have
+             * access to a body. *)
+            let cf_eval_body : cm_fun =
+              match fid with
+              | BoxNew -> eval_box_new_concrete config generics
+              | BoxFree ->
+                  (* Should have been treated above *)
+                  raise (Failure "Unreachable")
+              | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
+              | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut
+                ->
+                  raise (Failure "Unimplemented")
+            in
 
-        let cc = comp cc cf_eval_body in
+            let cc = comp cc cf_eval_body in
 
-        (* Pop the frame *)
-        let cc = comp cc (pop_frame_assign config dest) in
+            (* Pop the frame *)
+            let cc = comp cc (pop_frame_assign config dest) in
 
-        (* Continue *)
-        cc cf
-      in
-      (* Compose and apply *)
-      comp cf_eval_ops cf_eval_call
-
-let instantiate_fun_sig (type_params : T.ety list)
-    (cg_params : T.const_generic list) (sg : A.fun_sig) : A.inst_fun_sig =
-  (* Generate fresh abstraction ids and create a substitution from region
-   * group ids to abstraction ids *)
-  let rg_abs_ids_bindings =
-    List.map
-      (fun rg ->
-        let abs_id = C.fresh_abstraction_id () in
-        (rg.T.id, abs_id))
-      sg.regions_hierarchy
-  in
-  let asubst_map : V.AbstractionId.id T.RegionGroupId.Map.t =
-    List.fold_left
-      (fun mp (rg_id, abs_id) -> T.RegionGroupId.Map.add rg_id abs_id mp)
-      T.RegionGroupId.Map.empty rg_abs_ids_bindings
-  in
-  let asubst (rg_id : T.RegionGroupId.id) : V.AbstractionId.id =
-    T.RegionGroupId.Map.find rg_id asubst_map
-  in
-  (* Generate fresh regions and their substitutions *)
-  let _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params in
-  (* Generate the type substitution
-   * Note that we need the substitution to map the type variables to
-   * {!rty} types (not {!ety}). In order to do that, we convert the
-   * type parameters to types with regions. This is possible only
-   * if those types don't contain any regions.
-   * This is a current limitation of the analysis: there is still some
-   * work to do to properly handle full type parametrization.
-   * *)
-  let rtype_params = List.map ety_no_regions_to_rty type_params in
-  let tsubst = Subst.make_type_subst_from_vars sg.type_params rtype_params in
-  let cgsubst =
-    Subst.make_const_generic_subst_from_vars sg.const_generic_params cg_params
-  in
-  (* Substitute the signature *)
-  let inst_sig = Subst.substitute_signature asubst rsubst tsubst cgsubst sg in
-  (* Return *)
-  inst_sig
+            (* Continue *)
+            cc cf ctx
+          in
+          (* Compose and apply *)
+          comp cf_eval_ops cf_eval_call)
 
 (** Helper
  
@@ -710,49 +581,48 @@ let instantiate_fun_sig (type_params : T.ety list)
     which can end or not.
  *)
 let create_empty_abstractions_from_abs_region_groups
-    (kind : T.RegionGroupId.id -> V.abs_kind) (rgl : A.abs_region_group list)
-    (region_can_end : T.RegionGroupId.id -> bool) : V.abs list =
+    (kind : RegionGroupId.id -> abs_kind) (rgl : abs_region_group list)
+    (region_can_end : RegionGroupId.id -> bool) : abs list =
   (* We use a reference to progressively create a map from abstraction ids
    * to set of ancestor regions. Note that {!abs_to_ancestors_regions} [abs_id]
    * returns the union of:
    * - the regions of the ancestors of abs_id
    * - the regions of abs_id
    *)
-  let abs_to_ancestors_regions : T.RegionId.Set.t V.AbstractionId.Map.t ref =
-    ref V.AbstractionId.Map.empty
+  let abs_to_ancestors_regions : RegionId.Set.t AbstractionId.Map.t ref =
+    ref AbstractionId.Map.empty
   in
   (* Auxiliary function to create one abstraction *)
-  let create_abs (rg_id : T.RegionGroupId.id) (rg : A.abs_region_group) : V.abs
-      =
-    let abs_id = rg.T.id in
+  let create_abs (rg_id : RegionGroupId.id) (rg : abs_region_group) : abs =
+    let abs_id = rg.id in
     let original_parents = rg.parents in
     let parents =
       List.fold_left
-        (fun s pid -> V.AbstractionId.Set.add pid s)
-        V.AbstractionId.Set.empty rg.parents
+        (fun s pid -> AbstractionId.Set.add pid s)
+        AbstractionId.Set.empty rg.parents
     in
     let regions =
       List.fold_left
-        (fun s rid -> T.RegionId.Set.add rid s)
-        T.RegionId.Set.empty rg.regions
+        (fun s rid -> RegionId.Set.add rid s)
+        RegionId.Set.empty rg.regions
     in
     let ancestors_regions =
       List.fold_left
         (fun acc parent_id ->
-          T.RegionId.Set.union acc
-            (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
-        T.RegionId.Set.empty rg.parents
+          RegionId.Set.union acc
+            (AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
+        RegionId.Set.empty rg.parents
     in
     let ancestors_regions_union_current_regions =
-      T.RegionId.Set.union ancestors_regions regions
+      RegionId.Set.union ancestors_regions regions
     in
     let can_end = region_can_end rg_id in
     abs_to_ancestors_regions :=
-      V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions
+      AbstractionId.Map.add abs_id ancestors_regions_union_current_regions
         !abs_to_ancestors_regions;
     (* Create the abstraction *)
     {
-      V.abs_id;
+      abs_id;
       kind = kind rg_id;
       can_end;
       parents;
@@ -763,14 +633,13 @@ let create_empty_abstractions_from_abs_region_groups
     }
   in
   (* Apply *)
-  T.RegionGroupId.mapi create_abs rgl
+  RegionGroupId.mapi create_abs rgl
 
 let create_push_abstractions_from_abs_region_groups
-    (kind : T.RegionGroupId.id -> V.abs_kind) (rgl : A.abs_region_group list)
-    (region_can_end : T.RegionGroupId.id -> bool)
-    (compute_abs_avalues :
-      V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list)
-    (ctx : C.eval_ctx) : C.eval_ctx =
+    (kind : RegionGroupId.id -> abs_kind) (rgl : abs_region_group list)
+    (region_can_end : RegionGroupId.id -> bool)
+    (compute_abs_avalues : abs -> eval_ctx -> eval_ctx * typed_avalue list)
+    (ctx : eval_ctx) : eval_ctx =
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let empty_absl =
     create_empty_abstractions_from_abs_region_groups kind rgl region_can_end
@@ -778,20 +647,254 @@ let create_push_abstractions_from_abs_region_groups
 
   (* Compute and add the avalues to the abstractions, the insert the abstractions
    * in the context. *)
-  let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx =
+  let insert_abs (ctx : eval_ctx) (abs : abs) : eval_ctx =
     (* Compute the values to insert in the abstraction *)
     let ctx, avalues = compute_abs_avalues abs ctx in
     (* 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
   List.fold_left insert_abs ctx empty_absl
 
+(** Auxiliary helper for [eval_transparent_function_call_symbolic]
+    Instantiate the signature and introduce fresh abstractions and region ids while doing so.
+
+    We perform some manipulations when instantiating the signature.
+
+    # Trait impl calls
+    ==================
+    In particular, we have a special treatment of trait method calls when
+    the trait ref is a known impl.
+
+    For instance:
+    {[
+      trait HasValue {
+        fn has_value(&self) -> bool;
+      }
+
+      impl<T> HasValue for Option<T> {
+        fn has_value(&self) {
+          match self {
+            None => false,
+            Some(_) => true,
+          }
+        }
+      }
+
+      fn option_has_value<T>(x: &Option<T>) -> bool {
+        x.has_value()
+      }
+    ]}
+
+    The generated code looks like this:
+    {[
+      structure HasValue (Self : Type) = {
+        has_value : Self -> result bool
+      }
+
+      let OptionHasValueImpl.has_value (Self : Type) (self : Self) : result bool =
+        match self with
+        | None => false
+        | Some _ => true
+
+      let OptionHasValueInstance (T : Type) : HasValue (Option T) = {
+        has_value = OptionHasValueInstance.has_value
+      }
+    ]}
+
+    In [option_has_value], we don't want to refer to the [has_value] method
+    of the instance of [HasValue] for [Option<T>]. We want to refer directly
+    to the function which implements [has_value] for [Option<T>].
+    That is, instead of generating this:
+    {[
+      let option_has_value (T : Type) (x : Option T) : result bool =
+        (OptionHasValueInstance T).has_value x
+    ]}
+
+    We want to generate this:
+    {[
+      let option_has_value (T : Type) (x : Option T) : result bool =
+        OptionHasValueImpl.has_value T x
+    ]}
+
+    # Provided trait methods
+    ========================
+    Calls to provided trait methods also have a special treatment because
+    for now we forbid overriding provided trait methods in the trait implementations,
+    which means that whenever we call a provided trait method, we do not refer
+    to a trait clause but directly to the method provided in the trait declaration.
+ *)
+let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
+    : fun_id_or_trait_method_ref * generic_args * fun_decl * inst_fun_sig =
+  match call.func with
+  | FnOpMove _ ->
+      (* Closure case: TODO *)
+      raise (Failure "Closures are not supported yet")
+  | FnOpRegular func -> (
+      match func.func with
+      | FunId (FRegular fid) ->
+          let def = ctx_lookup_fun_decl ctx fid in
+          log#ldebug
+            (lazy
+              ("fun call:\n- call: " ^ call_to_string ctx call
+             ^ "\n- call.generics:\n"
+              ^ generic_args_to_string ctx func.generics
+              ^ "\n- def.signature:\n"
+              ^ fun_sig_to_string ctx def.signature));
+          let tr_self = UnknownTrait __FUNCTION__ in
+          let regions_hierarchy =
+            LlbcAstUtils.FunIdMap.find (FRegular fid)
+              ctx.fun_context.regions_hierarchies
+          in
+          let inst_sg =
+            instantiate_fun_sig ctx func.generics tr_self def.signature
+              regions_hierarchy
+          in
+          (func.func, func.generics, def, inst_sg)
+      | FunId (FAssumed _) ->
+          (* Unreachable: must be a transparent function *)
+          raise (Failure "Unreachable")
+      | TraitMethod (trait_ref, method_name, _) -> (
+          log#ldebug
+            (lazy
+              ("trait method call:\n- call: " ^ call_to_string ctx call
+             ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n"
+              ^ generic_args_to_string ctx func.generics
+              ^ "\n- trait and method generics:\n"
+              ^ generic_args_to_string ctx
+                  (Option.get func.trait_and_method_generic_args)));
+          (* When instantiating, we need to group the generics for the trait ref
+             and the method *)
+          let generics = Option.get func.trait_and_method_generic_args in
+          (* Lookup the trait method signature - there are several possibilities
+             depending on whethere we call a top-level trait method impl or the
+             method from a local clause *)
+          match trait_ref.trait_id with
+          | TraitImpl impl_id -> (
+              (* Lookup the trait impl *)
+              let trait_impl = ctx_lookup_trait_impl ctx impl_id in
+              log#ldebug
+                (lazy ("trait impl: " ^ trait_impl_to_string ctx trait_impl));
+              (* First look in the required methods *)
+              let method_id =
+                List.find_opt
+                  (fun (s, _) -> s = method_name)
+                  trait_impl.required_methods
+              in
+              match method_id with
+              | Some (_, id) ->
+                  (* This is a required method *)
+                  let method_def = ctx_lookup_fun_decl ctx id in
+                  (* Instantiate *)
+                  let tr_self = TraitRef trait_ref in
+                  let fid : fun_id = FRegular id in
+                  let regions_hierarchy =
+                    LlbcAstUtils.FunIdMap.find fid
+                      ctx.fun_context.regions_hierarchies
+                  in
+                  let inst_sg =
+                    instantiate_fun_sig ctx generics tr_self
+                      method_def.signature regions_hierarchy
+                  in
+                  (* Also update the function identifier: we want to forget
+                     the fact that we called a trait method, and treat it as
+                     a regular function call to the top-level function
+                     which implements the method. In order to do this properly,
+                     we also need to update the generics.
+                  *)
+                  let func = FunId fid in
+                  (func, generics, method_def, inst_sg)
+              | None ->
+                  (* If not found, lookup the methods provided by the trait *declaration*
+                     (remember: for now, we forbid overriding provided methods) *)
+                  assert (trait_impl.provided_methods = []);
+                  let trait_decl =
+                    ctx_lookup_trait_decl ctx
+                      trait_ref.trait_decl_ref.trait_decl_id
+                  in
+                  let _, method_id =
+                    List.find
+                      (fun (s, _) -> s = method_name)
+                      trait_decl.provided_methods
+                  in
+                  let method_id = Option.get method_id in
+                  let method_def = ctx_lookup_fun_decl ctx method_id in
+                  (* For the instantiation we have to do something peculiar
+                     because the method was defined for the trait declaration.
+                     We have to group:
+                     - the parameters given to the trait decl reference
+                     - the parameters given to the method itself
+                     For instance:
+                     {[
+                       trait Foo<T> {
+                         fn f<U>(...) { ... }
+                       }
+
+                       fn g<G>(x : G) where Clause0: Foo<G, bool>
+                       {
+                         x.f::<u32>(...) // The arguments to f are: <G, bool, u32>
+                       }
+                     ]}
+                  *)
+                  let all_generics =
+                    TypesUtils.merge_generic_args
+                      trait_ref.trait_decl_ref.decl_generics func.generics
+                  in
+                  log#ldebug
+                    (lazy
+                      ("provided method call:" ^ "\n- method name: "
+                     ^ method_name ^ "\n- all_generics:\n"
+                      ^ generic_args_to_string ctx all_generics
+                      ^ "\n- parent params info: "
+                      ^ Print.option_to_string show_params_info
+                          method_def.signature.parent_params_info));
+                  let regions_hierarchy =
+                    LlbcAstUtils.FunIdMap.find (FRegular method_id)
+                      ctx.fun_context.regions_hierarchies
+                  in
+                  let tr_self = TraitRef trait_ref in
+                  let inst_sg =
+                    instantiate_fun_sig ctx all_generics tr_self
+                      method_def.signature regions_hierarchy
+                  in
+                  (func.func, func.generics, method_def, inst_sg))
+          | _ ->
+              (* We are using a local clause - we lookup the trait decl *)
+              let trait_decl =
+                ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id
+              in
+              (* Lookup the method decl in the required *and* the provided methods *)
+              let _, method_id =
+                let provided =
+                  List.filter_map
+                    (fun (id, f) ->
+                      match f with None -> None | Some f -> Some (id, f))
+                    trait_decl.provided_methods
+                in
+                List.find
+                  (fun (s, _) -> s = method_name)
+                  (List.append trait_decl.required_methods provided)
+              in
+              let method_def = ctx_lookup_fun_decl ctx method_id in
+              log#ldebug
+                (lazy ("method:\n" ^ fun_decl_to_string ctx method_def));
+              (* Instantiate *)
+              let regions_hierarchy =
+                LlbcAstUtils.FunIdMap.find (FRegular method_id)
+                  ctx.fun_context.regions_hierarchies
+              in
+              let tr_self = TraitRef trait_ref in
+              let inst_sg =
+                instantiate_fun_sig ctx generics tr_self method_def.signature
+                  regions_hierarchy
+              in
+              (func.func, func.generics, method_def, inst_sg)))
+
 (** Evaluate a statement *)
-let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
+let rec eval_statement (config : config) (st : statement) : st_cm_fun =
  fun cf ctx ->
   (* Debugging *)
   log#ldebug
@@ -804,23 +907,23 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
    * checking the invariants *)
   let cc = greedy_expand_symbolic_values config in
   (* Sanity check *)
-  let cc = comp cc Inv.cf_check_invariants in
+  let cc = comp cc Invariants.cf_check_invariants in
 
   (* Evaluate *)
   let cf_eval_st cf : m_fun =
    fun ctx ->
     match st.content with
-    | A.Assign (p, rvalue) -> (
+    | Assign (p, rvalue) -> (
         (* We handle global assignments separately *)
         match rvalue with
-        | E.Global gid ->
+        | Global gid ->
             (* Evaluate the global *)
             eval_global config p gid cf ctx
         | _ ->
             (* Evaluate the rvalue *)
             let cf_eval_rvalue = eval_rvalue_not_global config rvalue in
             (* Assign *)
-            let cf_assign cf (res : (V.typed_value, eval_error) result) ctx =
+            let cf_assign cf (res : (typed_value, eval_error) result) ctx =
               log#ldebug
                 (lazy
                   ("about to assign to place: " ^ place_to_string ctx p
@@ -834,11 +937,10 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
                    * also it can lead to issues - for instance, if we borrow a
                    * reserved borrow, we later can't translate it to pure values...) *)
                   match rvalue with
-                  | E.Global _ -> raise (Failure "Unreachable")
-                  | E.Use _
-                  | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow))
-                  | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _
-                  | E.Aggregate _ ->
+                  | Global _ -> raise (Failure "Unreachable")
+                  | Use _
+                  | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow))
+                  | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ ->
                       let rp = rvalue_get_place rvalue in
                       let rp =
                         match rp with
@@ -851,18 +953,18 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
 
             (* Compose and apply *)
             comp cf_eval_rvalue cf_assign cf ctx)
-    | A.FakeRead p -> eval_fake_read config p (cf Unit) ctx
-    | A.SetDiscriminant (p, variant_id) ->
+    | FakeRead p -> eval_fake_read config p (cf Unit) ctx
+    | SetDiscriminant (p, variant_id) ->
         set_discriminant config p variant_id cf ctx
-    | A.Drop p -> drop_value config p (cf Unit) ctx
-    | A.Assert assertion -> eval_assertion config assertion cf ctx
-    | A.Call call -> eval_function_call config call cf ctx
-    | A.Panic -> cf Panic ctx
-    | A.Return -> cf Return ctx
-    | A.Break i -> cf (Break i) ctx
-    | A.Continue i -> cf (Continue i) ctx
-    | A.Nop -> cf Unit ctx
-    | A.Sequence (st1, st2) ->
+    | Drop p -> drop_value config p (cf Unit) ctx
+    | Assert assertion -> eval_assertion config assertion cf ctx
+    | Call call -> eval_function_call config call cf ctx
+    | Panic -> cf Panic ctx
+    | Return -> cf Return ctx
+    | Break i -> cf (Break i) ctx
+    | Continue i -> cf (Continue i) ctx
+    | Nop -> cf Unit ctx
+    | Sequence (st1, st2) ->
         (* Evaluate the first statement *)
         let cf_st1 = eval_statement config st1 in
         (* Evaluate the sequence *)
@@ -877,30 +979,36 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
         in
         (* Compose and apply *)
         comp cf_st1 cf_st2 cf ctx
-    | A.Loop loop_body ->
-        InterpreterLoops.eval_loop config
+    | Loop loop_body ->
+        InterpreterLoops.eval_loop config st.meta
           (eval_statement config loop_body)
           cf ctx
-    | A.Switch switch -> eval_switch config switch cf ctx
+    | Switch switch -> eval_switch config switch cf ctx
   in
   (* Compose and apply *)
   comp cc cf_eval_st cf ctx
 
-and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id)
-    : st_cm_fun =
+and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) :
+    st_cm_fun =
  fun cf ctx ->
-  let global = C.ctx_lookup_global_decl ctx gid in
+  let global = ctx_lookup_global_decl ctx gid in
   match config.mode with
   | ConcreteMode ->
       (* Treat the evaluation of the global as a call to the global body (without arguments) *)
-      (eval_local_function_call_concrete config global.body_id [] [] [] [] dest)
-        cf ctx
+      let func =
+        {
+          func = FunId (FRegular global.body);
+          generics = TypesUtils.empty_generic_args;
+          trait_and_method_generic_args = None;
+        }
+      in
+      let call = { func = FnOpRegular func; args = []; dest } in
+      (eval_transparent_function_call_concrete config global.body call) cf ctx
   | 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 Global global.ty in
       let cc =
         assign_to_place config (mk_typed_value_from_symbolic_value sval) dest
       in
@@ -908,7 +1016,7 @@ and eval_global (config : C.config) (dest : E.place) (gid : LA.GlobalDeclId.id)
       S.synthesize_global_eval gid sval e
 
 (** Evaluate a switch *)
-and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
+and eval_switch (config : config) (switch : switch) : st_cm_fun =
  fun cf ctx ->
   (* We evaluate the operand in two steps:
    * first we prepare it, then we check if its value is concrete or
@@ -922,14 +1030,14 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
   let cf_match : st_cm_fun =
    fun cf ctx ->
     match switch with
-    | A.If (op, st1, st2) ->
+    | If (op, st1, st2) ->
         (* Evaluate the operand *)
         let cf_eval_op = eval_operand config op in
         (* Switch on the value *)
-        let cf_if (cf : st_m_fun) (op_v : V.typed_value) : m_fun =
+        let cf_if (cf : st_m_fun) (op_v : typed_value) : m_fun =
          fun ctx ->
           match op_v.value with
-          | V.Literal (PV.Bool b) ->
+          | VLiteral (VBool b) ->
               (* Evaluate the if and the branch body *)
               let cf_branch cf : m_fun =
                 (* Branch *)
@@ -938,7 +1046,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
               in
               (* Compose the continuations *)
               cf_branch cf ctx
-          | V.Symbolic sv ->
+          | VSymbolic sv ->
               (* Expand the symbolic boolean, and continue by evaluating
                * the branches *)
               let cf_true : st_cm_fun = eval_statement config st1 in
@@ -950,18 +1058,18 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
         in
         (* Compose *)
         comp cf_eval_op cf_if cf ctx
-    | A.SwitchInt (op, int_ty, stgts, otherwise) ->
+    | SwitchInt (op, int_ty, stgts, otherwise) ->
         (* Evaluate the operand *)
         let cf_eval_op = eval_operand config op in
         (* Switch on the value *)
-        let cf_switch (cf : st_m_fun) (op_v : V.typed_value) : m_fun =
+        let cf_switch (cf : st_m_fun) (op_v : typed_value) : m_fun =
          fun ctx ->
           match op_v.value with
-          | V.Literal (PV.Scalar sv) ->
+          | VLiteral (VScalar sv) ->
               (* Evaluate the branch *)
               let cf_eval_branch cf =
                 (* Sanity check *)
-                assert (sv.PV.int_ty = int_ty);
+                assert (sv.int_ty = int_ty);
                 (* Find the branch *)
                 match List.find_opt (fun (svl, _) -> List.mem sv svl) stgts with
                 | None -> eval_statement config otherwise cf
@@ -969,7 +1077,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
               in
               (* Compose *)
               cf_eval_branch cf ctx
-          | V.Symbolic sv ->
+          | VSymbolic sv ->
               (* Expand the symbolic value and continue by evaluating the
                * proper branches *)
               let stgts =
@@ -997,7 +1105,7 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
         in
         (* Compose *)
         comp cf_eval_op cf_switch cf ctx
-    | A.Match (p, stgts, otherwise) ->
+    | Match (p, stgts, otherwise) ->
         (* Access the place *)
         let access = Read in
         let expand_prim_copy = false in
@@ -1005,21 +1113,21 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
           access_rplace_reorganize_and_read config expand_prim_copy access p cf
         in
         (* Match on the value *)
-        let cf_match (cf : st_m_fun) (p_v : V.typed_value) : m_fun =
+        let cf_match (cf : st_m_fun) (p_v : typed_value) : m_fun =
          fun ctx ->
           (* The value may be shared: we need to ignore the shared loans
              to read the value itself *)
           let p_v = value_strip_shared_loans p_v in
           (* Match *)
           match p_v.value with
-          | V.Adt adt -> (
+          | VAdt adt -> (
               (* Evaluate the discriminant *)
               let dv = Option.get adt.variant_id in
               (* Find the branch, evaluate and continue *)
               match List.find_opt (fun (svl, _) -> List.mem dv svl) stgts with
               | None -> eval_statement config otherwise cf ctx
               | Some (_, tgt) -> eval_statement config tgt cf ctx)
-          | V.Symbolic sv ->
+          | VSymbolic sv ->
               (* Expand the symbolic value - may lead to branching *)
               let cf_expand =
                 expand_symbolic_adt config sv (Some (S.mk_mplace p ctx))
@@ -1036,132 +1144,175 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
   cf_match cf ctx
 
 (** Evaluate a function call (auxiliary helper for [eval_statement]) *)
-and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
-  (* There are two cases:
+and eval_function_call (config : config) (call : call) : st_cm_fun =
+  (* There are several cases:
      - this is a local function, in which case we execute its body
-     - this is a non-local function, in which case there is a special treatment
+     - this is an assumed function, in which case there is a special treatment
+     - this is a trait method
   *)
-  match call.func with
-  | A.Regular fid ->
-      eval_local_function_call config fid call.region_args call.type_args
-        call.const_generic_args call.args call.dest
-  | A.Assumed fid ->
-      eval_non_local_function_call config fid call.region_args call.type_args
-        call.const_generic_args call.args call.dest
+  match config.mode with
+  | ConcreteMode -> eval_function_call_concrete config call
+  | SymbolicMode -> eval_function_call_symbolic config call
 
-(** 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_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
+and eval_function_call_concrete (config : config) (call : call) : st_cm_fun =
  fun cf ctx ->
-  (* Retrieve the (correctly instantiated) body *)
-  let def = C.ctx_lookup_fun_decl ctx fid in
-  (* We can evaluate the function call only if it is not opaque *)
-  let body =
-    match def.body with
-    | None ->
-        raise
-          (Failure
-             ("Can't evaluate a call to an opaque function: "
-             ^ Print.name_to_string def.name))
-    | Some body -> body
-  in
-  let tsubst =
-    Subst.make_type_subst_from_vars def.A.signature.type_params type_args
-  in
-  let cgsubst =
-    Subst.make_const_generic_subst_from_vars
-      def.A.signature.const_generic_params cg_args
-  in
-  let locals, body_st = Subst.fun_body_substitute_in_body tsubst cgsubst body in
-
-  (* Evaluate the input operands *)
-  assert (List.length args = body.A.arg_count);
-  let cc = eval_operands config args in
+  match call.func with
+  | FnOpMove _ -> raise (Failure "Closures are not supported yet")
+  | FnOpRegular func -> (
+      match func.func with
+      | FunId (FRegular fid) ->
+          eval_transparent_function_call_concrete config fid call cf ctx
+      | 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
+           * panic case into account... *)
+          eval_assumed_function_call_concrete config fid call (cf Unit) ctx
+      | TraitMethod _ -> raise (Failure "Unimplemented"))
+
+and eval_function_call_symbolic (config : config) (call : call) : st_cm_fun =
+  match call.func with
+  | FnOpMove _ -> raise (Failure "Closures are not supported yet")
+  | FnOpRegular func -> (
+      match func.func with
+      | FunId (FRegular _) | TraitMethod _ ->
+          eval_transparent_function_call_symbolic config call
+      | FunId (FAssumed fid) ->
+          eval_assumed_function_call_symbolic config fid call func)
 
-  (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
-   * of the operands evaluation from above to the functions afterwards, while
-   * ignoring it in this function *)
-  let cc = comp_transmit cc push_frame in
-
-  (* Compute the initial values for the local variables *)
-  (* 1. Push the return value *)
-  let ret_var, locals =
-    match locals with
-    | ret_ty :: locals -> (ret_ty, locals)
-    | _ -> raise (Failure "Unreachable")
-  in
-  let input_locals, locals =
-    Collections.List.split_at locals body.A.arg_count
-  in
+(** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
+and eval_transparent_function_call_concrete (config : config)
+    (fid : FunDeclId.id) (call : call) : st_cm_fun =
+  let args = call.args in
+  let dest = call.dest in
+  match call.func with
+  | FnOpMove _ -> raise (Failure "Closures are not supported yet")
+  | FnOpRegular func ->
+      let generics = func.generics in
+      (* Sanity check: we don't fully handle the const generic vars environment
+         in concrete mode yet *)
+      assert (generics.const_generics = []);
+      fun cf ctx ->
+        (* Retrieve the (correctly instantiated) body *)
+        let def = ctx_lookup_fun_decl ctx fid in
+        (* We can evaluate the function call only if it is not opaque *)
+        let body =
+          match def.body with
+          | None ->
+              raise
+                (Failure
+                   ("Can't evaluate a call to an opaque function: "
+                   ^ name_to_string ctx def.name))
+          | Some body -> body
+        in
+        (* TODO: we need to normalize the types if we want to correctly support traits *)
+        assert (generics.trait_refs = []);
+        (* There shouldn't be any reference to Self *)
+        let tr_self = UnknownTrait __FUNCTION__ in
+        let subst =
+          Subst.make_subst_from_generics def.signature.generics generics tr_self
+        in
+        let locals, body_st = Subst.fun_body_substitute_in_body subst body in
+
+        (* Evaluate the input operands *)
+        assert (List.length args = body.arg_count);
+        let cc = eval_operands config args in
+
+        (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
+         * of the operands evaluation from above to the functions afterwards, while
+         * ignoring it in this function *)
+        let cc = comp_transmit cc push_frame in
+
+        (* Compute the initial values for the local variables *)
+        (* 1. Push the return value *)
+        let ret_var, locals =
+          match locals with
+          | ret_ty :: locals -> (ret_ty, locals)
+          | _ -> raise (Failure "Unreachable")
+        in
+        let input_locals, locals =
+          Collections.List.split_at locals body.arg_count
+        in
 
-  let cc = comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty)) in
+        let cc =
+          comp_transmit cc (push_var ret_var (mk_bottom ret_var.var_ty))
+        in
 
-  (* 2. Push the input values *)
-  let cf_push_inputs cf args =
-    let inputs = List.combine input_locals args in
-    (* Note that this function checks that the variables and their values
-     * have the same type (this is important) *)
-    push_vars inputs cf
-  in
-  let cc = comp cc cf_push_inputs in
+        (* 2. Push the input values *)
+        let cf_push_inputs cf args =
+          let inputs = List.combine input_locals args in
+          (* Note that this function checks that the variables and their values
+           * have the same type (this is important) *)
+          push_vars inputs cf
+        in
+        let cc = comp cc cf_push_inputs in
 
-  (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
-  let cc = comp cc (push_uninitialized_vars locals) in
+        (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
+        let cc = comp cc (push_uninitialized_vars locals) in
 
-  (* Execute the function body *)
-  let cc = comp cc (eval_function_body config body_st) in
+        (* Execute the function body *)
+        let cc = comp cc (eval_function_body config body_st) in
 
-  (* Pop the stack frame and move the return value to its destination *)
-  let cf_finish cf res =
-    match res with
-    | Panic -> cf Panic
-    | Return ->
-        (* Pop the stack frame, retrieve the return value, move it to
-         * its destination and continue *)
-        pop_frame_assign config dest (cf Unit)
-    | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
-    | EndContinue _ ->
-        raise (Failure "Unreachable")
-  in
-  let cc = comp cc cf_finish in
+        (* Pop the stack frame and move the return value to its destination *)
+        let cf_finish cf res =
+          match res with
+          | Panic -> cf Panic
+          | Return ->
+              (* Pop the stack frame, retrieve the return value, move it to
+               * its destination and continue *)
+              pop_frame_assign config dest (cf Unit)
+          | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
+          | EndContinue _ ->
+              raise (Failure "Unreachable")
+        in
+        let cc = comp cc cf_finish in
 
-  (* Continue *)
-  cc cf ctx
+        (* Continue *)
+        cc cf ctx
 
 (** 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_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
+and eval_transparent_function_call_symbolic (config : config) (call : call) :
     st_cm_fun =
  fun cf ctx ->
-  (* Retrieve the (correctly instantiated) signature *)
-  let def = C.ctx_lookup_fun_decl ctx fid in
-  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_args cg_args sg in
+  let func, generics, def, inst_sg =
+    eval_transparent_function_call_symbolic_inst call ctx
+  in
   (* Sanity check *)
-  assert (List.length args = List.length def.A.signature.inputs);
+  assert (List.length call.args = List.length def.signature.inputs);
   (* Evaluate the function call *)
-  eval_function_call_symbolic_from_inst_sig config (A.Regular fid) inst_sg
-    region_args type_args cg_args args dest cf ctx
+  eval_function_call_symbolic_from_inst_sig config func inst_sg generics
+    call.args call.dest cf ctx
 
 (** Evaluate a function call in symbolic mode by using the function signature.
 
     This allows us to factorize the evaluation of local and non-local function
     calls in symbolic mode: only their signatures matter.
+
+    The [self_trait_ref] trait ref refers to [Self]. We use it when calling
+    a provided trait method, because those methods have a special treatment:
+    we dot not group them with the required trait methods, and forbid (for now)
+    overriding them. We treat them as regular method, which take an additional
+    trait ref as input.
  *)
-and eval_function_call_symbolic_from_inst_sig (config : C.config)
-    (fid : A.fun_id) (inst_sg : A.inst_fun_sig)
-    (_region_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
+and eval_function_call_symbolic_from_inst_sig (config : config)
+    (fid : fun_id_or_trait_method_ref) (inst_sg : inst_fun_sig)
+    (generics : generic_args) (args : operand list) (dest : place) : st_cm_fun =
  fun cf ctx ->
+  log#ldebug
+    (lazy
+      ("eval_function_call_symbolic_from_inst_sig:\n- fid: "
+      ^ fun_id_or_trait_method_ref_to_string ctx fid
+      ^ "\n- inst_sg:\n"
+      ^ inst_fun_sig_to_string ctx inst_sg
+      ^ "\n- call.generics:\n"
+      ^ 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));
+
   (* 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
+  let ret_sv_ty = inst_sg.output in
+  let ret_spc = mk_fresh_symbolic_value FunCallRet ret_sv_ty in
   let ret_value = mk_typed_value_from_symbolic_value ret_spc in
   let ret_av regions =
     mk_aproj_loans_value_from_symbolic_value regions ret_spc
@@ -1173,16 +1324,16 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
   let cc = eval_operands config args in
 
   (* Generate the abstractions and insert them in the context *)
-  let abs_ids = List.map (fun rg -> rg.T.id) inst_sg.regions_hierarchy in
-  let cf_call cf (args : V.typed_value list) : m_fun =
+  let abs_ids = List.map (fun rg -> rg.id) inst_sg.regions_hierarchy in
+  let cf_call cf (args : typed_value list) : m_fun =
    fun ctx ->
-    let args_with_rtypes = List.combine args inst_sg.A.inputs in
+    let args_with_rtypes = List.combine args inst_sg.inputs in
 
     (* Check the type of the input arguments *)
     assert (
       List.for_all
-        (fun ((arg, rty) : V.typed_value * T.rty) ->
-          arg.V.ty = Subst.erase_regions rty)
+        (fun ((arg, rty) : typed_value * rty) ->
+          arg.ty = Subst.erase_regions rty)
         args_with_rtypes);
     (* Check that the input arguments don't contain symbolic values that can't 
      * be fed to functions (i.e., symbolic values output from function return
@@ -1198,8 +1349,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
      * First, we define the function which, given an initialized, empty
      * abstraction, computes the avalues which should be inserted inside.
      *)
-    let compute_abs_avalues (abs : V.abs) (ctx : C.eval_ctx) :
-        C.eval_ctx * V.typed_avalue list =
+    let compute_abs_avalues (abs : abs) (ctx : eval_ctx) :
+        eval_ctx * typed_avalue list =
       (* Project over the input values *)
       let ctx, args_projs =
         List.fold_left_map
@@ -1212,20 +1363,20 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
       (ctx, List.append args_projs [ ret_av abs.regions ])
     in
     (* Actually initialize and insert the abstractions *)
-    let call_id = C.fresh_fun_call_id () in
+    let call_id = fresh_fun_call_id () in
     let region_can_end _ = true in
     let ctx =
       create_push_abstractions_from_abs_region_groups
-        (fun rg_id -> V.FunCall (call_id, rg_id))
-        inst_sg.A.regions_hierarchy region_can_end compute_abs_avalues ctx
+        (fun rg_id -> FunCall (call_id, rg_id))
+        inst_sg.regions_hierarchy region_can_end compute_abs_avalues ctx
     in
 
     (* Apply the continuation *)
     let expr = cf ctx in
 
     (* Synthesize the symbolic AST *)
-    S.synthesize_regular_function_call fid call_id ctx abs_ids type_args cg_args
-      args args_places ret_spc dest_place expr
+    S.synthesize_regular_function_call fid call_id ctx abs_ids generics args
+      args_places ret_spc dest_place expr
   in
   let cc = comp cc cf_call in
 
@@ -1245,9 +1396,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
       List.partition
         (fun abs_id ->
           (* Lookup the abstraction *)
-          let abs = C.ctx_lookup_abs ctx abs_id in
+          let abs = ctx_lookup_abs ctx abs_id in
           (* Check if it has parents *)
-          V.AbstractionId.Set.is_empty abs.parents
+          AbstractionId.Set.is_empty abs.parents
           (* Check if it contains non-ignored loans *)
           && Option.is_none
                (InterpreterBorrowsCore
@@ -1259,7 +1410,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
       (* Update the reference to the list of asbtraction ids, for the recursive calls *)
       abs_ids := with_loans_abs;
       (* End the abstractions which can be ended *)
-      let no_loans_abs = V.AbstractionId.Set.of_list no_loans_abs in
+      let no_loans_abs = AbstractionId.Set.of_list no_loans_abs in
       let cc = InterpreterBorrows.end_abstractions config no_loans_abs in
       (* Recursive call *)
       let cc = comp cc end_abs_with_no_loans in
@@ -1286,17 +1437,18 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
   cc (cf Unit) ctx
 
 (** 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_args : T.erased_region list)
-    (type_args : T.ety list) (cg_args : T.const_generic list)
-    (args : E.operand list) (dest : E.place) : st_cm_fun =
+and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id)
+    (call : call) (func : fn_ptr) : st_cm_fun =
  fun cf ctx ->
+  let generics = func.generics in
+  let args = call.args in
+  let dest = call.dest in
   (* Sanity check: make sure the type parameters don't contain regions -
    * this is a current limitation of our synthesis *)
   assert (
     List.for_all
       (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty))
-      type_args);
+      generics.types);
 
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
@@ -1304,10 +1456,10 @@ and eval_non_local_function_call_symbolic (config : C.config)
        See {!eval_box_free}
   *)
   match fid with
-  | A.BoxFree ->
+  | 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_args type_args cg_args args dest (cf Unit) ctx
+      eval_box_free config generics args dest (cf Unit) ctx
   | _ ->
       (* "Normal" case: not box_free *)
       (* In symbolic mode, the behaviour of a function call is completely defined
@@ -1315,62 +1467,27 @@ and eval_non_local_function_call_symbolic (config : C.config)
        * instantiated signatures, and delegate the work to an auxiliary function *)
       let inst_sig =
         match fid with
-        | A.BoxFree ->
-            (* should have been treated above *)
+        | BoxFree ->
+            (* Should have been treated above *)
             raise (Failure "Unreachable")
         | _ ->
-            instantiate_fun_sig type_args cg_args (Assumed.get_assumed_sig fid)
+            let regions_hierarchy =
+              LlbcAstUtils.FunIdMap.find (FAssumed fid)
+                ctx.fun_context.regions_hierarchies
+            in
+            (* There shouldn't be any reference to Self *)
+            let tr_self = UnknownTrait __FUNCTION__ in
+            instantiate_fun_sig ctx generics tr_self
+              (Assumed.get_assumed_fun_sig fid)
+              regions_hierarchy
       in
 
       (* Evaluate the function call *)
-      eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig
-        region_args type_args cg_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_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
- fun cf ctx ->
-  (* Debug *)
-  log#ldebug
-    (lazy
-      (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_args: " ^ type_args ^ "\n- args: " ^ args ^ "\n- dest: "
-       ^ dest));
-
-  match config.mode with
-  | C.ConcreteMode ->
-      eval_non_local_function_call_concrete config fid region_args type_args
-        cg_args args dest (cf Unit) ctx
-  | C.SymbolicMode ->
-      eval_non_local_function_call_symbolic config fid region_args type_args
-        cg_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_args : T.erased_region list) (type_args : T.ety list)
-    (cg_args : T.const_generic list) (args : E.operand list) (dest : E.place) :
-    st_cm_fun =
-  match config.mode with
-  | ConcreteMode ->
-      eval_local_function_call_concrete config fid region_args type_args cg_args
-        args dest
-  | SymbolicMode ->
-      eval_local_function_call_symbolic config fid region_args type_args cg_args
-        args dest
+      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 *)
-and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
+and eval_function_body (config : config) (body : statement) : st_cm_fun =
  fun cf ctx ->
   let cc = eval_statement config body in
   let cf_finish cf res =
@@ -1380,7 +1497,7 @@ and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
      * checking the invariants *)
     let cc = greedy_expand_symbolic_values config in
     (* Sanity check *)
-    let cc = comp_check_ctx cc Inv.check_invariants in
+    let cc = comp_check_ctx cc Invariants.check_invariants in
     (* Continue *)
     cc (cf res)
   in
diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli
index 814bc964..3832d02f 100644
--- a/compiler/InterpreterStatements.mli
+++ b/compiler/InterpreterStatements.mli
@@ -1,15 +1,8 @@
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module A = LlbcAst
-module L = Logging
-module Inv = Invariants
-module S = SynthesizeSymbolic
+open Types
+open Values
+open Contexts
+open LlbcAst
 open Cps
-open InterpreterExpressions
 
 (** Pop the current frame.
 
@@ -17,22 +10,13 @@ open InterpreterExpressions
     dummy variables, after ending the proper borrows of course) but the return
     variable, move the return value out of the return variable, remove all the
     local variables (but preserve the abstractions!), remove the
-    {!constructor:C.env_elem.Frame} indicator delimiting the current frame and
+    {!constructor:Contexts.env_elem.EFrame} indicator delimiting the current frame and
     handle the return value to the continuation.
 
     If the boolean is false, we don't move the return value, and call the
     continuation with [None].
  *)
-val pop_frame : C.config -> bool -> (V.typed_value option -> m_fun) -> m_fun
-
-(** Instantiate a function signature, introducing **fresh** abstraction ids and
-    region ids. This is mostly used in preparation of function calls, when
-    evaluating in symbolic mode of course.
-
-    Note: there are no region parameters, because they should be erased.
- *)
-val instantiate_fun_sig :
-  T.ety list -> T.const_generic list -> LA.fun_sig -> LA.inst_fun_sig
+val pop_frame : config -> bool -> (typed_value option -> m_fun) -> m_fun
 
 (** Helper.
 
@@ -53,15 +37,15 @@ val instantiate_fun_sig :
     - [ctx]
 *)
 val create_push_abstractions_from_abs_region_groups :
-  (T.RegionGroupId.id -> V.abs_kind) ->
-  LA.abs_region_group list ->
-  (T.RegionGroupId.id -> bool) ->
-  (V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list) ->
-  C.eval_ctx ->
-  C.eval_ctx
+  (RegionGroupId.id -> abs_kind) ->
+  abs_region_group list ->
+  (RegionGroupId.id -> bool) ->
+  (abs -> eval_ctx -> eval_ctx * typed_avalue list) ->
+  eval_ctx ->
+  eval_ctx
 
 (** Evaluate a statement *)
-val eval_statement : C.config -> LA.statement -> st_cm_fun
+val eval_statement : config -> statement -> st_cm_fun
 
 (** Evaluate a statement seen as a function body *)
-val eval_function_body : C.config -> LA.statement -> st_cm_fun
+val eval_function_body : config -> statement -> st_cm_fun