|
1 (* Title: Pure/sorts.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
|
4 |
|
5 Type classes and sorts. |
|
6 *) |
|
7 |
|
8 signature SORTS = |
|
9 sig |
|
10 type classrel |
|
11 type arities |
|
12 val str_of_sort: sort -> string |
|
13 val str_of_arity: string * sort list * sort -> string |
|
14 val class_eq: classrel -> class * class -> bool |
|
15 val class_less: classrel -> class * class -> bool |
|
16 val class_le: classrel -> class * class -> bool |
|
17 val sort_eq: classrel -> sort * sort -> bool |
|
18 val sort_less: classrel -> sort * sort -> bool |
|
19 val sort_le: classrel -> sort * sort -> bool |
|
20 val sorts_le: classrel -> sort list * sort list -> bool |
|
21 val inter_class: classrel -> class * sort -> sort |
|
22 val inter_sort: classrel -> sort * sort -> sort |
|
23 val norm_sort: classrel -> sort -> sort |
|
24 val least_sort: classrel -> arities -> typ -> sort |
|
25 val mg_domain: classrel -> arities -> string -> sort -> sort list |
|
26 val nonempty_sort: classrel -> arities -> sort list -> sort -> bool |
|
27 end; |
|
28 |
|
29 structure Sorts: SORTS = |
|
30 struct |
|
31 |
|
32 |
|
33 (** type classes and sorts **) |
|
34 |
|
35 (* |
|
36 Classes denote (possibly empty) collections of types that are |
|
37 partially ordered by class inclusion. They are represented |
|
38 symbolically by strings. |
|
39 |
|
40 Sorts are intersections of finitely many classes. They are |
|
41 represented by lists of classes. Normal forms of sorts are sorted |
|
42 lists of minimal classes (wrt. current class inclusion). |
|
43 |
|
44 (already defined in Pure/term.ML) |
|
45 *) |
|
46 |
|
47 |
|
48 (* sort signature information *) |
|
49 |
|
50 (* |
|
51 classrel: |
|
52 association list representing the proper subclass relation; |
|
53 pairs (c, cs) represent the superclasses cs of c; |
|
54 |
|
55 arities: |
|
56 two-fold association list of all type arities; (t, ars) means |
|
57 that type constructor t has the arities ars; an element (c, Ss) of |
|
58 ars represents the arity t::(Ss)c. |
|
59 *) |
|
60 |
|
61 type classrel = (class * class list) list; |
|
62 type arities = (string * (class * sort list) list) list; |
|
63 |
|
64 |
|
65 (* print sorts and arities *) |
|
66 |
|
67 fun str_of_sort [c] = c |
|
68 | str_of_sort cs = enclose "{" "}" (commas cs); |
|
69 |
|
70 fun str_of_dom Ss = enclose "(" ")" (commas (map str_of_sort Ss)); |
|
71 |
|
72 fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S |
|
73 | str_of_arity (t, Ss, S) = |
|
74 t ^ " :: " ^ str_of_dom Ss ^ " " ^ str_of_sort S; |
|
75 |
|
76 |
|
77 |
|
78 (** equality and inclusion **) |
|
79 |
|
80 (* classes *) |
|
81 |
|
82 fun class_eq _ (c1, c2:class) = c1 = c2; |
|
83 |
|
84 fun class_less classrel (c1, c2) = |
|
85 (case assoc (classrel, c1) of |
|
86 Some cs => c2 mem_string cs |
|
87 | None => false); |
|
88 |
|
89 fun class_le classrel (c1, c2) = |
|
90 c1 = c2 orelse class_less classrel (c1, c2); |
|
91 |
|
92 |
|
93 (* sorts *) |
|
94 |
|
95 fun sort_le classrel (S1, S2) = |
|
96 forall (fn c2 => exists (fn c1 => class_le classrel (c1, c2)) S1) S2; |
|
97 |
|
98 fun sorts_le classrel (Ss1, Ss2) = |
|
99 ListPair.all (sort_le classrel) (Ss1, Ss2); |
|
100 |
|
101 fun sort_eq classrel (S1, S2) = |
|
102 sort_le classrel (S1, S2) andalso sort_le classrel (S2, S1); |
|
103 |
|
104 fun sort_less classrel (S1, S2) = |
|
105 sort_le classrel (S1, S2) andalso not (sort_le classrel (S2, S1)); |
|
106 |
|
107 |
|
108 (* normal forms of sorts *) |
|
109 |
|
110 fun minimal_class classrel S c = |
|
111 not (exists (fn c' => class_less classrel (c', c)) S); |
|
112 |
|
113 fun norm_sort classrel S = |
|
114 sort_strings (distinct (filter (minimal_class classrel S) S)); |
|
115 |
|
116 |
|
117 |
|
118 (** intersection **) |
|
119 |
|
120 (*intersect class with sort (preserves minimality)*) (* FIXME tune? *) |
|
121 fun inter_class classrel (c, S) = |
|
122 let |
|
123 fun intr [] = [c] |
|
124 | intr (S' as c' :: c's) = |
|
125 if class_le classrel (c', c) then S' |
|
126 else if class_le classrel (c, c') then intr c's |
|
127 else c' :: intr c's |
|
128 in intr S end; |
|
129 |
|
130 (*instersect sorts (preserves minimality)*) |
|
131 fun inter_sort classrel = foldr (inter_class classrel); |
|
132 |
|
133 |
|
134 |
|
135 (** sorts of types **) |
|
136 |
|
137 (* least_sort *) |
|
138 |
|
139 fun least_sort classrel arities T = |
|
140 let |
|
141 fun match_dom Ss (c, Ss') = |
|
142 if sorts_le classrel (Ss, Ss') then Some c |
|
143 else None; |
|
144 |
|
145 fun leastS (Type (a, Ts)) = |
|
146 norm_sort classrel |
|
147 (mapfilter (match_dom (map leastS Ts)) (assocs arities a)) |
|
148 | leastS (TFree (_, S)) = S |
|
149 | leastS (TVar (_, S)) = S |
|
150 in leastS T end; |
|
151 |
|
152 |
|
153 (* mg_domain *) (*exception TYPE*) |
|
154 |
|
155 fun mg_dom arities a c = |
|
156 (case assoc2 (arities, (a, c)) of |
|
157 None => raise_type ("No way to get " ^ a ^ "::" ^ c ^ ".") [] [] |
|
158 | Some Ss => Ss); |
|
159 |
|
160 fun mg_domain _ _ _ [] = sys_error "mg_domain" (*don't know number of args!*) |
|
161 | mg_domain classrel arities a S = |
|
162 let val doms = map (mg_dom arities a) S in |
|
163 foldl (ListPair.map (inter_sort classrel)) (hd doms, tl doms) |
|
164 end; |
|
165 |
|
166 |
|
167 |
|
168 (** nonempty_sort **) |
|
169 |
|
170 (* FIXME improve: proper sorts; non-base, non-ground types (vars from hyps) *) |
|
171 fun nonempty_sort classrel _ _ [] = true |
|
172 | nonempty_sort classrel arities hyps S = |
|
173 exists (exists (fn (c, Ss) => [c] = S andalso null Ss) o snd) arities |
|
174 orelse exists (fn S' => sort_le classrel (S', S)) hyps; |
|
175 |
|
176 end; |