1 files changed, 78 insertions, 84 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index cd7952e0..74e4e815 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -10,100 +10,94 @@ open InterpreterStatements
 (** The local logger *)
 let log = L.interpreter_log
 
-module Test = struct
-  let initialize_context (m : M.cfim_module) (type_vars : T.type_var list) :
-      C.eval_ctx =
-    let type_decls, _ = M.split_declarations m.declarations in
-    let type_defs, fun_defs = M.compute_defs_maps m in
-    let type_defs_groups, _funs_defs_groups =
-      M.split_declarations_to_group_maps m.declarations
-    in
-    let type_infos =
-      TypesAnalysis.analyze_type_declarations type_defs type_decls
-    in
-    let type_context = { C.type_defs_groups; type_defs; type_infos } in
-    C.reset_global_counters ();
-    {
-      C.type_context;
-      C.fun_context = fun_defs;
-      C.type_vars;
-      C.env = [];
-      C.ended_regions = T.RegionId.Set.empty;
-    }
-
-  (** Initialize an evaluation context to execute a function.
+let initialize_context (m : M.cfim_module) (type_vars : T.type_var list) :
+    C.eval_ctx =
+  let type_decls, _ = M.split_declarations m.declarations in
+  let type_defs, fun_defs = M.compute_defs_maps m in
+  let type_defs_groups, _funs_defs_groups =
+    M.split_declarations_to_group_maps m.declarations
+  in
+  let type_infos =
+    TypesAnalysis.analyze_type_declarations type_defs type_decls
+  in
+  let type_context = { C.type_defs_groups; type_defs; type_infos } in
+  C.reset_global_counters ();
+  {
+    C.type_context;
+    C.fun_context = fun_defs;
+    C.type_vars;
+    C.env = [];
+    C.ended_regions = T.RegionId.Set.empty;
+  }
+
+(** Initialize an evaluation context to execute a function.
 
       Introduces local variables initialized in the following manner:
       - input arguments are initialized as symbolic values
       - the remaining locals are initialized as ⊥
       Abstractions are introduced for the regions present in the function
       signature.
-   *)
-  let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def)
-      : C.eval_ctx =
-    (* The abstractions are not initialized the same way as for function
-     * calls: they contain *loan* projectors, because they "provide" us
-     * with the input values (which behave as if they had been returned
-     * by some function calls...).
-     * Also, note that we properly set the set of parents of every abstraction:
-     * this should not be necessary, as those abstractions should never be
-     * *automatically* ended (because ending some borrows requires to end
-     * one of them), but rather selectively ended when generating code
-     * for each of the backward functions. We do it only because we can
-     * do it, and because it gives a bit of sanity.
-     * *)
-    let sg = fdef.signature in
-    (* Create the context *)
-    let ctx = initialize_context m sg.type_params in
-    (* Instantiate the signature *)
-    let type_params =
-      List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params
-    in
-    let inst_sg = instantiate_fun_sig type_params sg in
-    (* Create fresh symbolic values for the inputs *)
-    let input_svs =
-      List.map
-        (fun ty -> mk_fresh_symbolic_value V.SynthInput ty)
-        inst_sg.inputs
+ *)
+let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) :
+    C.eval_ctx =
+  (* The abstractions are not initialized the same way as for function
+   * calls: they contain *loan* projectors, because they "provide" us
+   * with the input values (which behave as if they had been returned
+   * by some function calls...).
+   * Also, note that we properly set the set of parents of every abstraction:
+   * this should not be necessary, as those abstractions should never be
+   * *automatically* ended (because ending some borrows requires to end
+   * one of them), but rather selectively ended when generating code
+   * for each of the backward functions. We do it only because we can
+   * do it, and because it gives a bit of sanity.
+   * *)
+  let sg = fdef.signature in
+  (* Create the context *)
+  let ctx = initialize_context m sg.type_params in
+  (* Instantiate the signature *)
+  let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in
+  let inst_sg = instantiate_fun_sig type_params sg in
+  (* Create fresh symbolic values for the inputs *)
+  let input_svs =
+    List.map (fun ty -> mk_fresh_symbolic_value V.SynthInput ty) inst_sg.inputs
+  in
+  (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
+  let call_id = C.fresh_fun_call_id () in
+  assert (call_id = V.FunCallId.zero);
+  let empty_absl =
+    create_empty_abstractions_from_abs_region_groups call_id V.SynthInput
+      inst_sg.A.regions_hierarchy
+  in
+  (* Add the avalues to the abstractions and insert them in the context *)
+  let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx =
+    (* Project over the values - we use *loan* projectors, as explained above *)
+    let avalues =
+      List.map (mk_aproj_loans_value_from_symbolic_value abs.regions) input_svs
     in
-    (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
-    let call_id = C.fresh_fun_call_id () in
-    assert (call_id = V.FunCallId.zero);
-    let empty_absl =
-      create_empty_abstractions_from_abs_region_groups call_id V.SynthInput
-        inst_sg.A.regions_hierarchy
-    in
-    (* Add the avalues to the abstractions and insert them in the context *)
-    let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx =
-      (* Project over the values - we use *loan* projectors, as explained above *)
-      let avalues =
-        List.map
-          (mk_aproj_loans_value_from_symbolic_value abs.regions)
-          input_svs
-      in
-      (* Insert the avalues in the abstraction *)
-      let abs = { abs with avalues } in
-      (* Insert the abstraction in the context *)
-      let ctx = { ctx with env = Abs abs :: ctx.env } in
-      (* Return *)
-      ctx
-    in
-    let ctx = List.fold_left insert_abs ctx empty_absl in
-    (* Split the variables between return var, inputs and remaining locals *)
-    let ret_var = List.hd fdef.locals in
-    let input_vars, local_vars =
-      Collections.List.split_at (List.tl fdef.locals) fdef.arg_count
-    in
-    (* Push the return variable (initialized with ⊥) *)
-    let ctx = C.ctx_push_uninitialized_var ctx ret_var in
-    (* Push the input variables (initialized with symbolic values) *)
-    let input_values = List.map mk_typed_value_from_symbolic_value input_svs in
-    let ctx = C.ctx_push_vars ctx (List.combine input_vars input_values) in
-    (* Push the remaining local variables (initialized with ⊥) *)
-    let ctx = C.ctx_push_uninitialized_vars ctx local_vars in
+    (* Insert the avalues in the abstraction *)
+    let abs = { abs with avalues } in
+    (* Insert the abstraction in the context *)
+    let ctx = { ctx with env = Abs abs :: ctx.env } in
     (* Return *)
     ctx
+  in
+  let ctx = List.fold_left insert_abs ctx empty_absl in
+  (* Split the variables between return var, inputs and remaining locals *)
+  let ret_var = List.hd fdef.locals in
+  let input_vars, local_vars =
+    Collections.List.split_at (List.tl fdef.locals) fdef.arg_count
+  in
+  (* Push the return variable (initialized with ⊥) *)
+  let ctx = C.ctx_push_uninitialized_var ctx ret_var in
+  (* Push the input variables (initialized with symbolic values) *)
+  let input_values = List.map mk_typed_value_from_symbolic_value input_svs in
+  let ctx = C.ctx_push_vars ctx (List.combine input_vars input_values) in
+  (* Push the remaining local variables (initialized with ⊥) *)
+  let ctx = C.ctx_push_uninitialized_vars ctx local_vars in
+  (* Return *)
+  ctx
 
+module Test = struct
   (** Test a unit function (taking no arguments) by evaluating it in an empty
       environment.
    *)