# HG changeset patch
# User haftmann
# Date 1284714353 -7200
# Node ID 80b2cf3b077976051369a4c25ea16be01f09b1ce
# Parent  e992bcc4440e50b5afa6fa57cf2061989f53c562
proper closures for static evaluation; no need for FIXMEs any longer

diff -r e992bcc4440e -r 80b2cf3b0779 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Sep 17 11:05:51 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Sep 17 11:05:53 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 **)