Mercurial > urweb

annotate src/elaborate.sml @ 1588:65d6488c82d5

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