# 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);