src/Doc/more_antiquote.ML
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (19 months ago)
changeset 67022 49309fe530fd
parent 63554 d7c6a3a01b79
child 67386 998e01d6f8fd
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@48985
     1
(*  Title:      Doc/more_antiquote.ML
haftmann@28440
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@28440
     3
haftmann@63026
     4
More antiquotations (partly depending on Isabelle/HOL).
haftmann@28440
     5
*)
haftmann@28440
     6
wenzelm@56061
     7
structure More_Antiquote : sig end =
haftmann@28440
     8
struct
haftmann@28440
     9
haftmann@63026
    10
(* class specifications *)
haftmann@63026
    11
haftmann@63026
    12
local
haftmann@63026
    13
haftmann@63026
    14
fun class_spec ctxt s =
haftmann@63026
    15
  let
haftmann@63026
    16
    val thy = Proof_Context.theory_of ctxt;
haftmann@63026
    17
    val class = Sign.intern_class thy s;
haftmann@63026
    18
  in Thy_Output.output ctxt (Class.pretty_specification thy class) end;
haftmann@63026
    19
haftmann@63026
    20
in
haftmann@63026
    21
haftmann@63026
    22
val _ =
haftmann@63026
    23
  Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name)
haftmann@63026
    24
    (fn {context, ...} => class_spec context));
haftmann@63026
    25
haftmann@63026
    26
end;
haftmann@63026
    27
haftmann@63554
    28
haftmann@29397
    29
(* code theorem antiquotation *)
haftmann@29397
    30
haftmann@29397
    31
local
haftmann@29397
    32
haftmann@29397
    33
fun no_vars ctxt thm =
haftmann@29397
    34
  let
haftmann@29397
    35
    val ctxt' = Variable.set_body false ctxt;
wenzelm@31794
    36
    val ((_, [thm]), _) = Variable.import true [thm] ctxt';
haftmann@29397
    37
  in thm end;
haftmann@29397
    38
haftmann@63554
    39
fun pretty_code_thm ctxt raw_const =
haftmann@29397
    40
  let
wenzelm@42361
    41
    val thy = Proof_Context.theory_of ctxt;
haftmann@31156
    42
    val const = Code.check_const thy raw_const;
haftmann@63160
    43
    val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
haftmann@29874
    44
    fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
haftmann@34896
    45
    val thms = Code_Preproc.cert eqngr const
haftmann@35246
    46
      |> Code.equations_of_cert thy
haftmann@34896
    47
      |> snd
haftmann@54889
    48
      |> these
haftmann@35246
    49
      |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
wenzelm@63073
    50
      |> map (holize o no_vars ctxt o Axclass.overload ctxt);
haftmann@63554
    51
  in Thy_Output.output ctxt (map (Thy_Output.pretty_thm ctxt) thms) end;
haftmann@29397
    52
haftmann@29397
    53
in
haftmann@29397
    54
wenzelm@56061
    55
val _ =
wenzelm@56061
    56
  Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term
haftmann@63554
    57
    (fn {context, ...} => pretty_code_thm context));
haftmann@29397
    58
haftmann@29397
    59
end;
haftmann@29397
    60
haftmann@28440
    61
end;