(*  Title:      doc-src/more_antiquote.ML

     Author:     Florian Haftmann, TU Muenchen

 More antiquotations.

 *)

 signature MORE_ANTIQUOTE =

 sig

   val setup: theory -> theory

 end;

 structure More_Antiquote : MORE_ANTIQUOTE =

 struct

 (* code theorem antiquotation *)

 local

 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;

 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;

 fun no_vars ctxt thm =

   let

     val ctxt' = Variable.set_body false ctxt;

     val ((_, [thm]), _) = Variable.import true [thm] ctxt';

   in thm end;

 fun pretty_code_thm src ctxt raw_const =

   let

     val thy = Proof_Context.theory_of ctxt;

     val const = Code.check_const thy raw_const;

     val (_, eqngr) = Code_Preproc.obtain true thy [const] [];

     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];

     val thms = Code_Preproc.cert eqngr const

       |> Code.equations_of_cert thy

       |> snd

       |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)

       |> map (holize o no_vars ctxt o AxClass.overload thy);

   in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;

 in

 val setup =

   Thy_Output.antiquotation @{binding code_thms} Args.term

     (fn {source, context, ...} => pretty_code_thm source context);

 end;

 end;