# HG changeset patch # User wenzelm # Date 1618059350 -7200 # Node ID 53c148e398199b598d405f2218078f86ceb41ec1 # Parent 2f6855142a8c07faf18ab02b8080b76e280dc27f proper treatment of nested antiquotations; clarified signature; diff -r 2f6855142a8c -r 53c148e39819 src/HOL/Analysis/measurable.ML --- a/src/HOL/Analysis/measurable.ML Fri Apr 09 22:06:59 2021 +0200 +++ b/src/HOL/Analysis/measurable.ML Sat Apr 10 14:55:50 2021 +0200 @@ -274,7 +274,7 @@ val t = HOLogic.mk_Trueprop (Thm.term_of redex); fun tac {context = ctxt, prems = _ } = SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt)); - in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end; + in \<^try>\Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}\ end; end diff -r 2f6855142a8c -r 53c148e39819 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Fri Apr 09 22:06:59 2021 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Sat Apr 10 14:55:50 2021 +0200 @@ -97,7 +97,7 @@ (*FIXME: currently does not "rename variables apart"*) fun first_order_resolve ctxt thA thB = (case - try (fn () => + \<^try>\ let val thy = Proof_Context.theory_of ctxt val tmA = Thm.concl_of thA val Const(\<^const_name>\Pure.imp\,_) $ tmB $ _ = Thm.prop_of thB @@ -105,7 +105,7 @@ Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty) |> snd val insts = Vartab.fold (fn (xi, (_, t)) => cons (xi, Thm.cterm_of ctxt t)) tenv []; - in thA RS (infer_instantiate ctxt insts thB) end) () of + in thA RS (infer_instantiate ctxt insts thB) end\ of SOME th => th | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) diff -r 2f6855142a8c -r 53c148e39819 src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Apr 09 22:06:59 2021 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Sat Apr 10 14:55:50 2021 +0200 @@ -166,9 +166,9 @@ SOME (Const (\<^const_name>\HOL.eq\, _) $ _ $ _) => SOME (@{thm refl} RS thm) | SOME _ => (case body_type (fastype_of lhs) of Type (typ_name, _) => - try (fn () => + \<^try>\ #equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name)) - RS @{thm Equiv_Relations.equivp_reflp} RS thm) () + RS @{thm Equiv_Relations.equivp_reflp} RS thm\ | _ => NONE ) | _ => NONE diff -r 2f6855142a8c -r 53c148e39819 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Fri Apr 09 22:06:59 2021 +0200 +++ b/src/Pure/General/antiquote.ML Sat Apr 10 14:55:50 2021 +0200 @@ -9,7 +9,8 @@ type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list} type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list} datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq - val the_text: 'a antiquote -> 'a + val is_text: 'a antiquote -> bool + val the_text: string -> 'a antiquote -> 'a type text_antiquote = Symbol_Pos.T list antiquote val text_antiquote_range: text_antiquote -> Position.range val text_range: text_antiquote list -> Position.range @@ -33,10 +34,15 @@ type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}; datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq; -fun bad_text pos = error ("Unexpected antiquotation" ^ Position.here pos); -fun the_text (Text x) = x - | the_text (Control {range, ...}) = bad_text (#1 range) - | the_text (Antiq {range, ...}) = bad_text (#1 range); +val is_text = fn Text _ => true | _ => false; + +fun the_text msg antiq = + let fun err pos = error (msg ^ Position.here pos) in + (case antiq of + Text x => x + | Control {range, ...} => err (#1 range) + | Antiq {range, ...} => err (#1 range)) + end; type text_antiquote = Symbol_Pos.T list antiquote; diff -r 2f6855142a8c -r 53c148e39819 src/Pure/ML/ml_antiquotation.ML --- a/src/Pure/ML/ml_antiquotation.ML Fri Apr 09 22:06:59 2021 +0200 +++ b/src/Pure/ML/ml_antiquotation.ML Sat Apr 10 14:55:50 2021 +0200 @@ -73,15 +73,17 @@ val (s, _) = Token.syntax (Scan.lift Args.embedded_input) src ctxt; val tokenize = ML_Lex.tokenize_range Position.no_range; val tokenize_range = ML_Lex.tokenize_range (Input.range_of s); - fun decl (_: Proof.context) = + + val (decl, ctxt') = ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt; + fun decl' ctxt'' = let - val expr = ML_Lex.read_source s |> map Antiquote.the_text; - val ml = - tokenize "let val expr = (fn () => " @ expr @ tokenize ");" @ + val (ml_env, ml_body) = decl ctxt''; + val ml_body' = + tokenize "let val expr = (fn () => " @ ml_body @ tokenize ");" @ tokenize " val " @ tokenize_range "result" @ - tokenize (" = " ^ operator ^ " expr; in result end") - in ([], ml) end; - in (decl, ctxt) end); + tokenize (" = " ^ operator ^ " expr; in result end"); + in (ml_env, ml_body') end; + in (decl', ctxt') end); (* basic antiquotations *) diff -r 2f6855142a8c -r 53c148e39819 src/Pure/ML/ml_context.ML --- a/src/Pure/ML/ml_context.ML Fri Apr 09 22:06:59 2021 +0200 +++ b/src/Pure/ML/ml_context.ML Sat Apr 10 14:55:50 2021 +0200 @@ -13,6 +13,8 @@ type antiquotation = Position.range -> Token.src -> Proof.context -> decl * Proof.context val add_antiquotation: binding -> bool -> antiquotation -> theory -> theory val print_antiquotations: bool -> Proof.context -> unit + val expand_antiquotes: ML_Lex.token Antiquote.antiquote list -> + Proof.context -> decl * Proof.context val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit val eval_file: ML_Compiler.flags -> Path.T -> unit val eval_source: ML_Compiler.flags -> Input.source -> unit @@ -90,13 +92,38 @@ in antiquotation range src' ctxt end; -(* parsing and evaluation *) +(* parsing *) local val antiq = Parse.!!! ((Parse.token Parse.liberal_name ::: Parse.args) --| Scan.ahead Parse.eof); +fun expand_antiquote ant ctxt = + (case ant of + Antiquote.Text tok => (K ([], [tok]), ctxt) + | Antiquote.Control {name, range, body} => + ctxt |> apply_antiquotation range + (Token.make_src name (if null body then [] else [Token.read_cartouche body])) + | Antiquote.Antiq {range, body, ...} => + ctxt |> apply_antiquotation range + (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range))); + +in + +fun expand_antiquotes ants ctxt = + let + val (decls, ctxt') = fold_map expand_antiquote ants ctxt; + fun decl ctxt'' = decls |> map (fn d => d ctxt'') |> split_list |> apply2 flat; + in (decl, ctxt') end; + +end; + + +(* evaluation *) + +local + fun make_env name visible = (ML_Lex.tokenize ("structure " ^ name ^ " =\nstruct\n\ @@ -106,38 +133,22 @@ fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end"); -fun eval_antiquotes (ants, pos) opt_context = - let - val visible = - (case opt_context of - SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt - | _ => true); - val opt_ctxt = Option.map Context.proof_of opt_context; - - val ((ml_env, ml_body), opt_ctxt') = - if forall (fn Antiquote.Text _ => true | _ => false) ants - then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt) - else - let - fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt) - | expand (Antiquote.Control {name, range, body}) ctxt = - apply_antiquotation range - (Token.make_src name (if null body then [] else [Token.read_cartouche body])) ctxt - | expand (Antiquote.Antiq {range, body, ...}) ctxt = - apply_antiquotation range - (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt; - - val ctxt = - (case opt_ctxt of - NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos) - | SOME ctxt => struct_begin ctxt); - - val (begin_env, end_env) = make_env (struct_name ctxt) visible; - val (decls, ctxt') = fold_map expand ants ctxt; - val (ml_env, ml_body) = - decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat; - in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end; - in ((ml_env, ml_body), opt_ctxt') end; +fun eval_antiquotes ants opt_context = + if forall Antiquote.is_text ants orelse is_none opt_context then + (([], map (Antiquote.the_text "No context -- cannot expand ML antiquotations") ants), + Option.map Context.proof_of opt_context) + else + let + val context = the opt_context; + val visible = + (case context of + Context.Proof ctxt => Context_Position.is_visible ctxt + | _ => true); + val ctxt = struct_begin (Context.proof_of context); + val (begin_env, end_env) = make_env (struct_name ctxt) visible; + val (decl, ctxt') = expand_antiquotes ants ctxt; + val (ml_env, ml_body) = decl ctxt'; + in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end; in @@ -146,7 +157,7 @@ val non_verbose = ML_Compiler.verbose false flags; (*prepare source text*) - val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.get_generic_context ()); + val ((env, body), env_ctxt) = eval_antiquotes ants (Context.get_generic_context ()); val _ = (case env_ctxt of SOME ctxt =>