src/Doc/more_antiquote.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 69597 ff784d5a5bfb
child 70304 1514efa1e57a
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      Doc/more_antiquote.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 More antiquotations (partly depending on Isabelle/HOL).
     5 *)
     6 
     7 structure More_Antiquote : sig end =
     8 struct
     9 
    10 (* class specifications *)
    11 
    12 val _ =
    13   Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\<open>class_spec\<close> (Scan.lift Args.name)
    14     (fn ctxt => fn s =>
    15       let
    16         val thy = Proof_Context.theory_of ctxt;
    17         val class = Sign.intern_class thy s;
    18       in Pretty.chunks (Class.pretty_specification thy class) end));
    19 
    20 
    21 (* code theorem antiquotation *)
    22 
    23 fun no_vars ctxt thm =
    24   let
    25     val ctxt' = Variable.set_body false ctxt;
    26     val ((_, [thm]), _) = Variable.import true [thm] ctxt';
    27   in thm end;
    28 
    29 val _ =
    30   Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\<open>code_thms\<close> Args.term
    31     (fn ctxt => fn raw_const =>
    32       let
    33         val thy = Proof_Context.theory_of ctxt;
    34         val const = Code.check_const thy raw_const;
    35         val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
    36         val thms = Code_Preproc.cert eqngr const
    37           |> Code.equations_of_cert thy
    38           |> snd
    39           |> these
    40           |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
    41           |> map (HOLogic.mk_obj_eq o no_vars ctxt o Axclass.overload ctxt);
    42       in Pretty.chunks (map (Thy_Output.pretty_thm ctxt) thms) end));
    43 
    44 end;