merged

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

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

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

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

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