# HG changeset patch
# User wenzelm
# Date 1269548824 -3600
# Node ID 00e48e1d9afd867155e46ed17102e52442c0cd68
# Parent  536c07a2a0bc120625ec80f10cf1bf03ca3444b8
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed  (SUBTLE CHANGE IN SEMANTICS);
officially export weaken as Sorts.classrel_derivation;
tuned comments;

diff -r 536c07a2a0bc -r 00e48e1d9afd src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Mar 25 21:14:15 2010 +0100
+++ b/src/Pure/axclass.ML	Thu Mar 25 21:27:04 2010 +0100
@@ -187,7 +187,7 @@
       Sign.super_classes thy c
       |> filter_out (fn c1 => exists (fn ((c2, Ss2), _) => c1 = c2
           andalso Sorts.sorts_le algebra (Ss2, Ss)) (Symtab.lookup_list arities t));
-    val completions = map (fn c1 => (Sorts.weaken algebra
+    val completions = map (fn c1 => (Sorts.classrel_derivation algebra
       (fn (th, c2) => fn c3 => th RS the_classrel thy (c2, c3)) (th, c) c1
         |> Thm.close_derivation, c1)) super_class_completions;
     val arities' = fold (fn (th1, c1) => Symtab.cons_list (t, ((c1, Ss), (th1, thy_name))))
diff -r 536c07a2a0bc -r 00e48e1d9afd src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Thu Mar 25 21:14:15 2010 +0100
+++ b/src/Pure/sorts.ML	Thu Mar 25 21:27:04 2010 +0100
@@ -56,12 +56,13 @@
     -> sort Vartab.table -> sort Vartab.table   (*exception CLASS_ERROR*)
   val meet_sort_typ: algebra -> typ * sort -> typ -> typ   (*exception CLASS_ERROR*)
   val of_sort: algebra -> typ * sort -> bool
-  val weaken: algebra -> ('a * class -> class -> 'a) -> 'a * class -> class -> 'a
   val of_sort_derivation: algebra ->
     {class_relation: 'a * class -> class -> 'a,
      type_constructor: string -> ('a * class) list list -> class -> 'a,
      type_variable: typ -> ('a * class) list} ->
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
+  val classrel_derivation: algebra ->
+    ('a * class -> class -> 'a) -> 'a * class -> class -> 'a  (*exception CLASS_ERROR*)
   val witness_sorts: algebra -> string list -> (typ * sort) list -> sort list -> (typ * sort) list
 end;
 
@@ -317,7 +318,7 @@
 
 (** sorts of types **)
 
-(* errors -- delayed message composition *)
+(* errors -- performance tuning via delayed message composition *)
 
 datatype class_error =
   NoClassrel of class * class |
@@ -391,24 +392,13 @@
 
 (* animating derivations *)
 
-fun weaken algebra class_relation =
-  let
-    fun path (x, c1 :: c2 :: cs) = path (class_relation (x, c1) c2, c2 :: cs)
-      | path (x, _) = x;
-  in fn (x, c1) => fn c2 =>
-    (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
-      [] => raise CLASS_ERROR (NoClassrel (c1, c2))
-    | cs :: _ => path (x, cs))
-  end;
-
 fun of_sort_derivation algebra {class_relation, type_constructor, type_variable} =
   let
-    val weaken = weaken algebra class_relation;
     val arities = arities_of algebra;
 
-    fun weakens S1 S2 = S2 |> map (fn c2 =>
+    fun weaken S1 S2 = S2 |> map (fn c2 =>
       (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
-        SOME d1 => weaken d1 c2
+        SOME d1 => class_relation d1 c2
       | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
 
     fun derive _ [] = []
@@ -420,12 +410,23 @@
             S |> map (fn c =>
               let
                 val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
-                val dom' = map2 (fn d => fn S' => weakens d S' ~~ S') dom Ss';
-              in weaken (type_constructor a dom' c0, c0) c end)
+                val dom' = map2 (fn d => fn S' => weaken d S' ~~ S') dom Ss';
+              in class_relation (type_constructor a dom' c0, c0) c end)
           end
-      | derive T S = weakens (type_variable T) S;
+      | derive T S = weaken (type_variable T) S;
   in uncurry derive end;
 
+fun classrel_derivation algebra class_relation =
+  let
+    fun path (x, c1 :: c2 :: cs) = path (class_relation (x, c1) c2, c2 :: cs)
+      | path (x, _) = x;
+  in
+    fn (x, c1) => fn c2 =>
+      (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
+        [] => raise CLASS_ERROR (NoClassrel (c1, c2))
+      | cs :: _ => path (x, cs))
+  end;
+
 
 (* witness_sorts *)
 
diff -r 536c07a2a0bc -r 00e48e1d9afd src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Mar 25 21:14:15 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML	Thu Mar 25 21:27:04 2010 +0100
@@ -774,7 +774,8 @@
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
     val typargs = Sorts.of_sort_derivation algebra
-      {class_relation = class_relation, type_constructor = type_constructor,
+      {class_relation = Sorts.classrel_derivation algebra class_relation,
+       type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
       handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;
     fun mk_dict (Global (inst, yss)) =