equal
deleted
inserted
replaced
17 type classes |
17 type classes |
18 type arities |
18 type arities |
19 val class_eq: classes -> class * class -> bool |
19 val class_eq: classes -> class * class -> bool |
20 val class_less: classes -> class * class -> bool |
20 val class_less: classes -> class * class -> bool |
21 val class_le: classes -> class * class -> bool |
21 val class_le: classes -> class * class -> bool |
22 val construct_dep: classes -> class * class list -> class list * class |
|
23 val sort_eq: classes -> sort * sort -> bool |
22 val sort_eq: classes -> sort * sort -> bool |
24 val sort_less: classes -> sort * sort -> bool |
23 val sort_less: classes -> sort * sort -> bool |
25 val sort_le: classes -> sort * sort -> bool |
24 val sort_le: classes -> sort * sort -> bool |
26 val sorts_le: classes -> sort list * sort list -> bool |
25 val sorts_le: classes -> sort list * sort list -> bool |
27 val inter_class: classes -> class * sort -> sort |
26 val inter_class: classes -> class * sort -> sort |
102 |
101 |
103 fun class_eq (_: classes) (c1, c2:class) = c1 = c2; |
102 fun class_eq (_: classes) (c1, c2:class) = c1 = c2; |
104 val class_less: classes -> class * class -> bool = Graph.is_edge; |
103 val class_less: classes -> class * class -> bool = Graph.is_edge; |
105 fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2); |
104 fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2); |
106 |
105 |
107 fun construct_dep classes (subc, supercs) = |
|
108 (hd o Library.flat) (map (fn superc => |
|
109 map (fn path => (path, superc)) (Graph.find_paths classes (subc, superc)) |
|
110 ) supercs) |
|
111 |
106 |
112 (* sorts *) |
107 (* sorts *) |
113 |
108 |
114 fun sort_le classes (S1, S2) = |
109 fun sort_le classes (S1, S2) = |
115 forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2; |
110 forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2; |