--- a/src/Tools/Code/code_preproc.ML Tue Dec 21 11:05:30 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML Tue Dec 21 12:02:05 2010 +0100
@@ -29,9 +29,9 @@
val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
-> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
val static_conv: theory -> string list
- -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
+ -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
- -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
+ -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
val setup: theory -> theory
end
@@ -490,7 +490,7 @@
fun static_conv thy consts conv =
let
val (algebra, eqngr) = obtain true thy consts [];
- val conv' = conv algebra eqngr thy;
+ val conv' = conv algebra eqngr;
in
no_variables_conv ((preprocess_conv thy)
then_conv (fn ct => uncurry conv' (dest_cterm ct) ct)
@@ -504,7 +504,7 @@
in
preprocess_term thy
#-> (fn resubst => fn t => t
- |> evaluator' thy (Term.add_tfrees t [])
+ |> evaluator' (Term.add_tfrees t [])
|> postproc (postprocess_term thy o resubst))
end;
--- a/src/Tools/Code/code_runtime.ML Tue Dec 21 11:05:30 2010 +0100
+++ b/src/Tools/Code/code_runtime.ML Tue Dec 21 12:02:05 2010 +0100
@@ -86,25 +86,14 @@
val ctxt = ProofContext.init_global thy;
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
-fun obtain_serializer thy some_target = Code_Target.produce_code_for thy
- (the_default target some_target) NONE "Code" [];
+fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target);
-fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args =
+fun evaluation cookie thy evaluator vs_t args =
let
val ctxt = ProofContext.init_global thy;
- val _ = if Code_Thingol.contains_dict_var t then
- error "Term to be evaluated contains free dictionaries" else ();
- val v' = Name.variant (map fst vs) "a";
- val vs' = (v', []) :: vs;
- val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
- val value_name = "Value.value.value"
- val program' = program
- |> 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']) = serializer naming program' [value_name];
+ val (program_code, value_name) = evaluator vs_t;
val value_code = space_implode " "
- (value_name' :: "()" :: map (enclose "(" ")") args);
+ (value_name :: "()" :: map (enclose "(" ")") args);
in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
fun partiality_as_none e = SOME (Exn.release e)
@@ -119,7 +108,7 @@
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
else ()
fun evaluator naming program ((_, vs_ty), t) deps =
- base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
+ evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args;
in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
fun dynamic_value_strict cookie thy some_target postproc t args =
@@ -128,18 +117,20 @@
fun dynamic_value cookie thy some_target postproc t args =
partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args);
-fun static_value_exn cookie thy some_target postproc consts =
+fun static_evaluator cookie thy some_target naming program consts' =
let
- val serializer = obtain_serializer thy some_target;
- fun evaluator naming program thy ((_, vs_ty), t) deps =
- base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
- in Code_Thingol.static_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
+ val evaluator = obtain_evaluator thy some_target naming program consts'
+ in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end;
-fun static_value_strict cookie thy some_target postproc consts t =
- Exn.release (static_value_exn cookie thy some_target postproc consts t);
+fun static_value_exn cookie thy some_target postproc consts =
+ Code_Thingol.static_value thy (Exn.map_result o postproc) consts
+ (static_evaluator cookie thy some_target) o reject_vars thy;
-fun static_value cookie thy some_target postproc consts t =
- partiality_as_none (static_value_exn cookie thy some_target postproc consts t);
+fun static_value_strict cookie thy some_target postproc consts =
+ Exn.release o static_value_exn cookie thy some_target postproc consts;
+
+fun static_value cookie thy some_target postproc consts =
+ partiality_as_none o static_value_exn cookie thy some_target postproc consts;
(* evaluation for truth or nothing *)
@@ -154,14 +145,16 @@
val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
-fun check_holds serializer naming thy program vs_t deps ct =
+local
+
+fun check_holds thy evaluator 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 serializer naming thy program vs_t deps [])
+ val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t [])
of SOME Holds => true
| _ => false;
in
@@ -170,23 +163,24 @@
val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (Binding.name "holds_by_evaluation",
- fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct)));
+ fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_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);
+fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
+ raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct);
+
+in
fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy
- (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
- o reject_vars thy;
+ (fn naming => fn program => fn vs_t => fn deps =>
+ check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps)
+ o reject_vars thy;
-fun static_holds_conv thy consts =
- let
- val serializer = obtain_serializer thy NONE;
- in
- Code_Thingol.static_conv thy consts
- (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
- o reject_vars thy
- end;
+fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts
+ (fn naming => fn program => fn consts' =>
+ check_holds_oracle thy (obtain_evaluator thy NONE naming program consts'))
+ o reject_vars thy;
+
+end; (*local*)
(** instrumentalization **)
--- a/src/Tools/Code/code_simp.ML Tue Dec 21 11:05:30 2010 +0100
+++ b/src/Tools/Code/code_simp.ML Tue Dec 21 12:02:05 2010 +0100
@@ -68,7 +68,7 @@
fun static_conv thy some_ss consts =
Code_Thingol.static_conv_simple thy consts
- (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
+ (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
THEN' conclude_tac thy some_ss;
--- a/src/Tools/Code/code_target.ML Tue Dec 21 11:05:30 2010 +0100
+++ b/src/Tools/Code/code_target.ML Tue Dec 21 12:02:05 2010 +0100
@@ -421,7 +421,7 @@
val program = prepared_program
|> 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;
+ |> fold (curry (perhaps o try o Graph.add_edge) value_name) deps;
val (program_code, deresolve) = produce (mounted_serializer program);
val value_name' = the (deresolve value_name);
in (program_code, value_name') end;
--- a/src/Tools/Code/code_thingol.ML Tue Dec 21 11:05:30 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Tue Dec 21 12:02:05 2010 +0100
@@ -100,14 +100,14 @@
val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
-> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
-> term -> 'a
- val static_conv: theory -> string list -> (naming -> program
- -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+ val static_conv: theory -> string list -> (naming -> program -> string list
+ -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
-> conv
val static_conv_simple: theory -> string list
- -> (program -> theory -> (string * sort) list -> term -> conv) -> conv
+ -> (program -> (string * sort) list -> term -> conv) -> conv
val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
- (naming -> program
- -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
+ (naming -> program -> string list
+ -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
-> term -> 'a
end;
@@ -916,27 +916,27 @@
let
fun generate_consts thy algebra eqngr =
fold_map (ensure_const thy algebra eqngr false);
- val (_, (naming, program)) = invoke_generation true thy (algebra, eqngr)
+ val (consts', (naming, program)) = invoke_generation true thy (algebra, eqngr)
generate_consts consts;
- in f algebra eqngr naming program end;
+ in f algebra eqngr naming program consts' end;
-fun static_evaluator evaluator algebra eqngr naming program thy vs t =
+fun static_evaluation thy evaluator algebra eqngr naming program consts' 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;
+ in evaluator naming program' consts' ((original_sorts vs vs', (vs', ty')), t') deps end;
fun static_conv thy consts conv =
Code_Preproc.static_conv thy consts
- (provide_program thy consts (static_evaluator conv));
+ (provide_program thy consts (static_evaluation thy conv));
fun static_conv_simple thy consts conv =
Code_Preproc.static_conv thy consts
- (provide_program thy consts ((K o K o K) conv));
+ (provide_program thy consts (fn _ => fn _ => fn _ => fn program => fn _ => conv program));
fun static_value thy postproc consts evaluator =
Code_Preproc.static_value thy postproc consts
- (provide_program thy consts (static_evaluator evaluator));
+ (provide_program thy consts (static_evaluation thy evaluator));
(** diagnostic commands **)
--- a/src/Tools/nbe.ML Tue Dec 21 11:05:30 2010 +0100
+++ b/src/Tools/nbe.ML Tue Dec 21 12:02:05 2010 +0100
@@ -602,13 +602,13 @@
fun static_conv thy consts =
lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
- (K (fn program => let val nbe_program = compile true thy program
- in fn thy => oracle thy program nbe_program end)));
+ (K (fn program => fn _ => let val nbe_program = compile true thy program
+ in oracle thy program nbe_program end)));
fun static_value thy consts = lift_triv_classes_rew thy
(Code_Thingol.static_value thy I consts
- (K (fn program => let val nbe_program = compile true thy program
- in fn thy => eval_term thy program (compile false thy program) end)));
+ (K (fn program => fn _ => let val nbe_program = compile true thy program
+ in eval_term thy program (compile false thy program) end)));
(** setup **)