# HG changeset patch # User haftmann # Date 1282554589 -7200 # Node ID 9ff76d0f0610b06141c1af7ed3bf657e362c210b # Parent e8236c4aff1679875f2876782bed0180a5c3269f refined and unified naming convention for dynamic code evaluation techniques diff -r e8236c4aff16 -r 9ff76d0f0610 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Aug 23 11:09:48 2010 +0200 +++ b/src/HOL/HOL.thy Mon Aug 23 11:09:49 2010 +0200 @@ -1998,7 +1998,7 @@ "solve goal by evaluation" method_setup normalization = {* - Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k))))) + Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k))))) *} "solve goal by normalization" diff -r e8236c4aff16 -r 9ff76d0f0610 src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Mon Aug 23 11:09:48 2010 +0200 +++ b/src/Tools/Code/code_eval.ML Mon Aug 23 11:09:49 2010 +0200 @@ -62,7 +62,7 @@ val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; in ML_Context.evaluate ctxt false reff sml_code end; - in Code_Thingol.eval thy postproc evaluator t end; + in Code_Thingol.dynamic_eval_value thy postproc evaluator t end; (** instrumentalization by antiquotation **) diff -r e8236c4aff16 -r 9ff76d0f0610 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Mon Aug 23 11:09:48 2010 +0200 +++ b/src/Tools/Code/code_preproc.ML Mon Aug 23 11:09:49 2010 +0200 @@ -24,9 +24,9 @@ val all: code_graph -> string list val pretty: theory -> code_graph -> Pretty.T val obtain: theory -> string list -> term list -> code_algebra * code_graph - val eval_conv: theory + val dynamic_eval_conv: theory -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm - val eval: theory -> ((term -> term) -> 'a -> 'a) + val dynamic_eval_value: 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 @@ -74,8 +74,7 @@ if AList.defined (op =) xs key then AList.delete (op =) key xs else error ("No such " ^ msg ^ ": " ^ quote key); -fun map_data f = Code.purge_data - #> (Code_Preproc_Data.map o map_thmproc) f; +val map_data = Code_Preproc_Data.map o map_thmproc; val map_pre_post = map_data o apfst; val map_pre = map_pre_post o apfst; @@ -425,7 +424,7 @@ fun obtain thy cs ts = apsnd snd (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts)); -fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct = +fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct = let val pp = Syntax.pp_global thy; val ct = cterm_of proto_ct; @@ -440,10 +439,7 @@ val (algebra', eqngr') = obtain thy consts [t']; in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end; -fun simple_evaluator evaluator algebra eqngr vs t ct = - evaluator algebra eqngr vs t; - -fun eval_conv thy = +fun dynamic_eval_conv thy = let fun conclude_evaluation thm2 thm1 = let @@ -453,10 +449,10 @@ error ("could not construct evaluation proof:\n" ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3]) end; - in gen_eval thy I conclude_evaluation end; + in dynamic_eval thy I conclude_evaluation end; -fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy) - (K o postproc (postprocess_term thy)) (simple_evaluator evaluator); +fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy) + (K o postproc (postprocess_term thy)) (K oooo evaluator); fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy); diff -r e8236c4aff16 -r 9ff76d0f0610 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Mon Aug 23 11:09:48 2010 +0200 +++ b/src/Tools/Code/code_simp.ML Mon Aug 23 11:09:49 2010 +0200 @@ -8,11 +8,11 @@ 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 current_value: theory -> term -> term - val make_conv: theory -> simpset option -> string list -> conv - val make_tac: theory -> simpset option -> string list -> int -> tactic + val dynamic_eval_conv: theory -> conv + val dynamic_eval_tac: theory -> int -> tactic + val dynamic_eval_value: theory -> term -> term + val static_eval_conv: theory -> simpset option -> string list -> conv + val static_eval_tac: theory -> simpset option -> string list -> int -> tactic val setup: theory -> theory end; @@ -67,25 +67,25 @@ (* evaluation with current code context *) -fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy +fun dynamic_eval_conv thy = no_frees_conv (Code_Thingol.dynamic_eval_conv thy (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)); -fun current_tac thy = CONVERSION (current_conv thy) THEN' conclude_tac thy NONE; +fun dynamic_eval_tac thy = CONVERSION (dynamic_eval_conv thy) THEN' conclude_tac thy NONE; -fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy; +fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv thy o Thm.cterm_of thy; val setup = Method.setup (Binding.name "code_simp") - (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo current_tac o ProofContext.theory_of))) + (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of))) "simplification with code equations" - #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of); + #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of); (* evaluation with freezed code context *) -fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy +fun static_eval_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) +fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts) THEN' conclude_tac thy some_ss; end; diff -r e8236c4aff16 -r 9ff76d0f0610 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Mon Aug 23 11:09:48 2010 +0200 +++ b/src/Tools/Code/code_thingol.ML Mon Aug 23 11:09:49 2010 +0200 @@ -92,10 +92,10 @@ val read_const_exprs: theory -> string list -> string list * string list val consts_program: theory -> bool -> string list -> string list * (naming * program) - val eval_conv: theory + val dynamic_eval_conv: theory -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm) -> cterm -> thm - val eval: theory -> ((term -> term) -> 'a -> 'a) + val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) -> term -> 'a end; @@ -895,8 +895,8 @@ val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs'; in evaluator naming program ((vs'', (vs', ty')), t') deps end; -fun eval_conv thy = Code_Preproc.eval_conv thy o base_evaluator thy; -fun eval thy postproc = Code_Preproc.eval thy postproc o base_evaluator thy; +fun dynamic_eval_conv thy = Code_Preproc.dynamic_eval_conv thy o base_evaluator thy; +fun dynamic_eval_value thy postproc = Code_Preproc.dynamic_eval_value thy postproc o base_evaluator thy; (** diagnostic commands **) diff -r e8236c4aff16 -r 9ff76d0f0610 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Mon Aug 23 11:09:48 2010 +0200 +++ b/src/Tools/nbe.ML Mon Aug 23 11:09:49 2010 +0200 @@ -6,8 +6,8 @@ signature NBE = sig - val norm_conv: cterm -> thm - val norm: theory -> term -> term + val dynamic_eval_conv: cterm -> thm + val dynamic_eval_value: theory -> term -> term datatype Univ = Const of int * Univ list (*named (uninterpreted) constants*) @@ -574,12 +574,11 @@ val rhs = Thm.cterm_of thy raw_rhs; in Thm.mk_binop eq lhs rhs end; -val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result +val (_, raw_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) => mk_equals thy ct (normalize thy program vsp_ty_t deps)))); -fun norm_oracle thy program vsp_ty_t deps ct = - raw_norm_oracle (thy, program, vsp_ty_t, deps, ct); +fun oracle thy program vsp_ty_t deps ct = raw_oracle (thy, program, vsp_ty_t, deps, ct); fun no_frees_rew rew t = let @@ -591,12 +590,11 @@ |> (fn t' => Term.betapplys (t', frees)) end; -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); +val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy + (fn thy => lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy (K (oracle thy))))); -fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (K (normalize thy)))); +fun dynamic_eval_value thy = lift_triv_classes_rew thy + (no_frees_rew (Code_Thingol.dynamic_eval_value thy I (K (normalize thy)))); (* evaluation command *) @@ -604,7 +602,7 @@ fun norm_print_term ctxt modes t = let val thy = ProofContext.theory_of ctxt; - val t' = norm thy t; + val t' = dynamic_eval_value thy t; val ty' = Term.type_of t'; val ctxt' = Variable.auto_fixes t ctxt; val p = Print_Mode.with_modes modes (fn () => @@ -619,7 +617,7 @@ let val ctxt = Toplevel.context_of state in norm_print_term ctxt modes (Syntax.read_term ctxt s) end; -val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of); +val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of); val opt_modes = Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];