src/Tools/Code/code_simp.ML
author haftmann
Tue Jun 05 07:05:56 2012 +0200 (2012-06-05)
changeset 48072 ace701efe203
parent 47576 b32aae03e3d6
child 51717 9e7d1c139569
permissions -rw-r--r--
prefer records with speaking labels over deeply nested tuples
     1 (*  Title:      Tools/Code/code_simp.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Connecting the simplifier and the code generator.
     5 *)
     6 
     7 signature CODE_SIMP =
     8 sig
     9   val map_ss: (simpset -> simpset) -> theory -> theory
    10   val dynamic_conv: theory -> conv
    11   val dynamic_tac: theory -> int -> tactic
    12   val dynamic_value: theory -> term -> term
    13   val static_conv: theory -> simpset option -> string list -> conv
    14   val static_tac: theory -> simpset option -> string list -> int -> tactic
    15   val setup: theory -> theory
    16 end;
    17 
    18 structure Code_Simp : CODE_SIMP =
    19 struct
    20 
    21 (* dedicated simpset *)
    22 
    23 structure Simpset = Theory_Data
    24 (
    25   type T = simpset;
    26   val empty = empty_ss;
    27   fun extend ss = Simplifier.inherit_context empty_ss ss;
    28   val merge = merge_ss;
    29 );
    30 
    31 val map_ss = Simpset.map;
    32 
    33 fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy);
    34 
    35 
    36 (* build simpset and conversion from program *)
    37 
    38 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
    39       ss addsimps (map_filter (fst o snd)) eqs
    40       |> fold Simplifier.add_cong (the_list some_cong)
    41   | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss =
    42       ss addsimps (map (fst o snd) inst_params)
    43   | add_stmt _ ss = ss;
    44 
    45 val add_program = Graph.fold (add_stmt o fst o snd);
    46 
    47 fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite
    48   (add_program program (simpset_default thy some_ss));
    49 
    50 fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss);
    51 
    52 
    53 (* evaluation with dynamic code context *)
    54 
    55 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
    56   (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
    57 
    58 fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE;
    59 
    60 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
    61 
    62 val setup =
    63   Method.setup @{binding code_simp}
    64     (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
    65     "simplification with code equations"
    66   #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);
    67 
    68 
    69 (* evaluation with static code context *)
    70 
    71 fun static_conv thy some_ss consts =
    72   Code_Thingol.static_conv_simple thy consts
    73     (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
    74 
    75 fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
    76   THEN' conclude_tac thy some_ss;
    77 
    78 end;