# HG changeset patch
# User haftmann
# Date 1207144720 -7200
# Node ID ef036a63f6e9c4e249725b1f8700897892dd446a
# Parent  1bf210ac0a90cc47997f6146c393bd2fcf6f7687
canonical meet_sort operation

diff -r 1bf210ac0a90 -r ef036a63f6e9 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Wed Apr 02 15:58:38 2008 +0200
+++ b/src/Pure/sorts.ML	Wed Apr 02 15:58:40 2008 +0200
@@ -50,10 +50,10 @@
   type class_error
   val msg_class_error: Pretty.pp -> class_error -> string
   val class_error: Pretty.pp -> class_error -> 'a
-  val NoSubsort: sort * sort -> class_error
   exception CLASS_ERROR of class_error
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   val of_sort: algebra -> typ * sort -> bool
+  val meet_sort: algebra -> typ * sort -> sort Vartab.table -> sort Vartab.table
   val of_sort_derivation: Pretty.pp -> algebra ->
     {class_relation: 'a * class -> class -> 'a,
      type_constructor: string -> ('a * class) list list -> class -> 'a,
@@ -355,6 +355,20 @@
   in ofS end;
 
 
+(* meet_sort *)
+
+fun meet_sort algebra =
+  let
+    fun meet _ [] = I
+      | meet (TFree (_, S)) S' = if sort_le algebra (S, S') then I
+          else raise CLASS_ERROR (NoSubsort (S, S'))
+      | meet (TVar (v, S)) S' = if sort_le algebra (S, S') then I
+          else Vartab.map_default (v, S) (curry (inter_sort algebra) S')
+      | meet (Type (a, Ts)) S =
+          fold2 meet Ts (mg_domain algebra a S)
+  in uncurry meet end;
+
+
 (* of_sort_derivation *)
 
 fun of_sort_derivation pp algebra {class_relation, type_constructor, type_variable} =
diff -r 1bf210ac0a90 -r ef036a63f6e9 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Apr 02 15:58:38 2008 +0200
+++ b/src/Pure/type.ML	Wed Apr 02 15:58:40 2008 +0200
@@ -59,8 +59,6 @@
   val lookup: tyenv -> indexname * sort -> typ option
   val typ_match: tsig -> typ * typ -> tyenv -> tyenv
   val typ_instance: tsig -> typ * typ -> bool
-  val typ_of_sort: Sorts.algebra -> typ -> sort
-    -> sort Vartab.table -> sort Vartab.table
   val raw_match: typ * typ -> tyenv -> tyenv
   val raw_matches: typ list * typ list -> tyenv -> tyenv
   val raw_instance: typ * typ -> bool
@@ -349,18 +347,6 @@
 
 exception TYPE_MATCH;
 
-fun typ_of_sort algebra =
-  let
-    val inters = Sorts.inter_sort algebra;
-    fun of_sort _ [] = I
-      | of_sort (TVar (v, S)) S' = Vartab.map_default (v, [])
-          (fn S'' => inters (S, inters (S', S'')))
-      | of_sort (TFree (_, S)) S' = if Sorts.sort_le algebra (S, S') then I
-          else raise Sorts.CLASS_ERROR (Sorts.NoSubsort (S, S'))
-      | of_sort (Type (a, Ts)) S =
-          fold2 of_sort Ts (Sorts.mg_domain algebra a S)
-  in of_sort end;
-
 fun typ_match tsig =
   let
     fun match (TVar (v, S), T) subs =
diff -r 1bf210ac0a90 -r ef036a63f6e9 src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Wed Apr 02 15:58:38 2008 +0200
+++ b/src/Tools/code/code_funcgr.ML	Wed Apr 02 15:58:40 2008 +0200
@@ -76,7 +76,7 @@
       Sorts.of_sort_derivation (Sign.pp thy) algebra
         { class_relation = class_relation, type_constructor = type_constructor,
           type_variable = type_variable }
-        (ty, sort)
+        (ty, sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*)
   in
     flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl []))
   end;
@@ -110,20 +110,18 @@
         val thy = Thm.theory_of_thm thm;
         val pp = Sign.pp thy;
         val cs = fold_consts (insert (op =)) thms [];
-        fun class_error (c, ty_decl) e =
-          error ;
         fun match_const c (ty, ty_decl) =
           let
             val tys = Sign.const_typargs thy (c, ty);
             val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl));
-          in fn tab => fold2 (Type.typ_of_sort algebra) tys sorts tab 
+          in fn tab => fold2 (curry (Sorts.meet_sort algebra)) tys sorts tab
             handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.msg_class_error pp e ^ ",\n"
               ^ "for constant " ^ CodeUnit.string_of_const thy c
               ^ "\nin defining equations(s)\n"
               ^ (cat_lines o map string_of_thm) thms)
+            (*handle Sorts.CLASS_ERROR _ => tab (*permissive!*)*)
           end;
-        fun match (c, ty) =
-          case tap_typ c
+        fun match (c, ty) = case tap_typ c
            of SOME ty_decl => match_const c (ty, ty_decl)
             | NONE => I;
         val tvars = fold match cs Vartab.empty;
@@ -161,7 +159,7 @@
     val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
     fun all_classparams tyco class =
       these (try (#params o AxClass.get_info thy) class)
-      |> map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
+      |> map_filter (fn (c, _) => try (AxClass.param_of_inst thy) (c, tyco))
   in
     Symtab.empty
     |> fold (fn (tyco, class) =>
@@ -173,7 +171,7 @@
 fun instances_of_consts thy algebra funcgr consts =
   let
     fun inst (cexpr as (c, ty)) = insts_of thy algebra c
-      ((fst o Graph.get_node funcgr) c) ty handle Sorts.CLASS_ERROR _ => [];
+      ((fst o Graph.get_node funcgr) c) ty;
   in
     []
     |> fold (fold (insert (op =)) o inst) consts