src/Tools/Code/code_simp.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69593 3dda49e08b9d
permissions -rw-r--r--
more strict AFP properties;
     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: (Proof.context -> Proof.context) -> theory -> theory
    10   val dynamic_conv: Proof.context -> conv
    11   val dynamic_tac: Proof.context -> int -> tactic
    12   val dynamic_value: Proof.context -> term -> term
    13   val static_conv: { ctxt: Proof.context, simpset: simpset option, consts: string list }
    14     -> Proof.context -> conv
    15   val static_tac: { ctxt: Proof.context, simpset: simpset option, consts: string list }
    16     -> Proof.context -> int -> tactic
    17   val trace: bool Config.T
    18 end;
    19 
    20 structure Code_Simp : CODE_SIMP =
    21 struct
    22 
    23 (* dedicated simpset *)
    24 
    25 structure Simpset = Theory_Data
    26 (
    27   type T = simpset;
    28   val empty = empty_ss;
    29   val extend = I;
    30   val merge = merge_ss;
    31 );
    32 
    33 fun map_ss f thy =
    34   Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy;
    35 
    36 fun simpset_default ctxt some_ss =
    37   the_default (Simpset.get (Proof_Context.theory_of ctxt)) some_ss;
    38 
    39 
    40 (* diagnostic *)
    41 
    42 val trace = Attrib.setup_config_bool \<^binding>\<open>code_simp_trace\<close> (K false);
    43 
    44 fun set_trace ctxt =
    45   let
    46     val global = Config.get ctxt trace;
    47   in
    48     ctxt |> Config.map Simplifier.simp_trace (fn b => b orelse global)
    49   end;
    50 
    51 
    52 (* build simpset context and conversion from program *)
    53 
    54 fun add_stmt (Code_Thingol.Fun ((_, eqs), some_cong)) ss =
    55       ss
    56       |> fold Simplifier.add_simp ((map_filter (fst o snd)) eqs)
    57       |> fold Simplifier.add_cong (the_list some_cong)
    58   | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss =
    59       ss
    60       |> fold Simplifier.add_simp (map (fst o snd) inst_params)
    61   | add_stmt _ ss = ss;
    62 
    63 val add_program = Code_Symbol.Graph.fold (add_stmt o fst o snd);
    64 
    65 val simpset_program =
    66   Code_Preproc.timed "building simpset" #ctxt
    67   (fn { ctxt, some_ss, program } => simpset_map ctxt (add_program program) (simpset_default ctxt some_ss));
    68 
    69 fun rewrite_modulo ctxt some_ss program =
    70   let
    71     val ss = simpset_program
    72       { ctxt = ctxt, some_ss = some_ss, program = program };
    73   in fn ctxt => 
    74     Code_Preproc.timed_conv "simplifying"
    75       Simplifier.full_rewrite (ctxt |> put_simpset ss |> set_trace)
    76   end;
    77 
    78 fun conclude_tac ctxt some_ss =
    79   let
    80     val ss = simpset_default ctxt some_ss
    81   in fn ctxt => Simplifier.full_simp_tac (ctxt |> put_simpset ss) end;
    82 
    83 
    84 (* evaluation with dynamic code context *)
    85 
    86 fun dynamic_conv ctxt = Code_Thingol.dynamic_conv ctxt
    87   (fn program => fn _ => fn _ => rewrite_modulo ctxt NONE program ctxt);
    88 
    89 fun dynamic_tac ctxt = CONVERSION (dynamic_conv ctxt)
    90   THEN' conclude_tac ctxt NONE ctxt;
    91 
    92 fun dynamic_value ctxt =
    93   snd o Logic.dest_equals o Thm.prop_of o dynamic_conv ctxt o Thm.cterm_of ctxt;
    94 
    95 val _ = Theory.setup 
    96   (Method.setup \<^binding>\<open>code_simp\<close>
    97     (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac)))
    98     "simplification with code equations");
    99 
   100 
   101 (* evaluation with static code context *)
   102 
   103 fun static_conv { ctxt, simpset, consts } =
   104   Code_Thingol.static_conv_isa { ctxt = ctxt, consts = consts }
   105     (fn program => let
   106        val conv = rewrite_modulo ctxt simpset program
   107      in fn ctxt => fn _ => conv ctxt end);
   108 
   109 fun static_tac { ctxt, simpset, consts } =
   110   let
   111     val conv = static_conv { ctxt = ctxt, simpset = simpset, consts = consts };
   112     val tac = conclude_tac ctxt simpset;
   113   in fn ctxt' => CONVERSION (conv ctxt') THEN' (tac ctxt') end;
   114 
   115 end;