1 (* Title: doc-src/more_antiquote.ML
2 Author: Florian Haftmann, TU Muenchen
7 signature MORE_ANTIQUOTE =
11 structure More_Antiquote : MORE_ANTIQUOTE =
14 (* code theorem antiquotation *)
18 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
20 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
22 fun no_vars ctxt thm =
24 val ctxt' = Variable.set_body false ctxt;
25 val ((_, [thm]), _) = Variable.import true [thm] ctxt';
28 fun pretty_code_thm src ctxt raw_const =
30 val thy = ProofContext.theory_of ctxt;
31 val const = Code.check_const thy raw_const;
32 val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
33 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
34 val thms = Code_Preproc.cert eqngr const
35 |> Code.equations_of_cert thy
37 |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
38 |> map (holize o no_vars ctxt o AxClass.overload thy);
39 in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
43 val _ = Thy_Output.antiquotation "code_thms" Args.term
44 (fn {source, context, ...} => pretty_code_thm source context);