diff options
author | Son Ho | 2023-11-21 14:43:12 +0100 |
---|---|---|
committer | Son Ho | 2023-11-21 14:43:12 +0100 |
commit | 77ba13b371cccbe8098e432ebd287108d5373666 (patch) | |
tree | 845bd9059f6fe94ce8c9e447104367d3a8e9d3c2 /compiler | |
parent | e94cd72ffa63dbc5fc40c7c1a422c1a70ba4a7e5 (diff) |
Add span information to the generated code
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/Extract.ml | 31 | ||||
-rw-r--r-- | compiler/ExtractTypes.ml | 15 | ||||
-rw-r--r-- | compiler/InterpreterLoops.ml | 12 | ||||
-rw-r--r-- | compiler/InterpreterLoops.mli | 3 | ||||
-rw-r--r-- | compiler/InterpreterStatements.ml | 2 | ||||
-rw-r--r-- | compiler/PrintPure.ml | 4 | ||||
-rw-r--r-- | compiler/Pure.ml | 13 | ||||
-rw-r--r-- | compiler/PureMicroPasses.ml | 9 | ||||
-rw-r--r-- | compiler/PureUtils.ml | 6 | ||||
-rw-r--r-- | compiler/SymbolicAst.ml | 13 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 21 | ||||
-rw-r--r-- | compiler/SynthesizeSymbolic.ml | 7 |
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") |