diff --git a/spectec/src/backend-prose/gen.ml b/spectec/src/backend-prose/gen.ml index 18093508e7..dd275684f6 100644 --- a/spectec/src/backend-prose/gen.ml +++ b/spectec/src/backend-prose/gen.ml @@ -37,7 +37,7 @@ let is_empty_context_rel def = | Ast.RelD (_, [ { it = El.Atom.Turnstile; _} ] :: _, _, _) -> true | _ -> false -let preprocess_il il = +let extract_validation_il il = il |> List.concat_map flatten_rec |> List.filter (fun rel -> is_context_rel rel || is_empty_context_rel rel) @@ -181,7 +181,7 @@ let rec prem_to_instrs prem = | Ast.IfPr e -> if_expr_to_instrs e | Ast.RulePr (id, _, e) -> - let rel = match List.find_opt (rel_has_id id) !Langs.preprocessed_il with Some rel -> rel | None -> failwith id.it in + let rel = match List.find_opt (rel_has_id id) !Langs.validation_il with Some rel -> rel | None -> failwith id.it in let args = exp_to_argexpr e in ( match get_rel_kind rel, args with (* contextless *) @@ -518,7 +518,7 @@ let postprocess_prose defs = (** Entry for generating validation prose **) let gen_validation_prose () = - prose_of_rels (!Langs.preprocessed_il) + prose_of_rels (!Langs.validation_il) let get_state_arg_opt f = let arg = ref (Al.Ast.TypA (Il.Ast.BoolT $ no_region)) in @@ -596,7 +596,7 @@ let gen_execution_prose () = (** Main entry for generating prose **) let gen_prose el il al = Langs.el := el; - Langs.preprocessed_il := preprocess_il il; + Langs.validation_il := extract_validation_il il; Langs.il := il; Langs.al := al; diff --git a/spectec/src/backend-prose/langs.ml b/spectec/src/backend-prose/langs.ml index 5462e128fc..f8799ad3b0 100644 --- a/spectec/src/backend-prose/langs.ml +++ b/spectec/src/backend-prose/langs.ml @@ -1,4 +1,4 @@ let el = ref [] -let preprocessed_il = ref [] +let validation_il = ref [] let il = ref [] let al = ref [] diff --git a/spectec/src/backend-prose/langs.mli b/spectec/src/backend-prose/langs.mli index ca29dcdcaf..e8ddae43bf 100644 --- a/spectec/src/backend-prose/langs.mli +++ b/spectec/src/backend-prose/langs.mli @@ -1,4 +1,4 @@ val el : El.Ast.script ref -val preprocessed_il : Il.Ast.script ref +val validation_il : Il.Ast.script ref val il : Il.Ast.script ref val al : Al.Ast.script ref