# HG changeset patch
# User haftmann
# Date 1201269289 -3600
# Node ID d3f8ab2726edf7c3637d0f697b3afb4161fbc78f
# Parent  66cfe1d00be00b67251908bdc30ce09ce155ced6
tuned

diff -r 66cfe1d00be0 -r d3f8ab2726ed src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Fri Jan 25 14:54:48 2008 +0100
+++ b/src/Tools/code/code_package.ML	Fri Jan 25 14:54:49 2008 +0100
@@ -84,17 +84,9 @@
    of SOME (c, trns) => (SOME c, trns)
     | NONE => (NONE, trns);
 
-fun generate thy funcgr gen it =
-  let
-    val naming = NameSpace.qualified_names NameSpace.default_naming;
-    val consttab = Consts.empty
-      |> fold (fn c => Consts.declare true naming [] (c, CodeFuncgr.typ funcgr c))
-           (CodeFuncgr.all funcgr);
-    val algbr = (Code.operational_algebra thy, consttab);
-  in   
-    Program.change_yield thy
-      (CodeThingol.transact (gen thy algbr funcgr it))
-  end;
+fun generate thy funcgr f x =
+  Program.change_yield thy (CodeThingol.transact thy funcgr
+    (fn thy => fn funcgr => fn algbr => f thy funcgr algbr x));
 
 fun code thy permissive cs seris =
   let
diff -r 66cfe1d00be0 -r d3f8ab2726ed src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Fri Jan 25 14:54:48 2008 +0100
+++ b/src/Tools/code/code_target.ML	Fri Jan 25 14:54:49 2008 +0100
@@ -243,12 +243,12 @@
     fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
           else if c = c_min then
             if negative then SOME ~1 else NONE
-          else error "Illegal numeral expression"
+          else error "Illegal numeral expression: illegal leading digit"
       | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
           if c = c_bit then let val (n, b) = (dest_numeral t1, dest_bit t2)
             in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
-          else error "Illegal numeral expression"
-      | dest_numeral _ = error "Illegal numeral expression";
+          else error "Illegal numeral expression: illegal bit shift operator"
+      | dest_numeral _ = error "Illegal numeral expression: illegal constant";
   in dest_numeral #> the_default 0 end;
 
 fun implode_monad c_bind t =
diff -r 66cfe1d00be0 -r d3f8ab2726ed src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Fri Jan 25 14:54:48 2008 +0100
+++ b/src/Tools/code/code_thingol.ML	Fri Jan 25 14:54:49 2008 +0100
@@ -87,7 +87,9 @@
   val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
     -> CodeFuncgr.T -> term -> transact -> string * transact;
   val add_value_stmt: iterm * itype -> code -> code;
-  val transact: (transact -> 'a * transact) -> code -> 'a * code;
+  val transact: theory -> CodeFuncgr.T
+    -> (theory -> ((sort -> sort) * Sorts.algebra) * Consts.T -> CodeFuncgr.T
+      -> transact -> 'a * transact) -> code -> 'a * code;
 end;
 
 structure CodeThingol: CODE_THINGOL =
@@ -357,10 +359,18 @@
     |> pair name
   end;
 
-fun transact f code =
-  (NONE, code)
-  |> f
-  |-> (fn x => fn (_, code) => (x, code));
+fun transact thy funcgr f code =
+  let
+    val naming = NameSpace.qualified_names NameSpace.default_naming;
+    val consttab = Consts.empty
+      |> fold (fn c => Consts.declare true naming [] (c, CodeFuncgr.typ funcgr c))
+           (CodeFuncgr.all funcgr);
+    val algbr = (Code.operational_algebra thy, consttab);
+  in
+    (NONE, code)
+    |> f thy algbr funcgr
+    |-> (fn x => fn (_, code) => (x, code))
+  end;
 
 
 (* translation kernel *)
@@ -614,6 +624,14 @@
       end
   | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
 
+
+(** evaluation **)
+
+fun add_value_stmt (t, ty) code =
+  code
+  |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
+  |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
+
 fun ensure_value thy algbr funcgr t = 
   let
     val ty = fastype_of t;
@@ -628,10 +646,37 @@
     ensure_stmt stmt_value CodeName.value_name
   end;
 
-fun add_value_stmt (t, ty) code =
-  code
-  |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
-  |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
+fun eval evaluate term_of thy g code0 =
+  let
+    fun result (_, code) =
+      let
+        val Fun ((vs, ty), [(([], t), _)]) =
+          Graph.get_node code CodeName.value_name;
+        val deps = Graph.imm_succs code CodeName.value_name;
+        val code' = Graph.del_nodes [CodeName.value_name] code;
+        val code'' = project_code false [] (SOME deps) code';
+      in ((code'', ((vs, ty), t), deps), code') end;
+    fun h funcgr ct =
+      let
+        val ((code, vs_ty_t, deps), _) =
+          code0
+          |> transact thy funcgr (fn thy => fn algbr => fn funcgr =>
+               ensure_value thy algbr funcgr (term_of ct))
+          |> result
+          ||> `(fn code' => code');
+      in g code vs_ty_t deps ct end;
+  in evaluate thy h end;
+
+val _ : (theory -> (CodeFuncgr.T -> 'Z -> 'Y) -> 'X)
+                  -> ('Z -> term)
+                     -> theory
+                        -> (stmt Graph.T
+                            -> ((vname * sort) list * itype) * iterm
+                               -> Graph.key list -> 'Z -> 'Y)
+                           -> stmt Graph.T -> 'X = eval;
+
+fun eval_conv thy = eval CodeFuncgr.eval_conv Thm.term_of thy;
+fun eval_term thy = eval CodeFuncgr.eval_term I thy;
 
 end; (*struct*)