author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18428  4059413acbc1 
child 18931  427df66052a1 
permissions  rwrr 
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 

16598
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

10 
(*operations on ordered lists*) 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

11 
val eq_set: sort list * sort list > bool 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

12 
val union: sort list > sort list > sort list 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

13 
val subtract: sort list > sort list > sort list 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

14 
val insert_sort: sort > sort list > sort list 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

15 
val insert_typ: typ > sort list > sort list 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

16 
val insert_typs: typ list > sort list > sort list 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

17 
val insert_term: term > sort list > sort list 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

18 
val insert_terms: term list > sort list > sort list 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

19 
(*signature information*) 
14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

20 
type classes 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

21 
type arities 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

22 
val class_eq: classes > class * class > bool 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

23 
val class_less: classes > class * class > bool 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

24 
val class_le: classes > class * class > bool 
17155  25 
val class_le_path: classes > class * class > class list option 
26 
val superclasses: classes > class > class list 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

27 
val sort_eq: classes > sort * sort > bool 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

28 
val sort_less: classes > sort * sort > bool 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

29 
val sort_le: classes > sort * sort > bool 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

30 
val sorts_le: classes > sort list * sort list > bool 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

31 
val inter_sort: classes > sort * sort > sort 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

32 
val norm_sort: classes > sort > sort 
14986  33 
val certify_class: classes > class > class 
34 
val certify_sort: classes > sort > sort 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

35 
val of_sort: classes * arities > typ * sort > bool 
7643  36 
exception DOMAIN of string * class 
14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

37 
val mg_domain: classes * arities > string > sort > sort list (*exception DOMAIN*) 
14828  38 
val witness_sorts: classes * arities > string list > 
39 
sort list > sort list > (typ * sort) list 

2956  40 
end; 
41 

42 
structure Sorts: SORTS = 

43 
struct 

44 

45 
(** type classes and sorts **) 

46 

47 
(* 

48 
Classes denote (possibly empty) collections of types that are 

49 
partially ordered by class inclusion. They are represented 

50 
symbolically by strings. 

51 

52 
Sorts are intersections of finitely many classes. They are 

53 
represented by lists of classes. Normal forms of sorts are sorted 

54 
lists of minimal classes (wrt. current class inclusion). 

55 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

56 
(types already defined in Pure/term.ML) 
2956  57 
*) 
58 

59 

16598
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

60 
(* ordered lists of sorts *) 
14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

61 

16598
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

62 
val eq_set = OrdList.eq_set Term.sort_ord; 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

63 
val op union = OrdList.union Term.sort_ord; 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

64 
val subtract = OrdList.subtract Term.sort_ord; 
14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

65 

16598
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

66 
val insert_sort = OrdList.insert Term.sort_ord; 
14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

67 

16598
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

68 
fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

69 
 insert_typ (TVar (_, S)) Ss = insert_sort S Ss 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

70 
 insert_typ (Type (_, Ts)) Ss = insert_typs Ts Ss 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

71 
and insert_typs [] Ss = Ss 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

72 
 insert_typs (T :: Ts) Ss = insert_typs Ts (insert_typ T Ss); 
14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

73 

16598
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

74 
fun insert_term (Const (_, T)) Ss = insert_typ T Ss 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

75 
 insert_term (Free (_, T)) Ss = insert_typ T Ss 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

76 
 insert_term (Var (_, T)) Ss = insert_typ T Ss 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

77 
 insert_term (Bound _) Ss = Ss 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

78 
 insert_term (Abs (_, T, t)) Ss = insert_term t (insert_typ T Ss) 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

79 
 insert_term (t $ u) Ss = insert_term t (insert_term u Ss); 
14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

80 

16598
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

81 
fun insert_terms [] Ss = Ss 
59381032be14
removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
wenzelm
parents:
16400
diff
changeset

82 
 insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss); 
14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

83 

d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

84 

2956  85 
(* sort signature information *) 
86 

87 
(* 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

88 
classes: graph representing class declarations together with proper 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

89 
subclass relation, which needs to be transitive and acyclic. 
2956  90 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

91 
arities: table of association lists of all type arities; (t, ars) 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

92 
means that type constructor t has the arities ars; an element (c, 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

93 
Ss) of ars represents the arity t::(Ss)c. "Coregularity" of the 
14870  94 
arities structure requires that for any two declarations 
95 
t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2. 

2956  96 
*) 
97 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

98 
type classes = stamp Graph.T; 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

99 
type arities = (class * sort list) list Symtab.table; 
2956  100 

101 

102 

103 
(** equality and inclusion **) 

104 

105 
(* classes *) 

106 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

107 
fun class_eq (_: classes) (c1, c2:class) = c1 = c2; 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

108 
val class_less: classes > class * class > bool = Graph.is_edge; 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

109 
fun class_le classes (c1, c2) = c1 = c2 orelse class_less classes (c1, c2); 
2956  110 

17155  111 
fun class_le_path classes (subclass, superclass) = 
112 
if class_eq classes (subclass, superclass) 

113 
then SOME [subclass] 

114 
else case Graph.find_paths classes (subclass, superclass) 

115 
of [] => NONE 

116 
 (p::_) => SOME p 

117 

118 
val superclasses = Graph.imm_succs 

119 

2956  120 

121 
(* sorts *) 

122 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

123 
fun sort_le classes (S1, S2) = 
17155  124 
forall (fn c2 => exists (fn c1 => class_le classes (c1, c2)) S1) S2; 
2956  125 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

126 
fun sorts_le classes (Ss1, Ss2) = 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

127 
ListPair.all (sort_le classes) (Ss1, Ss2); 
2956  128 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

129 
fun sort_eq classes (S1, S2) = 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

130 
sort_le classes (S1, S2) andalso sort_le classes (S2, S1); 
2956  131 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

132 
fun sort_less classes (S1, S2) = 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

133 
sort_le classes (S1, S2) andalso not (sort_le classes (S2, S1)); 
2956  134 

135 

136 
(* normal forms of sorts *) 

137 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

138 
fun minimal_class classes S c = 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

139 
not (exists (fn c' => class_less classes (c', c)) S); 
2956  140 

14986  141 
fun norm_sort _ [] = [] 
142 
 norm_sort _ (S as [_]) = S 

18428  143 
 norm_sort classes S = sort_distinct string_ord (filter (minimal_class classes S) S); 
14986  144 

145 

146 
(* certify *) 

147 

148 
fun certify_class classes c = 

149 
if can (Graph.get_node classes) c then c 

150 
else raise TYPE ("Undeclared class: " ^ quote c, [], []); 

151 

152 
fun certify_sort classes = norm_sort classes o map (certify_class classes); 

2956  153 

154 

155 

156 
(** intersection **) 

157 

7643  158 
(*intersect class with sort (preserves minimality)*) 
16881  159 
fun inter_class classes c S = 
2956  160 
let 
161 
fun intr [] = [c] 

162 
 intr (S' as c' :: c's) = 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

163 
if class_le classes (c', c) then S' 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

164 
else if class_le classes (c, c') then intr c's 
2956  165 
else c' :: intr c's 
166 
in intr S end; 

167 

168 
(*instersect sorts (preserves minimality)*) 

16881  169 
fun inter_sort classes (S1, S2) = 
170 
sort_strings (fold (inter_class classes) S1 S2); 

2956  171 

172 

173 

174 
(** sorts of types **) 

175 

7643  176 
(* mg_domain *) 
177 

178 
exception DOMAIN of string * class; 

2956  179 

16881  180 
fun mg_domain (classes, arities) a S = 
181 
let 

182 
fun dom c = 

17412  183 
(case AList.lookup (op =) (Symtab.lookup_multi arities a) c of 
16881  184 
NONE => raise DOMAIN (a, c) 
185 
 SOME Ss => Ss); 

186 
fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss); 

187 
in 

188 
(case S of 

189 
[] => sys_error "mg_domain" (*don't know number of args!*) 

190 
 c :: cs => fold dom_inter cs (dom c)) 

191 
end; 

2956  192 

193 

2990  194 
(* of_sort *) 
195 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

196 
fun of_sort (classes, arities) = 
2990  197 
let 
198 
fun ofS (_, []) = true 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

199 
 ofS (TFree (_, S), S') = sort_le classes (S, S') 
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

200 
 ofS (TVar (_, S), S') = sort_le classes (S, S') 
2990  201 
 ofS (Type (a, Ts), S) = 
14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

202 
let val Ss = mg_domain (classes, arities) a S in 
2990  203 
ListPair.all ofS (Ts, Ss) 
7643  204 
end handle DOMAIN _ => false; 
2990  205 
in ofS end; 
206 

207 

2956  208 

7643  209 
(** witness_sorts **) 
210 

14828  211 
local 
212 

213 
fun witness_aux (classes, arities) log_types hyps sorts = 

7643  214 
let 
215 
val top_witn = (propT, []); 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

216 
fun le S1 S2 = sort_le classes (S1, S2); 
15531  217 
fun get_solved S2 (T, S1) = if le S1 S2 then SOME (T, S2) else NONE; 
218 
fun get_hyp S2 S1 = if le S1 S2 then SOME (TFree ("'hyp", S1), S2) else NONE; 

219 
fun mg_dom t S = SOME (mg_domain (classes, arities) t S) handle DOMAIN _ => NONE; 

7643  220 

15531  221 
fun witn_sort _ (solved_failed, []) = (solved_failed, SOME top_witn) 
7643  222 
 witn_sort path ((solved, failed), S) = 
15531  223 
if exists (le S) failed then ((solved, failed), NONE) 
7643  224 
else 
225 
(case get_first (get_solved S) solved of 

15531  226 
SOME w => ((solved, failed), SOME w) 
227 
 NONE => 

7643  228 
(case get_first (get_hyp S) hyps of 
15531  229 
SOME w => ((w :: solved, failed), SOME w) 
230 
 NONE => witn_types path log_types ((solved, failed), S))) 

7643  231 

232 
and witn_sorts path x = foldl_map (witn_sort path) x 

2956  233 

15531  234 
and witn_types _ [] ((solved, failed), S) = ((solved, S :: failed), NONE) 
7643  235 
 witn_types path (t :: ts) (solved_failed, S) = 
236 
(case mg_dom t S of 

15531  237 
SOME SS => 
7643  238 
(*do not descend into stronger args (achieving termination)*) 
239 
if exists (fn D => le D S orelse exists (le D) path) SS then 

240 
witn_types path ts (solved_failed, S) 

241 
else 

242 
let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in 

17756  243 
if forall is_some ws then 
15570  244 
let val w = (Type (t, map (#1 o valOf) ws), S) 
15531  245 
in ((w :: solved', failed'), SOME w) end 
7643  246 
else witn_types path ts ((solved', failed'), S) 
247 
end 

15531  248 
 NONE => witn_types path ts (solved_failed, S)); 
7643  249 

250 
in witn_sorts [] (([], []), sorts) end; 

251 

14828  252 
fun str_of_sort [c] = c 
253 
 str_of_sort cs = enclose "{" "}" (commas cs); 

254 

255 
in 

7643  256 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

257 
fun witness_sorts (classes, arities) log_types hyps sorts = 
7643  258 
let 
16881  259 
(*double check result of witness construction*) 
15531  260 
fun check_result NONE = NONE 
261 
 check_result (SOME (T, S)) = 

262 
if of_sort (classes, arities) (T, S) then SOME (T, S) 

14782
d6ce35a1c386
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm
parents:
9281
diff
changeset

263 
else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S); 
15570  264 
in List.mapPartial check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end; 
2956  265 

266 
end; 

14828  267 

268 
end; 