# HG changeset patch # User haftmann # Date 1292920193 -3600 # Node ID ce825d32b4507a6d8a2319a2e4009ff6ea0446dd # Parent e284a364f724b683f891f7f2113e356fb155e850# Parent 0e2a3f22f0185de37ef6a7d79230dde462707c47 merged diff -r e284a364f724 -r ce825d32b450 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Tue Dec 21 09:16:03 2010 +0100 +++ b/src/Tools/Code/code_preproc.ML Tue Dec 21 09:29:53 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; diff -r e284a364f724 -r ce825d32b450 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Tue Dec 21 09:16:03 2010 +0100 +++ b/src/Tools/Code/code_runtime.ML Tue Dec 21 09:29:53 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 **) diff -r e284a364f724 -r ce825d32b450 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Tue Dec 21 09:16:03 2010 +0100 +++ b/src/Tools/Code/code_simp.ML Tue Dec 21 09:29:53 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; diff -r e284a364f724 -r ce825d32b450 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Dec 21 09:16:03 2010 +0100 +++ b/src/Tools/Code/code_thingol.ML Tue Dec 21 09:29:53 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 **) diff -r e284a364f724 -r ce825d32b450 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Dec 21 09:16:03 2010 +0100 +++ b/src/Tools/nbe.ML Tue Dec 21 09:29:53 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 **)