src/Doc/more_antiquote.ML
author blanchet
Mon Dec 17 22:06:28 2012 +0100 (2012-12-17)
changeset 50583 681edd111e9b
parent 48985 5386df44a037
child 51685 385ef6706252
permissions -rw-r--r--
really honor pattern depth, and use 2 by default
     1 (*  Title:      Doc/more_antiquote.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 More antiquotations.
     5 *)
     6 
     7 signature MORE_ANTIQUOTE =
     8 sig
     9   val setup: theory -> theory
    10 end;
    11 
    12 structure More_Antiquote : MORE_ANTIQUOTE =
    13 struct
    14 
    15 (* code theorem antiquotation *)
    16 
    17 local
    18 
    19 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
    20 
    21 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    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 fun pretty_code_thm src ctxt raw_const =
    30   let
    31     val thy = Proof_Context.theory_of ctxt;
    32     val const = Code.check_const thy raw_const;
    33     val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
    34     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    35     val thms = Code_Preproc.cert eqngr const
    36       |> Code.equations_of_cert thy
    37       |> snd
    38       |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
    39       |> map (holize o no_vars ctxt o AxClass.overload thy);
    40   in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
    41 
    42 in
    43 
    44 val setup =
    45   Thy_Output.antiquotation @{binding code_thms} Args.term
    46     (fn {source, context, ...} => pretty_code_thm source context);
    47 
    48 end;
    49 
    50 end;