summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoopsCore.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/InterpreterLoopsCore.ml')
-rw-r--r--compiler/InterpreterLoopsCore.ml266
1 files changed, 126 insertions, 140 deletions
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml
index 6e33c75b..d14230c6 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,13 +32,13 @@ 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}.
@@ -56,14 +47,14 @@ type abs_borrows_loans_maps = {
{!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,15 +221,14 @@ 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
@@ -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;