doc-src/more_antiquote.ML
author bulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 42020 2da02764d523
parent 39540 49c319fff40c
child 42361 23f352990944
permissions -rw-r--r--
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
     1 (*  Title:      doc-src/more_antiquote.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 More antiquotations.
     5 *)
     6 
     7 signature MORE_ANTIQUOTE =
     8 sig
     9 end;
    10 
    11 structure More_Antiquote : MORE_ANTIQUOTE =
    12 struct
    13 
    14 (* code theorem antiquotation *)
    15 
    16 local
    17 
    18 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
    19 
    20 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    21 
    22 fun no_vars ctxt thm =
    23   let
    24     val ctxt' = Variable.set_body false ctxt;
    25     val ((_, [thm]), _) = Variable.import true [thm] ctxt';
    26   in thm end;
    27 
    28 fun pretty_code_thm src ctxt raw_const =
    29   let
    30     val thy = ProofContext.theory_of ctxt;
    31     val const = Code.check_const thy raw_const;
    32     val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
    33     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    34     val thms = Code_Preproc.cert eqngr const
    35       |> Code.equations_of_cert thy
    36       |> snd
    37       |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
    38       |> map (holize o no_vars ctxt o AxClass.overload thy);
    39   in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
    40 
    41 in
    42 
    43 val _ = Thy_Output.antiquotation "code_thms" Args.term
    44   (fn {source, context, ...} => pretty_code_thm source context);
    45 
    46 end;
    47 
    48 end;