1 (* Title: Pure/sorts.ML
3 Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
5 Type classes and sorts.
10 val eq_sort: sort * sort -> bool
11 val mem_sort: sort * sort list -> bool
12 val subset_sort: sort list * sort list -> bool
13 val eq_set_sort: sort list * sort list -> bool
14 val ins_sort: sort * sort list -> sort list
15 val union_sort: sort list * sort list -> sort list
16 val rems_sort: sort list * sort list -> sort list
19 val class_eq: classes -> class * class -> bool
20 val class_less: classes -> class * class -> bool
21 val class_le: classes -> class * class -> bool
22 val sort_eq: classes -> sort * sort -> bool
23 val sort_less: classes -> sort * sort -> bool
24 val sort_le: classes -> sort * sort -> bool
25 val sorts_le: classes -> sort list * sort list -> bool
26 val inter_class: classes -> class * sort -> sort
27 val inter_sort: classes -> sort * sort -> sort
28 val norm_sort: classes -> sort -> sort
29 val of_sort: classes * arities -> typ * sort -> bool
30 exception DOMAIN of string * class
31 val mg_domain: classes * arities -> string -> sort -> sort list (*exception DOMAIN*)
32 val witness_sorts: classes * arities -> string list ->
33 sort list -> sort list -> (typ * sort) list
36 structure Sorts: SORTS =
39 (** type classes and sorts **)
42 Classes denote (possibly empty) collections of types that are
43 partially ordered by class inclusion. They are represented
44 symbolically by strings.
46 Sorts are intersections of finitely many classes. They are
47 represented by lists of classes. Normal forms of sorts are sorted
48 lists of minimal classes (wrt. current class inclusion).
50 (types already defined in Pure/term.ML)
54 (* equality, membership and insertion of sorts *)
56 fun eq_sort ([]: sort, []) = true
57 | eq_sort ((S1 :: Ss1), (S2 :: Ss2)) = S1 = S2 andalso eq_sort (Ss1, Ss2)
58 | eq_sort (_, _) = false;
60 fun mem_sort (_: sort, []) = false
61 | mem_sort (S, S' :: Ss) = eq_sort (S, S') orelse mem_sort (S, Ss);
63 fun ins_sort (S, Ss) = if mem_sort (S, Ss) then Ss else S :: Ss;
65 fun union_sort (Ss, []) = Ss
66 | union_sort ([], Ss) = Ss
67 | union_sort ((S :: Ss), Ss') = union_sort (Ss, ins_sort (S, Ss'));
69 fun subset_sort ([], Ss) = true
70 | subset_sort (S :: Ss, Ss') = mem_sort (S, Ss') andalso subset_sort (Ss, Ss');
72 fun eq_set_sort (Ss, Ss') =
73 Ss = Ss' orelse (subset_sort (Ss, Ss') andalso subset_sort (Ss', Ss));
75 val rems_sort = gen_rems eq_sort;
78 (* sort signature information *)
81 classes: graph representing class declarations together with proper
82 subclass relation, which needs to be transitive and acyclic.
84 arities: table of association lists of all type arities; (t, ars)
85 means that type constructor t has the arities ars; an element (c,
86 Ss) of ars represents the arity t::(Ss)c. "Coregularity" of the
87 arities structure requires that for any two declarations
88 t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2.
91 type classes = stamp Graph.T;
92 type arities = (class * sort list) list Symtab.table;
96 (** equality and inclusion **)
100 fun class_eq (_: classes) (c1, c2:class) = c1 = c2;
101 val class_less: classes -> class * class -> bool = Graph.is_edge;
102 fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2);
107 fun sort_le classes (S1, S2) =
108 forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2;
110 fun sorts_le classes (Ss1, Ss2) =
111 ListPair.all (sort_le classes) (Ss1, Ss2);
113 fun sort_eq classes (S1, S2) =
114 sort_le classes (S1, S2) andalso sort_le classes (S2, S1);
116 fun sort_less classes (S1, S2) =
117 sort_le classes (S1, S2) andalso not (sort_le classes (S2, S1));
120 (* normal forms of sorts *)
122 fun minimal_class classes S c =
123 not (exists (fn c' => class_less classes (c', c)) S);
125 fun norm_sort classes S =
126 sort_strings (distinct (filter (minimal_class classes S) S));
132 (*intersect class with sort (preserves minimality)*)
133 fun inter_class classes (c, S) =
136 | intr (S' as c' :: c's) =
137 if class_le classes (c', c) then S'
138 else if class_le classes (c, c') then intr c's
142 (*instersect sorts (preserves minimality)*)
143 fun inter_sort classes = sort_strings o foldr (inter_class classes);
147 (** sorts of types **)
151 exception DOMAIN of string * class;
153 fun mg_domain _ _ [] = sys_error "mg_domain" (*don't know number of args!*)
154 | mg_domain (classes, arities) a S =
157 (case Library.assoc_string (Symtab.lookup_multi (arities, a), c) of
158 None => raise DOMAIN (a, c)
160 val doms = map mg_dom S;
161 in foldl (ListPair.map (inter_sort classes)) (hd doms, tl doms) end;
166 fun of_sort (classes, arities) =
168 fun ofS (_, []) = true
169 | ofS (TFree (_, S), S') = sort_le classes (S, S')
170 | ofS (TVar (_, S), S') = sort_le classes (S, S')
171 | ofS (Type (a, Ts), S) =
172 let val Ss = mg_domain (classes, arities) a S in
173 ListPair.all ofS (Ts, Ss)
174 end handle DOMAIN _ => false;
179 (** witness_sorts **)
183 fun witness_aux (classes, arities) log_types hyps sorts =
185 val top_witn = (propT, []);
186 fun le S1 S2 = sort_le classes (S1, S2);
187 fun get_solved S2 (T, S1) = if le S1 S2 then Some (T, S2) else None;
188 fun get_hyp S2 S1 = if le S1 S2 then Some (TFree ("'hyp", S1), S2) else None;
189 fun mg_dom t S = Some (mg_domain (classes, arities) t S) handle DOMAIN _ => None;
191 fun witn_sort _ (solved_failed, []) = (solved_failed, Some top_witn)
192 | witn_sort path ((solved, failed), S) =
193 if exists (le S) failed then ((solved, failed), None)
195 (case get_first (get_solved S) solved of
196 Some w => ((solved, failed), Some w)
198 (case get_first (get_hyp S) hyps of
199 Some w => ((w :: solved, failed), Some w)
200 | None => witn_types path log_types ((solved, failed), S)))
202 and witn_sorts path x = foldl_map (witn_sort path) x
204 and witn_types _ [] ((solved, failed), S) = ((solved, S :: failed), None)
205 | witn_types path (t :: ts) (solved_failed, S) =
208 (*do not descend into stronger args (achieving termination)*)
209 if exists (fn D => le D S orelse exists (le D) path) SS then
210 witn_types path ts (solved_failed, S)
212 let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
213 if forall is_some ws then
214 let val w = (Type (t, map (#1 o the) ws), S)
215 in ((w :: solved', failed'), Some w) end
216 else witn_types path ts ((solved', failed'), S)
218 | None => witn_types path ts (solved_failed, S));
220 in witn_sorts [] (([], []), sorts) end;
222 fun str_of_sort [c] = c
223 | str_of_sort cs = enclose "{" "}" (commas cs);
227 fun witness_sorts (classes, arities) log_types hyps sorts =
229 (*double check result of witness search*)
230 fun check_result None = None
231 | check_result (Some (T, S)) =
232 if of_sort (classes, arities) (T, S) then Some (T, S)
233 else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S);
234 in mapfilter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;