Mercurial > urweb

annotate src/elaborate.sml @ 1591:20f898c29525

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