author | Walther Neuper <neuper@ist.tugraz.at> |
Sun, 14 Jul 2013 14:48:14 +0200 | |
changeset 52056 | f5d9bceb4dc0 |
parent 50000 | 5386df44a037 |
child 52822 | 385ef6706252 |
permissions | -rw-r--r-- |
wenzelm@50000 | 1 |
(* Title: Doc/more_antiquote.ML |
haftmann@28440 | 2 |
Author: Florian Haftmann, TU Muenchen |
haftmann@28440 | 3 |
|
haftmann@28440 | 4 |
More antiquotations. |
haftmann@28440 | 5 |
*) |
haftmann@28440 | 6 |
|
haftmann@28440 | 7 |
signature MORE_ANTIQUOTE = |
haftmann@28440 | 8 |
sig |
wenzelm@44450 | 9 |
val setup: theory -> theory |
haftmann@28440 | 10 |
end; |
haftmann@28440 | 11 |
|
haftmann@28440 | 12 |
structure More_Antiquote : MORE_ANTIQUOTE = |
haftmann@28440 | 13 |
struct |
haftmann@28440 | 14 |
|
haftmann@29394 | 15 |
(* code theorem antiquotation *) |
haftmann@29394 | 16 |
|
haftmann@29394 | 17 |
local |
haftmann@29394 | 18 |
|
haftmann@29394 | 19 |
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; |
haftmann@29394 | 20 |
|
haftmann@29394 | 21 |
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
haftmann@29394 | 22 |
|
haftmann@29394 | 23 |
fun no_vars ctxt thm = |
haftmann@29394 | 24 |
let |
haftmann@29394 | 25 |
val ctxt' = Variable.set_body false ctxt; |
wenzelm@31794 | 26 |
val ((_, [thm]), _) = Variable.import true [thm] ctxt'; |
haftmann@29394 | 27 |
in thm end; |
haftmann@29394 | 28 |
|
haftmann@29394 | 29 |
fun pretty_code_thm src ctxt raw_const = |
haftmann@29394 | 30 |
let |
wenzelm@43232 | 31 |
val thy = Proof_Context.theory_of ctxt; |
haftmann@31156 | 32 |
val const = Code.check_const thy raw_const; |
haftmann@39762 | 33 |
val (_, eqngr) = Code_Preproc.obtain true thy [const] []; |
haftmann@29811 | 34 |
fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; |
haftmann@34896 | 35 |
val thms = Code_Preproc.cert eqngr const |
haftmann@35246 | 36 |
|> Code.equations_of_cert thy |
haftmann@34896 | 37 |
|> snd |
haftmann@35246 | 38 |
|> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |
haftmann@29811 | 39 |
|> map (holize o no_vars ctxt o AxClass.overload thy); |
wenzelm@39042 | 40 |
in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end; |
haftmann@29394 | 41 |
|
haftmann@29394 | 42 |
in |
haftmann@29394 | 43 |
|
wenzelm@44450 | 44 |
val setup = |
wenzelm@44450 | 45 |
Thy_Output.antiquotation @{binding code_thms} Args.term |
wenzelm@44450 | 46 |
(fn {source, context, ...} => pretty_code_thm source context); |
haftmann@29394 | 47 |
|
haftmann@29394 | 48 |
end; |
haftmann@29394 | 49 |
|
haftmann@28440 | 50 |
end; |