doc-src/more_antiquote.ML
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 43564 9864182c6bad
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
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
wenzelm@43564
     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@29397
    15
(* code theorem antiquotation *)
haftmann@29397
    16
haftmann@29397
    17
local
haftmann@29397
    18
haftmann@29397
    19
fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
haftmann@29397
    20
haftmann@29397
    21
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
haftmann@29397
    22
haftmann@29397
    23
fun no_vars ctxt thm =
haftmann@29397
    24
  let
haftmann@29397
    25
    val ctxt' = Variable.set_body false ctxt;
wenzelm@31794
    26
    val ((_, [thm]), _) = Variable.import true [thm] ctxt';
haftmann@29397
    27
  in thm end;
haftmann@29397
    28
haftmann@29397
    29
fun pretty_code_thm src ctxt raw_const =
haftmann@29397
    30
  let
wenzelm@42361
    31
    val thy = Proof_Context.theory_of ctxt;
haftmann@31156
    32
    val const = Code.check_const thy raw_const;
haftmann@39540
    33
    val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
haftmann@29874
    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@29874
    39
      |> map (holize o no_vars ctxt o AxClass.overload thy);
wenzelm@38767
    40
  in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
haftmann@29397
    41
haftmann@29397
    42
in
haftmann@29397
    43
wenzelm@43564
    44
val setup =
wenzelm@43564
    45
  Thy_Output.antiquotation @{binding code_thms} Args.term
wenzelm@43564
    46
    (fn {source, context, ...} => pretty_code_thm source context);
haftmann@29397
    47
haftmann@29397
    48
end;
haftmann@29397
    49
haftmann@28440
    50
end;