Merge branch 'main' into son_fixes2

1 files changed, 130 insertions, 144 deletions

diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 6e33c75b..ca1f8f31 100644
--- a/compiler/InterpreterLoopsCore.ml
+++ b/compiler/InterpreterLoopsCore.ml
@@ -1,26 +1,17 @@
 (** Core definitions for the [IntepreterLoops*] *)
 
-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
-module UF = UnionFind
+open Types
+open Values
+open Contexts
 open InterpreterUtils
-open InterpreterExpressions
 
 type updt_env_kind =
-  | AbsInLeft of V.AbstractionId.id
-  | LoanInLeft of V.BorrowId.id
-  | LoansInLeft of V.BorrowId.Set.t
-  | AbsInRight of V.AbstractionId.id
-  | LoanInRight of V.BorrowId.id
-  | LoansInRight of V.BorrowId.Set.t
+  | AbsInLeft of AbstractionId.id
+  | LoanInLeft of BorrowId.id
+  | LoansInLeft of BorrowId.Set.t
+  | AbsInRight of AbstractionId.id
+  | LoanInRight of BorrowId.id
+  | LoansInRight of BorrowId.Set.t
 
 (** Utility exception *)
 exception ValueMatchFailure of updt_env_kind
@@ -28,10 +19,10 @@ exception ValueMatchFailure of updt_env_kind
 (** Utility exception *)
 exception Distinct of string
 
-type ctx_or_update = (C.eval_ctx, updt_env_kind) result
+type ctx_or_update = (eval_ctx, updt_env_kind) result
 
 (** Union Find *)
-module UnionFind = UF.Make (UF.StoreMap)
+module UF = UnionFind.Make (UnionFind.StoreMap)
 
 (** A small utility -
 
@@ -41,29 +32,29 @@ module UnionFind = UF.Make (UF.StoreMap)
     instance, [borrow_to_abs] maps to a *set* of ids).
 *)
 type abs_borrows_loans_maps = {
-  abs_ids : V.AbstractionId.id list;
-  abs_to_borrows : V.BorrowId.Set.t V.AbstractionId.Map.t;
-  abs_to_loans : V.BorrowId.Set.t V.AbstractionId.Map.t;
-  abs_to_borrows_loans : V.BorrowId.Set.t V.AbstractionId.Map.t;
-  borrow_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t;
-  loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t;
-  borrow_loan_to_abs : V.AbstractionId.Set.t V.BorrowId.Map.t;
+  abs_ids : AbstractionId.id list;
+  abs_to_borrows : BorrowId.Set.t AbstractionId.Map.t;
+  abs_to_loans : BorrowId.Set.t AbstractionId.Map.t;
+  abs_to_borrows_loans : BorrowId.Set.t AbstractionId.Map.t;
+  borrow_to_abs : AbstractionId.Set.t BorrowId.Map.t;
+  loan_to_abs : AbstractionId.Set.t BorrowId.Map.t;
+  borrow_loan_to_abs : AbstractionId.Set.t BorrowId.Map.t;
 }
 
-(** See {!InterpreterLoopsMatchCtxs.MakeMatcher} and {!InterpreterLoopsCore.Matcher}.
+(** See {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} and [Matcher].
 
     This module contains primitive match functions to instantiate the generic
-    {!InterpreterLoopsMatchCtxs.MakeMatcher} functor.
+    {!module:Aeneas.InterpreterLoopsMatchCtxs.MakeMatcher} functor.
   *)
 module type PrimMatcher = sig
-  val match_etys : T.ety -> T.ety -> T.ety
-  val match_rtys : T.rty -> T.rty -> T.rty
+  val match_etys : ety -> ety -> ety
+  val match_rtys : rty -> rty -> rty
 
   (** The input primitive values are not equal *)
-  val match_distinct_literals : T.ety -> V.literal -> V.literal -> V.typed_value
+  val match_distinct_literals : ety -> literal -> literal -> typed_value
 
   (** The input ADTs don't have the same variant *)
-  val match_distinct_adts : T.ety -> V.adt_value -> V.adt_value -> V.typed_value
+  val match_distinct_adts : ety -> adt_value -> adt_value -> typed_value
 
   (** The meta-value is the result of a match.
 
@@ -76,11 +67,11 @@ module type PrimMatcher = sig
       calling the match function.
    *)
   val match_shared_borrows :
-    (V.typed_value -> V.typed_value -> V.typed_value) ->
-    T.ety ->
-    V.borrow_id ->
-    V.borrow_id ->
-    V.borrow_id
+    (typed_value -> typed_value -> typed_value) ->
+    ety ->
+    borrow_id ->
+    borrow_id ->
+    borrow_id
 
   (** The input parameters are:
       - [ty]
@@ -91,13 +82,13 @@ module type PrimMatcher = sig
       - [bv]: the result of matching [bv0] with [bv1]
   *)
   val match_mut_borrows :
-    T.ety ->
-    V.borrow_id ->
-    V.typed_value ->
-    V.borrow_id ->
-    V.typed_value ->
-    V.typed_value ->
-    V.borrow_id * V.typed_value
+    ety ->
+    borrow_id ->
+    typed_value ->
+    borrow_id ->
+    typed_value ->
+    typed_value ->
+    borrow_id * typed_value
 
   (** Parameters:
       [ty]
@@ -106,17 +97,16 @@ module type PrimMatcher = sig
       [v]: the result of matching the shared values coming from the two loans
    *)
   val match_shared_loans :
-    T.ety ->
-    V.loan_id_set ->
-    V.loan_id_set ->
-    V.typed_value ->
-    V.loan_id_set * V.typed_value
+    ety ->
+    loan_id_set ->
+    loan_id_set ->
+    typed_value ->
+    loan_id_set * typed_value
 
-  val match_mut_loans : T.ety -> V.loan_id -> V.loan_id -> V.loan_id
+  val match_mut_loans : ety -> loan_id -> loan_id -> loan_id
 
   (** There are no constraints on the input symbolic values *)
-  val match_symbolic_values :
-    V.symbolic_value -> V.symbolic_value -> V.symbolic_value
+  val match_symbolic_values : symbolic_value -> symbolic_value -> symbolic_value
 
   (** Match a symbolic value with a value which is not symbolic.
 
@@ -126,7 +116,7 @@ module type PrimMatcher = sig
       end loans in one of the two environments).
    *)
   val match_symbolic_with_other :
-    bool -> V.symbolic_value -> V.typed_value -> V.typed_value
+    bool -> symbolic_value -> typed_value -> typed_value
 
   (** Match a bottom value with a value which is not bottom.
 
@@ -135,11 +125,11 @@ module type PrimMatcher = sig
       is important when throwing exceptions, for instance when we need to
       end loans in one of the two environments).
    *)
-  val match_bottom_with_other : bool -> V.typed_value -> V.typed_value
+  val match_bottom_with_other : bool -> typed_value -> typed_value
 
   (** The input ADTs don't have the same variant *)
   val match_distinct_aadts :
-    T.rty -> V.adt_avalue -> T.rty -> V.adt_avalue -> T.rty -> V.typed_avalue
+    rty -> adt_avalue -> rty -> adt_avalue -> rty -> typed_avalue
 
   (** Parameters:
       [ty0]
@@ -149,7 +139,7 @@ module type PrimMatcher = sig
       [ty]: result of matching ty0 and ty1
    *)
   val match_ashared_borrows :
-    T.rty -> V.borrow_id -> T.rty -> V.borrow_id -> T.rty -> V.typed_avalue
+    rty -> borrow_id -> rty -> borrow_id -> rty -> typed_avalue
 
   (** Parameters:
       [ty0]
@@ -162,15 +152,15 @@ module type PrimMatcher = sig
       [av]: result of matching av0 and av1
    *)
   val match_amut_borrows :
-    T.rty ->
-    V.borrow_id ->
-    V.typed_avalue ->
-    T.rty ->
-    V.borrow_id ->
-    V.typed_avalue ->
-    T.rty ->
-    V.typed_avalue ->
-    V.typed_avalue
+    rty ->
+    borrow_id ->
+    typed_avalue ->
+    rty ->
+    borrow_id ->
+    typed_avalue ->
+    rty ->
+    typed_avalue ->
+    typed_avalue
 
   (** Parameters:
       [ty0]
@@ -186,18 +176,18 @@ module type PrimMatcher = sig
       [av]: result of matching av0 and av1
    *)
   val match_ashared_loans :
-    T.rty ->
-    V.loan_id_set ->
-    V.typed_value ->
-    V.typed_avalue ->
-    T.rty ->
-    V.loan_id_set ->
-    V.typed_value ->
-    V.typed_avalue ->
-    T.rty ->
-    V.typed_value ->
-    V.typed_avalue ->
-    V.typed_avalue
+    rty ->
+    loan_id_set ->
+    typed_value ->
+    typed_avalue ->
+    rty ->
+    loan_id_set ->
+    typed_value ->
+    typed_avalue ->
+    rty ->
+    typed_value ->
+    typed_avalue ->
+    typed_avalue
 
   (** Parameters:
       [ty0]
@@ -210,20 +200,20 @@ module type PrimMatcher = sig
       [av]: result of matching av0 and av1
    *)
   val match_amut_loans :
-    T.rty ->
-    V.borrow_id ->
-    V.typed_avalue ->
-    T.rty ->
-    V.borrow_id ->
-    V.typed_avalue ->
-    T.rty ->
-    V.typed_avalue ->
-    V.typed_avalue
+    rty ->
+    borrow_id ->
+    typed_avalue ->
+    rty ->
+    borrow_id ->
+    typed_avalue ->
+    rty ->
+    typed_avalue ->
+    typed_avalue
 
   (** Match two arbitrary avalues whose constructors don't match (this function
       is typically used to raise the proper exception).
    *)
-  val match_avalues : V.typed_avalue -> V.typed_avalue -> V.typed_avalue
+  val match_avalues : typed_avalue -> typed_avalue -> typed_avalue
 end
 
 module type Matcher = sig
@@ -231,19 +221,18 @@ module type Matcher = sig
 
       Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}.
    *)
-  val match_typed_values :
-    C.eval_ctx -> V.typed_value -> V.typed_value -> V.typed_value
+  val match_typed_values : eval_ctx -> typed_value -> typed_value -> typed_value
 
   (** Match two avalues.
 
       Rem.: this function raises exceptions of type {!Aeneas.InterpreterLoopsCore.ValueMatchFailure}.
    *)
   val match_typed_avalues :
-    C.eval_ctx -> V.typed_avalue -> V.typed_avalue -> V.typed_avalue
+    eval_ctx -> typed_avalue -> typed_avalue -> typed_avalue
 end
 
-(** See {!InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
-    {!InterpreterLoopsCore.CheckEquivMatcher}.
+(** See {!module:InterpreterLoopsMatchCtxs.MakeCheckEquivMatcher} and
+    {!module-type:InterpreterLoopsCore.CheckEquivMatcher}.
 
     Very annoying: functors only take modules as inputs...
  *)
@@ -252,78 +241,75 @@ module type MatchCheckEquivState = sig
       a source context with a target context. *)
   val check_equiv : bool
 
-  val ctx : C.eval_ctx
-  val rid_map : T.RegionId.InjSubst.t ref
+  val ctx : eval_ctx
+  val rid_map : RegionId.InjSubst.t ref
 
   (** Substitution for the loan and borrow ids - used only if [check_equiv] is true *)
-  val blid_map : V.BorrowId.InjSubst.t ref
+  val blid_map : BorrowId.InjSubst.t ref
 
   (** Substitution for the borrow ids - used only if [check_equiv] is false *)
-  val borrow_id_map : V.BorrowId.InjSubst.t ref
+  val borrow_id_map : BorrowId.InjSubst.t ref
 
   (** Substitution for the loans ids - used only if [check_equiv] is false *)
-  val loan_id_map : V.BorrowId.InjSubst.t ref
+  val loan_id_map : BorrowId.InjSubst.t ref
 
-  val sid_map : V.SymbolicValueId.InjSubst.t ref
-  val sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t ref
-  val aid_map : V.AbstractionId.InjSubst.t ref
-  val lookup_shared_value_in_ctx0 : V.BorrowId.id -> V.typed_value
-  val lookup_shared_value_in_ctx1 : V.BorrowId.id -> V.typed_value
+  val sid_map : SymbolicValueId.InjSubst.t ref
+  val sid_to_value_map : typed_value SymbolicValueId.Map.t ref
+  val aid_map : AbstractionId.InjSubst.t ref
+  val lookup_shared_value_in_ctx0 : BorrowId.id -> typed_value
+  val lookup_shared_value_in_ctx1 : BorrowId.id -> typed_value
 end
 
 module type CheckEquivMatcher = sig
   include PrimMatcher
 
-  val match_aid : V.abstraction_id -> V.abstraction_id -> V.abstraction_id
+  val match_aid : abstraction_id -> abstraction_id -> abstraction_id
 
   val match_aidl :
-    V.abstraction_id list -> V.abstraction_id list -> V.abstraction_id list
+    abstraction_id list -> abstraction_id list -> abstraction_id list
 
   val match_aids :
-    V.abstraction_id_set -> V.abstraction_id_set -> V.abstraction_id_set
-
-  val match_rid : V.region_id -> V.region_id -> V.region_id
-  val match_rids : V.region_id_set -> V.region_id_set -> V.region_id_set
-  val match_borrow_id : V.borrow_id -> V.borrow_id -> V.borrow_id
-
-  val match_borrow_idl :
-    V.borrow_id list -> V.borrow_id list -> V.borrow_id list
-
-  val match_borrow_ids : V.borrow_id_set -> V.borrow_id_set -> V.borrow_id_set
-  val match_loan_id : V.loan_id -> V.loan_id -> V.loan_id
-  val match_loan_idl : V.loan_id list -> V.loan_id list -> V.loan_id list
-  val match_loan_ids : V.loan_id_set -> V.loan_id_set -> V.loan_id_set
+    abstraction_id_set -> abstraction_id_set -> abstraction_id_set
+
+  val match_rid : region_id -> region_id -> region_id
+  val match_rids : region_id_set -> region_id_set -> region_id_set
+  val match_borrow_id : borrow_id -> borrow_id -> borrow_id
+  val match_borrow_idl : borrow_id list -> borrow_id list -> borrow_id list
+  val match_borrow_ids : borrow_id_set -> borrow_id_set -> borrow_id_set
+  val match_loan_id : loan_id -> loan_id -> loan_id
+  val match_loan_idl : loan_id list -> loan_id list -> loan_id list
+  val match_loan_ids : loan_id_set -> loan_id_set -> loan_id_set
 end
 
 (** See {!InterpreterLoopsMatchCtxs.match_ctxs} *)
 type ids_maps = {
-  aid_map : V.AbstractionId.InjSubst.t;
-  blid_map : V.BorrowId.InjSubst.t;
+  aid_map : AbstractionId.InjSubst.t;
+  blid_map : BorrowId.InjSubst.t;
       (** Substitution for the loan and borrow ids *)
-  borrow_id_map : V.BorrowId.InjSubst.t;  (** Substitution for the borrow ids *)
-  loan_id_map : V.BorrowId.InjSubst.t;  (** Substitution for the loan ids *)
-  rid_map : T.RegionId.InjSubst.t;
-  sid_map : V.SymbolicValueId.InjSubst.t;
-  sid_to_value_map : V.typed_value V.SymbolicValueId.Map.t;
+  borrow_id_map : BorrowId.InjSubst.t;  (** Substitution for the borrow ids *)
+  loan_id_map : BorrowId.InjSubst.t;  (** Substitution for the loan ids *)
+  rid_map : RegionId.InjSubst.t;
+  sid_map : SymbolicValueId.InjSubst.t;
+  sid_to_value_map : typed_value SymbolicValueId.Map.t;
 }
 [@@deriving show]
 
 type borrow_loan_corresp = {
-  borrow_to_loan_id_map : V.BorrowId.InjSubst.t;
-  loan_to_borrow_id_map : V.BorrowId.InjSubst.t;
+  borrow_to_loan_id_map : BorrowId.InjSubst.t;
+  loan_to_borrow_id_map : BorrowId.InjSubst.t;
 }
 [@@deriving show]
 
 (* Very annoying: functors only take modules as inputs... *)
 module type MatchJoinState = sig
   (** The current context *)
-  val ctx : C.eval_ctx
+  val ctx : eval_ctx
 
   (** The current loop *)
-  val loop_id : V.LoopId.id
+  val loop_id : LoopId.id
 
   (** The abstractions introduced when performing the matches *)
-  val nabs : V.abs list ref
+  val nabs : abs list ref
 end
 
 (** Split an environment between the fixed abstractions, values, etc. and
@@ -331,36 +317,36 @@ end
 
     Returns: (fixed, new abs, new dummies)
  *)
-let ctx_split_fixed_new (fixed_ids : ids_sets) (ctx : C.eval_ctx) :
-    C.env * V.abs list * V.typed_value list =
-  let is_fresh_did (id : C.DummyVarId.id) : bool =
-    not (C.DummyVarId.Set.mem id fixed_ids.dids)
+let ctx_split_fixed_new (fixed_ids : ids_sets) (ctx : eval_ctx) :
+    env * abs list * typed_value list =
+  let is_fresh_did (id : DummyVarId.id) : bool =
+    not (DummyVarId.Set.mem id fixed_ids.dids)
   in
-  let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
-    not (V.AbstractionId.Set.mem id fixed_ids.aids)
+  let is_fresh_abs_id (id : AbstractionId.id) : bool =
+    not (AbstractionId.Set.mem id fixed_ids.aids)
   in
   (* Filter the new abstractions and dummy variables (there shouldn't be any new dummy variable
      though) in the target context *)
-  let is_fresh (ee : C.env_elem) : bool =
+  let is_fresh (ee : env_elem) : bool =
     match ee with
-    | C.Var (VarBinder _, _) | C.Frame -> false
-    | C.Var (DummyBinder bv, _) -> is_fresh_did bv
-    | C.Abs abs -> is_fresh_abs_id abs.abs_id
+    | EBinding (BVar _, _) | EFrame -> false
+    | EBinding (BDummy bv, _) -> is_fresh_did bv
+    | EAbs abs -> is_fresh_abs_id abs.abs_id
   in
   let new_eel, filt_env = List.partition is_fresh ctx.env in
-  let is_abs ee = match ee with C.Abs _ -> true | _ -> false in
+  let is_abs ee = match ee with EAbs _ -> true | _ -> false in
   let new_absl, new_dummyl = List.partition is_abs new_eel in
   let new_absl =
     List.map
       (fun ee ->
-        match ee with C.Abs abs -> abs | _ -> raise (Failure "Unreachable"))
+        match ee with EAbs abs -> abs | _ -> raise (Failure "Unreachable"))
       new_absl
   in
   let new_dummyl =
     List.map
       (fun ee ->
         match ee with
-        | C.Var (DummyBinder _, v) -> v
+        | EBinding (BDummy _, v) -> v
         | _ -> raise (Failure "Unreachable"))
       new_dummyl
   in
@@ -370,7 +356,7 @@ let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets =
   let { aids; blids = _; borrow_ids = _; loan_ids = _; dids; rids; sids } =
     ids
   in
-  let empty = V.BorrowId.Set.empty in
+  let empty = BorrowId.Set.empty in
   let ids =
     {
       aids;