separation of static and dynamic thy context

--- a/src/Tools/Code/code_preproc.ML	Thu Sep 16 16:51:34 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu Sep 16 16:51:34 2010 +0200
@@ -29,7 +29,9 @@
   val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
   val static_eval_conv: theory -> string list
-    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
+    -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
+  val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
+    -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
 
   val setup: theory -> theory
 end
@@ -138,6 +140,8 @@
 
 fun preprocess_conv thy ct =
   let
+    val ctxt = ProofContext.init_global thy;
+    val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
     val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
     ct
@@ -145,6 +149,8 @@
     |> trans_conv_rule (AxClass.unoverload_conv thy)
   end;
 
+fun preprocess_term thy = term_of_conv thy (preprocess_conv thy);
+
 fun postprocess_conv thy ct =
   let
     val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
@@ -427,43 +433,56 @@
 
 fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
 
-fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
+fun dynamic_eval_conv thy conv ct =
   let
-    val ctxt = Syntax.init_pretty_global thy;
-    val ct = cterm_of proto_ct;
-    val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
-    val thm = preprocess_conv thy ct;
-    val ct' = Thm.rhs_of thm;
+    val thm1 = preprocess_conv thy ct;
+    val ct' = Thm.rhs_of thm1;
     val (vs', t') = dest_cterm ct';
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
     val (algebra', eqngr') = obtain false thy consts [t'];
-  in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end;
+    val thm2 = conv algebra' eqngr' vs' t' ct';
+    val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
+  in
+    Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
+      error ("could not construct evaluation proof:\n"
+      ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
+  end;
 
-fun dynamic_eval_conv thy =
+fun dynamic_eval_value thy postproc evaluator t =
   let
-    fun conclude_evaluation thm2 thm1 =
-      let
-        val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
-      in
-        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
-          error ("could not construct evaluation proof:\n"
-          ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
-      end;
-  in dynamic_eval thy I conclude_evaluation end;
-
-fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
-  (K o postproc (postprocess_term thy)) (K oooo evaluator);
+    val t' = preprocess_term thy t;
+    val vs' = Term.add_tfrees t' [];
+    val consts = fold_aterms
+      (fn Const (c, _) => insert (op =) c | _ => I) t' [];
+    val (algebra', eqngr') = obtain false thy consts [t'];
+    val result = evaluator algebra' eqngr' vs' t';
+  in
+    evaluator algebra' eqngr' vs' t'
+    |> postproc (postprocess_term thy)
+  end;
 
 fun static_eval_conv thy consts conv =
   let
     val (algebra, eqngr) = obtain true thy consts [];
+    val conv' = conv algebra eqngr;
   in
     Conv.tap_thy (fn thy => (preprocess_conv thy)
-      then_conv (fn ct => uncurry (conv algebra eqngr) (dest_cterm ct) ct)
+      then_conv (fn ct => uncurry (conv' thy) (dest_cterm ct) ct)
       then_conv (postprocess_conv thy))
   end;
 
+fun static_eval_value thy postproc consts evaluator =
+  let
+    val (algebra, eqngr) = obtain true thy consts [];
+    val evaluator' = evaluator algebra eqngr;
+  in fn t =>
+    t
+    |> preprocess_term thy
+    |> (fn t => evaluator' thy (Term.add_tfrees t [])  t)
+    |> postproc (postprocess_term thy)
+  end;
+
 
 (** setup **)
 

--- a/src/Tools/Code/code_simp.ML	Thu Sep 16 16:51:34 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu Sep 16 16:51:34 2010 +0200
@@ -84,7 +84,8 @@
 (* evaluation with freezed code context *)
 
 fun static_eval_conv thy some_ss consts = no_frees_conv
-  (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
+  (Code_Thingol.static_eval_conv_simple thy consts
+    (fn program => fn thy => 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_thingol.ML	Thu Sep 16 16:51:34 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Sep 16 16:51:34 2010 +0200
@@ -99,10 +99,13 @@
     -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
   val static_eval_conv: theory -> string list
-    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
+    -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
     -> conv
   val static_eval_conv_simple: theory -> string list
-    -> (program -> conv) -> conv
+    -> (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)
+    -> term -> 'a
 end;
 
 structure Code_Thingol: CODE_THINGOL =
@@ -884,25 +887,34 @@
     #> term_value
   end;
 
-fun base_evaluator thy evaluator algebra eqngr vs t =
+fun base_evaluator evaluator algebra eqngr thy 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 ((vs'', (vs', ty')), t') deps end;
+  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;
 
-fun dynamic_eval_conv thy = Code_Preproc.dynamic_eval_conv thy o base_evaluator thy;
-fun dynamic_eval_value thy postproc = Code_Preproc.dynamic_eval_value thy postproc o base_evaluator thy;
+fun dynamic_eval_conv thy evaluator =
+  Code_Preproc.dynamic_eval_conv thy (dynamic_evaluator thy evaluator);
+
+fun dynamic_eval_value thy postproc evaluator =
+  Code_Preproc.dynamic_eval_value thy postproc (dynamic_evaluator thy evaluator);
 
 fun static_eval_conv thy consts conv =
-  Code_Preproc.static_eval_conv thy consts (base_evaluator thy conv); (*FIXME avoid re-generation*)
+  Code_Preproc.static_eval_conv thy consts (base_evaluator conv); (*FIXME avoid re-generation*)
 
 fun static_eval_conv_simple thy consts conv =
-  Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn _ => fn _ => fn ct =>
+  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)) ct);
+      |> (snd o snd o snd)) thy ct);
 
+fun static_eval_value thy postproc consts conv =
+  Code_Preproc.static_eval_value thy postproc consts (base_evaluator conv); (*FIXME avoid re-generation*)
+  
 
 (** diagnostic commands **)
 

--- a/src/Tools/nbe.ML	Thu Sep 16 16:51:34 2010 +0200
+++ b/src/Tools/nbe.ML	Thu Sep 16 16:51:34 2010 +0200
@@ -609,7 +609,8 @@
 
 fun static_eval_conv thy consts = Code_Simp.no_frees_conv
   (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
-    (K (fn program => oracle thy program (compile true thy program)))));
+    (K (fn program => let val nbe_program = compile true thy program
+      in fn thy => oracle thy program nbe_program end))));
 
 
 (** setup **)