Merge branch 'main' into son_fixes2

1 files changed, 14 insertions, 30 deletions

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