doc-src/more_antiquote.ML
author wenzelm
Sat, 16 Apr 2011 16:15:37 +0200
changeset 42361 23f352990944
parent 39540 49c319fff40c
child 43564 9864182c6bad
permissions -rw-r--r--
modernized structure Proof_Context;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30202
diff changeset
     1
(*  Title:      doc-src/more_antiquote.ML
28440
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     3
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     4
More antiquotations.
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     5
*)
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     6
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     7
signature MORE_ANTIQUOTE =
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     8
sig
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
     9
end;
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    10
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    11
structure More_Antiquote : MORE_ANTIQUOTE =
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    12
struct
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    13
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    14
(* code theorem antiquotation *)
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    15
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    16
local
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    17
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    18
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    19
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    20
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    21
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    22
fun no_vars ctxt thm =
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    23
  let
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    24
    val ctxt' = Variable.set_body false ctxt;
31794
71af1fd6a5e4 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents: 31156
diff changeset
    25
    val ((_, [thm]), _) = Variable.import true [thm] ctxt';
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    26
  in thm end;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    27
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    28
fun pretty_code_thm src ctxt raw_const =
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    29
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 39540
diff changeset
    30
    val thy = Proof_Context.theory_of ctxt;
31156
90fed3d4430f merged module code_unit.ML into code.ML
haftmann
parents: 31143
diff changeset
    31
    val const = Code.check_const thy raw_const;
39540
49c319fff40c adjusted
haftmann
parents: 39478
diff changeset
    32
    val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
29874
0b92f68124e8 display code theorems with HOL equality
haftmann
parents: 29619
diff changeset
    33
    fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
34896
a22b09addd78 adjusted to changes in code equation administration
haftmann
parents: 34072
diff changeset
    34
    val thms = Code_Preproc.cert eqngr const
35246
bcbb5ba7dbbc adjusted to changes in cs b987b803616d
haftmann
parents: 34896
diff changeset
    35
      |> Code.equations_of_cert thy
34896
a22b09addd78 adjusted to changes in code equation administration
haftmann
parents: 34072
diff changeset
    36
      |> snd
35246
bcbb5ba7dbbc adjusted to changes in cs b987b803616d
haftmann
parents: 34896
diff changeset
    37
      |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
29874
0b92f68124e8 display code theorems with HOL equality
haftmann
parents: 29619
diff changeset
    38
      |> map (holize o no_vars ctxt o AxClass.overload thy);
38767
d8da44a8dd25 proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents: 37216
diff changeset
    39
  in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    40
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    41
in
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    42
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36745
diff changeset
    43
val _ = Thy_Output.antiquotation "code_thms" Args.term
30394
c11a1e65a2ed moved @{ML_functor} and @{ML_text} to Pure;
wenzelm
parents: 30202
diff changeset
    44
  (fn {source, context, ...} => pretty_code_thm source context);
29397
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    45
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    46
end;
aab26a65e80f dded code_thm antiquotation
haftmann
parents: 28921
diff changeset
    47
28440
0b9ddfa6458e added more_antiquote.ML
haftmann
parents:
diff changeset
    48
end;