Do more cleanup

2 files changed, 34 insertions, 38 deletions

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 30b9316d..f88fc977 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -1,12 +1,7 @@
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module A = LlbcAst
+open Types
+open Values
+open Contexts
 open ValuesUtils
-module Inv = Invariants
 module S = SynthesizeSymbolic
 open Cps
 open InterpreterUtils
@@ -22,7 +17,7 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
  fun cf ctx ->
   (* We need a loop id for the [LoopReturn]. In practice it won't be used
      (it is useful only for the symbolic execution *)
-  let loop_id = C.fresh_loop_id () in
+  let loop_id = fresh_loop_id () in
   (* Continuation for after we evaluate the loop body: depending the result
      of doing one loop iteration:
      - redoes a loop iteration
@@ -65,7 +60,7 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
   eval_loop_body reeval_loop_body ctx
 
 (** Evaluate a loop in symbolic mode *)
-let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
+let eval_loop_symbolic (config : config) (eval_loop_body : st_cm_fun) :
     st_cm_fun =
  fun cf ctx ->
   (* Debug *)
@@ -73,7 +68,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
     (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string ctx ^ "\n\n"));
 
   (* Generate a fresh loop id *)
-  let loop_id = C.fresh_loop_id () in
+  let loop_id = fresh_loop_id () in
 
   (* Compute the fixed point at the loop entrance *)
   let fp_ctx, fixed_ids, rg_to_abs =
@@ -88,7 +83,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
 
   (* Compute the loop input parameters *)
   let fresh_sids, input_svalues = compute_fp_ctx_symbolic_values ctx fp_ctx in
-  let fp_input_svalues = List.map (fun sv -> sv.V.sv_id) input_svalues in
+  let fp_input_svalues = List.map (fun sv -> sv.sv_id) input_svalues in
 
   (* Synthesize the end of the function - we simply match the context at the
      loop entry with the fixed point: in the synthesized code, the function
@@ -139,9 +134,9 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
       ^ "\n- fixed point:\n"
       ^ eval_ctx_to_string_no_filter fp_ctx
       ^ "\n- fixed_sids: "
-      ^ V.SymbolicValueId.Set.show fixed_ids.sids
+      ^ SymbolicValueId.Set.show fixed_ids.sids
       ^ "\n- fresh_sids: "
-      ^ V.SymbolicValueId.Set.show fresh_sids
+      ^ SymbolicValueId.Set.show fresh_sids
       ^ "\n- input_svalues: "
       ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues
       ^ "\n\n"));
@@ -154,9 +149,9 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
      is important in {!SymbolicToPure}, where we expect the given back
      values to have a specific order.
   *)
-  let compute_abs_given_back_tys (abs : V.abs) : T.RegionId.Set.t * T.rty list =
-    let is_borrow (av : V.typed_avalue) : bool =
-      match av.V.value with
+  let compute_abs_given_back_tys (abs : abs) : RegionId.Set.t * rty list =
+    let is_borrow (av : typed_avalue) : bool =
+      match av.value with
       | ABorrow _ -> true
       | ALoan _ -> false
       | _ -> raise (Failure "Unreachable")
@@ -165,25 +160,25 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
 
     let borrows =
       List.filter_map
-        (fun av ->
-          match av.V.value with
-          | V.ABorrow (V.AMutBorrow (bid, child_av)) ->
-              assert (is_aignored child_av.V.value);
-              Some (bid, child_av.V.ty)
-          | V.ABorrow (V.ASharedBorrow _) -> None
+        (fun (av : typed_avalue) ->
+          match av.value with
+          | ABorrow (AMutBorrow (bid, child_av)) ->
+              assert (is_aignored child_av.value);
+              Some (bid, child_av.ty)
+          | ABorrow (ASharedBorrow _) -> None
           | _ -> raise (Failure "Unreachable"))
         borrows
     in
-    let borrows = ref (V.BorrowId.Map.of_list borrows) in
+    let borrows = ref (BorrowId.Map.of_list borrows) in
 
     let loan_ids =
       List.filter_map
-        (fun av ->
-          match av.V.value with
-          | V.ALoan (V.AMutLoan (bid, child_av)) ->
-              assert (is_aignored child_av.V.value);
+        (fun (av : typed_avalue) ->
+          match av.value with
+          | ALoan (AMutLoan (bid, child_av)) ->
+              assert (is_aignored child_av.value);
               Some bid
-          | V.ALoan (V.ASharedLoan _) -> None
+          | ALoan (ASharedLoan _) -> None
           | _ -> raise (Failure "Unreachable"))
         loans
     in
@@ -193,28 +188,28 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
       List.map
         (fun lid ->
           let bid =
-            V.BorrowId.InjSubst.find lid fp_bl_corresp.loan_to_borrow_id_map
+            BorrowId.InjSubst.find lid fp_bl_corresp.loan_to_borrow_id_map
           in
-          let ty = V.BorrowId.Map.find bid !borrows in
-          borrows := V.BorrowId.Map.remove bid !borrows;
+          let ty = BorrowId.Map.find bid !borrows in
+          borrows := BorrowId.Map.remove bid !borrows;
           ty)
         loan_ids
     in
-    assert (V.BorrowId.Map.is_empty !borrows);
+    assert (BorrowId.Map.is_empty !borrows);
 
     (abs.regions, given_back_tys)
   in
   let rg_to_given_back =
-    T.RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs
+    RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs
   in
 
   (* Put together *)
   S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back end_expr
     loop_expr
 
-let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun =
+let eval_loop (config : config) (eval_loop_body : st_cm_fun) : st_cm_fun =
  fun cf ctx ->
-  match config.C.mode with
+  match config.mode with
   | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx
   | SymbolicMode ->
       (* We want to make sure the loop will *not* manipulate shared avalues
diff --git a/compiler/InterpreterLoops.mli b/compiler/InterpreterLoops.mli
index 7395739b..320e4bcb 100644
--- a/compiler/InterpreterLoops.mli
+++ b/compiler/InterpreterLoops.mli
@@ -56,7 +56,8 @@
     From here, we deduce that [abs@fp { MB l0, ML l1}] is the loop abstraction.
   *)
 
-module C = Contexts
+open Contexts
+open Cps
 
 (** Evaluate a loop *)
-val eval_loop : C.config -> Cps.st_cm_fun -> Cps.st_cm_fun
+val eval_loop : config -> st_cm_fun -> st_cm_fun