# HG changeset patch
# User haftmann
# Date 1190299054 -7200
# Node ID f79f6061525c5ec77bf9a1857c182f559668cdbd
# Parent  a705b98345900535fb21a68849616bea23a7ec55
more precise treatment of free dictionary parameters for evaluation

diff -r a705b9834590 -r f79f6061525c src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Thu Sep 20 16:37:33 2007 +0200
+++ b/src/Tools/code/code_package.ML	Thu Sep 20 16:37:34 2007 +0200
@@ -468,15 +468,8 @@
 fun satisfies thy ct witnesses =
   let
     fun evl code ((vs, ty), t) deps ct =
-      let
-        val t0 = Thm.term_of ct
-        val _ = (Term.map_types o Term.map_atyps) (fn _ =>
-          error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
-          t0;
-      in
-        eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
-          code (t, ty) witnesses
-      end;
+      eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
+        code (t, ty) witnesses;
   in eval_term thy evl ct end;
 
 fun filter_generatable thy consts =
diff -r a705b9834590 -r f79f6061525c src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Thu Sep 20 16:37:33 2007 +0200
+++ b/src/Tools/code/code_target.ML	Thu Sep 20 16:37:34 2007 +0200
@@ -1601,6 +1601,8 @@
 
 fun eval_invoke thy labelled_name allows_exception (ref_name, reff) code (t, ty) args =
   let
+    val _ = if CodeThingol.contains_dictvar t then
+      error "Term to be evaluated constains free dictionaries" else ();
     val val_name = "Isabelle_Eval.EVAL.EVAL";
     val val_name' = "Isabelle_Eval.EVAL";
     val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
diff -r a705b9834590 -r f79f6061525c src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Thu Sep 20 16:37:33 2007 +0200
+++ b/src/Tools/code/code_thingol.ML	Thu Sep 20 16:37:34 2007 +0200
@@ -53,6 +53,7 @@
   val collapse_let: ((vname * itype) * iterm) * iterm
     -> (iterm * itype) * (iterm * iterm) list;
   val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
+  val contains_dictvar: iterm -> bool;
   val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
@@ -231,6 +232,15 @@
     val vs_tys = Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys);
   in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
 
+fun contains_dictvar t =
+  let
+    fun contains (DictConst (_, dss)) = (fold o fold) contains dss
+      | contains (DictVar _) = K true;
+  in
+    fold_aiterms
+      (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false
+  end;
+  
 
 (** definitions, transactions **)