--- 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)
--- 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 *}
--- 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 \
--- 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 **)
--- /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;
--- 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
--- 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);