summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/Extract.ml14
-rw-r--r--compiler/ExtractBase.ml24
-rw-r--r--compiler/ExtractTypes.ml2
-rw-r--r--compiler/InterpreterLoops.ml4
-rw-r--r--compiler/InterpreterLoopsFixedPoint.ml14
-rw-r--r--compiler/InterpreterLoopsFixedPoint.mli2
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml8
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.mli2
-rw-r--r--compiler/PureMicroPasses.ml2
-rw-r--r--compiler/SymbolicToPure.ml14
-rw-r--r--compiler/Translate.ml5
11 files changed, 50 insertions, 41 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 0e86e187..43acba94 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -46,7 +46,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
let f = def.f in
let open ExtractBuiltin in
let fun_id = (Pure.FunId (FRegular f.def_id), f.loop_id) in
- ctx_add (FunId (FromLlbc fun_id)) fun_info.extract_name ctx
+ ctx_add f.meta (FunId (FromLlbc fun_id)) fun_info.extract_name ctx
| None ->
(* Not builtin *)
(* If this is a trait method implementation, we prefix the name with the
@@ -194,7 +194,7 @@ let extract_global (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
(* Extract the global name *)
F.pp_print_string fmt (ctx_get_global meta id ctx);
(* Extract the generics *)
- extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
+ extract_generic_args meta ctx fmt TypeDeclId.Set.empty generics;
if use_brackets then F.pp_print_string fmt ")";
F.pp_close_box fmt ()
@@ -336,7 +336,7 @@ and extract_App (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (i
| AdtCons adt_cons_id ->
extract_adt_cons meta ctx fmt inside adt_cons_id qualif.generics args
| Proj proj ->
- extract_field_projector ctx fmt inside app proj qualif.generics args
+ extract_field_projector meta ctx fmt inside app proj qualif.generics args
| TraitConst (trait_ref, const_name) ->
extract_trait_ref meta ctx fmt TypeDeclId.Set.empty true trait_ref;
let name =
@@ -1735,7 +1735,7 @@ let extract_global_decl_body_gen (meta : Meta.meta) (ctx : extraction_ctx) (fmt
(* Extract the generic parameters *)
let space = ref true in
- extract_generic_params ctx fmt TypeDeclId.Set.empty ~space:(Some space)
+ extract_generic_params meta ctx fmt TypeDeclId.Set.empty ~space:(Some space)
generics type_params cg_params trait_clauses;
if not !space then F.pp_print_space fmt ();
@@ -1838,6 +1838,8 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx) (f
*)
let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(global : global_decl) (body : fun_decl) (interface : bool) : unit =
+
+ let meta = body.meta in
cassert body.is_global_decl_body body.meta "TODO: Error message";
cassert (body.signature.inputs = []) body.meta "TODO: Error message";
@@ -1865,7 +1867,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
in
(* Add the type parameters *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params global.llbc_name global.llbc_generics global.generics
+ ctx_add_generic_params meta global.llbc_name global.llbc_generics global.generics
ctx
in
match body.body with
@@ -2657,7 +2659,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
is a provided constant or not *)
let print_params () =
if provided_id = Some id then
- extract_generic_args ctx fmt TypeDeclId.Set.empty
+ extract_generic_args impl.meta ctx fmt TypeDeclId.Set.empty
impl.impl_trait.decl_generics
else
let all_params =
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 022643f5..aae11f19 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1273,12 +1273,20 @@ let ctx_prepare_name (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name
craise
meta
("Unexpected name shape: "
- ^ TranslateCore.name_to_string ctx.trans_ctx name))
+ ^ TranslateCore.name_to_string ctx.trans_ctx name)
+
+(** Helper *)
+let ctx_compute_simple_name (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name) :
+ string list =
+ (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
+ let name = ctx_prepare_name meta ctx name in
+ name_to_simple_name ctx.trans_ctx name
(** Helper *)
let ctx_compute_simple_type_name = ctx_compute_simple_name
(** Helper *)
+
let ctx_compute_type_name_no_suffix (meta : Meta.meta) (ctx : extraction_ctx) (name : llbc_name) :
string =
flatten_name (ctx_compute_simple_type_name meta ctx name)
@@ -1369,7 +1377,7 @@ let ctx_compute_global_name (meta : Meta.meta) (ctx : extraction_ctx) (name : ll
| Coq | FStar | HOL4 ->
let parts = List.map to_snake_case (ctx_compute_simple_name meta ctx name) in
String.concat "_" parts
- | Lean -> flatten_name (ctx_compute_simple_name ctx name)
+ | Lean -> flatten_name (ctx_compute_simple_name meta ctx name)
(** Helper function: generate a suffix for a function name, i.e., generates
a suffix like "_loop", "loop1", etc. to append to a function name.
@@ -1386,7 +1394,7 @@ let default_fun_loop_suffix (num_loops : int) (loop_id : LoopId.id option) :
(** A helper function: generates a function suffix.
TODO: move all those helpers.
*)
-let default_fun_suffix (meta : Meta.meta) (num_loops : int) (loop_id : LoopId.id option) : string =
+let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) : string =
(* We only generate a suffix for the functions we generate from the loops *)
default_fun_loop_suffix num_loops loop_id
@@ -1404,7 +1412,7 @@ let ctx_compute_fun_name (meta : Meta.meta) (ctx : extraction_ctx) (fname : llbc
(num_loops : int) (loop_id : LoopId.id option) : string =
let fname = ctx_compute_fun_name_no_suffix meta ctx fname in
(* Compute the suffix *)
- let suffix = default_fun_suffix meta num_loops loop_id in
+ let suffix = default_fun_suffix num_loops loop_id in
(* Concatenate *)
fname ^ suffix
@@ -1423,7 +1431,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
let name =
let params = trait_impl.llbc_generics in
let args = trait_impl.llbc_impl_trait.decl_generics in
- let name = ctx_prepare_name ctx trait_decl.llbc_name in
+ let name = ctx_prepare_name trait_impl.meta ctx trait_decl.llbc_name in
trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
in
let name = flatten_name name in
@@ -1879,7 +1887,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
ctx_add def.meta decl name ctx
| None ->
(* Not the case: "standard" registration *)
- let name = ctx_compute_global_name ctx def.name in
+ let name = ctx_compute_global_name def.meta ctx def.name in
let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
(* If this is a provided constant (i.e., the default value for a constant
in a trait declaration) we add a suffix. Otherwise there is a clash
@@ -1888,8 +1896,8 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
let suffix =
match def.kind with TraitItemProvided _ -> "_default" | _ -> ""
in
- let ctx = ctx_add decl (name ^ suffix) ctx in
- let ctx = ctx_add body (name ^ suffix ^ "_body") ctx in
+ let ctx = ctx_add def.meta decl (name ^ suffix) ctx in
+ let ctx = ctx_add def.meta body (name ^ suffix ^ "_body") ctx in
ctx
let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index a8143876..94acd08c 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -548,7 +548,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
*)
match trait_ref.trait_id with
| Self ->
- cassert (trait_ref.generics = empty_generic_args) "TODO: Error message";
+ cassert (trait_ref.generics = empty_generic_args) meta "TODO: Error message";
extract_trait_instance_id_with_dot meta ctx fmt no_params_tys false
trait_ref.trait_id;
F.pp_print_string fmt type_name
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index d2f1b5fb..89015f71 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -102,7 +102,7 @@ let eval_loop_symbolic (config : config) (meta : meta)
- src ctx (fixed-point ctx):\n" ^ eval_ctx_to_string fp_ctx
^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx));
- prepare_match_ctx_with_target config loop_id fixed_ids fp_ctx cf ctx
+ prepare_match_ctx_with_target config meta loop_id fixed_ids fp_ctx cf ctx
in
(* Actually match *)
@@ -264,7 +264,7 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) :
| SymbolicMode ->
(* Simplify the context by ending the unnecessary borrows/loans and getting
rid of the useless symbolic values (which are in anonymous variables) *)
- let cc = cleanup_fresh_values_and_abs config empty_ids_set in
+ let cc = cleanup_fresh_values_and_abs config meta empty_ids_set in
(* We want to make sure the loop will *not* manipulate shared avalues
containing themselves shared loans (i.e., nested shared loans in
diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml
index f6ce9b32..f5bd4a35 100644
--- a/compiler/InterpreterLoopsFixedPoint.ml
+++ b/compiler/InterpreterLoopsFixedPoint.ml
@@ -23,7 +23,7 @@ exception FoundAbsId of AbstractionId.id
- end the borrows which appear in fresh anonymous values and don't contain loans
- end the fresh region abstractions which can be ended (no loans)
*)
-let rec end_useless_fresh_borrows_and_abs (config : config)
+let rec end_useless_fresh_borrows_and_abs (config : config) (meta : Meta.meta)
(fixed_ids : ids_sets) : cm_fun =
fun cf ctx ->
let rec explore_env (env : env) : unit =
@@ -56,7 +56,7 @@ let rec end_useless_fresh_borrows_and_abs (config : config)
| EAbs abs :: env when not (AbstractionId.Set.mem abs.abs_id fixed_ids.aids)
-> (
(* Check if it is possible to end the abstraction: if yes, raise an exception *)
- let opt_loan = get_first_non_ignored_aloan_in_abstraction abs in
+ let opt_loan = get_first_non_ignored_aloan_in_abstraction meta abs in
match opt_loan with
| None ->
(* No remaining loans: we can end the abstraction *)
@@ -66,7 +66,7 @@ let rec end_useless_fresh_borrows_and_abs (config : config)
explore_env env)
| _ :: env -> explore_env env
in
- let rec_call = end_useless_fresh_borrows_and_abs config fixed_ids in
+ let rec_call = end_useless_fresh_borrows_and_abs config meta fixed_ids in
try
(* Explore the environment *)
explore_env ctx.env;
@@ -74,10 +74,10 @@ let rec end_useless_fresh_borrows_and_abs (config : config)
cf ctx
with
| FoundAbsId abs_id ->
- let cc = end_abstraction config abs_id in
+ let cc = end_abstraction config meta abs_id in
comp cc rec_call cf ctx
| FoundBorrowId bid ->
- let cc = end_borrow config bid in
+ let cc = end_borrow config meta bid in
comp cc rec_call cf ctx
(* Explore the fresh anonymous values and replace all the values which are not
@@ -121,11 +121,11 @@ let cleanup_fresh_values (fixed_ids : ids_sets) : cm_fun =
- also end the borrows which appear in fresh anonymous values and don't contain loans
- end the fresh region abstractions which can be ended (no loans)
*)
-let cleanup_fresh_values_and_abs (config : config) (fixed_ids : ids_sets) :
+let cleanup_fresh_values_and_abs (config : config) (meta : Meta.meta) (fixed_ids : ids_sets) :
cm_fun =
fun cf ctx ->
comp
- (end_useless_fresh_borrows_and_abs config fixed_ids)
+ (end_useless_fresh_borrows_and_abs config meta fixed_ids)
(cleanup_fresh_values fixed_ids)
cf ctx
diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli
index 4568bf79..54e4d780 100644
--- a/compiler/InterpreterLoopsFixedPoint.mli
+++ b/compiler/InterpreterLoopsFixedPoint.mli
@@ -13,7 +13,7 @@ open InterpreterLoopsCore
- config
- fixed ids (the fixeds ids are the ids we consider as non-fresh)
*)
-val cleanup_fresh_values_and_abs : config -> ids_sets -> Cps.cm_fun
+val cleanup_fresh_values_and_abs : config -> Meta.meta -> ids_sets -> Cps.cm_fun
(** Prepare the shared loans in the abstractions by moving them to fresh
abstractions.
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index c02d3117..24e588f2 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -459,8 +459,8 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
(* Lookup the shared values and match them - we do this mostly
to make sure we end loans which might appear on one side
and not on the other. *)
- let sv0 = lookup_shared_value ctx0 bid0 in
- let sv1 = lookup_shared_value ctx1 bid1 in
+ let sv0 = lookup_shared_value meta ctx0 bid0 in
+ let sv1 = lookup_shared_value meta ctx1 bid1 in
let sv = match_rec sv0 sv1 in
if bid0 = bid1 then bid0
else
@@ -1544,7 +1544,7 @@ let prepare_match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id
(* Apply the reorganization *)
cf_reorganize_join_tgt cf tgt_ctx
-let match_ctx_with_target (config : config) (loop_id : LoopId.id)
+let match_ctx_with_target (config : config) (meta : Meta.meta) (loop_id : LoopId.id)
(is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp)
(fp_input_svalues : SymbolicValueId.id list) (fixed_ids : ids_sets)
(src_ctx : eval_ctx) : st_cm_fun =
@@ -1562,7 +1562,7 @@ let match_ctx_with_target (config : config) (loop_id : LoopId.id)
were introduced during the loop iterations)
*)
let cf_reorganize_join_tgt =
- prepare_match_ctx_with_target config loop_id fixed_ids src_ctx
+ prepare_match_ctx_with_target config meta loop_id fixed_ids src_ctx
in
(* Introduce the "identity" abstractions for the loop re-entry.
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 4a6d24a9..a8002ad4 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -151,7 +151,7 @@ val ctxs_are_equivalent : Meta.meta -> ids_sets -> eval_ctx -> eval_ctx -> bool
*)
val prepare_match_ctx_with_target :
- config -> LoopId.id -> ids_sets -> eval_ctx -> cm_fun
+ config -> Meta.meta -> LoopId.id -> ids_sets -> eval_ctx -> cm_fun
(** Match a context with a target context.
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 1df7176d..ab4686c9 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1140,7 +1140,7 @@ let simplify_let_then_return _ctx (def : fun_decl) =
(* The first let-binding is monadic *)
match opt_destruct_ret next_e with
| Some e ->
- if match_pattern_and_expr def.meta lv e then rv.e else not_simpl_e
+ if match_pattern_and_expr lv e then rv.e else not_simpl_e
| None -> not_simpl_e
else
(* The first let-binding is not monadic *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index e60d6870..3532b2dd 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1325,7 +1325,7 @@ let compute_output_ty_from_decomposed (dsg : Pure.decomposed_fun_sig) : ty =
in
mk_output_ty_from_effect_info effect_info output
-let translate_fun_sig_from_decomposed (meta : Meta.meta) (dsg : Pure.decomposed_fun_sig) : fun_sig
+let translate_fun_sig_from_decomposed (dsg : Pure.decomposed_fun_sig) : fun_sig
=
let generics = dsg.generics in
let llbc_generics = dsg.llbc_generics in
@@ -2512,7 +2512,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs)
^ "\nfunc type: "
^ pure_ty_to_string ctx func.ty
^ "\n\nargs:\n" ^ String.concat "\n" args));
- let call = mk_apps func args in
+ let call = mk_apps ctx.fun_decl.meta func args in
mk_let effect_info.can_fail output call next_e
and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs)
@@ -2671,7 +2671,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
match func with
| None -> next_e
| Some func ->
- let call = mk_apps func args in
+ let call = mk_apps ctx.fun_decl.meta func args in
(* Add meta-information - this is slightly hacky: we look at the
values consumed by the abstraction (note that those come from
*before* we applied the fixed-point context) and use them to
@@ -3682,7 +3682,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
let llbc_name = def.name in
let name = name_to_string ctx llbc_name in
(* Translate the signature *)
- let signature = translate_fun_sig_from_decomposed def.meta ctx.sg in
+ let signature = translate_fun_sig_from_decomposed ctx.sg in
(* Translate the body, if there is *)
let body =
match body with
@@ -3915,9 +3915,9 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
(Print.Contexts.decls_ctx_to_fmt_env ctx)
llbc_name
in
- let generics = translate_generic_params llbc_generics in
- let preds = translate_predicates preds in
- let ty = translate_fwd_ty ctx.type_ctx.type_infos ty in
+ let generics = translate_generic_params decl.meta llbc_generics in
+ let preds = translate_predicates decl.meta preds in
+ let ty = translate_fwd_ty decl.meta ctx.type_ctx.type_infos ty in
{
meta;
def_id;
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index f97d7ab1..9834fe81 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -447,9 +447,8 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
let global_decls = ctx.trans_ctx.global_ctx.global_decls in
let global = GlobalDeclId.Map.find id global_decls in
let trans = FunDeclId.Map.find global.body ctx.trans_funs in
- sanity_check (trans.fwd.loops = []) global.meta;
- sanity_check (trans.backs = []) global.meta;
- let body = trans.fwd.f in
+ sanity_check (trans.loops = []) global.meta;
+ let body = trans.f in
let is_opaque = Option.is_none body.Pure.body in
(* Check if we extract the global *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 03:45:01 +0000