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