src/Pure/sorts.ML
changeset 17155 e904580c3ee0
parent 16881 570592642670
child 17184 3d80209e9a53
     1.1 --- a/src/Pure/sorts.ML	Sun Aug 28 09:26:22 2005 +0200
     1.2 +++ b/src/Pure/sorts.ML	Sun Aug 28 09:36:18 2005 +0200
     1.3 @@ -22,6 +22,8 @@
     1.4    val class_eq: classes -> class * class -> bool
     1.5    val class_less: classes -> class * class -> bool
     1.6    val class_le: classes -> class * class -> bool
     1.7 +  val class_le_path: classes -> class * class -> class list option
     1.8 +  val superclasses: classes -> class -> class list
     1.9    val sort_eq: classes -> sort * sort -> bool
    1.10    val sort_less: classes -> sort * sort -> bool
    1.11    val sort_le: classes -> sort * sort -> bool
    1.12 @@ -106,11 +108,20 @@
    1.13  val class_less: classes -> class * class -> bool = Graph.is_edge;
    1.14  fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2);
    1.15  
    1.16 +fun class_le_path classes (subclass, superclass) =
    1.17 +  if class_eq classes (subclass, superclass)
    1.18 +  then SOME [subclass]
    1.19 +  else case Graph.find_paths classes (subclass, superclass)
    1.20 +    of [] => NONE
    1.21 +     | (p::_) => SOME p
    1.22 +
    1.23 +val superclasses = Graph.imm_succs
    1.24 +
    1.25  
    1.26  (* sorts *)
    1.27  
    1.28  fun sort_le classes (S1, S2) =
    1.29 -  forall (fn c2 => exists  (fn c1 => class_le classes (c1, c2)) S1) S2;
    1.30 +  forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2;
    1.31  
    1.32  fun sorts_le classes (Ss1, Ss2) =
    1.33    ListPair.all (sort_le classes) (Ss1, Ss2);