author | wenzelm |
Sun, 30 Jan 2011 22:44:02 +0100 | |
changeset 42535 | e4e0b2c08950 |
parent 39762 | 49c319fff40c |
child 43232 | 23f352990944 |
permissions | -rw-r--r-- |
wenzelm@30394 | 1 |
(* Title: doc-src/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 |
haftmann@28440 | 9 |
end; |
haftmann@28440 | 10 |
|
haftmann@28440 | 11 |
structure More_Antiquote : MORE_ANTIQUOTE = |
haftmann@28440 | 12 |
struct |
haftmann@28440 | 13 |
|
haftmann@29394 | 14 |
(* code theorem antiquotation *) |
haftmann@29394 | 15 |
|
haftmann@29394 | 16 |
local |
haftmann@29394 | 17 |
|
haftmann@29394 | 18 |
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; |
haftmann@29394 | 19 |
|
haftmann@29394 | 20 |
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; |
haftmann@29394 | 21 |
|
haftmann@29394 | 22 |
fun no_vars ctxt thm = |
haftmann@29394 | 23 |
let |
haftmann@29394 | 24 |
val ctxt' = Variable.set_body false ctxt; |
wenzelm@31794 | 25 |
val ((_, [thm]), _) = Variable.import true [thm] ctxt'; |
haftmann@29394 | 26 |
in thm end; |
haftmann@29394 | 27 |
|
haftmann@29394 | 28 |
fun pretty_code_thm src ctxt raw_const = |
haftmann@29394 | 29 |
let |
haftmann@29394 | 30 |
val thy = ProofContext.theory_of ctxt; |
haftmann@31156 | 31 |
val const = Code.check_const thy raw_const; |
haftmann@39762 | 32 |
val (_, eqngr) = Code_Preproc.obtain true thy [const] []; |
haftmann@29811 | 33 |
fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; |
haftmann@34896 | 34 |
val thms = Code_Preproc.cert eqngr const |
haftmann@35246 | 35 |
|> Code.equations_of_cert thy |
haftmann@34896 | 36 |
|> snd |
haftmann@35246 | 37 |
|> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) |
haftmann@29811 | 38 |
|> map (holize o no_vars ctxt o AxClass.overload thy); |
wenzelm@39042 | 39 |
in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end; |
haftmann@29394 | 40 |
|
haftmann@29394 | 41 |
in |
haftmann@29394 | 42 |
|
wenzelm@37216 | 43 |
val _ = Thy_Output.antiquotation "code_thms" Args.term |
wenzelm@30394 | 44 |
(fn {source, context, ...} => pretty_code_thm source context); |
haftmann@29394 | 45 |
|
haftmann@29394 | 46 |
end; |
haftmann@29394 | 47 |
|
haftmann@28440 | 48 |
end; |