2956
|
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
|
3633
|
12 |
val str_of_classrel: class * class -> string
|
2956
|
13 |
val str_of_sort: sort -> string
|
|
14 |
val str_of_arity: string * sort list * sort -> string
|
|
15 |
val class_eq: classrel -> class * class -> bool
|
|
16 |
val class_less: classrel -> class * class -> bool
|
|
17 |
val class_le: classrel -> class * class -> bool
|
|
18 |
val sort_eq: classrel -> sort * sort -> bool
|
|
19 |
val sort_less: classrel -> sort * sort -> bool
|
|
20 |
val sort_le: classrel -> sort * sort -> bool
|
|
21 |
val sorts_le: classrel -> sort list * sort list -> bool
|
|
22 |
val inter_class: classrel -> class * sort -> sort
|
|
23 |
val inter_sort: classrel -> sort * sort -> sort
|
|
24 |
val norm_sort: classrel -> sort -> sort
|
7643
|
25 |
val of_sort: classrel * arities -> typ * sort -> bool
|
|
26 |
exception DOMAIN of string * class
|
|
27 |
val mg_domain: classrel * arities -> string -> sort -> sort list
|
|
28 |
val witness_sorts: classrel * arities * string list
|
|
29 |
-> sort list -> sort list -> (typ * sort) list
|
2956
|
30 |
end;
|
|
31 |
|
|
32 |
structure Sorts: SORTS =
|
|
33 |
struct
|
|
34 |
|
|
35 |
|
|
36 |
(** type classes and sorts **)
|
|
37 |
|
|
38 |
(*
|
|
39 |
Classes denote (possibly empty) collections of types that are
|
|
40 |
partially ordered by class inclusion. They are represented
|
|
41 |
symbolically by strings.
|
|
42 |
|
|
43 |
Sorts are intersections of finitely many classes. They are
|
|
44 |
represented by lists of classes. Normal forms of sorts are sorted
|
|
45 |
lists of minimal classes (wrt. current class inclusion).
|
|
46 |
|
|
47 |
(already defined in Pure/term.ML)
|
|
48 |
*)
|
|
49 |
|
|
50 |
|
|
51 |
(* sort signature information *)
|
|
52 |
|
|
53 |
(*
|
|
54 |
classrel:
|
7067
|
55 |
table representing the proper subclass relation; entries (c, cs)
|
|
56 |
represent the superclasses cs of c;
|
2956
|
57 |
|
|
58 |
arities:
|
7067
|
59 |
table of association lists of all type arities; (t, ars) means
|
2956
|
60 |
that type constructor t has the arities ars; an element (c, Ss) of
|
7067
|
61 |
ars represents the arity t::(Ss)c;
|
2956
|
62 |
*)
|
|
63 |
|
7067
|
64 |
type classrel = (class list) Symtab.table;
|
|
65 |
type arities = ((class * sort list) list) Symtab.table;
|
2956
|
66 |
|
|
67 |
|
|
68 |
(* print sorts and arities *)
|
|
69 |
|
3783
|
70 |
val str_of_sort = Syntax.simple_str_of_sort;
|
|
71 |
fun str_of_classrel (c1, c2) = str_of_sort [c1] ^ " < " ^ str_of_sort [c2];
|
2956
|
72 |
fun str_of_dom Ss = enclose "(" ")" (commas (map str_of_sort Ss));
|
|
73 |
|
|
74 |
fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
|
|
75 |
| str_of_arity (t, Ss, S) =
|
|
76 |
t ^ " :: " ^ str_of_dom Ss ^ " " ^ str_of_sort S;
|
|
77 |
|
|
78 |
|
|
79 |
|
|
80 |
(** equality and inclusion **)
|
|
81 |
|
|
82 |
(* classes *)
|
|
83 |
|
|
84 |
fun class_eq _ (c1, c2:class) = c1 = c2;
|
|
85 |
|
|
86 |
fun class_less classrel (c1, c2) =
|
7067
|
87 |
(case Symtab.lookup (classrel, c1) of
|
2956
|
88 |
Some cs => c2 mem_string cs
|
|
89 |
| None => false);
|
|
90 |
|
|
91 |
fun class_le classrel (c1, c2) =
|
|
92 |
c1 = c2 orelse class_less classrel (c1, c2);
|
|
93 |
|
|
94 |
|
|
95 |
(* sorts *)
|
|
96 |
|
|
97 |
fun sort_le classrel (S1, S2) =
|
|
98 |
forall (fn c2 => exists (fn c1 => class_le classrel (c1, c2)) S1) S2;
|
|
99 |
|
|
100 |
fun sorts_le classrel (Ss1, Ss2) =
|
|
101 |
ListPair.all (sort_le classrel) (Ss1, Ss2);
|
|
102 |
|
|
103 |
fun sort_eq classrel (S1, S2) =
|
|
104 |
sort_le classrel (S1, S2) andalso sort_le classrel (S2, S1);
|
|
105 |
|
|
106 |
fun sort_less classrel (S1, S2) =
|
|
107 |
sort_le classrel (S1, S2) andalso not (sort_le classrel (S2, S1));
|
|
108 |
|
|
109 |
|
|
110 |
(* normal forms of sorts *)
|
|
111 |
|
|
112 |
fun minimal_class classrel S c =
|
|
113 |
not (exists (fn c' => class_less classrel (c', c)) S);
|
|
114 |
|
|
115 |
fun norm_sort classrel S =
|
|
116 |
sort_strings (distinct (filter (minimal_class classrel S) S));
|
|
117 |
|
|
118 |
|
|
119 |
|
|
120 |
(** intersection **)
|
|
121 |
|
7643
|
122 |
(*intersect class with sort (preserves minimality)*)
|
2956
|
123 |
fun inter_class classrel (c, S) =
|
|
124 |
let
|
|
125 |
fun intr [] = [c]
|
|
126 |
| intr (S' as c' :: c's) =
|
|
127 |
if class_le classrel (c', c) then S'
|
|
128 |
else if class_le classrel (c, c') then intr c's
|
|
129 |
else c' :: intr c's
|
|
130 |
in intr S end;
|
|
131 |
|
|
132 |
(*instersect sorts (preserves minimality)*)
|
|
133 |
fun inter_sort classrel = foldr (inter_class classrel);
|
|
134 |
|
|
135 |
|
|
136 |
|
|
137 |
(** sorts of types **)
|
|
138 |
|
7643
|
139 |
(* mg_domain *)
|
|
140 |
|
|
141 |
exception DOMAIN of string * class;
|
2956
|
142 |
|
|
143 |
fun mg_dom arities a c =
|
7643
|
144 |
(case Symtab.lookup (arities, a) of
|
|
145 |
None => raise DOMAIN (a, c)
|
|
146 |
| Some ars => (case assoc (ars, c) of None => raise DOMAIN (a, c) | Some Ss => Ss));
|
2956
|
147 |
|
7643
|
148 |
fun mg_domain _ _ [] = sys_error "mg_domain" (*don't know number of args!*)
|
|
149 |
| mg_domain (classrel, arities) a S =
|
2956
|
150 |
let val doms = map (mg_dom arities a) S in
|
|
151 |
foldl (ListPair.map (inter_sort classrel)) (hd doms, tl doms)
|
|
152 |
end;
|
|
153 |
|
|
154 |
|
2990
|
155 |
(* of_sort *)
|
|
156 |
|
7643
|
157 |
fun of_sort (classrel, arities) =
|
2990
|
158 |
let
|
|
159 |
fun ofS (_, []) = true
|
|
160 |
| ofS (TFree (_, S), S') = sort_le classrel (S, S')
|
|
161 |
| ofS (TVar (_, S), S') = sort_le classrel (S, S')
|
|
162 |
| ofS (Type (a, Ts), S) =
|
7643
|
163 |
let val Ss = mg_domain (classrel, arities) a S in
|
2990
|
164 |
ListPair.all ofS (Ts, Ss)
|
7643
|
165 |
end handle DOMAIN _ => false;
|
2990
|
166 |
in ofS end;
|
|
167 |
|
|
168 |
|
2956
|
169 |
|
7643
|
170 |
(** witness_sorts **)
|
|
171 |
|
|
172 |
fun witness_sorts_aux (classrel, arities, log_types) hyps sorts =
|
|
173 |
let
|
|
174 |
val top_witn = (propT, []);
|
|
175 |
fun le S1 S2 = sort_le classrel (S1, S2);
|
|
176 |
fun get_solved S2 (T, S1) = if le S1 S2 then Some (T, S2) else None;
|
|
177 |
fun get_hyp S2 S1 = if le S1 S2 then Some (TFree ("'hyp", S1), S2) else None;
|
|
178 |
fun mg_dom t S = Some (mg_domain (classrel, arities) t S) handle DOMAIN _ => None;
|
|
179 |
|
|
180 |
fun witn_sort _ (solved_failed, []) = (solved_failed, Some top_witn)
|
|
181 |
| witn_sort path ((solved, failed), S) =
|
|
182 |
if exists (le S) failed then ((solved, failed), None)
|
|
183 |
else
|
|
184 |
(case get_first (get_solved S) solved of
|
|
185 |
Some w => ((solved, failed), Some w)
|
|
186 |
| None =>
|
|
187 |
(case get_first (get_hyp S) hyps of
|
|
188 |
Some w => ((w :: solved, failed), Some w)
|
|
189 |
| None => witn_types path log_types ((solved, failed), S)))
|
|
190 |
|
|
191 |
and witn_sorts path x = foldl_map (witn_sort path) x
|
2956
|
192 |
|
7643
|
193 |
and witn_types _ [] ((solved, failed), S) = ((solved, S :: failed), None)
|
|
194 |
| witn_types path (t :: ts) (solved_failed, S) =
|
|
195 |
(case mg_dom t S of
|
|
196 |
Some SS =>
|
|
197 |
(*do not descend into stronger args (achieving termination)*)
|
|
198 |
if exists (fn D => le D S orelse exists (le D) path) SS then
|
|
199 |
witn_types path ts (solved_failed, S)
|
|
200 |
else
|
|
201 |
let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
|
|
202 |
if forall is_some ws then
|
|
203 |
let val w = (Type (t, map (#1 o the) ws), S)
|
|
204 |
in ((w :: solved', failed'), Some w) end
|
|
205 |
else witn_types path ts ((solved', failed'), S)
|
|
206 |
end
|
|
207 |
| None => witn_types path ts (solved_failed, S));
|
|
208 |
|
|
209 |
in witn_sorts [] (([], []), sorts) end;
|
|
210 |
|
|
211 |
|
|
212 |
fun witness_sorts (classrel, arities, log_types) hyps sorts =
|
|
213 |
let
|
|
214 |
fun check_result None = None
|
|
215 |
| check_result (Some (T, S)) =
|
|
216 |
if of_sort (classrel, arities) (T, S) then Some (T, S)
|
|
217 |
else (warning ("witness_sorts: rejected bad witness for " ^ str_of_sort S); None);
|
|
218 |
in mapfilter check_result (#2 (witness_sorts_aux (classrel, arities, log_types) hyps sorts)) end;
|
|
219 |
|
2956
|
220 |
|
|
221 |
end;
|