4 files changed, 49 insertions, 7 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index dfa7527e..b693a4db 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -180,8 +180,8 @@ let var_of_json (js : json) : (var, string) result =
     | `Assoc [ ("index", index); ("name", name); ("ty", ty) ] ->
         let* index = VarId.id_of_json index in
         let* name = string_option_of_json name in
-        let* ty = ety_of_json ty in
-        Ok { index; name; ty }
+        let* var_ty = ety_of_json ty in
+        Ok { index; name; var_ty }
     | _ -> Error "")
 
 let big_int_of_json (js : json) : (big_int, string) result =
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 74cbe70d..77af0b54 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1933,4 +1933,27 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
 
 and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) :
     (C.eval_ctx * statement_eval_res) eval_result =
+  (* There are two 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
+  *)
+  match call.func with
+  | A.Local fid ->
+      eval_local_function_call fid call.region_params call.type_params call.args
+        call.dest
+  | A.Assumed fid ->
+      eval_assumed_function_call fid call.region_params call.type_params
+        call.args call.dest
+
+and eval_local_function_call (fid : A.FunDefId.id)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (args : E.operand list) (dest : E.place) :
+    (C.eval_ctx * statement_eval_res) eval_result =
+  (* Retrieve the (correctly instantiated) body *)
+  raise Unimplemented
+
+and eval_assumed_function_call (fid : A.assumed_fun_id)
+    (region_params : T.erased_region list) (type_params : T.ety list)
+    (args : E.operand list) (dest : E.place) :
+    (C.eval_ctx * statement_eval_res) eval_result =
   raise Unimplemented
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 917275af..5cd62c0c 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -4,13 +4,14 @@
 
 module T = Types
 module V = Values
+module A = CfimAst
 module C = Contexts
 
 (** Substitute types variables and regions in a type *)
-let rec ty_subst (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty)
-    (ty : 'r1 T.ty) : 'r2 T.ty =
+let rec ty_substitute (rsubst : 'r1 -> 'r2)
+    (tsubst : T.TypeVarId.id -> 'r2 T.ty) (ty : 'r1 T.ty) : 'r2 T.ty =
   let open T in
-  let subst = ty_subst rsubst tsubst in
+  let subst = ty_substitute rsubst tsubst in
   (* helper *)
   match ty with
   | Adt (def_id, regions, tys) ->
@@ -34,7 +35,7 @@ let rec ty_subst (rsubst : 'r1 -> 'r2) (tsubst : T.TypeVarId.id -> 'r2 T.ty)
 let erase_regions_substitute_types (tsubst : T.TypeVarId.id -> T.ety)
     (ty : T.rty) : T.ety =
   let rsubst (r : T.RegionVarId.id T.region) : T.erased_region = T.Erased in
-  ty_subst rsubst tsubst ty
+  ty_substitute rsubst tsubst ty
 
 (** Create a type substitution from a list of type variable ids and a list of
     types (with which to substitute the type variable ids *)
@@ -90,3 +91,21 @@ let ctx_adt_get_instantiated_field_types (ctx : C.eval_ctx)
     (types : T.ety list) : T.ety T.FieldId.vector =
   let def = C.ctx_lookup_type_def ctx def_id in
   type_def_get_instantiated_field_type def opt_variant_id types
+
+(** Apply a type substitution to an expression *)
+let rec expression_substitute (tsubst : T.TypeVarId.id -> T.ety)
+    (e : A.expression) : A.expression =
+  raise Errors.Unimplemented
+
+(** Apply a type substitution to a function body. Return the local variables
+    and the body. *)
+let fun_def_substitute_in_body (tsubst : T.TypeVarId.id -> T.ety)
+    (def : A.fun_def) : V.var V.VarId.vector * A.expression =
+  let rsubst r = r in
+  let locals =
+    V.VarId.map
+      (fun v -> { v with V.var_ty = ty_substitute rsubst tsubst v.V.var_ty })
+      def.A.locals
+  in
+  let body = expression_substitute tsubst def.body in
+  (locals, body)
diff --git a/src/Values.ml b/src/Values.ml
index 5c31feef..2c80cfe9 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -14,7 +14,7 @@ module RegionId = IdGen ()
 type var = {
   index : VarId.id;  (** Unique variable identifier *)
   name : string option;
-  ty : ety;
+  var_ty : ety;
       (** The variable type - erased type, because variables are not used
        ** in function signatures *)
 }