# HG changeset patch
# User wenzelm
# Date 1342466456 -7200
# Node ID db75b4005d9aa2bcd90296795ea6a0baa28a160d
# Parent  b28defd0b5a5d59ad022411719ef6859b97b7d64
more direct Sorts.has_instance;
tuned Sorts.mg_domain;

diff -r b28defd0b5a5 -r db75b4005d9a src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Jul 16 15:57:21 2012 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Jul 16 21:20:56 2012 +0200
@@ -139,7 +139,7 @@
     val certs = map (mk_case_cert thy) tycos;
     val tycos_eq =
       filter_out
-        (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_equal]) tycos;
+        (fn tyco => Sorts.has_instance (Sign.classes_of thy) tyco [HOLogic.class_equal]) tycos;
   in
     if null css then thy
     else
diff -r b28defd0b5a5 -r db75b4005d9a src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 16 15:57:21 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 16 21:20:56 2012 +0200
@@ -60,8 +60,8 @@
 
 fun ensure_partial_term_of (tyco, (raw_vs, _)) thy =
   let
-    val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of})
-      andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
+    val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of})
+      andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
   in if need_inst then add_partial_term_of tyco raw_vs thy else thy end;
 
 
@@ -111,7 +111,7 @@
 
 fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
   let
-    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of};
+    val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of};
   in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end;
 
 
diff -r b28defd0b5a5 -r db75b4005d9a src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jul 16 15:57:21 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Jul 16 21:20:56 2012 +0200
@@ -449,7 +449,7 @@
       (Datatype_Aux.interpret_construction descr vs constr)
     val insts = insts_of sort  { atyp = single, dtyp = (K o K o K) [] }
       @ insts_of aux_sort { atyp = K [], dtyp = K o K }
-    val has_inst = exists (fn tyco => can (Sorts.mg_domain algebra tyco) sort) tycos;
+    val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos;
   in if has_inst then thy
     else case perhaps_constrain thy insts vs
      of SOME constrain => instantiate config descr
diff -r b28defd0b5a5 -r db75b4005d9a src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Mon Jul 16 15:57:21 2012 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Mon Jul 16 21:20:56 2012 +0200
@@ -47,8 +47,8 @@
 
 fun ensure_term_of (tyco, (raw_vs, _)) thy =
   let
-    val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of})
-      andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
+    val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of})
+      andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
   in if need_inst then add_term_of tyco raw_vs thy else thy end;
 
 
@@ -88,7 +88,7 @@
 
 fun ensure_term_of_code (tyco, (raw_vs, cs)) thy =
   let
-    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
+    val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of};
   in if has_inst then add_term_of_code tyco raw_vs cs thy else thy end;
 
 
@@ -125,7 +125,7 @@
 
 fun ensure_abs_term_of_code (tyco, (raw_vs, ((abs, (_, ty)), (proj, _)))) thy =
   let
-    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
+    val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of};
   in if has_inst then add_abs_term_of_code tyco raw_vs abs ty proj thy else thy end;
 
 
diff -r b28defd0b5a5 -r db75b4005d9a src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Jul 16 15:57:21 2012 +0200
+++ b/src/HOL/Tools/record.ML	Mon Jul 16 21:20:56 2012 +0200
@@ -1722,7 +1722,7 @@
 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy =
   let
     val algebra = Sign.classes_of thy;
-    val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort;
+    val has_inst = Sorts.has_instance algebra ext_tyco sort;
   in
     if has_inst then thy
     else
diff -r b28defd0b5a5 -r db75b4005d9a src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Mon Jul 16 15:57:21 2012 +0200
+++ b/src/HOL/Typerep.thy	Mon Jul 16 21:20:56 2012 +0200
@@ -64,8 +64,8 @@
   end;
 
 fun ensure_typerep tyco thy =
-  if not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep})
-    andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort type}
+  if not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep})
+    andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort type}
   then add_typerep tyco thy else thy;
 
 in
diff -r b28defd0b5a5 -r db75b4005d9a src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Jul 16 15:57:21 2012 +0200
+++ b/src/Pure/sorts.ML	Mon Jul 16 21:20:56 2012 +0200
@@ -48,6 +48,7 @@
   type class_error
   val class_error: Context.pretty -> class_error -> string
   exception CLASS_ERROR of class_error
+  val has_instance: algebra -> string -> sort -> bool
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   val meet_sort: algebra -> typ * sort
     -> sort Vartab.table -> sort Vartab.table   (*exception CLASS_ERROR*)
@@ -337,13 +338,16 @@
 exception CLASS_ERROR of class_error;
 
 
-(* mg_domain *)
+(* instances *)
+
+fun has_instance algebra a =
+  forall (AList.defined (op =) (Symtab.lookup_list (arities_of algebra) a));
 
 fun mg_domain algebra a S =
   let
-    val arities = arities_of algebra;
+    val ars = Symtab.lookup_list (arities_of algebra) a;
     fun dom c =
-      (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
+      (case AList.lookup (op =) ars c of
         NONE => raise CLASS_ERROR (No_Arity (a, c))
       | SOME Ss => Ss);
     fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);