summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/AssociatedTypes.ml10
-rw-r--r--compiler/Contexts.ml42
-rw-r--r--compiler/Interpreter.ml8
-rw-r--r--compiler/InterpreterBorrows.ml12
-rw-r--r--compiler/InterpreterExpansion.ml2
-rw-r--r--compiler/InterpreterExpressions.ml5
-rw-r--r--compiler/InterpreterLoopsFixedPoint.ml18
-rw-r--r--compiler/InterpreterLoopsJoinCtxs.ml36
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml4
-rw-r--r--compiler/InterpreterStatements.ml12
-rw-r--r--compiler/InterpreterUtils.ml26
-rw-r--r--compiler/Invariants.ml2
-rw-r--r--compiler/Print.ml10
-rw-r--r--compiler/SymbolicToPure.ml78
-rw-r--r--compiler/Translate.ml14
15 files changed, 139 insertions, 140 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index e2f687e8..054c8169 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -493,11 +493,11 @@ let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx)
let mk_norm_ctx (ctx : eval_ctx) : norm_ctx =
{
norm_trait_types = ctx.norm_trait_types;
- type_decls = ctx.type_context.type_decls;
- fun_decls = ctx.fun_context.fun_decls;
- global_decls = ctx.global_context.global_decls;
- trait_decls = ctx.trait_decls_context.trait_decls;
- trait_impls = ctx.trait_impls_context.trait_impls;
+ type_decls = ctx.type_ctx.type_decls;
+ fun_decls = ctx.fun_ctx.fun_decls;
+ global_decls = ctx.global_ctx.global_decls;
+ trait_decls = ctx.trait_decls_ctx.trait_decls;
+ trait_impls = ctx.trait_impls_ctx.trait_impls;
type_vars = ctx.type_vars;
const_generic_vars = ctx.const_generic_vars;
}
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index a30ed0f1..5d646a61 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -180,35 +180,35 @@ type config = {
let mk_config (mode : interpreter_mode) : config = { mode }
-type type_context = {
+type type_ctx = {
type_decls_groups : type_declaration_group TypeDeclId.Map.t;
type_decls : type_decl TypeDeclId.Map.t;
type_infos : TypesAnalysis.type_infos;
}
[@@deriving show]
-type fun_context = {
+type fun_ctx = {
fun_decls : fun_decl FunDeclId.Map.t;
fun_infos : FunsAnalysis.fun_info FunDeclId.Map.t;
regions_hierarchies : region_var_groups FunIdMap.t;
}
[@@deriving show]
-type global_context = { global_decls : global_decl GlobalDeclId.Map.t }
+type global_ctx = { global_decls : global_decl GlobalDeclId.Map.t }
[@@deriving show]
-type trait_decls_context = { trait_decls : trait_decl TraitDeclId.Map.t }
+type trait_decls_ctx = { trait_decls : trait_decl TraitDeclId.Map.t }
[@@deriving show]
-type trait_impls_context = { trait_impls : trait_impl TraitImplId.Map.t }
+type trait_impls_ctx = { trait_impls : trait_impl TraitImplId.Map.t }
[@@deriving show]
type decls_ctx = {
- type_ctx : type_context;
- fun_ctx : fun_context;
- global_ctx : global_context;
- trait_decls_ctx : trait_decls_context;
- trait_impls_ctx : trait_impls_context;
+ type_ctx : type_ctx;
+ fun_ctx : fun_ctx;
+ global_ctx : global_ctx;
+ trait_decls_ctx : trait_decls_ctx;
+ trait_impls_ctx : trait_impls_ctx;
}
[@@deriving show]
@@ -230,11 +230,11 @@ module TraitTypeRefMap = Collections.MakeMap (TraitTypeRefOrd)
(** Evaluation context *)
type eval_ctx = {
- type_context : type_context;
- fun_context : fun_context;
- global_context : global_context;
- trait_decls_context : trait_decls_context;
- trait_impls_context : trait_impls_context;
+ type_ctx : type_ctx;
+ fun_ctx : fun_ctx;
+ global_ctx : global_ctx;
+ trait_decls_ctx : trait_decls_ctx;
+ trait_impls_ctx : trait_impls_ctx;
region_groups : RegionGroupId.id list;
type_vars : type_var list;
const_generic_vars : const_generic_var list;
@@ -290,20 +290,20 @@ let ctx_lookup_var_binder (ctx : eval_ctx) (vid : VarId.id) : var_binder =
fst (env_lookup_var ctx.env vid)
let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
- TypeDeclId.Map.find tid ctx.type_context.type_decls
+ TypeDeclId.Map.find tid ctx.type_ctx.type_decls
let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
- FunDeclId.Map.find fid ctx.fun_context.fun_decls
+ FunDeclId.Map.find fid ctx.fun_ctx.fun_decls
let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) :
global_decl =
- GlobalDeclId.Map.find gid ctx.global_context.global_decls
+ GlobalDeclId.Map.find gid ctx.global_ctx.global_decls
let ctx_lookup_trait_decl (ctx : eval_ctx) (id : TraitDeclId.id) : trait_decl =
- TraitDeclId.Map.find id ctx.trait_decls_context.trait_decls
+ TraitDeclId.Map.find id ctx.trait_decls_ctx.trait_decls
let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl =
- TraitImplId.Map.find id ctx.trait_impls_context.trait_impls
+ TraitImplId.Map.find id ctx.trait_impls_ctx.trait_impls
(** Retrieve a variable's value in the current frame *)
let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
@@ -528,7 +528,7 @@ let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
fst (ctx_subst_abs ctx abs_id abs)
let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
- let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
+ let decl_group = TypeDeclId.Map.find id ctx.type_ctx.type_decls_groups in
match decl_group with RecGroup _ -> true | NonRecGroup _ -> false
(** Visitor to iterate over the values in the *current* frame *)
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 76432faa..22d176c9 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -195,7 +195,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
List.map (fun (g : region_var_group) -> g.id) regions_hierarchy
in
let ctx =
- initialize_eval_context ctx region_groups sg.generics.types
+ initialize_eval_ctx ctx region_groups sg.generics.types
sg.generics.const_generics
in
(* Instantiate the signature. This updates the context because we compute
@@ -277,7 +277,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
* an instantiation of the signature, so that we use fresh
* region ids for the return abstractions. *)
let regions_hierarchy =
- FunIdMap.find (FRegular fdef.def_id) ctx.fun_context.regions_hierarchies
+ FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
in
let _, ret_inst_sg =
symbolic_instantiate_fun_sig ctx fdef.signature regions_hierarchy fdef.kind
@@ -466,7 +466,7 @@ let evaluate_function_symbolic (synthesize : bool) (ctx : decls_ctx)
let ctx, input_svs, inst_sg = initialize_symbolic_context_for_fun ctx fdef in
let regions_hierarchy =
- FunIdMap.find (FRegular fdef.def_id) ctx.fun_context.regions_hierarchies
+ FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies
in
(* Create the continuation to finish the evaluation *)
@@ -615,7 +615,7 @@ module Test = struct
assert (body.arg_count = 0);
(* Create the evaluation context *)
- let ctx = initialize_eval_context decls_ctx [] [] [] in
+ let ctx = initialize_eval_ctx decls_ctx [] [] [] in
(* Insert the (uninitialized) local variables *)
let ctx = ctx_push_uninitialized_vars ctx body.locals in
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index e56919fa..a2eb2545 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -1628,7 +1628,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
push { value; ty }
| AIgnoredMutLoan (opt_bid, child_av) ->
(* We don't support nested borrows for now *)
- assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+ assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
assert (opt_bid = None);
(* Simply explore the child *)
list_avalues false push_fail child_av
@@ -1639,7 +1639,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
{ child = child_av; given_back = _; given_back_meta = _ }
| AIgnoredSharedLoan child_av ->
(* We don't support nested borrows for now *)
- assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+ assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
(* Simply explore the child *)
list_avalues false push_fail child_av)
| ABorrow bc -> (
@@ -1659,14 +1659,14 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
push av
| AIgnoredMutBorrow (opt_bid, child_av) ->
(* We don't support nested borrows for now *)
- assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+ assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
assert (opt_bid = None);
(* Just explore the child *)
list_avalues false push_fail child_av
| AEndedIgnoredMutBorrow
{ child = child_av; given_back = _; given_back_meta = _ } ->
(* We don't support nested borrows for now *)
- assert (not (ty_has_borrows ctx.type_context.type_infos child_av.ty));
+ assert (not (ty_has_borrows ctx.type_ctx.type_infos child_av.ty));
(* Just explore the child *)
list_avalues false push_fail child_av
| AProjSharedBorrow asb ->
@@ -1683,7 +1683,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
| ASymbolic _ ->
(* For now, we fore all symbolic values containing borrows to be eagerly
expanded *)
- assert (not (ty_has_borrows ctx.type_context.type_infos ty))
+ assert (not (ty_has_borrows ctx.type_ctx.type_infos ty))
and list_values (v : typed_value) : typed_avalue list * typed_value =
let ty = v.ty in
match v.value with
@@ -1732,7 +1732,7 @@ let destructure_abs (abs_kind : abs_kind) (can_end : bool)
| VSymbolic _ ->
(* For now, we fore all symbolic values containing borrows to be eagerly
expanded *)
- assert (not (ty_has_borrows ctx.type_context.type_infos ty));
+ assert (not (ty_has_borrows ctx.type_ctx.type_infos ty));
([], v)
in
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index bbf4d9d5..e489ddc3 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -627,7 +627,7 @@ let greedy_expand_symbolics_with_borrows (config : config) : cm_fun =
inherit [_] iter_eval_ctx
method! visit_VSymbolic _ sv =
- if ty_has_borrows ctx.type_context.type_infos sv.sv_ty then
+ if ty_has_borrows ctx.type_ctx.type_infos sv.sv_ty then
raise (FoundSymbolicValue sv)
else ()
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 1b5b79dd..8536b4ab 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -32,8 +32,7 @@ let expand_primitively_copyable_at_place (config : config)
fun cf ctx ->
let v = read_place access p ctx in
match
- find_first_primitively_copyable_sv_with_borrows
- ctx.type_context.type_infos v
+ find_first_primitively_copyable_sv_with_borrows ctx.type_ctx.type_infos v
with
| None -> cf ctx
| Some sv ->
@@ -351,7 +350,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
assert (
Option.is_none
(find_first_primitively_copyable_sv_with_borrows
- ctx.type_context.type_infos v));
+ ctx.type_ctx.type_infos v));
(* Actually perform the copy *)
let allow_adt_copy = false in
let ctx, v = copy_value allow_adt_copy config ctx v in
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index c4e180fa..4dabe974 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -300,7 +300,7 @@ let prepare_ashared_loans (loop_id : LoopId.id option) : cm_fun =
let env = List.append fresh_absl env in
let ctx = { ctx with env } in
- let _, new_ctx_ids_map = compute_context_ids ctx in
+ let _, new_ctx_ids_map = compute_ctx_ids ctx in
(* Synthesize *)
match cf ctx with
@@ -385,8 +385,8 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
match !fixed_ids with
| Some _ -> ctx1
| None ->
- let old_ids, _ = compute_context_ids ctx1 in
- let new_ids, _ = compute_contexts_ids !ctxs in
+ let old_ids, _ = compute_ctx_ids ctx1 in
+ let new_ids, _ = compute_ctxs_ids !ctxs in
let blids = BorrowId.Set.diff old_ids.blids new_ids.blids in
let aids = AbstractionId.Set.diff old_ids.aids new_ids.aids in
(* End those borrows and abstractions *)
@@ -409,7 +409,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
ctxs := List.map (end_borrows_abs blids aids) !ctxs;
(* Note that the fixed ids are given by the original context, from *before*
we introduce fresh abstractions/reborrows for the shared values *)
- fixed_ids := Some (fst (compute_context_ids ctx0));
+ fixed_ids := Some (fst (compute_ctx_ids ctx0));
ctx1
in
@@ -424,12 +424,12 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
intersection of ids between the original environment and the list
of new environments *)
let compute_fixed_ids (ctxl : eval_ctx list) : ids_sets =
- let fixed_ids, _ = compute_context_ids ctx0 in
+ let fixed_ids, _ = compute_ctx_ids ctx0 in
let { aids; blids; borrow_ids; loan_ids; dids; rids; sids } = fixed_ids in
let sids = ref sids in
List.iter
(fun ctx ->
- let fixed_ids, _ = compute_context_ids ctx in
+ let fixed_ids, _ = compute_ctx_ids ctx in
sids := SymbolicValueId.Set.inter !sids fixed_ids.sids)
ctxl;
let sids = !sids in
@@ -568,7 +568,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id)
InterpreterBorrows.end_abstraction_no_synth config abs_id ctx
in
(* Explore the context, and check which abstractions are not there anymore *)
- let ids, _ = compute_context_ids ctx in
+ let ids, _ = compute_ctx_ids ctx in
let ended_ids = AbstractionId.Set.diff !fp_aids ids.aids in
add_ended_aids rg_id ended_ids)
ctx.region_groups
@@ -840,8 +840,8 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
let compute_fp_ctx_symbolic_values (ctx : eval_ctx) (fp_ctx : eval_ctx) :
SymbolicValueId.Set.t * symbolic_value list =
- let old_ids, _ = compute_context_ids ctx in
- let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in
+ let old_ids, _ = compute_ctx_ids ctx in
+ let fp_ids, fp_ids_maps = compute_ctx_ids fp_ctx in
let fresh_sids = SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in
(* Compute the set of symbolic values which appear in shared values inside
diff --git a/compiler/InterpreterLoopsJoinCtxs.ml b/compiler/InterpreterLoopsJoinCtxs.ml
index 8d485483..445e5abf 100644
--- a/compiler/InterpreterLoopsJoinCtxs.ml
+++ b/compiler/InterpreterLoopsJoinCtxs.ml
@@ -326,8 +326,8 @@ let mk_collapse_ctx_merge_duplicate_funs (loop_id : LoopId.id) (ctx : eval_ctx)
let _ =
let _, ty0, _ = ty_as_ref ty0 in
let _, ty1, _ = ty_as_ref ty1 in
- assert (not (ty_has_borrows ctx.type_context.type_infos ty0));
- assert (not (ty_has_borrows ctx.type_context.type_infos ty1))
+ assert (not (ty_has_borrows ctx.type_ctx.type_infos ty0));
+ assert (not (ty_has_borrows ctx.type_ctx.type_infos ty1))
in
(* Same remarks as for [merge_amut_borrows] *)
@@ -543,11 +543,11 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
(* Construct the joined context - of course, the type, fun, etc. contexts
* should be the same in the two contexts *)
let {
- type_context;
- fun_context;
- global_context;
- trait_decls_context;
- trait_impls_context;
+ type_ctx;
+ fun_ctx;
+ global_ctx;
+ trait_decls_ctx;
+ trait_impls_ctx;
region_groups;
type_vars;
const_generic_vars;
@@ -559,11 +559,11 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
ctx0
in
let {
- type_context = _;
- fun_context = _;
- global_context = _;
- trait_decls_context = _;
- trait_impls_context = _;
+ type_ctx = _;
+ fun_ctx = _;
+ global_ctx = _;
+ trait_decls_ctx = _;
+ trait_impls_ctx = _;
region_groups = _;
type_vars = _;
const_generic_vars = _;
@@ -577,11 +577,11 @@ let join_ctxs (loop_id : LoopId.id) (fixed_ids : ids_sets) (ctx0 : eval_ctx)
let ended_regions = RegionId.Set.union ended_regions0 ended_regions1 in
Ok
{
- type_context;
- fun_context;
- global_context;
- trait_decls_context;
- trait_impls_context;
+ type_ctx;
+ fun_ctx;
+ global_ctx;
+ trait_decls_ctx;
+ trait_impls_ctx;
region_groups;
type_vars;
const_generic_vars;
@@ -621,7 +621,7 @@ let destructure_new_abs (loop_id : LoopId.id)
contexts we join don't have non-fixed abstractions with the same ids.
*)
let refresh_abs (old_abs : AbstractionId.Set.t) (ctx : eval_ctx) : eval_ctx =
- let ids, _ = compute_context_ids ctx in
+ let ids, _ = compute_ctx_ids ctx in
let abs_to_refresh = AbstractionId.Set.diff ids.aids old_abs in
let aids_subst =
List.map
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 90559c29..2a688fa7 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -658,7 +658,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
else (
(* The caller should have checked that the symbolic values don't contain
borrows *)
- assert (not (ty_has_borrows S.ctx.type_context.type_infos sv0.sv_ty));
+ assert (not (ty_has_borrows S.ctx.type_ctx.type_infos sv0.sv_ty));
(* We simply introduce a fresh symbolic value *)
mk_fresh_symbolic_value sv0.sv_ty)
@@ -669,7 +669,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
- there are no borrows in the "regular" value
If there are loans in the regular value, raise an exception.
*)
- assert (not (ty_has_borrows S.ctx.type_context.type_infos sv.sv_ty));
+ assert (not (ty_has_borrows S.ctx.type_ctx.type_infos sv.sv_ty));
assert (not (value_has_borrows S.ctx v.value));
let value_is_left = not left in
(match InterpreterBorrowsCore.get_first_loan_in_value v with
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 30b7b333..da617c64 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -747,7 +747,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
let tr_self = UnknownTrait __FUNCTION__ in
let regions_hierarchy =
LlbcAstUtils.FunIdMap.find (FRegular fid)
- ctx.fun_context.regions_hierarchies
+ ctx.fun_ctx.regions_hierarchies
in
let inst_sg =
instantiate_fun_sig ctx func.generics tr_self def.signature
@@ -793,7 +793,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
let fid : fun_id = FRegular id in
let regions_hierarchy =
LlbcAstUtils.FunIdMap.find fid
- ctx.fun_context.regions_hierarchies
+ ctx.fun_ctx.regions_hierarchies
in
let inst_sg =
instantiate_fun_sig ctx generics tr_self
@@ -853,7 +853,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
method_def.signature.parent_params_info));
let regions_hierarchy =
LlbcAstUtils.FunIdMap.find (FRegular method_id)
- ctx.fun_context.regions_hierarchies
+ ctx.fun_ctx.regions_hierarchies
in
let tr_self = TraitRef trait_ref in
let inst_sg =
@@ -884,7 +884,7 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx)
(* Instantiate *)
let regions_hierarchy =
LlbcAstUtils.FunIdMap.find (FRegular method_id)
- ctx.fun_context.regions_hierarchies
+ ctx.fun_ctx.regions_hierarchies
in
let tr_self = TraitRef trait_ref in
let inst_sg =
@@ -1450,7 +1450,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id)
* this is a current limitation of our synthesis *)
assert (
List.for_all
- (fun ty -> not (ty_has_borrows ctx.type_context.type_infos ty))
+ (fun ty -> not (ty_has_borrows ctx.type_ctx.type_infos ty))
generics.types);
(* There are two cases (and this is extremely annoying):
@@ -1476,7 +1476,7 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id)
| _ ->
let regions_hierarchy =
LlbcAstUtils.FunIdMap.find (FAssumed fid)
- ctx.fun_context.regions_hierarchies
+ ctx.fun_ctx.regions_hierarchies
in
(* There shouldn't be any reference to Self *)
let tr_self = UnknownTrait __FUNCTION__ in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index e04a6b90..a1a06ee5 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -265,7 +265,7 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx)
inherit [_] iter_typed_value
method! visit_symbolic_value _ s =
- if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
+ if ty_has_borrow_under_mut ctx.type_ctx.type_infos s.sv_ty then
raise Found
else ()
end
@@ -288,15 +288,15 @@ let rvalue_get_place (rv : rvalue) : place option =
(** See {!ValuesUtils.symbolic_value_has_borrows} *)
let symbolic_value_has_borrows (ctx : eval_ctx) (sv : symbolic_value) : bool =
- ValuesUtils.symbolic_value_has_borrows ctx.type_context.type_infos sv
+ ValuesUtils.symbolic_value_has_borrows ctx.type_ctx.type_infos sv
(** See {!ValuesUtils.value_has_borrows}. *)
let value_has_borrows (ctx : eval_ctx) (v : value) : bool =
- ValuesUtils.value_has_borrows ctx.type_context.type_infos v
+ ValuesUtils.value_has_borrows ctx.type_ctx.type_infos v
(** See {!ValuesUtils.value_has_loans_or_borrows}. *)
let value_has_loans_or_borrows (ctx : eval_ctx) (v : value) : bool =
- ValuesUtils.value_has_loans_or_borrows ctx.type_context.type_infos v
+ ValuesUtils.value_has_loans_or_borrows ctx.type_ctx.type_infos v
(** See {!ValuesUtils.value_has_loans}. *)
let value_has_loans (v : value) : bool = ValuesUtils.value_has_loans v
@@ -401,19 +401,19 @@ let compute_env_elem_ids (x : env_elem) : ids_sets * ids_to_values =
compute_env_ids [ x ]
(** Compute the sets of ids found in a list of contexts. *)
-let compute_contexts_ids (ctxl : eval_ctx list) : ids_sets * ids_to_values =
+let compute_ctxs_ids (ctxl : eval_ctx list) : ids_sets * ids_to_values =
let compute, get_ids, get_ids_to_values = compute_ids () in
List.iter (compute#visit_eval_ctx ()) ctxl;
(get_ids (), get_ids_to_values ())
(** Compute the sets of ids found in a context. *)
-let compute_context_ids (ctx : eval_ctx) : ids_sets * ids_to_values =
- compute_contexts_ids [ ctx ]
+let compute_ctx_ids (ctx : eval_ctx) : ids_sets * ids_to_values =
+ compute_ctxs_ids [ ctx ]
(** **WARNING**: this function doesn't compute the normalized types
(for the trait type aliases). This should be computed afterwards.
*)
-let initialize_eval_context (ctx : decls_ctx)
+let initialize_eval_ctx (ctx : decls_ctx)
(region_groups : RegionGroupId.id list) (type_vars : type_var list)
(const_generic_vars : const_generic_var list) : eval_ctx =
reset_global_counters ();
@@ -427,11 +427,11 @@ let initialize_eval_context (ctx : decls_ctx)
const_generic_vars)
in
{
- type_context = ctx.type_ctx;
- fun_context = ctx.fun_ctx;
- global_context = ctx.global_ctx;
- trait_decls_context = ctx.trait_decls_ctx;
- trait_impls_context = ctx.trait_impls_ctx;
+ type_ctx = ctx.type_ctx;
+ fun_ctx = ctx.fun_ctx;
+ global_ctx = ctx.global_ctx;
+ trait_decls_ctx = ctx.trait_decls_ctx;
+ trait_impls_ctx = ctx.trait_impls_ctx;
region_groups;
type_vars;
const_generic_vars;
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index fa0d7436..b87cdff7 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -768,7 +768,7 @@ let check_symbolic_values (ctx : eval_ctx) : unit =
assert (info.env_count = 0 || info.aproj_borrows = []);
(* A symbolic value containing borrows can't be duplicated (i.e., copied):
* it must be expanded first *)
- if ty_has_borrows ctx.type_context.type_infos info.ty then
+ if ty_has_borrows ctx.type_ctx.type_infos info.ty then
assert (info.env_count <= 1);
(* A duplicated symbolic value is necessarily primitively copyable *)
assert (info.env_count <= 1 || ty_is_primitively_copyable info.ty);
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 0e2ec1fc..8999c77d 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -409,11 +409,11 @@ module Contexts = struct
}
let eval_ctx_to_fmt_env (ctx : eval_ctx) : fmt_env =
- let type_decls = ctx.type_context.type_decls in
- let fun_decls = ctx.fun_context.fun_decls in
- let global_decls = ctx.global_context.global_decls in
- let trait_decls = ctx.trait_decls_context.trait_decls in
- let trait_impls = ctx.trait_impls_context.trait_impls in
+ let type_decls = ctx.type_ctx.type_decls in
+ let fun_decls = ctx.fun_ctx.fun_decls in
+ let global_decls = ctx.global_ctx.global_decls in
+ let trait_decls = ctx.trait_decls_ctx.trait_decls in
+ let trait_impls = ctx.trait_impls_ctx.trait_impls in
(* Below: it is always safe to omit fields - if an id can't be found at
printing time, we print the id (in raw form) instead of the name it
designates. *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 204fc399..d8213317 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -15,7 +15,7 @@ module PP = PrintPure
(** The local logger *)
let log = Logging.symbolic_to_pure_log
-type type_context = {
+type type_ctx = {
llbc_type_decls : T.type_decl TypeDeclId.Map.t;
type_decls : type_decl TypeDeclId.Map.t;
(** We use this for type-checking (for sanity checks) when translating
@@ -43,18 +43,18 @@ type fun_sig_named_outputs = {
}
[@@deriving show]
-type fun_context = {
+type fun_ctx = {
llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
fun_infos : fun_info A.FunDeclId.Map.t;
regions_hierarchies : T.region_var_groups FunIdMap.t;
}
[@@deriving show]
-type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t }
+type global_ctx = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t }
[@@deriving show]
-type trait_decls_context = A.trait_decl A.TraitDeclId.Map.t [@@deriving show]
-type trait_impls_context = A.trait_impl A.TraitImplId.Map.t [@@deriving show]
+type trait_decls_ctx = A.trait_decl A.TraitDeclId.Map.t [@@deriving show]
+type trait_impls_ctx = A.trait_impl A.TraitImplId.Map.t [@@deriving show]
(** Whenever we translate a function call or an ended abstraction, we
store the related information (this is useful when translating ended
@@ -120,11 +120,11 @@ type loop_info = {
(** Body synthesis context *)
type bs_ctx = {
- type_context : type_context; (* TODO: rename *)
- fun_context : fun_context; (* TODO: rename *)
- global_context : global_context; (* TODO: rename *)
- trait_decls_ctx : trait_decls_context;
- trait_impls_ctx : trait_impls_context;
+ type_ctx : type_ctx;
+ fun_ctx : fun_ctx;
+ global_ctx : global_ctx;
+ trait_decls_ctx : trait_decls_ctx;
+ trait_impls_ctx : trait_impls_ctx;
fun_decl : A.fun_decl;
bid : RegionGroupId.id option;
(** TODO: rename
@@ -234,9 +234,9 @@ type bs_ctx = {
(* TODO: move *)
let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
- let type_decls = ctx.type_context.llbc_type_decls in
- let fun_decls = ctx.fun_context.llbc_fun_decls in
- let global_decls = ctx.global_context.llbc_global_decls in
+ let type_decls = ctx.type_ctx.llbc_type_decls in
+ let fun_decls = ctx.fun_ctx.llbc_fun_decls in
+ let global_decls = ctx.global_ctx.llbc_global_decls in
let trait_decls = ctx.trait_decls_ctx in
let trait_impls = ctx.trait_impls_ctx in
let { regions; types; const_generics; trait_clauses } : T.generic_params =
@@ -258,9 +258,9 @@ let bs_ctx_to_fmt_env (ctx : bs_ctx) : Print.fmt_env =
}
let bs_ctx_to_pure_fmt_env (ctx : bs_ctx) : PrintPure.fmt_env =
- let type_decls = ctx.type_context.llbc_type_decls in
- let fun_decls = ctx.fun_context.llbc_fun_decls in
- let global_decls = ctx.global_context.llbc_global_decls in
+ let type_decls = ctx.type_ctx.llbc_type_decls in
+ let fun_decls = ctx.fun_ctx.llbc_fun_decls in
+ let global_decls = ctx.global_ctx.llbc_global_decls in
let trait_decls = ctx.trait_decls_ctx in
let trait_impls = ctx.trait_impls_ctx in
let generics = ctx.sg.generics in
@@ -346,11 +346,11 @@ let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
T.type_decl =
- TypeDeclId.Map.find id ctx.type_context.llbc_type_decls
+ TypeDeclId.Map.find id ctx.type_ctx.llbc_type_decls
let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) :
A.fun_decl =
- A.FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls
+ A.FunDeclId.Map.find id ctx.fun_ctx.llbc_fun_decls
(* Some generic translation functions (we need to translate different "flavours"
of types: forward types, backward types, etc.) *)
@@ -617,13 +617,13 @@ and translate_fwd_trait_instance_id (type_infos : type_infos)
(** Simply calls [translate_fwd_ty] *)
let ctx_translate_fwd_ty (ctx : bs_ctx) (ty : T.ty) : ty =
- let type_infos = ctx.type_context.type_infos in
+ let type_infos = ctx.type_ctx.type_infos in
translate_fwd_ty type_infos ty
(** Simply calls [translate_fwd_generic_args] *)
let ctx_translate_fwd_generic_args (ctx : bs_ctx) (generics : T.generic_args) :
generic_args =
- let type_infos = ctx.type_context.type_infos in
+ let type_infos = ctx.type_ctx.type_infos in
translate_fwd_generic_args type_infos generics
(** Translate a type, when some regions may have ended.
@@ -708,7 +708,7 @@ let rec translate_back_ty (type_infos : type_infos)
(** Simply calls [translate_back_ty] *)
let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
(inside_mut : bool) (ty : T.ty) : ty option =
- let type_infos = ctx.type_context.type_infos in
+ let type_infos = ctx.type_ctx.type_infos in
translate_back_ty type_infos keep_region inside_mut ty
let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
@@ -721,8 +721,8 @@ let mk_type_check_ctx (ctx : bs_ctx) : PureTypeCheck.tc_ctx =
in
let env = VarId.Map.empty in
{
- PureTypeCheck.type_decls = ctx.type_context.type_decls;
- global_decls = ctx.global_context.llbc_global_decls;
+ PureTypeCheck.type_decls = ctx.type_ctx.type_decls;
+ global_decls = ctx.global_ctx.llbc_global_decls;
env;
const_generics;
}
@@ -742,7 +742,7 @@ let translate_fun_id_or_trait_method_ref (ctx : bs_ctx)
match id with
| FunId fun_id -> FunId fun_id
| TraitMethod (trait_ref, method_name, fun_decl_id) ->
- let type_infos = ctx.type_context.type_infos in
+ let type_infos = ctx.type_ctx.type_infos in
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
TraitMethod (trait_ref, method_name, fun_decl_id)
@@ -894,7 +894,7 @@ let translate_fun_sig_to_decomposed (decls_ctx : C.decls_ctx)
List.map (fun (g : T.region_var_group) -> g.id) regions_hierarchy
in
let ctx =
- InterpreterUtils.initialize_eval_context decls_ctx region_groups
+ InterpreterUtils.initialize_eval_ctx decls_ctx region_groups
sg.generics.types sg.generics.const_generics
in
(* Compute the normalization map for the *sty* types and add it to the context *)
@@ -1786,7 +1786,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
(* Retrieve the effect information about this function (can fail,
* takes a state as input, etc.) *)
let effect_info =
- get_fun_effect_info ctx.fun_context.fun_infos fid None None
+ get_fun_effect_info ctx.fun_ctx.fun_infos fid None None
in
(* Depending on the function effects:
* - add the fuel
@@ -2006,7 +2006,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
raise (Failure "Unreachable")
in
let effect_info =
- get_fun_effect_info ctx.fun_context.fun_infos fun_id None (Some rg_id)
+ get_fun_effect_info ctx.fun_ctx.fun_infos fun_id None (Some rg_id)
in
let generics = ctx_translate_fwd_generic_args ctx call.generics in
(* Retrieve the original call and the parent abstractions *)
@@ -2194,8 +2194,8 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
| V.LoopCall ->
let fun_id = E.FRegular ctx.fun_decl.def_id in
let effect_info =
- get_fun_effect_info ctx.fun_context.fun_infos (FunId fun_id)
- (Some vloop_id) (Some rg_id)
+ get_fun_effect_info ctx.fun_ctx.fun_infos (FunId fun_id) (Some vloop_id)
+ (Some rg_id)
in
let loop_info = LoopId.Map.find loop_id ctx.loops in
let generics = loop_info.generics in
@@ -2306,7 +2306,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
(e : S.expression) (ctx : bs_ctx) : texpression =
let ctx, var = fresh_var_for_symbolic_value sval ctx in
- let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in
+ let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in
let global_expr = { id = Global gid; generics = empty_generic_args } in
(* We use translate_fwd_ty to translate the global type *)
let ty = ctx_translate_fwd_ty ctx decl.ty in
@@ -2482,7 +2482,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
- if we forbid using field projectors.
*)
let is_rec_def =
- T.TypeDeclId.Set.mem adt_id ctx.type_context.recursive_decls
+ T.TypeDeclId.Set.mem adt_id ctx.type_ctx.recursive_decls
in
let use_let_with_cons =
is_enum
@@ -2495,7 +2495,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
like Coq don't, in which case we have to deconstruct the whole ADT
at once (`let (a, b, c) = x in`) *)
|| TypesUtils.type_decl_from_type_id_is_tuple_struct
- ctx.type_context.type_infos type_id
+ ctx.type_ctx.type_infos type_id
&& not (Config.backend_has_tuple_projectors ())
in
if use_let_with_cons then
@@ -2588,7 +2588,7 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
{ e = StructUpdate su; ty = var.ty }
| VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty }
| VaTraitConstValue (trait_ref, generics, const_name) ->
- let type_infos = ctx.type_context.type_infos in
+ let type_infos = ctx.type_ctx.type_infos in
let trait_ref = translate_fwd_trait_ref type_infos trait_ref in
let generics = translate_fwd_generic_args type_infos generics in
let qualif_id = TraitConst (trait_ref, generics, const_name) in
@@ -2722,7 +2722,7 @@ and translate_forward_end (ectx : C.eval_ctx)
let sg = ctx.fun_decl.signature in
let regions_hierarchy =
LlbcAstUtils.FunIdMap.find (FRegular def_id)
- ctx.fun_context.regions_hierarchies
+ ctx.fun_ctx.regions_hierarchies
in
List.map
(fun (gid, _) ->
@@ -2816,7 +2816,7 @@ and translate_forward_end (ectx : C.eval_ctx)
(* Lookup the effect info for the loop function *)
let fid = E.FRegular ctx.fun_decl.def_id in
let effect_info =
- get_fun_effect_info ctx.fun_context.fun_infos (FunId fid) None ctx.bid
+ get_fun_effect_info ctx.fun_ctx.fun_infos (FunId fid) None ctx.bid
in
(* Introduce a fresh output value for the forward function *)
@@ -2949,7 +2949,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
List.map
(fun ty ->
assert (
- not (TypesUtils.ty_has_borrows !ctx.type_context.type_infos ty));
+ not (TypesUtils.ty_has_borrows !ctx.type_ctx.type_infos ty));
(None, ctx_translate_fwd_ty !ctx ty))
tys
in
@@ -3173,7 +3173,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
(* Translate the signature *)
let signature = translate_fun_sig_from_decomposed ctx.sg ctx.bid in
let regions_hierarchy =
- FunIdMap.find (FRegular def_id) ctx.fun_context.regions_hierarchies
+ FunIdMap.find (FRegular def_id) ctx.fun_ctx.regions_hierarchies
in
(* Translate the body, if there is *)
let body =
@@ -3181,8 +3181,8 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
| None -> None
| Some body ->
let effect_info =
- get_fun_effect_info ctx.fun_context.fun_infos
- (FunId (FRegular def_id)) None bid
+ get_fun_effect_info ctx.fun_ctx.fun_infos (FunId (FRegular def_id))
+ None bid
in
let body = translate_expression body ctx in
(* Add a match over the fuel, if necessary *)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8b221c93..e153f4f4 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -72,7 +72,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
| RecGroup _ -> Some tid)
(TypeDeclId.Map.bindings trans_ctx.type_ctx.type_decls_groups))
in
- let type_context =
+ let type_ctx =
{
SymbolicToPure.type_infos = trans_ctx.type_ctx.type_infos;
llbc_type_decls = trans_ctx.type_ctx.type_decls;
@@ -80,14 +80,14 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
recursive_decls = recursive_type_decls;
}
in
- let fun_context =
+ let fun_ctx =
{
SymbolicToPure.llbc_fun_decls = trans_ctx.fun_ctx.fun_decls;
fun_infos = trans_ctx.fun_ctx.fun_infos;
regions_hierarchies = trans_ctx.fun_ctx.regions_hierarchies;
}
in
- let global_context =
+ let global_ctx =
{ SymbolicToPure.llbc_global_decls = trans_ctx.global_ctx.global_decls }
in
@@ -134,7 +134,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
in
let regions_hierarchy =
- LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_context.regions_hierarchies
+ LlbcAstUtils.FunIdMap.find (FRegular def_id) fun_ctx.regions_hierarchies
in
let var_counter, back_state_vars =
@@ -160,9 +160,9 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
back_state_vars;
fuel0;
fuel;
- type_context;
- fun_context;
- global_context;
+ type_ctx;
+ fun_ctx;
+ global_ctx;
trait_decls_ctx = trans_ctx.trait_decls_ctx.trait_decls;
trait_impls_ctx = trans_ctx.trait_impls_ctx.trait_impls;
fun_decl = fdef;
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 19:33:25 +0000