src/Doc/more_antiquote.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 months ago)
changeset 69981 3dced198b9ec
parent 69597 ff784d5a5bfb
child 70304 1514efa1e57a
permissions -rw-r--r--
more strict AFP properties;
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
val _ =
wenzelm@69597
    13
  Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\<open>class_spec\<close> (Scan.lift Args.name)
wenzelm@67463
    14
    (fn ctxt => fn s =>
wenzelm@67463
    15
      let
wenzelm@67463
    16
        val thy = Proof_Context.theory_of ctxt;
wenzelm@67463
    17
        val class = Sign.intern_class thy s;
wenzelm@67505
    18
      in Pretty.chunks (Class.pretty_specification thy class) end));
haftmann@63026
    19
haftmann@63554
    20
haftmann@29397
    21
(* code theorem antiquotation *)
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
wenzelm@56061
    29
val _ =
wenzelm@69597
    30
  Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\<open>code_thms\<close> Args.term
wenzelm@67463
    31
    (fn ctxt => fn raw_const =>
wenzelm@67463
    32
      let
wenzelm@67463
    33
        val thy = Proof_Context.theory_of ctxt;
wenzelm@67463
    34
        val const = Code.check_const thy raw_const;
wenzelm@67463
    35
        val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
wenzelm@67463
    36
        val thms = Code_Preproc.cert eqngr const
wenzelm@67463
    37
          |> Code.equations_of_cert thy
wenzelm@67463
    38
          |> snd
wenzelm@67463
    39
          |> these
wenzelm@67463
    40
          |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
wenzelm@67710
    41
          |> map (HOLogic.mk_obj_eq o no_vars ctxt o Axclass.overload ctxt);
wenzelm@67505
    42
      in Pretty.chunks (map (Thy_Output.pretty_thm ctxt) thms) end));
haftmann@29397
    43
haftmann@29397
    44
end;