# HG changeset patch # User haftmann # Date 1284719217 -7200 # Node ID 742435a3a99225fa8c280b70d9924276db1e9255 # Parent 9f0e5684f04bc7023853455d1682480a14a3eede# Parent 80b2cf3b077976051369a4c25ea16be01f09b1ce merged diff -r 9f0e5684f04b -r 742435a3a992 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Fri Sep 17 10:52:35 2010 +0200 +++ b/src/Tools/Code/code_runtime.ML Fri Sep 17 12:26:57 2010 +0200 @@ -47,17 +47,23 @@ val _ = Context.>> (Context.map_theory (Code_Target.extend_target (target, (Code_ML.target_SML, K I)) - #> Code_Target.add_tyco_syntax target @{type_name prop} (SOME (0, (K o K o K) (Code_Printer.str s_truth))) - #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds} (SOME (Code_Printer.plain_const_syntax s_Holds)) + #> Code_Target.add_tyco_syntax target @{type_name prop} + (SOME (0, (K o K o K) (Code_Printer.str s_truth))) + #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds} + (SOME (Code_Printer.plain_const_syntax s_Holds)) #> Code_Target.add_reserved target this - #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"])); (*avoid further pervasive infix names*) + #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"])); + (*avoid further pervasive infix names*) (* evaluation into target language values *) type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string; -fun base_evaluator cookie thy some_target naming program ((vs, ty), t) deps args = +fun obtain_serializer thy some_target = Code_Target.produce_code_for thy + (the_default target some_target) NONE "Code" []; + +fun base_evaluator cookie serializer naming thy program ((vs, ty), t) deps args = let val ctxt = ProofContext.init_global thy; val _ = if Code_Thingol.contains_dictvar t then @@ -70,8 +76,7 @@ |> Graph.new_node (value_name, Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))) |> fold (curry Graph.add_edge value_name) deps; - val (program_code, [SOME value_name']) = Code_Target.produce_code_for thy - (the_default target some_target) NONE "Code" [] naming program' [value_name]; + val (program_code, [SOME value_name']) = serializer naming program' [value_name]; val value_code = space_implode " " (value_name' :: "()" :: map (enclose "(" ")") args); in Exn.capture (ML_Context.value ctxt cookie) (program_code, value_code) end; @@ -84,7 +89,7 @@ fun dynamic_value_exn cookie thy some_target postproc t args = let fun evaluator naming program ((_, vs_ty), t) deps = - base_evaluator cookie thy some_target naming program (vs_ty, t) deps args; + base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args; in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end; fun dynamic_value_strict cookie thy some_target postproc t args = @@ -95,8 +100,9 @@ fun static_value_exn cookie thy some_target postproc consts = let + val serializer = obtain_serializer thy some_target; fun evaluator naming program thy ((_, vs_ty), t) deps = - base_evaluator cookie thy some_target naming program (vs_ty, t) deps []; + base_evaluator cookie serializer naming thy program (vs_ty, t) deps []; in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end; fun static_value_strict cookie thy some_target postproc consts t = @@ -115,14 +121,14 @@ val put_truth = Truth_Result.put; val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth"); -fun check_holds thy naming program vs_t deps ct = +fun check_holds serializer naming thy program vs_t deps ct = let val t = Thm.term_of ct; val _ = if fastype_of t <> propT then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) else (); val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT)); - val result = case partiality_as_none (base_evaluator truth_cookie thy NONE naming program vs_t deps []) + val result = case partiality_as_none (base_evaluator truth_cookie serializer naming thy program vs_t deps []) of SOME Holds => true | _ => false; in @@ -131,15 +137,21 @@ val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "holds_by_evaluation", - fn (thy, naming, program, vs_t, deps, ct) => check_holds thy naming program vs_t deps ct))); + fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct))); -fun check_holds_oracle thy naming program ((_, vs_ty), t) deps ct = - raw_check_holds_oracle (thy, naming, program, (vs_ty, t), deps, ct); +fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct = + raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct); + +val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy + (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)); -val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy (check_holds_oracle thy)); - -fun static_holds_conv thy consts = Code_Thingol.static_eval_conv thy consts - (fn naming => fn program => fn thy => check_holds_oracle thy naming program); +fun static_holds_conv thy consts = + let + val serializer = obtain_serializer thy NONE; + in + Code_Thingol.static_eval_conv thy consts + (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program) + end; (** instrumentalization **) @@ -253,7 +265,7 @@ fun add_eval_const (const, const') = Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const'))); -fun process (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy = +fun process_reflection (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy = thy |> Code_Target.add_reserved target module_name |> Context.theory_map @@ -261,7 +273,7 @@ |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map |> fold (add_eval_const o apsnd Code_Printer.str) const_map - | process (code_body, _) _ (SOME file_name) thy = + | process_reflection (code_body, _) _ (SOME file_name) thy = let val preamble = "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy)) @@ -283,7 +295,7 @@ |> (apsnd o apsnd) (chop (length constrs)); in thy - |> process result module_name some_file + |> process_reflection result module_name some_file end; val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); diff -r 9f0e5684f04b -r 742435a3a992 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Fri Sep 17 10:52:35 2010 +0200 +++ b/src/Tools/Code/code_simp.ML Fri Sep 17 12:26:57 2010 +0200 @@ -66,7 +66,7 @@ fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss); -(* evaluation with current code context *) +(* evaluation with dynamic code context *) 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)); @@ -81,11 +81,11 @@ #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of); -(* evaluation with freezed code context *) +(* evaluation with static code context *) fun static_eval_conv thy some_ss consts = no_frees_conv (Code_Thingol.static_eval_conv_simple thy consts - (fn program => fn thy => rewrite_modulo thy some_ss program)); + (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program)); fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts) THEN' conclude_tac thy some_ss; diff -r 9f0e5684f04b -r 742435a3a992 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Fri Sep 17 10:52:35 2010 +0200 +++ b/src/Tools/Code/code_target.ML Fri Sep 17 12:26:57 2010 +0200 @@ -241,7 +241,7 @@ local -fun activate_target_for thy target naming program = +fun activate_target thy target = let val ((targets, abortable), default_width) = Targets.get thy; fun collapse_hierarchy target = @@ -250,13 +250,13 @@ of SOME data => data | NONE => error ("Unknown code target language: " ^ quote target); in case the_description data - of Fundamental _ => (I, data) + of Fundamental _ => (K I, data) | Extension (super, modify) => let val (modify', data') = collapse_hierarchy super - in (modify' #> modify naming, merge_target false target (data', data)) end + in (fn naming => modify' naming #> modify naming, merge_target false target (data', data)) end end; val (modify, data) = collapse_hierarchy target; - in (default_width, abortable, data, modify program) end; + in (default_width, abortable, data, modify) end; fun activate_syntax lookup_name src_tab = Symtab.empty |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier @@ -303,7 +303,7 @@ val program4 = Graph.subgraph (member (op =) names4) program3; in (names4, program4) end; -fun invoke_serializer thy abortable serializer literals reserved abs_includes +fun invoke_serializer thy abortable serializer literals reserved all_includes module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax module_name args naming proto_program names = let @@ -311,7 +311,12 @@ activate_symbol_syntax thy literals naming proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax; val (names_all, program) = project_program thy abortable names_hidden names proto_program; - val includes = abs_includes names_all; + fun select_include (name, (content, cs)) = + if null cs orelse exists (fn c => case Code_Thingol.lookup_const naming c + of SOME name => member (op =) names_all name + | NONE => false) cs + then SOME (name, content) else NONE; + val includes = map_filter select_include (Symtab.dest all_includes); in serializer args { labelled_name = Code_Thingol.labelled_name thy proto_program, @@ -324,29 +329,20 @@ program = program } end; -fun mount_serializer thy target some_width module_name args naming proto_program names = +fun mount_serializer thy target some_width module_name args = let - val (default_width, abortable, data, program) = - activate_target_for thy target naming proto_program; + val (default_width, abortable, data, modify) = activate_target thy target; val serializer = case the_description data of Fundamental seri => #serializer seri; val reserved = the_reserved data; - fun select_include names_all (name, (content, cs)) = - if null cs then SOME (name, content) - else if exists (fn c => case Code_Thingol.lookup_const naming c - of SOME name => member (op =) names_all name - | NONE => false) cs - then SOME (name, content) else NONE; - fun includes names_all = map_filter (select_include names_all) - ((Symtab.dest o the_includes) data); val module_alias = the_module_alias data val { class, instance, tyco, const } = the_symbol_syntax data; val literals = the_literals thy target; val width = the_default default_width some_width; - in + in fn naming => fn program => fn names => invoke_serializer thy abortable serializer literals reserved - includes module_alias class instance tyco const module_name args - naming program names width + (the_includes data) module_alias class instance tyco const module_name args + naming (modify naming program) names width end; fun assert_module_name "" = error ("Empty module name not allowed.") @@ -354,16 +350,22 @@ in -fun export_code_for thy some_path target some_width some_module_name args naming program names = - export some_path (mount_serializer thy target some_width some_module_name args naming program names); +fun export_code_for thy some_path target some_width module_name args = + export some_path ooo mount_serializer thy target some_width module_name args; -fun produce_code_for thy target some_width module_name args naming program names = +fun produce_code_for thy target some_width module_name args = let - val (s, deresolve) = produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names) - in (s, map deresolve names) end; + val serializer = mount_serializer thy target some_width (assert_module_name module_name) args; + in fn naming => fn program => fn names => + produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names) + end; -fun present_code_for thy target some_width module_name args naming program (names, selects) = - present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names); +fun present_code_for thy target some_width module_name args = + let + val serializer = mount_serializer thy target some_width (assert_module_name module_name) args; + in fn naming => fn program => fn (names, selects) => + present selects (serializer naming program names) + end; fun check_code_for thy target strict args naming program names_cs = let diff -r 9f0e5684f04b -r 742435a3a992 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Sep 17 10:52:35 2010 +0200 +++ b/src/Tools/Code/code_thingol.ML Fri Sep 17 12:26:57 2010 +0200 @@ -92,19 +92,20 @@ val read_const_exprs: theory -> string list -> string list * string list val consts_program: theory -> bool -> string list -> string list * (naming * program) - val dynamic_eval_conv: theory - -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv) + val dynamic_eval_conv: theory -> (naming -> program + -> ((string * sort) list * typscheme) * iterm -> string list -> conv) -> conv - val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a) - -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) + val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program + -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) -> term -> 'a - val static_eval_conv: theory -> string list - -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv) + val static_eval_conv: theory -> string list -> (naming -> program + -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv) -> conv val static_eval_conv_simple: theory -> string list - -> (program -> theory -> conv) -> conv - val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list - -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) + -> (program -> theory -> (string * sort) list -> term -> conv) -> conv + val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list -> + (naming -> program + -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) -> term -> 'a end; @@ -844,17 +845,17 @@ (* program generation *) -fun consts_program thy permissive cs = +fun consts_program thy permissive consts = let - fun project_consts cs (naming, program) = (*FIXME only necessary for cache_generation*) - let - val cs_all = Graph.all_succs program cs; - in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end; + fun project_consts consts (naming, program) = + if permissive then (consts, (naming, program)) + else (consts, (naming, Graph.subgraph + (member (op =) (Graph.all_succs program consts)) program)); fun generate_consts thy algebra eqngr = fold_map (ensure_const thy algebra eqngr permissive); in - invoke_generation (not permissive) thy (Code_Preproc.obtain false thy cs []) - generate_consts cs + invoke_generation permissive thy (Code_Preproc.obtain false thy consts []) + generate_consts consts |-> project_consts end; @@ -887,15 +888,14 @@ #> term_value end; -fun base_evaluator evaluator algebra eqngr thy vs t = +fun original_sorts vs = + map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)); + +fun dynamic_evaluator thy evaluator algebra eqngr vs t = let val (((naming, program), (((vs', ty'), t'), deps)), _) = invoke_generation false thy (algebra, eqngr) ensure_value t; - val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs'; - in evaluator naming program thy ((vs'', (vs', ty')), t') deps end; - -fun dynamic_evaluator thy evaluator algebra eqngr vs t = - base_evaluator (fn naming => fn program => fn _ => evaluator naming program) algebra eqngr thy vs t; + in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end; fun dynamic_eval_conv thy evaluator = Code_Preproc.dynamic_eval_conv thy (dynamic_evaluator thy evaluator); @@ -903,18 +903,32 @@ fun dynamic_eval_value thy postproc evaluator = Code_Preproc.dynamic_eval_value thy postproc (dynamic_evaluator thy evaluator); +fun provide_program thy consts f algebra eqngr = + let + fun generate_consts thy algebra eqngr = + fold_map (ensure_const thy algebra eqngr false); + val (_, (naming, program)) = invoke_generation true thy (algebra, eqngr) + generate_consts consts; + in f algebra eqngr naming program end; + +fun static_evaluator evaluator algebra eqngr naming program thy vs t = + let + val (((_, program'), (((vs', ty'), t'), deps)), _) = + ensure_value thy algebra eqngr t (NONE, (naming, program)); + in evaluator naming program' thy ((original_sorts vs vs', (vs', ty')), t') deps end; + fun static_eval_conv thy consts conv = - Code_Preproc.static_eval_conv thy consts (base_evaluator conv); (*FIXME avoid re-generation*) + Code_Preproc.static_eval_conv thy consts + (provide_program thy consts (static_evaluator conv)); fun static_eval_conv_simple thy consts conv = - Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn thy => fn _ => fn _ => fn ct => - conv ((NONE, (empty_naming, Graph.empty)) (*FIXME provide abstraction for this kind of invocation*) - |> fold_map (ensure_const thy algebra eqngr false) consts - |> (snd o snd o snd)) thy ct); + Code_Preproc.static_eval_conv thy consts + (provide_program thy consts ((K o K o K) conv)); -fun static_eval_value thy postproc consts conv = - Code_Preproc.static_eval_value thy postproc consts (base_evaluator conv); (*FIXME avoid re-generation*) - +fun static_eval_value thy postproc consts evaluator = + Code_Preproc.static_eval_value thy postproc consts + (provide_program thy consts (static_evaluator evaluator)); + (** diagnostic commands **)