# HG changeset patch
# User haftmann
# Date 1187695838 -7200
# Node ID 560e8ecdf633c63e3561e2e99321fb582f64731a
# Parent  c215e256becadd305a8de2dc8183bfde89000d60
improved evaluation interface

diff -r c215e256beca -r 560e8ecdf633 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Tue Aug 21 13:30:36 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Tue Aug 21 13:30:38 2007 +0200
@@ -167,7 +167,8 @@
 end;
 *}
 
-oracle eval_oracle ("term * CodeThingol.code * CodeThingol.iterm * CodeThingol.itype * cterm") = {* fn thy => fn (t0, code, t, ty, ct) => 
+oracle eval_oracle ("term * CodeThingol.code * (CodeThingol.typscheme * CodeThingol.iterm) * cterm") =
+{* fn thy => fn (t0, code, ((vs, ty), t), ct) => 
 let
   val _ = (Term.map_types o Term.map_atyps) (fn _ =>
     error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
@@ -181,7 +182,7 @@
 
 open Eval;
 
-fun eval_invoke thy t0 code (t, ty) _ ct = eval_oracle thy (t0, code, t, ty, ct);
+fun eval_invoke thy t0 code vs_ty_t _ ct = eval_oracle thy (t0, code, vs_ty_t, ct);
 
 fun eval_conv ct =
   let
diff -r c215e256beca -r 560e8ecdf633 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Tue Aug 21 13:30:36 2007 +0200
+++ b/src/Tools/code/code_package.ML	Tue Aug 21 13:30:38 2007 +0200
@@ -9,10 +9,12 @@
 sig
   (* interfaces *)
   val eval_conv: theory
-    -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> thm)
+    -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
+       -> string list -> cterm -> thm)
     -> cterm -> thm;
   val eval_term: theory
-    -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> 'a)
+    -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
+       -> string list -> cterm -> 'a)
     -> cterm -> 'a;
   val satisfies_ref: bool option ref;
   val satisfies: theory -> cterm -> string list -> bool;
@@ -285,10 +287,10 @@
           ##>> exprgen_term thy algbr funcgr rhs;
       in
         trns
-        |> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
-        ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+        |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
         ||>> exprgen_typ thy algbr funcgr ty
-        |>> (fn ((eqs, vs), ty) => CodeThingol.Fun (eqs, (vs, ty)))
+        ||>> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
+        |>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
       end;
     val defgen = if (is_some o Code.get_datatype_of_constr thy) const
       then defgen_datatypecons
@@ -536,25 +538,28 @@
     val value_name = "Isabelle_Eval.EVAL.EVAL";
     fun ensure_eval thy algbr funcgr t = 
       let
+        val ty = fastype_of t;
+        val vs = typ_tfrees ty;
         val defgen_eval =
-          exprgen_term' thy algbr funcgr t
-          ##>> exprgen_typ thy algbr funcgr (fastype_of t)
-          #>> (fn (t, ty) => CodeThingol.Fun ([([], t)], ([], ty)));
+          fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+          ##>> exprgen_typ thy algbr funcgr ty
+          ##>> exprgen_term' thy algbr funcgr t
+          #>> (fn ((vs, ty), t) => CodeThingol.Fun ((vs, ty), [([], t)]));
         fun result (dep, code) =
           let
-            val CodeThingol.Fun ([([], t)], ([], ty)) = Graph.get_node code value_name;
+            val CodeThingol.Fun ((vs, ty), [([], t)]) = Graph.get_node code value_name;
             val deps = Graph.imm_succs code value_name;
             val code' = Graph.del_nodes [value_name] code;
             val code'' = CodeThingol.project_code false [] (SOME deps) code';
-          in ((code'', (t, ty), deps), (dep, code')) end;
+          in ((code'', ((vs, ty), t), deps), (dep, code')) end;
       in
         ensure_def thy defgen_eval "evaluation" value_name
         #> result
       end;
     fun h funcgr ct =
       let
-        val (code, (t, ty), deps) = generate thy funcgr ensure_eval (Thm.term_of ct);
-      in g code (t, ty) deps ct end;
+        val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (Thm.term_of ct);
+      in g code vs_ty_t deps ct end;
   in f thy h end;
 
 fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
@@ -564,7 +569,7 @@
 
 fun satisfies thy ct witnesses =
   let
-    fun evl code (t, ty) deps ct =
+    fun evl code ((vs, ty), t) deps ct =
       let
         val t0 = Thm.term_of ct
         val _ = (Term.map_types o Term.map_atyps) (fn _ =>
diff -r c215e256beca -r 560e8ecdf633 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Tue Aug 21 13:30:36 2007 +0200
+++ b/src/Tools/code/code_target.ML	Tue Aug 21 13:30:38 2007 +0200
@@ -293,7 +293,7 @@
 (** SML/OCaml serializer **)
 
 datatype ml_def =
-    MLFuns of (string * ((iterm list * iterm) list * typscheme)) list
+    MLFuns of (string * (typscheme * (iterm list * iterm) list)) list
   | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
   | MLClass of string * ((class * string) list * (vname * (string * itype) list))
   | MLClassinst of string * ((class * (string * (vname * sort) list))
@@ -423,13 +423,13 @@
                 fun mk [] [] = "val"
                   | mk (_::_) _ = "fun"
                   | mk [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";
-                fun chk (_, ((ts, _) :: _, (vs, _))) NONE = SOME (mk ts vs)
-                  | chk (_, ((ts, _) :: _, (vs, _))) (SOME defi) =
+                fun chk (_, ((vs, _), (ts, _) :: _)) NONE = SOME (mk ts vs)
+                  | chk (_, ((vs, _), (ts, _) :: _)) (SOME defi) =
                       if defi = mk ts vs then SOME defi
                       else error ("Mixing simultaneous vals and funs not implemented: "
                         ^ commas (map (labelled_name o fst) funns));
               in the (fold chk funns NONE) end;
-            fun pr_funn definer (name, (eqs as eq::eqs', (raw_vs, ty))) =
+            fun pr_funn definer (name, ((raw_vs, ty), eqs as eq :: eqs')) =
               let
                 val vs = filter_out (null o snd) raw_vs;
                 val shift = if null eqs' then I else
@@ -758,7 +758,7 @@
                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
                     )
                   end;
-            fun pr_funn definer (name, (eqs, (vs, ty))) =
+            fun pr_funn definer (name, ((vs, ty), eqs)) =
               concat (
                 str definer
                 :: (str o deresolv) name
@@ -1173,7 +1173,7 @@
             ) (map pr bs)
           end
       | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
-    fun pr_def (name, CodeThingol.Fun (eqs, (vs, ty))) =
+    fun pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) =
           let
             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
             fun pr_eq (ts, t) =
diff -r c215e256beca -r 560e8ecdf633 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Tue Aug 21 13:30:36 2007 +0200
+++ b/src/Tools/code/code_thingol.ML	Tue Aug 21 13:30:38 2007 +0200
@@ -58,7 +58,7 @@
 
   datatype def =
       Bot
-    | Fun of (iterm list * iterm) list * typscheme
+    | Fun of typscheme * (iterm list * iterm) list
     | Datatype of (vname * sort) list * (string * itype list) list
     | Datatypecons of string
     | Class of (class * string) list * (vname * (string * itype) list)
@@ -231,12 +231,10 @@
 
 (** definitions, transactions **)
 
-(* type definitions *)
-
 type typscheme = (vname * sort) list * itype;
 datatype def =
     Bot
-  | Fun of (iterm list * iterm) list * typscheme
+  | Fun of typscheme * (iterm list * iterm) list
   | Datatype of (vname * sort) list * (string * itype list) list
   | Datatypecons of string
   | Class of (class * string) list * (vname * (string * itype) list)
@@ -273,7 +271,7 @@
 fun project_code delete_empty_funs hidden raw_selected code =
   let
     fun is_empty_fun name = case Graph.get_node code name
-     of Fun ([], _) => true
+     of Fun (_, []) => true
       | _ => false;
     val names = subtract (op =) hidden (Graph.keys code);
     val deleted = Graph.all_preds code (filter is_empty_fun names);
@@ -291,7 +289,7 @@
   end;
 
 fun empty_funs code =
-  Graph.fold (fn (name, (Fun ([], _), _)) => cons name
+  Graph.fold (fn (name, (Fun (_, []), _)) => cons name
                | _ => I) code [];
 
 fun is_cons code name = case Graph.get_node code name
@@ -322,8 +320,8 @@
 
 fun check_prep_def code Bot =
       Bot
-  | check_prep_def code (Fun (eqs, d)) =
-      Fun (check_funeqs eqs, d)
+  | check_prep_def code (Fun (d, eqs)) =
+      Fun (d, check_funeqs eqs)
   | check_prep_def code (d as Datatype _) =
       d
   | check_prep_def code (Datatypecons dtco) =
@@ -405,7 +403,7 @@
 
 fun add_eval_def (name, (t, ty)) code =
   code
-  |> Graph.new_node (name, Fun ([([], t)], ([], ty)))
+  |> Graph.new_node (name, Fun (([], ty), [([], t)]))
   |> fold (curry Graph.add_edge name) (Graph.keys code);
 
 end; (*struct*)
diff -r c215e256beca -r 560e8ecdf633 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Aug 21 13:30:36 2007 +0200
+++ b/src/Tools/nbe.ML	Tue Aug 21 13:30:38 2007 +0200
@@ -15,7 +15,7 @@
 signature NBE =
 sig
   datatype Univ = 
-      Const of string * Univ list        (*named constructors*)
+      Const of string * Univ list            (*named (uninterpreted) constants*)
     | Free of string * Univ list
     | BVar of int * Univ list
     | Abs of (int * (Univ list -> Univ)) * Univ list;
@@ -63,11 +63,11 @@
 *)
 
 datatype Univ = 
-    Const of string * Univ list        (*named constructors*)
+    Const of string * Univ list        (*named (uninterpreted) constants*)
   | Free of string * Univ list         (*free variables*)
   | BVar of int * Univ list            (*bound named variables*)
   | Abs of (int * (Univ list -> Univ)) * Univ list
-                                      (*functions*);
+                                      (*abstractions as closures*);
 
 (* constructor functions *)
 
@@ -108,7 +108,7 @@
       let
         val _ = univs_ref := [];
         val s = "Nbe.univs_ref := " ^ raw_s;
-        val _ = tracing (fn () => "\n---generated code:\n" ^ s) ();
+        val _ = tracing (fn () => "\n--- generated code:\n" ^ s) ();
         val _ = tab_ref := SOME tab;
         val _ = use_text "" (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
           Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n")
@@ -228,7 +228,7 @@
         val result = ml_list (map (fn (c, n) => nbe_abss n (nbe_fun c)) num_args);
       in (cs, ml_Let (bind_funs @ [bind_locals]) result) end;
 
-fun assemble_eval thy is_fun (t, deps) =
+fun assemble_eval thy is_fun (((vs, ty), t), deps) =
   let
     val funs = CodeThingol.fold_constnames (insert (op =)) t [];
     val frees = CodeThingol.fold_unbound_varnames (insert (op =)) t [];
@@ -238,9 +238,9 @@
     val result = ml_list [nbe_value `$` ml_list (map nbe_free frees)];
   in ([nbe_value], ml_Let (bind_funs @ [bind_value]) result) end;
 
-fun eqns_of_stmt ((_, CodeThingol.Fun ([], _)), _) =
+fun eqns_of_stmt ((_, CodeThingol.Fun (_, [])), _) =
       NONE
-  | eqns_of_stmt ((name, CodeThingol.Fun (eqns, _)), deps) =
+  | eqns_of_stmt ((name, CodeThingol.Fun (_, eqns)), deps) =
       SOME ((name, eqns), deps)
   | eqns_of_stmt ((_, CodeThingol.Datatypecons _), _) =
       NONE
@@ -312,7 +312,7 @@
 
 (* evaluation with type reconstruction *)
 
-fun eval thy code t t' deps =
+fun eval thy code t vs_ty_t deps =
   let
     val ty = type_of t;
     fun subst_Frees [] = I
@@ -328,37 +328,37 @@
       error ("Illegal schematic type variables in normalized term: "
         ^ setmp show_types true (Sign.string_of_term thy) t);
   in
-    (t', deps)
+    (vs_ty_t, deps)
     |> eval_term thy (Symtab.defined (ensure_funs thy code))
     |> term_of_univ thy
     |> tracing (fn t => "Normalized:\n" ^ setmp show_types true Display.raw_string_of_term t)
-    |> tracing (fn _ => "Term type:\n" ^ Display.raw_string_of_typ ty)
     |> anno_vars
     |> tracing (fn t => "Vars typed:\n" ^ setmp show_types true Display.raw_string_of_term t)
-    |> tracing (fn t => setmp show_types true (Sign.string_of_term thy) t)
     |> constrain
     |> tracing (fn t => "Types inferred:\n" ^ setmp show_types true Display.raw_string_of_term t)
     |> check_tvars
+    |> tracing (fn _ => "---\n")
   end;
 
 (* evaluation oracle *)
 
-exception Normalization of CodeThingol.code * term * CodeThingol.iterm * string list;
+exception Normalization of CodeThingol.code * term
+  * (CodeThingol.typscheme * CodeThingol.iterm) * string list;
 
-fun normalization_oracle (thy, Normalization (code, t, t', deps)) =
-  Logic.mk_equals (t, eval thy code t t' deps);
+fun normalization_oracle (thy, Normalization (code, t, vs_ty_t, deps)) =
+  Logic.mk_equals (t, eval thy code t vs_ty_t deps);
 
-fun normalization_invoke thy code t t' deps =
-  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t', deps));
+fun normalization_invoke thy code t vs_ty_t deps =
+  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, vs_ty_t, deps));
   (*FIXME get rid of hardwired theory name*)
 
 fun normalization_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
-    fun conv code (t', ty') deps ct =
+    fun conv code vs_ty_t deps ct =
       let
         val t = Thm.term_of ct;
-      in normalization_invoke thy code t t' deps end;
+      in normalization_invoke thy code t vs_ty_t deps end;
   in CodePackage.eval_conv thy conv ct end;
 
 (* evaluation command *)