summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml31
-rw-r--r--compiler/ExtractTypes.ml15
-rw-r--r--compiler/InterpreterLoops.ml12
-rw-r--r--compiler/InterpreterLoops.mli3
-rw-r--r--compiler/InterpreterStatements.ml2
-rw-r--r--compiler/PrintPure.ml4
-rw-r--r--compiler/Pure.ml13
-rw-r--r--compiler/PureMicroPasses.ml9
-rw-r--r--compiler/PureUtils.ml6
-rw-r--r--compiler/SymbolicAst.ml13
-rw-r--r--compiler/SymbolicToPure.ml21
-rw-r--r--compiler/SynthesizeSymbolic.ml7
12 files changed, 91 insertions, 45 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index fb3364f4..d7b4c152 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1135,8 +1135,9 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
- extract_comment fmt
- [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ];
+ extract_comment_with_span fmt
+ [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
+ def.meta.span;
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
* one line *)
@@ -1197,8 +1198,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
- extract_comment fmt
- [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ];
+ extract_comment_with_span fmt
+ [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]
+ def.meta.span;
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
* one line *)
@@ -1251,8 +1253,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
let def_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
(* syntax <def_name> term ... term : tactic *)
F.pp_print_break fmt 0 0;
- extract_comment fmt
- [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ];
+ extract_comment_with_span fmt
+ [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]
+ def.meta.span;
F.pp_print_space fmt ();
F.pp_open_hvbox fmt 0;
F.pp_print_string fmt "syntax \"";
@@ -1313,7 +1316,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
| [ s ] -> [ comment_pre ^ loop_comment ^ s ]
| s :: sl -> (comment_pre ^ loop_comment ^ s) :: sl
in
- extract_comment fmt comment
+ extract_comment_with_span fmt comment def.meta.span
(** Extract a function declaration.
@@ -1765,7 +1768,9 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break then the name of the corresponding LLBC declaration *)
F.pp_print_break fmt 0 0;
- extract_comment fmt [ "[" ^ name_to_string ctx global.name ^ "]" ];
+ extract_comment_with_span fmt
+ [ "[" ^ name_to_string ctx global.name ^ "]" ]
+ global.meta.span;
F.pp_print_space fmt ();
let decl_name = ctx_get_global global.def_id ctx in
@@ -2190,8 +2195,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
- extract_comment fmt
- [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ];
+ extract_comment_with_span fmt
+ [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
+ decl.meta.span;
F.pp_print_break fmt 0 0;
(* Open two outer boxes for the definition, so that whenever possible it gets printed on
one line and indents are correct.
@@ -2478,8 +2484,9 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
- extract_comment fmt
- [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ];
+ extract_comment_with_span fmt
+ [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
+ impl.meta.span;
F.pp_print_break fmt 0 0;
(* Open two outer boxes for the definition, so that whenever possible it gets printed on
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index a74bd532..4dcefabc 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1813,6 +1813,17 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
F.pp_print_string fmt rd;
F.pp_close_box fmt ()
+let extract_comment_with_span (fmt : F.formatter) (sl : string list)
+ (span : Meta.span) : unit =
+ let file = match span.file with Virtual s | Local s -> s in
+ let span =
+ "Source: '" ^ file ^ "': lines "
+ ^ string_of_int span.beg_loc.line
+ ^ "-"
+ ^ string_of_int span.end_loc.line
+ in
+ extract_comment fmt (sl @ [ span ])
+
let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
let trait_name = ctx_get_trait_decl clause.trait_id ctx in
@@ -2034,7 +2045,9 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
if !backend <> HOL4 || not (decl_is_first_from_group kind) then
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
- extract_comment fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ];
+ extract_comment_with_span fmt
+ [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
+ def.meta.span;
F.pp_print_break fmt 0 0;
(* Open a box for the definition, so that whenever possible it gets printed on
* one line. Note however that in the case of Lean line breaks are important
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index f88fc977..ed2a9587 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -2,6 +2,7 @@ open Types
open Values
open Contexts
open ValuesUtils
+open Meta
module S = SynthesizeSymbolic
open Cps
open InterpreterUtils
@@ -60,8 +61,8 @@ 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 : config) (eval_loop_body : st_cm_fun) :
- st_cm_fun =
+let eval_loop_symbolic (config : config) (meta : meta)
+ (eval_loop_body : st_cm_fun) : st_cm_fun =
fun cf ctx ->
(* Debug *)
log#ldebug
@@ -205,9 +206,10 @@ let eval_loop_symbolic (config : config) (eval_loop_body : st_cm_fun) :
(* Put together *)
S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back end_expr
- loop_expr
+ loop_expr meta
-let eval_loop (config : config) (eval_loop_body : st_cm_fun) : st_cm_fun =
+let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) :
+ st_cm_fun =
fun cf ctx ->
match config.mode with
| ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx
@@ -231,4 +233,4 @@ let eval_loop (config : config) (eval_loop_body : st_cm_fun) : st_cm_fun =
*non-fixed* abstractions.
*)
let cc = prepare_ashared_loans None in
- comp cc (eval_loop_symbolic config eval_loop_body) cf ctx
+ comp cc (eval_loop_symbolic config meta eval_loop_body) cf ctx
diff --git a/compiler/InterpreterLoops.mli b/compiler/InterpreterLoops.mli
index 320e4bcb..03633861 100644
--- a/compiler/InterpreterLoops.mli
+++ b/compiler/InterpreterLoops.mli
@@ -58,6 +58,7 @@
open Contexts
open Cps
+open Meta
(** Evaluate a loop *)
-val eval_loop : config -> st_cm_fun -> st_cm_fun
+val eval_loop : config -> meta -> st_cm_fun -> st_cm_fun
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index e8069e31..9ea5387f 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -739,7 +739,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
(* Compose and apply *)
comp cf_st1 cf_st2 cf ctx
| Loop loop_body ->
- InterpreterLoops.eval_loop config
+ InterpreterLoops.eval_loop config st.meta
(eval_statement config loop_body)
cf ctx
| Switch switch -> eval_switch config switch cf ctx
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 49e74b6c..5d8297d3 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -590,7 +590,7 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string)
"[ " ^ String.concat ", " fields ^ " ]"
| _ -> raise (Failure "Unexpected"))
| Meta (meta, e) -> (
- let meta_s = meta_to_string env meta in
+ let meta_s = emeta_to_string env meta in
let e = texpression_to_string env inside indent indent_incr e in
match meta with
| Assignment _ | SymbolicAssignment _ | Tag _ ->
@@ -724,7 +724,7 @@ and loop_to_string (env : fmt_env) (indent : string) (indent_incr : string)
^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n"
^ indent ^ "}"
-and meta_to_string (env : fmt_env) (meta : meta) : string =
+and emeta_to_string (env : fmt_env) (meta : emeta) : string =
let meta =
match meta with
| Assignment (lp, rv, rp) ->
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ebcaa68d..42f51075 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -48,6 +48,10 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
type loop_id = LoopId.id [@@deriving show, ord]
type region_group_id = T.region_group_id [@@deriving show, ord]
type mutability = Mut | Const [@@deriving show, ord]
+type loc = Meta.loc [@@deriving show, ord]
+type file_name = Meta.file_name [@@deriving show, ord]
+type span = Meta.span [@@deriving show, ord]
+type meta = Meta.meta [@@deriving show, ord]
(** The assumed types for the pure AST.
@@ -389,6 +393,7 @@ type type_decl = {
the name used at extraction time will be derived from the
llbc_name.
*)
+ meta : meta;
generics : generic_params;
kind : type_decl_kind;
preds : predicates;
@@ -717,7 +722,7 @@ type expression =
| Switch of texpression * switch_body
| Loop of loop (** See the comments for {!loop} *)
| StructUpdate of struct_update (** See the comments for {!struct_update} *)
- | Meta of (meta[@opaque]) * texpression (** Meta-information *)
+ | Meta of (emeta[@opaque]) * texpression (** Meta-information *)
and switch_body = If of texpression * texpression | Match of match_branch list
and match_branch = { pat : typed_pattern; branch : texpression }
@@ -736,6 +741,7 @@ and match_branch = { pat : typed_pattern; branch : texpression }
and loop = {
fun_end : texpression;
loop_id : loop_id;
+ meta : meta; [@opaque]
fuel0 : var_id;
fuel : var_id;
input_state : var_id option;
@@ -791,7 +797,7 @@ and texpression = { e : expression; ty : ty }
and mvalue = (texpression[@opaque])
(** Meta-information stored in the AST *)
-and meta =
+and emeta =
| Assignment of mplace * mvalue * mplace option
(** Information about an assignment which occured in LLBC.
We use this to guide the heuristics which derive pretty names.
@@ -993,6 +999,7 @@ type fun_kind = A.fun_kind [@@deriving show]
type fun_decl = {
def_id : FunDeclId.id;
is_local : bool;
+ meta : meta;
kind : fun_kind;
num_loops : int;
(** The number of loops in the parent forward function (basically the number
@@ -1019,6 +1026,7 @@ type trait_decl = {
is_local : bool;
llbc_name : llbc_name;
name : string;
+ meta : meta;
generics : generic_params;
preds : predicates;
parent_clauses : trait_clause list;
@@ -1034,6 +1042,7 @@ type trait_impl = {
is_local : bool;
llbc_name : llbc_name;
name : string;
+ meta : meta;
impl_trait : trait_decl_ref;
generics : generic_params;
preds : predicates;
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 1565f252..8463f56c 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -391,7 +391,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| Switch (scrut, body) -> update_switch_body scrut body ctx
| Loop loop -> update_loop loop ctx
| StructUpdate supd -> update_struct_update supd ctx
- | Meta (meta, e) -> update_meta meta e ctx
+ | Meta (meta, e) -> update_emeta meta e ctx
in
(ctx, { e; ty })
(* *)
@@ -449,6 +449,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let {
fun_end;
loop_id;
+ meta;
fuel0;
fuel;
input_state;
@@ -467,6 +468,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
{
fun_end;
loop_id;
+ meta;
fuel0;
fuel;
input_state;
@@ -490,7 +492,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let supd = { struct_id; init; updates } in
(ctx, StructUpdate supd)
(* *)
- and update_meta (meta : meta) (e : texpression) (ctx : pn_ctx) :
+ and update_emeta (meta : emeta) (e : texpression) (ctx : pn_ctx) :
pn_ctx * expression =
let ctx =
match meta with
@@ -516,7 +518,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| Tag _ -> ctx
in
let ctx, e = update_texpression e ctx in
- let e = mk_meta meta e in
+ let e = mk_emeta meta e in
(ctx, e.e)
in
@@ -1428,6 +1430,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
{
def_id = def.def_id;
is_local = def.is_local;
+ meta = loop.meta;
kind = def.kind;
num_loops;
loop_id = Some loop.loop_id;
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index d410abdc..992ea499 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -453,13 +453,13 @@ let mk_dummy_pattern (ty : ty) : typed_pattern =
let value = PatDummy in
{ value; ty }
-let mk_meta (m : meta) (e : texpression) : texpression =
+let mk_emeta (m : emeta) (e : texpression) : texpression =
let ty = e.ty in
let e = Meta (m, e) in
{ e; ty }
let mk_mplace_texpression (mp : mplace) (e : texpression) : texpression =
- mk_meta (MPlace mp) e
+ mk_emeta (MPlace mp) e
let mk_opt_mplace_texpression (mp : mplace option) (e : texpression) :
texpression =
@@ -649,6 +649,7 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
is_local = _;
name = _;
llbc_name = _;
+ meta = _;
generics = _;
preds = _;
parent_clauses;
@@ -668,6 +669,7 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool =
is_local = _;
name = _;
llbc_name = _;
+ meta = _;
impl_trait = _;
generics = _;
preds = _;
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index c9820ba5..a9f45926 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -51,11 +51,10 @@ type call = {
}
[@@deriving show]
-(** Meta information, not necessary for synthesis but useful to guide it to
- generate a pretty output.
+(** Meta information for expressions, not necessary for synthesis but useful to
+ guide it to generate a pretty output.
*)
-
-type meta =
+type emeta =
| Assignment of Contexts.eval_ctx * mplace * typed_value * mplace option
(** We generated an assignment (destination, assigned value, src) *)
[@@deriving show]
@@ -82,7 +81,8 @@ class ['self] iter_expression_base =
fun _ _ -> ()
method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
- method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
+ method visit_emeta : 'env -> emeta -> unit = fun _ _ -> ()
+ method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> ()
method visit_region_group_id_map
: 'a. ('env -> 'a -> unit) -> 'env -> 'a region_group_id_map -> unit =
@@ -200,7 +200,7 @@ type expression =
The boolean is [is_continue].
*)
- | Meta of meta * expression (** Meta information *)
+ | Meta of emeta * expression (** Meta information *)
and loop = {
loop_id : loop_id;
@@ -215,6 +215,7 @@ and loop = {
end_expr : expression;
(** The end of the function (upon the moment it enters the loop) *)
loop_expr : expression; (** The symbolically executed loop body *)
+ meta : Meta.meta; (** Information about where the origin of the loop body *)
}
and expansion =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 9899a0c6..5dee23db 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -496,7 +496,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
let kind = translate_type_decl_kind def.T.kind in
let preds = translate_predicates def.preds in
let is_local = def.is_local in
- { def_id; is_local; llbc_name; name; generics; kind; preds }
+ let meta = def.meta in
+ { def_id; is_local; llbc_name; name; meta; generics; kind; preds }
let translate_type_id (id : T.type_id) : type_id =
match id with
@@ -1489,11 +1490,11 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) :
(call_info.forward, abs_ancestors)
(** Add meta-information to an expression *)
-let mk_meta_symbolic_assignments (vars : var list) (values : texpression list)
+let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list)
(e : texpression) : texpression =
let var_values = List.combine vars values in
List.fold_right
- (fun (var, arg) e -> mk_meta (SymbolicAssignment (var_get_id var, arg)) e)
+ (fun (var, arg) e -> mk_emeta (SymbolicAssignment (var_get_id var, arg)) e)
var_values e
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
@@ -1509,7 +1510,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
| Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
| IntroSymbolic (ectx, p, sv, v, e) ->
translate_intro_symbolic ectx p sv v e ctx
- | Meta (meta, e) -> translate_meta meta e ctx
+ | Meta (meta, e) -> translate_emeta meta e ctx
| ForwardEnd (ectx, loop_input_values, e, back_e) ->
translate_forward_end ectx loop_input_values e back_e ctx
| Loop loop -> translate_loop loop ctx
@@ -2206,7 +2207,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
var_values
in
let vars, values = List.split var_values in
- mk_meta_symbolic_assignments vars values next_e
+ mk_emeta_symbolic_assignments vars values next_e
else next_e
in
@@ -2637,7 +2638,7 @@ and translate_forward_end (ectx : C.eval_ctx)
We then remove all the meta information from the body *before* calling
{!PureMicroPasses.decompose_loops}.
*)
- mk_meta_symbolic_assignments loop_info.input_vars org_args e
+ mk_emeta_symbolic_assignments loop_info.input_vars org_args e
and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in
@@ -2795,6 +2796,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
{
fun_end;
loop_id;
+ meta = loop.meta;
fuel0 = ctx.fuel0;
fuel = ctx.fuel;
input_state;
@@ -2810,7 +2812,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
let ty = fun_end.ty in
{ e = loop; ty }
-and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
+and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) :
texpression =
let next_e = translate_expression e ctx in
let meta =
@@ -3028,6 +3030,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
{
def_id;
is_local = def.is_local;
+ meta = def.meta;
kind = def.kind;
num_loops;
loop_id;
@@ -3108,6 +3111,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
def_id;
is_local;
name = llbc_name;
+ meta;
generics;
preds;
parent_clauses;
@@ -3145,6 +3149,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
is_local;
llbc_name;
name;
+ meta;
generics;
preds;
parent_clauses;
@@ -3160,6 +3165,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
A.def_id;
is_local;
name = llbc_name;
+ meta;
impl_trait;
generics;
preds;
@@ -3201,6 +3207,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
is_local;
llbc_name;
name;
+ meta;
impl_trait;
generics;
preds;
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 9e14a4d6..efcf001a 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -15,7 +15,7 @@ let mk_opt_place_from_op (op : operand) (ctx : Contexts.eval_ctx) :
mplace option =
match op with Copy p | Move p -> Some (mk_mplace p ctx) | Constant _ -> None
-let mk_meta (m : meta) (e : expression) : expression = Meta (m, e)
+let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e)
let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
(seel : symbolic_expansion option list) (el : expression list option) :
@@ -163,8 +163,8 @@ let synthesize_forward_end (ctx : Contexts.eval_ctx)
let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
(fresh_svalues : SymbolicValueId.Set.t)
(rg_to_given_back_tys : (RegionId.Set.t * ty list) RegionGroupId.Map.t)
- (end_expr : expression option) (loop_expr : expression option) :
- expression option =
+ (end_expr : expression option) (loop_expr : expression option)
+ (meta : Meta.meta) : expression option =
match (end_expr, loop_expr) with
| None, None -> None
| Some end_expr, Some loop_expr ->
@@ -177,5 +177,6 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
rg_to_given_back_tys;
end_expr;
loop_expr;
+ meta;
})
| _ -> raise (Failure "Unreachable")
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 13:03:38 +0000