20 type classes |
20 type classes |
21 type arities |
21 type arities |
22 val class_eq: classes -> class * class -> bool |
22 val class_eq: classes -> class * class -> bool |
23 val class_less: classes -> class * class -> bool |
23 val class_less: classes -> class * class -> bool |
24 val class_le: classes -> class * class -> bool |
24 val class_le: classes -> class * class -> bool |
|
25 val class_le_path: classes -> class * class -> class list option |
|
26 val superclasses: classes -> class -> class list |
25 val sort_eq: classes -> sort * sort -> bool |
27 val sort_eq: classes -> sort * sort -> bool |
26 val sort_less: classes -> sort * sort -> bool |
28 val sort_less: classes -> sort * sort -> bool |
27 val sort_le: classes -> sort * sort -> bool |
29 val sort_le: classes -> sort * sort -> bool |
28 val sorts_le: classes -> sort list * sort list -> bool |
30 val sorts_le: classes -> sort list * sort list -> bool |
29 val inter_sort: classes -> sort * sort -> sort |
31 val inter_sort: classes -> sort * sort -> sort |
104 |
106 |
105 fun class_eq (_: classes) (c1, c2:class) = c1 = c2; |
107 fun class_eq (_: classes) (c1, c2:class) = c1 = c2; |
106 val class_less: classes -> class * class -> bool = Graph.is_edge; |
108 val class_less: classes -> class * class -> bool = Graph.is_edge; |
107 fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2); |
109 fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2); |
108 |
110 |
|
111 fun class_le_path classes (subclass, superclass) = |
|
112 if class_eq classes (subclass, superclass) |
|
113 then SOME [subclass] |
|
114 else case Graph.find_paths classes (subclass, superclass) |
|
115 of [] => NONE |
|
116 | (p::_) => SOME p |
|
117 |
|
118 val superclasses = Graph.imm_succs |
|
119 |
109 |
120 |
110 (* sorts *) |
121 (* sorts *) |
111 |
122 |
112 fun sort_le classes (S1, S2) = |
123 fun sort_le classes (S1, S2) = |
113 forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2; |
124 forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2; |
114 |
125 |
115 fun sorts_le classes (Ss1, Ss2) = |
126 fun sorts_le classes (Ss1, Ss2) = |
116 ListPair.all (sort_le classes) (Ss1, Ss2); |
127 ListPair.all (sort_le classes) (Ss1, Ss2); |
117 |
128 |
118 fun sort_eq classes (S1, S2) = |
129 fun sort_eq classes (S1, S2) = |