# HG changeset patch
# User haftmann
# Date 1125214578 -7200
# Node ID e904580c3ee0377eadcf98b50d43ad1328f39e5e
# Parent  c18f911f2c9e0e4ce5f4ad8a177774d47ae5a530
added superclasses, class_le_path

diff -r c18f911f2c9e -r e904580c3ee0 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sun Aug 28 09:26:22 2005 +0200
+++ b/src/Pure/sorts.ML	Sun Aug 28 09:36:18 2005 +0200
@@ -22,6 +22,8 @@
   val class_eq: classes -> class * class -> bool
   val class_less: classes -> class * class -> bool
   val class_le: classes -> class * class -> bool
+  val class_le_path: classes -> class * class -> class list option
+  val superclasses: classes -> class -> class list
   val sort_eq: classes -> sort * sort -> bool
   val sort_less: classes -> sort * sort -> bool
   val sort_le: classes -> sort * sort -> bool
@@ -106,11 +108,20 @@
 val class_less: classes -> class * class -> bool = Graph.is_edge;
 fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2);
 
+fun class_le_path classes (subclass, superclass) =
+  if class_eq classes (subclass, superclass)
+  then SOME [subclass]
+  else case Graph.find_paths classes (subclass, superclass)
+    of [] => NONE
+     | (p::_) => SOME p
+
+val superclasses = Graph.imm_succs
+
 
 (* sorts *)
 
 fun sort_le classes (S1, S2) =
-  forall (fn c2 => exists  (fn c1 => class_le classes (c1, c2)) S1) S2;
+  forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2;
 
 fun sorts_le classes (Ss1, Ss2) =
   ListPair.all (sort_le classes) (Ss1, Ss2);