Mercurial > urweb

comparison src/elaborate.sml @ 403:8084fa9216de

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New implicit argument handling
author Adam Chlipala <adamc@hcoop.net>
date Tue, 21 Oct 2008 16:41:11 -0400
parents ebf27030ae3b
children 06fcddcd20d3
comparison
equal deleted inserted replaced
402:ebf27030ae3b 403:8084fa9216de
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
7 * - Redistributions of source code must retain the above copyright notice, 7 * - Redistributions of source code must retain the above copyright notice,
8 * this list of conditions and the following disclaimer. 8 * this list of conditions and the following disclaimer.
9 * - Redistributions in binary form must reproduce the above copyright notice, 9 * - Redistributions in binary form must reproduce the above copyright notice,
10 * this list of conditions and the following disclaimer in the documentation 10 * this list of conditions and the following disclaimer in the documentation
11 * and/or other materials provided with the distribution. 11 * and/or other materials provided with the distribution.
12 * - The names of contributors may not be used to endorse or promote products 12 * - The names of contributors may not be used to endorse or promote products
13 * derived from this software without specific prior written permission. 13 * derived from this software without specific prior written permission.
14 * 14 *
15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE. 25 * POSSIBILITY OF SUCH DAMAGE.
26 *) 26 *)
27 27
28 structure Elaborate :> ELABORATE = struct 28 structure Elaborate :> ELABORATE = struct
29 29
30 structure P = Prim 30 structure P = Prim
31 structure L = Source 31 structure L = Source
32 structure L' = Elab 32 structure L' = Elab
33 structure E = ElabEnv 33 structure E = ElabEnv
34 structure U = ElabUtil 34 structure U = ElabUtil
35 structure D = Disjoint 35 structure D = Disjoint
36 36
37 open Print 37 open Print
38 open ElabPrint 38 open ElabPrint
39 open ElabErr 39 open ElabErr
40 40
41 structure IM = IntBinaryMap 41 structure IM = IntBinaryMap
42 42
43 structure SK = struct 43 structure SK = struct
44 type ord_key = string 44 type ord_key = string
45 val compare = String.compare 45 val compare = String.compare
46 end 46 end
47 47
48 structure SS = BinarySetFn(SK) 48 structure SS = BinarySetFn(SK)
49 structure SM = BinaryMapFn(SK) 49 structure SM = BinaryMapFn(SK)
50 50
51 val basis_r = ref 0 51 val basis_r = ref 0
52 52
53 fun elabExplicitness e = 53 fun elabExplicitness e =
54 case e of 54 case e of
55 L.Explicit => L'.Explicit 55 L.Explicit => L'.Explicit
56 | L.Implicit => L'.Implicit 56 | L.Implicit => L'.Implicit
57 57
58 fun occursKind r = 58 fun occursKind r =
59 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r' 59 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
60 | _ => false) 60 | _ => false)
61 61
62 exception KUnify' of kunify_error 62 exception KUnify' of kunify_error
63 63
64 fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) = 64 fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
65 let 65 let
66 fun err f = raise KUnify' (f (k1All, k2All)) 66 fun err f = raise KUnify' (f (k1All, k2All))
67 in 67 in
68 case (k1, k2) of 68 case (k1, k2) of
69 (L'.KType, L'.KType) => () 69 (L'.KType, L'.KType) => ()
70 | (L'.KUnit, L'.KUnit) => () 70 | (L'.KUnit, L'.KUnit) => ()
71 71
72 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => 72 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
73 (unifyKinds' d1 d2; 73 (unifyKinds' d1 d2;
74 unifyKinds' r1 r2) 74 unifyKinds' r1 r2)
75 | (L'.KName, L'.KName) => () 75 | (L'.KName, L'.KName) => ()
76 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 76 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
77 | (L'.KTuple ks1, L'.KTuple ks2) => 77 | (L'.KTuple ks1, L'.KTuple ks2) =>
78 ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2)) 78 ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2))
79 handle ListPair.UnequalLengths => err KIncompatible) 79 handle ListPair.UnequalLengths => err KIncompatible)
80 80
81 | (L'.KError, _) => () 81 | (L'.KError, _) => ()
82 | (_, L'.KError) => () 82 | (_, L'.KError) => ()
83 83
84 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All 84 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
85 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All 85 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
86 86
87 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => 87 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
88 if r1 = r2 then 88 if r1 = r2 then
89 () 89 ()
90 else 90 else
91 r1 := SOME k2All 91 r1 := SOME k2All
92 92
93 | (L'.KUnif (_, _, r), _) => 93 | (L'.KUnif (_, _, r), _) =>
94 if occursKind r k2All then 94 if occursKind r k2All then
95 err KOccursCheckFailed 95 err KOccursCheckFailed
96 else 96 else
97 r := SOME k2All 97 r := SOME k2All
98 | (_, L'.KUnif (_, _, r)) => 98 | (_, L'.KUnif (_, _, r)) =>
99 if occursKind r k1All then 99 if occursKind r k1All then
100 err KOccursCheckFailed 100 err KOccursCheckFailed
101 else 101 else
102 r := SOME k1All 102 r := SOME k1All
103 103
104 | _ => err KIncompatible 104 | _ => err KIncompatible
105 end 105 end
106 106
107 exception KUnify of L'.kind * L'.kind * kunify_error 107 exception KUnify of L'.kind * L'.kind * kunify_error
108 108
109 fun unifyKinds k1 k2 = 109 fun unifyKinds k1 k2 =
110 unifyKinds' k1 k2 110 unifyKinds' k1 k2
111 handle KUnify' err => raise KUnify (k1, k2, err) 111 handle KUnify' err => raise KUnify (k1, k2, err)
112 112
113 fun checkKind env c k1 k2 = 113 fun checkKind env c k1 k2 =
114 unifyKinds k1 k2 114 unifyKinds k1 k2
115 handle KUnify (k1, k2, err) => 115 handle KUnify (k1, k2, err) =>
116 conError env (WrongKind (c, k1, k2, err)) 116 conError env (WrongKind (c, k1, k2, err))
117 117
118 val dummy = ErrorMsg.dummySpan 118 val dummy = ErrorMsg.dummySpan
119 119
120 val ktype = (L'.KType, dummy) 120 val ktype = (L'.KType, dummy)
121 val kname = (L'.KName, dummy) 121 val kname = (L'.KName, dummy)
122 val ktype_record = (L'.KRecord ktype, dummy) 122 val ktype_record = (L'.KRecord ktype, dummy)
123 123
124 val cerror = (L'.CError, dummy) 124 val cerror = (L'.CError, dummy)
125 val kerror = (L'.KError, dummy) 125 val kerror = (L'.KError, dummy)
126 val eerror = (L'.EError, dummy) 126 val eerror = (L'.EError, dummy)
127 val sgnerror = (L'.SgnError, dummy) 127 val sgnerror = (L'.SgnError, dummy)
128 val strerror = (L'.StrError, dummy) 128 val strerror = (L'.StrError, dummy)
129 129
130 val int = ref cerror 130 val int = ref cerror
131 val float = ref cerror 131 val float = ref cerror
132 val string = ref cerror 132 val string = ref cerror
133 val table = ref cerror 133 val table = ref cerror
134 134
135 local 135 local
136 val count = ref 0 136 val count = ref 0
137 in 137 in
138 138
139 fun resetKunif () = count := 0 139 fun resetKunif () = count := 0
140 140
141 fun kunif loc = 141 fun kunif loc =
142 let 142 let
143 val n = !count 143 val n = !count
144 val s = if n <= 26 then 144 val s = if n <= 26 then
145 str (chr (ord #"A" + n)) 145 str (chr (ord #"A" + n))
146 else 146 else
147 "U" ^ Int.toString (n - 26) 147 "U" ^ Int.toString (n - 26)
148 in 148 in
149 count := n + 1; 149 count := n + 1;
150 (L'.KUnif (loc, s, ref NONE), dummy) 150 (L'.KUnif (loc, s, ref NONE), dummy)
151 end 151 end
152 152
153 end 153 end
154 154
155 local 155 local
156 val count = ref 0 156 val count = ref 0
157 in 157 in
158 158
159 fun resetCunif () = count := 0 159 fun resetCunif () = count := 0
160 160
161 fun cunif (loc, k) = 161 fun cunif (loc, k) =
162 let 162 let
163 val n = !count 163 val n = !count
164 val s = if n <= 26 then 164 val s = if n <= 26 then
165 str (chr (ord #"A" + n)) 165 str (chr (ord #"A" + n))
166 else 166 else
167 "U" ^ Int.toString (n - 26) 167 "U" ^ Int.toString (n - 26)
168 in 168 in
169 count := n + 1; 169 count := n + 1;
170 (L'.CUnif (loc, k, s, ref NONE), dummy) 170 (L'.CUnif (loc, k, s, ref NONE), dummy)
171 end 171 end
172 172
173 end 173 end
174 174
175 fun elabKind (k, loc) = 175 fun elabKind (k, loc) =
176 case k of 176 case k of
177 L.KType => (L'.KType, loc) 177 L.KType => (L'.KType, loc)
178 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) 178 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
179 | L.KName => (L'.KName, loc) 179 | L.KName => (L'.KName, loc)
180 | L.KRecord k => (L'.KRecord (elabKind k), loc) 180 | L.KRecord k => (L'.KRecord (elabKind k), loc)
181 | L.KUnit => (L'.KUnit, loc) 181 | L.KUnit => (L'.KUnit, loc)
182 | L.KTuple ks => (L'.KTuple (map elabKind ks), loc) 182 | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
183 | L.KWild => kunif loc 183 | L.KWild => kunif loc
184 184
185 fun foldKind (dom, ran, loc)= 185 fun foldKind (dom, ran, loc)=
186 (L'.KArrow ((L'.KArrow ((L'.KName, loc), 186 (L'.KArrow ((L'.KArrow ((L'.KName, loc),
187 (L'.KArrow (dom, 187 (L'.KArrow (dom,
188 (L'.KArrow (ran, ran), loc)), loc)), loc), 188 (L'.KArrow (ran, ran), loc)), loc)), loc),
189 (L'.KArrow (ran, 189 (L'.KArrow (ran,
190 (L'.KArrow ((L'.KRecord dom, loc), 190 (L'.KArrow ((L'.KRecord dom, loc),
191 ran), loc)), loc)), loc) 191 ran), loc)), loc)), loc)
192 192
193 fun hnormKind (kAll as (k, _)) = 193 fun hnormKind (kAll as (k, _)) =
194 case k of 194 case k of
195 L'.KUnif (_, _, ref (SOME k)) => hnormKind k 195 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
196 | _ => kAll 196 | _ => kAll
197 197
198 fun elabCon (env, denv) (c, loc) = 198 fun elabCon (env, denv) (c, loc) =
199 case c of 199 case c of
200 L.CAnnot (c, k) => 200 L.CAnnot (c, k) =>
201 let 201 let
202 val k' = elabKind k 202 val k' = elabKind k
203 val (c', ck, gs) = elabCon (env, denv) c 203 val (c', ck, gs) = elabCon (env, denv) c
204 in 204 in
205 checkKind env c' ck k'; 205 checkKind env c' ck k';
206 (c', k', gs) 206 (c', k', gs)
207 end 207 end
208 208
209 | L.TFun (t1, t2) => 209 | L.TFun (t1, t2) =>
210 let 210 let
211 val (t1', k1, gs1) = elabCon (env, denv) t1 211 val (t1', k1, gs1) = elabCon (env, denv) t1
212 val (t2', k2, gs2) = elabCon (env, denv) t2 212 val (t2', k2, gs2) = elabCon (env, denv) t2
213 in 213 in
214 checkKind env t1' k1 ktype; 214 checkKind env t1' k1 ktype;
215 checkKind env t2' k2 ktype; 215 checkKind env t2' k2 ktype;
216 ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2) 216 ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2)
217 end 217 end
218 | L.TCFun (e, x, k, t) => 218 | L.TCFun (e, x, k, t) =>
219 let 219 let
220 val e' = elabExplicitness e 220 val e' = elabExplicitness e
221 val k' = elabKind k 221 val k' = elabKind k
222 val env' = E.pushCRel env x k' 222 val env' = E.pushCRel env x k'
223 val (t', tk, gs) = elabCon (env', D.enter denv) t 223 val (t', tk, gs) = elabCon (env', D.enter denv) t
224 in 224 in
225 checkKind env t' tk ktype; 225 checkKind env t' tk ktype;
226 ((L'.TCFun (e', x, k', t'), loc), ktype, gs) 226 ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
227 end 227 end
228 | L.CDisjoint (c1, c2, c) => 228 | L.CDisjoint (c1, c2, c) =>
229 let 229 let
230 val (c1', k1, gs1) = elabCon (env, denv) c1 230 val (c1', k1, gs1) = elabCon (env, denv) c1
231 val (c2', k2, gs2) = elabCon (env, denv) c2 231 val (c2', k2, gs2) = elabCon (env, denv) c2
232 232
233 val ku1 = kunif loc 233 val ku1 = kunif loc
234 val ku2 = kunif loc 234 val ku2 = kunif loc
235 235
236 val (denv', gs3) = D.assert env denv (c1', c2') 236 val (denv', gs3) = D.assert env denv (c1', c2')
237 val (c', k, gs4) = elabCon (env, denv') c 237 val (c', k, gs4) = elabCon (env, denv') c
238 in 238 in
239 checkKind env c1' k1 (L'.KRecord ku1, loc); 239 checkKind env c1' k1 (L'.KRecord ku1, loc);
240 checkKind env c2' k2 (L'.KRecord ku2, loc); 240 checkKind env c2' k2 (L'.KRecord ku2, loc);
241 241
242 ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4) 242 ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
243 end 243 end
244 | L.TRecord c => 244 | L.TRecord c =>
245 let 245 let
246 val (c', ck, gs) = elabCon (env, denv) c 246 val (c', ck, gs) = elabCon (env, denv) c
247 val k = (L'.KRecord ktype, loc) 247 val k = (L'.KRecord ktype, loc)
248 in 248 in
249 checkKind env c' ck k; 249 checkKind env c' ck k;
250 ((L'.TRecord c', loc), ktype, gs) 250 ((L'.TRecord c', loc), ktype, gs)
251 end 251 end
252 252
253 | L.CVar ([], s) => 253 | L.CVar ([], s) =>
254 (case E.lookupC env s of 254 (case E.lookupC env s of
255 E.NotBound => 255 E.NotBound =>
256 (conError env (UnboundCon (loc, s)); 256 (conError env (UnboundCon (loc, s));
257 (cerror, kerror, [])) 257 (cerror, kerror, []))
258 | E.Rel (n, k) => 258 | E.Rel (n, k) =>
259 ((L'.CRel n, loc), k, []) 259 ((L'.CRel n, loc), k, [])
260 | E.Named (n, k) => 260 | E.Named (n, k) =>
261 ((L'.CNamed n, loc), k, [])) 261 ((L'.CNamed n, loc), k, []))
262 | L.CVar (m1 :: ms, s) => 262 | L.CVar (m1 :: ms, s) =>
263 (case E.lookupStr env m1 of 263 (case E.lookupStr env m1 of
264 NONE => (conError env (UnboundStrInCon (loc, m1)); 264 NONE => (conError env (UnboundStrInCon (loc, m1));
265 (cerror, kerror, []))
266 | SOME (n, sgn) =>
267 let
268 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
269 case E.projectStr env {sgn = sgn, str = str, field = m} of
270 NONE => (conError env (UnboundStrInCon (loc, m));
271 (strerror, sgnerror))
272 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
273 ((L'.StrVar n, loc), sgn) ms
274
275 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
276 NONE => (conError env (UnboundCon (loc, s));
277 kerror)
278 | SOME (k, _) => k
279 in
280 ((L'.CModProj (n, ms, s), loc), k, [])
281 end)
282
283 | L.CApp (c1, c2) =>
284 let
285 val (c1', k1, gs1) = elabCon (env, denv) c1
286 val (c2', k2, gs2) = elabCon (env, denv) c2
287 val dom = kunif loc
288 val ran = kunif loc
289 in
290 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
291 checkKind env c2' k2 dom;
292 ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2)
293 end
294 | L.CAbs (x, ko, t) =>
295 let
296 val k' = case ko of
297 NONE => kunif loc
298 | SOME k => elabKind k
299 val env' = E.pushCRel env x k'
300 val (t', tk, gs) = elabCon (env', D.enter denv) t
301 in
302 ((L'.CAbs (x, k', t'), loc),
303 (L'.KArrow (k', tk), loc),
304 gs)
305 end
306
307 | L.CName s =>
308 ((L'.CName s, loc), kname, [])
309
310 | L.CRecord xcs =>
311 let
312 val k = kunif loc
313
314 val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
315 let
316 val (x', xk, gs1) = elabCon (env, denv) x
317 val (c', ck, gs2) = elabCon (env, denv) c
318 in
319 checkKind env x' xk kname;
320 checkKind env c' ck k;
321 ((x', c'), gs1 @ gs2 @ gs)
322 end) [] xcs
323
324 val rc = (L'.CRecord (k, xcs'), loc)
325 (* Add duplicate field checking later. *)
326
327 fun prove (xcs, ds) =
328 case xcs of
329 [] => ds
330 | xc :: rest =>
331 let
332 val r1 = (L'.CRecord (k, [xc]), loc)
333 val ds = foldl (fn (xc', ds) =>
334 let
335 val r2 = (L'.CRecord (k, [xc']), loc)
336 in
337 D.prove env denv (r1, r2, loc) @ ds
338 end)
339 ds rest
340 in
341 prove (rest, ds)
342 end
343 in
344 (rc, (L'.KRecord k, loc), prove (xcs', gs))
345 end
346 | L.CConcat (c1, c2) =>
347 let
348 val (c1', k1, gs1) = elabCon (env, denv) c1
349 val (c2', k2, gs2) = elabCon (env, denv) c2
350 val ku = kunif loc
351 val k = (L'.KRecord ku, loc)
352 in
353 checkKind env c1' k1 k;
354 checkKind env c2' k2 k;
355 ((L'.CConcat (c1', c2'), loc), k,
356 D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
357 end
358 | L.CFold =>
359 let
360 val dom = kunif loc
361 val ran = kunif loc
362 in
363 ((L'.CFold (dom, ran), loc),
364 foldKind (dom, ran, loc),
365 [])
366 end
367
368 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
369
370 | L.CTuple cs =>
371 let
372 val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) =>
373 let
374 val (c', k, gs') = elabCon (env, denv) c
375 in
376 (c' :: cs', k :: ks, gs' @ gs)
377 end) ([], [], []) cs
378 in
379 ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs)
380 end
381 | L.CProj (c, n) =>
382 let
383 val (c', k, gs) = elabCon (env, denv) c
384 in
385 case hnormKind k of
386 (L'.KTuple ks, _) =>
387 if n <= 0 orelse n > length ks then
388 (conError env (ProjBounds (c', n));
265 (cerror, kerror, [])) 389 (cerror, kerror, []))
266 | SOME (n, sgn) => 390 else
391 ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs)
392 | k => (conError env (ProjMismatch (c', k));
393 (cerror, kerror, []))
394 end
395
396 | L.CWild k =>
397 let
398 val k' = elabKind k
399 in
400 (cunif (loc, k'), k', [])
401 end
402
403 fun kunifsRemain k =
404 case k of
405 L'.KUnif (_, _, ref NONE) => true
406 | _ => false
407 fun cunifsRemain c =
408 case c of
409 L'.CUnif (loc, _, _, ref NONE) => SOME loc
410 | _ => NONE
411
412 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
413 con = fn _ => false,
414 exp = fn _ => false,
415 sgn_item = fn _ => false,
416 sgn = fn _ => false,
417 str = fn _ => false,
418 decl = fn _ => false}
419
420 val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
421 con = cunifsRemain,
422 exp = fn _ => NONE,
423 sgn_item = fn _ => NONE,
424 sgn = fn _ => NONE,
425 str = fn _ => NONE,
426 decl = fn _ => NONE}
427
428 fun occursCon r =
429 U.Con.exists {kind = fn _ => false,
430 con = fn L'.CUnif (_, _, _, r') => r = r'
431 | _ => false}
432
433 exception CUnify' of cunify_error
434
435 exception SynUnif = E.SynUnif
436
437 open ElabOps
438
439 type record_summary = {
440 fields : (L'.con * L'.con) list,
441 unifs : (L'.con * L'.con option ref) list,
442 others : L'.con list
443 }
444
445 fun summaryToCon {fields, unifs, others} =
446 let
447 val c = (L'.CRecord (ktype, []), dummy)
448 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
449 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
450 in
451 (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
452 end
453
454 fun p_summary env s = p_con env (summaryToCon s)
455
456 exception CUnify of L'.con * L'.con * cunify_error
457
458 fun kindof env (c, loc) =
459 case c of
460 L'.TFun _ => ktype
461 | L'.TCFun _ => ktype
462 | L'.TRecord _ => ktype
463
464 | L'.CRel xn => #2 (E.lookupCRel env xn)
465 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
466 | L'.CModProj (n, ms, x) =>
467 let
468 val (_, sgn) = E.lookupStrNamed env n
469 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
470 case E.projectStr env {sgn = sgn, str = str, field = m} of
471 NONE => raise Fail "kindof: Unknown substructure"
472 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
473 ((L'.StrVar n, loc), sgn) ms
474 in
475 case E.projectCon env {sgn = sgn, str = str, field = x} of
476 NONE => raise Fail "kindof: Unknown con in structure"
477 | SOME (k, _) => k
478 end
479
480 | L'.CApp (c, _) =>
481 (case hnormKind (kindof env c) of
482 (L'.KArrow (_, k), _) => k
483 | (L'.KError, _) => kerror
484 | k => raise CUnify' (CKindof (k, c)))
485 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
486 | L'.CDisjoint (_, _, _, c) => kindof env c
487
488 | L'.CName _ => kname
489
490 | L'.CRecord (k, _) => (L'.KRecord k, loc)
491 | L'.CConcat (c, _) => kindof env c
492 | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
493
494 | L'.CUnit => (L'.KUnit, loc)
495
496 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
497 | L'.CProj (c, n) =>
498 (case hnormKind (kindof env c) of
499 (L'.KTuple ks, _) => List.nth (ks, n - 1)
500 | k => raise CUnify' (CKindof (k, c)))
501
502 | L'.CError => kerror
503 | L'.CUnif (_, k, _, _) => k
504
505 val hnormCon = D.hnormCon
506
507 datatype con_summary =
508 Nil
509 | Cons
510 | Unknown
511
512 fun compatible cs =
513 case cs of
514 (Unknown, _) => false
515 | (_, Unknown) => false
516 | (s1, s2) => s1 = s2
517
518 fun summarizeCon (env, denv) c =
519 let
520 val (c, gs) = hnormCon (env, denv) c
521 in
522 case #1 c of
523 L'.CRecord (_, []) => (Nil, gs)
524 | L'.CRecord (_, _ :: _) => (Cons, gs)
525 | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
526 | L'.CDisjoint (_, _, _, c) =>
267 let 527 let
268 val (str, sgn) = foldl (fn (m, (str, sgn)) => 528 val (s, gs') = summarizeCon (env, denv) c
269 case E.projectStr env {sgn = sgn, str = str, field = m} of
270 NONE => (conError env (UnboundStrInCon (loc, m));
271 (strerror, sgnerror))
272 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
273 ((L'.StrVar n, loc), sgn) ms
274
275 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
276 NONE => (conError env (UnboundCon (loc, s));
277 kerror)
278 | SOME (k, _) => k
279 in 529 in
280 ((L'.CModProj (n, ms, s), loc), k, []) 530 (s, gs @ gs')
281 end) 531 end
282 532 | _ => (Unknown, gs)
283 | L.CApp (c1, c2) => 533 end
284 let 534
285 val (c1', k1, gs1) = elabCon (env, denv) c1 535 fun p_con_summary s =
286 val (c2', k2, gs2) = elabCon (env, denv) c2 536 Print.PD.string (case s of
287 val dom = kunif loc 537 Nil => "Nil"
288 val ran = kunif loc 538 | Cons => "Cons"
289 in 539 | Unknown => "Unknown")
290 checkKind env c1' k1 (L'.KArrow (dom, ran), loc); 540
291 checkKind env c2' k2 dom; 541 exception SummaryFailure
292 ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2) 542
293 end 543 fun unifyRecordCons (env, denv) (c1, c2) =
294 | L.CAbs (x, ko, t) => 544 let
295 let 545 fun rkindof c =
296 val k' = case ko of 546 case hnormKind (kindof env c) of
297 NONE => kunif loc 547 (L'.KRecord k, _) => k
298 | SOME k => elabKind k 548 | (L'.KError, _) => kerror
299 val env' = E.pushCRel env x k' 549 | k => raise CUnify' (CKindof (k, c))
300 val (t', tk, gs) = elabCon (env', D.enter denv) t 550
301 in 551 val k1 = rkindof c1
302 ((L'.CAbs (x, k', t'), loc), 552 val k2 = rkindof c2
303 (L'.KArrow (k', tk), loc), 553
304 gs) 554 val (r1, gs1) = recordSummary (env, denv) c1
305 end 555 val (r2, gs2) = recordSummary (env, denv) c2
306 556 in
307 | L.CName s => 557 unifyKinds k1 k2;
308 ((L'.CName s, loc), kname, []) 558 unifySummaries (env, denv) (k1, r1, r2);
309 559 gs1 @ gs2
310 | L.CRecord xcs => 560 end
311 let 561
312 val k = kunif loc 562 and recordSummary (env, denv) c =
313 563 let
314 val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) => 564 val (c, gs) = hnormCon (env, denv) c
315 let 565
316 val (x', xk, gs1) = elabCon (env, denv) x 566 val (sum, gs') =
317 val (c', ck, gs2) = elabCon (env, denv) c 567 case c of
318 in 568 (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, [])
319 checkKind env x' xk kname; 569 | (L'.CConcat (c1, c2), _) =>
320 checkKind env c' ck k; 570 let
321 ((x', c'), gs1 @ gs2 @ gs) 571 val (s1, gs1) = recordSummary (env, denv) c1
322 end) [] xcs 572 val (s2, gs2) = recordSummary (env, denv) c2
323 573 in
324 val rc = (L'.CRecord (k, xcs'), loc) 574 ({fields = #fields s1 @ #fields s2,
325 (* Add duplicate field checking later. *) 575 unifs = #unifs s1 @ #unifs s2,
326 576 others = #others s1 @ #others s2},
327 fun prove (xcs, ds) = 577 gs1 @ gs2)
328 case xcs of 578 end
329 [] => ds 579 | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c
330 | xc :: rest => 580 | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, [])
331 let 581 | c' => ({fields = [], unifs = [], others = [c']}, [])
332 val r1 = (L'.CRecord (k, [xc]), loc) 582 in
333 val ds = foldl (fn (xc', ds) => 583 (sum, gs @ gs')
334 let 584 end
335 val r2 = (L'.CRecord (k, [xc']), loc) 585
336 in 586 and consEq (env, denv) (c1, c2) =
337 D.prove env denv (r1, r2, loc) @ ds 587 let
338 end) 588 val gs = unifyCons (env, denv) c1 c2
339 ds rest 589 in
340 in 590 List.all (fn (loc, env, denv, c1, c2) =>
341 prove (rest, ds) 591 case D.prove env denv (c1, c2, loc) of
342 end 592 [] => true
343 in 593 | _ => false) gs
344 (rc, (L'.KRecord k, loc), prove (xcs', gs)) 594 end
345 end 595 handle CUnify _ => false
346 | L.CConcat (c1, c2) => 596
347 let 597 and consNeq env (c1, c2) =
348 val (c1', k1, gs1) = elabCon (env, denv) c1 598 case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of
349 val (c2', k2, gs2) = elabCon (env, denv) c2 599 (L'.CName x1, L'.CName x2) => x1 <> x2
350 val ku = kunif loc 600 | _ => false
351 val k = (L'.KRecord ku, loc) 601
352 in 602 and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
353 checkKind env c1' k1 k; 603 let
354 checkKind env c2' k2 k; 604 val loc = #2 k
355 ((L'.CConcat (c1', c2'), loc), k, 605 (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
356 D.prove env denv (c1', c2', loc) @ gs1 @ gs2) 606 ("#2", p_summary env s2)]*)
357 end 607
358 | L.CFold => 608 fun eatMatching p (ls1, ls2) =
359 let 609 let
360 val dom = kunif loc 610 fun em (ls1, ls2, passed1) =
361 val ran = kunif loc 611 case ls1 of
362 in 612 [] => (rev passed1, ls2)
363 ((L'.CFold (dom, ran), loc), 613 | h1 :: t1 =>
364 foldKind (dom, ran, loc), 614 let
615 fun search (ls2', passed2) =
616 case ls2' of
617 [] => em (t1, ls2, h1 :: passed1)
618 | h2 :: t2 =>
619 if p (h1, h2) then
620 em (t1, List.revAppend (passed2, t2), passed1)
621 else
622 search (t2, h2 :: passed2)
623 in
624 search (ls2, [])
625 end
626 in
627 em (ls1, ls2, [])
628 end
629
630 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
631 not (consNeq env (x1, x2))
632 andalso consEq (env, denv) (c1, c2)
633 andalso consEq (env, denv) (x1, x2))
634 (#fields s1, #fields s2)
635 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
636 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
637 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
638 val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2)
639 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
640 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
641
642 fun unifFields (fs, others, unifs) =
643 case (fs, others, unifs) of
644 ([], [], _) => ([], [], unifs)
645 | (_, _, []) => (fs, others, [])
646 | (_, _, (_, r) :: rest) =>
647 let
648 val r' = ref NONE
649 val kr = (L'.KRecord k, dummy)
650 val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy)
651
652 val prefix = case (fs, others) of
653 ([], other :: others) =>
654 List.foldl (fn (other, c) =>
655 (L'.CConcat (c, other), dummy))
656 other others
657 | (fs, []) =>
658 (L'.CRecord (k, fs), dummy)
659 | (fs, others) =>
660 List.foldl (fn (other, c) =>
661 (L'.CConcat (c, other), dummy))
662 (L'.CRecord (k, fs), dummy) others
663 in
664 r := SOME (L'.CConcat (prefix, cr'), dummy);
665 ([], [], (cr', r') :: rest)
666 end
667
668 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
669 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
670
671 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
672 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
673
674 fun isGuessable (other, fs) =
675 let
676 val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure)
677 in
678 List.all (fn (loc, env, denv, c1, c2) =>
679 case D.prove env denv (c1, c2, loc) of
680 [] => true
681 | _ => false) gs
682 end
683 handle SummaryFailure => false
684
685 val (fs1, fs2, others1, others2) =
686 case (fs1, fs2, others1, others2) of
687 ([], _, [other1], []) =>
688 if isGuessable (other1, fs2) then
689 ([], [], [], [])
690 else
691 (fs1, fs2, others1, others2)
692 | (_, [], [], [other2]) =>
693 if isGuessable (other2, fs1) then
694 ([], [], [], [])
695 else
696 (fs1, fs2, others1, others2)
697 | _ => (fs1, fs2, others1, others2)
698
699 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
700 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
701
702 val clear = case (fs1, others1, fs2, others2) of
703 ([], [], [], []) => true
704 | _ => false
705 val empty = (L'.CRecord (k, []), dummy)
706
707 fun unsummarize {fields, unifs, others} =
708 let
709 val c = (L'.CRecord (k, fields), loc)
710
711 val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
712 c unifs
713 in
714 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
715 c others
716 end
717
718 fun pairOffUnifs (unifs1, unifs2) =
719 case (unifs1, unifs2) of
720 ([], _) =>
721 if clear then
722 List.app (fn (_, r) => r := SOME empty) unifs2
723 else
724 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
725 | (_, []) =>
726 if clear then
727 List.app (fn (_, r) => r := SOME empty) unifs1
728 else
729 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
730 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
731 (r2 := SOME c1;
732 pairOffUnifs (rest1, rest2))
733 in
734 pairOffUnifs (unifs1, unifs2)
735 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
736 ("#2", p_summary env s2)]*)
737 end
738
739 and guessFold (env, denv) (c1, c2, gs, ex) =
740 let
741 val loc = #2 c1
742
743 fun unfold (dom, ran, f, i, r, c) =
744 let
745 val nm = cunif (loc, (L'.KName, loc))
746 val v = cunif (loc, dom)
747 val rest = cunif (loc, (L'.KRecord dom, loc))
748 val acc = (L'.CFold (dom, ran), loc)
749 val acc = (L'.CApp (acc, f), loc)
750 val acc = (L'.CApp (acc, i), loc)
751 val acc = (L'.CApp (acc, rest), loc)
752
753 val (iS, gs3) = summarizeCon (env, denv) i
754
755 val app = (L'.CApp (f, nm), loc)
756 val app = (L'.CApp (app, v), loc)
757 val app = (L'.CApp (app, acc), loc)
758 val (appS, gs4) = summarizeCon (env, denv) app
759
760 val (cS, gs5) = summarizeCon (env, denv) c
761 in
762 (*prefaces "Summaries" [("iS", p_con_summary iS),
763 ("appS", p_con_summary appS),
764 ("cS", p_con_summary cS)];*)
765
766 if compatible (iS, appS) then
767 raise ex
768 else if compatible (cS, iS) then
769 let
770 (*val () = prefaces "Same?" [("i", p_con env i),
771 ("c", p_con env c)]*)
772 val gs6 = unifyCons (env, denv) i c
773 (*val () = TextIO.print "Yes!\n"*)
774
775 val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
776 in
777 gs @ gs3 @ gs5 @ gs6 @ gs7
778 end
779 else if compatible (cS, appS) then
780 let
781 (*val () = prefaces "Same?" [("app", p_con env app),
782 ("c", p_con env c),
783 ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
784 val gs6 = unifyCons (env, denv) app c
785 (*val () = TextIO.print "Yes!\n"*)
786
787 val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
788 val concat = (L'.CConcat (singleton, rest), loc)
789 (*val () = prefaces "Pre-crew" [("r", p_con env r),
790 ("concat", p_con env concat)]*)
791 val gs7 = unifyCons (env, denv) r concat
792 in
793 (*prefaces "The crew" [("nm", p_con env nm),
794 ("v", p_con env v),
795 ("rest", p_con env rest)];*)
796
797 gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
798 end
799 else
800 raise ex
801 end
802 handle _ => raise ex
803 in
804 case (#1 c1, #1 c2) of
805 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) =>
806 unfold (dom, ran, f, i, r, c2)
807 | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) =>
808 unfold (dom, ran, f, i, r, c1)
809 | _ => raise ex
810 end
811
812 and unifyCons' (env, denv) c1 c2 =
813 case (#1 c1, #1 c2) of
814 (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) =>
815 let
816 val gs1 = unifyCons' (env, denv) x1 x2
817 val gs2 = unifyCons' (env, denv) y1 y2
818 val (denv', gs3) = D.assert env denv (x1, y1)
819 val gs4 = unifyCons' (env, denv') t1 t2
820 in
821 gs1 @ gs2 @ gs3 @ gs4
822 end
823 | _ =>
824 let
825 val (c1, gs1) = hnormCon (env, denv) c1
826 val (c2, gs2) = hnormCon (env, denv) c2
827 in
828 let
829 val gs3 = unifyCons'' (env, denv) c1 c2
830 in
831 gs1 @ gs2 @ gs3
832 end
833 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
834 end
835
836 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
837 let
838 fun err f = raise CUnify' (f (c1All, c2All))
839
840 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
841 in
842 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
843 ("c2All", p_con env c2All)];*)
844
845 case (c1, c2) of
846 (L'.CUnit, L'.CUnit) => []
847
848 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
849 unifyCons' (env, denv) d1 d2
850 @ unifyCons' (env, denv) r1 r2
851 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
852 if expl1 <> expl2 then
853 err CExplicitness
854 else
855 (unifyKinds d1 d2;
856 unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2)
857 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2
858
859 | (L'.CRel n1, L'.CRel n2) =>
860 if n1 = n2 then
861 []
862 else
863 err CIncompatible
864 | (L'.CNamed n1, L'.CNamed n2) =>
865 if n1 = n2 then
866 []
867 else
868 err CIncompatible
869
870 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
871 (unifyCons' (env, denv) d1 d2;
872 unifyCons' (env, denv) r1 r2)
873 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
874 (unifyKinds k1 k2;
875 unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
876
877 | (L'.CName n1, L'.CName n2) =>
878 if n1 = n2 then
879 []
880 else
881 err CIncompatible
882
883 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
884 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
885 []
886 else
887 err CIncompatible
888
889 | (L'.CTuple cs1, L'.CTuple cs2) =>
890 ((ListPair.foldlEq (fn (c1, c2, gs) =>
891 let
892 val gs' = unifyCons' (env, denv) c1 c2
893 in
894 gs' @ gs
895 end) [] (cs1, cs2))
896 handle ListPair.UnequalLengths => err CIncompatible)
897
898 | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) =>
899 unifyCons' (env, denv) (L'.CProj (c1, n1), loc) c2All
900 | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) =>
901 unifyCons' (env, denv) c1All (L'.CProj (c2, n2), loc)
902 | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) =>
903 let
904 val us = map (fn k => cunif (loc, k)) ks
905 in
906 r := SOME (L'.CTuple us, loc);
907 unifyCons' (env, denv) (List.nth (us, n - 1)) c2All
908 end
909 | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) =>
910 let
911 val us = map (fn k => cunif (loc, k)) ks
912 in
913 r := SOME (L'.CTuple us, loc);
914 unifyCons' (env, denv) c1All (List.nth (us, n - 1))
915 end
916 | (L'.CProj (c1, n1), L'.CProj (c2, n2)) =>
917 if n1 = n2 then
918 unifyCons' (env, denv) c1 c2
919 else
920 err CIncompatible
921
922 | (L'.CError, _) => []
923 | (_, L'.CError) => []
924
925 | (L'.CRecord _, _) => isRecord ()
926 | (_, L'.CRecord _) => isRecord ()
927 | (L'.CConcat _, _) => isRecord ()
928 | (_, L'.CConcat _) => isRecord ()
929
930 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
931 if r1 = r2 then
932 []
933 else
934 (unifyKinds k1 k2;
935 r1 := SOME c2All;
936 [])
937
938 | (L'.CUnif (_, _, _, r), _) =>
939 if occursCon r c2All then
940 err COccursCheckFailed
941 else
942 (r := SOME c2All;
943 [])
944 | (_, L'.CUnif (_, _, _, r)) =>
945 if occursCon r c1All then
946 err COccursCheckFailed
947 else
948 (r := SOME c1All;
949 [])
950
951 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
952 (unifyKinds dom1 dom2;
953 unifyKinds ran1 ran2;
954 [])
955
956 | _ => err CIncompatible
957 end
958
959 and unifyCons (env, denv) c1 c2 =
960 unifyCons' (env, denv) c1 c2
961 handle CUnify' err => raise CUnify (c1, c2, err)
962 | KUnify args => raise CUnify (c1, c2, CKind args)
963
964 fun checkCon (env, denv) e c1 c2 =
965 unifyCons (env, denv) c1 c2
966 handle CUnify (c1, c2, err) =>
967 (expError env (Unify (e, c1, c2, err));
365 []) 968 [])
366 end 969
367 970 fun checkPatCon (env, denv) p c1 c2 =
368 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), []) 971 unifyCons (env, denv) c1 c2
369 972 handle CUnify (c1, c2, err) =>
370 | L.CTuple cs => 973 (expError env (PatUnify (p, c1, c2, err));
371 let
372 val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) =>
373 let
374 val (c', k, gs') = elabCon (env, denv) c
375 in
376 (c' :: cs', k :: ks, gs' @ gs)
377 end) ([], [], []) cs
378 in
379 ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs)
380 end
381 | L.CProj (c, n) =>
382 let
383 val (c', k, gs) = elabCon (env, denv) c
384 in
385 case hnormKind k of
386 (L'.KTuple ks, _) =>
387 if n <= 0 orelse n > length ks then
388 (conError env (ProjBounds (c', n));
389 (cerror, kerror, []))
390 else
391 ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs)
392 | k => (conError env (ProjMismatch (c', k));
393 (cerror, kerror, []))
394 end
395
396 | L.CWild k =>
397 let
398 val k' = elabKind k
399 in
400 (cunif (loc, k'), k', [])
401 end
402
403 fun kunifsRemain k =
404 case k of
405 L'.KUnif (_, _, ref NONE) => true
406 | _ => false
407 fun cunifsRemain c =
408 case c of
409 L'.CUnif (loc, _, _, ref NONE) => SOME loc
410 | _ => NONE
411
412 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
413 con = fn _ => false,
414 exp = fn _ => false,
415 sgn_item = fn _ => false,
416 sgn = fn _ => false,
417 str = fn _ => false,
418 decl = fn _ => false}
419
420 val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
421 con = cunifsRemain,
422 exp = fn _ => NONE,
423 sgn_item = fn _ => NONE,
424 sgn = fn _ => NONE,
425 str = fn _ => NONE,
426 decl = fn _ => NONE}
427
428 fun occursCon r =
429 U.Con.exists {kind = fn _ => false,
430 con = fn L'.CUnif (_, _, _, r') => r = r'
431 | _ => false}
432
433 exception CUnify' of cunify_error
434
435 exception SynUnif = E.SynUnif
436
437 open ElabOps
438
439 type record_summary = {
440 fields : (L'.con * L'.con) list,
441 unifs : (L'.con * L'.con option ref) list,
442 others : L'.con list
443 }
444
445 fun summaryToCon {fields, unifs, others} =
446 let
447 val c = (L'.CRecord (ktype, []), dummy)
448 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
449 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
450 in
451 (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
452 end
453
454 fun p_summary env s = p_con env (summaryToCon s)
455
456 exception CUnify of L'.con * L'.con * cunify_error
457
458 fun kindof env (c, loc) =
459 case c of
460 L'.TFun _ => ktype
461 | L'.TCFun _ => ktype
462 | L'.TRecord _ => ktype
463
464 | L'.CRel xn => #2 (E.lookupCRel env xn)
465 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
466 | L'.CModProj (n, ms, x) =>
467 let
468 val (_, sgn) = E.lookupStrNamed env n
469 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
470 case E.projectStr env {sgn = sgn, str = str, field = m} of
471 NONE => raise Fail "kindof: Unknown substructure"
472 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
473 ((L'.StrVar n, loc), sgn) ms
474 in
475 case E.projectCon env {sgn = sgn, str = str, field = x} of
476 NONE => raise Fail "kindof: Unknown con in structure"
477 | SOME (k, _) => k
478 end
479
480 | L'.CApp (c, _) =>
481 (case hnormKind (kindof env c) of
482 (L'.KArrow (_, k), _) => k
483 | (L'.KError, _) => kerror
484 | k => raise CUnify' (CKindof (k, c)))
485 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
486 | L'.CDisjoint (_, _, _, c) => kindof env c
487
488 | L'.CName _ => kname
489
490 | L'.CRecord (k, _) => (L'.KRecord k, loc)
491 | L'.CConcat (c, _) => kindof env c
492 | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
493
494 | L'.CUnit => (L'.KUnit, loc)
495
496 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
497 | L'.CProj (c, n) =>
498 (case hnormKind (kindof env c) of
499 (L'.KTuple ks, _) => List.nth (ks, n - 1)
500 | k => raise CUnify' (CKindof (k, c)))
501
502 | L'.CError => kerror
503 | L'.CUnif (_, k, _, _) => k
504
505 val hnormCon = D.hnormCon
506
507 datatype con_summary =
508 Nil
509 | Cons
510 | Unknown
511
512 fun compatible cs =
513 case cs of
514 (Unknown, _) => false
515 | (_, Unknown) => false
516 | (s1, s2) => s1 = s2
517
518 fun summarizeCon (env, denv) c =
519 let
520 val (c, gs) = hnormCon (env, denv) c
521 in
522 case #1 c of
523 L'.CRecord (_, []) => (Nil, gs)
524 | L'.CRecord (_, _ :: _) => (Cons, gs)
525 | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
526 | L'.CDisjoint (_, _, _, c) =>
527 let
528 val (s, gs') = summarizeCon (env, denv) c
529 in
530 (s, gs @ gs')
531 end
532 | _ => (Unknown, gs)
533 end
534
535 fun p_con_summary s =
536 Print.PD.string (case s of
537 Nil => "Nil"
538 | Cons => "Cons"
539 | Unknown => "Unknown")
540
541 exception SummaryFailure
542
543 fun unifyRecordCons (env, denv) (c1, c2) =
544 let
545 fun rkindof c =
546 case hnormKind (kindof env c) of
547 (L'.KRecord k, _) => k
548 | (L'.KError, _) => kerror
549 | k => raise CUnify' (CKindof (k, c))
550
551 val k1 = rkindof c1
552 val k2 = rkindof c2
553
554 val (r1, gs1) = recordSummary (env, denv) c1
555 val (r2, gs2) = recordSummary (env, denv) c2
556 in
557 unifyKinds k1 k2;
558 unifySummaries (env, denv) (k1, r1, r2);
559 gs1 @ gs2
560 end
561
562 and recordSummary (env, denv) c =
563 let
564 val (c, gs) = hnormCon (env, denv) c
565
566 val (sum, gs') =
567 case c of
568 (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, [])
569 | (L'.CConcat (c1, c2), _) =>
570 let
571 val (s1, gs1) = recordSummary (env, denv) c1
572 val (s2, gs2) = recordSummary (env, denv) c2
573 in
574 ({fields = #fields s1 @ #fields s2,
575 unifs = #unifs s1 @ #unifs s2,
576 others = #others s1 @ #others s2},
577 gs1 @ gs2)
578 end
579 | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c
580 | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, [])
581 | c' => ({fields = [], unifs = [], others = [c']}, [])
582 in
583 (sum, gs @ gs')
584 end
585
586 and consEq (env, denv) (c1, c2) =
587 let
588 val gs = unifyCons (env, denv) c1 c2
589 in
590 List.all (fn (loc, env, denv, c1, c2) =>
591 case D.prove env denv (c1, c2, loc) of
592 [] => true
593 | _ => false) gs
594 end
595 handle CUnify _ => false
596
597 and consNeq env (c1, c2) =
598 case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of
599 (L'.CName x1, L'.CName x2) => x1 <> x2
600 | _ => false
601
602 and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
603 let
604 val loc = #2 k
605 (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
606 ("#2", p_summary env s2)]*)
607
608 fun eatMatching p (ls1, ls2) =
609 let
610 fun em (ls1, ls2, passed1) =
611 case ls1 of
612 [] => (rev passed1, ls2)
613 | h1 :: t1 =>
614 let
615 fun search (ls2', passed2) =
616 case ls2' of
617 [] => em (t1, ls2, h1 :: passed1)
618 | h2 :: t2 =>
619 if p (h1, h2) then
620 em (t1, List.revAppend (passed2, t2), passed1)
621 else
622 search (t2, h2 :: passed2)
623 in
624 search (ls2, [])
625 end
626 in
627 em (ls1, ls2, [])
628 end
629
630 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
631 not (consNeq env (x1, x2))
632 andalso consEq (env, denv) (c1, c2)
633 andalso consEq (env, denv) (x1, x2))
634 (#fields s1, #fields s2)
635 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
636 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
637 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
638 val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2)
639 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
640 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
641
642 fun unifFields (fs, others, unifs) =
643 case (fs, others, unifs) of
644 ([], [], _) => ([], [], unifs)
645 | (_, _, []) => (fs, others, [])
646 | (_, _, (_, r) :: rest) =>
647 let
648 val r' = ref NONE
649 val kr = (L'.KRecord k, dummy)
650 val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy)
651
652 val prefix = case (fs, others) of
653 ([], other :: others) =>
654 List.foldl (fn (other, c) =>
655 (L'.CConcat (c, other), dummy))
656 other others
657 | (fs, []) =>
658 (L'.CRecord (k, fs), dummy)
659 | (fs, others) =>
660 List.foldl (fn (other, c) =>
661 (L'.CConcat (c, other), dummy))
662 (L'.CRecord (k, fs), dummy) others
663 in
664 r := SOME (L'.CConcat (prefix, cr'), dummy);
665 ([], [], (cr', r') :: rest)
666 end
667
668 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
669 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
670
671 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
672 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
673
674 fun isGuessable (other, fs) =
675 let
676 val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure)
677 in
678 List.all (fn (loc, env, denv, c1, c2) =>
679 case D.prove env denv (c1, c2, loc) of
680 [] => true
681 | _ => false) gs
682 end
683 handle SummaryFailure => false
684
685 val (fs1, fs2, others1, others2) =
686 case (fs1, fs2, others1, others2) of
687 ([], _, [other1], []) =>
688 if isGuessable (other1, fs2) then
689 ([], [], [], [])
690 else
691 (fs1, fs2, others1, others2)
692 | (_, [], [], [other2]) =>
693 if isGuessable (other2, fs1) then
694 ([], [], [], [])
695 else
696 (fs1, fs2, others1, others2)
697 | _ => (fs1, fs2, others1, others2)
698
699 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
700 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
701
702 val clear = case (fs1, others1, fs2, others2) of
703 ([], [], [], []) => true
704 | _ => false
705 val empty = (L'.CRecord (k, []), dummy)
706
707 fun unsummarize {fields, unifs, others} =
708 let
709 val c = (L'.CRecord (k, fields), loc)
710
711 val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
712 c unifs
713 in
714 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
715 c others
716 end
717
718 fun pairOffUnifs (unifs1, unifs2) =
719 case (unifs1, unifs2) of
720 ([], _) =>
721 if clear then
722 List.app (fn (_, r) => r := SOME empty) unifs2
723 else
724 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
725 | (_, []) =>
726 if clear then
727 List.app (fn (_, r) => r := SOME empty) unifs1
728 else
729 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
730 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
731 (r2 := SOME c1;
732 pairOffUnifs (rest1, rest2))
733 in
734 pairOffUnifs (unifs1, unifs2)
735 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
736 ("#2", p_summary env s2)]*)
737 end
738
739 and guessFold (env, denv) (c1, c2, gs, ex) =
740 let
741 val loc = #2 c1
742
743 fun unfold (dom, ran, f, i, r, c) =
744 let
745 val nm = cunif (loc, (L'.KName, loc))
746 val v = cunif (loc, dom)
747 val rest = cunif (loc, (L'.KRecord dom, loc))
748 val acc = (L'.CFold (dom, ran), loc)
749 val acc = (L'.CApp (acc, f), loc)
750 val acc = (L'.CApp (acc, i), loc)
751 val acc = (L'.CApp (acc, rest), loc)
752
753 val (iS, gs3) = summarizeCon (env, denv) i
754
755 val app = (L'.CApp (f, nm), loc)
756 val app = (L'.CApp (app, v), loc)
757 val app = (L'.CApp (app, acc), loc)
758 val (appS, gs4) = summarizeCon (env, denv) app
759
760 val (cS, gs5) = summarizeCon (env, denv) c
761 in
762 (*prefaces "Summaries" [("iS", p_con_summary iS),
763 ("appS", p_con_summary appS),
764 ("cS", p_con_summary cS)];*)
765
766 if compatible (iS, appS) then
767 raise ex
768 else if compatible (cS, iS) then
769 let
770 (*val () = prefaces "Same?" [("i", p_con env i),
771 ("c", p_con env c)]*)
772 val gs6 = unifyCons (env, denv) i c
773 (*val () = TextIO.print "Yes!\n"*)
774
775 val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
776 in
777 gs @ gs3 @ gs5 @ gs6 @ gs7
778 end
779 else if compatible (cS, appS) then
780 let
781 (*val () = prefaces "Same?" [("app", p_con env app),
782 ("c", p_con env c),
783 ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
784 val gs6 = unifyCons (env, denv) app c
785 (*val () = TextIO.print "Yes!\n"*)
786
787 val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
788 val concat = (L'.CConcat (singleton, rest), loc)
789 (*val () = prefaces "Pre-crew" [("r", p_con env r),
790 ("concat", p_con env concat)]*)
791 val gs7 = unifyCons (env, denv) r concat
792 in
793 (*prefaces "The crew" [("nm", p_con env nm),
794 ("v", p_con env v),
795 ("rest", p_con env rest)];*)
796
797 gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
798 end
799 else
800 raise ex
801 end
802 handle _ => raise ex
803 in
804 case (#1 c1, #1 c2) of
805 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) =>
806 unfold (dom, ran, f, i, r, c2)
807 | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) =>
808 unfold (dom, ran, f, i, r, c1)
809 | _ => raise ex
810 end
811
812 and unifyCons' (env, denv) c1 c2 =
813 case (#1 c1, #1 c2) of
814 (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) =>
815 let
816 val gs1 = unifyCons' (env, denv) x1 x2
817 val gs2 = unifyCons' (env, denv) y1 y2
818 val (denv', gs3) = D.assert env denv (x1, y1)
819 val gs4 = unifyCons' (env, denv') t1 t2
820 in
821 gs1 @ gs2 @ gs3 @ gs4
822 end
823 | _ =>
824 let
825 val (c1, gs1) = hnormCon (env, denv) c1
826 val (c2, gs2) = hnormCon (env, denv) c2
827 in
828 let
829 val gs3 = unifyCons'' (env, denv) c1 c2
830 in
831 gs1 @ gs2 @ gs3
832 end
833 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
834 end
835
836 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
837 let
838 fun err f = raise CUnify' (f (c1All, c2All))
839
840 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
841 in
842 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
843 ("c2All", p_con env c2All)];*)
844
845 case (c1, c2) of
846 (L'.CUnit, L'.CUnit) => []
847
848 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
849 unifyCons' (env, denv) d1 d2
850 @ unifyCons' (env, denv) r1 r2
851 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
852 if expl1 <> expl2 then
853 err CExplicitness
854 else
855 (unifyKinds d1 d2;
856 unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2)
857 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2
858
859 | (L'.CRel n1, L'.CRel n2) =>
860 if n1 = n2 then
861 []
862 else
863 err CIncompatible
864 | (L'.CNamed n1, L'.CNamed n2) =>
865 if n1 = n2 then
866 []
867 else
868 err CIncompatible
869
870 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
871 (unifyCons' (env, denv) d1 d2;
872 unifyCons' (env, denv) r1 r2)
873 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
874 (unifyKinds k1 k2;
875 unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
876
877 | (L'.CName n1, L'.CName n2) =>
878 if n1 = n2 then
879 []
880 else
881 err CIncompatible
882
883 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
884 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
885 []
886 else
887 err CIncompatible
888
889 | (L'.CTuple cs1, L'.CTuple cs2) =>
890 ((ListPair.foldlEq (fn (c1, c2, gs) =>
891 let
892 val gs' = unifyCons' (env, denv) c1 c2
893 in
894 gs' @ gs
895 end) [] (cs1, cs2))
896 handle ListPair.UnequalLengths => err CIncompatible)
897
898 | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) =>
899 unifyCons' (env, denv) (L'.CProj (c1, n1), loc) c2All
900 | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) =>
901 unifyCons' (env, denv) c1All (L'.CProj (c2, n2), loc)
902 | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) =>
903 let
904 val us = map (fn k => cunif (loc, k)) ks
905 in
906 r := SOME (L'.CTuple us, loc);
907 unifyCons' (env, denv) (List.nth (us, n - 1)) c2All
908 end
909 | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) =>
910 let
911 val us = map (fn k => cunif (loc, k)) ks
912 in
913 r := SOME (L'.CTuple us, loc);
914 unifyCons' (env, denv) c1All (List.nth (us, n - 1))
915 end
916 | (L'.CProj (c1, n1), L'.CProj (c2, n2)) =>
917 if n1 = n2 then
918 unifyCons' (env, denv) c1 c2
919 else
920 err CIncompatible
921
922 | (L'.CError, _) => []
923 | (_, L'.CError) => []
924
925 | (L'.CRecord _, _) => isRecord ()
926 | (_, L'.CRecord _) => isRecord ()
927 | (L'.CConcat _, _) => isRecord ()
928 | (_, L'.CConcat _) => isRecord ()
929
930 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
931 if r1 = r2 then
932 []
933 else
934 (unifyKinds k1 k2;
935 r1 := SOME c2All;
936 [])
937
938 | (L'.CUnif (_, _, _, r), _) =>
939 if occursCon r c2All then
940 err COccursCheckFailed
941 else
942 (r := SOME c2All;
943 [])
944 | (_, L'.CUnif (_, _, _, r)) =>
945 if occursCon r c1All then
946 err COccursCheckFailed
947 else
948 (r := SOME c1All;
949 [])
950
951 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
952 (unifyKinds dom1 dom2;
953 unifyKinds ran1 ran2;
954 []) 974 [])
955 975
956 | _ => err CIncompatible 976 fun primType env p =
957 end 977 case p of
958 978 P.Int _ => !int
959 and unifyCons (env, denv) c1 c2 = 979 | P.Float _ => !float
960 unifyCons' (env, denv) c1 c2 980 | P.String _ => !string
961 handle CUnify' err => raise CUnify (c1, c2, err) 981
962 | KUnify args => raise CUnify (c1, c2, CKind args) 982 fun recCons (k, nm, v, rest, loc) =
963 983 (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
964 fun checkCon (env, denv) e c1 c2 = 984 rest), loc)
965 unifyCons (env, denv) c1 c2 985
966 handle CUnify (c1, c2, err) => 986 fun foldType (dom, loc) =
967 (expError env (Unify (e, c1, c2, err)); 987 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
968 []) 988 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
969 989 (L'.TCFun (L'.Explicit, "v", dom,
970 fun checkPatCon (env, denv) p c1 c2 = 990 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
971 unifyCons (env, denv) c1 c2 991 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
972 handle CUnify (c1, c2, err) => 992 (L'.CDisjoint (L'.Instantiate,
973 (expError env (PatUnify (p, c1, c2, err)); 993 (L'.CRecord
974 []) 994 ((L'.KUnit, loc),
975 995 [((L'.CRel 2, loc),
976 fun primType env p = 996 (L'.CUnit, loc))]), loc),
977 case p of 997 (L'.CRel 0, loc),
978 P.Int _ => !int 998 (L'.CApp ((L'.CRel 3, loc),
979 | P.Float _ => !float 999 recCons (dom,
980 | P.String _ => !string 1000 (L'.CRel 2, loc),
981 1001 (L'.CRel 1, loc),
982 fun recCons (k, nm, v, rest, loc) = 1002 (L'.CRel 0, loc),
983 (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc), 1003 loc)), loc)),
984 rest), loc) 1004 loc)), loc)),
985 1005 loc)), loc)), loc),
986 fun foldType (dom, loc) = 1006 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
987 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc), 1007 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
988 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc), 1008 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
989 (L'.TCFun (L'.Explicit, "v", dom, 1009 loc)), loc)), loc)
990 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc), 1010
991 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc), 1011 datatype constraint =
992 (L'.CDisjoint (L'.Instantiate, 1012 Disjoint of D.goal
993 (L'.CRecord 1013 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
994 ((L'.KUnit, loc), 1014
995 [((L'.CRel 2, loc), 1015 val enD = map Disjoint
996 (L'.CUnit, loc))]), loc), 1016
997 (L'.CRel 0, loc), 1017 fun elabHead (env, denv) infer (e as (_, loc)) t =
998 (L'.CApp ((L'.CRel 3, loc), 1018 let
999 recCons (dom, 1019 fun unravel (t, e) =
1000 (L'.CRel 2, loc), 1020 let
1001 (L'.CRel 1, loc), 1021 val (t, gs) = hnormCon (env, denv) t
1002 (L'.CRel 0, loc), 1022 in
1003 loc)), loc)), 1023 case t of
1004 loc)), loc)), 1024 (L'.TCFun (L'.Implicit, x, k, t'), _) =>
1005 loc)), loc)), loc), 1025 let
1006 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc), 1026 val u = cunif (loc, k)
1007 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc), 1027
1008 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)), 1028 val t'' = subConInCon (0, u) t'
1009 loc)), loc)), loc) 1029 val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc))
1010 1030 in
1011 datatype constraint = 1031 (*prefaces "Unravel" [("t'", p_con env t'),
1012 Disjoint of D.goal 1032 ("t''", p_con env t'')];*)
1013 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span 1033 (e, t, enD gs @ gs')
1014 1034 end
1015 val enD = map Disjoint 1035 | (L'.TFun (dom as (L'.CApp (cl, _), _), ran), _) =>
1016 1036 let
1017 fun elabHead (env, denv) (e as (_, loc)) t = 1037 val cl = #1 (hnormCon (env, denv) cl)
1018 let 1038 in
1019 fun unravel (t, e) = 1039 if infer <> L.TypesOnly andalso E.isClass env cl then
1020 let 1040 let
1021 val (t, gs) = hnormCon (env, denv) t 1041 val r = ref NONE
1022 in 1042 val (e, t, gs') = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
1023 case t of 1043 in
1024 (L'.TCFun (L'.Implicit, x, k, t'), _) => 1044 (e, t, TypeClass (env, dom, r, loc) :: enD gs @ gs')
1025 let 1045 end
1026 val u = cunif (loc, k) 1046 else
1027 1047 (e, t, enD gs)
1028 val t'' = subConInCon (0, u) t' 1048 end
1029 val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc))
1030 in
1031 (*prefaces "Unravel" [("t'", p_con env t'),
1032 ("t''", p_con env t'')];*)
1033 (e, t, enD gs @ gs')
1034 end
1035 | _ => (e, t, enD gs) 1049 | _ => (e, t, enD gs)
1036 end 1050 end
1037 in 1051 in
1038 unravel (t, e) 1052 case infer of
1053 L.DontInfer => (e, t, [])
1054 | _ => unravel (t, e)
1039 end 1055 end
1040 1056
1041 fun elabPat (pAll as (p, loc), (env, denv, bound)) = 1057 fun elabPat (pAll as (p, loc), (env, denv, bound)) =
1042 let 1058 let
1043 val perror = (L'.PWild, loc) 1059 val perror = (L'.PWild, loc)
1391 in 1407 in
1392 (e', t', gs1 @ enD gs2 @ enD gs3) 1408 (e', t', gs1 @ enD gs2 @ enD gs3)
1393 end 1409 end
1394 1410
1395 | L.EPrim p => ((L'.EPrim p, loc), primType env p, []) 1411 | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
1396 | L.EVar ([], s) => 1412 | L.EVar ([], s, infer) =>
1397 (case E.lookupE env s of 1413 (case E.lookupE env s of
1398 E.NotBound => 1414 E.NotBound =>
1399 (expError env (UnboundExp (loc, s)); 1415 (expError env (UnboundExp (loc, s));
1400 (eerror, cerror, [])) 1416 (eerror, cerror, []))
1401 | E.Rel (n, t) => ((L'.ERel n, loc), t, []) 1417 | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t
1402 | E.Named (n, t) => 1418 | E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed n, loc) t)
1403 if Char.isUpper (String.sub (s, 0)) then 1419 | L.EVar (m1 :: ms, s, infer) =>
1404 elabHead (env, denv) (L'.ENamed n, loc) t
1405 else
1406 ((L'.ENamed n, loc), t, []))
1407 | L.EVar (m1 :: ms, s) =>
1408 (case E.lookupStr env m1 of 1420 (case E.lookupStr env m1 of
1409 NONE => (expError env (UnboundStrInExp (loc, m1)); 1421 NONE => (expError env (UnboundStrInExp (loc, m1));
1410 (eerror, cerror, [])) 1422 (eerror, cerror, []))
1411 | SOME (n, sgn) => 1423 | SOME (n, sgn) =>
1412 let 1424 let
1420 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of 1432 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
1421 NONE => (expError env (UnboundExp (loc, s)); 1433 NONE => (expError env (UnboundExp (loc, s));
1422 cerror) 1434 cerror)
1423 | SOME t => t 1435 | SOME t => t
1424 in 1436 in
1425 ((L'.EModProj (n, ms, s), loc), t, []) 1437 elabHead (env, denv) infer (L'.EModProj (n, ms, s), loc) t
1426 end) 1438 end)
1427 1439
1428 | L.EWild => 1440 | L.EWild =>
1429 let 1441 let
1430 val r = ref NONE 1442 val r = ref NONE
1434 end 1446 end
1435 1447
1436 | L.EApp (e1, e2) => 1448 | L.EApp (e1, e2) =>
1437 let 1449 let
1438 val (e1', t1, gs1) = elabExp (env, denv) e1 1450 val (e1', t1, gs1) = elabExp (env, denv) e1
1439 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 1451 val (e2', t2, gs2) = elabExp (env, denv) e2
1440 val (e2', t2, gs3) = elabExp (env, denv) e2
1441 1452
1442 val dom = cunif (loc, ktype) 1453 val dom = cunif (loc, ktype)
1443 val ran = cunif (loc, ktype) 1454 val ran = cunif (loc, ktype)
1444 val t = (L'.TFun (dom, ran), dummy) 1455 val t = (L'.TFun (dom, ran), dummy)
1445 1456
1446 val gs4 = checkCon (env, denv) e1' t1 t 1457 val gs3 = checkCon (env, denv) e1' t1 t
1447 val gs5 = checkCon (env, denv) e2' t2 dom 1458 val gs4 = checkCon (env, denv) e2' t2 dom
1448 1459
1449 val gs = gs1 @ gs2 @ gs3 @ enD gs4 @ enD gs5 1460 val gs = gs1 @ gs2 @ enD gs3 @ enD gs4
1450 in 1461 in
1451 ((L'.EApp (e1', e2'), loc), ran, gs) 1462 ((L'.EApp (e1', e2'), loc), ran, gs)
1452 end 1463 end
1453 | L.EAbs (x, to, e) => 1464 | L.EAbs (x, to, e) =>
1454 let 1465 let
1470 end 1481 end
1471 | L.ECApp (e, c) => 1482 | L.ECApp (e, c) =>
1472 let 1483 let
1473 val (e', et, gs1) = elabExp (env, denv) e 1484 val (e', et, gs1) = elabExp (env, denv) e
1474 val oldEt = et 1485 val oldEt = et
1475 val (e', et, gs2) = elabHead (env, denv) e' et 1486 val (c', ck, gs2) = elabCon (env, denv) c
1476 val (c', ck, gs3) = elabCon (env, denv) c 1487 val ((et', _), gs3) = hnormCon (env, denv) et
1477 val ((et', _), gs4) = hnormCon (env, denv) et
1478 in 1488 in
1479 case et' of 1489 case et' of
1480 L'.CError => (eerror, cerror, []) 1490 L'.CError => (eerror, cerror, [])
1481 | L'.TCFun (_, x, k, eb) => 1491 | L'.TCFun (_, x, k, eb) =>
1482 let 1492 let
1489 ("et", p_con env oldEt), 1499 ("et", p_con env oldEt),
1490 ("x", PD.string x), 1500 ("x", PD.string x),
1491 ("eb", p_con (E.pushCRel env x k) eb), 1501 ("eb", p_con (E.pushCRel env x k) eb),
1492 ("c", p_con env c'), 1502 ("c", p_con env c'),
1493 ("eb'", p_con env eb')];*) 1503 ("eb'", p_con env eb')];*)
1494 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4) 1504 ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2 @ enD gs3)
1495 end 1505 end
1496 1506
1497 | _ => 1507 | _ =>
1498 (expError env (WrongForm ("constructor function", e', et)); 1508 (expError env (WrongForm ("constructor function", e', et));
1499 (eerror, cerror, [])) 1509 (eerror, cerror, []))