# HG changeset patch
# User haftmann
# Date 1276604902 -7200
# Node ID 037ee7b712b269fcb425a36a0eb91e079dfdf609
# Parent  69ba3f21c2958f8dfcc2db6bb60e71b1486c4544
added code_simp infrastructure

diff -r 69ba3f21c295 -r 037ee7b712b2 NEWS
--- a/NEWS	Tue Jun 15 14:28:08 2010 +0200
+++ b/NEWS	Tue Jun 15 14:28:22 2010 +0200
@@ -35,6 +35,12 @@
 * List.thy: use various operations from the Haskell prelude when
 generating Haskell code.
 
+* code_simp.ML: simplification with rules determined by
+code generator.
+
+* code generator: do not print function definitions for case
+combinators any longer.
+
 
 
 New in Isabelle2009-2 (June 2010)
diff -r 69ba3f21c295 -r 037ee7b712b2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Jun 15 14:28:08 2010 +0200
+++ b/src/HOL/HOL.thy	Tue Jun 15 14:28:22 2010 +0200
@@ -1773,6 +1773,7 @@
 setup {*
   Code_Preproc.map_pre (K HOL_basic_ss)
   #> Code_Preproc.map_post (K HOL_basic_ss)
+  #> Code_Simp.map_ss (K HOL_basic_ss)
 *}
 
 subsubsection {* Equality *}
diff -r 69ba3f21c295 -r 037ee7b712b2 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jun 15 14:28:08 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Jun 15 14:28:22 2010 +0200
@@ -112,6 +112,7 @@
   $(SRC)/Tools/Code/code_preproc.ML \
   $(SRC)/Tools/Code/code_printer.ML \
   $(SRC)/Tools/Code/code_scala.ML \
+  $(SRC)/Tools/Code/code_simp.ML \
   $(SRC)/Tools/Code/code_target.ML \
   $(SRC)/Tools/Code/code_thingol.ML \
   $(SRC)/Tools/Code_Generator.thy \
diff -r 69ba3f21c295 -r 037ee7b712b2 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Jun 15 14:28:08 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Jun 15 14:28:22 2010 +0200
@@ -28,6 +28,7 @@
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
   val eval: theory -> ((term -> term) -> 'a -> 'a)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
+  val pre_post_conv: theory -> (cterm -> thm) -> cterm -> thm
 
   val setup: theory -> theory
 end
@@ -457,6 +458,8 @@
 fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
   (K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
 
+fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy);
+
 
 (** setup **)
 
diff -r 69ba3f21c295 -r 037ee7b712b2 src/Tools/Code/code_simp.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/code_simp.ML	Tue Jun 15 14:28:22 2010 +0200
@@ -0,0 +1,83 @@
+(*  Title:      Tools/code/code_simp.ML
+    Author:     Florian Haftmann, TU Muenchen
+
+Connecting the simplifier and the code generator.
+*)
+
+signature CODE_SIMP =
+sig
+  val no_frees_conv: conv -> conv
+  val map_ss: (simpset -> simpset) -> theory -> theory
+  val current_conv: theory -> conv
+  val current_tac: theory -> int -> tactic
+  val make_conv: theory -> simpset option -> string list -> conv
+  val make_tac: theory -> simpset option -> string list -> int -> tactic
+  val setup: theory -> theory
+end;
+
+structure Code_Simp : CODE_SIMP =
+struct
+
+(* avoid free variables during conversion *)
+
+fun no_frees_conv conv ct =
+  let
+    val frees = Thm.add_cterm_frees ct [];
+    fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
+      |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
+      |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
+  in
+    ct
+    |> fold_rev Thm.cabs frees
+    |> conv
+    |> fold apply_beta frees
+  end;
+
+
+(* dedicated simpset *)
+
+structure Simpset = Theory_Data (
+  type T = simpset;
+  val empty = empty_ss;
+  fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
+  val merge = merge_ss;
+);
+
+val map_ss = Simpset.map;
+
+
+(* build simpset and conversion from program *)
+
+fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
+      ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong)
+  | add_stmt (Code_Thingol.Classinst (_, (_, classparam_insts))) ss =
+      ss addsimps (map (fst o snd) classparam_insts)
+  | add_stmt _ ss = ss;
+
+val add_program = Graph.fold (add_stmt o fst o snd)
+
+fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite
+  (add_program program (Simplifier.global_context thy
+    (the_default (Simpset.get thy) some_ss)));
+
+
+(* evaluation with current code context *)
+
+fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy
+  (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
+
+fun current_tac thy = CONVERSION (current_conv thy);
+
+val setup = Method.setup (Binding.name "code_simp")
+  (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of))
+  "simplification with code equations"
+
+
+(* evaluation with freezed code context *)
+
+fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
+  ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
+
+fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts);
+
+end;
diff -r 69ba3f21c295 -r 037ee7b712b2 src/Tools/Code_Generator.thy
--- a/src/Tools/Code_Generator.thy	Tue Jun 15 14:28:08 2010 +0200
+++ b/src/Tools/Code_Generator.thy	Tue Jun 15 14:28:22 2010 +0200
@@ -13,6 +13,7 @@
   "~~/src/Tools/value.ML"
   "~~/src/Tools/Code/code_preproc.ML" 
   "~~/src/Tools/Code/code_thingol.ML"
+  "~~/src/Tools/Code/code_simp.ML"
   "~~/src/Tools/Code/code_printer.ML"
   "~~/src/Tools/Code/code_target.ML"
   "~~/src/Tools/Code/code_ml.ML"
@@ -24,6 +25,7 @@
 
 setup {*
   Code_Preproc.setup
+  #> Code_Simp.setup
   #> Code_ML.setup
   #> Code_Eval.setup
   #> Code_Haskell.setup
diff -r 69ba3f21c295 -r 037ee7b712b2 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Jun 15 14:28:08 2010 +0200
+++ b/src/Tools/nbe.ML	Tue Jun 15 14:28:22 2010 +0200
@@ -581,19 +581,6 @@
 fun norm_oracle thy program vsp_ty_t deps ct =
   raw_norm_oracle (thy, program, vsp_ty_t, deps, ct);
 
-fun no_frees_conv conv ct =
-  let
-    val frees = Thm.add_cterm_frees ct [];
-    fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
-      |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
-      |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
-  in
-    ct
-    |> fold_rev Thm.cabs frees
-    |> conv
-    |> fold apply_beta frees
-  end;
-
 fun no_frees_rew rew t =
   let
     val frees = map Free (Term.add_frees t []);
@@ -604,7 +591,7 @@
     |> (fn t' => Term.betapplys (t', frees))
   end;
 
-val norm_conv = no_frees_conv (fn ct =>
+val norm_conv = Code_Simp.no_frees_conv (fn ct =>
   let
     val thy = Thm.theory_of_cterm ct;
   in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (K (norm_oracle thy))) ct end);