wenzelm@2956
|
1 |
(* Title: Pure/sorts.ML
|
wenzelm@2956
|
2 |
ID: $Id$
|
wenzelm@2956
|
3 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
|
wenzelm@2956
|
4 |
|
wenzelm@2956
|
5 |
Type classes and sorts.
|
wenzelm@2956
|
6 |
*)
|
wenzelm@2956
|
7 |
|
wenzelm@2956
|
8 |
signature SORTS =
|
wenzelm@2956
|
9 |
sig
|
wenzelm@16598
|
10 |
(*operations on ordered lists*)
|
wenzelm@16598
|
11 |
val eq_set: sort list * sort list -> bool
|
wenzelm@16598
|
12 |
val union: sort list -> sort list -> sort list
|
wenzelm@16598
|
13 |
val subtract: sort list -> sort list -> sort list
|
wenzelm@16598
|
14 |
val insert_sort: sort -> sort list -> sort list
|
wenzelm@16598
|
15 |
val insert_typ: typ -> sort list -> sort list
|
wenzelm@16598
|
16 |
val insert_typs: typ list -> sort list -> sort list
|
wenzelm@16598
|
17 |
val insert_term: term -> sort list -> sort list
|
wenzelm@16598
|
18 |
val insert_terms: term list -> sort list -> sort list
|
wenzelm@16598
|
19 |
(*signature information*)
|
wenzelm@14782
|
20 |
type classes
|
wenzelm@14782
|
21 |
type arities
|
wenzelm@14782
|
22 |
val class_eq: classes -> class * class -> bool
|
wenzelm@14782
|
23 |
val class_less: classes -> class * class -> bool
|
wenzelm@14782
|
24 |
val class_le: classes -> class * class -> bool
|
haftmann@17155
|
25 |
val class_le_path: classes -> class * class -> class list option
|
haftmann@17155
|
26 |
val superclasses: classes -> class -> class list
|
wenzelm@14782
|
27 |
val sort_eq: classes -> sort * sort -> bool
|
wenzelm@14782
|
28 |
val sort_less: classes -> sort * sort -> bool
|
wenzelm@14782
|
29 |
val sort_le: classes -> sort * sort -> bool
|
wenzelm@14782
|
30 |
val sorts_le: classes -> sort list * sort list -> bool
|
wenzelm@14782
|
31 |
val inter_sort: classes -> sort * sort -> sort
|
wenzelm@14782
|
32 |
val norm_sort: classes -> sort -> sort
|
wenzelm@14986
|
33 |
val certify_class: classes -> class -> class
|
wenzelm@14986
|
34 |
val certify_sort: classes -> sort -> sort
|
wenzelm@14782
|
35 |
val of_sort: classes * arities -> typ * sort -> bool
|
wenzelm@7643
|
36 |
exception DOMAIN of string * class
|
wenzelm@14782
|
37 |
val mg_domain: classes * arities -> string -> sort -> sort list (*exception DOMAIN*)
|
wenzelm@14828
|
38 |
val witness_sorts: classes * arities -> string list ->
|
wenzelm@14828
|
39 |
sort list -> sort list -> (typ * sort) list
|
wenzelm@2956
|
40 |
end;
|
wenzelm@2956
|
41 |
|
wenzelm@2956
|
42 |
structure Sorts: SORTS =
|
wenzelm@2956
|
43 |
struct
|
wenzelm@2956
|
44 |
|
wenzelm@2956
|
45 |
(** type classes and sorts **)
|
wenzelm@2956
|
46 |
|
wenzelm@2956
|
47 |
(*
|
wenzelm@2956
|
48 |
Classes denote (possibly empty) collections of types that are
|
wenzelm@2956
|
49 |
partially ordered by class inclusion. They are represented
|
wenzelm@2956
|
50 |
symbolically by strings.
|
wenzelm@2956
|
51 |
|
wenzelm@2956
|
52 |
Sorts are intersections of finitely many classes. They are
|
wenzelm@2956
|
53 |
represented by lists of classes. Normal forms of sorts are sorted
|
wenzelm@2956
|
54 |
lists of minimal classes (wrt. current class inclusion).
|
wenzelm@2956
|
55 |
|
wenzelm@14782
|
56 |
(types already defined in Pure/term.ML)
|
wenzelm@2956
|
57 |
*)
|
wenzelm@2956
|
58 |
|
wenzelm@2956
|
59 |
|
wenzelm@16598
|
60 |
(* ordered lists of sorts *)
|
wenzelm@14782
|
61 |
|
wenzelm@16598
|
62 |
val eq_set = OrdList.eq_set Term.sort_ord;
|
wenzelm@16598
|
63 |
val op union = OrdList.union Term.sort_ord;
|
wenzelm@16598
|
64 |
val subtract = OrdList.subtract Term.sort_ord;
|
wenzelm@14782
|
65 |
|
wenzelm@16598
|
66 |
val insert_sort = OrdList.insert Term.sort_ord;
|
wenzelm@14782
|
67 |
|
wenzelm@16598
|
68 |
fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
|
wenzelm@16598
|
69 |
| insert_typ (TVar (_, S)) Ss = insert_sort S Ss
|
wenzelm@16598
|
70 |
| insert_typ (Type (_, Ts)) Ss = insert_typs Ts Ss
|
wenzelm@16598
|
71 |
and insert_typs [] Ss = Ss
|
wenzelm@16598
|
72 |
| insert_typs (T :: Ts) Ss = insert_typs Ts (insert_typ T Ss);
|
wenzelm@14782
|
73 |
|
wenzelm@16598
|
74 |
fun insert_term (Const (_, T)) Ss = insert_typ T Ss
|
wenzelm@16598
|
75 |
| insert_term (Free (_, T)) Ss = insert_typ T Ss
|
wenzelm@16598
|
76 |
| insert_term (Var (_, T)) Ss = insert_typ T Ss
|
wenzelm@16598
|
77 |
| insert_term (Bound _) Ss = Ss
|
wenzelm@16598
|
78 |
| insert_term (Abs (_, T, t)) Ss = insert_term t (insert_typ T Ss)
|
wenzelm@16598
|
79 |
| insert_term (t $ u) Ss = insert_term t (insert_term u Ss);
|
wenzelm@14782
|
80 |
|
wenzelm@16598
|
81 |
fun insert_terms [] Ss = Ss
|
wenzelm@16598
|
82 |
| insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss);
|
wenzelm@14782
|
83 |
|
wenzelm@14782
|
84 |
|
wenzelm@2956
|
85 |
(* sort signature information *)
|
wenzelm@2956
|
86 |
|
wenzelm@2956
|
87 |
(*
|
wenzelm@14782
|
88 |
classes: graph representing class declarations together with proper
|
wenzelm@14782
|
89 |
subclass relation, which needs to be transitive and acyclic.
|
wenzelm@2956
|
90 |
|
wenzelm@14782
|
91 |
arities: table of association lists of all type arities; (t, ars)
|
wenzelm@14782
|
92 |
means that type constructor t has the arities ars; an element (c,
|
wenzelm@14782
|
93 |
Ss) of ars represents the arity t::(Ss)c. "Coregularity" of the
|
wenzelm@14870
|
94 |
arities structure requires that for any two declarations
|
wenzelm@14870
|
95 |
t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2.
|
wenzelm@2956
|
96 |
*)
|
wenzelm@2956
|
97 |
|
wenzelm@14782
|
98 |
type classes = stamp Graph.T;
|
wenzelm@14782
|
99 |
type arities = (class * sort list) list Symtab.table;
|
wenzelm@2956
|
100 |
|
wenzelm@2956
|
101 |
|
wenzelm@2956
|
102 |
|
wenzelm@2956
|
103 |
(** equality and inclusion **)
|
wenzelm@2956
|
104 |
|
wenzelm@2956
|
105 |
(* classes *)
|
wenzelm@2956
|
106 |
|
wenzelm@14782
|
107 |
fun class_eq (_: classes) (c1, c2:class) = c1 = c2;
|
wenzelm@14782
|
108 |
val class_less: classes -> class * class -> bool = Graph.is_edge;
|
wenzelm@14782
|
109 |
fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2);
|
wenzelm@2956
|
110 |
|
haftmann@17155
|
111 |
fun class_le_path classes (subclass, superclass) =
|
haftmann@17155
|
112 |
if class_eq classes (subclass, superclass)
|
haftmann@17155
|
113 |
then SOME [subclass]
|
haftmann@17155
|
114 |
else case Graph.find_paths classes (subclass, superclass)
|
haftmann@17155
|
115 |
of [] => NONE
|
haftmann@17155
|
116 |
| (p::_) => SOME p
|
haftmann@17155
|
117 |
|
haftmann@17155
|
118 |
val superclasses = Graph.imm_succs
|
haftmann@17155
|
119 |
|
wenzelm@2956
|
120 |
|
wenzelm@2956
|
121 |
(* sorts *)
|
wenzelm@2956
|
122 |
|
wenzelm@14782
|
123 |
fun sort_le classes (S1, S2) =
|
haftmann@17155
|
124 |
forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2;
|
wenzelm@2956
|
125 |
|
wenzelm@14782
|
126 |
fun sorts_le classes (Ss1, Ss2) =
|
wenzelm@14782
|
127 |
ListPair.all (sort_le classes) (Ss1, Ss2);
|
wenzelm@2956
|
128 |
|
wenzelm@14782
|
129 |
fun sort_eq classes (S1, S2) =
|
wenzelm@14782
|
130 |
sort_le classes (S1, S2) andalso sort_le classes (S2, S1);
|
wenzelm@2956
|
131 |
|
wenzelm@14782
|
132 |
fun sort_less classes (S1, S2) =
|
wenzelm@14782
|
133 |
sort_le classes (S1, S2) andalso not (sort_le classes (S2, S1));
|
wenzelm@2956
|
134 |
|
wenzelm@2956
|
135 |
|
wenzelm@2956
|
136 |
(* normal forms of sorts *)
|
wenzelm@2956
|
137 |
|
wenzelm@14782
|
138 |
fun minimal_class classes S c =
|
wenzelm@14782
|
139 |
not (exists (fn c' => class_less classes (c', c)) S);
|
wenzelm@2956
|
140 |
|
wenzelm@14986
|
141 |
fun norm_sort _ [] = []
|
wenzelm@14986
|
142 |
| norm_sort _ (S as [_]) = S
|
wenzelm@16881
|
143 |
| norm_sort classes S = unique_strings (sort_strings (filter (minimal_class classes S) S));
|
wenzelm@14986
|
144 |
|
wenzelm@14986
|
145 |
|
wenzelm@14986
|
146 |
(* certify *)
|
wenzelm@14986
|
147 |
|
wenzelm@14986
|
148 |
fun certify_class classes c =
|
wenzelm@14986
|
149 |
if can (Graph.get_node classes) c then c
|
wenzelm@14986
|
150 |
else raise TYPE ("Undeclared class: " ^ quote c, [], []);
|
wenzelm@14986
|
151 |
|
wenzelm@14986
|
152 |
fun certify_sort classes = norm_sort classes o map (certify_class classes);
|
wenzelm@2956
|
153 |
|
wenzelm@2956
|
154 |
|
wenzelm@2956
|
155 |
|
wenzelm@2956
|
156 |
(** intersection **)
|
wenzelm@2956
|
157 |
|
wenzelm@7643
|
158 |
(*intersect class with sort (preserves minimality)*)
|
wenzelm@16881
|
159 |
fun inter_class classes c S =
|
wenzelm@2956
|
160 |
let
|
wenzelm@2956
|
161 |
fun intr [] = [c]
|
wenzelm@2956
|
162 |
| intr (S' as c' :: c's) =
|
wenzelm@14782
|
163 |
if class_le classes (c', c) then S'
|
wenzelm@14782
|
164 |
else if class_le classes (c, c') then intr c's
|
wenzelm@2956
|
165 |
else c' :: intr c's
|
wenzelm@2956
|
166 |
in intr S end;
|
wenzelm@2956
|
167 |
|
wenzelm@2956
|
168 |
(*instersect sorts (preserves minimality)*)
|
wenzelm@16881
|
169 |
fun inter_sort classes (S1, S2) =
|
wenzelm@16881
|
170 |
sort_strings (fold (inter_class classes) S1 S2);
|
wenzelm@2956
|
171 |
|
wenzelm@2956
|
172 |
|
wenzelm@2956
|
173 |
|
wenzelm@2956
|
174 |
(** sorts of types **)
|
wenzelm@2956
|
175 |
|
wenzelm@7643
|
176 |
(* mg_domain *)
|
wenzelm@7643
|
177 |
|
wenzelm@7643
|
178 |
exception DOMAIN of string * class;
|
wenzelm@2956
|
179 |
|
wenzelm@16881
|
180 |
fun mg_domain (classes, arities) a S =
|
wenzelm@16881
|
181 |
let
|
wenzelm@16881
|
182 |
fun dom c =
|
wenzelm@17412
|
183 |
(case AList.lookup (op =) (Symtab.lookup_multi arities a) c of
|
wenzelm@16881
|
184 |
NONE => raise DOMAIN (a, c)
|
wenzelm@16881
|
185 |
| SOME Ss => Ss);
|
wenzelm@16881
|
186 |
fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
|
wenzelm@16881
|
187 |
in
|
wenzelm@16881
|
188 |
(case S of
|
wenzelm@16881
|
189 |
[] => sys_error "mg_domain" (*don't know number of args!*)
|
wenzelm@16881
|
190 |
| c :: cs => fold dom_inter cs (dom c))
|
wenzelm@16881
|
191 |
end;
|
wenzelm@2956
|
192 |
|
wenzelm@2956
|
193 |
|
wenzelm@2990
|
194 |
(* of_sort *)
|
wenzelm@2990
|
195 |
|
wenzelm@14782
|
196 |
fun of_sort (classes, arities) =
|
wenzelm@2990
|
197 |
let
|
wenzelm@2990
|
198 |
fun ofS (_, []) = true
|
wenzelm@14782
|
199 |
| ofS (TFree (_, S), S') = sort_le classes (S, S')
|
wenzelm@14782
|
200 |
| ofS (TVar (_, S), S') = sort_le classes (S, S')
|
wenzelm@2990
|
201 |
| ofS (Type (a, Ts), S) =
|
wenzelm@14782
|
202 |
let val Ss = mg_domain (classes, arities) a S in
|
wenzelm@2990
|
203 |
ListPair.all ofS (Ts, Ss)
|
wenzelm@7643
|
204 |
end handle DOMAIN _ => false;
|
wenzelm@2990
|
205 |
in ofS end;
|
wenzelm@2990
|
206 |
|
wenzelm@2990
|
207 |
|
wenzelm@2956
|
208 |
|
wenzelm@7643
|
209 |
(** witness_sorts **)
|
wenzelm@2956
|
210 |
|
wenzelm@14828
|
211 |
local
|
wenzelm@14828
|
212 |
|
wenzelm@14828
|
213 |
fun witness_aux (classes, arities) log_types hyps sorts =
|
wenzelm@7643
|
214 |
let
|
wenzelm@7643
|
215 |
val top_witn = (propT, []);
|
wenzelm@14782
|
216 |
fun le S1 S2 = sort_le classes (S1, S2);
|
skalberg@15531
|
217 |
fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE;
|
skalberg@15531
|
218 |
fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE;
|
skalberg@15531
|
219 |
fun mg_dom t S = SOME (mg_domain (classes, arities) t S) handle DOMAIN _ => NONE;
|
wenzelm@7643
|
220 |
|
skalberg@15531
|
221 |
fun witn_sort _ (solved_failed, []) = (solved_failed, SOME top_witn)
|
wenzelm@7643
|
222 |
| witn_sort path ((solved, failed), S) =
|
skalberg@15531
|
223 |
if exists (le S) failed then ((solved, failed), NONE)
|
wenzelm@7643
|
224 |
else
|
wenzelm@7643
|
225 |
(case get_first (get_solved S) solved of
|
skalberg@15531
|
226 |
SOME w => ((solved, failed), SOME w)
|
skalberg@15531
|
227 |
| NONE =>
|
wenzelm@7643
|
228 |
(case get_first (get_hyp S) hyps of
|
skalberg@15531
|
229 |
SOME w => ((w :: solved, failed), SOME w)
|
skalberg@15531
|
230 |
| NONE => witn_types path log_types ((solved, failed), S)))
|
wenzelm@7643
|
231 |
|
wenzelm@7643
|
232 |
and witn_sorts path x = foldl_map (witn_sort path) x
|
wenzelm@7643
|
233 |
|
skalberg@15531
|
234 |
and witn_types _ [] ((solved, failed), S) = ((solved, S :: failed), NONE)
|
wenzelm@7643
|
235 |
| witn_types path (t :: ts) (solved_failed, S) =
|
wenzelm@7643
|
236 |
(case mg_dom t S of
|
skalberg@15531
|
237 |
SOME SS =>
|
wenzelm@7643
|
238 |
(*do not descend into stronger args (achieving termination)*)
|
wenzelm@7643
|
239 |
if exists (fn D => le D S orelse exists (le D) path) SS then
|
wenzelm@7643
|
240 |
witn_types path ts (solved_failed, S)
|
wenzelm@7643
|
241 |
else
|
wenzelm@7643
|
242 |
let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
|
wenzelm@17756
|
243 |
if forall is_some ws then
|
skalberg@15570
|
244 |
let val w = (Type (t, map (#1 o valOf) ws), S)
|
skalberg@15531
|
245 |
in ((w :: solved', failed'), SOME w) end
|
wenzelm@7643
|
246 |
else witn_types path ts ((solved', failed'), S)
|
wenzelm@7643
|
247 |
end
|
skalberg@15531
|
248 |
| NONE => witn_types path ts (solved_failed, S));
|
wenzelm@7643
|
249 |
|
wenzelm@7643
|
250 |
in witn_sorts [] (([], []), sorts) end;
|
wenzelm@7643
|
251 |
|
wenzelm@14828
|
252 |
fun str_of_sort [c] = c
|
wenzelm@14828
|
253 |
| str_of_sort cs = enclose "{" "}" (commas cs);
|
wenzelm@14828
|
254 |
|
wenzelm@14828
|
255 |
in
|
wenzelm@7643
|
256 |
|
wenzelm@14782
|
257 |
fun witness_sorts (classes, arities) log_types hyps sorts =
|
wenzelm@7643
|
258 |
let
|
wenzelm@16881
|
259 |
(*double check result of witness construction*)
|
skalberg@15531
|
260 |
fun check_result NONE = NONE
|
skalberg@15531
|
261 |
| check_result (SOME (T, S)) =
|
skalberg@15531
|
262 |
if of_sort (classes, arities) (T, S) then SOME (T, S)
|
wenzelm@14782
|
263 |
else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S);
|
skalberg@15570
|
264 |
in List.mapPartial check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;
|
wenzelm@2956
|
265 |
|
wenzelm@2956
|
266 |
end;
|
wenzelm@14828
|
267 |
|
wenzelm@14828
|
268 |
end;
|