# HG changeset patch
# User haftmann
# Date 1241706155 -7200
# Node ID 88aaab83b6fcd93e95bb900288f918dafa08161f
# Parent  878e00798148f5ee6fe61e4106d25f5637d07f75
dropped explicit suppport for frees in evaluation conversion stack

diff -r 878e00798148 -r 88aaab83b6fc src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Thu May 07 16:22:34 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Thu May 07 16:22:35 2009 +0200
@@ -958,10 +958,7 @@
 fun eval some_target reff postproc thy t args =
   let
     val ctxt = ProofContext.init thy;
-    val _ = if null (Term.add_frees t []) then () else error ("Term "
-      ^ quote (Syntax.string_of_term_global thy t)
-      ^ " to be evaluated contains free variables");
-    fun evaluator naming program (((_, (_, ty)), _), t) deps =
+    fun evaluator naming program ((_, (_, ty)), t) deps =
       let
         val _ = if Code_Thingol.contains_dictvar t then
           error "Term to be evaluated contains free dictionaries" else ();
diff -r 878e00798148 -r 88aaab83b6fc src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Thu May 07 16:22:34 2009 +0200
+++ b/src/Tools/code/code_thingol.ML	Thu May 07 16:22:35 2009 +0200
@@ -85,10 +85,10 @@
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
   val eval_conv: theory -> (sort -> sort)
-    -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> cterm -> thm)
+    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
     -> cterm -> thm
   val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
-    -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> 'a)
+    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     -> term -> 'a
 end;
 
@@ -755,7 +755,7 @@
 
 (* value evaluation *)
 
-fun ensure_value thy algbr funcgr (fs, t) =
+fun ensure_value thy algbr funcgr t =
   let
     val ty = fastype_of t;
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
@@ -766,7 +766,7 @@
       ##>> translate_term thy algbr funcgr NONE t
       #>> (fn ((vs, ty), t) => Fun
         (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
-    fun term_value fs (dep, (naming, program1)) =
+    fun term_value (dep, (naming, program1)) =
       let
         val Fun (_, (vs_ty, [(([], t), _)])) =
           Graph.get_node program1 Term.dummy_patternN;
@@ -774,22 +774,19 @@
         val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
         val deps_all = Graph.all_succs program2 deps;
         val program3 = Graph.subgraph (member (op =) deps_all) program2;
-      in (((naming, program3), (((vs_ty, fs), t), deps)), (dep, (naming, program2))) end;
+      in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
   in
     ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
     #> snd
-    #> fold_map (fn (v, ty) => translate_typ thy algbr funcgr ty
-         #-> (fn ty' => pair (v, ty'))) fs
-    #-> (fn fs' => term_value fs')
+    #> term_value
   end;
 
 fun base_evaluator thy evaluator algebra funcgr vs t =
   let
-    val fs = Term.add_frees t [];
-    val (((naming, program), ((((vs', ty'), fs'), t'), deps)), _) =
-      invoke_generation thy (algebra, funcgr) ensure_value (fs, t);
+    val (((naming, program), (((vs', ty'), t'), deps)), _) =
+      invoke_generation thy (algebra, funcgr) 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')), fs'), t') deps end;
+  in evaluator naming program ((vs'', (vs', ty')), t') deps end;
 
 fun eval_conv thy prep_sort = Code_Wellsorted.eval_conv thy prep_sort o base_evaluator thy;
 fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy;
diff -r 878e00798148 -r 88aaab83b6fc src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Thu May 07 16:22:34 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML	Thu May 07 16:22:35 2009 +0200
@@ -293,19 +293,22 @@
 fun obtain thy cs ts = apsnd snd
   (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
 
-fun prepare_sorts prep_sort (Const (c, ty)) = Const (c, map_type_tfree
-      (fn (v, sort) => TFree (v, prep_sort sort)) ty)
+fun prepare_sorts_typ prep_sort
+  = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort));
+
+fun prepare_sorts prep_sort (Const (c, ty)) =
+      Const (c, prepare_sorts_typ prep_sort ty)
   | prepare_sorts prep_sort (t1 $ t2) =
       prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2
   | prepare_sorts prep_sort (Abs (v, ty, t)) =
-      Abs (v, Type.strip_sorts ty, prepare_sorts prep_sort t)
-  | prepare_sorts _ (Term.Free (v, ty)) = Term.Free (v, Type.strip_sorts ty)
+      Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t)
   | prepare_sorts _ (t as Bound _) = t;
 
 fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct =
   let
+    val pp = Syntax.pp_global thy;
     val ct = cterm_of proto_ct;
-    val _ = (Term.map_types Type.no_tvars o Sign.no_vars (Syntax.pp_global thy))
+    val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
       (Thm.term_of ct);
     val thm = Code.preprocess_conv thy ct;
     val ct' = Thm.rhs_of thm;
@@ -313,6 +316,7 @@
     val vs = Term.add_tfrees t' [];
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
+ 
     val t'' = prepare_sorts prep_sort t';
     val (algebra', eqngr') = obtain thy consts [t''];
   in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end;