Mercurial > urweb

annotate src/elaborate.sml @ 1640:dc986eb6113c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Order constructors properly in wildification, to avoid spuriously displeasing the new scoping check
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 12:00:36 -0500
parents 6c00d8af6239
children 2b7d3d99dc42
rev   line source
adam@1529 1 (* Copyright (c) 2008-2011, Adam Chlipala
adamc@445 2 * All rights reserved.
adamc@445 3 *
adamc@445 4 * Redistribution and use in source and binary forms, with or without
adamc@445 5 * modification, are permitted provided that the following conditions are met:
adamc@445 6 *
adamc@445 7 * - Redistributions of source code must retain the above copyright notice,
adamc@445 8 * this list of conditions and the following disclaimer.
adamc@445 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@445 10 * this list of conditions and the following disclaimer in the documentation
adamc@445 11 * and/or other materials provided with the distribution.
adamc@445 12 * - The names of contributors may not be used to endorse or promote products
adamc@445 13 * derived from this software without specific prior written permission.
adamc@445 14 *
adamc@445 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@445 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@445 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@445 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@445 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@445 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@445 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@445 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@445 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@445 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@445 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@445 26 *)
adamc@403 27
adamc@403 28 structure Elaborate :> ELABORATE = struct
adamc@403 29
adamc@403 30 structure P = Prim
adamc@403 31 structure L = Source
adamc@403 32 structure L' = Elab
adamc@403 33 structure E = ElabEnv
adamc@403 34 structure U = ElabUtil
adamc@403 35 structure D = Disjoint
adamc@403 36
adamc@403 37 open Print
adamc@403 38 open ElabPrint
adamc@403 39 open ElabErr
adamc@403 40
adam@1531 41 val dumpTypes = ref false
adam@1531 42
adamc@819 43 structure IS = IntBinarySet
adamc@403 44 structure IM = IntBinaryMap
adamc@403 45
adamc@403 46 structure SK = struct
adamc@403 47 type ord_key = string
adamc@403 48 val compare = String.compare
adamc@403 49 end
adamc@403 50
adamc@403 51 structure SS = BinarySetFn(SK)
adamc@403 52 structure SM = BinaryMapFn(SK)
adamc@403 53
adamc@403 54 val basis_r = ref 0
adamc@633 55 val top_r = ref 0
adamc@403 56
adamc@403 57 fun elabExplicitness e =
adamc@403 58 case e of
adamc@403 59 L.Explicit => L'.Explicit
adamc@403 60 | L.Implicit => L'.Implicit
adamc@403 61
adamc@403 62 fun occursKind r =
adamc@403 63 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
adamc@403 64 | _ => false)
adamc@403 65
adam@1639 66 fun validateCon env c =
adam@1639 67 (U.Con.appB {kind = fn env' => fn k => case k of
adam@1639 68 L'.KRel n => ignore (E.lookupKRel env' n)
adam@1639 69 | L'.KUnif (_, _, r as ref (L'.KUnknown f)) =>
adam@1639 70 r := L'.KUnknown (fn k => f k andalso validateKind env' k)
adam@1639 71 | _ => (),
adam@1639 72 con = fn env' => fn c => case c of
adam@1639 73 L'.CRel n => ignore (E.lookupCRel env' n)
adam@1639 74 | L'.CNamed n => ignore (E.lookupCNamed env' n)
adam@1639 75 | L'.CModProj (n, _, _) => ignore (E.lookupStrNamed env' n)
adam@1639 76 | L'.CUnif (_, _, _, _, r as ref (L'.Unknown f)) =>
adam@1639 77 r := L'.Unknown (fn c => f c andalso validateCon env' c)
adam@1639 78 | _ => (),
adam@1639 79 bind = fn (env', b) => case b of
adam@1639 80 U.Con.RelK x => E.pushKRel env' x
adam@1639 81 | U.Con.RelC (x, k) => E.pushCRel env' x k
adam@1639 82 | U.Con.NamedC (x, n, k, co) => E.pushCNamedAs env x n k co}
adam@1639 83 env c;
adam@1639 84 true)
adam@1639 85 handle _ => false
adam@1639 86
adam@1639 87 and validateKind env k = validateCon env (L'.CRecord (k, []), ErrorMsg.dummySpan)
adam@1639 88
adamc@403 89 exception KUnify' of kunify_error
adamc@403 90
adamc@623 91 fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
adamc@403 92 let
adamc@403 93 fun err f = raise KUnify' (f (k1All, k2All))
adamc@403 94 in
adamc@403 95 case (k1, k2) of
adamc@403 96 (L'.KType, L'.KType) => ()
adamc@403 97 | (L'.KUnit, L'.KUnit) => ()
adamc@403 98
adamc@403 99 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
adamc@623 100 (unifyKinds' env d1 d2;
adamc@623 101 unifyKinds' env r1 r2)
adamc@403 102 | (L'.KName, L'.KName) => ()
adamc@623 103 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' env k1 k2
adamc@403 104 | (L'.KTuple ks1, L'.KTuple ks2) =>
adamc@623 105 ((ListPair.appEq (fn (k1, k2) => unifyKinds' env k1 k2) (ks1, ks2))
adamc@403 106 handle ListPair.UnequalLengths => err KIncompatible)
adamc@403 107
adamc@623 108 | (L'.KRel n1, L'.KRel n2) =>
adamc@623 109 if n1 = n2 then
adamc@623 110 ()
adamc@623 111 else
adamc@623 112 err KIncompatible
adamc@623 113 | (L'.KFun (x, k1), L'.KFun (_, k2)) =>
adamc@623 114 unifyKinds' (E.pushKRel env x) k1 k2
adamc@623 115
adamc@403 116 | (L'.KError, _) => ()
adamc@403 117 | (_, L'.KError) => ()
adamc@403 118
adam@1639 119 | (L'.KUnif (_, _, ref (L'.KKnown k1All)), _) => unifyKinds' env k1All k2All
adam@1639 120 | (_, L'.KUnif (_, _, ref (L'.KKnown k2All))) => unifyKinds' env k1All k2All
adam@1639 121
adam@1639 122 | (L'.KTupleUnif (_, _, ref (L'.KKnown k)), _) => unifyKinds' env k k2All
adam@1639 123 | (_, L'.KTupleUnif (_, _, ref (L'.KKnown k))) => unifyKinds' env k1All k
adam@1639 124
adam@1639 125 | (L'.KUnif (_, _, r1 as ref (L'.KUnknown f1)), L'.KUnif (_, _, r2 as ref (L'.KUnknown f2))) =>
adamc@403 126 if r1 = r2 then
adamc@403 127 ()
adamc@403 128 else
adam@1639 129 (r1 := L'.KKnown k2All;
adam@1639 130 r2 := L'.KUnknown (fn x => f1 x andalso f2 x))
adam@1639 131
adam@1639 132 | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) =>
adamc@403 133 if occursKind r k2All then
adamc@403 134 err KOccursCheckFailed
adam@1639 135 else if not (f k2All) then
adam@1639 136 err KScope
adamc@403 137 else
adam@1639 138 r := L'.KKnown k2All
adam@1639 139 | (_, L'.KUnif (_, _, r as ref (L'.KUnknown f))) =>
adamc@403 140 if occursKind r k1All then
adamc@403 141 err KOccursCheckFailed
adam@1639 142 else if not (f k1All) then
adam@1639 143 err KScope
adamc@403 144 else
adam@1639 145 r := L'.KKnown k1All
adam@1639 146
adam@1639 147 | (L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f)), L'.KTuple ks) =>
adam@1639 148 if not (f k2All) then
adam@1639 149 err KScope
adam@1639 150 else
adam@1639 151 ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks;
adam@1639 152 r := L'.KKnown k2All)
adam@1639 153 handle Subscript => err KIncompatible)
adam@1639 154 | (L'.KTuple ks, L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f))) =>
adam@1639 155 if not (f k2All) then
adam@1639 156 err KScope
adam@1639 157 else
adam@1639 158 ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks;
adam@1639 159 r := L'.KKnown k1All)
adam@1639 160 handle Subscript => err KIncompatible)
adam@1639 161 | (L'.KTupleUnif (loc, nks1, r1 as ref (L'.KUnknown f1)), L'.KTupleUnif (_, nks2, r2 as ref (L'.KUnknown f2))) =>
adam@1302 162 let
adam@1302 163 val nks = foldl (fn (p as (n, k1), nks) =>
adam@1302 164 case ListUtil.search (fn (n', k2) =>
adam@1302 165 if n' = n then
adam@1302 166 SOME k2
adam@1302 167 else
adam@1302 168 NONE) nks2 of
adam@1302 169 NONE => p :: nks
adam@1302 170 | SOME k2 => (unifyKinds' env k1 k2;
adam@1302 171 nks)) nks2 nks1
adam@1302 172
adam@1639 173 val k = (L'.KTupleUnif (loc, nks, ref (L'.KUnknown (fn x => f1 x andalso f2 x))), loc)
adam@1302 174 in
adam@1639 175 r1 := L'.KKnown k;
adam@1639 176 r2 := L'.KKnown k
adam@1302 177 end
adam@1302 178
adamc@403 179 | _ => err KIncompatible
adamc@403 180 end
adamc@403 181
adamc@403 182 exception KUnify of L'.kind * L'.kind * kunify_error
adamc@403 183
adamc@623 184 fun unifyKinds env k1 k2 =
adamc@623 185 unifyKinds' env k1 k2
adamc@403 186 handle KUnify' err => raise KUnify (k1, k2, err)
adamc@403 187
adamc@403 188 fun checkKind env c k1 k2 =
adamc@623 189 unifyKinds env k1 k2
adamc@403 190 handle KUnify (k1, k2, err) =>
adamc@403 191 conError env (WrongKind (c, k1, k2, err))
adamc@403 192
adamc@403 193 val dummy = ErrorMsg.dummySpan
adamc@403 194
adamc@403 195 val ktype = (L'.KType, dummy)
adamc@403 196 val kname = (L'.KName, dummy)
adamc@403 197 val ktype_record = (L'.KRecord ktype, dummy)
adamc@403 198
adamc@403 199 val cerror = (L'.CError, dummy)
adamc@403 200 val kerror = (L'.KError, dummy)
adamc@403 201 val eerror = (L'.EError, dummy)
adamc@403 202 val sgnerror = (L'.SgnError, dummy)
adamc@403 203 val strerror = (L'.StrError, dummy)
adamc@403 204
adamc@403 205 val int = ref cerror
adamc@403 206 val float = ref cerror
adamc@403 207 val string = ref cerror
adamc@821 208 val char = ref cerror
adamc@403 209 val table = ref cerror
adamc@403 210
adam@1639 211
adamc@403 212 local
adamc@403 213 val count = ref 0
adamc@403 214 in
adamc@403 215
adamc@403 216 fun resetKunif () = count := 0
adamc@403 217
adam@1639 218 fun kunif' f loc =
adamc@403 219 let
adamc@403 220 val n = !count
adamc@403 221 val s = if n <= 26 then
adamc@403 222 str (chr (ord #"A" + n))
adamc@403 223 else
adamc@403 224 "U" ^ Int.toString (n - 26)
adamc@403 225 in
adamc@403 226 count := n + 1;
adam@1639 227 (L'.KUnif (loc, s, ref (L'.KUnknown f)), loc)
adamc@403 228 end
adamc@403 229
adam@1639 230 fun kunif env = kunif' (validateKind env)
adam@1639 231
adamc@403 232 end
adamc@403 233
adamc@403 234 local
adamc@403 235 val count = ref 0
adamc@403 236 in
adamc@403 237
adamc@403 238 fun resetCunif () = count := 0
adamc@403 239
adam@1639 240 fun cunif' f (loc, k) =
adamc@403 241 let
adamc@403 242 val n = !count
adamc@712 243 val s = if n < 26 then
adamc@403 244 str (chr (ord #"A" + n))
adamc@403 245 else
adamc@403 246 "U" ^ Int.toString (n - 26)
adamc@403 247 in
adamc@403 248 count := n + 1;
adam@1639 249 (L'.CUnif (0, loc, k, s, ref (L'.Unknown f)), loc)
adamc@403 250 end
adamc@403 251
adam@1639 252 fun cunif env = cunif' (validateCon env)
adam@1639 253
adamc@403 254 end
adamc@403 255
adamc@623 256 fun elabKind env (k, loc) =
adamc@403 257 case k of
adamc@403 258 L.KType => (L'.KType, loc)
adamc@623 259 | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc)
adamc@403 260 | L.KName => (L'.KName, loc)
adamc@623 261 | L.KRecord k => (L'.KRecord (elabKind env k), loc)
adamc@403 262 | L.KUnit => (L'.KUnit, loc)
adamc@623 263 | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc)
adam@1639 264 | L.KWild => kunif env loc
adamc@403 265
adamc@623 266 | L.KVar s => (case E.lookupK env s of
adamc@623 267 NONE =>
adamc@623 268 (kindError env (UnboundKind (loc, s));
adamc@623 269 kerror)
adamc@623 270 | SOME n => (L'.KRel n, loc))
adamc@623 271 | L.KFun (x, k) => (L'.KFun (x, elabKind (E.pushKRel env x) k), loc)
adamc@623 272
adamc@621 273 fun mapKind (dom, ran, loc)=
adamc@621 274 (L'.KArrow ((L'.KArrow (dom, ran), loc),
adamc@621 275 (L'.KArrow ((L'.KRecord dom, loc),
adamc@621 276 (L'.KRecord ran, loc)), loc)), loc)
adamc@403 277
adamc@403 278 fun hnormKind (kAll as (k, _)) =
adamc@403 279 case k of
adam@1639 280 L'.KUnif (_, _, ref (L'.KKnown k)) => hnormKind k
adamc@403 281 | _ => kAll
adamc@403 282
adamc@623 283 open ElabOps
adamc@623 284
adam@1639 285 fun elabConHead env (c as (_, loc)) k =
adamc@623 286 let
adamc@623 287 fun unravel (k, c) =
adamc@623 288 case hnormKind k of
adamc@623 289 (L'.KFun (x, k'), _) =>
adamc@623 290 let
adam@1639 291 val u = kunif env loc
adamc@623 292
adamc@623 293 val k'' = subKindInKind (0, u) k'
adamc@623 294 in
adamc@623 295 unravel (k'', (L'.CKApp (c, u), loc))
adamc@623 296 end
adamc@623 297 | _ => (c, k)
adamc@623 298 in
adamc@623 299 unravel (k, c)
adamc@623 300 end
adamc@623 301
adamc@403 302 fun elabCon (env, denv) (c, loc) =
adamc@403 303 case c of
adamc@403 304 L.CAnnot (c, k) =>
adamc@403 305 let
adamc@623 306 val k' = elabKind env k
adamc@403 307 val (c', ck, gs) = elabCon (env, denv) c
adamc@403 308 in
adamc@403 309 checkKind env c' ck k';
adamc@403 310 (c', k', gs)
adamc@403 311 end
adamc@403 312
adamc@403 313 | L.TFun (t1, t2) =>
adamc@403 314 let
adamc@403 315 val (t1', k1, gs1) = elabCon (env, denv) t1
adamc@403 316 val (t2', k2, gs2) = elabCon (env, denv) t2
adamc@403 317 in
adamc@403 318 checkKind env t1' k1 ktype;
adamc@403 319 checkKind env t2' k2 ktype;
adamc@403 320 ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2)
adamc@403 321 end
adamc@403 322 | L.TCFun (e, x, k, t) =>
adamc@403 323 let
adamc@403 324 val e' = elabExplicitness e
adamc@623 325 val k' = elabKind env k
adamc@403 326 val env' = E.pushCRel env x k'
adamc@403 327 val (t', tk, gs) = elabCon (env', D.enter denv) t
adamc@403 328 in
adamc@403 329 checkKind env t' tk ktype;
adamc@403 330 ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
adamc@403 331 end
adamc@623 332 | L.TKFun (x, t) =>
adamc@623 333 let
adamc@623 334 val env' = E.pushKRel env x
adamc@623 335 val (t', tk, gs) = elabCon (env', denv) t
adamc@623 336 in
adamc@623 337 checkKind env t' tk ktype;
adamc@623 338 ((L'.TKFun (x, t'), loc), ktype, gs)
adamc@623 339 end
adamc@628 340 | L.TDisjoint (c1, c2, c) =>
adamc@403 341 let
adamc@403 342 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@403 343 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@403 344
adam@1639 345 val ku1 = kunif env loc
adam@1639 346 val ku2 = kunif env loc
adamc@403 347
adamc@628 348 val denv' = D.assert env denv (c1', c2')
adamc@403 349 val (c', k, gs4) = elabCon (env, denv') c
adamc@403 350 in
adamc@403 351 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@403 352 checkKind env c2' k2 (L'.KRecord ku2, loc);
adam@1351 353 checkKind env c' k (L'.KType, loc);
adamc@403 354
adamc@628 355 ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs4)
adamc@403 356 end
adamc@403 357 | L.TRecord c =>
adamc@403 358 let
adamc@403 359 val (c', ck, gs) = elabCon (env, denv) c
adamc@403 360 val k = (L'.KRecord ktype, loc)
adamc@403 361 in
adamc@403 362 checkKind env c' ck k;
adamc@403 363 ((L'.TRecord c', loc), ktype, gs)
adamc@403 364 end
adamc@403 365
adamc@403 366 | L.CVar ([], s) =>
adamc@403 367 (case E.lookupC env s of
adamc@403 368 E.NotBound =>
adamc@403 369 (conError env (UnboundCon (loc, s));
adamc@403 370 (cerror, kerror, []))
adamc@403 371 | E.Rel (n, k) =>
adamc@623 372 let
adam@1639 373 val (c, k) = elabConHead env (L'.CRel n, loc) k
adamc@623 374 in
adamc@623 375 (c, k, [])
adamc@623 376 end
adamc@403 377 | E.Named (n, k) =>
adamc@623 378 let
adam@1639 379 val (c, k) = elabConHead env (L'.CNamed n, loc) k
adamc@623 380 in
adamc@623 381 (c, k, [])
adamc@623 382 end)
adamc@403 383 | L.CVar (m1 :: ms, s) =>
adamc@403 384 (case E.lookupStr env m1 of
adamc@403 385 NONE => (conError env (UnboundStrInCon (loc, m1));
adamc@403 386 (cerror, kerror, []))
adamc@403 387 | SOME (n, sgn) =>
adamc@403 388 let
adamc@403 389 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@403 390 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@403 391 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@403 392 (strerror, sgnerror))
adamc@403 393 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@403 394 ((L'.StrVar n, loc), sgn) ms
adamc@403 395
adamc@403 396 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
adamc@403 397 NONE => (conError env (UnboundCon (loc, s));
adamc@403 398 kerror)
adamc@403 399 | SOME (k, _) => k
adam@1639 400 val (c, k) = elabConHead env (L'.CModProj (n, ms, s), loc) k
adamc@403 401 in
adamc@987 402 (c, k, [])
adamc@403 403 end)
adamc@403 404
adamc@403 405 | L.CApp (c1, c2) =>
adamc@403 406 let
adamc@403 407 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@403 408 val (c2', k2, gs2) = elabCon (env, denv) c2
adam@1639 409 val dom = kunif env loc
adam@1639 410 val ran = kunif env loc
adamc@403 411 in
adamc@403 412 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
adamc@403 413 checkKind env c2' k2 dom;
adamc@403 414 ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2)
adamc@403 415 end
adamc@403 416 | L.CAbs (x, ko, t) =>
adamc@403 417 let
adamc@403 418 val k' = case ko of
adam@1639 419 NONE => kunif env loc
adamc@623 420 | SOME k => elabKind env k
adamc@403 421 val env' = E.pushCRel env x k'
adamc@403 422 val (t', tk, gs) = elabCon (env', D.enter denv) t
adamc@403 423 in
adamc@403 424 ((L'.CAbs (x, k', t'), loc),
adamc@403 425 (L'.KArrow (k', tk), loc),
adamc@403 426 gs)
adamc@403 427 end
adamc@623 428 | L.CKAbs (x, t) =>
adamc@623 429 let
adamc@623 430 val env' = E.pushKRel env x
adamc@623 431 val (t', tk, gs) = elabCon (env', denv) t
adamc@623 432 in
adamc@623 433 ((L'.CKAbs (x, t'), loc),
adamc@623 434 (L'.KFun (x, tk), loc),
adamc@623 435 gs)
adamc@623 436 end
adamc@403 437
adamc@403 438 | L.CName s =>
adamc@403 439 ((L'.CName s, loc), kname, [])
adamc@403 440
adamc@403 441 | L.CRecord xcs =>
adamc@403 442 let
adam@1639 443 val k = kunif env loc
adamc@403 444
adamc@403 445 val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
adamc@403 446 let
adamc@403 447 val (x', xk, gs1) = elabCon (env, denv) x
adamc@403 448 val (c', ck, gs2) = elabCon (env, denv) c
adamc@403 449 in
adamc@403 450 checkKind env x' xk kname;
adamc@403 451 checkKind env c' ck k;
adamc@403 452 ((x', c'), gs1 @ gs2 @ gs)
adamc@403 453 end) [] xcs
adamc@403 454
adamc@403 455 val rc = (L'.CRecord (k, xcs'), loc)
adamc@403 456 (* Add duplicate field checking later. *)
adamc@403 457
adamc@403 458 fun prove (xcs, ds) =
adamc@403 459 case xcs of
adamc@403 460 [] => ds
adamc@403 461 | xc :: rest =>
adamc@403 462 let
adamc@403 463 val r1 = (L'.CRecord (k, [xc]), loc)
adamc@403 464 val ds = foldl (fn (xc', ds) =>
adamc@403 465 let
adamc@403 466 val r2 = (L'.CRecord (k, [xc']), loc)
adamc@403 467 in
adamc@403 468 D.prove env denv (r1, r2, loc) @ ds
adamc@403 469 end)
adamc@403 470 ds rest
adamc@403 471 in
adamc@403 472 prove (rest, ds)
adamc@403 473 end
adamc@403 474 in
adamc@403 475 (rc, (L'.KRecord k, loc), prove (xcs', gs))
adamc@403 476 end
adamc@403 477 | L.CConcat (c1, c2) =>
adamc@403 478 let
adamc@403 479 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@403 480 val (c2', k2, gs2) = elabCon (env, denv) c2
adam@1639 481 val ku = kunif env loc
adamc@403 482 val k = (L'.KRecord ku, loc)
adamc@403 483 in
adamc@403 484 checkKind env c1' k1 k;
adamc@403 485 checkKind env c2' k2 k;
adamc@403 486 ((L'.CConcat (c1', c2'), loc), k,
adamc@403 487 D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
adamc@403 488 end
adamc@621 489 | L.CMap =>
adamc@403 490 let
adam@1639 491 val dom = kunif env loc
adam@1639 492 val ran = kunif env loc
adamc@403 493 in
adamc@621 494 ((L'.CMap (dom, ran), loc),
adamc@621 495 mapKind (dom, ran, loc),
adamc@403 496 [])
adamc@403 497 end
adamc@403 498
adamc@403 499 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
adamc@403 500
adamc@403 501 | L.CTuple cs =>
adamc@403 502 let
adamc@403 503 val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) =>
adamc@403 504 let
adamc@403 505 val (c', k, gs') = elabCon (env, denv) c
adamc@403 506 in
adamc@403 507 (c' :: cs', k :: ks, gs' @ gs)
adamc@403 508 end) ([], [], []) cs
adamc@403 509 in
adamc@403 510 ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs)
adamc@403 511 end
adamc@403 512 | L.CProj (c, n) =>
adamc@403 513 let
adamc@403 514 val (c', k, gs) = elabCon (env, denv) c
adam@1302 515
adam@1639 516 val k' = kunif env loc
adamc@403 517 in
adam@1302 518 if n <= 0 then
adam@1302 519 (conError env (ProjBounds (c', n));
adam@1302 520 (cerror, kerror, []))
adam@1302 521 else
adam@1639 522 (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref (L'.KUnknown (validateKind env))), loc);
adam@1302 523 ((L'.CProj (c', n), loc), k', gs))
adamc@403 524 end
adamc@403 525
adamc@403 526 | L.CWild k =>
adamc@403 527 let
adamc@623 528 val k' = elabKind env k
adamc@403 529 in
adam@1639 530 (cunif env (loc, k'), k', [])
adamc@403 531 end
adamc@403 532
adamc@403 533 fun kunifsRemain k =
adamc@403 534 case k of
adam@1639 535 L'.KUnif (_, _, ref (L'.KUnknown _)) => true
adam@1639 536 | L'.KTupleUnif (_, _, ref (L'.KUnknown _)) => true
adamc@403 537 | _ => false
adamc@403 538 fun cunifsRemain c =
adamc@403 539 case c of
adam@1639 540 L'.CUnif (_, loc, k, _, r as ref (L'.Unknown _)) =>
adam@1326 541 (case #1 (hnormKind k) of
adam@1639 542 L'.KUnit => (r := L'.Known (L'.CUnit, loc); false)
adam@1584 543 | _ => true)
adam@1584 544 | _ => false
adamc@403 545
adamc@403 546 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
adamc@403 547 con = fn _ => false,
adamc@403 548 exp = fn _ => false,
adamc@403 549 sgn_item = fn _ => false,
adamc@403 550 sgn = fn _ => false,
adamc@403 551 str = fn _ => false,
adamc@403 552 decl = fn _ => false}
adamc@403 553
adam@1584 554 val cunifsInDecl = U.Decl.exists {kind = fn _ => false,
adamc@403 555 con = cunifsRemain,
adam@1584 556 exp = fn _ => false,
adam@1584 557 sgn_item = fn _ => false,
adam@1584 558 sgn = fn _ => false,
adam@1584 559 str = fn _ => false,
adam@1584 560 decl = fn _ => false}
adamc@403 561
adamc@403 562 fun occursCon r =
adamc@403 563 U.Con.exists {kind = fn _ => false,
adam@1303 564 con = fn L'.CUnif (_, _, _, _, r') => r = r'
adamc@403 565 | _ => false}
adamc@403 566
adamc@403 567 exception CUnify' of cunify_error
adamc@403 568
adamc@403 569 type record_summary = {
adamc@403 570 fields : (L'.con * L'.con) list,
adam@1639 571 unifs : (L'.con * L'.cunif ref) list,
adamc@403 572 others : L'.con list
adamc@403 573 }
adamc@403 574
adamc@403 575 fun summaryToCon {fields, unifs, others} =
adamc@403 576 let
adam@1626 577 fun concat (c1, c2) =
adam@1626 578 case #1 c1 of
adam@1626 579 L'.CRecord (_, []) => c2
adam@1626 580 | _ => case #1 c2 of
adam@1626 581 L'.CRecord (_, []) => c1
adam@1626 582 | _ => (L'.CConcat (c1, c2), dummy)
adam@1626 583
adamc@403 584 val c = (L'.CRecord (ktype, []), dummy)
adam@1626 585 val c = List.foldr concat c others
adam@1626 586 val c = List.foldr (fn ((c', _), c) => concat (c', c)) c unifs
adamc@403 587 in
adam@1626 588 concat ((L'.CRecord (ktype, fields), dummy), c)
adamc@403 589 end
adamc@403 590
adamc@403 591 fun p_summary env s = p_con env (summaryToCon s)
adamc@403 592
adamc@403 593 exception CUnify of L'.con * L'.con * cunify_error
adamc@403 594
adamc@403 595 fun kindof env (c, loc) =
adamc@403 596 case c of
adamc@403 597 L'.TFun _ => ktype
adamc@403 598 | L'.TCFun _ => ktype
adamc@403 599 | L'.TRecord _ => ktype
adamc@628 600 | L'.TDisjoint _ => ktype
adamc@403 601
adamc@403 602 | L'.CRel xn => #2 (E.lookupCRel env xn)
adamc@403 603 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
adamc@403 604 | L'.CModProj (n, ms, x) =>
adamc@403 605 let
adamc@403 606 val (_, sgn) = E.lookupStrNamed env n
adamc@403 607 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@403 608 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@403 609 NONE => raise Fail "kindof: Unknown substructure"
adamc@403 610 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@403 611 ((L'.StrVar n, loc), sgn) ms
adamc@403 612 in
adamc@403 613 case E.projectCon env {sgn = sgn, str = str, field = x} of
adamc@403 614 NONE => raise Fail "kindof: Unknown con in structure"
adamc@403 615 | SOME (k, _) => k
adamc@403 616 end
adamc@403 617
adamc@403 618 | L'.CApp (c, _) =>
adamc@403 619 (case hnormKind (kindof env c) of
adamc@403 620 (L'.KArrow (_, k), _) => k
adamc@403 621 | (L'.KError, _) => kerror
adamc@413 622 | k => raise CUnify' (CKindof (k, c, "arrow")))
adamc@403 623 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
adamc@628 624
adamc@403 625
adamc@403 626 | L'.CName _ => kname
adamc@403 627
adamc@403 628 | L'.CRecord (k, _) => (L'.KRecord k, loc)
adamc@403 629 | L'.CConcat (c, _) => kindof env c
adamc@621 630 | L'.CMap (dom, ran) => mapKind (dom, ran, loc)
adamc@403 631
adamc@403 632 | L'.CUnit => (L'.KUnit, loc)
adamc@403 633
adamc@403 634 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
adamc@403 635 | L'.CProj (c, n) =>
adamc@403 636 (case hnormKind (kindof env c) of
adamc@403 637 (L'.KTuple ks, _) => List.nth (ks, n - 1)
adam@1311 638 | (L'.KUnif (_, _, r), _) =>
adam@1311 639 let
adam@1639 640 val ku = kunif env loc
adam@1639 641 val k = (L'.KTupleUnif (loc, [(n, ku)], r), loc)
adam@1311 642 in
adam@1639 643 r := L'.KKnown k;
adam@1311 644 k
adam@1311 645 end
adam@1311 646 | (L'.KTupleUnif (_, nks, r), _) =>
adam@1311 647 (case ListUtil.search (fn (n', k) => if n' = n then SOME k else NONE) nks of
adam@1311 648 SOME k => k
adam@1311 649 | NONE =>
adam@1311 650 let
adam@1639 651 val ku = kunif env loc
adam@1639 652 val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), r), loc)
adam@1311 653 in
adam@1639 654 r := L'.KKnown k;
adam@1311 655 k
adam@1311 656 end)
adamc@413 657 | k => raise CUnify' (CKindof (k, c, "tuple")))
adamc@403 658
adamc@403 659 | L'.CError => kerror
adam@1303 660 | L'.CUnif (_, _, k, _, _) => k
adamc@403 661
adamc@623 662 | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc)
adamc@623 663 | L'.CKApp (c, k) =>
adamc@623 664 (case hnormKind (kindof env c) of
adamc@623 665 (L'.KFun (_, k'), _) => subKindInKind (0, k) k'
adamc@623 666 | k => raise CUnify' (CKindof (k, c, "kapp")))
adamc@623 667 | L'.TKFun _ => ktype
adamc@403 668
adamc@621 669 exception GuessFailure
adamc@403 670
adamc@513 671 fun isUnitCon env (c, loc) =
adamc@513 672 case c of
adamc@513 673 L'.TFun _ => false
adamc@513 674 | L'.TCFun _ => false
adamc@513 675 | L'.TRecord _ => false
adamc@628 676 | L'.TDisjoint _ => false
adamc@513 677
adam@1316 678 | L'.CRel xn => #1 (hnormKind (#2 (E.lookupCRel env xn))) = L'.KUnit
adam@1316 679 | L'.CNamed xn => #1 (hnormKind (#2 (E.lookupCNamed env xn))) = L'.KUnit
adamc@518 680 | L'.CModProj (n, ms, x) => false
adamc@518 681 (*let
adamc@513 682 val (_, sgn) = E.lookupStrNamed env n
adamc@513 683 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@513 684 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@513 685 NONE => raise Fail "kindof: Unknown substructure"
adamc@513 686 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@513 687 ((L'.StrVar n, loc), sgn) ms
adamc@513 688 in
adamc@513 689 case E.projectCon env {sgn = sgn, str = str, field = x} of
adamc@513 690 NONE => raise Fail "kindof: Unknown con in structure"
adamc@513 691 | SOME ((k, _), _) => k = L'.KUnit
adamc@518 692 end*)
adamc@518 693
adamc@518 694 | L'.CApp (c, _) => false
adamc@518 695 (*(case hnormKind (kindof env c) of
adamc@513 696 (L'.KArrow (_, k), _) => #1 k = L'.KUnit
adamc@513 697 | (L'.KError, _) => false
adamc@518 698 | k => raise CUnify' (CKindof (k, c, "arrow")))*)
adamc@513 699 | L'.CAbs _ => false
adamc@513 700
adamc@513 701 | L'.CName _ => false
adamc@513 702
adamc@513 703 | L'.CRecord _ => false
adamc@513 704 | L'.CConcat _ => false
adamc@621 705 | L'.CMap _ => false
adamc@513 706
adamc@513 707 | L'.CUnit => true
adamc@513 708
adamc@513 709 | L'.CTuple _ => false
adamc@518 710 | L'.CProj (c, n) => false
adamc@518 711 (*(case hnormKind (kindof env c) of
adamc@513 712 (L'.KTuple ks, _) => #1 (List.nth (ks, n - 1)) = L'.KUnit
adamc@518 713 | k => raise CUnify' (CKindof (k, c, "tuple")))*)
adamc@513 714
adamc@513 715 | L'.CError => false
adam@1316 716 | L'.CUnif (_, _, k, _, _) => #1 (hnormKind k) = L'.KUnit
adamc@513 717
adamc@623 718 | L'.CKAbs _ => false
adamc@623 719 | L'.CKApp _ => false
adamc@623 720 | L'.TKFun _ => false
adamc@623 721
adamc@709 722 val recdCounter = ref 0
adamc@709 723
adamc@713 724 val mayDelay = ref false
adamc@777 725 val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list)
adamc@777 726
adamc@830 727 val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list)
adamc@830 728
adam@1304 729 exception CantSquish
adam@1304 730
adam@1304 731 fun squish by =
adam@1304 732 U.Con.mapB {kind = fn _ => fn k => k,
adam@1304 733 con = fn bound => fn c =>
adam@1304 734 case c of
adam@1304 735 L'.CRel xn =>
adam@1304 736 if xn < bound then
adam@1304 737 c
adam@1304 738 else if bound <= xn andalso xn < bound + by then
adam@1304 739 raise CantSquish
adam@1304 740 else
adam@1304 741 L'.CRel (xn - by)
adam@1304 742 | L'.CUnif _ => raise CantSquish
adam@1304 743 | _ => c,
adam@1304 744 bind = fn (bound, U.Con.RelC _) => bound + 1
adam@1304 745 | (bound, _) => bound} 0
adam@1304 746
adam@1582 747 val reducedSummaries = ref (NONE : (Print.PD.pp_desc * Print.PD.pp_desc) option)
adam@1582 748
adamc@777 749 fun unifyRecordCons env (loc, c1, c2) =
adamc@403 750 let
adamc@403 751 fun rkindof c =
adamc@403 752 case hnormKind (kindof env c) of
adamc@403 753 (L'.KRecord k, _) => k
adamc@403 754 | (L'.KError, _) => kerror
adam@1639 755 | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) =>
adamc@753 756 let
adam@1639 757 val k = kunif' f (#2 c)
adamc@753 758 in
adam@1639 759 r := L'.KKnown (L'.KRecord k, #2 c);
adamc@753 760 k
adamc@753 761 end
adamc@413 762 | k => raise CUnify' (CKindof (k, c, "record"))
adamc@403 763
adamc@403 764 val k1 = rkindof c1
adamc@403 765 val k2 = rkindof c2
adamc@403 766
adamc@628 767 val r1 = recordSummary env c1
adamc@628 768 val r2 = recordSummary env c2
adamc@403 769 in
adamc@623 770 unifyKinds env k1 k2;
adamc@777 771 unifySummaries env (loc, k1, r1, r2)
adamc@403 772 end
adamc@403 773
adamc@777 774 and normalizeRecordSummary env (r : record_summary) =
adamc@777 775 recordSummary env (summaryToCon r)
adamc@777 776
adamc@628 777 and recordSummary env c =
adamc@403 778 let
adamc@628 779 val c = hnormCon env c
adamc@628 780
adamc@628 781 val sum =
adamc@403 782 case c of
adamc@628 783 (L'.CRecord (_, xcs), _) => {fields = xcs, unifs = [], others = []}
adamc@403 784 | (L'.CConcat (c1, c2), _) =>
adamc@403 785 let
adamc@628 786 val s1 = recordSummary env c1
adamc@628 787 val s2 = recordSummary env c2
adamc@403 788 in
adamc@628 789 {fields = #fields s1 @ #fields s2,
adamc@628 790 unifs = #unifs s1 @ #unifs s2,
adamc@628 791 others = #others s1 @ #others s2}
adamc@403 792 end
adam@1639 793 | (L'.CUnif (nl, _, _, _, ref (L'.Known c)), _) => recordSummary env (E.mliftConInCon nl c)
adam@1303 794 | c' as (L'.CUnif (0, _, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
adamc@628 795 | c' => {fields = [], unifs = [], others = [c']}
adamc@403 796 in
adamc@628 797 sum
adamc@403 798 end
adamc@403 799
adamc@987 800 and consEq env loc (c1, c2) =
adamc@777 801 let
adamc@777 802 val mayDelay' = !mayDelay
adamc@777 803 in
adamc@777 804 (mayDelay := false;
adamc@987 805 unifyCons env loc c1 c2;
adamc@777 806 mayDelay := mayDelay';
adamc@777 807 true)
adamc@777 808 handle CUnify _ => (mayDelay := mayDelay'; false)
adamc@777 809 end
adamc@403 810
adamc@403 811 and consNeq env (c1, c2) =
adamc@628 812 case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of
adamc@403 813 (L'.CName x1, L'.CName x2) => x1 <> x2
adamc@1093 814 | (L'.CName _, L'.CRel _) => true
adamc@1093 815 | (L'.CRel _, L'.CName _) => true
adamc@1093 816 | (L'.CRel n1, L'.CRel n2) => n1 <> n2
adamc@1093 817 | (L'.CRel _, L'.CNamed _) => true
adamc@1093 818 | (L'.CNamed _, L'.CRel _) => true
adamc@1093 819 | (L'.CRel _, L'.CModProj _) => true
adamc@1093 820 | (L'.CModProj _, L'.CRel _) => true
adamc@1269 821 | (L'.CModProj (_, _, n1), L'.CModProj (_, _, n2)) => n1 <> n2
adam@1589 822 | (L'.CModProj _, L'.CName _) => true
adam@1589 823 | (L'.CName _, L'.CModProj _) => true
adam@1589 824 | (L'.CNamed _, L'.CName _) => true
adam@1589 825 | (L'.CName _, L'.CNamed _) => true
adamc@403 826 | _ => false
adamc@403 827
adamc@777 828 and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) =
adamc@403 829 let
adam@1583 830 val () = reducedSummaries := NONE
adam@1583 831
adamc@848 832 (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)),
adam@1303 833 ("#1", p_summary env s1),
adam@1303 834 ("#2", p_summary env s2)]*)
adamc@403 835
adamc@403 836 fun eatMatching p (ls1, ls2) =
adamc@403 837 let
adamc@403 838 fun em (ls1, ls2, passed1) =
adamc@403 839 case ls1 of
adamc@403 840 [] => (rev passed1, ls2)
adamc@403 841 | h1 :: t1 =>
adamc@403 842 let
adamc@403 843 fun search (ls2', passed2) =
adamc@403 844 case ls2' of
adamc@403 845 [] => em (t1, ls2, h1 :: passed1)
adamc@403 846 | h2 :: t2 =>
adamc@403 847 if p (h1, h2) then
adamc@403 848 em (t1, List.revAppend (passed2, t2), passed1)
adamc@403 849 else
adamc@403 850 search (t2, h2 :: passed2)
adamc@403 851 in
adamc@403 852 search (ls2, [])
adamc@403 853 end
adamc@403 854 in
adamc@403 855 em (ls1, ls2, [])
adamc@403 856 end
adamc@403 857
adamc@403 858 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
adamc@403 859 not (consNeq env (x1, x2))
adamc@987 860 andalso consEq env loc (c1, c2)
adamc@987 861 andalso consEq env loc (x1, x2))
adamc@403 862 (#fields s1, #fields s2)
adamc@403 863 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
adamc@403 864 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
adamc@646 865
adamc@403 866 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
adamc@646 867
adamc@987 868 val (others1, others2) = eatMatching (consEq env loc) (#others s1, #others s2)
adamc@403 869 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
adamc@403 870 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
adamc@403 871
adamc@709 872 fun unsummarize {fields, unifs, others} =
adamc@709 873 let
adamc@709 874 val c = (L'.CRecord (k, fields), loc)
adamc@709 875
adamc@709 876 val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
adamc@709 877 c unifs
adamc@709 878 in
adamc@709 879 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
adamc@709 880 c others
adamc@709 881 end
adamc@709 882
adamc@710 883 val empties = ([], [], [], [], [], [])
adamc@710 884
adamc@709 885 val (unifs1, fs1, others1, unifs2, fs2, others2) =
adamc@709 886 case (unifs1, fs1, others1, unifs2, fs2, others2) of
adam@1639 887 orig as ([(_, r as ref (L'.Unknown f))], [], [], _, _, _) =>
adamc@709 888 let
adamc@709 889 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
adamc@709 890 in
adam@1639 891 if occursCon r c orelse not (f c) then
adamc@709 892 orig
adamc@709 893 else
adam@1639 894 (r := L'.Known c;
adamc@710 895 empties)
adamc@709 896 end
adam@1639 897 | orig as (_, _, _, [(_, r as ref (L'.Unknown f))], [], []) =>
adamc@709 898 let
adamc@709 899 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
adamc@709 900 in
adam@1639 901 if occursCon r c orelse not (f c) then
adamc@709 902 orig
adamc@709 903 else
adam@1639 904 (r := L'.Known c;
adamc@710 905 empties)
adamc@709 906 end
adam@1639 907 | orig as ([(_, r1 as ref (L'.Unknown f1))], _, [], [(_, r2 as ref (L'.Unknown f2))], _, []) =>
adamc@710 908 if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then
adamc@710 909 let
adamc@838 910 val kr = (L'.KRecord k, loc)
adam@1639 911 val u = cunif env (loc, kr)
adam@1639 912
adam@1639 913 val c1 = (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc)
adam@1639 914 val c2 = (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc)
adamc@710 915 in
adam@1639 916 if not (f1 c1) orelse not (f2 c2) then
adam@1639 917 orig
adam@1639 918 else
adam@1639 919 (r1 := L'.Known c1;
adam@1639 920 r2 := L'.Known c2;
adam@1639 921 empties)
adamc@710 922 end
adamc@710 923 else
adamc@710 924 orig
adamc@709 925 | orig => orig
adamc@709 926
adamc@403 927 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
adamc@777 928 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
adamc@403 929
adamc@753 930 fun isGuessable (other, fs, unifs) =
adamc@753 931 let
adamc@753 932 val c = (L'.CRecord (k, fs), loc)
adamc@753 933 val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs
adamc@753 934 in
adamc@987 935 (guessMap env loc (other, c, GuessFailure);
adamc@753 936 true)
adamc@753 937 handle GuessFailure => false
adamc@753 938 end
adamc@403 939
adamc@754 940 val (fs1, fs2, others1, others2, unifs1, unifs2) =
adamc@753 941 case (fs1, fs2, others1, others2, unifs1, unifs2) of
adamc@753 942 ([], _, [other1], [], [], _) =>
adamc@753 943 if isGuessable (other1, fs2, unifs2) then
adamc@754 944 ([], [], [], [], [], [])
adamc@403 945 else
adamc@754 946 (fs1, fs2, others1, others2, unifs1, unifs2)
adamc@753 947 | (_, [], [], [other2], _, []) =>
adamc@777 948 if isGuessable (other2, fs1, unifs1) then
adamc@777 949 ([], [], [], [], [], [])
adamc@777 950 else
adamc@777 951 (fs1, fs2, others1, others2, unifs1, unifs2)
adamc@754 952 | _ => (fs1, fs2, others1, others2, unifs1, unifs2)
adamc@403 953
adam@1582 954 val () = if !mayDelay then
adam@1582 955 ()
adam@1582 956 else
adam@1626 957 let
adam@1626 958 val c1 = summaryToCon {fields = fs1, unifs = unifs1, others = others1}
adam@1626 959 val c2 = summaryToCon {fields = fs2, unifs = unifs2, others = others2}
adam@1626 960 in
adam@1626 961 case (c1, c2) of
adam@1626 962 ((L'.CRecord (_, []), _), (L'.CRecord (_, []), _)) => reducedSummaries := NONE
adam@1626 963 | _ => reducedSummaries := SOME (p_con env c1, p_con env c2)
adam@1626 964 end
adam@1582 965
adamc@403 966 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
adamc@646 967 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
adamc@403 968
adamc@838 969 val empty = (L'.CRecord (k, []), loc)
adamc@1071 970 fun failure () =
adamc@1071 971 let
adamc@1071 972 val fs2 = #fields s2
adamc@1071 973
adamc@1071 974 fun findPointwise fs1 =
adamc@1071 975 case fs1 of
adamc@1071 976 [] => NONE
adamc@1071 977 | (nm1, c1) :: fs1 =>
adamc@1071 978 case List.find (fn (nm2, _) => consEq env loc (nm1, nm2)) fs2 of
adamc@1071 979 NONE => findPointwise fs1
adamc@1071 980 | SOME (_, c2) =>
adamc@1071 981 if consEq env loc (c1, c2) then
adamc@1071 982 findPointwise fs1
adamc@1071 983 else
adam@1588 984 SOME (nm1, c1, c2, (unifyCons env loc c1 c2; NONE)
adam@1588 985 handle CUnify (_, _, err) => (reducedSummaries := NONE;
adam@1588 986 SOME err))
adamc@1071 987 in
adamc@1071 988 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1)))
adamc@1071 989 end
adam@1341 990
adam@1341 991 fun default () = if !mayDelay then
adam@1341 992 delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs
adam@1341 993 else
adam@1341 994 failure ()
adamc@709 995 in
adamc@777 996 (case (unifs1, fs1, others1, unifs2, fs2, others2) of
adamc@777 997 (_, [], [], [], [], []) =>
adam@1639 998 app (fn (_, r) => r := L'.Known empty) unifs1
adamc@777 999 | ([], [], [], _, [], []) =>
adam@1639 1000 app (fn (_, r) => r := L'.Known empty) unifs2
adam@1639 1001 | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)]) =>
adam@1341 1002 let
adam@1341 1003 val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1}
adam@1341 1004 in
adam@1341 1005 if occursCon r c then
adam@1588 1006 (reducedSummaries := NONE;
adam@1588 1007 raise CUnify' (COccursCheckFailed (cr, c)))
adam@1341 1008 else
adam@1639 1009 let
adam@1639 1010 val sq = squish nl c
adam@1639 1011 in
adam@1639 1012 if not (f sq) then
adam@1639 1013 default ()
adam@1639 1014 else
adam@1639 1015 r := L'.Known sq
adam@1639 1016 end
adam@1341 1017 handle CantSquish => default ()
adam@1341 1018 end
adam@1639 1019 | ([], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)], _, _, _) =>
adam@1341 1020 let
adam@1341 1021 val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2}
adam@1341 1022 in
adam@1341 1023 if occursCon r c then
adam@1588 1024 (reducedSummaries := NONE;
adam@1588 1025 raise CUnify' (COccursCheckFailed (cr, c)))
adam@1341 1026 else
adam@1639 1027 let
adam@1639 1028 val sq = squish nl c
adam@1639 1029 in
adam@1639 1030 if not (f sq) then
adam@1639 1031 default ()
adam@1639 1032 else
adam@1639 1033 r := L'.Known sq
adam@1639 1034 end
adam@1341 1035 handle CantSquish => default ()
adam@1341 1036 end
adam@1341 1037 | _ => default ())
adam@1341 1038
adamc@777 1039 (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)),
adamc@777 1040 ("#2", p_summary env (normalizeRecordSummary env s2))]*)
adamc@403 1041 end
adamc@403 1042
adamc@987 1043 and guessMap env loc (c1, c2, ex) =
adamc@403 1044 let
adamc@621 1045 fun unfold (dom, ran, f, r, c) =
adamc@403 1046 let
adamc@621 1047 fun unfold (r, c) =
adamc@754 1048 case #1 (hnormCon env c) of
adamc@987 1049 L'.CRecord (_, []) => unifyCons env loc r (L'.CRecord (dom, []), loc)
adamc@628 1050 | L'.CRecord (_, [(x, v)]) =>
adamc@628 1051 let
adamc@628 1052 val v' = case dom of
adamc@628 1053 (L'.KUnit, _) => (L'.CUnit, loc)
adam@1639 1054 | _ => cunif env (loc, dom)
adamc@628 1055 in
adamc@987 1056 unifyCons env loc v (L'.CApp (f, v'), loc);
adamc@987 1057 unifyCons env loc r (L'.CRecord (dom, [(x, v')]), loc)
adamc@628 1058 end
adamc@628 1059 | L'.CRecord (_, (x, v) :: rest) =>
adamc@628 1060 let
adam@1639 1061 val r1 = cunif env (loc, (L'.KRecord dom, loc))
adam@1639 1062 val r2 = cunif env (loc, (L'.KRecord dom, loc))
adamc@628 1063 in
adamc@628 1064 unfold (r1, (L'.CRecord (ran, [(x, v)]), loc));
adamc@628 1065 unfold (r2, (L'.CRecord (ran, rest), loc));
adamc@987 1066 unifyCons env loc r (L'.CConcat (r1, r2), loc)
adamc@628 1067 end
adamc@628 1068 | L'.CConcat (c1', c2') =>
adamc@628 1069 let
adam@1639 1070 val r1 = cunif env (loc, (L'.KRecord dom, loc))
adam@1639 1071 val r2 = cunif env (loc, (L'.KRecord dom, loc))
adamc@628 1072 in
adamc@628 1073 unfold (r1, c1');
adamc@628 1074 unfold (r2, c2');
adamc@987 1075 unifyCons env loc r (L'.CConcat (r1, r2), loc)
adamc@628 1076 end
adam@1639 1077 | L'.CUnif (0, _, _, _, ur as ref (L'.Unknown rf)) =>
adam@1639 1078 let
adam@1639 1079 val c' = (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
adam@1639 1080 in
adam@1639 1081 if not (rf c') then
adam@1639 1082 cunifyError env (CScope (c, c'))
adam@1639 1083 else
adam@1639 1084 ur := L'.Known c'
adam@1639 1085 end
adamc@628 1086 | _ => raise ex
adamc@403 1087 in
adamc@621 1088 unfold (r, c)
adamc@403 1089 end
adamc@632 1090 handle _ => raise ex
adamc@403 1091 in
adamc@403 1092 case (#1 c1, #1 c2) of
adamc@621 1093 (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
adamc@621 1094 unfold (dom, ran, f, r, c2)
adamc@621 1095 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>
adamc@621 1096 unfold (dom, ran, f, r, c1)
adamc@403 1097 | _ => raise ex
adamc@403 1098 end
adamc@403 1099
adamc@987 1100 and unifyCons' env loc c1 c2 =
adamc@628 1101 if isUnitCon env c1 andalso isUnitCon env c2 then
adamc@628 1102 ()
adamc@628 1103 else
adamc@403 1104 let
adamc@628 1105 (*val befor = Time.now ()
adamc@628 1106 val old1 = c1
adamc@628 1107 val old2 = c2*)
adamc@628 1108 val c1 = hnormCon env c1
adamc@628 1109 val c2 = hnormCon env c2
adamc@403 1110 in
adamc@987 1111 unifyCons'' env loc c1 c2
adamc@987 1112 handle ex => guessMap env loc (c1, c2, ex)
adamc@403 1113 end
adamc@628 1114
adamc@987 1115 and unifyCons'' env loc (c1All as (c1, _)) (c2All as (c2, _)) =
adamc@403 1116 let
adamc@403 1117 fun err f = raise CUnify' (f (c1All, c2All))
adamc@403 1118
adamc@706 1119 fun projSpecial1 (c1, n1, onFail) =
adamc@403 1120 let
adamc@632 1121 fun trySnd () =
adamc@632 1122 case #1 (hnormCon env c2All) of
adamc@632 1123 L'.CProj (c2, n2) =>
adamc@632 1124 let
adamc@632 1125 fun tryNormal () =
adamc@632 1126 if n1 = n2 then
adamc@987 1127 unifyCons' env loc c1 c2
adamc@632 1128 else
adamc@706 1129 onFail ()
adamc@632 1130 in
adamc@632 1131 case #1 (hnormCon env c2) of
adam@1639 1132 L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
adamc@632 1133 (case #1 (hnormKind k) of
adamc@632 1134 L'.KTuple ks =>
adamc@632 1135 let
adamc@632 1136 val loc = #2 c2
adam@1639 1137 val us = map (fn k => cunif' f (loc, k)) ks
adamc@632 1138 in
adam@1639 1139 r := L'.Known (L'.CTuple us, loc);
adamc@987 1140 unifyCons' env loc c1All (List.nth (us, n2 - 1))
adamc@632 1141 end
adamc@632 1142 | _ => tryNormal ())
adamc@632 1143 | _ => tryNormal ()
adamc@632 1144 end
adamc@706 1145 | _ => onFail ()
adamc@403 1146 in
adamc@632 1147 case #1 (hnormCon env c1) of
adam@1639 1148 L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
adamc@632 1149 (case #1 (hnormKind k) of
adamc@632 1150 L'.KTuple ks =>
adamc@632 1151 let
adamc@632 1152 val loc = #2 c1
adam@1639 1153 val us = map (fn k => cunif' f (loc, k)) ks
adamc@632 1154 in
adam@1639 1155 r := L'.Known (L'.CTuple us, loc);
adamc@987 1156 unifyCons' env loc (List.nth (us, n1 - 1)) c2All
adamc@632 1157 end
adamc@632 1158 | _ => trySnd ())
adamc@632 1159 | _ => trySnd ()
adamc@403 1160 end
adamc@632 1161
adamc@706 1162 fun projSpecial2 (c2, n2, onFail) =
adamc@706 1163 case #1 (hnormCon env c2) of
adam@1639 1164 L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
adamc@706 1165 (case #1 (hnormKind k) of
adamc@706 1166 L'.KTuple ks =>
adamc@706 1167 let
adamc@706 1168 val loc = #2 c2
adam@1639 1169 val us = map (fn k => cunif' f (loc, k)) ks
adamc@706 1170 in
adam@1639 1171 r := L'.Known (L'.CTuple us, loc);
adamc@987 1172 unifyCons' env loc c1All (List.nth (us, n2 - 1))
adamc@706 1173 end
adamc@706 1174 | _ => onFail ())
adamc@706 1175 | _ => onFail ()
adamc@706 1176
adamc@777 1177 fun isRecord' () = unifyRecordCons env (loc, c1All, c2All)
adamc@706 1178
adamc@706 1179 fun isRecord () =
adamc@706 1180 case (c1, c2) of
adamc@706 1181 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord')
adamc@706 1182 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord')
adamc@706 1183 | _ => isRecord' ()
adamc@706 1184 in
adamc@706 1185 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
adamc@706 1186 ("c2All", p_con env c2All)];*)
adamc@706 1187
adamc@706 1188 case (c1, c2) of
adamc@706 1189 (L'.CError, _) => ()
adamc@706 1190 | (_, L'.CError) => ()
adamc@403 1191
adam@1639 1192 | (L'.CUnif (nl1, loc1, k1, _, r1 as ref (L'.Unknown f1)), L'.CUnif (nl2, loc2, k2, _, r2 as ref (L'.Unknown f2))) =>
adam@1303 1193 if r1 = r2 andalso nl1 = nl2 then
adamc@705 1194 ()
adam@1303 1195 else if nl1 = 0 then
adamc@705 1196 (unifyKinds env k1 k2;
adam@1639 1197 if f1 c2All then
adam@1639 1198 r1 := L'.Known c2All
adam@1639 1199 else
adam@1639 1200 err CScope)
adam@1303 1201 else if nl2 = 0 then
adam@1303 1202 (unifyKinds env k1 k2;
adam@1639 1203 if f2 c1All then
adam@1639 1204 r2 := L'.Known c1All
adam@1639 1205 else
adam@1639 1206 err CScope)
adam@1303 1207 else
adam@1303 1208 err (fn _ => TooLifty (loc1, loc2))
adam@1303 1209
adam@1639 1210 | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) =>
adam@1639 1211 if occursCon r c2All then
adam@1639 1212 err COccursCheckFailed
adam@1639 1213 else if f c2All then
adam@1639 1214 r := L'.Known c2All
adam@1639 1215 else
adam@1639 1216 err CScope
adam@1639 1217 | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) =>
adam@1639 1218 if occursCon r c1All then
adam@1639 1219 err COccursCheckFailed
adam@1639 1220 else if f c1All then
adam@1639 1221 r := L'.Known c1All
adam@1639 1222 else
adam@1639 1223 err CScope
adam@1639 1224
adam@1639 1225 | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) =>
adamc@705 1226 if occursCon r c2All then
adamc@705 1227 err COccursCheckFailed
adamc@705 1228 else
adam@1639 1229 (let
adam@1639 1230 val sq = squish nl c2All
adam@1639 1231 in
adam@1639 1232 if f sq then
adam@1639 1233 r := L'.Known sq
adam@1639 1234 else
adam@1639 1235 err CScope
adam@1639 1236 end
adam@1639 1237 handle CantSquish => err (fn _ => TooDeep))
adam@1639 1238 | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) =>
adamc@705 1239 if occursCon r c1All then
adamc@705 1240 err COccursCheckFailed
adamc@705 1241 else
adam@1639 1242 (let
adam@1639 1243 val sq = squish nl c1All
adam@1639 1244 in
adam@1639 1245 if f sq then
adam@1639 1246 r := L'.Known sq
adam@1639 1247 else
adam@1639 1248 err CScope
adam@1639 1249 end
adam@1306 1250 handle CantSquish => err (fn _ => TooDeep))
adam@1304 1251
adam@1341 1252 | (L'.CRecord _, _) => isRecord ()
adam@1341 1253 | (_, L'.CRecord _) => isRecord ()
adam@1341 1254 | (L'.CConcat _, _) => isRecord ()
adam@1341 1255 | (_, L'.CConcat _) => isRecord ()
adam@1341 1256
adam@1341 1257
adamc@705 1258 | (L'.CUnit, L'.CUnit) => ()
adamc@705 1259
adamc@705 1260 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
adamc@987 1261 (unifyCons' env loc d1 d2;
adam@1639 1262 unifyCons' env loc r1 r2)
adamc@705 1263 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
adamc@705 1264 if expl1 <> expl2 then
adamc@705 1265 err CExplicitness
adamc@705 1266 else
adamc@705 1267 (unifyKinds env d1 d2;
adamc@705 1268 let
adamc@705 1269 (*val befor = Time.now ()*)
adamc@705 1270 val env' = E.pushCRel env x1 d1
adamc@705 1271 in
adamc@705 1272 (*TextIO.print ("E.pushCRel: "
adamc@705 1273 ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))
adamc@705 1274 ^ "\n");*)
adamc@987 1275 unifyCons' env' loc r1 r2
adamc@705 1276 end)
adamc@987 1277 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env loc r1 r2
adamc@705 1278 | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) =>
adamc@987 1279 (unifyCons' env loc c1 c2;
adamc@987 1280 unifyCons' env loc d1 d2;
adamc@987 1281 unifyCons' env loc e1 e2)
adamc@705 1282
adamc@705 1283 | (L'.CRel n1, L'.CRel n2) =>
adamc@705 1284 if n1 = n2 then
adamc@705 1285 ()
adamc@705 1286 else
adamc@705 1287 err CIncompatible
adamc@705 1288 | (L'.CNamed n1, L'.CNamed n2) =>
adamc@705 1289 if n1 = n2 then
adamc@705 1290 ()
adamc@705 1291 else
adamc@705 1292 err CIncompatible
adamc@705 1293
adamc@705 1294 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
adamc@987 1295 (unifyCons' env loc d1 d2;
adamc@987 1296 unifyCons' env loc r1 r2)
adamc@705 1297 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
adamc@705 1298 (unifyKinds env k1 k2;
adamc@987 1299 unifyCons' (E.pushCRel env x1 k1) loc c1 c2)
adamc@705 1300
adamc@705 1301 | (L'.CName n1, L'.CName n2) =>
adamc@705 1302 if n1 = n2 then
adamc@705 1303 ()
adamc@705 1304 else
adamc@705 1305 err CIncompatible
adamc@705 1306
adamc@705 1307 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
adamc@705 1308 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
adamc@705 1309 ()
adamc@705 1310 else
adamc@705 1311 err CIncompatible
adamc@705 1312
adamc@705 1313 | (L'.CTuple cs1, L'.CTuple cs2) =>
adamc@987 1314 ((ListPair.appEq (fn (c1, c2) => unifyCons' env loc c1 c2) (cs1, cs2))
adamc@705 1315 handle ListPair.UnequalLengths => err CIncompatible)
adamc@705 1316
adamc@706 1317 | (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible)
adamc@706 1318 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible)
adamc@706 1319
adamc@623 1320 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
adamc@623 1321 (unifyKinds env dom1 dom2;
adamc@628 1322 unifyKinds env ran1 ran2)
adamc@623 1323
adamc@623 1324 | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) =>
adamc@987 1325 unifyCons' (E.pushKRel env x) loc c1 c2
adamc@623 1326 | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) =>
adamc@623 1327 (unifyKinds env k1 k2;
adamc@987 1328 unifyCons' env loc c1 c2)
adamc@623 1329 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
adamc@987 1330 unifyCons' (E.pushKRel env x) loc c1 c2
adamc@628 1331
adamc@403 1332 | _ => err CIncompatible
adamc@403 1333 end
adamc@403 1334
adamc@987 1335 and unifyCons env loc c1 c2 =
adamc@987 1336 unifyCons' env loc c1 c2
adamc@403 1337 handle CUnify' err => raise CUnify (c1, c2, err)
adamc@403 1338 | KUnify args => raise CUnify (c1, c2, CKind args)
adamc@403 1339
adamc@628 1340 fun checkCon env e c1 c2 =
adamc@987 1341 unifyCons env (#2 e) c1 c2
adamc@403 1342 handle CUnify (c1, c2, err) =>
adamc@628 1343 expError env (Unify (e, c1, c2, err))
adamc@628 1344
adamc@628 1345 fun checkPatCon env p c1 c2 =
adamc@987 1346 unifyCons env (#2 p) c1 c2
adamc@403 1347 handle CUnify (c1, c2, err) =>
adamc@628 1348 expError env (PatUnify (p, c1, c2, err))
adamc@71 1349
adamc@403 1350 fun primType env p =
adamc@403 1351 case p of
adamc@403 1352 P.Int _ => !int
adamc@403 1353 | P.Float _ => !float
adamc@403 1354 | P.String _ => !string
adamc@821 1355 | P.Char _ => !char
adamc@623 1356
adamc@403 1357 datatype constraint =
adamc@403 1358 Disjoint of D.goal
adamc@403 1359 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
adamc@403 1360
adam@1591 1361 fun relocConstraint loc c =
adam@1591 1362 case c of
adam@1591 1363 Disjoint (_, a, b, c, d) => Disjoint (loc, a, b, c, d)
adam@1591 1364 | TypeClass (a, b, c, _) => TypeClass (a, b, c, loc)
adam@1591 1365
adamc@403 1366 val enD = map Disjoint
adamc@403 1367
adamc@634 1368 fun isClassOrFolder env cl =
adamc@634 1369 E.isClass env cl
adamc@634 1370 orelse case hnormCon env cl of
adamc@634 1371 (L'.CKApp (cl, _), _) =>
adamc@634 1372 (case hnormCon env cl of
adamc@634 1373 (L'.CModProj (top_n, [], "folder"), _) => top_n = !top_r
adamc@634 1374 | _ => false)
adamc@634 1375 | _ => false
adamc@634 1376
adam@1303 1377 fun subConInCon env x y =
adam@1303 1378 ElabOps.subConInCon x y
adam@1303 1379 handle SubUnif => (cunifyError env (TooUnify (#2 x, y));
adam@1303 1380 cerror)
adam@1303 1381
adamc@629 1382 fun elabHead (env, denv) infer (e as (_, loc)) t =
adamc@403 1383 let
adamc@898 1384 fun unravelKind (t, e) =
adamc@898 1385 case hnormCon env t of
adamc@898 1386 (L'.TKFun (x, t'), _) =>
adamc@898 1387 let
adam@1639 1388 val u = kunif env loc
adamc@898 1389
adamc@898 1390 val t'' = subKindInCon (0, u) t'
adamc@898 1391 in
adamc@898 1392 unravelKind (t'', (L'.EKApp (e, u), loc))
adamc@898 1393 end
adamc@898 1394 | t => (e, t, [])
adamc@898 1395
adamc@403 1396 fun unravel (t, e) =
adamc@628 1397 case hnormCon env t of
adamc@628 1398 (L'.TKFun (x, t'), _) =>
adamc@628 1399 let
adam@1639 1400 val u = kunif env loc
adamc@628 1401
adamc@628 1402 val t'' = subKindInCon (0, u) t'
adamc@628 1403 in
adamc@628 1404 unravel (t'', (L'.EKApp (e, u), loc))
adamc@628 1405 end
adamc@628 1406 | (L'.TCFun (L'.Implicit, x, k, t'), _) =>
adamc@628 1407 let
adam@1639 1408 val u = cunif env (loc, k)
adamc@628 1409
adam@1303 1410 val t'' = subConInCon env (0, u) t'
adamc@628 1411 in
adamc@628 1412 unravel (t'', (L'.ECApp (e, u), loc))
adamc@628 1413 end
adamc@633 1414 | (L'.TFun (dom, ran), _) =>
adamc@628 1415 let
adamc@633 1416 fun default () = (e, t, [])
adamc@750 1417
adamc@750 1418 fun isInstance () =
adamc@750 1419 if infer <> L.TypesOnly then
adamc@750 1420 let
adamc@750 1421 val r = ref NONE
adamc@750 1422 val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
adamc@750 1423 in
adamc@750 1424 (e, t, TypeClass (env, dom, r, loc) :: gs)
adamc@750 1425 end
adamc@750 1426 else
adamc@750 1427 default ()
adamc@750 1428
adamc@750 1429 fun hasInstance c =
adamc@753 1430 case hnormCon env c of
adamc@753 1431 (L'.TRecord c, _) => U.Con.exists {kind = fn _ => false,
adamc@753 1432 con = fn c =>
adamc@753 1433 E.isClass env (hnormCon env (c, loc))} c
adamc@753 1434 | c =>
adamc@750 1435 let
adamc@753 1436 fun findHead c =
adamc@753 1437 case #1 c of
adamc@753 1438 L'.CApp (f, _) => findHead f
adamc@753 1439 | _ => c
adamc@753 1440
adamc@753 1441 val cl = hnormCon env (findHead c)
adamc@750 1442 in
adamc@750 1443 isClassOrFolder env cl
adamc@750 1444 end
adamc@628 1445 in
adamc@750 1446 if hasInstance dom then
adamc@750 1447 isInstance ()
adamc@750 1448 else
adamc@750 1449 default ()
adamc@628 1450 end
adamc@629 1451 | (L'.TDisjoint (r1, r2, t'), loc) =>
adamc@629 1452 if infer <> L.TypesOnly then
adamc@629 1453 let
adamc@792 1454 val gs = D.prove env denv (r1, r2, #2 e)
adamc@629 1455 val (e, t, gs') = unravel (t', e)
adamc@629 1456 in
adamc@629 1457 (e, t, enD gs @ gs')
adamc@629 1458 end
adamc@629 1459 else
adamc@629 1460 (e, t, [])
adamc@628 1461 | t => (e, t, [])
adam@1591 1462
adam@1591 1463 val (e, t, gs) = case infer of
adam@1591 1464 L.DontInfer => unravelKind (t, e)
adam@1591 1465 | _ => unravel (t, e)
adamc@704 1466 in
adam@1591 1467 ((#1 e, loc), (#1 t, loc), map (relocConstraint loc) gs)
adamc@704 1468 end
adamc@15 1469
adamc@628 1470 fun elabPat (pAll as (p, loc), (env, bound)) =
adamc@171 1471 let
adamc@171 1472 val perror = (L'.PWild, loc)
adamc@171 1473 val terror = (L'.CError, loc)
adamc@171 1474 val pterror = (perror, terror)
adamc@171 1475 val rerror = (pterror, (env, bound))
adamc@171 1476
adamc@191 1477 fun pcon (pc, po, xs, to, dn, dk) =
adamc@188 1478 case (po, to) of
adamc@188 1479 (NONE, SOME _) => (expError env (PatHasNoArg loc);
adamc@188 1480 rerror)
adamc@188 1481 | (SOME _, NONE) => (expError env (PatHasArg loc);
adamc@188 1482 rerror)
adamc@191 1483 | (NONE, NONE) =>
adamc@191 1484 let
adamc@191 1485 val k = (L'.KType, loc)
adam@1639 1486 val unifs = map (fn _ => cunif env (loc, k)) xs
adamc@191 1487 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
adamc@191 1488 in
adamc@191 1489 (((L'.PCon (dk, pc, unifs, NONE), loc), dn),
adamc@191 1490 (env, bound))
adamc@191 1491 end
adamc@188 1492 | (SOME p, SOME t) =>
adamc@188 1493 let
adamc@628 1494 val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
adamc@191 1495
adamc@191 1496 val k = (L'.KType, loc)
adam@1639 1497 val unifs = map (fn _ => cunif env (loc, k)) xs
adamc@194 1498 val nxs = length unifs - 1
adam@1304 1499 val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i,
adam@1304 1500 E.mliftConInCon (nxs - i) u) t) t unifs
adamc@191 1501 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
adamc@188 1502 in
adamc@628 1503 ignore (checkPatCon env p' pt t);
adamc@191 1504 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
adamc@188 1505 (env, bound))
adamc@188 1506 end
adamc@171 1507 in
adamc@171 1508 case p of
adam@1639 1509 L.PWild => (((L'.PWild, loc), cunif env (loc, (L'.KType, loc))),
adamc@171 1510 (env, bound))
adamc@171 1511 | L.PVar x =>
adamc@171 1512 let
adamc@171 1513 val t = if SS.member (bound, x) then
adamc@171 1514 (expError env (DuplicatePatternVariable (loc, x));
adamc@171 1515 terror)
adamc@171 1516 else
adam@1639 1517 cunif env (loc, (L'.KType, loc))
adamc@171 1518 in
adamc@182 1519 (((L'.PVar (x, t), loc), t),
adamc@171 1520 (E.pushERel env x t, SS.add (bound, x)))
adamc@171 1521 end
adamc@173 1522 | L.PPrim p => (((L'.PPrim p, loc), primType env p),
adamc@173 1523 (env, bound))
adamc@171 1524 | L.PCon ([], x, po) =>
adamc@171 1525 (case E.lookupConstructor env x of
adamc@174 1526 NONE => (expError env (UnboundConstructor (loc, [], x));
adamc@171 1527 rerror)
adamc@191 1528 | SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk))
adamc@174 1529 | L.PCon (m1 :: ms, x, po) =>
adamc@174 1530 (case E.lookupStr env m1 of
adamc@174 1531 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@174 1532 rerror)
adamc@174 1533 | SOME (n, sgn) =>
adamc@174 1534 let
adamc@174 1535 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@174 1536 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@182 1537 NONE => raise Fail "elabPat: Unknown substructure"
adamc@174 1538 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@174 1539 ((L'.StrVar n, loc), sgn) ms
adamc@174 1540 in
adamc@174 1541 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
adamc@174 1542 NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
adamc@174 1543 rerror)
adamc@191 1544 | SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk)
adamc@174 1545 end)
adamc@174 1546
adamc@175 1547 | L.PRecord (xps, flex) =>
adamc@175 1548 let
adamc@175 1549 val (xpts, (env, bound, _)) =
adamc@175 1550 ListUtil.foldlMap (fn ((x, p), (env, bound, fbound)) =>
adamc@175 1551 let
adamc@628 1552 val ((p', t), (env, bound)) = elabPat (p, (env, bound))
adamc@175 1553 in
adamc@175 1554 if SS.member (fbound, x) then
adamc@175 1555 expError env (DuplicatePatField (loc, x))
adamc@175 1556 else
adamc@175 1557 ();
adamc@175 1558 ((x, p', t), (env, bound, SS.add (fbound, x)))
adamc@175 1559 end)
adamc@175 1560 (env, bound, SS.empty) xps
adamc@175 1561
adamc@175 1562 val k = (L'.KType, loc)
adamc@175 1563 val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc)
adamc@176 1564 val c =
adamc@175 1565 if flex then
adam@1639 1566 (L'.CConcat (c, cunif env (loc, (L'.KRecord k, loc))), loc)
adamc@175 1567 else
adamc@176 1568 c
adamc@175 1569 in
adamc@182 1570 (((L'.PRecord xpts, loc),
adamc@175 1571 (L'.TRecord c, loc)),
adamc@175 1572 (env, bound))
adamc@175 1573 end
adamc@822 1574
adamc@822 1575 | L.PAnnot (p, t) =>
adamc@822 1576 let
adamc@822 1577 val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
adamc@822 1578 val (t', k, _) = elabCon (env, D.empty) t
adamc@822 1579 in
adamc@822 1580 checkPatCon env p' pt t';
adamc@822 1581 ((p', t'), (env, bound))
adamc@822 1582 end
adamc@171 1583 end
adamc@171 1584
adamc@819 1585 (* This exhaustiveness checking follows Luc Maranget's paper "Warnings for pattern matching." *)
adamc@819 1586 fun exhaustive (env, t, ps, loc) =
adamc@819 1587 let
adamc@819 1588 fun fail n = raise Fail ("Elaborate.exhaustive: Impossible " ^ Int.toString n)
adamc@819 1589
adamc@819 1590 fun patConNum pc =
adamc@819 1591 case pc of
adamc@819 1592 L'.PConVar n => n
adamc@819 1593 | L'.PConProj (m1, ms, x) =>
adamc@819 1594 let
adamc@819 1595 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@819 1596 in
adamc@819 1597 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
adamc@819 1598 NONE => raise Fail "exhaustive: Can't project datatype"
adamc@819 1599 | SOME (_, n, _, _, _) => n
adamc@819 1600 end
adamc@819 1601
adamc@819 1602 fun nameOfNum (t, n) =
adamc@819 1603 case t of
adamc@819 1604 L'.CModProj (m1, ms, x) =>
adamc@819 1605 let
adamc@819 1606 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@819 1607 in
adamc@819 1608 case E.projectDatatype env {str = str, sgn = sgn, field = x} of
adamc@819 1609 NONE => raise Fail "exhaustive: Can't project datatype"
adamc@819 1610 | SOME (_, cons) =>
adamc@819 1611 case ListUtil.search (fn (name, n', _) =>
adamc@819 1612 if n' = n then
adamc@819 1613 SOME name
adamc@819 1614 else
adamc@819 1615 NONE) cons of
adamc@819 1616 NONE => fail 9
adamc@819 1617 | SOME name => L'.PConProj (m1, ms, name)
adamc@819 1618 end
adamc@819 1619 | _ => L'.PConVar n
adamc@819 1620
adamc@819 1621 fun S (args, c, P) =
adamc@819 1622 List.mapPartial
adamc@819 1623 (fn [] => fail 1
adamc@819 1624 | p1 :: ps =>
adamc@819 1625 let
adamc@819 1626 val loc = #2 p1
adamc@819 1627
adamc@819 1628 fun wild () =
adamc@819 1629 SOME (map (fn _ => (L'.PWild, loc)) args @ ps)
adamc@819 1630 in
adamc@819 1631 case #1 p1 of
adamc@819 1632 L'.PPrim _ => NONE
adamc@819 1633 | L'.PCon (_, c', _, NONE) =>
adamc@819 1634 if patConNum c' = c then
adamc@819 1635 SOME ps
adamc@819 1636 else
adamc@819 1637 NONE
adamc@819 1638 | L'.PCon (_, c', _, SOME p) =>
adamc@819 1639 if patConNum c' = c then
adamc@819 1640 SOME (p :: ps)
adamc@819 1641 else
adamc@819 1642 NONE
adamc@819 1643 | L'.PRecord xpts =>
adamc@819 1644 SOME (map (fn x =>
adamc@819 1645 case ListUtil.search (fn (x', p, _) =>
adamc@819 1646 if x = x' then
adamc@819 1647 SOME p
adamc@819 1648 else
adamc@819 1649 NONE) xpts of
adamc@819 1650 NONE => (L'.PWild, loc)
adamc@819 1651 | SOME p => p) args @ ps)
adamc@819 1652 | L'.PWild => wild ()
adamc@819 1653 | L'.PVar _ => wild ()
adamc@819 1654 end)
adamc@819 1655 P
adamc@819 1656
adamc@819 1657 fun D P =
adamc@819 1658 List.mapPartial
adamc@819 1659 (fn [] => fail 2
adamc@819 1660 | (p1, _) :: ps =>
adamc@819 1661 case p1 of
adamc@819 1662 L'.PWild => SOME ps
adamc@819 1663 | L'.PVar _ => SOME ps
adamc@819 1664 | L'.PPrim _ => NONE
adamc@819 1665 | L'.PCon _ => NONE
adamc@819 1666 | L'.PRecord _ => NONE)
adamc@819 1667 P
adamc@819 1668
adamc@819 1669 fun I (P, q) =
adamc@819 1670 (*(prefaces "I" [("P", p_list (fn P' => box [PD.string "[", p_list (p_pat env) P', PD.string "]"]) P),
adamc@819 1671 ("q", p_list (p_con env) q)];*)
adamc@819 1672 case q of
adamc@819 1673 [] => (case P of
adamc@819 1674 [] => SOME []
adamc@819 1675 | _ => NONE)
adamc@819 1676 | q1 :: qs =>
adamc@819 1677 let
adamc@819 1678 val loc = #2 q1
adamc@819 1679
adamc@819 1680 fun unapp (t, acc) =
adamc@830 1681 case #1 t of
adamc@830 1682 L'.CApp (t, arg) => unapp (t, arg :: acc)
adamc@819 1683 | _ => (t, rev acc)
adamc@819 1684
adamc@830 1685 val (t1, args) = unapp (hnormCon env q1, [])
adamc@830 1686 val t1 = hnormCon env t1
adam@1303 1687 fun doSub t = foldl (fn (arg, t) => subConInCon env (0, arg) t) t args
adamc@819 1688
adamc@819 1689 fun dtype (dtO, names) =
adamc@819 1690 let
adamc@819 1691 val nameSet = IS.addList (IS.empty, names)
adamc@819 1692 val nameSet = foldl (fn (ps, nameSet) =>
adamc@819 1693 case ps of
adamc@819 1694 [] => fail 4
adamc@819 1695 | (L'.PCon (_, pc, _, _), _) :: _ =>
adamc@819 1696 (IS.delete (nameSet, patConNum pc)
adamc@819 1697 handle NotFound => nameSet)
adamc@819 1698 | _ => nameSet)
adamc@819 1699 nameSet P
adamc@819 1700 in
adamc@819 1701 nameSet
adamc@819 1702 end
adamc@819 1703
adamc@819 1704 fun default () = (NONE, IS.singleton 0, [])
adamc@819 1705
adamc@819 1706 val (dtO, unused, cons) =
adamc@830 1707 case #1 t1 of
adamc@819 1708 L'.CNamed n =>
adamc@819 1709 let
adamc@819 1710 val dt = E.lookupDatatype env n
adamc@819 1711 val cons = E.constructors dt
adamc@819 1712 in
adamc@819 1713 (SOME dt,
adamc@819 1714 dtype (SOME dt, map #2 cons),
adamc@819 1715 map (fn (_, n, co) =>
adamc@819 1716 (n,
adamc@819 1717 case co of
adamc@819 1718 NONE => []
adamc@819 1719 | SOME t => [("", doSub t)])) cons)
adamc@819 1720 end
adamc@819 1721 | L'.CModProj (m1, ms, x) =>
adamc@819 1722 let
adamc@819 1723 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@819 1724 in
adamc@819 1725 case E.projectDatatype env {str = str, sgn = sgn, field = x} of
adamc@819 1726 NONE => default ()
adamc@819 1727 | SOME (_, cons) =>
adamc@819 1728 (NONE,
adamc@819 1729 dtype (NONE, map #2 cons),
adamc@819 1730 map (fn (s, _, co) =>
adamc@819 1731 (patConNum (L'.PConProj (m1, ms, s)),
adamc@819 1732 case co of
adamc@819 1733 NONE => []
adamc@819 1734 | SOME t => [("", doSub t)])) cons)
adamc@819 1735 end
adamc@830 1736 | L'.TRecord t =>
adamc@830 1737 (case #1 (hnormCon env t) of
adamc@830 1738 L'.CRecord (_, xts) =>
adamc@830 1739 let
adamc@830 1740 val xts = map (fn ((L'.CName x, _), co) => SOME (x, co)
adamc@830 1741 | _ => NONE) xts
adamc@830 1742 in
adamc@830 1743 if List.all Option.isSome xts then
adamc@830 1744 let
adamc@830 1745 val xts = List.mapPartial (fn x => x) xts
adamc@830 1746 val xts = ListMergeSort.sort (fn ((x1, _), (x2, _)) =>
adamc@830 1747 String.compare (x1, x2) = GREATER) xts
adamc@830 1748 in
adamc@830 1749 (NONE, IS.empty, [(0, xts)])
adamc@830 1750 end
adamc@830 1751 else
adamc@830 1752 default ()
adamc@830 1753 end
adamc@830 1754 | _ => default ())
adamc@819 1755 | _ => default ()
adamc@819 1756 in
adamc@819 1757 if IS.isEmpty unused then
adamc@819 1758 let
adamc@819 1759 fun recurse cons =
adamc@819 1760 case cons of
adamc@819 1761 [] => NONE
adamc@819 1762 | (name, args) :: cons =>
adamc@819 1763 case I (S (map #1 args, name, P),
adamc@819 1764 map #2 args @ qs) of
adamc@819 1765 NONE => recurse cons
adamc@819 1766 | SOME ps =>
adamc@819 1767 let
adamc@819 1768 val nargs = length args
adamc@819 1769 val argPs = List.take (ps, nargs)
adamc@819 1770 val restPs = List.drop (ps, nargs)
adamc@819 1771
adamc@819 1772 val p = case name of
adamc@819 1773 0 => L'.PRecord (ListPair.map
adamc@819 1774 (fn ((name, t), p) => (name, p, t))
adamc@819 1775 (args, argPs))
adamc@830 1776 | _ => L'.PCon (L'.Default, nameOfNum (#1 t1, name), [],
adamc@819 1777 case argPs of
adamc@819 1778 [] => NONE
adamc@819 1779 | [p] => SOME p
adamc@819 1780 | _ => fail 3)
adamc@819 1781 in
adamc@819 1782 SOME ((p, loc) :: restPs)
adamc@819 1783 end
adamc@819 1784 in
adamc@819 1785 recurse cons
adamc@819 1786 end
adamc@819 1787 else
adamc@819 1788 case I (D P, qs) of
adamc@819 1789 NONE => NONE
adamc@819 1790 | SOME ps =>
adamc@819 1791 let
adamc@819 1792 val p = case cons of
adamc@819 1793 [] => L'.PWild
adamc@819 1794 | (0, _) :: _ => L'.PWild
adamc@819 1795 | _ =>
adamc@819 1796 case IS.find (fn _ => true) unused of
adamc@819 1797 NONE => fail 6
adamc@819 1798 | SOME name =>
adamc@819 1799 case ListUtil.search (fn (name', args) =>
adamc@819 1800 if name = name' then
adamc@819 1801 SOME (name', args)
adamc@819 1802 else
adamc@819 1803 NONE) cons of
adamc@819 1804 SOME (n, []) =>
adamc@830 1805 L'.PCon (L'.Default, nameOfNum (#1 t1, n), [], NONE)
adamc@819 1806 | SOME (n, [_]) =>
adamc@830 1807 L'.PCon (L'.Default, nameOfNum (#1 t1, n), [], SOME (L'.PWild, loc))
adamc@819 1808 | _ => fail 7
adamc@819 1809 in
adamc@819 1810 SOME ((p, loc) :: ps)
adamc@819 1811 end
adamc@819 1812 end
adamc@819 1813 in
adamc@819 1814 case I (map (fn x => [x]) ps, [t]) of
adamc@819 1815 NONE => NONE
adamc@819 1816 | SOME [p] => SOME p
adamc@819 1817 | _ => fail 7
adamc@819 1818 end
adamc@819 1819
adamc@217 1820 fun unmodCon env (c, loc) =
adamc@217 1821 case c of
adamc@217 1822 L'.CNamed n =>
adamc@217 1823 (case E.lookupCNamed env n of
adamc@217 1824 (_, _, SOME (c as (L'.CModProj _, _))) => unmodCon env c
adamc@217 1825 | _ => (c, loc))
adamc@217 1826 | L'.CModProj (m1, ms, x) =>
adamc@217 1827 let
adamc@217 1828 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@217 1829 in
adamc@217 1830 case E.projectCon env {str = str, sgn = sgn, field = x} of
adamc@217 1831 NONE => raise Fail "unmodCon: Can't projectCon"
adamc@217 1832 | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c
adamc@217 1833 | _ => (c, loc)
adamc@217 1834 end
adamc@217 1835 | _ => (c, loc)
adamc@217 1836
adamc@721 1837 fun normClassKey env c =
adamc@467 1838 let
adamc@721 1839 val c = hnormCon env c
adamc@467 1840 in
adamc@467 1841 case #1 c of
adamc@467 1842 L'.CApp (c1, c2) =>
adamc@467 1843 let
adamc@721 1844 val c1 = normClassKey env c1
adamc@721 1845 val c2 = normClassKey env c2
adamc@467 1846 in
adamc@467 1847 (L'.CApp (c1, c2), #2 c)
adamc@467 1848 end
adamc@721 1849 | L'.CRecord (k, xcs) => (L'.CRecord (k, map (fn (x, c) => (normClassKey env x,
adamc@721 1850 normClassKey env c)) xcs), #2 c)
adamc@721 1851 | _ => unmodCon env c
adamc@467 1852 end
adamc@467 1853
adamc@467 1854 fun normClassConstraint env (c, loc) =
adamc@217 1855 case c of
adamc@217 1856 L'.CApp (f, x) =>
adamc@217 1857 let
adamc@721 1858 val f = normClassKey env f
adamc@467 1859 val x = normClassKey env x
adamc@217 1860 in
adamc@467 1861 (L'.CApp (f, x), loc)
adamc@217 1862 end
adamc@674 1863 | L'.TFun (c1, c2) =>
adamc@674 1864 let
adamc@674 1865 val c1 = normClassConstraint env c1
adamc@674 1866 val c2 = normClassConstraint env c2
adamc@674 1867 in
adamc@674 1868 (L'.TFun (c1, c2), loc)
adamc@674 1869 end
adamc@674 1870 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc)
adam@1639 1871 | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => normClassConstraint env (E.mliftConInCon nl c)
adamc@721 1872 | _ => unmodCon env (c, loc)
adamc@216 1873
adamc@1093 1874 fun findHead e e' =
adamc@1093 1875 let
adamc@1093 1876 fun findHead (e, _) =
adamc@1093 1877 case e of
adamc@1093 1878 L.EVar (_, _, infer) =>
adamc@1093 1879 let
adamc@1093 1880 fun findHead' (e, _) =
adamc@1093 1881 case e of
adamc@1093 1882 L'.ENamed _ => true
adamc@1093 1883 | L'.EModProj _ => true
adam@1472 1884 | L'.ERel _ => true
adamc@1093 1885 | L'.EApp (e, _) => findHead' e
adamc@1093 1886 | L'.ECApp (e, _) => findHead' e
adamc@1093 1887 | L'.EKApp (e, _) => findHead' e
adamc@1093 1888 | _ => false
adamc@1093 1889 in
adamc@1093 1890 if findHead' e' then
adamc@1093 1891 SOME infer
adamc@1093 1892 else
adamc@1093 1893 NONE
adamc@1093 1894 end
adamc@1093 1895 | L.EApp (e, _) => findHead e
adamc@1093 1896 | L.ECApp (e, _) => findHead e
adamc@1093 1897 | L.EDisjointApp e => findHead e
adamc@1093 1898 | _ => NONE
adamc@1093 1899 in
adamc@1093 1900 findHead e
adamc@1093 1901 end
adamc@1093 1902
adam@1640 1903 datatype needed = Needed of {Cons : (L'.kind * int) SM.map,
adam@1640 1904 NextCon : int,
adamc@1264 1905 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list,
adamc@1264 1906 Vals : SS.set,
adamc@1270 1907 Mods : (E.env * needed) SM.map}
adamc@1264 1908
adam@1640 1909 fun ncons (Needed r) = map (fn (k, (v, _)) => (k, v))
adam@1640 1910 (ListMergeSort.sort (fn ((_, (_, n1)), (_, (_, n2))) => n1 > n2)
adam@1640 1911 (SM.listItemsi (#Cons r)))
adamc@1264 1912 fun nconstraints (Needed r) = #Constraints r
adamc@1264 1913 fun nvals (Needed r) = #Vals r
adamc@1264 1914 fun nmods (Needed r) = #Mods r
adamc@1264 1915
adamc@1264 1916 val nempty = Needed {Cons = SM.empty,
adam@1640 1917 NextCon = 0,
adamc@1264 1918 Constraints = nil,
adamc@1264 1919 Vals = SS.empty,
adamc@1264 1920 Mods = SM.empty}
adamc@1264 1921
adamc@1264 1922 fun naddCon (r : needed, k, v) =
adamc@1264 1923 let
adamc@1264 1924 val Needed r = r
adamc@1264 1925 in
adam@1640 1926 Needed {Cons = SM.insert (#Cons r, k, (v, #NextCon r)),
adam@1640 1927 NextCon = #NextCon r + 1,
adamc@1264 1928 Constraints = #Constraints r,
adamc@1264 1929 Vals = #Vals r,
adamc@1264 1930 Mods = #Mods r}
adamc@1264 1931 end
adamc@1264 1932
adamc@1264 1933 fun naddConstraint (r : needed, v) =
adamc@1264 1934 let
adamc@1264 1935 val Needed r = r
adamc@1264 1936 in
adamc@1264 1937 Needed {Cons = #Cons r,
adam@1640 1938 NextCon = #NextCon r,
adamc@1264 1939 Constraints = v :: #Constraints r,
adamc@1264 1940 Vals = #Vals r,
adamc@1264 1941 Mods = #Mods r}
adamc@1264 1942 end
adamc@1264 1943
adamc@1264 1944 fun naddVal (r : needed, k) =
adamc@1264 1945 let
adamc@1264 1946 val Needed r = r
adamc@1264 1947 in
adamc@1264 1948 Needed {Cons = #Cons r,
adam@1640 1949 NextCon = #NextCon r,
adamc@1264 1950 Constraints = #Constraints r,
adamc@1264 1951 Vals = SS.add (#Vals r, k),
adamc@1264 1952 Mods = #Mods r}
adamc@1264 1953 end
adamc@1264 1954
adamc@1264 1955 fun naddMod (r : needed, k, v) =
adamc@1264 1956 let
adamc@1264 1957 val Needed r = r
adamc@1264 1958 in
adamc@1264 1959 Needed {Cons = #Cons r,
adam@1640 1960 NextCon = #NextCon r,
adamc@1264 1961 Constraints = #Constraints r,
adamc@1264 1962 Vals = #Vals r,
adamc@1264 1963 Mods = SM.insert (#Mods r, k, v)}
adamc@1264 1964 end
adamc@1264 1965
adamc@1264 1966 fun ndelCon (r : needed, k) =
adamc@1264 1967 let
adamc@1264 1968 val Needed r = r
adamc@1264 1969 in
adamc@1264 1970 Needed {Cons = #1 (SM.remove (#Cons r, k)) handle NotFound => #Cons r,
adam@1640 1971 NextCon = #NextCon r,
adamc@1264 1972 Constraints = #Constraints r,
adamc@1264 1973 Vals = #Vals r,
adamc@1264 1974 Mods = #Mods r}
adamc@1264 1975 end
adamc@1264 1976
adamc@1264 1977 fun ndelVal (r : needed, k) =
adamc@1264 1978 let
adamc@1264 1979 val Needed r = r
adamc@1264 1980 in
adamc@1264 1981 Needed {Cons = #Cons r,
adam@1640 1982 NextCon = #NextCon r,
adamc@1264 1983 Constraints = #Constraints r,
adamc@1264 1984 Vals = SS.delete (#Vals r, k) handle NotFound => #Vals r,
adamc@1264 1985 Mods = #Mods r}
adamc@1264 1986 end
adamc@1264 1987
adam@1591 1988 fun chaseUnifs c =
adam@1591 1989 case #1 c of
adam@1639 1990 L'.CUnif (_, _, _, _, ref (L'.Known c)) => chaseUnifs c
adam@1591 1991 | _ => c
adam@1591 1992
adamc@92 1993 fun elabExp (env, denv) (eAll as (e, loc)) =
adamc@91 1994 let
adamc@848 1995 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
adamc@514 1996 (*val befor = Time.now ()*)
adamc@280 1997
adamc@280 1998 val r = case e of
adamc@91 1999 L.EAnnot (e, t) =>
adamc@91 2000 let
adamc@91 2001 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 2002 val (t', _, gs2) = elabCon (env, denv) t
adamc@91 2003 in
adamc@628 2004 checkCon env e' et t';
adamc@628 2005 (e', t', gs1 @ enD gs2)
adamc@91 2006 end
adamc@34 2007
adamc@91 2008 | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
adamc@403 2009 | L.EVar ([], s, infer) =>
adamc@91 2010 (case E.lookupE env s of
adamc@91 2011 E.NotBound =>
adamc@91 2012 (expError env (UnboundExp (loc, s));
adamc@91 2013 (eerror, cerror, []))
adamc@629 2014 | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t
adamc@629 2015 | E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed n, loc) t)
adamc@403 2016 | L.EVar (m1 :: ms, s, infer) =>
adamc@91 2017 (case E.lookupStr env m1 of
adamc@91 2018 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@91 2019 (eerror, cerror, []))
adamc@91 2020 | SOME (n, sgn) =>
adamc@91 2021 let
adamc@91 2022 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@91 2023 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@91 2024 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@91 2025 (strerror, sgnerror))
adamc@91 2026 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@91 2027 ((L'.StrVar n, loc), sgn) ms
adamc@10 2028
adamc@91 2029 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
adamc@91 2030 NONE => (expError env (UnboundExp (loc, s));
adamc@91 2031 cerror)
adamc@91 2032 | SOME t => t
adamc@91 2033 in
adamc@629 2034 elabHead (env, denv) infer (L'.EModProj (n, ms, s), loc) t
adamc@91 2035 end)
adamc@86 2036
adamc@349 2037 | L.EWild =>
adamc@210 2038 let
adamc@349 2039 val r = ref NONE
adam@1639 2040 val c = cunif env (loc, (L'.KType, loc))
adamc@210 2041 in
adamc@349 2042 ((L'.EUnif r, loc), c, [TypeClass (env, c, r, loc)])
adamc@210 2043 end
adamc@210 2044
adamc@91 2045 | L.EApp (e1, e2) =>
adamc@91 2046 let
adamc@91 2047 val (e1', t1, gs1) = elabExp (env, denv) e1
adamc@1093 2048
adamc@403 2049 val (e2', t2, gs2) = elabExp (env, denv) e2
adamc@71 2050
adam@1639 2051 val dom = cunif env (loc, ktype)
adam@1639 2052 val ran = cunif env (loc, ktype)
adamc@838 2053 val t = (L'.TFun (dom, ran), loc)
adamc@1093 2054
adamc@1093 2055 val () = checkCon env e1' t1 t
adamc@1093 2056 val () = checkCon env e2' t2 dom
adamc@1093 2057
adamc@1093 2058 val ef = (L'.EApp (e1', e2'), loc)
adamc@1093 2059 val (ef, et, gs3) =
adamc@1093 2060 case findHead e1 e1' of
adam@1591 2061 NONE => (ef, (#1 (chaseUnifs ran), loc), [])
adamc@1093 2062 | SOME infer => elabHead (env, denv) infer ef ran
adamc@91 2063 in
adamc@1093 2064 (ef, et, gs1 @ gs2 @ gs3)
adamc@91 2065 end
adamc@91 2066 | L.EAbs (x, to, e) =>
adamc@91 2067 let
adamc@91 2068 val (t', gs1) = case to of
adam@1639 2069 NONE => (cunif env (loc, ktype), [])
adamc@91 2070 | SOME t =>
adamc@91 2071 let
adamc@91 2072 val (t', tk, gs) = elabCon (env, denv) t
adamc@91 2073 in
adamc@91 2074 checkKind env t' tk ktype;
adamc@91 2075 (t', gs)
adamc@91 2076 end
adamc@467 2077 val dom = normClassConstraint env t'
adamc@467 2078 val (e', et, gs2) = elabExp (E.pushERel env x dom, denv) e
adamc@91 2079 in
adamc@91 2080 ((L'.EAbs (x, t', et, e'), loc),
adamc@91 2081 (L'.TFun (t', et), loc),
adamc@467 2082 enD gs1 @ gs2)
adamc@91 2083 end
adamc@91 2084 | L.ECApp (e, c) =>
adamc@91 2085 let
adamc@91 2086 val (e', et, gs1) = elabExp (env, denv) e
adamc@1093 2087
adamc@328 2088 val oldEt = et
adamc@403 2089 val (c', ck, gs2) = elabCon (env, denv) c
adamc@628 2090 val (et', _) = hnormCon env et
adamc@91 2091 in
adamc@91 2092 case et' of
adamc@91 2093 L'.CError => (eerror, cerror, [])
adamc@328 2094 | L'.TCFun (_, x, k, eb) =>
adamc@91 2095 let
adamc@91 2096 val () = checkKind env c' ck k
adam@1303 2097 val eb' = subConInCon env (0, c') eb
adamc@1093 2098
adamc@1093 2099 val ef = (L'.ECApp (e', c'), loc)
adamc@1093 2100 val (ef, eb', gs3) =
adamc@1093 2101 case findHead e e' of
adamc@1093 2102 NONE => (ef, eb', [])
adamc@1093 2103 | SOME infer => elabHead (env, denv) infer ef eb'
adamc@91 2104 in
adamc@328 2105 (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
adamc@328 2106 ("et", p_con env oldEt),
adamc@328 2107 ("x", PD.string x),
adamc@328 2108 ("eb", p_con (E.pushCRel env x k) eb),
adamc@328 2109 ("c", p_con env c'),
adamc@328 2110 ("eb'", p_con env eb')];*)
adam@1591 2111 (ef, (#1 eb', loc), gs1 @ enD gs2 @ gs3)
adamc@91 2112 end
adamc@91 2113
adamc@91 2114 | _ =>
adamc@91 2115 (expError env (WrongForm ("constructor function", e', et));
adamc@91 2116 (eerror, cerror, []))
adamc@91 2117 end
adamc@91 2118 | L.ECAbs (expl, x, k, e) =>
adamc@91 2119 let
adamc@91 2120 val expl' = elabExplicitness expl
adamc@623 2121 val k' = elabKind env k
adamc@328 2122
adamc@328 2123 val env' = E.pushCRel env x k'
adamc@328 2124 val (e', et, gs) = elabExp (env', D.enter denv) e
adamc@91 2125 in
adamc@91 2126 ((L'.ECAbs (expl', x, k', e'), loc),
adamc@91 2127 (L'.TCFun (expl', x, k', et), loc),
adamc@91 2128 gs)
adamc@91 2129 end
adamc@623 2130 | L.EKAbs (x, e) =>
adamc@623 2131 let
adamc@623 2132 val env' = E.pushKRel env x
adamc@623 2133 val (e', et, gs) = elabExp (env', denv) e
adamc@623 2134 in
adamc@623 2135 ((L'.EKAbs (x, e'), loc),
adamc@623 2136 (L'.TKFun (x, et), loc),
adamc@623 2137 gs)
adamc@623 2138 end
adamc@91 2139
adamc@91 2140 | L.EDisjoint (c1, c2, e) =>
adamc@91 2141 let
adamc@91 2142 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@91 2143 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@91 2144
adam@1639 2145 val ku1 = kunif env loc
adam@1639 2146 val ku2 = kunif env loc
adamc@91 2147
adamc@628 2148 val denv' = D.assert env denv (c1', c2')
adamc@628 2149 val (e', t, gs3) = elabExp (env, denv') e
adamc@91 2150 in
adamc@91 2151 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@91 2152 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@91 2153
adamc@628 2154 (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ gs3)
adamc@91 2155 end
adamc@629 2156 | L.EDisjointApp e =>
adamc@629 2157 let
adamc@629 2158 val (e', t, gs1) = elabExp (env, denv) e
adamc@629 2159
adam@1639 2160 val k1 = kunif env loc
adam@1639 2161 val c1 = cunif env (loc, (L'.KRecord k1, loc))
adam@1639 2162 val k2 = kunif env loc
adam@1639 2163 val c2 = cunif env (loc, (L'.KRecord k2, loc))
adam@1639 2164 val t' = cunif env (loc, ktype)
adamc@629 2165 val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc)
adamc@629 2166 val gs2 = D.prove env denv (c1, c2, loc)
adamc@629 2167 in
adam@1591 2168 (e', (#1 (chaseUnifs t'), loc), enD gs2 @ gs1)
adamc@629 2169 end
adamc@91 2170
adamc@91 2171 | L.ERecord xes =>
adamc@91 2172 let
adamc@91 2173 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
adamc@91 2174 let
adamc@91 2175 val (x', xk, gs1) = elabCon (env, denv) x
adamc@91 2176 val (e', et, gs2) = elabExp (env, denv) e
adamc@91 2177 in
adamc@91 2178 checkKind env x' xk kname;
adamc@228 2179 ((x', e', et), enD gs1 @ gs2 @ gs)
adamc@91 2180 end)
adamc@91 2181 [] xes
adamc@91 2182
adamc@91 2183 val k = (L'.KType, loc)
adamc@91 2184
adamc@91 2185 fun prove (xets, gs) =
adamc@91 2186 case xets of
adamc@91 2187 [] => gs
adamc@91 2188 | (x, _, t) :: rest =>
adamc@91 2189 let
adamc@91 2190 val xc = (x, t)
adamc@91 2191 val r1 = (L'.CRecord (k, [xc]), loc)
adamc@91 2192 val gs = foldl (fn ((x', _, t'), gs) =>
adamc@91 2193 let
adamc@91 2194 val xc' = (x', t')
adamc@91 2195 val r2 = (L'.CRecord (k, [xc']), loc)
adamc@91 2196 in
adamc@91 2197 D.prove env denv (r1, r2, loc) @ gs
adamc@91 2198 end)
adamc@91 2199 gs rest
adamc@91 2200 in
adamc@91 2201 prove (rest, gs)
adamc@91 2202 end
adamc@228 2203
adamc@228 2204 val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs
adamc@228 2205 val gsO = List.filter (fn Disjoint _ => false | _ => true) gs
adamc@91 2206 in
adamc@255 2207 (*TextIO.print ("|gsO| = " ^ Int.toString (length gsO) ^ "\n");*)
adamc@91 2208 ((L'.ERecord xes', loc),
adamc@91 2209 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
adamc@228 2210 enD (prove (xes', gsD)) @ gsO)
adamc@91 2211 end
adamc@91 2212
adamc@91 2213 | L.EField (e, c) =>
adamc@91 2214 let
adamc@91 2215 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 2216 val (c', ck, gs2) = elabCon (env, denv) c
adamc@91 2217
adam@1639 2218 val ft = cunif env (loc, ktype)
adam@1639 2219 val rest = cunif env (loc, ktype_record)
adamc@91 2220 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
adamc@629 2221 val () = checkCon env e' et
adamc@629 2222 (L'.TRecord (L'.CConcat (first, rest), loc), loc);
adamc@628 2223 val gs3 = D.prove env denv (first, rest, loc)
adamc@91 2224 in
adamc@628 2225 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3)
adamc@91 2226 end
adamc@91 2227
adamc@445 2228 | L.EConcat (e1, e2) =>
adamc@339 2229 let
adamc@339 2230 val (e1', e1t, gs1) = elabExp (env, denv) e1
adamc@445 2231 val (e2', e2t, gs2) = elabExp (env, denv) e2
adamc@445 2232
adam@1639 2233 val r1 = cunif env (loc, ktype_record)
adam@1639 2234 val r2 = cunif env (loc, ktype_record)
adamc@445 2235
adamc@629 2236 val () = checkCon env e1' e1t (L'.TRecord r1, loc)
adamc@629 2237 val () = checkCon env e2' e2t (L'.TRecord r2, loc)
adamc@629 2238
adamc@628 2239 val gs3 = D.prove env denv (r1, r2, loc)
adamc@339 2240 in
adamc@445 2241 ((L'.EConcat (e1', r1, e2', r2), loc),
adamc@445 2242 (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc),
adamc@628 2243 gs1 @ gs2 @ enD gs3)
adamc@339 2244 end
adamc@149 2245 | L.ECut (e, c) =>
adamc@149 2246 let
adamc@149 2247 val (e', et, gs1) = elabExp (env, denv) e
adamc@149 2248 val (c', ck, gs2) = elabCon (env, denv) c
adamc@149 2249
adam@1639 2250 val ft = cunif env (loc, ktype)
adam@1639 2251 val rest = cunif env (loc, ktype_record)
adamc@149 2252 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
adamc@629 2253
adamc@629 2254 val () = checkCon env e' et
adamc@629 2255 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
adamc@149 2256
adamc@628 2257 val gs3 = D.prove env denv (first, rest, loc)
adamc@149 2258 in
adam@1299 2259 checkKind env c' ck kname;
adamc@228 2260 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
adamc@628 2261 gs1 @ enD gs2 @ enD gs3)
adamc@149 2262 end
adamc@493 2263 | L.ECutMulti (e, c) =>
adamc@493 2264 let
adamc@493 2265 val (e', et, gs1) = elabExp (env, denv) e
adamc@493 2266 val (c', ck, gs2) = elabCon (env, denv) c
adamc@493 2267
adam@1639 2268 val rest = cunif env (loc, ktype_record)
adamc@629 2269
adamc@629 2270 val () = checkCon env e' et
adamc@629 2271 (L'.TRecord (L'.CConcat (c', rest), loc), loc)
adamc@493 2272
adamc@628 2273 val gs3 = D.prove env denv (c', rest, loc)
adamc@493 2274 in
adam@1299 2275 checkKind env c' ck (L'.KRecord ktype, loc);
adamc@493 2276 ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc),
adamc@628 2277 gs1 @ enD gs2 @ enD gs3)
adamc@493 2278 end
adamc@149 2279
adamc@171 2280 | L.ECase (e, pes) =>
adamc@171 2281 let
adamc@171 2282 val (e', et, gs1) = elabExp (env, denv) e
adam@1639 2283 val result = cunif env (loc, (L'.KType, loc))
adamc@171 2284 val (pes', gs) = ListUtil.foldlMap
adamc@171 2285 (fn ((p, e), gs) =>
adamc@171 2286 let
adamc@628 2287 val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty))
adamc@628 2288
adamc@629 2289 val (e', et', gs1) = elabExp (env, denv) e
adamc@171 2290 in
adamc@628 2291 checkPatCon env p' pt et;
adamc@629 2292 checkCon env e' et' result;
adamc@628 2293 ((p', e'), gs1 @ gs)
adamc@171 2294 end)
adamc@171 2295 gs1 pes
adamc@171 2296 in
adamc@819 2297 case exhaustive (env, et, map #1 pes', loc) of
adamc@819 2298 NONE => ()
adamc@830 2299 | SOME p => if !mayDelay then
adamc@830 2300 delayedExhaustives := (env, et, map #1 pes', loc) :: !delayedExhaustives
adamc@830 2301 else
adamc@830 2302 expError env (Inexhaustive (loc, p));
adamc@172 2303
adamc@628 2304 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs)
adamc@171 2305 end
adamc@447 2306
adamc@447 2307 | L.ELet (eds, e) =>
adamc@447 2308 let
adamc@447 2309 val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds
adamc@447 2310 val (e, t, gs2) = elabExp (env, denv) e
adamc@447 2311 in
adamc@825 2312 ((L'.ELet (eds, e, t), loc), t, gs1 @ gs2)
adamc@447 2313 end
adamc@280 2314 in
adamc@819 2315 (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*)
adamc@280 2316 r
adamc@91 2317 end
adamc@31 2318
adamc@628 2319 and elabEdecl denv (dAll as (d, loc), (env, gs)) =
adamc@447 2320 let
adamc@447 2321 val r =
adamc@447 2322 case d of
adamc@825 2323 L.EDVal (p, e) =>
adamc@447 2324 let
adamc@825 2325 val ((p', pt), (env', _)) = elabPat (p, (env, SS.empty))
adamc@825 2326 val (e', et, gs1) = elabExp (env, denv) e
adamc@825 2327
adamc@825 2328 val () = checkCon env e' et pt
adamc@825 2329
adam@1554 2330 val env' = E.patBinds env p'
adam@1554 2331 (* Redo to get proper detection of type class witnesses *)
adam@1554 2332
adamc@825 2333 val pt = normClassConstraint env pt
adamc@447 2334 in
adamc@830 2335 case exhaustive (env, et, [p'], loc) of
adamc@830 2336 NONE => ()
adamc@830 2337 | SOME p => if !mayDelay then
adamc@830 2338 delayedExhaustives := (env, et, [p'], loc) :: !delayedExhaustives
adamc@830 2339 else
adamc@830 2340 expError env (Inexhaustive (loc, p));
adamc@830 2341
adamc@825 2342 ((L'.EDVal (p', pt, e'), loc), (env', gs1 @ gs))
adamc@447 2343 end
adamc@447 2344 | L.EDValRec vis =>
adamc@447 2345 let
adamc@447 2346 fun allowable (e, _) =
adamc@447 2347 case e of
adamc@447 2348 L.EAbs _ => true
adamc@447 2349 | L.ECAbs (_, _, _, e) => allowable e
adamc@623 2350 | L.EKAbs (_, e) => allowable e
adamc@447 2351 | L.EDisjoint (_, _, e) => allowable e
adamc@447 2352 | _ => false
adamc@447 2353
adamc@447 2354 val (vis, gs) = ListUtil.foldlMap
adamc@447 2355 (fn ((x, co, e), gs) =>
adamc@447 2356 let
adamc@447 2357 val (c', _, gs1) = case co of
adam@1639 2358 NONE => (cunif env (loc, ktype), ktype, [])
adamc@447 2359 | SOME c => elabCon (env, denv) c
adamc@447 2360 in
adamc@447 2361 ((x, c', e), enD gs1 @ gs)
adamc@447 2362 end) gs vis
adamc@447 2363
adamc@447 2364 val env = foldl (fn ((x, c', _), env) => E.pushERel env x c') env vis
adamc@447 2365
adamc@447 2366 val (vis, gs) = ListUtil.foldlMap (fn ((x, c', e), gs) =>
adamc@447 2367 let
adamc@447 2368 val (e', et, gs1) = elabExp (env, denv) e
adamc@447 2369 in
adamc@628 2370 checkCon env e' et c';
adamc@447 2371 if allowable e then
adamc@447 2372 ()
adamc@447 2373 else
adamc@447 2374 expError env (IllegalRec (x, e'));
adamc@628 2375 ((x, c', e'), gs1 @ gs)
adamc@447 2376 end) gs vis
adamc@447 2377 in
adamc@447 2378 ((L'.EDValRec vis, loc), (env, gs))
adamc@447 2379 end
adamc@447 2380 in
adamc@447 2381 r
adamc@447 2382 end
adamc@447 2383
adamc@42 2384 val hnormSgn = E.hnormSgn
adamc@31 2385
adamc@210 2386 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
adamc@338 2387 fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan)
adamc@754 2388 fun viewOf () = (L'.CModProj (!basis_r, [], "sql_view"), ErrorMsg.dummySpan)
adamc@754 2389 fun queryOf () = (L'.CModProj (!basis_r, [], "sql_query"), ErrorMsg.dummySpan)
adamc@459 2390 fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan)
adamc@718 2391 fun styleOf () = (L'.CModProj (!basis_r, [], "css_class"), ErrorMsg.dummySpan)
adamc@205 2392
adamc@469 2393 fun dopenConstraints (loc, env, denv) {str, strs} =
adamc@469 2394 case E.lookupStr env str of
adamc@469 2395 NONE => (strError env (UnboundStr (loc, str));
adamc@469 2396 denv)
adamc@469 2397 | SOME (n, sgn) =>
adamc@469 2398 let
adamc@469 2399 val (st, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@469 2400 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@469 2401 NONE => (strError env (UnboundStr (loc, m));
adamc@469 2402 (strerror, sgnerror))
adamc@469 2403 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@469 2404 ((L'.StrVar n, loc), sgn) strs
adamc@1030 2405
adamc@1030 2406 fun collect first (st, sgn) =
adamc@1030 2407 case E.projectConstraints env {sgn = sgn, str = st} of
adamc@1182 2408 NONE => []
adamc@1030 2409 | SOME cs =>
adamc@1030 2410 case #1 (hnormSgn env sgn) of
adamc@1030 2411 L'.SgnConst sgis =>
adamc@1030 2412 foldl (fn (sgi, cs) =>
adamc@1030 2413 case #1 sgi of
adamc@1030 2414 L'.SgiStr (x, _, _) =>
adamc@1030 2415 (case E.projectStr env {sgn = sgn, str = st, field = x} of
adamc@1030 2416 NONE => raise Fail "Elaborate: projectStr in collect"
adamc@1030 2417 | SOME sgn' =>
adamc@1030 2418 List.revAppend (collect false ((L'.StrProj (st, x), loc), sgn'),
adamc@1030 2419 cs))
adamc@1030 2420 | _ => cs) cs sgis
adamc@1030 2421 | _ => cs
adamc@469 2422 in
adamc@1030 2423 foldl (fn ((c1, c2), denv) =>
adamc@1030 2424 D.assert env denv (c1, c2)) denv (collect true (st, sgn))
adamc@469 2425 end
adamc@469 2426
adamc@88 2427 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
adamc@1270 2428 ((*Print.preface ("elabSgi", SourcePrint.p_sgn_item (sgi, loc));*)
adamc@1270 2429 case sgi of
adamc@1270 2430 L.SgiConAbs (x, k) =>
adamc@1270 2431 let
adamc@1270 2432 val k' = elabKind env k
adamc@1270 2433
adamc@1270 2434 val (env', n) = E.pushCNamed env x k' NONE
adamc@1270 2435 in
adamc@1270 2436 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs))
adamc@1270 2437 end
adamc@1270 2438
adamc@1270 2439 | L.SgiCon (x, ko, c) =>
adamc@1270 2440 let
adamc@1270 2441 val k' = case ko of
adam@1639 2442 NONE => kunif env loc
adamc@1270 2443 | SOME k => elabKind env k
adamc@1270 2444
adamc@1270 2445 val (c', ck, gs') = elabCon (env, denv) c
adamc@1270 2446 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@1270 2447 in
adamc@1270 2448 checkKind env c' ck k';
adamc@1270 2449
adamc@1270 2450 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
adamc@1270 2451 end
adamc@1270 2452
adamc@1270 2453 | L.SgiDatatype dts =>
adamc@1270 2454 let
adamc@1270 2455 val k = (L'.KType, loc)
adamc@1270 2456
adamc@1270 2457 val (dts, env) = ListUtil.foldlMap (fn ((x, xs, xcs), env) =>
adamc@1270 2458 let
adamc@1270 2459 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@1270 2460 val (env, n) = E.pushCNamed env x k' NONE
adamc@1270 2461 in
adamc@1270 2462 ((x, n, xs, xcs), env)
adamc@1270 2463 end)
adamc@1270 2464 env dts
adamc@1270 2465
adamc@1270 2466 val (dts, env) = ListUtil.foldlMap
adamc@1270 2467 (fn ((x, n, xs, xcs), env) =>
adamc@1270 2468 let
adamc@1270 2469 val t = (L'.CNamed n, loc)
adamc@1270 2470 val nxs = length xs - 1
adamc@1270 2471 val t = ListUtil.foldli (fn (i, _, t) =>
adamc@1270 2472 (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@1270 2473
adamc@1270 2474 val (env', denv') = foldl (fn (x, (env', denv')) =>
adamc@1270 2475 (E.pushCRel env' x k,
adamc@1270 2476 D.enter denv')) (env, denv) xs
adamc@1270 2477
adamc@1270 2478 val (xcs, (used, env, gs)) =
adamc@1270 2479 ListUtil.foldlMap
adamc@1270 2480 (fn ((x, to), (used, env, gs)) =>
adamc@1270 2481 let
adamc@1270 2482 val (to, t, gs') = case to of
adamc@1270 2483 NONE => (NONE, t, gs)
adamc@1270 2484 | SOME t' =>
adamc@1270 2485 let
adamc@1270 2486 val (t', tk, gs') =
adamc@1270 2487 elabCon (env', denv') t'
adamc@1270 2488 in
adamc@1270 2489 checkKind env' t' tk k;
adamc@1270 2490 (SOME t',
adamc@1270 2491 (L'.TFun (t', t), loc),
adamc@1270 2492 gs' @ gs)
adamc@1270 2493 end
adamc@1270 2494 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc))
adamc@1270 2495 t xs
adamc@1270 2496
adamc@1270 2497 val (env, n') = E.pushENamed env x t
adamc@1270 2498 in
adamc@1270 2499 if SS.member (used, x) then
adamc@1270 2500 strError env (DuplicateConstructor (x, loc))
adamc@1270 2501 else
adamc@1270 2502 ();
adamc@1270 2503 ((x, n', to), (SS.add (used, x), env, gs'))
adamc@1270 2504 end)
adamc@1270 2505 (SS.empty, env, []) xcs
adamc@1270 2506 in
adamc@1270 2507 ((x, n, xs, xcs), E.pushDatatype env n xs xcs)
adamc@1270 2508 end)
adamc@1270 2509 env dts
adamc@1270 2510 in
adamc@1270 2511 ([(L'.SgiDatatype dts, loc)], (env, denv, gs))
adamc@1270 2512 end
adamc@1270 2513
adamc@1270 2514 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
adamc@1270 2515
adamc@1270 2516 | L.SgiDatatypeImp (x, m1 :: ms, s) =>
adamc@1270 2517 (case E.lookupStr env m1 of
adamc@1270 2518 NONE => (strError env (UnboundStr (loc, m1));
adamc@1270 2519 ([], (env, denv, gs)))
adamc@1270 2520 | SOME (n, sgn) =>
adamc@1270 2521 let
adamc@1270 2522 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@1270 2523 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@1270 2524 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@1270 2525 (strerror, sgnerror))
adamc@1270 2526 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@1270 2527 ((L'.StrVar n, loc), sgn) ms
adamc@1270 2528 in
adamc@1270 2529 case hnormCon env (L'.CModProj (n, ms, s), loc) of
adamc@1270 2530 (L'.CModProj (n, ms, s), _) =>
adamc@1270 2531 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
adamc@1270 2532 NONE => (conError env (UnboundDatatype (loc, s));
adamc@1270 2533 ([], (env, denv, [])))
adamc@1270 2534 | SOME (xs, xncs) =>
adamc@1270 2535 let
adamc@1270 2536 val k = (L'.KType, loc)
adamc@1270 2537 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@1270 2538
adamc@1270 2539 val t = (L'.CModProj (n, ms, s), loc)
adamc@1270 2540 val (env, n') = E.pushCNamed env x k' (SOME t)
adamc@1270 2541 val env = E.pushDatatype env n' xs xncs
adamc@1270 2542
adamc@1270 2543 val t = (L'.CNamed n', loc)
adamc@1270 2544 val env = foldl (fn ((x, n, to), env) =>
adamc@805 2545 let
adamc@1270 2546 val t = case to of
adamc@1270 2547 NONE => t
adamc@1270 2548 | SOME t' => (L'.TFun (t', t), loc)
adamc@1270 2549
adamc@1270 2550 val t = foldr (fn (x, t) =>
adamc@1270 2551 (L'.TCFun (L'.Implicit, x, k, t), loc))
adamc@1270 2552 t xs
adamc@805 2553 in
adamc@1270 2554 E.pushENamedAs env x n t
adamc@1270 2555 end) env xncs
adamc@1270 2556 in
adamc@1270 2557 ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, []))
adamc@1270 2558 end)
adamc@1270 2559 | _ => (strError env (NotDatatype loc);
adamc@1270 2560 ([], (env, denv, [])))
adamc@1270 2561 end)
adamc@1270 2562
adamc@1270 2563 | L.SgiVal (x, c) =>
adamc@1270 2564 let
adamc@1270 2565 val (c', ck, gs') = elabCon (env, denv) c
adamc@1270 2566
adamc@1270 2567 val old = c'
adamc@1270 2568 val c' = normClassConstraint env c'
adamc@1270 2569 val (env', n) = E.pushENamed env x c'
adamc@1270 2570 in
adamc@1270 2571 (unifyKinds env ck ktype
adamc@1270 2572 handle KUnify ue => strError env (NotType (loc, ck, ue)));
adamc@1270 2573
adamc@1270 2574 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
adamc@1270 2575 end
adamc@1270 2576
adamc@1270 2577 | L.SgiTable (x, c, pe, ce) =>
adamc@1270 2578 let
adamc@1270 2579 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
adamc@1270 2580
adamc@1270 2581 val (c', ck, gs') = elabCon (env, denv) c
adam@1639 2582 val pkey = cunif env (loc, cstK)
adam@1639 2583 val visible = cunif env (loc, cstK)
adamc@1270 2584 val (env', ds, uniques) =
adamc@1270 2585 case (#1 pe, #1 ce) of
adamc@1270 2586 (L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) =>
adamc@1270 2587 let
adamc@1270 2588 val x' = x ^ "_hidden_constraints"
adamc@1270 2589 val (env', hidden_n) = E.pushCNamed env x' cstK NONE
adamc@1270 2590 val hidden = (L'.CNamed hidden_n, loc)
adamc@1270 2591 in
adamc@1270 2592 (env', [(L'.SgiConAbs (x', hidden_n, cstK), loc)], (L'.CConcat (visible, hidden), loc))
adamc@1270 2593 end
adamc@1270 2594 | _ => (env, [], visible)
adamc@1270 2595
adamc@1270 2596 val ct = tableOf ()
adamc@1270 2597 val ct = (L'.CApp (ct, c'), loc)
adamc@1270 2598 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc)
adamc@1270 2599
adamc@1270 2600 val (pe', pet, gs'') = elabExp (env', denv) pe
adamc@1270 2601 val gs'' = List.mapPartial (fn Disjoint x => SOME x
adamc@707 2602 | _ => NONE) gs''
adamc@707 2603
adamc@1270 2604 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc)
adamc@1270 2605 val pst = (L'.CApp (pst, c'), loc)
adamc@1270 2606 val pst = (L'.CApp (pst, pkey), loc)
adamc@1270 2607
adamc@1270 2608 val (env', n) = E.pushENamed env' x ct
adamc@1270 2609
adamc@1270 2610 val (ce', cet, gs''') = elabExp (env', denv) ce
adamc@1270 2611 val gs''' = List.mapPartial (fn Disjoint x => SOME x
adamc@1270 2612 | _ => NONE) gs'''
adamc@1270 2613
adamc@1270 2614 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
adamc@1270 2615 val cst = (L'.CApp (cst, c'), loc)
adamc@1270 2616 val cst = (L'.CApp (cst, visible), loc)
adamc@1270 2617 in
adamc@1270 2618 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc);
adamc@1270 2619 checkCon env' pe' pet pst;
adamc@1270 2620 checkCon env' ce' cet cst;
adamc@1270 2621
adamc@1270 2622 (ds @ [(L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
adamc@1270 2623 end
adamc@1270 2624
adamc@1270 2625 | L.SgiStr (x, sgn) =>
adamc@1270 2626 let
adamc@1270 2627 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@1270 2628 val (env', n) = E.pushStrNamed env x sgn'
adamc@1270 2629 in
adamc@1270 2630 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@1270 2631 end
adamc@1270 2632
adamc@1270 2633 | L.SgiSgn (x, sgn) =>
adamc@1270 2634 let
adamc@1270 2635 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@1270 2636 val (env', n) = E.pushSgnNamed env x sgn'
adamc@1270 2637 in
adamc@1270 2638 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@1270 2639 end
adamc@1270 2640
adamc@1270 2641 | L.SgiInclude sgn =>
adamc@1270 2642 let
adamc@1270 2643 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@1270 2644 in
adamc@1270 2645 case #1 (hnormSgn env sgn') of
adamc@1270 2646 L'.SgnConst sgis =>
adamc@1270 2647 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs))
adamc@1270 2648 | _ => (sgnError env (NotIncludable sgn');
adamc@1270 2649 ([], (env, denv, [])))
adamc@1270 2650 end
adamc@1270 2651
adamc@1270 2652 | L.SgiConstraint (c1, c2) =>
adamc@1270 2653 let
adamc@1270 2654 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@1270 2655 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@1270 2656
adamc@1270 2657 val denv = D.assert env denv (c1', c2')
adamc@1270 2658 in
adam@1639 2659 checkKind env c1' k1 (L'.KRecord (kunif env loc), loc);
adam@1639 2660 checkKind env c2' k2 (L'.KRecord (kunif env loc), loc);
adamc@1270 2661
adamc@1270 2662 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2))
adamc@1270 2663 end
adamc@1270 2664
adamc@1270 2665 | L.SgiClassAbs (x, k) =>
adamc@1270 2666 let
adamc@1270 2667 val k = elabKind env k
adamc@1270 2668 val (env, n) = E.pushCNamed env x k NONE
adamc@1270 2669 val env = E.pushClass env n
adamc@1270 2670 in
adamc@1270 2671 ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, []))
adamc@1270 2672 end
adamc@1270 2673
adamc@1270 2674 | L.SgiClass (x, k, c) =>
adamc@1270 2675 let
adamc@1270 2676 val k = elabKind env k
adamc@1270 2677 val (c', ck, gs) = elabCon (env, denv) c
adamc@1270 2678 val (env, n) = E.pushCNamed env x k (SOME c')
adamc@1270 2679 val env = E.pushClass env n
adamc@1270 2680 in
adamc@1270 2681 checkKind env c' ck k;
adamc@1270 2682 ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, []))
adamc@1270 2683 end)
adamc@211 2684
adamc@83 2685 and elabSgn (env, denv) (sgn, loc) =
adamc@31 2686 case sgn of
adamc@31 2687 L.SgnConst sgis =>
adamc@31 2688 let
adamc@88 2689 val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis
adamc@62 2690
adamc@62 2691 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) =>
adamc@62 2692 case sgi of
adamc@62 2693 L'.SgiConAbs (x, _, _) =>
adamc@62 2694 (if SS.member (cons, x) then
adamc@62 2695 sgnError env (DuplicateCon (loc, x))
adamc@62 2696 else
adamc@62 2697 ();
adamc@62 2698 (SS.add (cons, x), vals, sgns, strs))
adamc@62 2699 | L'.SgiCon (x, _, _, _) =>
adamc@62 2700 (if SS.member (cons, x) then
adamc@62 2701 sgnError env (DuplicateCon (loc, x))
adamc@62 2702 else
adamc@62 2703 ();
adamc@62 2704 (SS.add (cons, x), vals, sgns, strs))
adamc@805 2705 | L'.SgiDatatype dts =>
adamc@156 2706 let
adamc@805 2707 val (cons, vals) =
adamc@805 2708 let
adamc@805 2709 fun doOne ((x, _, _, xncs), (cons, vals)) =
adamc@805 2710 let
adamc@805 2711 val vals = foldl (fn ((x, _, _), vals) =>
adamc@805 2712 (if SS.member (vals, x) then
adamc@805 2713 sgnError env (DuplicateVal (loc, x))
adamc@805 2714 else
adamc@805 2715 ();
adamc@805 2716 SS.add (vals, x)))
adamc@805 2717 vals xncs
adamc@805 2718 in
adamc@805 2719 if SS.member (cons, x) then
adamc@805 2720 sgnError env (DuplicateCon (loc, x))
adamc@805 2721 else
adamc@805 2722 ();
adamc@805 2723 (SS.add (cons, x), vals)
adamc@805 2724 end
adamc@805 2725 in
adamc@805 2726 foldl doOne (cons, vals) dts
adamc@805 2727 end
adamc@156 2728 in
adamc@805 2729 (cons, vals, sgns, strs)
adamc@156 2730 end
adamc@191 2731 | L'.SgiDatatypeImp (x, _, _, _, _, _, _) =>
adamc@156 2732 (if SS.member (cons, x) then
adamc@156 2733 sgnError env (DuplicateCon (loc, x))
adamc@156 2734 else
adamc@156 2735 ();
adamc@156 2736 (SS.add (cons, x), vals, sgns, strs))
adamc@62 2737 | L'.SgiVal (x, _, _) =>
adamc@62 2738 (if SS.member (vals, x) then
adamc@62 2739 sgnError env (DuplicateVal (loc, x))
adamc@62 2740 else
adamc@62 2741 ();
adamc@62 2742 (cons, SS.add (vals, x), sgns, strs))
adamc@62 2743 | L'.SgiSgn (x, _, _) =>
adamc@62 2744 (if SS.member (sgns, x) then
adamc@62 2745 sgnError env (DuplicateSgn (loc, x))
adamc@62 2746 else
adamc@62 2747 ();
adamc@62 2748 (cons, vals, SS.add (sgns, x), strs))
adamc@62 2749 | L'.SgiStr (x, _, _) =>
adamc@62 2750 (if SS.member (strs, x) then
adamc@62 2751 sgnError env (DuplicateStr (loc, x))
adamc@62 2752 else
adamc@62 2753 ();
adamc@88 2754 (cons, vals, sgns, SS.add (strs, x)))
adamc@203 2755 | L'.SgiConstraint _ => (cons, vals, sgns, strs)
adamc@563 2756 | L'.SgiClassAbs (x, _, _) =>
adamc@211 2757 (if SS.member (cons, x) then
adamc@211 2758 sgnError env (DuplicateCon (loc, x))
adamc@211 2759 else
adamc@211 2760 ();
adamc@211 2761 (SS.add (cons, x), vals, sgns, strs))
adamc@563 2762 | L'.SgiClass (x, _, _, _) =>
adamc@211 2763 (if SS.member (cons, x) then
adamc@211 2764 sgnError env (DuplicateCon (loc, x))
adamc@211 2765 else
adamc@211 2766 ();
adamc@460 2767 (SS.add (cons, x), vals, sgns, strs)))
adamc@62 2768 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
adamc@31 2769 in
adamc@83 2770 ((L'.SgnConst sgis', loc), gs)
adamc@31 2771 end
adamc@31 2772 | L.SgnVar x =>
adamc@31 2773 (case E.lookupSgn env x of
adamc@31 2774 NONE =>
adamc@31 2775 (sgnError env (UnboundSgn (loc, x));
adamc@83 2776 ((L'.SgnError, loc), []))
adamc@83 2777 | SOME (n, sgis) => ((L'.SgnVar n, loc), []))
adamc@41 2778 | L.SgnFun (m, dom, ran) =>
adamc@41 2779 let
adamc@83 2780 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41 2781 val (env', n) = E.pushStrNamed env m dom'
adamc@469 2782 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []}
adamc@469 2783 val (ran', gs2) = elabSgn (env', denv') ran
adamc@41 2784 in
adamc@83 2785 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
adamc@41 2786 end
adamc@42 2787 | L.SgnWhere (sgn, x, c) =>
adamc@42 2788 let
adamc@83 2789 val (sgn', ds1) = elabSgn (env, denv) sgn
adamc@83 2790 val (c', ck, ds2) = elabCon (env, denv) c
adamc@42 2791 in
adamc@42 2792 case #1 (hnormSgn env sgn') of
adamc@83 2793 L'.SgnError => (sgnerror, [])
adamc@42 2794 | L'.SgnConst sgis =>
adamc@75 2795 if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
adamc@75 2796 x' = x andalso
adamc@623 2797 (unifyKinds env k ck
adamc@75 2798 handle KUnify x => sgnError env (WhereWrongKind x);
adamc@42 2799 true)
adamc@42 2800 | _ => false) sgis then
adamc@83 2801 ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2)
adamc@42 2802 else
adamc@42 2803 (sgnError env (UnWhereable (sgn', x));
adamc@83 2804 (sgnerror, []))
adamc@42 2805 | _ => (sgnError env (UnWhereable (sgn', x));
adamc@83 2806 (sgnerror, []))
adamc@42 2807 end
adamc@59 2808 | L.SgnProj (m, ms, x) =>
adamc@59 2809 (case E.lookupStr env m of
adamc@59 2810 NONE => (strError env (UnboundStr (loc, m));
adamc@83 2811 (sgnerror, []))
adamc@59 2812 | SOME (n, sgn) =>
adamc@59 2813 let
adamc@59 2814 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@59 2815 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@59 2816 NONE => (strError env (UnboundStr (loc, m));
adamc@59 2817 (strerror, sgnerror))
adamc@59 2818 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@59 2819 ((L'.StrVar n, loc), sgn) ms
adamc@59 2820 in
adamc@59 2821 case E.projectSgn env {sgn = sgn, str = str, field = x} of
adamc@59 2822 NONE => (sgnError env (UnboundSgn (loc, x));
adamc@83 2823 (sgnerror, []))
adamc@83 2824 | SOME _ => ((L'.SgnProj (n, ms, x), loc), [])
adamc@59 2825 end)
adamc@59 2826
adamc@31 2827
adamc@706 2828 and selfify env {str, strs, sgn} =
adamc@66 2829 case #1 (hnormSgn env sgn) of
adamc@66 2830 L'.SgnError => sgn
adamc@66 2831 | L'.SgnVar _ => sgn
adamc@66 2832
adamc@66 2833 | L'.SgnConst sgis =>
adam@1387 2834 (L'.SgnConst (#1 (ListUtil.foldlMapConcat
adam@1387 2835 (fn (sgi, env) =>
adam@1387 2836 (case sgi of (L'.SgiConAbs (x, n, k), loc) =>
adam@1387 2837 [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
adam@1387 2838 | (L'.SgiDatatype dts, loc) =>
adam@1387 2839 map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts
adam@1387 2840 | (L'.SgiClassAbs (x, n, k), loc) =>
adam@1387 2841 [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
adam@1387 2842 | (L'.SgiStr (x, n, sgn), loc) =>
adam@1387 2843 [(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)]
adam@1387 2844 | x => [x],
adam@1387 2845 E.sgiBinds env sgi)) env sgis)), #2 sgn)
adamc@66 2846 | L'.SgnFun _ => sgn
adamc@66 2847 | L'.SgnWhere _ => sgn
adamc@66 2848 | L'.SgnProj (m, ms, x) =>
adamc@66 2849 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66 2850 (L'.StrVar m, #2 sgn) ms,
adamc@66 2851 sgn = #2 (E.lookupStrNamed env m),
adamc@66 2852 field = x} of
adamc@66 2853 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
adamc@66 2854 | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
adamc@66 2855
adamc@706 2856 and selfifyAt env {str, sgn} =
adamc@66 2857 let
adamc@66 2858 fun self (str, _) =
adamc@66 2859 case str of
adamc@66 2860 L'.StrVar x => SOME (x, [])
adamc@66 2861 | L'.StrProj (str, x) =>
adamc@66 2862 (case self str of
adamc@66 2863 NONE => NONE
adamc@66 2864 | SOME (m, ms) => SOME (m, ms @ [x]))
adamc@66 2865 | _ => NONE
adamc@66 2866 in
adamc@66 2867 case self str of
adamc@66 2868 NONE => sgn
adamc@66 2869 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
adamc@66 2870 end
adamc@66 2871
adamc@706 2872 and dopen env {str, strs, sgn} =
adamc@66 2873 let
adam@1527 2874 fun isVisible x = x <> "" andalso String.sub (x, 0) <> #"?"
adam@1527 2875
adamc@66 2876 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66 2877 (L'.StrVar str, #2 sgn) strs
adamc@66 2878 in
adamc@66 2879 case #1 (hnormSgn env sgn) of
adamc@66 2880 L'.SgnConst sgis =>
adamc@805 2881 ListUtil.foldlMapConcat
adamc@805 2882 (fn ((sgi, loc), env') =>
adamc@805 2883 let
adamc@805 2884 val d =
adamc@805 2885 case sgi of
adamc@805 2886 L'.SgiConAbs (x, n, k) =>
adam@1527 2887 if isVisible x then
adam@1527 2888 let
adam@1527 2889 val c = (L'.CModProj (str, strs, x), loc)
adam@1527 2890 in
adam@1527 2891 [(L'.DCon (x, n, k, c), loc)]
adam@1527 2892 end
adam@1527 2893 else
adam@1527 2894 []
adamc@805 2895 | L'.SgiCon (x, n, k, c) =>
adam@1527 2896 if isVisible x then
adam@1527 2897 [(L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)]
adam@1527 2898 else
adam@1527 2899 []
adamc@805 2900 | L'.SgiDatatype dts =>
adam@1527 2901 List.mapPartial (fn (x, n, xs, xncs) => if isVisible x then
adam@1527 2902 SOME (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
adam@1527 2903 else
adam@1527 2904 NONE) dts
adamc@805 2905 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adam@1527 2906 if isVisible x then
adam@1527 2907 [(L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)]
adam@1527 2908 else
adam@1527 2909 []
adamc@805 2910 | L'.SgiVal (x, n, t) =>
adam@1527 2911 if isVisible x then
adam@1527 2912 [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)]
adam@1527 2913 else
adam@1527 2914 []
adamc@805 2915 | L'.SgiStr (x, n, sgn) =>
adam@1527 2916 if isVisible x then
adam@1527 2917 [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)]
adam@1527 2918 else
adam@1527 2919 []
adamc@805 2920 | L'.SgiSgn (x, n, sgn) =>
adam@1527 2921 if isVisible x then
adam@1527 2922 [(L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)]
adam@1527 2923 else
adam@1527 2924 []
adamc@805 2925 | L'.SgiConstraint (c1, c2) =>
adamc@805 2926 [(L'.DConstraint (c1, c2), loc)]
adamc@805 2927 | L'.SgiClassAbs (x, n, k) =>
adam@1527 2928 if isVisible x then
adam@1527 2929 let
adam@1527 2930 val c = (L'.CModProj (str, strs, x), loc)
adam@1527 2931 in
adam@1527 2932 [(L'.DCon (x, n, k, c), loc)]
adam@1527 2933 end
adam@1527 2934 else
adam@1527 2935 []
adamc@805 2936 | L'.SgiClass (x, n, k, _) =>
adam@1527 2937 if isVisible x then
adam@1527 2938 let
adam@1527 2939 val c = (L'.CModProj (str, strs, x), loc)
adam@1527 2940 in
adam@1527 2941 [(L'.DCon (x, n, k, c), loc)]
adam@1527 2942 end
adam@1527 2943 else
adam@1527 2944 []
adamc@805 2945 in
adamc@805 2946 (d, foldl (fn (d, env') => E.declBinds env' d) env' d)
adamc@805 2947 end)
adamc@805 2948 env sgis
adamc@66 2949 | _ => (strError env (UnOpenable sgn);
adamc@628 2950 ([], env))
adamc@66 2951 end
adamc@66 2952
adamc@706 2953 and sgiOfDecl (d, loc) =
adamc@31 2954 case d of
adamc@123 2955 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
adamc@156 2956 | L'.DDatatype x => [(L'.SgiDatatype x, loc)]
adamc@156 2957 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)]
adamc@123 2958 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
adamc@123 2959 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis
adamc@123 2960 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
adamc@123 2961 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
adamc@123 2962 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
adamc@123 2963 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
adamc@123 2964 | L'.DExport _ => []
adamc@707 2965 | L'.DTable (tn, x, n, c, _, pc, _, cc) =>
adamc@707 2966 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc),
adamc@707 2967 (L'.CConcat (pc, cc), loc)), loc)), loc)]
adamc@460 2968 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
adamc@754 2969 | L'.DView (tn, x, n, _, c) =>
adamc@754 2970 [(L'.SgiVal (x, n, (L'.CApp (viewOf (), c), loc)), loc)]
adamc@563 2971 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
adamc@271 2972 | L'.DDatabase _ => []
adamc@460 2973 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
adamc@720 2974 | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)]
adamc@1075 2975 | L'.DTask _ => []
adamc@1199 2976 | L'.DPolicy _ => []
adam@1294 2977 | L'.DOnError _ => []
adamc@88 2978
adamc@1000 2979 and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
adamc@469 2980 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
adamc@469 2981 ("sgn2", p_sgn env sgn2)];*)
adamc@35 2982 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
adamc@31 2983 (L'.SgnError, _) => ()
adamc@31 2984 | (_, L'.SgnError) => ()
adamc@31 2985
adamc@31 2986 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
adamc@31 2987 let
adamc@362 2988 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
adamc@362 2989 ("sgn2", p_sgn env sgn2),
adamc@362 2990 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),
adamc@362 2991 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*)
adamc@362 2992
adamc@838 2993 fun cpart n = IM.find (!counterparts, n)
adamc@838 2994 fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1)
adamc@838 2995
adamc@838 2996 val sub2 = U.Con.map {kind = fn k => k,
adamc@838 2997 con = fn c =>
adamc@838 2998 case c of
adamc@838 2999 L'.CNamed n2 =>
adamc@838 3000 (case cpart n2 of
adamc@838 3001 NONE => c
adamc@838 3002 | SOME n1 => L'.CNamed n1)
adamc@838 3003 | _ => c}
adamc@838 3004
adamc@628 3005 fun folder (sgi2All as (sgi, loc), env) =
adamc@31 3006 let
adamc@362 3007 (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*)
adamc@362 3008
adamc@805 3009 fun seek' f p =
adamc@31 3010 let
adamc@628 3011 fun seek env ls =
adamc@31 3012 case ls of
adamc@805 3013 [] => f env
adamc@31 3014 | h :: t =>
adamc@469 3015 case p (env, h) of
adamc@469 3016 NONE =>
adamc@469 3017 let
adamc@469 3018 val env = case #1 h of
adamc@469 3019 L'.SgiCon (x, n, k, c) =>
adamc@471 3020 if E.checkENamed env n then
adamc@471 3021 env
adamc@471 3022 else
adamc@471 3023 E.pushCNamedAs env x n k (SOME c)
adamc@469 3024 | L'.SgiConAbs (x, n, k) =>
adamc@471 3025 if E.checkENamed env n then
adamc@471 3026 env
adamc@471 3027 else
adamc@471 3028 E.pushCNamedAs env x n k NONE
adamc@469 3029 | _ => env
adamc@469 3030 in
adamc@628 3031 seek (E.sgiBinds env h) t
adamc@469 3032 end
adamc@88 3033 | SOME envs => envs
adamc@31 3034 in
adamc@628 3035 seek env sgis1
adamc@31 3036 end
adamc@805 3037
adamc@1000 3038 val seek = seek' (fn env => (sgnError env (UnmatchedSgi (strLoc, sgi2All));
adamc@805 3039 env))
adamc@31 3040 in
adamc@31 3041 case sgi of
adamc@31 3042 L'.SgiConAbs (x, n2, k2) =>
adam@1591 3043 seek (fn (env, sgi1All as (sgi1, loc)) =>
adamc@31 3044 let
adamc@41 3045 fun found (x', n1, k1, co1) =
adamc@41 3046 if x = x' then
adamc@41 3047 let
adamc@623 3048 val () = unifyKinds env k1 k2
adamc@41 3049 handle KUnify (k1, k2, err) =>
adam@1591 3050 sgnError env (SgiWrongKind (loc, sgi1All, k1,
adamc@1000 3051 sgi2All, k2, err))
adamc@41 3052 val env = E.pushCNamedAs env x n1 k1 co1
adamc@41 3053 in
adamc@41 3054 SOME (if n1 = n2 then
adamc@41 3055 env
adamc@41 3056 else
adamc@838 3057 (cparts (n2, n1);
adamc@838 3058 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2))))
adamc@41 3059 end
adamc@41 3060 else
adamc@41 3061 NONE
adamc@31 3062 in
adamc@31 3063 case sgi1 of
adamc@41 3064 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
adamc@41 3065 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
adamc@805 3066 | L'.SgiDatatype dts =>
adamc@191 3067 let
adamc@191 3068 val k = (L'.KType, loc)
adamc@805 3069
adamc@805 3070 fun search dts =
adamc@805 3071 case dts of
adamc@805 3072 [] => NONE
adamc@805 3073 | (x', n1, xs, _) :: dts =>
adamc@805 3074 let
adamc@805 3075 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@805 3076 in
adamc@805 3077 case found (x', n1, k', NONE) of
adamc@805 3078 NONE => search dts
adamc@805 3079 | x => x
adamc@805 3080 end
adamc@191 3081 in
adamc@805 3082 search dts
adamc@191 3083 end
adamc@191 3084 | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) =>
adamc@191 3085 let
adamc@191 3086 val k = (L'.KType, loc)
adamc@191 3087 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 3088 in
adamc@191 3089 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
adamc@191 3090 end
adamc@711 3091 | L'.SgiClassAbs (x', n1, k) => found (x', n1, k, NONE)
adamc@711 3092 | L'.SgiClass (x', n1, k, c) => found (x', n1, k, SOME c)
adamc@31 3093 | _ => NONE
adamc@31 3094 end)
adamc@31 3095
adamc@31 3096 | L'.SgiCon (x, n2, k2, c2) =>
adam@1591 3097 seek (fn (env, sgi1All as (sgi1, loc)) =>
adamc@211 3098 let
adamc@211 3099 fun found (x', n1, k1, c1) =
adamc@211 3100 if x = x' then
adamc@211 3101 let
adamc@838 3102 val c2 = sub2 c2
adamc@838 3103
adamc@327 3104 fun good () =
adamc@327 3105 let
adamc@327 3106 val env = E.pushCNamedAs env x n2 k2 (SOME c2)
adamc@327 3107 val env = if n1 = n2 then
adamc@327 3108 env
adamc@327 3109 else
adamc@839 3110 (cparts (n2, n1);
adamc@839 3111 E.pushCNamedAs env x n1 k1 (SOME c1))
adamc@327 3112 in
adamc@628 3113 SOME env
adamc@327 3114 end
adamc@211 3115 in
adamc@987 3116 (unifyCons env loc c1 c2;
adamc@628 3117 good ())
adamc@211 3118 handle CUnify (c1, c2, err) =>
adam@1591 3119 (sgnError env (SgiWrongCon (loc, sgi1All, c1,
adamc@1000 3120 sgi2All, c2, err));
adamc@211 3121 good ())
adamc@211 3122 end
adamc@211 3123 else
adamc@211 3124 NONE
adamc@211 3125 in
adamc@211 3126 case sgi1 of
adamc@211 3127 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
adamc@711 3128 | L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
adamc@211 3129 | _ => NONE
adamc@211 3130 end)
adamc@31 3131
adamc@805 3132 | L'.SgiDatatype dts2 =>
adamc@805 3133 let
adam@1591 3134 fun found' (sgi1All as (_, loc), (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) =
adamc@805 3135 if x1 <> x2 then
adamc@805 3136 NONE
adamc@805 3137 else
adamc@805 3138 let
adamc@805 3139 fun mismatched ue =
adam@1591 3140 (sgnError env (SgiMismatchedDatatypes (loc, sgi1All, sgi2All, ue));
adamc@805 3141 SOME env)
adamc@805 3142
adamc@805 3143 val k = (L'.KType, loc)
adamc@805 3144 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
adamc@805 3145
adamc@805 3146 fun good () =
adamc@805 3147 let
adamc@805 3148 val env = E.sgiBinds env sgi1All
adamc@805 3149 val env = if n1 = n2 then
adamc@805 3150 env
adamc@805 3151 else
adamc@838 3152 (cparts (n2, n1);
adamc@838 3153 E.pushCNamedAs env x1 n2 k'
adamc@838 3154 (SOME (L'.CNamed n1, loc)))
adamc@805 3155 in
adamc@805 3156 SOME env
adamc@805 3157 end
adamc@805 3158
adamc@805 3159 val env = E.pushCNamedAs env x1 n1 k' NONE
adamc@805 3160 val env = if n1 = n2 then
adamc@805 3161 env
adamc@805 3162 else
adamc@838 3163 (cparts (n2, n1);
adamc@838 3164 E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc)))
adamc@805 3165 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
adamc@805 3166 fun xncBad ((x1, _, t1), (x2, _, t2)) =
adamc@805 3167 String.compare (x1, x2) <> EQUAL
adamc@805 3168 orelse case (t1, t2) of
adamc@805 3169 (NONE, NONE) => false
adamc@805 3170 | (SOME t1, SOME t2) =>
adamc@987 3171 (unifyCons env loc t1 (sub2 t2); false)
adamc@805 3172 | _ => true
adamc@805 3173 in
adamc@805 3174 (if xs1 <> xs2
adamc@805 3175 orelse length xncs1 <> length xncs2
adamc@805 3176 orelse ListPair.exists xncBad (xncs1, xncs2) then
adamc@805 3177 mismatched NONE
adamc@160 3178 else
adamc@805 3179 good ())
adamc@805 3180 handle CUnify ue => mismatched (SOME ue)
adamc@805 3181 end
adamc@805 3182 in
adamc@805 3183 seek'
adamc@805 3184 (fn _ =>
adamc@805 3185 let
adamc@805 3186 fun seekOne (dt2, env) =
adamc@805 3187 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@805 3188 case sgi1 of
adamc@805 3189 L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
adamc@805 3190 found' (sgi1All, (x', n1, xs, xncs1), dt2, env)
adamc@805 3191 | _ => NONE)
adamc@805 3192
adamc@805 3193 fun seekAll (dts, env) =
adamc@805 3194 case dts of
adamc@805 3195 [] => env
adamc@805 3196 | dt :: dts => seekAll (dts, seekOne (dt, env))
adamc@805 3197 in
adamc@805 3198 seekAll (dts2, env)
adamc@805 3199 end)
adamc@805 3200 (fn (env, sgi1All as (sgi1, _)) =>
adamc@805 3201 let
adamc@805 3202 fun found dts1 =
adamc@805 3203 let
adamc@805 3204 fun iter (dts1, dts2, env) =
adamc@805 3205 case (dts1, dts2) of
adamc@805 3206 ([], []) => SOME env
adamc@805 3207 | (dt1 :: dts1, dt2 :: dts2) =>
adamc@805 3208 (case found' (sgi1All, dt1, dt2, env) of
adamc@805 3209 NONE => NONE
adamc@805 3210 | SOME env => iter (dts1, dts2, env))
adamc@805 3211 | _ => NONE
adamc@805 3212 in
adamc@805 3213 iter (dts1, dts2, env)
adamc@805 3214 end
adamc@805 3215 in
adamc@805 3216 case sgi1 of
adamc@805 3217 L'.SgiDatatype dts1 => found dts1
adamc@805 3218 | _ => NONE
adamc@805 3219 end)
adamc@805 3220 end
adamc@156 3221
adamc@191 3222 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
adam@1591 3223 seek (fn (env, sgi1All as (sgi1, loc)) =>
adamc@158 3224 case sgi1 of
adamc@191 3225 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) =>
adamc@158 3226 if x = x' then
adamc@158 3227 let
adamc@158 3228 val k = (L'.KType, loc)
adamc@191 3229 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@158 3230 val t1 = (L'.CModProj (m11, ms1, s1), loc)
adamc@158 3231 val t2 = (L'.CModProj (m12, ms2, s2), loc)
adamc@158 3232
adamc@158 3233 fun good () =
adamc@158 3234 let
adamc@191 3235 val env = E.pushCNamedAs env x n1 k' (SOME t1)
adamc@191 3236 val env = E.pushCNamedAs env x n2 k' (SOME t2)
adamc@158 3237 in
adamc@838 3238 cparts (n2, n1);
adamc@628 3239 SOME env
adamc@158 3240 end
adamc@158 3241 in
adamc@987 3242 (unifyCons env loc t1 t2;
adamc@628 3243 good ())
adamc@158 3244 handle CUnify (c1, c2, err) =>
adam@1591 3245 (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err));
adamc@158 3246 good ())
adamc@158 3247 end
adamc@158 3248 else
adamc@158 3249 NONE
adamc@158 3250
adamc@158 3251 | _ => NONE)
adamc@156 3252
adamc@32 3253 | L'.SgiVal (x, n2, c2) =>
adam@1591 3254 seek (fn (env, sgi1All as (sgi1, loc)) =>
adamc@32 3255 case sgi1 of
adamc@41 3256 L'.SgiVal (x', n1, c1) =>
adamc@41 3257 if x = x' then
adamc@838 3258 ((*prefaces "val" [("x", PD.string x),
adamc@838 3259 ("n1", PD.string (Int.toString n1)),
adamc@838 3260 ("c1", p_con env c1),
adamc@838 3261 ("c2", p_con env c2),
adamc@838 3262 ("c2'", p_con env (sub2 c2))];*)
adamc@987 3263 unifyCons env loc c1 (sub2 c2);
adamc@628 3264 SOME env)
adamc@86 3265 handle CUnify (c1, c2, err) =>
adam@1591 3266 (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, err));
adamc@628 3267 SOME env)
adamc@41 3268 else
adamc@41 3269 NONE
adamc@32 3270 | _ => NONE)
adamc@32 3271
adamc@33 3272 | L'.SgiStr (x, n2, sgn2) =>
adam@1591 3273 seek (fn (env, sgi1All as (sgi1, loc)) =>
adamc@33 3274 case sgi1 of
adamc@41 3275 L'.SgiStr (x', n1, sgn1) =>
adamc@41 3276 if x = x' then
adamc@66 3277 let
adam@1591 3278 val () = subSgn' counterparts env loc sgn1 sgn2
adamc@66 3279 val env = E.pushStrNamedAs env x n1 sgn1
adamc@66 3280 val env = if n1 = n2 then
adamc@66 3281 env
adamc@66 3282 else
adamc@66 3283 E.pushStrNamedAs env x n2
adamc@66 3284 (selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
adamc@66 3285 sgn = sgn2})
adamc@66 3286 in
adamc@628 3287 SOME env
adamc@66 3288 end
adamc@41 3289 else
adamc@41 3290 NONE
adamc@33 3291 | _ => NONE)
adamc@59 3292
adamc@59 3293 | L'.SgiSgn (x, n2, sgn2) =>
adam@1591 3294 seek (fn (env, sgi1All as (sgi1, loc)) =>
adamc@59 3295 case sgi1 of
adamc@59 3296 L'.SgiSgn (x', n1, sgn1) =>
adamc@59 3297 if x = x' then
adamc@65 3298 let
adam@1591 3299 val () = subSgn' counterparts env loc sgn1 sgn2
adam@1591 3300 val () = subSgn' counterparts env loc sgn2 sgn1
adamc@65 3301
adamc@65 3302 val env = E.pushSgnNamedAs env x n2 sgn2
adamc@65 3303 val env = if n1 = n2 then
adamc@65 3304 env
adamc@65 3305 else
adamc@838 3306 (cparts (n2, n1);
adamc@838 3307 E.pushSgnNamedAs env x n1 sgn2)
adamc@65 3308 in
adamc@628 3309 SOME env
adamc@65 3310 end
adamc@59 3311 else
adamc@59 3312 NONE
adamc@59 3313 | _ => NONE)
adamc@88 3314
adamc@88 3315 | L'.SgiConstraint (c2, d2) =>
adam@1591 3316 seek (fn (env, sgi1All as (sgi1, loc)) =>
adamc@88 3317 case sgi1 of
adamc@88 3318 L'.SgiConstraint (c1, d1) =>
adamc@987 3319 if consEq env loc (c1, c2)
adamc@987 3320 andalso consEq env loc (d1, d2) then
adamc@628 3321 SOME env
adamc@88 3322 else
adamc@88 3323 NONE
adamc@88 3324 | _ => NONE)
adamc@203 3325
adamc@563 3326 | L'.SgiClassAbs (x, n2, k2) =>
adam@1591 3327 seek (fn (env, sgi1All as (sgi1, loc)) =>
adamc@211 3328 let
adamc@563 3329 fun found (x', n1, k1, co) =
adamc@211 3330 if x = x' then
adamc@211 3331 let
adamc@623 3332 val () = unifyKinds env k1 k2
adamc@563 3333 handle KUnify (k1, k2, err) =>
adam@1591 3334 sgnError env (SgiWrongKind (loc, sgi1All, k1,
adamc@1000 3335 sgi2All, k2, err))
adamc@563 3336
adamc@711 3337 val env = E.pushCNamedAs env x n1 k1 co
adamc@211 3338 in
adamc@211 3339 SOME (if n1 = n2 then
adamc@211 3340 env
adamc@211 3341 else
adamc@838 3342 (cparts (n2, n1);
adamc@838 3343 E.pushCNamedAs env x n2 k1 (SOME (L'.CNamed n1, loc2))))
adamc@211 3344 end
adamc@211 3345 else
adamc@211 3346 NONE
adamc@211 3347 in
adamc@211 3348 case sgi1 of
adamc@563 3349 L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE)
adamc@563 3350 | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c)
adamc@211 3351 | _ => NONE
adamc@211 3352 end)
adamc@563 3353 | L'.SgiClass (x, n2, k2, c2) =>
adam@1591 3354 seek (fn (env, sgi1All as (sgi1, loc)) =>
adamc@211 3355 let
adamc@563 3356 fun found (x', n1, k1, c1) =
adamc@211 3357 if x = x' then
adamc@211 3358 let
adamc@623 3359 val () = unifyKinds env k1 k2
adamc@563 3360 handle KUnify (k1, k2, err) =>
adam@1591 3361 sgnError env (SgiWrongKind (loc, sgi1All, k1,
adamc@1000 3362 sgi2All, k2, err))
adamc@563 3363
adamc@838 3364 val c2 = sub2 c2
adamc@838 3365
adamc@218 3366 fun good () =
adamc@218 3367 let
adamc@711 3368 val env = E.pushCNamedAs env x n2 k2 (SOME c2)
adamc@218 3369 val env = if n1 = n2 then
adamc@218 3370 env
adamc@218 3371 else
adamc@839 3372 (cparts (n2, n1);
adamc@839 3373 E.pushCNamedAs env x n1 k2 (SOME c1))
adamc@218 3374 in
adamc@628 3375 SOME env
adamc@218 3376 end
adamc@211 3377 in
adamc@987 3378 (unifyCons env loc c1 c2;
adamc@628 3379 good ())
adamc@211 3380 handle CUnify (c1, c2, err) =>
adam@1591 3381 (sgnError env (SgiWrongCon (loc, sgi1All, c1,
adamc@1000 3382 sgi2All, c2, err));
adamc@211 3383 good ())
adamc@211 3384 end
adamc@211 3385 else
adamc@211 3386 NONE
adamc@211 3387 in
adamc@211 3388 case sgi1 of
adamc@563 3389 L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
adamc@211 3390 | _ => NONE
adamc@211 3391 end)
adamc@31 3392 end
adamc@31 3393 in
adamc@628 3394 ignore (foldl folder env sgis2)
adamc@31 3395 end
adamc@31 3396
adamc@41 3397 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
adamc@43 3398 let
adamc@480 3399 val ran2 =
adamc@43 3400 if n1 = n2 then
adamc@480 3401 ran2
adamc@43 3402 else
adamc@480 3403 subStrInSgn (n2, n1) ran2
adamc@43 3404 in
adamc@1000 3405 subSgn' counterparts env strLoc dom2 dom1;
adamc@1000 3406 subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) strLoc ran1 ran2
adamc@43 3407 end
adamc@41 3408
adamc@1000 3409 | _ => sgnError env (SgnWrongForm (strLoc, sgn1, sgn2)))
adamc@41 3410
adam@1580 3411 and subSgn env x y z = subSgn' (ref IM.empty) env x y z
adam@1580 3412 handle e as E.UnboundNamed _ => if ErrorMsg.anyErrors () then () else raise e
adamc@61 3413
adamc@706 3414 and positive self =
adamc@312 3415 let
adamc@312 3416 open L
adamc@312 3417
adamc@312 3418 fun none (c, _) =
adamc@312 3419 case c of
adamc@312 3420 CAnnot (c, _) => none c
adamc@312 3421
adamc@312 3422 | TFun (c1, c2) => none c1 andalso none c2
adamc@312 3423 | TCFun (_, _, _, c) => none c
adamc@312 3424 | TRecord c => none c
adamc@312 3425
adamc@312 3426 | CVar ([], x) => x <> self
adamc@312 3427 | CVar _ => true
adamc@312 3428 | CApp (c1, c2) => none c1 andalso none c2
adamc@312 3429 | CAbs _ => false
adamc@628 3430 | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
adamc@312 3431
adamc@623 3432 | CKAbs _ => false
adamc@623 3433 | TKFun _ => false
adamc@623 3434
adamc@312 3435 | CName _ => true
adamc@312 3436
adamc@312 3437 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
adamc@312 3438 | CConcat (c1, c2) => none c1 andalso none c2
adamc@621 3439 | CMap => true
adamc@312 3440
adamc@312 3441 | CUnit => true
adamc@312 3442
adamc@312 3443 | CTuple cs => List.all none cs
adamc@312 3444 | CProj (c, _) => none c
adamc@312 3445
adamc@312 3446 | CWild _ => false
adamc@312 3447
adamc@312 3448 fun pos (c, _) =
adamc@312 3449 case c of
adamc@312 3450 CAnnot (c, _) => pos c
adamc@312 3451
adamc@312 3452 | TFun (c1, c2) => none c1 andalso pos c2
adamc@312 3453 | TCFun (_, _, _, c) => pos c
adamc@312 3454 | TRecord c => pos c
adamc@312 3455
adamc@312 3456 | CVar _ => true
adamc@312 3457 | CApp (c1, c2) => pos c1 andalso none c2
adamc@312 3458 | CAbs _ => false
adamc@628 3459 | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
adamc@312 3460
adamc@623 3461 | CKAbs _ => false
adamc@623 3462 | TKFun _ => false
adamc@623 3463
adamc@312 3464 | CName _ => true
adamc@312 3465
adamc@312 3466 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
adamc@312 3467 | CConcat (c1, c2) => pos c1 andalso pos c2
adamc@621 3468 | CMap => true
adamc@312 3469
adamc@312 3470 | CUnit => true
adamc@312 3471
adamc@312 3472 | CTuple cs => List.all pos cs
adamc@312 3473 | CProj (c, _) => pos c
adamc@312 3474
adamc@312 3475 | CWild _ => false
adamc@312 3476 in
adamc@312 3477 pos
adamc@312 3478 end
adamc@312 3479
adamc@706 3480 and wildifyStr env (str, sgn) =
adamc@325 3481 case #1 (hnormSgn env sgn) of
adamc@325 3482 L'.SgnConst sgis =>
adamc@325 3483 (case #1 str of
adamc@325 3484 L.StrConst ds =>
adamc@325 3485 let
adamc@1270 3486 fun cname d =
adamc@1270 3487 case d of
adamc@1270 3488 L'.SgiCon (x, _, _, _) => SOME x
adamc@1270 3489 | L'.SgiConAbs (x, _, _) => SOME x
adamc@1270 3490 | L'.SgiClass (x, _, _, _) => SOME x
adamc@1270 3491 | L'.SgiClassAbs (x, _, _) => SOME x
adamc@1270 3492 | _ => NONE
adamc@1270 3493
adamc@1270 3494 fun dname (d, _) =
adamc@1270 3495 case d of
adamc@1270 3496 L.DCon (x, _, _) => SOME x
adamc@1270 3497 | L.DClass (x, _, _) => SOME x
adamc@1270 3498 | _ => NONE
adamc@1270 3499
adamc@493 3500 fun decompileKind (k, loc) =
adamc@493 3501 case k of
adamc@493 3502 L'.KType => SOME (L.KType, loc)
adamc@493 3503 | L'.KArrow (k1, k2) =>
adamc@493 3504 (case (decompileKind k1, decompileKind k2) of
adamc@493 3505 (SOME k1, SOME k2) => SOME (L.KArrow (k1, k2), loc)
adamc@493 3506 | _ => NONE)
adamc@493 3507 | L'.KName => SOME (L.KName, loc)
adamc@493 3508 | L'.KRecord k =>
adamc@493 3509 (case decompileKind k of
adamc@493 3510 SOME k => SOME (L.KRecord k, loc)
adamc@493 3511 | _ => NONE)
adamc@493 3512 | L'.KUnit => SOME (L.KUnit, loc)
adamc@493 3513 | L'.KTuple ks =>
adamc@493 3514 let
adamc@493 3515 val ks' = List.mapPartial decompileKind ks
adamc@493 3516 in
adamc@493 3517 if length ks' = length ks then
adamc@493 3518 SOME (L.KTuple ks', loc)
adamc@493 3519 else
adamc@493 3520 NONE
adamc@493 3521 end
adamc@493 3522
adamc@493 3523 | L'.KError => NONE
adam@1639 3524 | L'.KUnif (_, _, ref (L'.KKnown k)) => decompileKind k
adamc@493 3525 | L'.KUnif _ => NONE
adam@1639 3526 | L'.KTupleUnif (_, _, ref (L'.KKnown k)) => decompileKind k
adam@1302 3527 | L'.KTupleUnif _ => NONE
adamc@493 3528
adamc@623 3529 | L'.KRel _ => NONE
adamc@623 3530 | L'.KFun _ => NONE
adamc@623 3531
adam@1529 3532 fun maybeHnorm env c =
adam@1529 3533 hnormCon env c
adam@1529 3534 handle E.UnboundNamed _ => c
adam@1529 3535
adam@1529 3536 fun decompileCon env (c as (_, loc)) =
adam@1529 3537 case #1 (maybeHnorm env c) of
adamc@325 3538 L'.CRel i =>
adamc@325 3539 let
adamc@325 3540 val (s, _) = E.lookupCRel env i
adamc@325 3541 in
adamc@325 3542 SOME (L.CVar ([], s), loc)
adamc@325 3543 end
adamc@325 3544 | L'.CNamed i =>
adamc@325 3545 let
adamc@325 3546 val (s, _, _) = E.lookupCNamed env i
adamc@325 3547 in
adamc@325 3548 SOME (L.CVar ([], s), loc)
adamc@325 3549 end
adamc@325 3550 | L'.CModProj (m1, ms, x) =>
adamc@325 3551 let
adamc@325 3552 val (s, _) = E.lookupStrNamed env m1
adamc@325 3553 in
adamc@325 3554 SOME (L.CVar (s :: ms, x), loc)
adamc@325 3555 end
adamc@325 3556 | L'.CName s => SOME (L.CName s, loc)
adamc@325 3557 | L'.CRecord (_, xcs) =>
adamc@325 3558 let
adamc@325 3559 fun fields xcs =
adamc@325 3560 case xcs of
adamc@325 3561 [] => SOME []
adamc@325 3562 | (x, t) :: xcs =>
adamc@325 3563 case (decompileCon env x, decompileCon env t, fields xcs) of
adamc@325 3564 (SOME x, SOME t, SOME xcs) => SOME ((x, t) :: xcs)
adamc@325 3565 | _ => NONE
adamc@325 3566 in
adamc@325 3567 Option.map (fn xcs => (L.CRecord xcs, loc))
adamc@325 3568 (fields xcs)
adamc@325 3569 end
adamc@325 3570 | L'.CConcat (c1, c2) =>
adamc@325 3571 (case (decompileCon env c1, decompileCon env c2) of
adamc@325 3572 (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc)
adamc@325 3573 | _ => NONE)
adamc@325 3574 | L'.CUnit => SOME (L.CUnit, loc)
adam@1639 3575 | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => decompileCon env (E.mliftConInCon nl c)
adamc@325 3576
adam@1585 3577 | L'.CApp (f, x) =>
adam@1585 3578 (case (decompileCon env f, decompileCon env x) of
adam@1585 3579 (SOME f, SOME x) => SOME (L.CApp (f, x), loc)
adam@1585 3580 | _ => NONE)
adam@1585 3581
adam@1585 3582 | c => (Print.preface ("WTF?", p_con env (c, loc)); NONE)
adamc@325 3583
adamc@1264 3584 fun buildNeeded env sgis =
adamc@1275 3585 #1 (foldl (fn ((sgi, loc), (nd, env')) =>
adamc@1264 3586 (case sgi of
adam@1570 3587 L'.SgiCon (x, _, k, _) => naddCon (nd, x, k)
adam@1570 3588 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, k)
adamc@1264 3589 | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc))
adamc@1264 3590 | L'.SgiVal (x, _, t) =>
adamc@1264 3591 let
adamc@1277 3592 fun should t =
adamc@1277 3593 let
adamc@1277 3594 val t = normClassConstraint env' t
adamc@1277 3595 in
adamc@1277 3596 case #1 t of
adamc@1277 3597 L'.CApp (f, _) => isClassOrFolder env' f
adamc@1277 3598 | L'.TRecord t =>
adamc@1277 3599 (case hnormCon env' t of
adamc@1277 3600 (L'.CApp (f, _), _) =>
adamc@1277 3601 (case hnormCon env' f of
adamc@1277 3602 (L'.CApp (f, cl), loc) =>
adamc@1277 3603 (case hnormCon env' f of
adamc@1277 3604 (L'.CMap _, _) => isClassOrFolder env' cl
adamc@1277 3605 | _ => false)
adamc@1277 3606 | _ => false)
adamc@1277 3607 | _ => false)
adamc@1277 3608 | _ => false
adamc@1277 3609 end
adamc@1270 3610 in
adamc@1277 3611 if should t then
adamc@1277 3612 naddVal (nd, x)
adamc@1277 3613 else
adamc@1277 3614 nd
adamc@1264 3615 end
adamc@1264 3616 | L'.SgiStr (x, _, s) =>
adamc@1270 3617 (case #1 (hnormSgn env' s) of
adamc@1270 3618 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis'))
adamc@1264 3619 | _ => nd)
adamc@1264 3620 | _ => nd,
adamc@1275 3621 E.sgiBinds env' (sgi, loc)))
adamc@1275 3622 (nempty, env) sgis)
adamc@1264 3623
adamc@1264 3624 val nd = buildNeeded env sgis
adamc@1264 3625
adamc@1264 3626 fun removeUsed (nd, ds) =
adamc@1264 3627 foldl (fn ((d, _), nd) =>
adamc@634 3628 case d of
adamc@1264 3629 L.DCon (x, _, _) => ndelCon (nd, x)
adamc@1264 3630 | L.DClass (x, _, _) => ndelCon (nd, x)
adamc@1264 3631 | L.DVal (x, _, _) => ndelVal (nd, x)
adamc@1264 3632 | L.DOpen _ => nempty
adamc@1264 3633 | L.DStr (x, _, (L.StrConst ds', _)) =>
adamc@1264 3634 (case SM.find (nmods nd, x) of
adamc@1264 3635 NONE => nd
adamc@1270 3636 | SOME (env, nd') => naddMod (nd, x, (env, removeUsed (nd', ds'))))
adamc@1264 3637 | _ => nd)
adamc@1264 3638 nd ds
adamc@1264 3639
adamc@1264 3640 val nd = removeUsed (nd, ds)
adamc@1264 3641
adamc@1270 3642 fun extend (env, nd, ds) =
adamc@1264 3643 let
adamc@1264 3644 val ds' = List.mapPartial (fn (env', (c1, c2), loc) =>
adamc@1264 3645 case (decompileCon env' c1, decompileCon env' c2) of
adamc@1264 3646 (SOME c1, SOME c2) =>
adamc@1264 3647 SOME (L.DConstraint (c1, c2), loc)
adam@1586 3648 | _ => NONE) (nconstraints nd)
adamc@1264 3649
adamc@1264 3650 val ds' =
adamc@1264 3651 case SS.listItems (nvals nd) of
adamc@1264 3652 [] => ds'
adamc@1264 3653 | xs =>
adamc@1264 3654 let
adamc@1264 3655 val ewild = (L.EWild, #2 str)
adamc@1264 3656 val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs
adamc@1264 3657 in
adamc@1264 3658 ds'' @ ds'
adamc@1264 3659 end
adamc@1264 3660
adamc@1275 3661 val ds' =
adam@1640 3662 case ncons nd of
adamc@1275 3663 [] => ds'
adamc@1264 3664 | xs =>
adam@1570 3665 map (fn (x, k) =>
adamc@1270 3666 let
adamc@1270 3667 val k =
adamc@1270 3668 case decompileKind k of
adamc@1270 3669 NONE => (L.KWild, #2 str)
adamc@1270 3670 | SOME k => k
adamc@1275 3671
adamc@1270 3672 val cwild = (L.CWild k, #2 str)
adamc@1270 3673 in
adam@1570 3674 (L.DCon (x, NONE, cwild), #2 str)
adamc@1275 3675 end) xs @ ds'
adamc@1275 3676
adamc@1275 3677 val ds = ds @ ds'
adamc@1264 3678 in
adamc@1270 3679 map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) =>
adamc@1270 3680 (case SM.find (nmods nd, x) of
adamc@1270 3681 NONE => d
adamc@1270 3682 | SOME (env, nd') =>
adamc@1270 3683 (L.DStr (x, s, (L.StrConst (extend (env, nd', ds')), loc')), loc))
adamc@1270 3684 | d => d) ds
adamc@1264 3685 end
adamc@325 3686 in
adamc@1270 3687 (L.StrConst (extend (env, nd, ds)), #2 str)
adamc@325 3688 end
adamc@325 3689 | _ => str)
adamc@325 3690 | _ => str
adamc@325 3691
adamc@706 3692 and elabDecl (dAll as (d, loc), (env, denv, gs)) =
adamc@255 3693 let
adamc@904 3694 (*val () = preface ("elabDecl", SourcePrint.p_decl dAll)*)
adamc@514 3695 (*val befor = Time.now ()*)
adamc@255 3696
adamc@255 3697 val r =
adamc@255 3698 case d of
adamc@255 3699 L.DCon (x, ko, c) =>
adamc@255 3700 let
adamc@255 3701 val k' = case ko of
adam@1639 3702 NONE => kunif env loc
adamc@623 3703 | SOME k => elabKind env k
adamc@255 3704
adamc@255 3705 val (c', ck, gs') = elabCon (env, denv) c
adamc@255 3706 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@255 3707 in
adamc@255 3708 checkKind env c' ck k';
adamc@255 3709
adamc@255 3710 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
adamc@255 3711 end
adamc@805 3712 | L.DDatatype dts =>
adamc@255 3713 let
adamc@255 3714 val k = (L'.KType, loc)
adamc@805 3715
adamc@805 3716 val (dts, env) = ListUtil.foldlMap
adamc@805 3717 (fn ((x, xs, xcs), env) =>
adamc@805 3718 let
adamc@805 3719 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@805 3720 val (env, n) = E.pushCNamed env x k' NONE
adamc@805 3721 in
adamc@805 3722 ((x, n, xs, xcs), env)
adamc@805 3723 end)
adamc@805 3724 env dts
adamc@805 3725
adamc@805 3726 val (dts, (env, gs')) = ListUtil.foldlMap
adamc@805 3727 (fn ((x, n, xs, xcs), (env, gs')) =>
adamc@805 3728 let
adamc@805 3729 val t = (L'.CNamed n, loc)
adamc@805 3730 val nxs = length xs - 1
adamc@805 3731 val t = ListUtil.foldli
adamc@805 3732 (fn (i, _, t) =>
adamc@805 3733 (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@805 3734
adamc@805 3735 val (env', denv') = foldl (fn (x, (env', denv')) =>
adamc@805 3736 (E.pushCRel env' x k,
adamc@805 3737 D.enter denv')) (env, denv) xs
adamc@805 3738
adamc@805 3739 val (xcs, (used, env, gs')) =
adamc@805 3740 ListUtil.foldlMap
adamc@805 3741 (fn ((x, to), (used, env, gs)) =>
adamc@805 3742 let
adamc@805 3743 val (to, t, gs') = case to of
adamc@805 3744 NONE => (NONE, t, gs)
adamc@805 3745 | SOME t' =>
adamc@805 3746 let
adamc@805 3747 val (t', tk, gs') = elabCon (env', denv') t'
adamc@805 3748 in
adamc@805 3749 checkKind env' t' tk k;
adamc@805 3750 (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
adamc@805 3751 end
adamc@805 3752 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
adamc@805 3753
adamc@805 3754 val (env, n') = E.pushENamed env x t
adamc@805 3755 in
adamc@805 3756 if SS.member (used, x) then
adamc@805 3757 strError env (DuplicateConstructor (x, loc))
adamc@805 3758 else
adamc@805 3759 ();
adamc@805 3760 ((x, n', to), (SS.add (used, x), env, gs'))
adamc@805 3761 end)
adamc@805 3762 (SS.empty, env, gs') xcs
adamc@805 3763 in
adamc@805 3764 ((x, n, xs, xcs), (E.pushDatatype env n xs xcs, gs'))
adamc@805 3765 end)
adamc@805 3766 (env, []) dts
adamc@255 3767 in
adamc@805 3768 ([(L'.DDatatype dts, loc)], (env, denv, gs' @ gs))
adamc@255 3769 end
adamc@255 3770
adamc@255 3771 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
adamc@255 3772
adamc@255 3773 | L.DDatatypeImp (x, m1 :: ms, s) =>
adamc@255 3774 (case E.lookupStr env m1 of
adamc@255 3775 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@255 3776 ([], (env, denv, gs)))
adamc@255 3777 | SOME (n, sgn) =>
adamc@255 3778 let
adamc@255 3779 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@255 3780 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@255 3781 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@255 3782 (strerror, sgnerror))
adamc@255 3783 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@255 3784 ((L'.StrVar n, loc), sgn) ms
adamc@255 3785 in
adamc@628 3786 case hnormCon env (L'.CModProj (n, ms, s), loc) of
adamc@628 3787 (L'.CModProj (n, ms, s), _) =>
adamc@255 3788 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
adamc@255 3789 NONE => (conError env (UnboundDatatype (loc, s));
adamc@255 3790 ([], (env, denv, gs)))
adamc@255 3791 | SOME (xs, xncs) =>
adamc@255 3792 let
adamc@255 3793 val k = (L'.KType, loc)
adamc@255 3794 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@255 3795 val t = (L'.CModProj (n, ms, s), loc)
adamc@255 3796 val (env, n') = E.pushCNamed env x k' (SOME t)
adamc@255 3797 val env = E.pushDatatype env n' xs xncs
adamc@255 3798
adamc@255 3799 val t = (L'.CNamed n', loc)
adamc@844 3800 val nxs = length xs
adamc@844 3801 val t = ListUtil.foldli (fn (i, _, t) =>
adamc@844 3802 (L'.CApp (t, (L'.CRel (nxs - 1 - i), loc)), loc))
adamc@844 3803 t xs
adamc@255 3804 val env = foldl (fn ((x, n, to), env) =>
adamc@255 3805 let
adamc@255 3806 val t = case to of
adamc@255 3807 NONE => t
adamc@255 3808 | SOME t' => (L'.TFun (t', t), loc)
adamc@255 3809
adamc@255 3810 val t = foldr (fn (x, t) =>
adamc@255 3811 (L'.TCFun (L'.Implicit, x, k, t), loc))
adamc@255 3812 t xs
adamc@255 3813 in
adamc@255 3814 E.pushENamedAs env x n t
adamc@255 3815 end) env xncs
adamc@255 3816 in
adamc@628 3817 ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
adamc@255 3818 end)
adamc@255 3819 | _ => (strError env (NotDatatype loc);
adamc@255 3820 ([], (env, denv, [])))
adamc@255 3821 end)
adamc@255 3822
adamc@255 3823 | L.DVal (x, co, e) =>
adamc@255 3824 let
adamc@255 3825 val (c', _, gs1) = case co of
adam@1639 3826 NONE => (cunif env (loc, ktype), ktype, [])
adamc@255 3827 | SOME c => elabCon (env, denv) c
adamc@255 3828
adamc@255 3829 val (e', et, gs2) = elabExp (env, denv) e
adamc@629 3830
adamc@629 3831 val () = checkCon env e' et c'
adamc@629 3832
adamc@674 3833 val c' = normClassConstraint env c'
adamc@255 3834 val (env', n) = E.pushENamed env x c'
adamc@255 3835 in
adamc@255 3836 (*prefaces "DVal" [("x", Print.PD.string x),
adamc@362 3837 ("c'", p_con env c')];*)
adamc@628 3838 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs))
adamc@255 3839 end
adamc@255 3840 | L.DValRec vis =>
adamc@255 3841 let
adamc@255 3842 fun allowable (e, _) =
adamc@255 3843 case e of
adamc@255 3844 L.EAbs _ => true
adamc@255 3845 | L.ECAbs (_, _, _, e) => allowable e
adamc@623 3846 | L.EKAbs (_, e) => allowable e
adamc@255 3847 | L.EDisjoint (_, _, e) => allowable e
adamc@255 3848 | _ => false
adamc@255 3849
adamc@255 3850 val (vis, gs) = ListUtil.foldlMap
adamc@255 3851 (fn ((x, co, e), gs) =>
adamc@255 3852 let
adamc@255 3853 val (c', _, gs1) = case co of
adam@1639 3854 NONE => (cunif env (loc, ktype), ktype, [])
adamc@255 3855 | SOME c => elabCon (env, denv) c
adamc@674 3856 val c' = normClassConstraint env c'
adamc@255 3857 in
adamc@255 3858 ((x, c', e), enD gs1 @ gs)
adamc@280 3859 end) gs vis
adamc@255 3860
adamc@255 3861 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
adamc@255 3862 let
adamc@255 3863 val (env, n) = E.pushENamed env x c'
adamc@255 3864 in
adamc@255 3865 ((x, n, c', e), env)
adamc@255 3866 end) env vis
adamc@255 3867
adamc@255 3868 val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
adamc@255 3869 let
adamc@255 3870 val (e', et, gs1) = elabExp (env, denv) e
adamc@255 3871 in
adamc@628 3872 checkCon env e' et c';
adamc@255 3873 if allowable e then
adamc@255 3874 ()
adamc@255 3875 else
adamc@255 3876 expError env (IllegalRec (x, e'));
adamc@628 3877 ((x, n, c', e'), gs1 @ gs)
adamc@255 3878 end) gs vis
adamc@255 3879 in
adamc@255 3880 ([(L'.DValRec vis, loc)], (env, denv, gs))
adamc@255 3881 end
adamc@255 3882
adamc@255 3883 | L.DSgn (x, sgn) =>
adamc@255 3884 let
adamc@255 3885 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@255 3886 val (env', n) = E.pushSgnNamed env x sgn'
adamc@255 3887 in
adamc@255 3888 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
adamc@255 3889 end
adamc@255 3890
adamc@255 3891 | L.DStr (x, sgno, str) =>
adamc@255 3892 let
adamc@255 3893 val () = if x = "Basis" then
adamc@255 3894 raise Fail "Not allowed to redefine structure 'Basis'"
adamc@255 3895 else
adamc@255 3896 ()
adamc@255 3897
adamc@255 3898 val formal = Option.map (elabSgn (env, denv)) sgno
adamc@255 3899
adamc@255 3900 val (str', sgn', gs') =
adamc@255 3901 case formal of
adamc@255 3902 NONE =>
adamc@255 3903 let
adamc@255 3904 val (str', actual, gs') = elabStr (env, denv) str
adamc@255 3905 in
adamc@255 3906 (str', selfifyAt env {str = str', sgn = actual}, gs')
adamc@255 3907 end
adamc@255 3908 | SOME (formal, gs1) =>
adamc@255 3909 let
adamc@325 3910 val str = wildifyStr env (str, formal)
adamc@255 3911 val (str', actual, gs2) = elabStr (env, denv) str
adamc@255 3912 in
adamc@1000 3913 subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal;
adamc@255 3914 (str', formal, enD gs1 @ gs2)
adamc@255 3915 end
adamc@255 3916
adamc@255 3917 val (env', n) = E.pushStrNamed env x sgn'
adamc@834 3918 val denv' =
adamc@834 3919 case #1 str' of
adamc@834 3920 L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
adamc@1022 3921 | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []}
adamc@834 3922 | _ => denv
adamc@255 3923 in
adamc@255 3924 case #1 (hnormSgn env sgn') of
adamc@255 3925 L'.SgnFun _ =>
adamc@255 3926 (case #1 str' of
adamc@255 3927 L'.StrFun _ => ()
adamc@255 3928 | _ => strError env (FunctorRebind loc))
adamc@255 3929 | _ => ();
adamc@834 3930 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv', gs' @ gs))
adamc@255 3931 end
adamc@255 3932
adamc@255 3933 | L.DFfiStr (x, sgn) =>
adamc@255 3934 let
adamc@255 3935 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@255 3936
adamc@255 3937 val (env', n) = E.pushStrNamed env x sgn'
adamc@255 3938 in
adamc@255 3939 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
adamc@255 3940 end
adamc@255 3941
adamc@255 3942 | L.DOpen (m, ms) =>
adamc@255 3943 (case E.lookupStr env m of
adamc@255 3944 NONE => (strError env (UnboundStr (loc, m));
adamc@255 3945 ([], (env, denv, gs)))
adamc@255 3946 | SOME (n, sgn) =>
adamc@255 3947 let
adamc@1030 3948 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@1030 3949 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@1030 3950 NONE => (strError env (UnboundStr (loc, m));
adamc@1030 3951 (strerror, sgnerror))
adamc@1030 3952 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@1030 3953 ((L'.StrVar n, loc), sgn) ms
adamc@1030 3954
adamc@1030 3955 val sgn = selfifyAt env {str = str, sgn = sgn}
adamc@255 3956
adamc@628 3957 val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn}
adamc@628 3958 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = ms}
adamc@255 3959 in
adamc@255 3960 (ds, (env', denv', gs))
adamc@255 3961 end)
adamc@255 3962
adamc@255 3963 | L.DConstraint (c1, c2) =>
adamc@255 3964 let
adamc@255 3965 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@255 3966 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@255 3967 val gs3 = D.prove env denv (c1', c2', loc)
adamc@255 3968
adamc@628 3969 val denv' = D.assert env denv (c1', c2')
adamc@255 3970 in
adam@1639 3971 checkKind env c1' k1 (L'.KRecord (kunif env loc), loc);
adam@1639 3972 checkKind env c2' k2 (L'.KRecord (kunif env loc), loc);
adamc@255 3973
adamc@628 3974 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ gs))
adamc@255 3975 end
adamc@255 3976
adamc@255 3977 | L.DOpenConstraints (m, ms) =>
adamc@255 3978 let
adamc@255 3979 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
adamc@255 3980 in
adamc@255 3981 ([], (env, denv, gs))
adamc@255 3982 end
adamc@255 3983
adamc@255 3984 | L.DExport str =>
adamc@255 3985 let
adamc@255 3986 val (str', sgn, gs') = elabStr (env, denv) str
adamc@255 3987
adamc@255 3988 val sgn =
adamc@255 3989 case #1 (hnormSgn env sgn) of
adamc@255 3990 L'.SgnConst sgis =>
adamc@255 3991 let
adamc@255 3992 fun doOne (all as (sgi, _), env) =
adamc@255 3993 (case sgi of
adamc@255 3994 L'.SgiVal (x, n, t) =>
adamc@325 3995 let
adamc@325 3996 fun doPage (makeRes, ran) =
adamc@628 3997 case hnormCon env ran of
adamc@628 3998 (L'.CApp (tf, arg), _) =>
adamc@628 3999 (case (hnormCon env tf, hnormCon env arg) of
adamc@628 4000 ((L'.CModProj (basis, [], "transaction"), _),
adamc@720 4001 (L'.CApp (tf, arg3), _)) =>
adamc@325 4002 (case (basis = !basis_r,
adamc@720 4003 hnormCon env tf, hnormCon env arg3) of
adamc@325 4004 (true,
adamc@720 4005 (L'.CApp (tf, arg2), _),
adamc@628 4006 ((L'.CRecord (_, []), _))) =>
adamc@720 4007 (case (hnormCon env tf) of
adamc@720 4008 (L'.CApp (tf, arg1), _) =>
adamc@720 4009 (case (hnormCon env tf,
adamc@720 4010 hnormCon env arg1,
adamc@720 4011 hnormCon env arg2) of
adamc@720 4012 (tf, arg1,
adamc@720 4013 (L'.CRecord (_, []), _)) =>
adamc@720 4014 let
adamc@720 4015 val t = (L'.CApp (tf, arg1), loc)
adamc@720 4016 val t = (L'.CApp (t, arg2), loc)
adamc@720 4017 val t = (L'.CApp (t, arg3), loc)
adamc@720 4018 val t = (L'.CApp (
adamc@720 4019 (L'.CModProj
adamc@720 4020 (basis, [], "transaction"), loc),
adamc@325 4021 t), loc)
adam@1347 4022
adam@1347 4023 fun normArgs t =
adam@1347 4024 case hnormCon env t of
adam@1347 4025 (L'.TFun (dom, ran), loc) =>
adam@1347 4026 (L'.TFun (hnormCon env dom, normArgs ran), loc)
adam@1347 4027 | t' => t'
adamc@720 4028 in
adam@1347 4029 (L'.SgiVal (x, n, normArgs (makeRes t)), loc)
adamc@720 4030 end
adamc@325 4031 | _ => all)
adamc@325 4032 | _ => all)
adamc@325 4033 | _ => all)
adamc@325 4034 | _ => all)
adamc@325 4035 | _ => all
adamc@325 4036 in
adamc@628 4037 case hnormCon env t of
adamc@628 4038 (L'.TFun (dom, ran), _) =>
adamc@628 4039 (case hnormCon env dom of
adamc@628 4040 (L'.TRecord domR, _) =>
adamc@325 4041 doPage (fn t => (L'.TFun ((L'.TRecord domR,
adamc@325 4042 loc),
adamc@325 4043 t), loc), ran)
adamc@325 4044 | _ => all)
adamc@325 4045 | _ => doPage (fn t => t, t)
adamc@325 4046 end
adamc@255 4047 | _ => all,
adamc@255 4048 E.sgiBinds env all)
adamc@255 4049 in
adamc@255 4050 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
adamc@255 4051 end
adamc@255 4052 | _ => sgn
adamc@255 4053 in
adamc@255 4054 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
adamc@255 4055 end
adamc@255 4056
adamc@707 4057 | L.DTable (x, c, pe, ce) =>
adamc@255 4058 let
adamc@707 4059 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
adamc@707 4060
adamc@255 4061 val (c', k, gs') = elabCon (env, denv) c
adam@1639 4062 val pkey = cunif env (loc, cstK)
adam@1639 4063 val uniques = cunif env (loc, cstK)
adamc@705 4064
adamc@705 4065 val ct = tableOf ()
adamc@705 4066 val ct = (L'.CApp (ct, c'), loc)
adamc@707 4067 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc)
adamc@705 4068
adamc@705 4069 val (env, n) = E.pushENamed env x ct
adamc@707 4070 val (pe', pet, gs'') = elabExp (env, denv) pe
adamc@707 4071 val (ce', cet, gs''') = elabExp (env, denv) ce
adamc@707 4072
adamc@707 4073 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc)
adamc@707 4074 val pst = (L'.CApp (pst, c'), loc)
adamc@707 4075 val pst = (L'.CApp (pst, pkey), loc)
adamc@704 4076
adamc@704 4077 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
adamc@704 4078 val cst = (L'.CApp (cst, c'), loc)
adamc@705 4079 val cst = (L'.CApp (cst, uniques), loc)
adamc@255 4080 in
adamc@255 4081 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
adamc@707 4082 checkCon env pe' pet pst;
adamc@707 4083 checkCon env ce' cet cst;
adamc@707 4084 ([(L'.DTable (!basis_r, x, n, c', pe', pkey, ce', uniques), loc)],
adamc@707 4085 (env, denv, gs''' @ gs'' @ enD gs' @ gs))
adamc@255 4086 end
adamc@338 4087 | L.DSequence x =>
adamc@338 4088 let
adamc@338 4089 val (env, n) = E.pushENamed env x (sequenceOf ())
adamc@338 4090 in
adamc@338 4091 ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs))
adamc@338 4092 end
adamc@754 4093 | L.DView (x, e) =>
adamc@754 4094 let
adamc@754 4095 val (e', t, gs') = elabExp (env, denv) e
adamc@754 4096
adamc@754 4097 val k = (L'.KRecord (L'.KType, loc), loc)
adam@1639 4098 val fs = cunif env (loc, k)
adam@1639 4099 val ts = cunif env (loc, (L'.KRecord k, loc))
adamc@754 4100 val tf = (L'.CApp ((L'.CMap (k, k), loc),
adamc@754 4101 (L'.CAbs ("_", k, (L'.CRecord ((L'.KType, loc), []), loc)), loc)), loc)
adamc@754 4102 val ts = (L'.CApp (tf, ts), loc)
adamc@754 4103
adamc@754 4104 val cv = viewOf ()
adamc@754 4105 val cv = (L'.CApp (cv, fs), loc)
adamc@754 4106 val (env', n) = E.pushENamed env x cv
adamc@754 4107
adamc@754 4108 val ct = queryOf ()
adamc@1191 4109 val ct = (L'.CApp (ct, (L'.CRecord ((L'.KRecord (L'.KType, loc), loc), []), loc)), loc)
adam@1395 4110 val ct = (L'.CApp (ct, (L'.CRecord ((L'.KRecord (L'.KType, loc), loc), []), loc)), loc)
adamc@754 4111 val ct = (L'.CApp (ct, ts), loc)
adamc@754 4112 val ct = (L'.CApp (ct, fs), loc)
adamc@754 4113 in
adamc@754 4114 checkCon env e' t ct;
adamc@754 4115 ([(L'.DView (!basis_r, x, n, e', fs), loc)],
adamc@754 4116 (env', denv, gs' @ gs))
adamc@754 4117 end
adamc@255 4118
adamc@563 4119 | L.DClass (x, k, c) =>
adamc@255 4120 let
adamc@623 4121 val k = elabKind env k
adamc@280 4122 val (c', ck, gs') = elabCon (env, denv) c
adamc@711 4123 val (env, n) = E.pushCNamed env x k (SOME c')
adamc@255 4124 val env = E.pushClass env n
adamc@255 4125 in
adamc@711 4126 checkKind env c' ck k;
adamc@563 4127 ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs))
adamc@255 4128 end
adamc@271 4129
adamc@280 4130 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
adamc@280 4131
adamc@459 4132 | L.DCookie (x, c) =>
adamc@459 4133 let
adamc@459 4134 val (c', k, gs') = elabCon (env, denv) c
adamc@459 4135 val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc)
adamc@459 4136 in
adamc@459 4137 checkKind env c' k (L'.KType, loc);
adamc@459 4138 ([(L'.DCookie (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
adamc@459 4139 end
adamc@720 4140 | L.DStyle x =>
adamc@718 4141 let
adamc@720 4142 val (env, n) = E.pushENamed env x (styleOf ())
adamc@718 4143 in
adamc@720 4144 ([(L'.DStyle (!basis_r, x, n), loc)], (env, denv, gs))
adamc@718 4145 end
adamc@1075 4146 | L.DTask (e1, e2) =>
adamc@1073 4147 let
adamc@1075 4148 val (e1', t1, gs1) = elabExp (env, denv) e1
adamc@1075 4149 val (e2', t2, gs2) = elabExp (env, denv) e2
adamc@1075 4150
adam@1639 4151 val targ = cunif env (loc, (L'.KType, loc))
adam@1348 4152
adamc@1075 4153 val t1' = (L'.CModProj (!basis_r, [], "task_kind"), loc)
adam@1348 4154 val t1' = (L'.CApp (t1', targ), loc)
adam@1348 4155
adamc@1075 4156 val t2' = (L'.CApp ((L'.CModProj (!basis_r, [], "transaction"), loc),
adamc@1075 4157 (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)), loc)
adam@1348 4158 val t2' = (L'.TFun (targ, t2'), loc)
adamc@1073 4159 in
adamc@1075 4160 checkCon env e1' t1 t1';
adamc@1075 4161 checkCon env e2' t2 t2';
adamc@1075 4162 ([(L'.DTask (e1', e2'), loc)], (env, denv, gs2 @ gs1 @ gs))
adamc@1073 4163 end
adamc@1199 4164 | L.DPolicy e1 =>
adamc@1199 4165 let
adamc@1199 4166 val (e1', t1, gs1) = elabExp (env, denv) e1
adamc@1199 4167
adamc@1199 4168 val t1' = (L'.CModProj (!basis_r, [], "sql_policy"), loc)
adamc@1199 4169 in
adamc@1199 4170 checkCon env e1' t1 t1';
adamc@1199 4171 ([(L'.DPolicy e1', loc)], (env, denv, gs1 @ gs))
adamc@1199 4172 end
adamc@459 4173
adam@1294 4174 | L.DOnError (m1, ms, s) =>
adam@1294 4175 (case E.lookupStr env m1 of
adam@1294 4176 NONE => (expError env (UnboundStrInExp (loc, m1));
adam@1294 4177 ([], (env, denv, [])))
adam@1294 4178 | SOME (n, sgn) =>
adam@1294 4179 let
adam@1294 4180 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adam@1294 4181 case E.projectStr env {sgn = sgn, str = str, field = m} of
adam@1294 4182 NONE => (conError env (UnboundStrInCon (loc, m));
adam@1294 4183 (strerror, sgnerror))
adam@1294 4184 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adam@1294 4185 ((L'.StrVar n, loc), sgn) ms
adam@1294 4186
adam@1294 4187 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
adam@1294 4188 NONE => (expError env (UnboundExp (loc, s));
adam@1294 4189 cerror)
adam@1294 4190 | SOME t => t
adam@1294 4191
adam@1294 4192 val page = (L'.CModProj (!basis_r, [], "page"), loc)
adam@1294 4193 val xpage = (L'.CApp ((L'.CModProj (!basis_r, [], "transaction"), loc), page), loc)
adam@1294 4194 val func = (L'.TFun ((L'.CModProj (!basis_r, [], "xbody"), loc), xpage), loc)
adam@1294 4195 in
adam@1407 4196 (unifyCons env loc t func
adam@1407 4197 handle CUnify _ => ErrorMsg.error "onError handler has wrong type.");
adam@1294 4198 ([(L'.DOnError (n, ms, s), loc)], (env, denv, gs))
adam@1294 4199 end)
adam@1294 4200
adamc@280 4201 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
adamc@255 4202 in
adamc@904 4203 (*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll)];*)
adamc@255 4204 r
adamc@255 4205 end
adamc@211 4206
adamc@83 4207 and elabStr (env, denv) (str, loc) =
adamc@31 4208 case str of
adamc@31 4209 L.StrConst ds =>
adamc@31 4210 let
adamc@88 4211 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
adamc@123 4212 val sgis = ListUtil.mapConcat sgiOfDecl ds'
adamc@63 4213
adamc@63 4214 val (sgis, _, _, _, _) =
adamc@64 4215 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
adamc@63 4216 case sgi of
adamc@64 4217 L'.SgiConAbs (x, n, k) =>
adamc@64 4218 let
adamc@64 4219 val (cons, x) =
adamc@64 4220 if SS.member (cons, x) then
adamc@64 4221 (cons, "?" ^ x)
adamc@64 4222 else
adamc@64 4223 (SS.add (cons, x), x)
adamc@64 4224 in
adamc@64 4225 ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 4226 end
adamc@64 4227 | L'.SgiCon (x, n, k, c) =>
adamc@64 4228 let
adamc@64 4229 val (cons, x) =
adamc@64 4230 if SS.member (cons, x) then
adamc@64 4231 (cons, "?" ^ x)
adamc@64 4232 else
adamc@64 4233 (SS.add (cons, x), x)
adamc@64 4234 in
adamc@64 4235 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 4236 end
adamc@805 4237 | L'.SgiDatatype dts =>
adamc@156 4238 let
adamc@805 4239 fun doOne ((x, n, xs, xncs), (cons, vals)) =
adamc@805 4240 let
adamc@805 4241 val (cons, x) =
adamc@805 4242 if SS.member (cons, x) then
adamc@805 4243 (cons, "?" ^ x)
adamc@156 4244 else
adamc@805 4245 (SS.add (cons, x), x)
adamc@805 4246
adamc@805 4247 val (xncs, vals) =
adamc@805 4248 ListUtil.foldlMap
adamc@805 4249 (fn ((x, n, t), vals) =>
adamc@805 4250 if SS.member (vals, x) then
adamc@805 4251 (("?" ^ x, n, t), vals)
adamc@805 4252 else
adamc@805 4253 ((x, n, t), SS.add (vals, x)))
adamc@805 4254 vals xncs
adamc@805 4255 in
adamc@805 4256 ((x, n, xs, xncs), (cons, vals))
adamc@805 4257 end
adamc@805 4258
adamc@805 4259 val (dts, (cons, vals)) = ListUtil.foldlMap doOne (cons, vals) dts
adamc@156 4260 in
adamc@805 4261 ((L'.SgiDatatype dts, loc) :: sgis, cons, vals, sgns, strs)
adamc@156 4262 end
adamc@191 4263 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@156 4264 let
adamc@156 4265 val (cons, x) =
adamc@156 4266 if SS.member (cons, x) then
adamc@156 4267 (cons, "?" ^ x)
adamc@156 4268 else
adamc@156 4269 (SS.add (cons, x), x)
adamc@156 4270 in
adamc@191 4271 ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
adamc@156 4272 end
adamc@64 4273 | L'.SgiVal (x, n, c) =>
adamc@64 4274 let
adamc@64 4275 val (vals, x) =
adamc@64 4276 if SS.member (vals, x) then
adamc@64 4277 (vals, "?" ^ x)
adamc@64 4278 else
adamc@64 4279 (SS.add (vals, x), x)
adamc@64 4280 in
adamc@64 4281 ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 4282 end
adamc@64 4283 | L'.SgiSgn (x, n, sgn) =>
adamc@64 4284 let
adamc@64 4285 val (sgns, x) =
adamc@64 4286 if SS.member (sgns, x) then
adamc@64 4287 (sgns, "?" ^ x)
adamc@64 4288 else
adamc@64 4289 (SS.add (sgns, x), x)
adamc@64 4290 in
adamc@64 4291 ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 4292 end
adamc@64 4293
adamc@64 4294 | L'.SgiStr (x, n, sgn) =>
adamc@64 4295 let
adamc@64 4296 val (strs, x) =
adamc@64 4297 if SS.member (strs, x) then
adamc@64 4298 (strs, "?" ^ x)
adamc@64 4299 else
adamc@64 4300 (SS.add (strs, x), x)
adamc@64 4301 in
adamc@64 4302 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@88 4303 end
adamc@203 4304 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
adamc@563 4305 | L'.SgiClassAbs (x, n, k) =>
adamc@211 4306 let
adamc@211 4307 val (cons, x) =
adamc@211 4308 if SS.member (cons, x) then
adamc@211 4309 (cons, "?" ^ x)
adamc@211 4310 else
adamc@211 4311 (SS.add (cons, x), x)
adamc@211 4312 in
adamc@563 4313 ((L'.SgiClassAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
adamc@211 4314 end
adamc@563 4315 | L'.SgiClass (x, n, k, c) =>
adamc@211 4316 let
adamc@211 4317 val (cons, x) =
adamc@211 4318 if SS.member (cons, x) then
adamc@211 4319 (cons, "?" ^ x)
adamc@211 4320 else
adamc@211 4321 (SS.add (cons, x), x)
adamc@211 4322 in
adamc@563 4323 ((L'.SgiClass (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@203 4324 end)
adamc@64 4325
adamc@63 4326 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
adamc@31 4327 in
adamc@83 4328 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)
adamc@31 4329 end
adamc@31 4330 | L.StrVar x =>
adamc@31 4331 (case E.lookupStr env x of
adamc@31 4332 NONE =>
adamc@31 4333 (strError env (UnboundStr (loc, x));
adamc@83 4334 (strerror, sgnerror, []))
adamc@83 4335 | SOME (n, sgn) => ((L'.StrVar n, loc), sgn, []))
adamc@34 4336 | L.StrProj (str, x) =>
adamc@34 4337 let
adamc@83 4338 val (str', sgn, gs) = elabStr (env, denv) str
adamc@34 4339 in
adamc@34 4340 case E.projectStr env {str = str', sgn = sgn, field = x} of
adamc@34 4341 NONE => (strError env (UnboundStr (loc, x));
adamc@83 4342 (strerror, sgnerror, []))
adamc@83 4343 | SOME sgn => ((L'.StrProj (str', x), loc), sgn, gs)
adamc@34 4344 end
adamc@41 4345 | L.StrFun (m, dom, ranO, str) =>
adamc@41 4346 let
adamc@83 4347 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41 4348 val (env', n) = E.pushStrNamed env m dom'
adamc@834 4349 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []}
adamc@834 4350 val (str', actual, gs2) = elabStr (env', denv') str
adamc@41 4351
adamc@83 4352 val (formal, gs3) =
adamc@41 4353 case ranO of
adamc@83 4354 NONE => (actual, [])
adamc@41 4355 | SOME ran =>
adamc@41 4356 let
adamc@834 4357 val (ran', gs) = elabSgn (env', denv') ran
adamc@41 4358 in
adamc@1000 4359 subSgn env' loc actual ran';
adamc@83 4360 (ran', gs)
adamc@41 4361 end
adamc@41 4362 in
adamc@41 4363 ((L'.StrFun (m, n, dom', formal, str'), loc),
adamc@83 4364 (L'.SgnFun (m, n, dom', formal), loc),
adamc@228 4365 enD gs1 @ gs2 @ enD gs3)
adamc@41 4366 end
adamc@44 4367 | L.StrApp (str1, str2) =>
adamc@44 4368 let
adamc@83 4369 val (str1', sgn1, gs1) = elabStr (env, denv) str1
adamc@325 4370 val str2 =
adamc@325 4371 case sgn1 of
adamc@325 4372 (L'.SgnFun (_, _, dom, _), _) =>
adamc@1275 4373 let
adamc@1275 4374 val s = wildifyStr env (str2, dom)
adamc@1275 4375 in
adamc@1275 4376 (*Print.preface ("Wild", SourcePrint.p_str s);*)
adamc@1275 4377 s
adamc@1275 4378 end
adamc@325 4379 | _ => str2
adamc@83 4380 val (str2', sgn2, gs2) = elabStr (env, denv) str2
adamc@1270 4381 in
adamc@44 4382 case #1 (hnormSgn env sgn1) of
adamc@83 4383 L'.SgnError => (strerror, sgnerror, [])
adamc@44 4384 | L'.SgnFun (m, n, dom, ran) =>
adamc@1000 4385 (subSgn env loc sgn2 dom;
adamc@44 4386 case #1 (hnormSgn env ran) of
adamc@83 4387 L'.SgnError => (strerror, sgnerror, [])
adamc@44 4388 | L'.SgnConst sgis =>
adamc@44 4389 ((L'.StrApp (str1', str2'), loc),
adamc@83 4390 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
adamc@83 4391 gs1 @ gs2)
adamc@44 4392 | _ => raise Fail "Unable to hnormSgn in functor application")
adamc@44 4393 | _ => (strError env (NotFunctor sgn1);
adamc@83 4394 (strerror, sgnerror, []))
adamc@44 4395 end
adamc@31 4396
adamc@987 4397 fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env
adamc@833 4398
adamc@325 4399 fun elabFile basis topStr topSgn env file =
adamc@56 4400 let
adamc@713 4401 val () = mayDelay := true
adamc@713 4402 val () = delayedUnifs := []
adamc@830 4403 val () = delayedExhaustives := []
adamc@713 4404
adamc@83 4405 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
adamc@83 4406 val () = case gs of
adamc@83 4407 [] => ()
adamc@207 4408 | _ => (app (fn (_, env, _, c1, c2) =>
adamc@207 4409 prefaces "Unresolved"
adamc@207 4410 [("c1", p_con env c1),
adamc@207 4411 ("c2", p_con env c2)]) gs;
adamc@207 4412 raise Fail "Unresolved disjointness constraints in Basis")
adamc@83 4413
adamc@56 4414 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
adamc@210 4415 val () = basis_r := basis_n
adamc@56 4416
adamc@628 4417 val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn}
adamc@56 4418
adamc@56 4419 fun discoverC r x =
adamc@56 4420 case E.lookupC env' x of
adamc@56 4421 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
adamc@56 4422 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
adamc@56 4423 | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc)
adamc@56 4424
adamc@56 4425 val () = discoverC int "int"
adamc@56 4426 val () = discoverC float "float"
adamc@56 4427 val () = discoverC string "string"
adamc@821 4428 val () = discoverC char "char"
adamc@203 4429 val () = discoverC table "sql_table"
adamc@56 4430
adamc@325 4431 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan)
adamc@325 4432 val () = case gs of
adamc@325 4433 [] => ()
adamc@325 4434 | _ => raise Fail "Unresolved disjointness constraints in top.urs"
adamc@325 4435 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
adamc@325 4436 val () = case gs of
adamc@325 4437 [] => ()
adamc@329 4438 | _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
adamc@329 4439 (case D.prove env denv (c1, c2, loc) of
adamc@329 4440 [] => ()
adamc@329 4441 | _ =>
adamc@329 4442 (prefaces "Unresolved constraint in top.ur"
adamc@329 4443 [("loc", PD.string (ErrorMsg.spanToString loc)),
adamc@329 4444 ("c1", p_con env c1),
adamc@720 4445 ("c2", p_con env c2)];
adamc@478 4446 raise Fail "Unresolved constraint in top.ur"))
adamc@564 4447 | TypeClass (env, c, r, loc) =>
adamc@564 4448 let
adamc@564 4449 val c = normClassKey env c
adamc@564 4450 in
adamc@833 4451 case resolveClass env c of
adamc@564 4452 SOME e => r := SOME e
adamc@564 4453 | NONE => expError env (Unresolvable (loc, c))
adamc@634 4454 end) gs
adamc@564 4455
adamc@1000 4456 val () = subSgn env' ErrorMsg.dummySpan topSgn' topSgn
adamc@720 4457
adamc@325 4458 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
adamc@633 4459 val () = top_r := top_n
adamc@325 4460
adamc@628 4461 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
adamc@325 4462
adamc@83 4463 fun elabDecl' (d, (env, gs)) =
adamc@76 4464 let
adamc@76 4465 val () = resetKunif ()
adamc@76 4466 val () = resetCunif ()
adam@1345 4467 val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs))
adamc@76 4468 in
adam@1345 4469 (**)
adam@1345 4470 (ds, (env', gs))
adamc@76 4471 end
adamc@76 4472
adam@1345 4473 val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
adamc@753 4474
adamc@777 4475 fun oneSummaryRound () =
adamc@777 4476 if ErrorMsg.anyErrors () then
adamc@777 4477 ()
adamc@777 4478 else
adamc@777 4479 let
adamc@777 4480 val delayed = !delayedUnifs
adamc@777 4481 in
adamc@777 4482 delayedUnifs := [];
adamc@777 4483 app (fn (loc, env, k, s1, s2) =>
adamc@777 4484 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2))
adamc@777 4485 delayed
adamc@777 4486 end
adam@1576 4487
adam@1576 4488 val checkConstraintErrors = ref (fn () => ())
adamc@56 4489 in
adamc@777 4490 oneSummaryRound ();
adamc@753 4491
adamc@753 4492 if ErrorMsg.anyErrors () then
adamc@753 4493 ()
adamc@753 4494 else
adamc@753 4495 let
adamc@753 4496 fun solver gs =
adamc@753 4497 let
adamc@753 4498 val (gs, solved) =
adamc@753 4499 ListUtil.foldlMapPartial
adamc@753 4500 (fn (g, solved) =>
adamc@753 4501 case g of
adamc@753 4502 Disjoint (loc, env, denv, c1, c2) =>
adamc@753 4503 (case D.prove env denv (c1, c2, loc) of
adamc@753 4504 [] => (NONE, true)
adamc@753 4505 | _ => (SOME g, solved))
adamc@753 4506 | TypeClass (env, c, r, loc) =>
adamc@753 4507 let
adamc@753 4508 fun default () = (SOME g, solved)
adamc@753 4509
adamc@753 4510 val c = normClassKey env c
adamc@753 4511 in
adamc@833 4512 case resolveClass env c of
adamc@753 4513 SOME e => (r := SOME e;
adamc@753 4514 (NONE, true))
adamc@753 4515 | NONE =>
adamc@753 4516 case #1 (hnormCon env c) of
adamc@753 4517 L'.CApp (f, x) =>
adamc@753 4518 (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
adamc@753 4519 (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
adamc@753 4520 (case #1 (hnormCon env f) of
adamc@753 4521 L'.CModProj (top_n', [], "folder") =>
adamc@753 4522 if top_n' = top_n then
adamc@753 4523 let
adamc@753 4524 val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
adamc@753 4525 val e = (L'.EKApp (e, k), loc)
adamc@753 4526
adamc@753 4527 val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
adamc@753 4528 let
adamc@753 4529 val e = (L'.EModProj (top_n, ["Folder"],
adamc@753 4530 "cons"), loc)
adamc@753 4531 val e = (L'.EKApp (e, k), loc)
adamc@753 4532 val e = (L'.ECApp (e,
adamc@753 4533 (L'.CRecord (k, xcs),
adamc@753 4534 loc)), loc)
adamc@753 4535 val e = (L'.ECApp (e, x), loc)
adamc@753 4536 val e = (L'.ECApp (e, c), loc)
adamc@753 4537 val e = (L'.EApp (e, folder), loc)
adamc@753 4538 in
adamc@753 4539 (e, (x, c) :: xcs)
adamc@753 4540 end)
adamc@753 4541 (e, []) xcs
adamc@753 4542 in
adamc@753 4543 (r := SOME folder;
adamc@753 4544 (NONE, true))
adamc@753 4545 end
adamc@753 4546 else
adamc@753 4547 default ()
adamc@753 4548 | _ => default ())
adamc@753 4549 | _ => default ())
adamc@753 4550 | _ => default ()
adamc@753 4551 end)
adamc@753 4552 false gs
adamc@753 4553 in
adamc@753 4554 case (gs, solved) of
adamc@753 4555 ([], _) => ()
adamc@777 4556 | (_, true) => (oneSummaryRound (); solver gs)
adamc@753 4557 | _ =>
adam@1576 4558 checkConstraintErrors :=
adam@1576 4559 (fn () => app (fn Disjoint (loc, env, denv, c1, c2) =>
adam@1576 4560 let
adam@1576 4561 val c1' = ElabOps.hnormCon env c1
adam@1576 4562 val c2' = ElabOps.hnormCon env c2
adam@1576 4563
adam@1576 4564 fun isUnif (c, _) =
adam@1576 4565 case c of
adam@1576 4566 L'.CUnif _ => true
adam@1576 4567 | _ => false
adam@1576 4568
adam@1576 4569 fun maybeAttr (c, _) =
adam@1576 4570 case c of
adam@1576 4571 L'.CRecord ((L'.KType, _), xts) => true
adam@1576 4572 | _ => false
adam@1576 4573 in
adam@1576 4574 ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
adam@1576 4575 eprefaces' [("Con 1", p_con env c1),
adam@1576 4576 ("Con 2", p_con env c2),
adam@1576 4577 ("Hnormed 1", p_con env c1'),
adam@1576 4578 ("Hnormed 2", p_con env c2')]
adam@1576 4579
adam@1576 4580 (*app (fn (loc, env, k, s1, s2) =>
adam@1576 4581 eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)),
adam@1576 4582 ("s2", p_summary env (normalizeRecordSummary env s2))])
adam@1576 4583 (!delayedUnifs);*)
adam@1576 4584 end
adam@1576 4585 | TypeClass (env, c, r, loc) =>
adam@1576 4586 expError env (Unresolvable (loc, c)))
adam@1576 4587 gs)
adamc@753 4588 end
adamc@753 4589 in
adamc@753 4590 solver gs
adamc@753 4591 end;
adamc@753 4592
adamc@713 4593 mayDelay := false;
adamc@713 4594
adamc@777 4595 if ErrorMsg.anyErrors () then
adamc@777 4596 ()
adamc@777 4597 else
adamc@777 4598 (app (fn (loc, env, k, s1, s2) =>
adamc@777 4599 unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
adamc@777 4600 handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification";
adam@1582 4601 cunifyError env err;
adam@1582 4602 case !reducedSummaries of
adam@1582 4603 NONE => ()
adam@1582 4604 | SOME (s1, s2) =>
adam@1582 4605 (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:";
adam@1582 4606 eprefaces' [("Have", s1),
adam@1582 4607 ("Need", s2)])))
adamc@777 4608 (!delayedUnifs);
adamc@777 4609 delayedUnifs := []);
adamc@713 4610
adam@1346 4611 if ErrorMsg.anyErrors () then
adam@1346 4612 ()
adam@1346 4613 else
adam@1584 4614 if List.exists kunifsInDecl file then
adam@1584 4615 case U.File.findDecl kunifsInDecl file of
adam@1584 4616 NONE => ()
adam@1584 4617 | SOME d => declError env'' (KunifsRemain [d])
adam@1584 4618 else
adam@1584 4619 ();
adam@1345 4620
adam@1346 4621 if ErrorMsg.anyErrors () then
adam@1346 4622 ()
adam@1346 4623 else
adam@1584 4624 if List.exists cunifsInDecl file then
adam@1584 4625 case U.File.findDecl cunifsInDecl file of
adam@1584 4626 NONE => ()
adam@1584 4627 | SOME d => declError env'' (CunifsRemain [d])
adam@1584 4628 else
adam@1584 4629 ();
adamc@750 4630
adamc@830 4631 if ErrorMsg.anyErrors () then
adamc@830 4632 ()
adamc@830 4633 else
adamc@837 4634 app (fn all as (env, _, _, loc) =>
adamc@830 4635 case exhaustive all of
adamc@830 4636 NONE => ()
adamc@830 4637 | SOME p => expError env (Inexhaustive (loc, p)))
adamc@830 4638 (!delayedExhaustives);
adamc@830 4639
adam@1576 4640 if ErrorMsg.anyErrors () then
adam@1576 4641 ()
adam@1576 4642 else
adam@1576 4643 !checkConstraintErrors ();
adam@1576 4644
adamc@799 4645 (*preface ("file", p_file env' file);*)
adam@1531 4646
adam@1531 4647 if !dumpTypes then
adam@1531 4648 let
adam@1531 4649 open L'
adam@1531 4650 open Print.PD
adam@1531 4651 open Print
adam@1531 4652
adam@1531 4653 fun dumpDecl (d, env) =
adam@1531 4654 case #1 d of
adam@1531 4655 DCon (x, _, k, _) => (print (box [string x,
adam@1531 4656 space,
adam@1531 4657 string "::",
adam@1531 4658 space,
adam@1531 4659 p_kind env k,
adam@1531 4660 newline,
adam@1531 4661 newline]);
adam@1531 4662 E.declBinds env d)
adam@1531 4663 | DVal (x, _, t, _) => (print (box [string x,
adam@1531 4664 space,
adam@1531 4665 string ":",
adam@1531 4666 space,
adam@1531 4667 p_con env t,
adam@1531 4668 newline,
adam@1531 4669 newline]);
adam@1531 4670 E.declBinds env d)
adam@1531 4671 | DValRec vis => (app (fn (x, _, t, _) => print (box [string x,
adam@1531 4672 space,
adam@1531 4673 string ":",
adam@1531 4674 space,
adam@1531 4675 p_con env t,
adam@1531 4676 newline,
adam@1531 4677 newline])) vis;
adam@1531 4678 E.declBinds env d)
adam@1531 4679 | DStr (x, _, _, str) => (print (box [string ("<" ^ x ^ ">"),
adam@1531 4680 newline,
adam@1531 4681 newline]);
adam@1531 4682 dumpStr (str, env);
adam@1531 4683 print (box [string ("</" ^ x ^ ">"),
adam@1531 4684 newline,
adam@1531 4685 newline]);
adam@1531 4686 E.declBinds env d)
adam@1531 4687 | _ => E.declBinds env d
adam@1531 4688
adam@1531 4689 and dumpStr (str, env) =
adam@1531 4690 case #1 str of
adam@1531 4691 StrConst ds => ignore (foldl dumpDecl env ds)
adam@1531 4692 | _ => ()
adam@1531 4693 in
adam@1531 4694 ignore (foldl dumpDecl env' file)
adam@1531 4695 end
adam@1531 4696 else
adam@1531 4697 ();
adam@1345 4698
adamc@325 4699 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
adamc@325 4700 :: ds
adamc@325 4701 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
adamc@325 4702 :: ds' @ file
adamc@56 4703 end
adamc@2 4704
adamc@2 4705 end