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