Mercurial > urweb

annotate src/elaborate.sml @ 709:0406e9cccb72

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FOREIGN KEY, without ability to link NULL to NOT NULL (and with some lingering problems in row inference)
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Apr 2009 18:47:47 -0400
parents d8217b4cb617
children 71409a4ccb67
rev   line source
adamc@412 1 (* Copyright (c) 2008, 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
adamc@403 41 structure IM = IntBinaryMap
adamc@403 42
adamc@403 43 structure SK = struct
adamc@403 44 type ord_key = string
adamc@403 45 val compare = String.compare
adamc@403 46 end
adamc@403 47
adamc@403 48 structure SS = BinarySetFn(SK)
adamc@403 49 structure SM = BinaryMapFn(SK)
adamc@403 50
adamc@403 51 val basis_r = ref 0
adamc@633 52 val top_r = ref 0
adamc@403 53
adamc@403 54 fun elabExplicitness e =
adamc@403 55 case e of
adamc@403 56 L.Explicit => L'.Explicit
adamc@403 57 | L.Implicit => L'.Implicit
adamc@403 58
adamc@403 59 fun occursKind r =
adamc@403 60 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
adamc@403 61 | _ => false)
adamc@403 62
adamc@403 63 exception KUnify' of kunify_error
adamc@403 64
adamc@623 65 fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
adamc@403 66 let
adamc@403 67 fun err f = raise KUnify' (f (k1All, k2All))
adamc@403 68 in
adamc@403 69 case (k1, k2) of
adamc@403 70 (L'.KType, L'.KType) => ()
adamc@403 71 | (L'.KUnit, L'.KUnit) => ()
adamc@403 72
adamc@403 73 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
adamc@623 74 (unifyKinds' env d1 d2;
adamc@623 75 unifyKinds' env r1 r2)
adamc@403 76 | (L'.KName, L'.KName) => ()
adamc@623 77 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' env k1 k2
adamc@403 78 | (L'.KTuple ks1, L'.KTuple ks2) =>
adamc@623 79 ((ListPair.appEq (fn (k1, k2) => unifyKinds' env k1 k2) (ks1, ks2))
adamc@403 80 handle ListPair.UnequalLengths => err KIncompatible)
adamc@403 81
adamc@623 82 | (L'.KRel n1, L'.KRel n2) =>
adamc@623 83 if n1 = n2 then
adamc@623 84 ()
adamc@623 85 else
adamc@623 86 err KIncompatible
adamc@623 87 | (L'.KFun (x, k1), L'.KFun (_, k2)) =>
adamc@623 88 unifyKinds' (E.pushKRel env x) k1 k2
adamc@623 89
adamc@403 90 | (L'.KError, _) => ()
adamc@403 91 | (_, L'.KError) => ()
adamc@403 92
adamc@623 93 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All
adamc@623 94 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All
adamc@403 95
adamc@403 96 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
adamc@403 97 if r1 = r2 then
adamc@403 98 ()
adamc@403 99 else
adamc@403 100 r1 := SOME k2All
adamc@403 101
adamc@403 102 | (L'.KUnif (_, _, r), _) =>
adamc@403 103 if occursKind r k2All then
adamc@403 104 err KOccursCheckFailed
adamc@403 105 else
adamc@403 106 r := SOME k2All
adamc@403 107 | (_, L'.KUnif (_, _, r)) =>
adamc@403 108 if occursKind r k1All then
adamc@403 109 err KOccursCheckFailed
adamc@403 110 else
adamc@403 111 r := SOME k1All
adamc@403 112
adamc@403 113 | _ => err KIncompatible
adamc@403 114 end
adamc@403 115
adamc@403 116 exception KUnify of L'.kind * L'.kind * kunify_error
adamc@403 117
adamc@623 118 fun unifyKinds env k1 k2 =
adamc@623 119 unifyKinds' env k1 k2
adamc@403 120 handle KUnify' err => raise KUnify (k1, k2, err)
adamc@403 121
adamc@403 122 fun checkKind env c k1 k2 =
adamc@623 123 unifyKinds env k1 k2
adamc@403 124 handle KUnify (k1, k2, err) =>
adamc@403 125 conError env (WrongKind (c, k1, k2, err))
adamc@403 126
adamc@403 127 val dummy = ErrorMsg.dummySpan
adamc@403 128
adamc@403 129 val ktype = (L'.KType, dummy)
adamc@403 130 val kname = (L'.KName, dummy)
adamc@403 131 val ktype_record = (L'.KRecord ktype, dummy)
adamc@403 132
adamc@403 133 val cerror = (L'.CError, dummy)
adamc@403 134 val kerror = (L'.KError, dummy)
adamc@403 135 val eerror = (L'.EError, dummy)
adamc@403 136 val sgnerror = (L'.SgnError, dummy)
adamc@403 137 val strerror = (L'.StrError, dummy)
adamc@403 138
adamc@403 139 val int = ref cerror
adamc@403 140 val float = ref cerror
adamc@403 141 val string = ref cerror
adamc@403 142 val table = ref cerror
adamc@403 143
adamc@403 144 local
adamc@403 145 val count = ref 0
adamc@403 146 in
adamc@403 147
adamc@403 148 fun resetKunif () = count := 0
adamc@403 149
adamc@403 150 fun kunif loc =
adamc@403 151 let
adamc@403 152 val n = !count
adamc@403 153 val s = if n <= 26 then
adamc@403 154 str (chr (ord #"A" + n))
adamc@403 155 else
adamc@403 156 "U" ^ Int.toString (n - 26)
adamc@403 157 in
adamc@403 158 count := n + 1;
adamc@403 159 (L'.KUnif (loc, s, ref NONE), dummy)
adamc@403 160 end
adamc@403 161
adamc@403 162 end
adamc@403 163
adamc@403 164 local
adamc@403 165 val count = ref 0
adamc@403 166 in
adamc@403 167
adamc@403 168 fun resetCunif () = count := 0
adamc@403 169
adamc@403 170 fun cunif (loc, k) =
adamc@403 171 let
adamc@403 172 val n = !count
adamc@403 173 val s = if n <= 26 then
adamc@403 174 str (chr (ord #"A" + n))
adamc@403 175 else
adamc@403 176 "U" ^ Int.toString (n - 26)
adamc@403 177 in
adamc@403 178 count := n + 1;
adamc@403 179 (L'.CUnif (loc, k, s, ref NONE), dummy)
adamc@403 180 end
adamc@403 181
adamc@403 182 end
adamc@403 183
adamc@623 184 fun elabKind env (k, loc) =
adamc@403 185 case k of
adamc@403 186 L.KType => (L'.KType, loc)
adamc@623 187 | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc)
adamc@403 188 | L.KName => (L'.KName, loc)
adamc@623 189 | L.KRecord k => (L'.KRecord (elabKind env k), loc)
adamc@403 190 | L.KUnit => (L'.KUnit, loc)
adamc@623 191 | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc)
adamc@403 192 | L.KWild => kunif loc
adamc@403 193
adamc@623 194 | L.KVar s => (case E.lookupK env s of
adamc@623 195 NONE =>
adamc@623 196 (kindError env (UnboundKind (loc, s));
adamc@623 197 kerror)
adamc@623 198 | SOME n => (L'.KRel n, loc))
adamc@623 199 | L.KFun (x, k) => (L'.KFun (x, elabKind (E.pushKRel env x) k), loc)
adamc@623 200
adamc@621 201 fun mapKind (dom, ran, loc)=
adamc@621 202 (L'.KArrow ((L'.KArrow (dom, ran), loc),
adamc@621 203 (L'.KArrow ((L'.KRecord dom, loc),
adamc@621 204 (L'.KRecord ran, loc)), loc)), loc)
adamc@403 205
adamc@403 206 fun hnormKind (kAll as (k, _)) =
adamc@403 207 case k of
adamc@403 208 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
adamc@403 209 | _ => kAll
adamc@403 210
adamc@623 211 open ElabOps
adamc@623 212
adamc@623 213 fun elabConHead (c as (_, loc)) k =
adamc@623 214 let
adamc@623 215 fun unravel (k, c) =
adamc@623 216 case hnormKind k of
adamc@623 217 (L'.KFun (x, k'), _) =>
adamc@623 218 let
adamc@623 219 val u = kunif loc
adamc@623 220
adamc@623 221 val k'' = subKindInKind (0, u) k'
adamc@623 222 in
adamc@623 223 unravel (k'', (L'.CKApp (c, u), loc))
adamc@623 224 end
adamc@623 225 | _ => (c, k)
adamc@623 226 in
adamc@623 227 unravel (k, c)
adamc@623 228 end
adamc@623 229
adamc@403 230 fun elabCon (env, denv) (c, loc) =
adamc@403 231 case c of
adamc@403 232 L.CAnnot (c, k) =>
adamc@403 233 let
adamc@623 234 val k' = elabKind env k
adamc@403 235 val (c', ck, gs) = elabCon (env, denv) c
adamc@403 236 in
adamc@403 237 checkKind env c' ck k';
adamc@403 238 (c', k', gs)
adamc@403 239 end
adamc@403 240
adamc@403 241 | L.TFun (t1, t2) =>
adamc@403 242 let
adamc@403 243 val (t1', k1, gs1) = elabCon (env, denv) t1
adamc@403 244 val (t2', k2, gs2) = elabCon (env, denv) t2
adamc@403 245 in
adamc@403 246 checkKind env t1' k1 ktype;
adamc@403 247 checkKind env t2' k2 ktype;
adamc@403 248 ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2)
adamc@403 249 end
adamc@403 250 | L.TCFun (e, x, k, t) =>
adamc@403 251 let
adamc@403 252 val e' = elabExplicitness e
adamc@623 253 val k' = elabKind env k
adamc@403 254 val env' = E.pushCRel env x k'
adamc@403 255 val (t', tk, gs) = elabCon (env', D.enter denv) t
adamc@403 256 in
adamc@403 257 checkKind env t' tk ktype;
adamc@403 258 ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
adamc@403 259 end
adamc@623 260 | L.TKFun (x, t) =>
adamc@623 261 let
adamc@623 262 val env' = E.pushKRel env x
adamc@623 263 val (t', tk, gs) = elabCon (env', denv) t
adamc@623 264 in
adamc@623 265 checkKind env t' tk ktype;
adamc@623 266 ((L'.TKFun (x, t'), loc), ktype, gs)
adamc@623 267 end
adamc@628 268 | L.TDisjoint (c1, c2, c) =>
adamc@403 269 let
adamc@403 270 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@403 271 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@403 272
adamc@403 273 val ku1 = kunif loc
adamc@403 274 val ku2 = kunif loc
adamc@403 275
adamc@628 276 val denv' = D.assert env denv (c1', c2')
adamc@403 277 val (c', k, gs4) = elabCon (env, denv') c
adamc@403 278 in
adamc@403 279 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@403 280 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@403 281
adamc@628 282 ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs4)
adamc@403 283 end
adamc@403 284 | L.TRecord c =>
adamc@403 285 let
adamc@403 286 val (c', ck, gs) = elabCon (env, denv) c
adamc@403 287 val k = (L'.KRecord ktype, loc)
adamc@403 288 in
adamc@403 289 checkKind env c' ck k;
adamc@403 290 ((L'.TRecord c', loc), ktype, gs)
adamc@403 291 end
adamc@403 292
adamc@403 293 | L.CVar ([], s) =>
adamc@403 294 (case E.lookupC env s of
adamc@403 295 E.NotBound =>
adamc@403 296 (conError env (UnboundCon (loc, s));
adamc@403 297 (cerror, kerror, []))
adamc@403 298 | E.Rel (n, k) =>
adamc@623 299 let
adamc@623 300 val (c, k) = elabConHead (L'.CRel n, loc) k
adamc@623 301 in
adamc@623 302 (c, k, [])
adamc@623 303 end
adamc@403 304 | E.Named (n, k) =>
adamc@623 305 let
adamc@623 306 val (c, k) = elabConHead (L'.CNamed n, loc) k
adamc@623 307 in
adamc@623 308 (c, k, [])
adamc@623 309 end)
adamc@403 310 | L.CVar (m1 :: ms, s) =>
adamc@403 311 (case E.lookupStr env m1 of
adamc@403 312 NONE => (conError env (UnboundStrInCon (loc, m1));
adamc@403 313 (cerror, kerror, []))
adamc@403 314 | SOME (n, sgn) =>
adamc@403 315 let
adamc@403 316 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@403 317 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@403 318 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@403 319 (strerror, sgnerror))
adamc@403 320 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@403 321 ((L'.StrVar n, loc), sgn) ms
adamc@403 322
adamc@403 323 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
adamc@403 324 NONE => (conError env (UnboundCon (loc, s));
adamc@403 325 kerror)
adamc@403 326 | SOME (k, _) => k
adamc@403 327 in
adamc@403 328 ((L'.CModProj (n, ms, s), loc), k, [])
adamc@403 329 end)
adamc@403 330
adamc@403 331 | L.CApp (c1, c2) =>
adamc@403 332 let
adamc@403 333 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@403 334 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@403 335 val dom = kunif loc
adamc@403 336 val ran = kunif loc
adamc@403 337 in
adamc@403 338 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
adamc@403 339 checkKind env c2' k2 dom;
adamc@403 340 ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2)
adamc@403 341 end
adamc@403 342 | L.CAbs (x, ko, t) =>
adamc@403 343 let
adamc@403 344 val k' = case ko of
adamc@403 345 NONE => kunif loc
adamc@623 346 | SOME k => elabKind env k
adamc@403 347 val env' = E.pushCRel env x k'
adamc@403 348 val (t', tk, gs) = elabCon (env', D.enter denv) t
adamc@403 349 in
adamc@403 350 ((L'.CAbs (x, k', t'), loc),
adamc@403 351 (L'.KArrow (k', tk), loc),
adamc@403 352 gs)
adamc@403 353 end
adamc@623 354 | L.CKAbs (x, t) =>
adamc@623 355 let
adamc@623 356 val env' = E.pushKRel env x
adamc@623 357 val (t', tk, gs) = elabCon (env', denv) t
adamc@623 358 in
adamc@623 359 ((L'.CKAbs (x, t'), loc),
adamc@623 360 (L'.KFun (x, tk), loc),
adamc@623 361 gs)
adamc@623 362 end
adamc@403 363
adamc@403 364 | L.CName s =>
adamc@403 365 ((L'.CName s, loc), kname, [])
adamc@403 366
adamc@403 367 | L.CRecord xcs =>
adamc@403 368 let
adamc@403 369 val k = kunif loc
adamc@403 370
adamc@403 371 val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
adamc@403 372 let
adamc@403 373 val (x', xk, gs1) = elabCon (env, denv) x
adamc@403 374 val (c', ck, gs2) = elabCon (env, denv) c
adamc@403 375 in
adamc@403 376 checkKind env x' xk kname;
adamc@403 377 checkKind env c' ck k;
adamc@403 378 ((x', c'), gs1 @ gs2 @ gs)
adamc@403 379 end) [] xcs
adamc@403 380
adamc@403 381 val rc = (L'.CRecord (k, xcs'), loc)
adamc@403 382 (* Add duplicate field checking later. *)
adamc@403 383
adamc@403 384 fun prove (xcs, ds) =
adamc@403 385 case xcs of
adamc@403 386 [] => ds
adamc@403 387 | xc :: rest =>
adamc@403 388 let
adamc@403 389 val r1 = (L'.CRecord (k, [xc]), loc)
adamc@403 390 val ds = foldl (fn (xc', ds) =>
adamc@403 391 let
adamc@403 392 val r2 = (L'.CRecord (k, [xc']), loc)
adamc@403 393 in
adamc@403 394 D.prove env denv (r1, r2, loc) @ ds
adamc@403 395 end)
adamc@403 396 ds rest
adamc@403 397 in
adamc@403 398 prove (rest, ds)
adamc@403 399 end
adamc@403 400 in
adamc@403 401 (rc, (L'.KRecord k, loc), prove (xcs', gs))
adamc@403 402 end
adamc@403 403 | L.CConcat (c1, c2) =>
adamc@403 404 let
adamc@403 405 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@403 406 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@403 407 val ku = kunif loc
adamc@403 408 val k = (L'.KRecord ku, loc)
adamc@403 409 in
adamc@403 410 checkKind env c1' k1 k;
adamc@403 411 checkKind env c2' k2 k;
adamc@403 412 ((L'.CConcat (c1', c2'), loc), k,
adamc@403 413 D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
adamc@403 414 end
adamc@621 415 | L.CMap =>
adamc@403 416 let
adamc@403 417 val dom = kunif loc
adamc@403 418 val ran = kunif loc
adamc@403 419 in
adamc@621 420 ((L'.CMap (dom, ran), loc),
adamc@621 421 mapKind (dom, ran, loc),
adamc@403 422 [])
adamc@403 423 end
adamc@403 424
adamc@403 425 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
adamc@403 426
adamc@403 427 | L.CTuple cs =>
adamc@403 428 let
adamc@403 429 val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) =>
adamc@403 430 let
adamc@403 431 val (c', k, gs') = elabCon (env, denv) c
adamc@403 432 in
adamc@403 433 (c' :: cs', k :: ks, gs' @ gs)
adamc@403 434 end) ([], [], []) cs
adamc@403 435 in
adamc@403 436 ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs)
adamc@403 437 end
adamc@403 438 | L.CProj (c, n) =>
adamc@403 439 let
adamc@403 440 val (c', k, gs) = elabCon (env, denv) c
adamc@403 441 in
adamc@403 442 case hnormKind k of
adamc@403 443 (L'.KTuple ks, _) =>
adamc@403 444 if n <= 0 orelse n > length ks then
adamc@403 445 (conError env (ProjBounds (c', n));
adamc@83 446 (cerror, kerror, []))
adamc@403 447 else
adamc@403 448 ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs)
adamc@403 449 | k => (conError env (ProjMismatch (c', k));
adamc@403 450 (cerror, kerror, []))
adamc@403 451 end
adamc@403 452
adamc@403 453 | L.CWild k =>
adamc@403 454 let
adamc@623 455 val k' = elabKind env k
adamc@403 456 in
adamc@403 457 (cunif (loc, k'), k', [])
adamc@403 458 end
adamc@403 459
adamc@403 460 fun kunifsRemain k =
adamc@403 461 case k of
adamc@403 462 L'.KUnif (_, _, ref NONE) => true
adamc@403 463 | _ => false
adamc@403 464 fun cunifsRemain c =
adamc@403 465 case c of
adamc@709 466 L'.CUnif (loc, (L'.KRecord k, _), _, r as ref NONE) =>
adamc@709 467 (r := SOME (L'.CRecord (k, []), loc);
adamc@709 468 NONE)
adamc@709 469 | L'.CUnif (loc, _, _, ref NONE) => SOME loc
adamc@403 470 | _ => NONE
adamc@403 471
adamc@403 472 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
adamc@403 473 con = fn _ => false,
adamc@403 474 exp = fn _ => false,
adamc@403 475 sgn_item = fn _ => false,
adamc@403 476 sgn = fn _ => false,
adamc@403 477 str = fn _ => false,
adamc@403 478 decl = fn _ => false}
adamc@403 479
adamc@403 480 val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
adamc@403 481 con = cunifsRemain,
adamc@403 482 exp = fn _ => NONE,
adamc@403 483 sgn_item = fn _ => NONE,
adamc@403 484 sgn = fn _ => NONE,
adamc@403 485 str = fn _ => NONE,
adamc@403 486 decl = fn _ => NONE}
adamc@403 487
adamc@403 488 fun occursCon r =
adamc@403 489 U.Con.exists {kind = fn _ => false,
adamc@403 490 con = fn L'.CUnif (_, _, _, r') => r = r'
adamc@403 491 | _ => false}
adamc@403 492
adamc@403 493 exception CUnify' of cunify_error
adamc@403 494
adamc@403 495 exception SynUnif = E.SynUnif
adamc@403 496
adamc@403 497 type record_summary = {
adamc@403 498 fields : (L'.con * L'.con) list,
adamc@403 499 unifs : (L'.con * L'.con option ref) list,
adamc@403 500 others : L'.con list
adamc@403 501 }
adamc@403 502
adamc@403 503 fun summaryToCon {fields, unifs, others} =
adamc@403 504 let
adamc@403 505 val c = (L'.CRecord (ktype, []), dummy)
adamc@403 506 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
adamc@403 507 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
adamc@403 508 in
adamc@403 509 (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
adamc@403 510 end
adamc@403 511
adamc@403 512 fun p_summary env s = p_con env (summaryToCon s)
adamc@403 513
adamc@403 514 exception CUnify of L'.con * L'.con * cunify_error
adamc@403 515
adamc@403 516 fun kindof env (c, loc) =
adamc@403 517 case c of
adamc@403 518 L'.TFun _ => ktype
adamc@403 519 | L'.TCFun _ => ktype
adamc@403 520 | L'.TRecord _ => ktype
adamc@628 521 | L'.TDisjoint _ => ktype
adamc@403 522
adamc@403 523 | L'.CRel xn => #2 (E.lookupCRel env xn)
adamc@403 524 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
adamc@403 525 | L'.CModProj (n, ms, x) =>
adamc@403 526 let
adamc@403 527 val (_, sgn) = E.lookupStrNamed env n
adamc@403 528 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@403 529 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@403 530 NONE => raise Fail "kindof: Unknown substructure"
adamc@403 531 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@403 532 ((L'.StrVar n, loc), sgn) ms
adamc@403 533 in
adamc@403 534 case E.projectCon env {sgn = sgn, str = str, field = x} of
adamc@403 535 NONE => raise Fail "kindof: Unknown con in structure"
adamc@403 536 | SOME (k, _) => k
adamc@403 537 end
adamc@403 538
adamc@403 539 | L'.CApp (c, _) =>
adamc@403 540 (case hnormKind (kindof env c) of
adamc@403 541 (L'.KArrow (_, k), _) => k
adamc@403 542 | (L'.KError, _) => kerror
adamc@413 543 | k => raise CUnify' (CKindof (k, c, "arrow")))
adamc@403 544 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
adamc@628 545
adamc@403 546
adamc@403 547 | L'.CName _ => kname
adamc@403 548
adamc@403 549 | L'.CRecord (k, _) => (L'.KRecord k, loc)
adamc@403 550 | L'.CConcat (c, _) => kindof env c
adamc@621 551 | L'.CMap (dom, ran) => mapKind (dom, ran, loc)
adamc@403 552
adamc@403 553 | L'.CUnit => (L'.KUnit, loc)
adamc@403 554
adamc@403 555 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
adamc@403 556 | L'.CProj (c, n) =>
adamc@403 557 (case hnormKind (kindof env c) of
adamc@403 558 (L'.KTuple ks, _) => List.nth (ks, n - 1)
adamc@413 559 | k => raise CUnify' (CKindof (k, c, "tuple")))
adamc@403 560
adamc@403 561 | L'.CError => kerror
adamc@403 562 | L'.CUnif (_, k, _, _) => k
adamc@403 563
adamc@623 564 | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc)
adamc@623 565 | L'.CKApp (c, k) =>
adamc@623 566 (case hnormKind (kindof env c) of
adamc@623 567 (L'.KFun (_, k'), _) => subKindInKind (0, k) k'
adamc@623 568 | k => raise CUnify' (CKindof (k, c, "kapp")))
adamc@623 569 | L'.TKFun _ => ktype
adamc@403 570
adamc@621 571 exception GuessFailure
adamc@403 572
adamc@513 573 fun isUnitCon env (c, loc) =
adamc@513 574 case c of
adamc@513 575 L'.TFun _ => false
adamc@513 576 | L'.TCFun _ => false
adamc@513 577 | L'.TRecord _ => false
adamc@628 578 | L'.TDisjoint _ => false
adamc@513 579
adamc@513 580 | L'.CRel xn => #1 (#2 (E.lookupCRel env xn)) = L'.KUnit
adamc@513 581 | L'.CNamed xn => #1 (#2 (E.lookupCNamed env xn)) = L'.KUnit
adamc@518 582 | L'.CModProj (n, ms, x) => false
adamc@518 583 (*let
adamc@513 584 val (_, sgn) = E.lookupStrNamed env n
adamc@513 585 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@513 586 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@513 587 NONE => raise Fail "kindof: Unknown substructure"
adamc@513 588 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@513 589 ((L'.StrVar n, loc), sgn) ms
adamc@513 590 in
adamc@513 591 case E.projectCon env {sgn = sgn, str = str, field = x} of
adamc@513 592 NONE => raise Fail "kindof: Unknown con in structure"
adamc@513 593 | SOME ((k, _), _) => k = L'.KUnit
adamc@518 594 end*)
adamc@518 595
adamc@518 596 | L'.CApp (c, _) => false
adamc@518 597 (*(case hnormKind (kindof env c) of
adamc@513 598 (L'.KArrow (_, k), _) => #1 k = L'.KUnit
adamc@513 599 | (L'.KError, _) => false
adamc@518 600 | k => raise CUnify' (CKindof (k, c, "arrow")))*)
adamc@513 601 | L'.CAbs _ => false
adamc@513 602
adamc@513 603 | L'.CName _ => false
adamc@513 604
adamc@513 605 | L'.CRecord _ => false
adamc@513 606 | L'.CConcat _ => false
adamc@621 607 | L'.CMap _ => false
adamc@513 608
adamc@513 609 | L'.CUnit => true
adamc@513 610
adamc@513 611 | L'.CTuple _ => false
adamc@518 612 | L'.CProj (c, n) => false
adamc@518 613 (*(case hnormKind (kindof env c) of
adamc@513 614 (L'.KTuple ks, _) => #1 (List.nth (ks, n - 1)) = L'.KUnit
adamc@518 615 | k => raise CUnify' (CKindof (k, c, "tuple")))*)
adamc@513 616
adamc@513 617 | L'.CError => false
adamc@513 618 | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit
adamc@513 619
adamc@623 620 | L'.CKAbs _ => false
adamc@623 621 | L'.CKApp _ => false
adamc@623 622 | L'.TKFun _ => false
adamc@623 623
adamc@709 624 val recdCounter = ref 0
adamc@709 625
adamc@628 626 fun unifyRecordCons env (c1, c2) =
adamc@403 627 let
adamc@403 628 fun rkindof c =
adamc@403 629 case hnormKind (kindof env c) of
adamc@403 630 (L'.KRecord k, _) => k
adamc@403 631 | (L'.KError, _) => kerror
adamc@413 632 | k => raise CUnify' (CKindof (k, c, "record"))
adamc@403 633
adamc@403 634 val k1 = rkindof c1
adamc@403 635 val k2 = rkindof c2
adamc@403 636
adamc@628 637 val r1 = recordSummary env c1
adamc@628 638 val r2 = recordSummary env c2
adamc@403 639 in
adamc@623 640 unifyKinds env k1 k2;
adamc@628 641 unifySummaries env (k1, r1, r2)
adamc@403 642 end
adamc@403 643
adamc@628 644 and recordSummary env c =
adamc@403 645 let
adamc@628 646 val c = hnormCon env c
adamc@628 647
adamc@628 648 val sum =
adamc@403 649 case c of
adamc@628 650 (L'.CRecord (_, xcs), _) => {fields = xcs, unifs = [], others = []}
adamc@403 651 | (L'.CConcat (c1, c2), _) =>
adamc@403 652 let
adamc@628 653 val s1 = recordSummary env c1
adamc@628 654 val s2 = recordSummary env c2
adamc@403 655 in
adamc@628 656 {fields = #fields s1 @ #fields s2,
adamc@628 657 unifs = #unifs s1 @ #unifs s2,
adamc@628 658 others = #others s1 @ #others s2}
adamc@403 659 end
adamc@628 660 | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c
adamc@628 661 | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
adamc@628 662 | c' => {fields = [], unifs = [], others = [c']}
adamc@403 663 in
adamc@628 664 sum
adamc@403 665 end
adamc@403 666
adamc@628 667 and consEq env (c1, c2) =
adamc@628 668 (unifyCons env c1 c2;
adamc@628 669 true)
adamc@403 670 handle CUnify _ => false
adamc@403 671
adamc@403 672 and consNeq env (c1, c2) =
adamc@628 673 case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of
adamc@403 674 (L'.CName x1, L'.CName x2) => x1 <> x2
adamc@403 675 | _ => false
adamc@403 676
adamc@628 677 and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
adamc@403 678 let
adamc@403 679 val loc = #2 k
adamc@403 680 (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
adamc@403 681 ("#2", p_summary env s2)]*)
adamc@403 682
adamc@403 683 fun eatMatching p (ls1, ls2) =
adamc@403 684 let
adamc@403 685 fun em (ls1, ls2, passed1) =
adamc@403 686 case ls1 of
adamc@403 687 [] => (rev passed1, ls2)
adamc@403 688 | h1 :: t1 =>
adamc@403 689 let
adamc@403 690 fun search (ls2', passed2) =
adamc@403 691 case ls2' of
adamc@403 692 [] => em (t1, ls2, h1 :: passed1)
adamc@403 693 | h2 :: t2 =>
adamc@403 694 if p (h1, h2) then
adamc@403 695 em (t1, List.revAppend (passed2, t2), passed1)
adamc@403 696 else
adamc@403 697 search (t2, h2 :: passed2)
adamc@403 698 in
adamc@403 699 search (ls2, [])
adamc@403 700 end
adamc@403 701 in
adamc@403 702 em (ls1, ls2, [])
adamc@403 703 end
adamc@403 704
adamc@403 705 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
adamc@403 706 not (consNeq env (x1, x2))
adamc@628 707 andalso consEq env (c1, c2)
adamc@628 708 andalso consEq env (x1, x2))
adamc@403 709 (#fields s1, #fields s2)
adamc@403 710 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
adamc@403 711 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
adamc@646 712
adamc@403 713 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
adamc@646 714
adamc@628 715 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2)
adamc@403 716 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
adamc@403 717 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
adamc@403 718
adamc@709 719 fun unsummarize {fields, unifs, others} =
adamc@709 720 let
adamc@709 721 val c = (L'.CRecord (k, fields), loc)
adamc@709 722
adamc@709 723 val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
adamc@709 724 c unifs
adamc@709 725 in
adamc@709 726 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
adamc@709 727 c others
adamc@709 728 end
adamc@709 729
adamc@709 730 val (unifs1, fs1, others1, unifs2, fs2, others2) =
adamc@709 731 case (unifs1, fs1, others1, unifs2, fs2, others2) of
adamc@709 732 orig as ([(_, r)], [], [], _, _, _) =>
adamc@709 733 let
adamc@709 734 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
adamc@709 735 in
adamc@709 736 if occursCon r c then
adamc@709 737 orig
adamc@709 738 else
adamc@709 739 (r := SOME c;
adamc@709 740 ([], [], [], [], [], []))
adamc@709 741 end
adamc@709 742 | orig as (_, _, _, [(_, r)], [], []) =>
adamc@709 743 let
adamc@709 744 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
adamc@709 745 in
adamc@709 746 if occursCon r c then
adamc@709 747 orig
adamc@709 748 else
adamc@709 749 (r := SOME c;
adamc@709 750 ([], [], [], [], [], []))
adamc@709 751 end
adamc@709 752 | orig => orig
adamc@709 753
adamc@403 754 fun unifFields (fs, others, unifs) =
adamc@403 755 case (fs, others, unifs) of
adamc@403 756 ([], [], _) => ([], [], unifs)
adamc@403 757 | (_, _, []) => (fs, others, [])
adamc@403 758 | (_, _, (_, r) :: rest) =>
adamc@403 759 let
adamc@403 760 val r' = ref NONE
adamc@403 761 val kr = (L'.KRecord k, dummy)
adamc@709 762 val cr' = (L'.CUnif (dummy, kr, ("recd" ^ Int.toString (!recdCounter)), r'), dummy)
adamc@709 763 val () = recdCounter := 1 + !recdCounter
adamc@403 764
adamc@403 765 val prefix = case (fs, others) of
adamc@403 766 ([], other :: others) =>
adamc@403 767 List.foldl (fn (other, c) =>
adamc@403 768 (L'.CConcat (c, other), dummy))
adamc@403 769 other others
adamc@403 770 | (fs, []) =>
adamc@403 771 (L'.CRecord (k, fs), dummy)
adamc@403 772 | (fs, others) =>
adamc@403 773 List.foldl (fn (other, c) =>
adamc@403 774 (L'.CConcat (c, other), dummy))
adamc@403 775 (L'.CRecord (k, fs), dummy) others
adamc@403 776 in
adamc@403 777 r := SOME (L'.CConcat (prefix, cr'), dummy);
adamc@403 778 ([], [], (cr', r') :: rest)
adamc@403 779 end
adamc@403 780
adamc@403 781 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
adamc@403 782 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
adamc@403 783
adamc@403 784 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
adamc@403 785 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
adamc@403 786
adamc@403 787 fun isGuessable (other, fs) =
adamc@628 788 (guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure);
adamc@628 789 true)
adamc@621 790 handle GuessFailure => false
adamc@403 791
adamc@403 792 val (fs1, fs2, others1, others2) =
adamc@403 793 case (fs1, fs2, others1, others2) of
adamc@403 794 ([], _, [other1], []) =>
adamc@403 795 if isGuessable (other1, fs2) then
adamc@403 796 ([], [], [], [])
adamc@403 797 else
adamc@403 798 (fs1, fs2, others1, others2)
adamc@403 799 | (_, [], [], [other2]) =>
adamc@403 800 if isGuessable (other2, fs1) then
adamc@403 801 ([], [], [], [])
adamc@403 802 else
adamc@403 803 (fs1, fs2, others1, others2)
adamc@403 804 | _ => (fs1, fs2, others1, others2)
adamc@403 805
adamc@709 806 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (unifs1, unifs2)
adamc@709 807
adamc@403 808 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
adamc@646 809 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
adamc@403 810
adamc@403 811 val clear = case (fs1, others1, fs2, others2) of
adamc@403 812 ([], [], [], []) => true
adamc@403 813 | _ => false
adamc@403 814 val empty = (L'.CRecord (k, []), dummy)
adamc@403 815
adamc@709 816 fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
adamc@709 817 in
adamc@709 818 case (unifs1, fs1, others1, unifs2, fs2, others2) of
adamc@709 819 ([(_, r)], [], [], _, _, _) =>
adamc@403 820 let
adamc@709 821 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
adamc@403 822 in
adamc@709 823 if occursCon r c then
adamc@709 824 failure ()
adamc@709 825 else
adamc@709 826 r := SOME c
adamc@403 827 end
adamc@709 828 | (_, _, _, [(_, r)], [], []) =>
adamc@709 829 let
adamc@709 830 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
adamc@709 831 in
adamc@709 832 if occursCon r c then
adamc@709 833 failure ()
adamc@403 834 else
adamc@709 835 r := SOME c
adamc@709 836 end
adamc@709 837 | _ => if clear then
adamc@709 838 ()
adamc@709 839 else
adamc@709 840 failure ()
adamc@403 841 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
adamc@403 842 ("#2", p_summary env s2)]*)
adamc@403 843 end
adamc@403 844
adamc@628 845 and guessMap env (c1, c2, ex) =
adamc@403 846 let
adamc@403 847 val loc = #2 c1
adamc@403 848
adamc@621 849 fun unfold (dom, ran, f, r, c) =
adamc@403 850 let
adamc@621 851 fun unfold (r, c) =
adamc@628 852 case #1 c of
adamc@628 853 L'.CRecord (_, []) => unifyCons env r (L'.CRecord (dom, []), loc)
adamc@628 854 | L'.CRecord (_, [(x, v)]) =>
adamc@628 855 let
adamc@628 856 val v' = case dom of
adamc@628 857 (L'.KUnit, _) => (L'.CUnit, loc)
adamc@628 858 | _ => cunif (loc, dom)
adamc@628 859 in
adamc@628 860 unifyCons env v (L'.CApp (f, v'), loc);
adamc@628 861 unifyCons env r (L'.CRecord (dom, [(x, v')]), loc)
adamc@628 862 end
adamc@628 863 | L'.CRecord (_, (x, v) :: rest) =>
adamc@628 864 let
adamc@628 865 val r1 = cunif (loc, (L'.KRecord dom, loc))
adamc@628 866 val r2 = cunif (loc, (L'.KRecord dom, loc))
adamc@628 867 in
adamc@628 868 unfold (r1, (L'.CRecord (ran, [(x, v)]), loc));
adamc@628 869 unfold (r2, (L'.CRecord (ran, rest), loc));
adamc@628 870 unifyCons env r (L'.CConcat (r1, r2), loc)
adamc@628 871 end
adamc@628 872 | L'.CConcat (c1', c2') =>
adamc@628 873 let
adamc@628 874 val r1 = cunif (loc, (L'.KRecord dom, loc))
adamc@628 875 val r2 = cunif (loc, (L'.KRecord dom, loc))
adamc@628 876 in
adamc@628 877 unfold (r1, c1');
adamc@628 878 unfold (r2, c2');
adamc@628 879 unifyCons env r (L'.CConcat (r1, r2), loc)
adamc@628 880 end
adamc@628 881 | _ => raise ex
adamc@403 882 in
adamc@621 883 unfold (r, c)
adamc@403 884 end
adamc@632 885 handle _ => raise ex
adamc@403 886 in
adamc@403 887 case (#1 c1, #1 c2) of
adamc@621 888 (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) =>
adamc@621 889 unfold (dom, ran, f, r, c2)
adamc@621 890 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>
adamc@621 891 unfold (dom, ran, f, r, c1)
adamc@403 892 | _ => raise ex
adamc@403 893 end
adamc@403 894
adamc@628 895 and unifyCons' env c1 c2 =
adamc@628 896 if isUnitCon env c1 andalso isUnitCon env c2 then
adamc@628 897 ()
adamc@628 898 else
adamc@403 899 let
adamc@628 900 (*val befor = Time.now ()
adamc@628 901 val old1 = c1
adamc@628 902 val old2 = c2*)
adamc@628 903 val c1 = hnormCon env c1
adamc@628 904 val c2 = hnormCon env c2
adamc@403 905 in
adamc@628 906 unifyCons'' env c1 c2
adamc@628 907 handle ex => guessMap env (c1, c2, ex)
adamc@403 908 end
adamc@628 909
adamc@628 910 and unifyCons'' env (c1All as (c1, loc)) (c2All as (c2, _)) =
adamc@403 911 let
adamc@403 912 fun err f = raise CUnify' (f (c1All, c2All))
adamc@403 913
adamc@706 914 fun projSpecial1 (c1, n1, onFail) =
adamc@403 915 let
adamc@632 916 fun trySnd () =
adamc@632 917 case #1 (hnormCon env c2All) of
adamc@632 918 L'.CProj (c2, n2) =>
adamc@632 919 let
adamc@632 920 fun tryNormal () =
adamc@632 921 if n1 = n2 then
adamc@632 922 unifyCons' env c1 c2
adamc@632 923 else
adamc@706 924 onFail ()
adamc@632 925 in
adamc@632 926 case #1 (hnormCon env c2) of
adamc@632 927 L'.CUnif (_, k, _, r) =>
adamc@632 928 (case #1 (hnormKind k) of
adamc@632 929 L'.KTuple ks =>
adamc@632 930 let
adamc@632 931 val loc = #2 c2
adamc@632 932 val us = map (fn k => cunif (loc, k)) ks
adamc@632 933 in
adamc@632 934 r := SOME (L'.CTuple us, loc);
adamc@632 935 unifyCons' env c1All (List.nth (us, n2 - 1))
adamc@632 936 end
adamc@632 937 | _ => tryNormal ())
adamc@632 938 | _ => tryNormal ()
adamc@632 939 end
adamc@706 940 | _ => onFail ()
adamc@403 941 in
adamc@632 942 case #1 (hnormCon env c1) of
adamc@632 943 L'.CUnif (_, k, _, r) =>
adamc@632 944 (case #1 (hnormKind k) of
adamc@632 945 L'.KTuple ks =>
adamc@632 946 let
adamc@632 947 val loc = #2 c1
adamc@632 948 val us = map (fn k => cunif (loc, k)) ks
adamc@632 949 in
adamc@632 950 r := SOME (L'.CTuple us, loc);
adamc@632 951 unifyCons' env (List.nth (us, n1 - 1)) c2All
adamc@632 952 end
adamc@632 953 | _ => trySnd ())
adamc@632 954 | _ => trySnd ()
adamc@403 955 end
adamc@632 956
adamc@706 957 fun projSpecial2 (c2, n2, onFail) =
adamc@706 958 case #1 (hnormCon env c2) of
adamc@706 959 L'.CUnif (_, k, _, r) =>
adamc@706 960 (case #1 (hnormKind k) of
adamc@706 961 L'.KTuple ks =>
adamc@706 962 let
adamc@706 963 val loc = #2 c2
adamc@706 964 val us = map (fn k => cunif (loc, k)) ks
adamc@706 965 in
adamc@706 966 r := SOME (L'.CTuple us, loc);
adamc@706 967 unifyCons' env c1All (List.nth (us, n2 - 1))
adamc@706 968 end
adamc@706 969 | _ => onFail ())
adamc@706 970 | _ => onFail ()
adamc@706 971
adamc@706 972 fun isRecord' () = unifyRecordCons env (c1All, c2All)
adamc@706 973
adamc@706 974 fun isRecord () =
adamc@706 975 case (c1, c2) of
adamc@706 976 (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord')
adamc@706 977 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord')
adamc@706 978 | _ => isRecord' ()
adamc@706 979 in
adamc@706 980 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
adamc@706 981 ("c2All", p_con env c2All)];*)
adamc@706 982
adamc@706 983 case (c1, c2) of
adamc@706 984 (L'.CError, _) => ()
adamc@706 985 | (_, L'.CError) => ()
adamc@403 986
adamc@705 987 | (L'.CRecord _, _) => isRecord ()
adamc@705 988 | (_, L'.CRecord _) => isRecord ()
adamc@705 989 | (L'.CConcat _, _) => isRecord ()
adamc@705 990 | (_, L'.CConcat _) => isRecord ()
adamc@705 991
adamc@705 992 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
adamc@705 993 if r1 = r2 then
adamc@705 994 ()
adamc@705 995 else
adamc@705 996 (unifyKinds env k1 k2;
adamc@705 997 r1 := SOME c2All)
adamc@705 998
adamc@705 999 | (L'.CUnif (_, _, _, r), _) =>
adamc@705 1000 if occursCon r c2All then
adamc@705 1001 err COccursCheckFailed
adamc@705 1002 else
adamc@705 1003 r := SOME c2All
adamc@705 1004 | (_, L'.CUnif (_, _, _, r)) =>
adamc@705 1005 if occursCon r c1All then
adamc@705 1006 err COccursCheckFailed
adamc@705 1007 else
adamc@705 1008 r := SOME c1All
adamc@705 1009
adamc@705 1010 | (L'.CUnit, L'.CUnit) => ()
adamc@705 1011
adamc@705 1012 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
adamc@705 1013 (unifyCons' env d1 d2;
adamc@705 1014 unifyCons' env r1 r2)
adamc@705 1015 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
adamc@705 1016 if expl1 <> expl2 then
adamc@705 1017 err CExplicitness
adamc@705 1018 else
adamc@705 1019 (unifyKinds env d1 d2;
adamc@705 1020 let
adamc@705 1021 (*val befor = Time.now ()*)
adamc@705 1022 val env' = E.pushCRel env x1 d1
adamc@705 1023 in
adamc@705 1024 (*TextIO.print ("E.pushCRel: "
adamc@705 1025 ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))
adamc@705 1026 ^ "\n");*)
adamc@705 1027 unifyCons' env' r1 r2
adamc@705 1028 end)
adamc@705 1029 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2
adamc@705 1030 | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) =>
adamc@705 1031 (unifyCons' env c1 c2;
adamc@705 1032 unifyCons' env d1 d2;
adamc@705 1033 unifyCons' env e1 e2)
adamc@705 1034
adamc@705 1035 | (L'.CRel n1, L'.CRel n2) =>
adamc@705 1036 if n1 = n2 then
adamc@705 1037 ()
adamc@705 1038 else
adamc@705 1039 err CIncompatible
adamc@705 1040 | (L'.CNamed n1, L'.CNamed n2) =>
adamc@705 1041 if n1 = n2 then
adamc@705 1042 ()
adamc@705 1043 else
adamc@705 1044 err CIncompatible
adamc@705 1045
adamc@705 1046 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
adamc@705 1047 (unifyCons' env d1 d2;
adamc@705 1048 unifyCons' env r1 r2)
adamc@705 1049 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
adamc@705 1050 (unifyKinds env k1 k2;
adamc@705 1051 unifyCons' (E.pushCRel env x1 k1) c1 c2)
adamc@705 1052
adamc@705 1053 | (L'.CName n1, L'.CName n2) =>
adamc@705 1054 if n1 = n2 then
adamc@705 1055 ()
adamc@705 1056 else
adamc@705 1057 err CIncompatible
adamc@705 1058
adamc@705 1059 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
adamc@705 1060 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
adamc@705 1061 ()
adamc@705 1062 else
adamc@705 1063 err CIncompatible
adamc@705 1064
adamc@705 1065 | (L'.CTuple cs1, L'.CTuple cs2) =>
adamc@705 1066 ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
adamc@705 1067 handle ListPair.UnequalLengths => err CIncompatible)
adamc@705 1068
adamc@706 1069 | (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible)
adamc@706 1070 | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible)
adamc@706 1071
adamc@623 1072 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
adamc@623 1073 (unifyKinds env dom1 dom2;
adamc@628 1074 unifyKinds env ran1 ran2)
adamc@623 1075
adamc@623 1076 | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) =>
adamc@628 1077 unifyCons' (E.pushKRel env x) c1 c2
adamc@623 1078 | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) =>
adamc@623 1079 (unifyKinds env k1 k2;
adamc@628 1080 unifyCons' env c1 c2)
adamc@623 1081 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
adamc@628 1082 unifyCons' (E.pushKRel env x) c1 c2
adamc@628 1083
adamc@403 1084 | _ => err CIncompatible
adamc@403 1085 end
adamc@403 1086
adamc@628 1087 and unifyCons env c1 c2 =
adamc@628 1088 unifyCons' env c1 c2
adamc@403 1089 handle CUnify' err => raise CUnify (c1, c2, err)
adamc@403 1090 | KUnify args => raise CUnify (c1, c2, CKind args)
adamc@403 1091
adamc@628 1092 fun checkCon env e c1 c2 =
adamc@628 1093 unifyCons env c1 c2
adamc@403 1094 handle CUnify (c1, c2, err) =>
adamc@628 1095 expError env (Unify (e, c1, c2, err))
adamc@628 1096
adamc@628 1097 fun checkPatCon env p c1 c2 =
adamc@628 1098 unifyCons env c1 c2
adamc@403 1099 handle CUnify (c1, c2, err) =>
adamc@628 1100 expError env (PatUnify (p, c1, c2, err))
adamc@71 1101
adamc@403 1102 fun primType env p =
adamc@403 1103 case p of
adamc@403 1104 P.Int _ => !int
adamc@403 1105 | P.Float _ => !float
adamc@403 1106 | P.String _ => !string
adamc@623 1107
adamc@403 1108 datatype constraint =
adamc@403 1109 Disjoint of D.goal
adamc@403 1110 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
adamc@403 1111
adamc@403 1112 val enD = map Disjoint
adamc@403 1113
adamc@634 1114 fun isClassOrFolder env cl =
adamc@634 1115 E.isClass env cl
adamc@634 1116 orelse case hnormCon env cl of
adamc@634 1117 (L'.CKApp (cl, _), _) =>
adamc@634 1118 (case hnormCon env cl of
adamc@634 1119 (L'.CModProj (top_n, [], "folder"), _) => top_n = !top_r
adamc@634 1120 | _ => false)
adamc@634 1121 | _ => false
adamc@634 1122
adamc@629 1123 fun elabHead (env, denv) infer (e as (_, loc)) t =
adamc@403 1124 let
adamc@403 1125 fun unravel (t, e) =
adamc@628 1126 case hnormCon env t of
adamc@628 1127 (L'.TKFun (x, t'), _) =>
adamc@628 1128 let
adamc@628 1129 val u = kunif loc
adamc@628 1130
adamc@628 1131 val t'' = subKindInCon (0, u) t'
adamc@628 1132 in
adamc@628 1133 unravel (t'', (L'.EKApp (e, u), loc))
adamc@628 1134 end
adamc@628 1135 | (L'.TCFun (L'.Implicit, x, k, t'), _) =>
adamc@628 1136 let
adamc@628 1137 val u = cunif (loc, k)
adamc@628 1138
adamc@628 1139 val t'' = subConInCon (0, u) t'
adamc@628 1140 in
adamc@628 1141 unravel (t'', (L'.ECApp (e, u), loc))
adamc@628 1142 end
adamc@633 1143 | (L'.TFun (dom, ran), _) =>
adamc@628 1144 let
adamc@633 1145 fun default () = (e, t, [])
adamc@628 1146 in
adamc@633 1147 case #1 (hnormCon env dom) of
adamc@633 1148 L'.CApp (cl, x) =>
adamc@628 1149 let
adamc@633 1150 val cl = hnormCon env cl
adamc@628 1151 in
adamc@633 1152 if infer <> L.TypesOnly then
adamc@634 1153 if isClassOrFolder env cl then
adamc@633 1154 let
adamc@633 1155 val r = ref NONE
adamc@633 1156 val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
adamc@633 1157 in
adamc@633 1158 (e, t, TypeClass (env, dom, r, loc) :: gs)
adamc@633 1159 end
adamc@633 1160 else
adamc@634 1161 default ()
adamc@633 1162 else
adamc@633 1163 default ()
adamc@628 1164 end
adamc@633 1165 | _ => default ()
adamc@628 1166 end
adamc@629 1167 | (L'.TDisjoint (r1, r2, t'), loc) =>
adamc@629 1168 if infer <> L.TypesOnly then
adamc@629 1169 let
adamc@629 1170 val gs = D.prove env denv (r1, r2, loc)
adamc@629 1171 val (e, t, gs') = unravel (t', e)
adamc@629 1172 in
adamc@629 1173 (e, t, enD gs @ gs')
adamc@629 1174 end
adamc@629 1175 else
adamc@629 1176 (e, t, [])
adamc@628 1177 | t => (e, t, [])
adamc@704 1178 in
adamc@704 1179 case infer of
adamc@704 1180 L.DontInfer => (e, t, [])
adamc@704 1181 | _ => unravel (t, e)
adamc@704 1182 end
adamc@15 1183
adamc@628 1184 fun elabPat (pAll as (p, loc), (env, bound)) =
adamc@171 1185 let
adamc@171 1186 val perror = (L'.PWild, loc)
adamc@171 1187 val terror = (L'.CError, loc)
adamc@171 1188 val pterror = (perror, terror)
adamc@171 1189 val rerror = (pterror, (env, bound))
adamc@171 1190
adamc@191 1191 fun pcon (pc, po, xs, to, dn, dk) =
adamc@188 1192 case (po, to) of
adamc@188 1193 (NONE, SOME _) => (expError env (PatHasNoArg loc);
adamc@188 1194 rerror)
adamc@188 1195 | (SOME _, NONE) => (expError env (PatHasArg loc);
adamc@188 1196 rerror)
adamc@191 1197 | (NONE, NONE) =>
adamc@191 1198 let
adamc@191 1199 val k = (L'.KType, loc)
adamc@191 1200 val unifs = map (fn _ => cunif (loc, k)) xs
adamc@191 1201 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
adamc@191 1202 in
adamc@191 1203 (((L'.PCon (dk, pc, unifs, NONE), loc), dn),
adamc@191 1204 (env, bound))
adamc@191 1205 end
adamc@188 1206 | (SOME p, SOME t) =>
adamc@188 1207 let
adamc@628 1208 val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
adamc@191 1209
adamc@191 1210 val k = (L'.KType, loc)
adamc@191 1211 val unifs = map (fn _ => cunif (loc, k)) xs
adamc@194 1212 val nxs = length unifs - 1
adamc@194 1213 val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs
adamc@191 1214 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
adamc@188 1215 in
adamc@628 1216 ignore (checkPatCon env p' pt t);
adamc@191 1217 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
adamc@188 1218 (env, bound))
adamc@188 1219 end
adamc@171 1220 in
adamc@171 1221 case p of
adamc@171 1222 L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
adamc@171 1223 (env, bound))
adamc@171 1224 | L.PVar x =>
adamc@171 1225 let
adamc@171 1226 val t = if SS.member (bound, x) then
adamc@171 1227 (expError env (DuplicatePatternVariable (loc, x));
adamc@171 1228 terror)
adamc@171 1229 else
adamc@171 1230 cunif (loc, (L'.KType, loc))
adamc@171 1231 in
adamc@182 1232 (((L'.PVar (x, t), loc), t),
adamc@171 1233 (E.pushERel env x t, SS.add (bound, x)))
adamc@171 1234 end
adamc@173 1235 | L.PPrim p => (((L'.PPrim p, loc), primType env p),
adamc@173 1236 (env, bound))
adamc@171 1237 | L.PCon ([], x, po) =>
adamc@171 1238 (case E.lookupConstructor env x of
adamc@174 1239 NONE => (expError env (UnboundConstructor (loc, [], x));
adamc@171 1240 rerror)
adamc@191 1241 | SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk))
adamc@174 1242 | L.PCon (m1 :: ms, x, po) =>
adamc@174 1243 (case E.lookupStr env m1 of
adamc@174 1244 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@174 1245 rerror)
adamc@174 1246 | SOME (n, sgn) =>
adamc@174 1247 let
adamc@174 1248 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@174 1249 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@182 1250 NONE => raise Fail "elabPat: Unknown substructure"
adamc@174 1251 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@174 1252 ((L'.StrVar n, loc), sgn) ms
adamc@174 1253 in
adamc@174 1254 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
adamc@174 1255 NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
adamc@174 1256 rerror)
adamc@191 1257 | SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk)
adamc@174 1258 end)
adamc@174 1259
adamc@175 1260 | L.PRecord (xps, flex) =>
adamc@175 1261 let
adamc@175 1262 val (xpts, (env, bound, _)) =
adamc@175 1263 ListUtil.foldlMap (fn ((x, p), (env, bound, fbound)) =>
adamc@175 1264 let
adamc@628 1265 val ((p', t), (env, bound)) = elabPat (p, (env, bound))
adamc@175 1266 in
adamc@175 1267 if SS.member (fbound, x) then
adamc@175 1268 expError env (DuplicatePatField (loc, x))
adamc@175 1269 else
adamc@175 1270 ();
adamc@175 1271 ((x, p', t), (env, bound, SS.add (fbound, x)))
adamc@175 1272 end)
adamc@175 1273 (env, bound, SS.empty) xps
adamc@175 1274
adamc@175 1275 val k = (L'.KType, loc)
adamc@175 1276 val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc)
adamc@176 1277 val c =
adamc@175 1278 if flex then
adamc@176 1279 (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc)
adamc@175 1280 else
adamc@176 1281 c
adamc@175 1282 in
adamc@182 1283 (((L'.PRecord xpts, loc),
adamc@175 1284 (L'.TRecord c, loc)),
adamc@175 1285 (env, bound))
adamc@175 1286 end
adamc@175 1287
adamc@171 1288 end
adamc@171 1289
adamc@172 1290 datatype coverage =
adamc@172 1291 Wild
adamc@173 1292 | None
adamc@172 1293 | Datatype of coverage IM.map
adamc@175 1294 | Record of coverage SM.map list
adamc@172 1295
adamc@243 1296 fun c2s c =
adamc@243 1297 case c of
adamc@243 1298 Wild => "Wild"
adamc@243 1299 | None => "None"
adamc@243 1300 | Datatype _ => "Datatype"
adamc@243 1301 | Record _ => "Record"
adamc@243 1302
adamc@629 1303 fun exhaustive (env, t, ps, loc) =
adamc@172 1304 let
adamc@402 1305 fun depth (p, _) =
adamc@402 1306 case p of
adamc@402 1307 L'.PWild => 0
adamc@402 1308 | L'.PVar _ => 0
adamc@402 1309 | L'.PPrim _ => 0
adamc@402 1310 | L'.PCon (_, _, _, NONE) => 1
adamc@402 1311 | L'.PCon (_, _, _, SOME p) => 1 + depth p
adamc@402 1312 | L'.PRecord xps => foldl (fn ((_, p, _), n) => Int.max (depth p, n)) 0 xps
adamc@402 1313
adamc@402 1314 val depth = 1 + foldl (fn (p, n) => Int.max (depth p, n)) 0 ps
adamc@402 1315
adamc@172 1316 fun pcCoverage pc =
adamc@172 1317 case pc of
adamc@172 1318 L'.PConVar n => n
adamc@174 1319 | L'.PConProj (m1, ms, x) =>
adamc@174 1320 let
adamc@174 1321 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@174 1322 in
adamc@174 1323 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
adamc@174 1324 NONE => raise Fail "exhaustive: Can't project constructor"
adamc@191 1325 | SOME (_, n, _, _, _) => n
adamc@174 1326 end
adamc@172 1327
adamc@172 1328 fun coverage (p, _) =
adamc@172 1329 case p of
adamc@172 1330 L'.PWild => Wild
adamc@172 1331 | L'.PVar _ => Wild
adamc@173 1332 | L'.PPrim _ => None
adamc@191 1333 | L'.PCon (_, pc, _, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
adamc@191 1334 | L'.PCon (_, pc, _, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
adamc@182 1335 | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) =>
adamc@182 1336 SM.insert (fmap, x, coverage p)) SM.empty xps]
adamc@176 1337
adamc@172 1338 fun merge (c1, c2) =
adamc@172 1339 case (c1, c2) of
adamc@173 1340 (None, _) => c2
adamc@173 1341 | (_, None) => c1
adamc@173 1342
adamc@173 1343 | (Wild, _) => Wild
adamc@172 1344 | (_, Wild) => Wild
adamc@172 1345
adamc@172 1346 | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2))
adamc@172 1347
adamc@175 1348 | (Record fm1, Record fm2) => Record (fm1 @ fm2)
adamc@175 1349
adamc@175 1350 | _ => None
adamc@175 1351
adamc@172 1352 fun combinedCoverage ps =
adamc@172 1353 case ps of
adamc@172 1354 [] => raise Fail "Empty pattern list for coverage checking"
adamc@172 1355 | [p] => coverage p
adamc@172 1356 | p :: ps => merge (coverage p, combinedCoverage ps)
adamc@172 1357
adamc@402 1358 fun enumerateCases depth t =
adamc@402 1359 if depth = 0 then
adamc@402 1360 [Wild]
adamc@402 1361 else
adamc@402 1362 let
adamc@402 1363 fun dtype cons =
adamc@402 1364 ListUtil.mapConcat (fn (_, n, to) =>
adamc@402 1365 case to of
adamc@402 1366 NONE => [Datatype (IM.insert (IM.empty, n, Wild))]
adamc@402 1367 | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c)))
adamc@402 1368 (enumerateCases (depth-1) t)) cons
adamc@402 1369 in
adamc@628 1370 case #1 (hnormCon env t) of
adamc@402 1371 L'.CNamed n =>
adamc@402 1372 (let
adamc@402 1373 val dt = E.lookupDatatype env n
adamc@402 1374 val cons = E.constructors dt
adamc@175 1375 in
adamc@402 1376 dtype cons
adamc@402 1377 end handle E.UnboundNamed _ => [Wild])
adamc@402 1378 | L'.TRecord c =>
adamc@628 1379 (case #1 (hnormCon env c) of
adamc@402 1380 L'.CRecord (_, xts) =>
adamc@402 1381 let
adamc@628 1382 val xts = map (fn (x, t) => (hnormCon env x, t)) xts
adamc@402 1383
adamc@402 1384 fun exponentiate fs =
adamc@402 1385 case fs of
adamc@402 1386 [] => [SM.empty]
adamc@402 1387 | ((L'.CName x, _), t) :: rest =>
adamc@402 1388 let
adamc@402 1389 val this = enumerateCases depth t
adamc@402 1390 val rest = exponentiate rest
adamc@402 1391 in
adamc@402 1392 ListUtil.mapConcat (fn fmap =>
adamc@402 1393 map (fn c => SM.insert (fmap, x, c)) this) rest
adamc@402 1394 end
adamc@402 1395 | _ => raise Fail "exponentiate: Not CName"
adamc@402 1396 in
adamc@402 1397 if List.exists (fn ((L'.CName _, _), _) => false
adamc@402 1398 | (c, _) => true) xts then
adamc@402 1399 [Wild]
adamc@402 1400 else
adamc@402 1401 map (fn ls => Record [ls]) (exponentiate xts)
adamc@402 1402 end
adamc@402 1403 | _ => [Wild])
adamc@402 1404 | _ => [Wild]
adamc@402 1405 end
adamc@175 1406
adamc@175 1407 fun coverageImp (c1, c2) =
adamc@243 1408 let
adamc@243 1409 val r =
adamc@243 1410 case (c1, c2) of
adamc@243 1411 (Wild, _) => true
adamc@243 1412
adamc@243 1413 | (Datatype cmap1, Datatype cmap2) =>
adamc@243 1414 List.all (fn (n, c2) =>
adamc@243 1415 case IM.find (cmap1, n) of
adamc@243 1416 NONE => false
adamc@243 1417 | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2)
adamc@243 1418 | (Datatype cmap1, Wild) =>
adamc@243 1419 List.all (fn (n, c1) => coverageImp (c1, Wild)) (IM.listItemsi cmap1)
adamc@243 1420
adamc@243 1421 | (Record fmaps1, Record fmaps2) =>
adamc@243 1422 List.all (fn fmap2 =>
adamc@243 1423 List.exists (fn fmap1 =>
adamc@243 1424 List.all (fn (x, c2) =>
adamc@243 1425 case SM.find (fmap1, x) of
adamc@243 1426 NONE => true
adamc@243 1427 | SOME c1 => coverageImp (c1, c2))
adamc@243 1428 (SM.listItemsi fmap2))
adamc@243 1429 fmaps1) fmaps2
adamc@243 1430
adamc@243 1431 | (Record fmaps1, Wild) =>
adamc@243 1432 List.exists (fn fmap1 =>
adamc@243 1433 List.all (fn (x, c1) => coverageImp (c1, Wild))
adamc@243 1434 (SM.listItemsi fmap1)) fmaps1
adamc@243 1435
adamc@243 1436 | _ => false
adamc@243 1437 in
adamc@243 1438 (*TextIO.print ("coverageImp(" ^ c2s c1 ^ ", " ^ c2s c2 ^ ") = " ^ Bool.toString r ^ "\n");*)
adamc@243 1439 r
adamc@243 1440 end
adamc@175 1441
adamc@172 1442 fun isTotal (c, t) =
adamc@172 1443 case c of
adamc@628 1444 None => false
adamc@628 1445 | Wild => true
adamc@172 1446 | Datatype cm =>
adamc@172 1447 let
adamc@628 1448 val (t, _) = hnormCon env t
adamc@628 1449
adamc@628 1450 val dtype =
adamc@628 1451 List.all (fn (_, n, to) =>
adamc@628 1452 case IM.find (cm, n) of
adamc@628 1453 NONE => false
adamc@628 1454 | SOME c' =>
adamc@628 1455 case to of
adamc@628 1456 NONE => true
adamc@628 1457 | SOME t' => isTotal (c', t'))
adamc@191 1458
adamc@191 1459 fun unapp t =
adamc@191 1460 case t of
adamc@191 1461 L'.CApp ((t, _), _) => unapp t
adamc@191 1462 | _ => t
adamc@172 1463 in
adamc@191 1464 case unapp t of
adamc@172 1465 L'.CNamed n =>
adamc@172 1466 let
adamc@172 1467 val dt = E.lookupDatatype env n
adamc@172 1468 val cons = E.constructors dt
adamc@172 1469 in
adamc@174 1470 dtype cons
adamc@174 1471 end
adamc@174 1472 | L'.CModProj (m1, ms, x) =>
adamc@174 1473 let
adamc@174 1474 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@174 1475 in
adamc@174 1476 case E.projectDatatype env {str = str, sgn = sgn, field = x} of
adamc@174 1477 NONE => raise Fail "isTotal: Can't project datatype"
adamc@191 1478 | SOME (_, cons) => dtype cons
adamc@172 1479 end
adamc@628 1480 | L'.CError => true
adamc@341 1481 | c =>
adamc@629 1482 (prefaces "Not a datatype" [("loc", PD.string (ErrorMsg.spanToString loc)),
adamc@629 1483 ("c", p_con env (c, ErrorMsg.dummySpan))];
adamc@341 1484 raise Fail "isTotal: Not a datatype")
adamc@172 1485 end
adamc@628 1486 | Record _ => List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t)
adamc@172 1487 in
adamc@172 1488 isTotal (combinedCoverage ps, t)
adamc@172 1489 end
adamc@172 1490
adamc@217 1491 fun unmodCon env (c, loc) =
adamc@217 1492 case c of
adamc@217 1493 L'.CNamed n =>
adamc@217 1494 (case E.lookupCNamed env n of
adamc@217 1495 (_, _, SOME (c as (L'.CModProj _, _))) => unmodCon env c
adamc@217 1496 | _ => (c, loc))
adamc@217 1497 | L'.CModProj (m1, ms, x) =>
adamc@217 1498 let
adamc@217 1499 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@217 1500 in
adamc@217 1501 case E.projectCon env {str = str, sgn = sgn, field = x} of
adamc@217 1502 NONE => raise Fail "unmodCon: Can't projectCon"
adamc@217 1503 | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c
adamc@217 1504 | _ => (c, loc)
adamc@217 1505 end
adamc@217 1506 | _ => (c, loc)
adamc@217 1507
adamc@467 1508 fun normClassKey envs c =
adamc@467 1509 let
adamc@628 1510 val c = hnormCon envs c
adamc@467 1511 in
adamc@467 1512 case #1 c of
adamc@467 1513 L'.CApp (c1, c2) =>
adamc@467 1514 let
adamc@467 1515 val c1 = normClassKey envs c1
adamc@467 1516 val c2 = normClassKey envs c2
adamc@467 1517 in
adamc@467 1518 (L'.CApp (c1, c2), #2 c)
adamc@467 1519 end
adamc@467 1520 | _ => c
adamc@467 1521 end
adamc@467 1522
adamc@467 1523 fun normClassConstraint env (c, loc) =
adamc@217 1524 case c of
adamc@217 1525 L'.CApp (f, x) =>
adamc@217 1526 let
adamc@467 1527 val f = unmodCon env f
adamc@467 1528 val x = normClassKey env x
adamc@217 1529 in
adamc@467 1530 (L'.CApp (f, x), loc)
adamc@217 1531 end
adamc@674 1532 | L'.TFun (c1, c2) =>
adamc@674 1533 let
adamc@674 1534 val c1 = normClassConstraint env c1
adamc@674 1535 val c2 = normClassConstraint env c2
adamc@674 1536 in
adamc@674 1537 (L'.TFun (c1, c2), loc)
adamc@674 1538 end
adamc@674 1539 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc)
adamc@467 1540 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c
adamc@467 1541 | _ => (c, loc)
adamc@216 1542
adamc@92 1543 fun elabExp (env, denv) (eAll as (e, loc)) =
adamc@91 1544 let
adamc@280 1545 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
adamc@514 1546 (*val befor = Time.now ()*)
adamc@280 1547
adamc@280 1548 val r = case e of
adamc@91 1549 L.EAnnot (e, t) =>
adamc@91 1550 let
adamc@91 1551 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 1552 val (t', _, gs2) = elabCon (env, denv) t
adamc@91 1553 in
adamc@628 1554 checkCon env e' et t';
adamc@628 1555 (e', t', gs1 @ enD gs2)
adamc@91 1556 end
adamc@34 1557
adamc@91 1558 | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
adamc@403 1559 | L.EVar ([], s, infer) =>
adamc@91 1560 (case E.lookupE env s of
adamc@91 1561 E.NotBound =>
adamc@91 1562 (expError env (UnboundExp (loc, s));
adamc@91 1563 (eerror, cerror, []))
adamc@629 1564 | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t
adamc@629 1565 | E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed n, loc) t)
adamc@403 1566 | L.EVar (m1 :: ms, s, infer) =>
adamc@91 1567 (case E.lookupStr env m1 of
adamc@91 1568 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@91 1569 (eerror, cerror, []))
adamc@91 1570 | SOME (n, sgn) =>
adamc@91 1571 let
adamc@91 1572 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@91 1573 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@91 1574 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@91 1575 (strerror, sgnerror))
adamc@91 1576 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@91 1577 ((L'.StrVar n, loc), sgn) ms
adamc@10 1578
adamc@91 1579 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
adamc@91 1580 NONE => (expError env (UnboundExp (loc, s));
adamc@91 1581 cerror)
adamc@91 1582 | SOME t => t
adamc@91 1583 in
adamc@629 1584 elabHead (env, denv) infer (L'.EModProj (n, ms, s), loc) t
adamc@91 1585 end)
adamc@86 1586
adamc@349 1587 | L.EWild =>
adamc@210 1588 let
adamc@349 1589 val r = ref NONE
adamc@349 1590 val c = cunif (loc, (L'.KType, loc))
adamc@210 1591 in
adamc@349 1592 ((L'.EUnif r, loc), c, [TypeClass (env, c, r, loc)])
adamc@210 1593 end
adamc@210 1594
adamc@91 1595 | L.EApp (e1, e2) =>
adamc@91 1596 let
adamc@91 1597 val (e1', t1, gs1) = elabExp (env, denv) e1
adamc@403 1598 val (e2', t2, gs2) = elabExp (env, denv) e2
adamc@71 1599
adamc@91 1600 val dom = cunif (loc, ktype)
adamc@91 1601 val ran = cunif (loc, ktype)
adamc@91 1602 val t = (L'.TFun (dom, ran), dummy)
adamc@91 1603 in
adamc@628 1604 checkCon env e1' t1 t;
adamc@628 1605 checkCon env e2' t2 dom;
adamc@628 1606 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2)
adamc@91 1607 end
adamc@91 1608 | L.EAbs (x, to, e) =>
adamc@91 1609 let
adamc@91 1610 val (t', gs1) = case to of
adamc@91 1611 NONE => (cunif (loc, ktype), [])
adamc@91 1612 | SOME t =>
adamc@91 1613 let
adamc@91 1614 val (t', tk, gs) = elabCon (env, denv) t
adamc@91 1615 in
adamc@91 1616 checkKind env t' tk ktype;
adamc@91 1617 (t', gs)
adamc@91 1618 end
adamc@467 1619 val dom = normClassConstraint env t'
adamc@467 1620 val (e', et, gs2) = elabExp (E.pushERel env x dom, denv) e
adamc@91 1621 in
adamc@91 1622 ((L'.EAbs (x, t', et, e'), loc),
adamc@91 1623 (L'.TFun (t', et), loc),
adamc@467 1624 enD gs1 @ gs2)
adamc@91 1625 end
adamc@91 1626 | L.ECApp (e, c) =>
adamc@91 1627 let
adamc@91 1628 val (e', et, gs1) = elabExp (env, denv) e
adamc@328 1629 val oldEt = et
adamc@403 1630 val (c', ck, gs2) = elabCon (env, denv) c
adamc@628 1631 val (et', _) = hnormCon env et
adamc@91 1632 in
adamc@91 1633 case et' of
adamc@91 1634 L'.CError => (eerror, cerror, [])
adamc@328 1635 | L'.TCFun (_, x, k, eb) =>
adamc@91 1636 let
adamc@91 1637 val () = checkKind env c' ck k
adamc@91 1638 val eb' = subConInCon (0, c') eb
adamc@339 1639 handle SynUnif => (expError env (Unif ("substitution", loc, eb));
adamc@91 1640 cerror)
adamc@91 1641 in
adamc@328 1642 (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll),
adamc@328 1643 ("et", p_con env oldEt),
adamc@328 1644 ("x", PD.string x),
adamc@328 1645 ("eb", p_con (E.pushCRel env x k) eb),
adamc@328 1646 ("c", p_con env c'),
adamc@328 1647 ("eb'", p_con env eb')];*)
adamc@628 1648 ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2)
adamc@91 1649 end
adamc@91 1650
adamc@91 1651 | _ =>
adamc@91 1652 (expError env (WrongForm ("constructor function", e', et));
adamc@91 1653 (eerror, cerror, []))
adamc@91 1654 end
adamc@91 1655 | L.ECAbs (expl, x, k, e) =>
adamc@91 1656 let
adamc@91 1657 val expl' = elabExplicitness expl
adamc@623 1658 val k' = elabKind env k
adamc@328 1659
adamc@328 1660 val env' = E.pushCRel env x k'
adamc@328 1661 val (e', et, gs) = elabExp (env', D.enter denv) e
adamc@91 1662 in
adamc@91 1663 ((L'.ECAbs (expl', x, k', e'), loc),
adamc@91 1664 (L'.TCFun (expl', x, k', et), loc),
adamc@91 1665 gs)
adamc@91 1666 end
adamc@623 1667 | L.EKAbs (x, e) =>
adamc@623 1668 let
adamc@623 1669 val env' = E.pushKRel env x
adamc@623 1670 val (e', et, gs) = elabExp (env', denv) e
adamc@623 1671 in
adamc@623 1672 ((L'.EKAbs (x, e'), loc),
adamc@623 1673 (L'.TKFun (x, et), loc),
adamc@623 1674 gs)
adamc@623 1675 end
adamc@91 1676
adamc@91 1677 | L.EDisjoint (c1, c2, e) =>
adamc@91 1678 let
adamc@91 1679 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@91 1680 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@91 1681
adamc@91 1682 val ku1 = kunif loc
adamc@91 1683 val ku2 = kunif loc
adamc@91 1684
adamc@628 1685 val denv' = D.assert env denv (c1', c2')
adamc@628 1686 val (e', t, gs3) = elabExp (env, denv') e
adamc@91 1687 in
adamc@91 1688 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@91 1689 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@91 1690
adamc@628 1691 (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ gs3)
adamc@91 1692 end
adamc@629 1693 | L.EDisjointApp e =>
adamc@629 1694 let
adamc@629 1695 val (e', t, gs1) = elabExp (env, denv) e
adamc@629 1696
adamc@629 1697 val k1 = kunif loc
adamc@629 1698 val c1 = cunif (loc, (L'.KRecord k1, loc))
adamc@629 1699 val k2 = kunif loc
adamc@629 1700 val c2 = cunif (loc, (L'.KRecord k2, loc))
adamc@629 1701 val t' = cunif (loc, ktype)
adamc@629 1702 val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc)
adamc@629 1703 val gs2 = D.prove env denv (c1, c2, loc)
adamc@629 1704 in
adamc@629 1705 (e', t', enD gs2 @ gs1)
adamc@629 1706 end
adamc@91 1707
adamc@91 1708 | L.ERecord xes =>
adamc@91 1709 let
adamc@91 1710 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
adamc@91 1711 let
adamc@91 1712 val (x', xk, gs1) = elabCon (env, denv) x
adamc@91 1713 val (e', et, gs2) = elabExp (env, denv) e
adamc@91 1714 in
adamc@91 1715 checkKind env x' xk kname;
adamc@228 1716 ((x', e', et), enD gs1 @ gs2 @ gs)
adamc@91 1717 end)
adamc@91 1718 [] xes
adamc@91 1719
adamc@91 1720 val k = (L'.KType, loc)
adamc@91 1721
adamc@91 1722 fun prove (xets, gs) =
adamc@91 1723 case xets of
adamc@91 1724 [] => gs
adamc@91 1725 | (x, _, t) :: rest =>
adamc@91 1726 let
adamc@91 1727 val xc = (x, t)
adamc@91 1728 val r1 = (L'.CRecord (k, [xc]), loc)
adamc@91 1729 val gs = foldl (fn ((x', _, t'), gs) =>
adamc@91 1730 let
adamc@91 1731 val xc' = (x', t')
adamc@91 1732 val r2 = (L'.CRecord (k, [xc']), loc)
adamc@91 1733 in
adamc@91 1734 D.prove env denv (r1, r2, loc) @ gs
adamc@91 1735 end)
adamc@91 1736 gs rest
adamc@91 1737 in
adamc@91 1738 prove (rest, gs)
adamc@91 1739 end
adamc@228 1740
adamc@228 1741 val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs
adamc@228 1742 val gsO = List.filter (fn Disjoint _ => false | _ => true) gs
adamc@91 1743 in
adamc@255 1744 (*TextIO.print ("|gsO| = " ^ Int.toString (length gsO) ^ "\n");*)
adamc@91 1745 ((L'.ERecord xes', loc),
adamc@91 1746 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
adamc@228 1747 enD (prove (xes', gsD)) @ gsO)
adamc@91 1748 end
adamc@91 1749
adamc@91 1750 | L.EField (e, c) =>
adamc@91 1751 let
adamc@91 1752 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 1753 val (c', ck, gs2) = elabCon (env, denv) c
adamc@91 1754
adamc@91 1755 val ft = cunif (loc, ktype)
adamc@91 1756 val rest = cunif (loc, ktype_record)
adamc@91 1757 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
adamc@629 1758 val () = checkCon env e' et
adamc@629 1759 (L'.TRecord (L'.CConcat (first, rest), loc), loc);
adamc@628 1760 val gs3 = D.prove env denv (first, rest, loc)
adamc@91 1761 in
adamc@628 1762 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3)
adamc@91 1763 end
adamc@91 1764
adamc@445 1765 | L.EConcat (e1, e2) =>
adamc@339 1766 let
adamc@339 1767 val (e1', e1t, gs1) = elabExp (env, denv) e1
adamc@445 1768 val (e2', e2t, gs2) = elabExp (env, denv) e2
adamc@445 1769
adamc@445 1770 val r1 = cunif (loc, ktype_record)
adamc@445 1771 val r2 = cunif (loc, ktype_record)
adamc@445 1772
adamc@629 1773 val () = checkCon env e1' e1t (L'.TRecord r1, loc)
adamc@629 1774 val () = checkCon env e2' e2t (L'.TRecord r2, loc)
adamc@629 1775
adamc@628 1776 val gs3 = D.prove env denv (r1, r2, loc)
adamc@339 1777 in
adamc@445 1778 ((L'.EConcat (e1', r1, e2', r2), loc),
adamc@445 1779 (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc),
adamc@628 1780 gs1 @ gs2 @ enD gs3)
adamc@339 1781 end
adamc@149 1782 | L.ECut (e, c) =>
adamc@149 1783 let
adamc@149 1784 val (e', et, gs1) = elabExp (env, denv) e
adamc@149 1785 val (c', ck, gs2) = elabCon (env, denv) c
adamc@149 1786
adamc@149 1787 val ft = cunif (loc, ktype)
adamc@149 1788 val rest = cunif (loc, ktype_record)
adamc@149 1789 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
adamc@629 1790
adamc@629 1791 val () = checkCon env e' et
adamc@629 1792 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
adamc@149 1793
adamc@628 1794 val gs3 = D.prove env denv (first, rest, loc)
adamc@149 1795 in
adamc@228 1796 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc),
adamc@628 1797 gs1 @ enD gs2 @ enD gs3)
adamc@149 1798 end
adamc@493 1799 | L.ECutMulti (e, c) =>
adamc@493 1800 let
adamc@493 1801 val (e', et, gs1) = elabExp (env, denv) e
adamc@493 1802 val (c', ck, gs2) = elabCon (env, denv) c
adamc@493 1803
adamc@493 1804 val rest = cunif (loc, ktype_record)
adamc@629 1805
adamc@629 1806 val () = checkCon env e' et
adamc@629 1807 (L'.TRecord (L'.CConcat (c', rest), loc), loc)
adamc@493 1808
adamc@628 1809 val gs3 = D.prove env denv (c', rest, loc)
adamc@493 1810 in
adamc@493 1811 ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc),
adamc@628 1812 gs1 @ enD gs2 @ enD gs3)
adamc@493 1813 end
adamc@149 1814
adamc@171 1815 | L.ECase (e, pes) =>
adamc@171 1816 let
adamc@171 1817 val (e', et, gs1) = elabExp (env, denv) e
adamc@171 1818 val result = cunif (loc, (L'.KType, loc))
adamc@171 1819 val (pes', gs) = ListUtil.foldlMap
adamc@171 1820 (fn ((p, e), gs) =>
adamc@171 1821 let
adamc@628 1822 val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty))
adamc@628 1823
adamc@629 1824 val (e', et', gs1) = elabExp (env, denv) e
adamc@171 1825 in
adamc@628 1826 checkPatCon env p' pt et;
adamc@629 1827 checkCon env e' et' result;
adamc@628 1828 ((p', e'), gs1 @ gs)
adamc@171 1829 end)
adamc@171 1830 gs1 pes
adamc@171 1831 in
adamc@629 1832 if exhaustive (env, et, map #1 pes', loc) then
adamc@172 1833 ()
adamc@172 1834 else
adamc@172 1835 expError env (Inexhaustive loc);
adamc@172 1836
adamc@628 1837 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs)
adamc@171 1838 end
adamc@447 1839
adamc@447 1840 | L.ELet (eds, e) =>
adamc@447 1841 let
adamc@447 1842 val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds
adamc@447 1843 val (e, t, gs2) = elabExp (env, denv) e
adamc@447 1844 in
adamc@447 1845 ((L'.ELet (eds, e), loc), t, gs1 @ gs2)
adamc@447 1846 end
adamc@280 1847 in
adamc@513 1848 (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll),
adamc@514 1849 ("t", PD.string (LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))))];*)
adamc@280 1850 r
adamc@91 1851 end
adamc@31 1852
adamc@628 1853 and elabEdecl denv (dAll as (d, loc), (env, gs)) =
adamc@447 1854 let
adamc@447 1855 val r =
adamc@447 1856 case d of
adamc@447 1857 L.EDVal (x, co, e) =>
adamc@447 1858 let
adamc@447 1859 val (c', _, gs1) = case co of
adamc@447 1860 NONE => (cunif (loc, ktype), ktype, [])
adamc@447 1861 | SOME c => elabCon (env, denv) c
adamc@447 1862
adamc@447 1863 val (e', et, gs2) = elabExp (env, denv) e
adamc@628 1864
adamc@629 1865 val () = checkCon env e' et c'
adamc@629 1866
adamc@467 1867 val c' = normClassConstraint env c'
adamc@447 1868 val env' = E.pushERel env x c'
adamc@447 1869 in
adamc@628 1870 ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ gs))
adamc@447 1871 end
adamc@447 1872 | L.EDValRec vis =>
adamc@447 1873 let
adamc@447 1874 fun allowable (e, _) =
adamc@447 1875 case e of
adamc@447 1876 L.EAbs _ => true
adamc@447 1877 | L.ECAbs (_, _, _, e) => allowable e
adamc@623 1878 | L.EKAbs (_, e) => allowable e
adamc@447 1879 | L.EDisjoint (_, _, e) => allowable e
adamc@447 1880 | _ => false
adamc@447 1881
adamc@447 1882 val (vis, gs) = ListUtil.foldlMap
adamc@447 1883 (fn ((x, co, e), gs) =>
adamc@447 1884 let
adamc@447 1885 val (c', _, gs1) = case co of
adamc@447 1886 NONE => (cunif (loc, ktype), ktype, [])
adamc@447 1887 | SOME c => elabCon (env, denv) c
adamc@447 1888 in
adamc@447 1889 ((x, c', e), enD gs1 @ gs)
adamc@447 1890 end) gs vis
adamc@447 1891
adamc@447 1892 val env = foldl (fn ((x, c', _), env) => E.pushERel env x c') env vis
adamc@447 1893
adamc@447 1894 val (vis, gs) = ListUtil.foldlMap (fn ((x, c', e), gs) =>
adamc@447 1895 let
adamc@447 1896 val (e', et, gs1) = elabExp (env, denv) e
adamc@447 1897 in
adamc@628 1898 checkCon env e' et c';
adamc@447 1899 if allowable e then
adamc@447 1900 ()
adamc@447 1901 else
adamc@447 1902 expError env (IllegalRec (x, e'));
adamc@628 1903 ((x, c', e'), gs1 @ gs)
adamc@447 1904 end) gs vis
adamc@447 1905 in
adamc@447 1906 ((L'.EDValRec vis, loc), (env, gs))
adamc@447 1907 end
adamc@447 1908 in
adamc@447 1909 r
adamc@447 1910 end
adamc@447 1911
adamc@42 1912 val hnormSgn = E.hnormSgn
adamc@31 1913
adamc@210 1914 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
adamc@338 1915 fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan)
adamc@459 1916 fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan)
adamc@205 1917
adamc@469 1918 fun dopenConstraints (loc, env, denv) {str, strs} =
adamc@469 1919 case E.lookupStr env str of
adamc@469 1920 NONE => (strError env (UnboundStr (loc, str));
adamc@469 1921 denv)
adamc@469 1922 | SOME (n, sgn) =>
adamc@469 1923 let
adamc@469 1924 val (st, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@469 1925 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@469 1926 NONE => (strError env (UnboundStr (loc, m));
adamc@469 1927 (strerror, sgnerror))
adamc@469 1928 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@469 1929 ((L'.StrVar n, loc), sgn) strs
adamc@469 1930
adamc@469 1931 val cso = E.projectConstraints env {sgn = sgn, str = st}
adamc@469 1932 in
adamc@628 1933 case cso of
adamc@628 1934 NONE => (strError env (UnboundStr (loc, str));
adamc@628 1935 denv)
adamc@628 1936 | SOME cs => foldl (fn ((c1, c2), denv) =>
adamc@628 1937 D.assert env denv (c1, c2)) denv cs
adamc@469 1938 end
adamc@469 1939
adamc@88 1940 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
adamc@76 1941 case sgi of
adamc@76 1942 L.SgiConAbs (x, k) =>
adamc@76 1943 let
adamc@623 1944 val k' = elabKind env k
adamc@31 1945
adamc@76 1946 val (env', n) = E.pushCNamed env x k' NONE
adamc@76 1947 in
adamc@88 1948 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs))
adamc@76 1949 end
adamc@31 1950
adamc@76 1951 | L.SgiCon (x, ko, c) =>
adamc@76 1952 let
adamc@76 1953 val k' = case ko of
adamc@76 1954 NONE => kunif loc
adamc@623 1955 | SOME k => elabKind env k
adamc@31 1956
adamc@83 1957 val (c', ck, gs') = elabCon (env, denv) c
adamc@76 1958 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@76 1959 in
adamc@76 1960 checkKind env c' ck k';
adamc@31 1961
adamc@88 1962 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
adamc@76 1963 end
adamc@31 1964
adamc@191 1965 | L.SgiDatatype (x, xs, xcs) =>
adamc@157 1966 let
adamc@157 1967 val k = (L'.KType, loc)
adamc@191 1968 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 1969 val (env, n) = E.pushCNamed env x k' NONE
adamc@157 1970 val t = (L'.CNamed n, loc)
adamc@194 1971 val nxs = length xs - 1
adamc@194 1972 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@157 1973
adamc@284 1974 val (env', denv') = foldl (fn (x, (env', denv')) =>
adamc@284 1975 (E.pushCRel env' x k,
adamc@284 1976 D.enter denv')) (env, denv) xs
adamc@284 1977
adamc@157 1978 val (xcs, (used, env, gs)) =
adamc@157 1979 ListUtil.foldlMap
adamc@157 1980 (fn ((x, to), (used, env, gs)) =>
adamc@157 1981 let
adamc@157 1982 val (to, t, gs') = case to of
adamc@157 1983 NONE => (NONE, t, gs)
adamc@157 1984 | SOME t' =>
adamc@157 1985 let
adamc@284 1986 val (t', tk, gs') = elabCon (env', denv') t'
adamc@157 1987 in
adamc@284 1988 checkKind env' t' tk k;
adamc@157 1989 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
adamc@157 1990 end
adamc@191 1991 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
adamc@157 1992
adamc@157 1993 val (env, n') = E.pushENamed env x t
adamc@157 1994 in
adamc@157 1995 if SS.member (used, x) then
adamc@157 1996 strError env (DuplicateConstructor (x, loc))
adamc@157 1997 else
adamc@157 1998 ();
adamc@157 1999 ((x, n', to), (SS.add (used, x), env, gs'))
adamc@157 2000 end)
adamc@157 2001 (SS.empty, env, []) xcs
adamc@191 2002
adamc@191 2003 val env = E.pushDatatype env n xs xcs
adamc@157 2004 in
adamc@191 2005 ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
adamc@157 2006 end
adamc@156 2007
adamc@158 2008 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
adamc@158 2009
adamc@158 2010 | L.SgiDatatypeImp (x, m1 :: ms, s) =>
adamc@158 2011 (case E.lookupStr env m1 of
adamc@158 2012 NONE => (strError env (UnboundStr (loc, m1));
adamc@158 2013 ([], (env, denv, gs)))
adamc@158 2014 | SOME (n, sgn) =>
adamc@158 2015 let
adamc@158 2016 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@158 2017 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@158 2018 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@158 2019 (strerror, sgnerror))
adamc@158 2020 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@158 2021 ((L'.StrVar n, loc), sgn) ms
adamc@158 2022 in
adamc@628 2023 case hnormCon env (L'.CModProj (n, ms, s), loc) of
adamc@628 2024 (L'.CModProj (n, ms, s), _) =>
adamc@161 2025 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
adamc@161 2026 NONE => (conError env (UnboundDatatype (loc, s));
adamc@628 2027 ([], (env, denv, [])))
adamc@191 2028 | SOME (xs, xncs) =>
adamc@161 2029 let
adamc@161 2030 val k = (L'.KType, loc)
adamc@191 2031 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 2032
adamc@161 2033 val t = (L'.CModProj (n, ms, s), loc)
adamc@191 2034 val (env, n') = E.pushCNamed env x k' (SOME t)
adamc@191 2035 val env = E.pushDatatype env n' xs xncs
adamc@158 2036
adamc@161 2037 val t = (L'.CNamed n', loc)
adamc@161 2038 val env = foldl (fn ((x, n, to), env) =>
adamc@161 2039 let
adamc@161 2040 val t = case to of
adamc@161 2041 NONE => t
adamc@161 2042 | SOME t' => (L'.TFun (t', t), loc)
adamc@191 2043
adamc@191 2044 val t = foldr (fn (x, t) =>
adamc@191 2045 (L'.TCFun (L'.Implicit, x, k, t), loc))
adamc@191 2046 t xs
adamc@161 2047 in
adamc@161 2048 E.pushENamedAs env x n t
adamc@161 2049 end) env xncs
adamc@161 2050 in
adamc@628 2051 ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, []))
adamc@161 2052 end)
adamc@161 2053 | _ => (strError env (NotDatatype loc);
adamc@161 2054 ([], (env, denv, [])))
adamc@158 2055 end)
adamc@156 2056
adamc@76 2057 | L.SgiVal (x, c) =>
adamc@76 2058 let
adamc@83 2059 val (c', ck, gs') = elabCon (env, denv) c
adamc@31 2060
adamc@76 2061 val (env', n) = E.pushENamed env x c'
adamc@467 2062 val c' = normClassConstraint env c'
adamc@76 2063 in
adamc@623 2064 (unifyKinds env ck ktype
adamc@706 2065 handle KUnify ue => strError env (NotType (loc, ck, ue)));
adamc@31 2066
adamc@467 2067 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
adamc@76 2068 end
adamc@31 2069
adamc@707 2070 | L.SgiTable (x, c, pe, ce) =>
adamc@706 2071 let
adamc@706 2072 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
adamc@706 2073 val x' = x ^ "_hidden_constraints"
adamc@706 2074 val (env', hidden_n) = E.pushCNamed env x' cstK NONE
adamc@706 2075 val hidden = (L'.CNamed hidden_n, loc)
adamc@706 2076
adamc@706 2077 val (c', ck, gs') = elabCon (env, denv) c
adamc@707 2078 val pkey = cunif (loc, cstK)
adamc@706 2079 val visible = cunif (loc, cstK)
adamc@706 2080 val uniques = (L'.CConcat (visible, hidden), loc)
adamc@706 2081
adamc@706 2082 val ct = tableOf ()
adamc@706 2083 val ct = (L'.CApp (ct, c'), loc)
adamc@707 2084 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc)
adamc@707 2085
adamc@707 2086 val (pe', pet, gs'') = elabExp (env', denv) pe
adamc@707 2087 val gs'' = List.mapPartial (fn Disjoint x => SOME x
adamc@707 2088 | _ => NONE) gs''
adamc@707 2089
adamc@707 2090 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc)
adamc@707 2091 val pst = (L'.CApp (pst, c'), loc)
adamc@707 2092 val pst = (L'.CApp (pst, pkey), loc)
adamc@706 2093
adamc@706 2094 val (env', n) = E.pushENamed env' x ct
adamc@706 2095
adamc@707 2096 val (ce', cet, gs''') = elabExp (env', denv) ce
adamc@707 2097 val gs''' = List.mapPartial (fn Disjoint x => SOME x
adamc@707 2098 | _ => NONE) gs'''
adamc@706 2099
adamc@706 2100 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
adamc@706 2101 val cst = (L'.CApp (cst, c'), loc)
adamc@706 2102 val cst = (L'.CApp (cst, visible), loc)
adamc@706 2103 in
adamc@706 2104 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc);
adamc@707 2105 checkCon env' pe' pet pst;
adamc@707 2106 checkCon env' ce' cet cst;
adamc@706 2107
adamc@706 2108 ([(L'.SgiConAbs (x', hidden_n, cstK), loc),
adamc@707 2109 (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs))
adamc@706 2110 end
adamc@706 2111
adamc@76 2112 | L.SgiStr (x, sgn) =>
adamc@76 2113 let
adamc@83 2114 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 2115 val (env', n) = E.pushStrNamed env x sgn'
adamc@76 2116 in
adamc@88 2117 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 2118 end
adamc@31 2119
adamc@76 2120 | L.SgiSgn (x, sgn) =>
adamc@76 2121 let
adamc@83 2122 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 2123 val (env', n) = E.pushSgnNamed env x sgn'
adamc@76 2124 in
adamc@88 2125 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 2126 end
adamc@31 2127
adamc@76 2128 | L.SgiInclude sgn =>
adamc@76 2129 let
adamc@83 2130 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 2131 in
adamc@76 2132 case #1 (hnormSgn env sgn') of
adamc@76 2133 L'.SgnConst sgis =>
adamc@88 2134 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs))
adamc@76 2135 | _ => (sgnError env (NotIncludable sgn');
adamc@88 2136 ([], (env, denv, [])))
adamc@88 2137 end
adamc@88 2138
adamc@88 2139 | L.SgiConstraint (c1, c2) =>
adamc@88 2140 let
adamc@88 2141 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@88 2142 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@88 2143
adamc@628 2144 val denv = D.assert env denv (c1', c2')
adamc@88 2145 in
adamc@88 2146 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
adamc@88 2147 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
adamc@88 2148
adamc@628 2149 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2))
adamc@76 2150 end
adamc@31 2151
adamc@563 2152 | L.SgiClassAbs (x, k) =>
adamc@211 2153 let
adamc@623 2154 val k = elabKind env k
adamc@563 2155 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
adamc@563 2156 val (env, n) = E.pushCNamed env x k' NONE
adamc@211 2157 val env = E.pushClass env n
adamc@211 2158 in
adamc@563 2159 ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, []))
adamc@211 2160 end
adamc@211 2161
adamc@563 2162 | L.SgiClass (x, k, c) =>
adamc@211 2163 let
adamc@623 2164 val k = elabKind env k
adamc@563 2165 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
adamc@211 2166 val (c', ck, gs) = elabCon (env, denv) c
adamc@563 2167 val (env, n) = E.pushCNamed env x k' (SOME c')
adamc@211 2168 val env = E.pushClass env n
adamc@211 2169 in
adamc@563 2170 checkKind env c' ck k';
adamc@563 2171 ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, []))
adamc@211 2172 end
adamc@211 2173
adamc@83 2174 and elabSgn (env, denv) (sgn, loc) =
adamc@31 2175 case sgn of
adamc@31 2176 L.SgnConst sgis =>
adamc@31 2177 let
adamc@88 2178 val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis
adamc@62 2179
adamc@62 2180 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) =>
adamc@62 2181 case sgi of
adamc@62 2182 L'.SgiConAbs (x, _, _) =>
adamc@62 2183 (if SS.member (cons, x) then
adamc@62 2184 sgnError env (DuplicateCon (loc, x))
adamc@62 2185 else
adamc@62 2186 ();
adamc@62 2187 (SS.add (cons, x), vals, sgns, strs))
adamc@62 2188 | L'.SgiCon (x, _, _, _) =>
adamc@62 2189 (if SS.member (cons, x) then
adamc@62 2190 sgnError env (DuplicateCon (loc, x))
adamc@62 2191 else
adamc@62 2192 ();
adamc@62 2193 (SS.add (cons, x), vals, sgns, strs))
adamc@191 2194 | L'.SgiDatatype (x, _, _, xncs) =>
adamc@156 2195 let
adamc@156 2196 val vals = foldl (fn ((x, _, _), vals) =>
adamc@156 2197 (if SS.member (vals, x) then
adamc@156 2198 sgnError env (DuplicateVal (loc, x))
adamc@156 2199 else
adamc@156 2200 ();
adamc@156 2201 SS.add (vals, x)))
adamc@156 2202 vals xncs
adamc@156 2203 in
adamc@156 2204 if SS.member (cons, x) then
adamc@156 2205 sgnError env (DuplicateCon (loc, x))
adamc@156 2206 else
adamc@156 2207 ();
adamc@156 2208 (SS.add (cons, x), vals, sgns, strs)
adamc@156 2209 end
adamc@191 2210 | L'.SgiDatatypeImp (x, _, _, _, _, _, _) =>
adamc@156 2211 (if SS.member (cons, x) then
adamc@156 2212 sgnError env (DuplicateCon (loc, x))
adamc@156 2213 else
adamc@156 2214 ();
adamc@156 2215 (SS.add (cons, x), vals, sgns, strs))
adamc@62 2216 | L'.SgiVal (x, _, _) =>
adamc@62 2217 (if SS.member (vals, x) then
adamc@62 2218 sgnError env (DuplicateVal (loc, x))
adamc@62 2219 else
adamc@62 2220 ();
adamc@62 2221 (cons, SS.add (vals, x), sgns, strs))
adamc@62 2222 | L'.SgiSgn (x, _, _) =>
adamc@62 2223 (if SS.member (sgns, x) then
adamc@62 2224 sgnError env (DuplicateSgn (loc, x))
adamc@62 2225 else
adamc@62 2226 ();
adamc@62 2227 (cons, vals, SS.add (sgns, x), strs))
adamc@62 2228 | L'.SgiStr (x, _, _) =>
adamc@62 2229 (if SS.member (strs, x) then
adamc@62 2230 sgnError env (DuplicateStr (loc, x))
adamc@62 2231 else
adamc@62 2232 ();
adamc@88 2233 (cons, vals, sgns, SS.add (strs, x)))
adamc@203 2234 | L'.SgiConstraint _ => (cons, vals, sgns, strs)
adamc@563 2235 | L'.SgiClassAbs (x, _, _) =>
adamc@211 2236 (if SS.member (cons, x) then
adamc@211 2237 sgnError env (DuplicateCon (loc, x))
adamc@211 2238 else
adamc@211 2239 ();
adamc@211 2240 (SS.add (cons, x), vals, sgns, strs))
adamc@563 2241 | L'.SgiClass (x, _, _, _) =>
adamc@211 2242 (if SS.member (cons, x) then
adamc@211 2243 sgnError env (DuplicateCon (loc, x))
adamc@211 2244 else
adamc@211 2245 ();
adamc@460 2246 (SS.add (cons, x), vals, sgns, strs)))
adamc@62 2247 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
adamc@31 2248 in
adamc@83 2249 ((L'.SgnConst sgis', loc), gs)
adamc@31 2250 end
adamc@31 2251 | L.SgnVar x =>
adamc@31 2252 (case E.lookupSgn env x of
adamc@31 2253 NONE =>
adamc@31 2254 (sgnError env (UnboundSgn (loc, x));
adamc@83 2255 ((L'.SgnError, loc), []))
adamc@83 2256 | SOME (n, sgis) => ((L'.SgnVar n, loc), []))
adamc@41 2257 | L.SgnFun (m, dom, ran) =>
adamc@41 2258 let
adamc@83 2259 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41 2260 val (env', n) = E.pushStrNamed env m dom'
adamc@469 2261 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []}
adamc@469 2262 val (ran', gs2) = elabSgn (env', denv') ran
adamc@41 2263 in
adamc@83 2264 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
adamc@41 2265 end
adamc@42 2266 | L.SgnWhere (sgn, x, c) =>
adamc@42 2267 let
adamc@83 2268 val (sgn', ds1) = elabSgn (env, denv) sgn
adamc@83 2269 val (c', ck, ds2) = elabCon (env, denv) c
adamc@42 2270 in
adamc@42 2271 case #1 (hnormSgn env sgn') of
adamc@83 2272 L'.SgnError => (sgnerror, [])
adamc@42 2273 | L'.SgnConst sgis =>
adamc@75 2274 if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
adamc@75 2275 x' = x andalso
adamc@623 2276 (unifyKinds env k ck
adamc@75 2277 handle KUnify x => sgnError env (WhereWrongKind x);
adamc@42 2278 true)
adamc@42 2279 | _ => false) sgis then
adamc@83 2280 ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2)
adamc@42 2281 else
adamc@42 2282 (sgnError env (UnWhereable (sgn', x));
adamc@83 2283 (sgnerror, []))
adamc@42 2284 | _ => (sgnError env (UnWhereable (sgn', x));
adamc@83 2285 (sgnerror, []))
adamc@42 2286 end
adamc@59 2287 | L.SgnProj (m, ms, x) =>
adamc@59 2288 (case E.lookupStr env m of
adamc@59 2289 NONE => (strError env (UnboundStr (loc, m));
adamc@83 2290 (sgnerror, []))
adamc@59 2291 | SOME (n, sgn) =>
adamc@59 2292 let
adamc@59 2293 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@59 2294 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@59 2295 NONE => (strError env (UnboundStr (loc, m));
adamc@59 2296 (strerror, sgnerror))
adamc@59 2297 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@59 2298 ((L'.StrVar n, loc), sgn) ms
adamc@59 2299 in
adamc@59 2300 case E.projectSgn env {sgn = sgn, str = str, field = x} of
adamc@59 2301 NONE => (sgnError env (UnboundSgn (loc, x));
adamc@83 2302 (sgnerror, []))
adamc@83 2303 | SOME _ => ((L'.SgnProj (n, ms, x), loc), [])
adamc@59 2304 end)
adamc@59 2305
adamc@31 2306
adamc@706 2307 and selfify env {str, strs, sgn} =
adamc@66 2308 case #1 (hnormSgn env sgn) of
adamc@66 2309 L'.SgnError => sgn
adamc@66 2310 | L'.SgnVar _ => sgn
adamc@66 2311
adamc@66 2312 | L'.SgnConst sgis =>
adamc@66 2313 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
adamc@66 2314 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
adamc@191 2315 | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
adamc@191 2316 (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
adamc@563 2317 | (L'.SgiClassAbs (x, n, k), loc) =>
adamc@563 2318 (L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
adamc@66 2319 | (L'.SgiStr (x, n, sgn), loc) =>
adamc@66 2320 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
adamc@66 2321 | x => x) sgis), #2 sgn)
adamc@66 2322 | L'.SgnFun _ => sgn
adamc@66 2323 | L'.SgnWhere _ => sgn
adamc@66 2324 | L'.SgnProj (m, ms, x) =>
adamc@66 2325 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66 2326 (L'.StrVar m, #2 sgn) ms,
adamc@66 2327 sgn = #2 (E.lookupStrNamed env m),
adamc@66 2328 field = x} of
adamc@66 2329 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
adamc@66 2330 | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
adamc@66 2331
adamc@706 2332 and selfifyAt env {str, sgn} =
adamc@66 2333 let
adamc@66 2334 fun self (str, _) =
adamc@66 2335 case str of
adamc@66 2336 L'.StrVar x => SOME (x, [])
adamc@66 2337 | L'.StrProj (str, x) =>
adamc@66 2338 (case self str of
adamc@66 2339 NONE => NONE
adamc@66 2340 | SOME (m, ms) => SOME (m, ms @ [x]))
adamc@66 2341 | _ => NONE
adamc@66 2342 in
adamc@66 2343 case self str of
adamc@66 2344 NONE => sgn
adamc@66 2345 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
adamc@66 2346 end
adamc@66 2347
adamc@706 2348 and dopen env {str, strs, sgn} =
adamc@66 2349 let
adamc@66 2350 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66 2351 (L'.StrVar str, #2 sgn) strs
adamc@66 2352 in
adamc@66 2353 case #1 (hnormSgn env sgn) of
adamc@66 2354 L'.SgnConst sgis =>
adamc@628 2355 ListUtil.foldlMap (fn ((sgi, loc), env') =>
adamc@162 2356 let
adamc@162 2357 val d =
adamc@162 2358 case sgi of
adamc@162 2359 L'.SgiConAbs (x, n, k) =>
adamc@162 2360 let
adamc@162 2361 val c = (L'.CModProj (str, strs, x), loc)
adamc@162 2362 in
adamc@162 2363 (L'.DCon (x, n, k, c), loc)
adamc@162 2364 end
adamc@162 2365 | L'.SgiCon (x, n, k, c) =>
adamc@162 2366 (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
adamc@191 2367 | L'.SgiDatatype (x, n, xs, xncs) =>
adamc@191 2368 (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
adamc@191 2369 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@191 2370 (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)
adamc@162 2371 | L'.SgiVal (x, n, t) =>
adamc@162 2372 (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)
adamc@162 2373 | L'.SgiStr (x, n, sgn) =>
adamc@162 2374 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
adamc@162 2375 | L'.SgiSgn (x, n, sgn) =>
adamc@162 2376 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
adamc@162 2377 | L'.SgiConstraint (c1, c2) =>
adamc@162 2378 (L'.DConstraint (c1, c2), loc)
adamc@563 2379 | L'.SgiClassAbs (x, n, k) =>
adamc@211 2380 let
adamc@563 2381 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
adamc@211 2382 val c = (L'.CModProj (str, strs, x), loc)
adamc@211 2383 in
adamc@563 2384 (L'.DCon (x, n, k', c), loc)
adamc@211 2385 end
adamc@563 2386 | L'.SgiClass (x, n, k, _) =>
adamc@211 2387 let
adamc@563 2388 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
adamc@211 2389 val c = (L'.CModProj (str, strs, x), loc)
adamc@211 2390 in
adamc@563 2391 (L'.DCon (x, n, k', c), loc)
adamc@211 2392 end
adamc@162 2393 in
adamc@628 2394 (d, E.declBinds env' d)
adamc@162 2395 end)
adamc@628 2396 env sgis
adamc@66 2397 | _ => (strError env (UnOpenable sgn);
adamc@628 2398 ([], env))
adamc@66 2399 end
adamc@66 2400
adamc@706 2401 and sgiOfDecl (d, loc) =
adamc@31 2402 case d of
adamc@123 2403 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
adamc@156 2404 | L'.DDatatype x => [(L'.SgiDatatype x, loc)]
adamc@156 2405 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)]
adamc@123 2406 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
adamc@123 2407 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis
adamc@123 2408 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
adamc@123 2409 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
adamc@123 2410 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
adamc@123 2411 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
adamc@123 2412 | L'.DExport _ => []
adamc@707 2413 | L'.DTable (tn, x, n, c, _, pc, _, cc) =>
adamc@707 2414 [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc),
adamc@707 2415 (L'.CConcat (pc, cc), loc)), loc)), loc)]
adamc@460 2416 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
adamc@563 2417 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
adamc@271 2418 | L'.DDatabase _ => []
adamc@460 2419 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
adamc@88 2420
adamc@706 2421 and subSgn env sgn1 (sgn2 as (_, loc2)) =
adamc@469 2422 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
adamc@469 2423 ("sgn2", p_sgn env sgn2)];*)
adamc@35 2424 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
adamc@31 2425 (L'.SgnError, _) => ()
adamc@31 2426 | (_, L'.SgnError) => ()
adamc@31 2427
adamc@31 2428 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
adamc@31 2429 let
adamc@362 2430 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
adamc@362 2431 ("sgn2", p_sgn env sgn2),
adamc@362 2432 ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)),
adamc@362 2433 ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*)
adamc@362 2434
adamc@628 2435 fun folder (sgi2All as (sgi, loc), env) =
adamc@31 2436 let
adamc@362 2437 (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*)
adamc@362 2438
adamc@31 2439 fun seek p =
adamc@31 2440 let
adamc@628 2441 fun seek env ls =
adamc@31 2442 case ls of
adamc@31 2443 [] => (sgnError env (UnmatchedSgi sgi2All);
adamc@628 2444 env)
adamc@31 2445 | h :: t =>
adamc@469 2446 case p (env, h) of
adamc@469 2447 NONE =>
adamc@469 2448 let
adamc@469 2449 val env = case #1 h of
adamc@469 2450 L'.SgiCon (x, n, k, c) =>
adamc@471 2451 if E.checkENamed env n then
adamc@471 2452 env
adamc@471 2453 else
adamc@471 2454 E.pushCNamedAs env x n k (SOME c)
adamc@469 2455 | L'.SgiConAbs (x, n, k) =>
adamc@471 2456 if E.checkENamed env n then
adamc@471 2457 env
adamc@471 2458 else
adamc@471 2459 E.pushCNamedAs env x n k NONE
adamc@469 2460 | _ => env
adamc@469 2461 in
adamc@628 2462 seek (E.sgiBinds env h) t
adamc@469 2463 end
adamc@88 2464 | SOME envs => envs
adamc@31 2465 in
adamc@628 2466 seek env sgis1
adamc@31 2467 end
adamc@31 2468 in
adamc@31 2469 case sgi of
adamc@31 2470 L'.SgiConAbs (x, n2, k2) =>
adamc@469 2471 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@31 2472 let
adamc@41 2473 fun found (x', n1, k1, co1) =
adamc@41 2474 if x = x' then
adamc@41 2475 let
adamc@623 2476 val () = unifyKinds env k1 k2
adamc@41 2477 handle KUnify (k1, k2, err) =>
adamc@41 2478 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
adamc@41 2479 val env = E.pushCNamedAs env x n1 k1 co1
adamc@41 2480 in
adamc@41 2481 SOME (if n1 = n2 then
adamc@41 2482 env
adamc@41 2483 else
adamc@628 2484 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)))
adamc@41 2485 end
adamc@41 2486 else
adamc@41 2487 NONE
adamc@31 2488 in
adamc@31 2489 case sgi1 of
adamc@41 2490 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
adamc@41 2491 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
adamc@191 2492 | L'.SgiDatatype (x', n1, xs, _) =>
adamc@191 2493 let
adamc@191 2494 val k = (L'.KType, loc)
adamc@191 2495 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 2496 in
adamc@191 2497 found (x', n1, k', NONE)
adamc@191 2498 end
adamc@191 2499 | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) =>
adamc@191 2500 let
adamc@191 2501 val k = (L'.KType, loc)
adamc@191 2502 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 2503 in
adamc@191 2504 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
adamc@191 2505 end
adamc@563 2506 | L'.SgiClassAbs (x', n1, k) => found (x', n1,
adamc@563 2507 (L'.KArrow (k,
adamc@563 2508 (L'.KType, loc)), loc),
adamc@563 2509 NONE)
adamc@563 2510 | L'.SgiClass (x', n1, k, c) => found (x', n1,
adamc@563 2511 (L'.KArrow (k,
adamc@563 2512 (L'.KType, loc)), loc),
adamc@563 2513 SOME c)
adamc@31 2514 | _ => NONE
adamc@31 2515 end)
adamc@31 2516
adamc@31 2517 | L'.SgiCon (x, n2, k2, c2) =>
adamc@469 2518 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@211 2519 let
adamc@211 2520 fun found (x', n1, k1, c1) =
adamc@211 2521 if x = x' then
adamc@211 2522 let
adamc@327 2523 fun good () =
adamc@327 2524 let
adamc@327 2525 val env = E.pushCNamedAs env x n2 k2 (SOME c2)
adamc@327 2526 val env = if n1 = n2 then
adamc@327 2527 env
adamc@327 2528 else
adamc@327 2529 E.pushCNamedAs env x n1 k1 (SOME c1)
adamc@327 2530 in
adamc@628 2531 SOME env
adamc@327 2532 end
adamc@211 2533 in
adamc@628 2534 (unifyCons env c1 c2;
adamc@628 2535 good ())
adamc@211 2536 handle CUnify (c1, c2, err) =>
adamc@211 2537 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@211 2538 good ())
adamc@211 2539 end
adamc@211 2540 else
adamc@211 2541 NONE
adamc@211 2542 in
adamc@211 2543 case sgi1 of
adamc@211 2544 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
adamc@563 2545 | L'.SgiClass (x', n1, k1, c1) =>
adamc@563 2546 found (x', n1, (L'.KArrow (k1, (L'.KType, loc)), loc), c1)
adamc@211 2547 | _ => NONE
adamc@211 2548 end)
adamc@31 2549
adamc@191 2550 | L'.SgiDatatype (x, n2, xs2, xncs2) =>
adamc@469 2551 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@160 2552 let
adamc@191 2553 fun found (n1, xs1, xncs1) =
adamc@160 2554 let
adamc@160 2555 fun mismatched ue =
adamc@160 2556 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
adamc@628 2557 SOME env)
adamc@156 2558
adamc@191 2559 val k = (L'.KType, loc)
adamc@191 2560 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
adamc@191 2561
adamc@160 2562 fun good () =
adamc@160 2563 let
adamc@471 2564 val env = E.sgiBinds env sgi1All
adamc@160 2565 val env = if n1 = n2 then
adamc@160 2566 env
adamc@160 2567 else
adamc@471 2568 E.pushCNamedAs env x n2 k'
adamc@471 2569 (SOME (L'.CNamed n1, loc))
adamc@160 2570 in
adamc@628 2571 SOME env
adamc@160 2572 end
adamc@156 2573
adamc@397 2574 val env = E.pushCNamedAs env x n1 k' NONE
adamc@397 2575 val env = if n1 = n2 then
adamc@397 2576 env
adamc@397 2577 else
adamc@397 2578 E.pushCNamedAs env x n2 k' (SOME (L'.CNamed n1, loc))
adamc@191 2579 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
adamc@160 2580 fun xncBad ((x1, _, t1), (x2, _, t2)) =
adamc@160 2581 String.compare (x1, x2) <> EQUAL
adamc@160 2582 orelse case (t1, t2) of
adamc@160 2583 (NONE, NONE) => false
adamc@160 2584 | (SOME t1, SOME t2) =>
adamc@628 2585 (unifyCons env t1 t2; false)
adamc@160 2586 | _ => true
adamc@160 2587 in
adamc@191 2588 (if xs1 <> xs2
adamc@191 2589 orelse length xncs1 <> length xncs2
adamc@160 2590 orelse ListPair.exists xncBad (xncs1, xncs2) then
adamc@160 2591 mismatched NONE
adamc@160 2592 else
adamc@160 2593 good ())
adamc@160 2594 handle CUnify ue => mismatched (SOME ue)
adamc@160 2595 end
adamc@160 2596 in
adamc@160 2597 case sgi1 of
adamc@191 2598 L'.SgiDatatype (x', n1, xs, xncs1) =>
adamc@160 2599 if x' = x then
adamc@191 2600 found (n1, xs, xncs1)
adamc@160 2601 else
adamc@160 2602 NONE
adamc@191 2603 | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
adamc@162 2604 if x' = x then
adamc@191 2605 found (n1, xs, xncs1)
adamc@162 2606 else
adamc@162 2607 NONE
adamc@160 2608 | _ => NONE
adamc@160 2609 end)
adamc@156 2610
adamc@191 2611 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
adamc@469 2612 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@158 2613 case sgi1 of
adamc@191 2614 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) =>
adamc@158 2615 if x = x' then
adamc@158 2616 let
adamc@158 2617 val k = (L'.KType, loc)
adamc@191 2618 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@158 2619 val t1 = (L'.CModProj (m11, ms1, s1), loc)
adamc@158 2620 val t2 = (L'.CModProj (m12, ms2, s2), loc)
adamc@158 2621
adamc@158 2622 fun good () =
adamc@158 2623 let
adamc@191 2624 val env = E.pushCNamedAs env x n1 k' (SOME t1)
adamc@191 2625 val env = E.pushCNamedAs env x n2 k' (SOME t2)
adamc@158 2626 in
adamc@628 2627 SOME env
adamc@158 2628 end
adamc@158 2629 in
adamc@628 2630 (unifyCons env t1 t2;
adamc@628 2631 good ())
adamc@158 2632 handle CUnify (c1, c2, err) =>
adamc@158 2633 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@158 2634 good ())
adamc@158 2635 end
adamc@158 2636 else
adamc@158 2637 NONE
adamc@158 2638
adamc@158 2639 | _ => NONE)
adamc@156 2640
adamc@32 2641 | L'.SgiVal (x, n2, c2) =>
adamc@469 2642 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@32 2643 case sgi1 of
adamc@41 2644 L'.SgiVal (x', n1, c1) =>
adamc@41 2645 if x = x' then
adamc@628 2646 (unifyCons env c1 c2;
adamc@628 2647 SOME env)
adamc@86 2648 handle CUnify (c1, c2, err) =>
adamc@86 2649 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@628 2650 SOME env)
adamc@41 2651 else
adamc@41 2652 NONE
adamc@32 2653 | _ => NONE)
adamc@32 2654
adamc@33 2655 | L'.SgiStr (x, n2, sgn2) =>
adamc@469 2656 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@33 2657 case sgi1 of
adamc@41 2658 L'.SgiStr (x', n1, sgn1) =>
adamc@41 2659 if x = x' then
adamc@66 2660 let
adamc@628 2661 val () = subSgn env sgn1 sgn2
adamc@66 2662 val env = E.pushStrNamedAs env x n1 sgn1
adamc@66 2663 val env = if n1 = n2 then
adamc@66 2664 env
adamc@66 2665 else
adamc@66 2666 E.pushStrNamedAs env x n2
adamc@66 2667 (selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
adamc@66 2668 sgn = sgn2})
adamc@66 2669 in
adamc@628 2670 SOME env
adamc@66 2671 end
adamc@41 2672 else
adamc@41 2673 NONE
adamc@33 2674 | _ => NONE)
adamc@59 2675
adamc@59 2676 | L'.SgiSgn (x, n2, sgn2) =>
adamc@469 2677 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@59 2678 case sgi1 of
adamc@59 2679 L'.SgiSgn (x', n1, sgn1) =>
adamc@59 2680 if x = x' then
adamc@65 2681 let
adamc@628 2682 val () = subSgn env sgn1 sgn2
adamc@628 2683 val () = subSgn env sgn2 sgn1
adamc@65 2684
adamc@65 2685 val env = E.pushSgnNamedAs env x n2 sgn2
adamc@65 2686 val env = if n1 = n2 then
adamc@65 2687 env
adamc@65 2688 else
adamc@65 2689 E.pushSgnNamedAs env x n1 sgn2
adamc@65 2690 in
adamc@628 2691 SOME env
adamc@65 2692 end
adamc@59 2693 else
adamc@59 2694 NONE
adamc@59 2695 | _ => NONE)
adamc@88 2696
adamc@88 2697 | L'.SgiConstraint (c2, d2) =>
adamc@469 2698 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@88 2699 case sgi1 of
adamc@88 2700 L'.SgiConstraint (c1, d1) =>
adamc@628 2701 if consEq env (c1, c2) andalso consEq env (d1, d2) then
adamc@628 2702 SOME env
adamc@88 2703 else
adamc@88 2704 NONE
adamc@88 2705 | _ => NONE)
adamc@203 2706
adamc@563 2707 | L'.SgiClassAbs (x, n2, k2) =>
adamc@469 2708 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@211 2709 let
adamc@563 2710 fun found (x', n1, k1, co) =
adamc@211 2711 if x = x' then
adamc@211 2712 let
adamc@623 2713 val () = unifyKinds env k1 k2
adamc@563 2714 handle KUnify (k1, k2, err) =>
adamc@563 2715 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
adamc@563 2716
adamc@563 2717 val k = (L'.KArrow (k1, (L'.KType, loc)), loc)
adamc@211 2718 val env = E.pushCNamedAs env x n1 k co
adamc@211 2719 in
adamc@211 2720 SOME (if n1 = n2 then
adamc@211 2721 env
adamc@211 2722 else
adamc@628 2723 E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)))
adamc@211 2724 end
adamc@211 2725 else
adamc@211 2726 NONE
adamc@211 2727 in
adamc@211 2728 case sgi1 of
adamc@563 2729 L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE)
adamc@563 2730 | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c)
adamc@211 2731 | _ => NONE
adamc@211 2732 end)
adamc@563 2733 | L'.SgiClass (x, n2, k2, c2) =>
adamc@469 2734 seek (fn (env, sgi1All as (sgi1, _)) =>
adamc@211 2735 let
adamc@563 2736 val k = (L'.KArrow (k2, (L'.KType, loc)), loc)
adamc@563 2737
adamc@563 2738 fun found (x', n1, k1, c1) =
adamc@211 2739 if x = x' then
adamc@211 2740 let
adamc@623 2741 val () = unifyKinds env k1 k2
adamc@563 2742 handle KUnify (k1, k2, err) =>
adamc@563 2743 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
adamc@563 2744
adamc@218 2745 fun good () =
adamc@218 2746 let
adamc@218 2747 val env = E.pushCNamedAs env x n2 k (SOME c2)
adamc@218 2748 val env = if n1 = n2 then
adamc@218 2749 env
adamc@218 2750 else
adamc@218 2751 E.pushCNamedAs env x n1 k (SOME c1)
adamc@218 2752 in
adamc@628 2753 SOME env
adamc@218 2754 end
adamc@211 2755 in
adamc@628 2756 (unifyCons env c1 c2;
adamc@628 2757 good ())
adamc@211 2758 handle CUnify (c1, c2, err) =>
adamc@211 2759 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@211 2760 good ())
adamc@211 2761 end
adamc@211 2762 else
adamc@211 2763 NONE
adamc@211 2764 in
adamc@211 2765 case sgi1 of
adamc@563 2766 L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
adamc@211 2767 | _ => NONE
adamc@211 2768 end)
adamc@31 2769 end
adamc@31 2770 in
adamc@628 2771 ignore (foldl folder env sgis2)
adamc@31 2772 end
adamc@31 2773
adamc@41 2774 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
adamc@43 2775 let
adamc@480 2776 val ran2 =
adamc@43 2777 if n1 = n2 then
adamc@480 2778 ran2
adamc@43 2779 else
adamc@480 2780 subStrInSgn (n2, n1) ran2
adamc@43 2781 in
adamc@628 2782 subSgn env dom2 dom1;
adamc@628 2783 subSgn (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2
adamc@43 2784 end
adamc@41 2785
adamc@469 2786 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
adamc@41 2787
adamc@61 2788
adamc@706 2789 and positive self =
adamc@312 2790 let
adamc@312 2791 open L
adamc@312 2792
adamc@312 2793 fun none (c, _) =
adamc@312 2794 case c of
adamc@312 2795 CAnnot (c, _) => none c
adamc@312 2796
adamc@312 2797 | TFun (c1, c2) => none c1 andalso none c2
adamc@312 2798 | TCFun (_, _, _, c) => none c
adamc@312 2799 | TRecord c => none c
adamc@312 2800
adamc@312 2801 | CVar ([], x) => x <> self
adamc@312 2802 | CVar _ => true
adamc@312 2803 | CApp (c1, c2) => none c1 andalso none c2
adamc@312 2804 | CAbs _ => false
adamc@628 2805 | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
adamc@312 2806
adamc@623 2807 | CKAbs _ => false
adamc@623 2808 | TKFun _ => false
adamc@623 2809
adamc@312 2810 | CName _ => true
adamc@312 2811
adamc@312 2812 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
adamc@312 2813 | CConcat (c1, c2) => none c1 andalso none c2
adamc@621 2814 | CMap => true
adamc@312 2815
adamc@312 2816 | CUnit => true
adamc@312 2817
adamc@312 2818 | CTuple cs => List.all none cs
adamc@312 2819 | CProj (c, _) => none c
adamc@312 2820
adamc@312 2821 | CWild _ => false
adamc@312 2822
adamc@312 2823 fun pos (c, _) =
adamc@312 2824 case c of
adamc@312 2825 CAnnot (c, _) => pos c
adamc@312 2826
adamc@312 2827 | TFun (c1, c2) => none c1 andalso pos c2
adamc@312 2828 | TCFun (_, _, _, c) => pos c
adamc@312 2829 | TRecord c => pos c
adamc@312 2830
adamc@312 2831 | CVar _ => true
adamc@312 2832 | CApp (c1, c2) => pos c1 andalso none c2
adamc@312 2833 | CAbs _ => false
adamc@628 2834 | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
adamc@312 2835
adamc@623 2836 | CKAbs _ => false
adamc@623 2837 | TKFun _ => false
adamc@623 2838
adamc@312 2839 | CName _ => true
adamc@312 2840
adamc@312 2841 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
adamc@312 2842 | CConcat (c1, c2) => pos c1 andalso pos c2
adamc@621 2843 | CMap => true
adamc@312 2844
adamc@312 2845 | CUnit => true
adamc@312 2846
adamc@312 2847 | CTuple cs => List.all pos cs
adamc@312 2848 | CProj (c, _) => pos c
adamc@312 2849
adamc@312 2850 | CWild _ => false
adamc@312 2851 in
adamc@312 2852 pos
adamc@312 2853 end
adamc@312 2854
adamc@706 2855 and wildifyStr env (str, sgn) =
adamc@325 2856 case #1 (hnormSgn env sgn) of
adamc@325 2857 L'.SgnConst sgis =>
adamc@325 2858 (case #1 str of
adamc@325 2859 L.StrConst ds =>
adamc@325 2860 let
adamc@493 2861 fun decompileKind (k, loc) =
adamc@493 2862 case k of
adamc@493 2863 L'.KType => SOME (L.KType, loc)
adamc@493 2864 | L'.KArrow (k1, k2) =>
adamc@493 2865 (case (decompileKind k1, decompileKind k2) of
adamc@493 2866 (SOME k1, SOME k2) => SOME (L.KArrow (k1, k2), loc)
adamc@493 2867 | _ => NONE)
adamc@493 2868 | L'.KName => SOME (L.KName, loc)
adamc@493 2869 | L'.KRecord k =>
adamc@493 2870 (case decompileKind k of
adamc@493 2871 SOME k => SOME (L.KRecord k, loc)
adamc@493 2872 | _ => NONE)
adamc@493 2873 | L'.KUnit => SOME (L.KUnit, loc)
adamc@493 2874 | L'.KTuple ks =>
adamc@493 2875 let
adamc@493 2876 val ks' = List.mapPartial decompileKind ks
adamc@493 2877 in
adamc@493 2878 if length ks' = length ks then
adamc@493 2879 SOME (L.KTuple ks', loc)
adamc@493 2880 else
adamc@493 2881 NONE
adamc@493 2882 end
adamc@493 2883
adamc@493 2884 | L'.KError => NONE
adamc@493 2885 | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
adamc@493 2886 | L'.KUnif _ => NONE
adamc@493 2887
adamc@623 2888 | L'.KRel _ => NONE
adamc@623 2889 | L'.KFun _ => NONE
adamc@623 2890
adamc@325 2891 fun decompileCon env (c, loc) =
adamc@325 2892 case c of
adamc@325 2893 L'.CRel i =>
adamc@325 2894 let
adamc@325 2895 val (s, _) = E.lookupCRel env i
adamc@325 2896 in
adamc@325 2897 SOME (L.CVar ([], s), loc)
adamc@325 2898 end
adamc@325 2899 | L'.CNamed i =>
adamc@325 2900 let
adamc@325 2901 val (s, _, _) = E.lookupCNamed env i
adamc@325 2902 in
adamc@325 2903 SOME (L.CVar ([], s), loc)
adamc@325 2904 end
adamc@325 2905 | L'.CModProj (m1, ms, x) =>
adamc@325 2906 let
adamc@325 2907 val (s, _) = E.lookupStrNamed env m1
adamc@325 2908 in
adamc@325 2909 SOME (L.CVar (s :: ms, x), loc)
adamc@325 2910 end
adamc@325 2911 | L'.CName s => SOME (L.CName s, loc)
adamc@325 2912 | L'.CRecord (_, xcs) =>
adamc@325 2913 let
adamc@325 2914 fun fields xcs =
adamc@325 2915 case xcs of
adamc@325 2916 [] => SOME []
adamc@325 2917 | (x, t) :: xcs =>
adamc@325 2918 case (decompileCon env x, decompileCon env t, fields xcs) of
adamc@325 2919 (SOME x, SOME t, SOME xcs) => SOME ((x, t) :: xcs)
adamc@325 2920 | _ => NONE
adamc@325 2921 in
adamc@325 2922 Option.map (fn xcs => (L.CRecord xcs, loc))
adamc@325 2923 (fields xcs)
adamc@325 2924 end
adamc@325 2925 | L'.CConcat (c1, c2) =>
adamc@325 2926 (case (decompileCon env c1, decompileCon env c2) of
adamc@325 2927 (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc)
adamc@325 2928 | _ => NONE)
adamc@325 2929 | L'.CUnit => SOME (L.CUnit, loc)
adamc@325 2930
adamc@325 2931 | _ => NONE
adamc@325 2932
adamc@469 2933 val (neededC, constraints, neededV, _) =
adamc@469 2934 foldl (fn ((sgi, loc), (neededC, constraints, neededV, env')) =>
adamc@325 2935 let
adamc@469 2936 val (needed, constraints, neededV) =
adamc@325 2937 case sgi of
adamc@493 2938 L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, k), constraints, neededV)
adamc@469 2939 | L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV)
adamc@469 2940
adamc@469 2941 | L'.SgiVal (x, _, t) =>
adamc@469 2942 let
adamc@469 2943 fun default () = (neededC, constraints, neededV)
adamc@469 2944
adamc@469 2945 val t = normClassConstraint env' t
adamc@469 2946 in
adamc@469 2947 case #1 t of
adamc@469 2948 L'.CApp (f, _) =>
adamc@634 2949 if isClassOrFolder env' f then
adamc@469 2950 (neededC, constraints, SS.add (neededV, x))
adamc@469 2951 else
adamc@469 2952 default ()
adamc@469 2953 | _ => default ()
adamc@469 2954 end
adamc@469 2955
adamc@469 2956 | _ => (neededC, constraints, neededV)
adamc@325 2957 in
adamc@469 2958 (needed, constraints, neededV, E.sgiBinds env' (sgi, loc))
adamc@325 2959 end)
adamc@493 2960 (SM.empty, [], SS.empty, env) sgis
adamc@325 2961
adamc@634 2962 val (neededC, neededV) =
adamc@634 2963 foldl (fn ((d, _), needed as (neededC, neededV)) =>
adamc@634 2964 case d of
adamc@634 2965 L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
adamc@634 2966 handle NotFound =>
adamc@634 2967 needed)
adamc@634 2968 | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
adamc@634 2969 handle NotFound => needed)
adamc@634 2970 | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
adamc@634 2971 handle NotFound => needed)
adamc@634 2972 | L.DOpen _ => (SM.empty, SS.empty)
adamc@634 2973 | _ => needed)
adamc@634 2974 (neededC, neededV) ds
adamc@469 2975
adamc@469 2976 val ds' = List.mapPartial (fn (env', (c1, c2), loc) =>
adamc@325 2977 case (decompileCon env' c1, decompileCon env' c2) of
adamc@325 2978 (SOME c1, SOME c2) =>
adamc@325 2979 SOME (L.DConstraint (c1, c2), loc)
adamc@325 2980 | _ => NONE) constraints
adamc@469 2981
adamc@469 2982 val ds' =
adamc@469 2983 case SS.listItems neededV of
adamc@469 2984 [] => ds'
adamc@469 2985 | xs =>
adamc@469 2986 let
adamc@469 2987 val ewild = (L.EWild, #2 str)
adamc@469 2988 val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs
adamc@469 2989 in
adamc@469 2990 ds'' @ ds'
adamc@469 2991 end
adamc@469 2992
adamc@469 2993 val ds' =
adamc@493 2994 case SM.listItemsi neededC of
adamc@469 2995 [] => ds'
adamc@469 2996 | xs =>
adamc@469 2997 let
adamc@493 2998 val ds'' = map (fn (x, k) =>
adamc@493 2999 let
adamc@493 3000 val k =
adamc@493 3001 case decompileKind k of
adamc@493 3002 NONE => (L.KWild, #2 str)
adamc@493 3003 | SOME k => k
adamc@493 3004 val cwild = (L.CWild k, #2 str)
adamc@493 3005 in
adamc@493 3006 (L.DCon (x, NONE, cwild), #2 str)
adamc@493 3007 end) xs
adamc@469 3008 in
adamc@469 3009 ds'' @ ds'
adamc@469 3010 end
adamc@325 3011 in
adamc@469 3012 (L.StrConst (ds @ ds'), #2 str)
adamc@325 3013 end
adamc@325 3014 | _ => str)
adamc@325 3015 | _ => str
adamc@325 3016
adamc@706 3017 and elabDecl (dAll as (d, loc), (env, denv, gs)) =
adamc@255 3018 let
adamc@255 3019 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
adamc@514 3020 (*val befor = Time.now ()*)
adamc@255 3021
adamc@255 3022 val r =
adamc@255 3023 case d of
adamc@255 3024 L.DCon (x, ko, c) =>
adamc@255 3025 let
adamc@255 3026 val k' = case ko of
adamc@255 3027 NONE => kunif loc
adamc@623 3028 | SOME k => elabKind env k
adamc@255 3029
adamc@255 3030 val (c', ck, gs') = elabCon (env, denv) c
adamc@255 3031 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@255 3032 in
adamc@255 3033 checkKind env c' ck k';
adamc@255 3034
adamc@255 3035 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs))
adamc@255 3036 end
adamc@255 3037 | L.DDatatype (x, xs, xcs) =>
adamc@255 3038 let
adamc@312 3039 val positive = List.all (fn (_, to) =>
adamc@312 3040 case to of
adamc@312 3041 NONE => true
adamc@312 3042 | SOME t => positive x t) xcs
adamc@312 3043
adamc@255 3044 val k = (L'.KType, loc)
adamc@255 3045 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@255 3046 val (env, n) = E.pushCNamed env x k' NONE
adamc@255 3047 val t = (L'.CNamed n, loc)
adamc@255 3048 val nxs = length xs - 1
adamc@255 3049 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@255 3050
adamc@255 3051 val (env', denv') = foldl (fn (x, (env', denv')) =>
adamc@255 3052 (E.pushCRel env' x k,
adamc@255 3053 D.enter denv')) (env, denv) xs
adamc@255 3054
adamc@255 3055 val (xcs, (used, env, gs')) =
adamc@255 3056 ListUtil.foldlMap
adamc@255 3057 (fn ((x, to), (used, env, gs)) =>
adamc@255 3058 let
adamc@255 3059 val (to, t, gs') = case to of
adamc@255 3060 NONE => (NONE, t, gs)
adamc@255 3061 | SOME t' =>
adamc@255 3062 let
adamc@255 3063 val (t', tk, gs') = elabCon (env', denv') t'
adamc@255 3064 in
adamc@255 3065 checkKind env' t' tk k;
adamc@255 3066 (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs)
adamc@255 3067 end
adamc@255 3068 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
adamc@255 3069
adamc@255 3070 val (env, n') = E.pushENamed env x t
adamc@255 3071 in
adamc@255 3072 if SS.member (used, x) then
adamc@255 3073 strError env (DuplicateConstructor (x, loc))
adamc@255 3074 else
adamc@255 3075 ();
adamc@255 3076 ((x, n', to), (SS.add (used, x), env, gs'))
adamc@255 3077 end)
adamc@255 3078 (SS.empty, env, []) xcs
adamc@255 3079
adamc@255 3080 val env = E.pushDatatype env n xs xcs
adamc@312 3081 val d' = (L'.DDatatype (x, n, xs, xcs), loc)
adamc@255 3082 in
adamc@601 3083 (*if positive then
adamc@312 3084 ()
adamc@312 3085 else
adamc@601 3086 declError env (Nonpositive d');*)
adamc@312 3087
adamc@312 3088 ([d'], (env, denv, gs' @ gs))
adamc@255 3089 end
adamc@255 3090
adamc@255 3091 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
adamc@255 3092
adamc@255 3093 | L.DDatatypeImp (x, m1 :: ms, s) =>
adamc@255 3094 (case E.lookupStr env m1 of
adamc@255 3095 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@255 3096 ([], (env, denv, gs)))
adamc@255 3097 | SOME (n, sgn) =>
adamc@255 3098 let
adamc@255 3099 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@255 3100 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@255 3101 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@255 3102 (strerror, sgnerror))
adamc@255 3103 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@255 3104 ((L'.StrVar n, loc), sgn) ms
adamc@255 3105 in
adamc@628 3106 case hnormCon env (L'.CModProj (n, ms, s), loc) of
adamc@628 3107 (L'.CModProj (n, ms, s), _) =>
adamc@255 3108 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
adamc@255 3109 NONE => (conError env (UnboundDatatype (loc, s));
adamc@255 3110 ([], (env, denv, gs)))
adamc@255 3111 | SOME (xs, xncs) =>
adamc@255 3112 let
adamc@255 3113 val k = (L'.KType, loc)
adamc@255 3114 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@255 3115 val t = (L'.CModProj (n, ms, s), loc)
adamc@255 3116 val (env, n') = E.pushCNamed env x k' (SOME t)
adamc@255 3117 val env = E.pushDatatype env n' xs xncs
adamc@255 3118
adamc@255 3119 val t = (L'.CNamed n', loc)
adamc@255 3120 val env = foldl (fn ((x, n, to), env) =>
adamc@255 3121 let
adamc@255 3122 val t = case to of
adamc@255 3123 NONE => t
adamc@255 3124 | SOME t' => (L'.TFun (t', t), loc)
adamc@255 3125
adamc@255 3126 val t = foldr (fn (x, t) =>
adamc@255 3127 (L'.TCFun (L'.Implicit, x, k, t), loc))
adamc@255 3128 t xs
adamc@255 3129 in
adamc@255 3130 E.pushENamedAs env x n t
adamc@255 3131 end) env xncs
adamc@255 3132 in
adamc@628 3133 ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
adamc@255 3134 end)
adamc@255 3135 | _ => (strError env (NotDatatype loc);
adamc@255 3136 ([], (env, denv, [])))
adamc@255 3137 end)
adamc@255 3138
adamc@255 3139 | L.DVal (x, co, e) =>
adamc@255 3140 let
adamc@255 3141 val (c', _, gs1) = case co of
adamc@255 3142 NONE => (cunif (loc, ktype), ktype, [])
adamc@255 3143 | SOME c => elabCon (env, denv) c
adamc@255 3144
adamc@255 3145 val (e', et, gs2) = elabExp (env, denv) e
adamc@629 3146
adamc@629 3147 val () = checkCon env e' et c'
adamc@629 3148
adamc@674 3149 val c' = normClassConstraint env c'
adamc@255 3150 val (env', n) = E.pushENamed env x c'
adamc@255 3151 in
adamc@255 3152 (*prefaces "DVal" [("x", Print.PD.string x),
adamc@362 3153 ("c'", p_con env c')];*)
adamc@628 3154 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs))
adamc@255 3155 end
adamc@255 3156 | L.DValRec vis =>
adamc@255 3157 let
adamc@255 3158 fun allowable (e, _) =
adamc@255 3159 case e of
adamc@255 3160 L.EAbs _ => true
adamc@255 3161 | L.ECAbs (_, _, _, e) => allowable e
adamc@623 3162 | L.EKAbs (_, e) => allowable e
adamc@255 3163 | L.EDisjoint (_, _, e) => allowable e
adamc@255 3164 | _ => false
adamc@255 3165
adamc@255 3166 val (vis, gs) = ListUtil.foldlMap
adamc@255 3167 (fn ((x, co, e), gs) =>
adamc@255 3168 let
adamc@255 3169 val (c', _, gs1) = case co of
adamc@255 3170 NONE => (cunif (loc, ktype), ktype, [])
adamc@255 3171 | SOME c => elabCon (env, denv) c
adamc@674 3172 val c' = normClassConstraint env c'
adamc@255 3173 in
adamc@255 3174 ((x, c', e), enD gs1 @ gs)
adamc@280 3175 end) gs vis
adamc@255 3176
adamc@255 3177 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
adamc@255 3178 let
adamc@255 3179 val (env, n) = E.pushENamed env x c'
adamc@255 3180 in
adamc@255 3181 ((x, n, c', e), env)
adamc@255 3182 end) env vis
adamc@255 3183
adamc@255 3184 val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
adamc@255 3185 let
adamc@255 3186 val (e', et, gs1) = elabExp (env, denv) e
adamc@255 3187 in
adamc@628 3188 checkCon env e' et c';
adamc@255 3189 if allowable e then
adamc@255 3190 ()
adamc@255 3191 else
adamc@255 3192 expError env (IllegalRec (x, e'));
adamc@628 3193 ((x, n, c', e'), gs1 @ gs)
adamc@255 3194 end) gs vis
adamc@255 3195 in
adamc@255 3196 ([(L'.DValRec vis, loc)], (env, denv, gs))
adamc@255 3197 end
adamc@255 3198
adamc@255 3199 | L.DSgn (x, sgn) =>
adamc@255 3200 let
adamc@255 3201 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@255 3202 val (env', n) = E.pushSgnNamed env x sgn'
adamc@255 3203 in
adamc@255 3204 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
adamc@255 3205 end
adamc@255 3206
adamc@255 3207 | L.DStr (x, sgno, str) =>
adamc@255 3208 let
adamc@255 3209 val () = if x = "Basis" then
adamc@255 3210 raise Fail "Not allowed to redefine structure 'Basis'"
adamc@255 3211 else
adamc@255 3212 ()
adamc@255 3213
adamc@255 3214 val formal = Option.map (elabSgn (env, denv)) sgno
adamc@255 3215
adamc@255 3216 val (str', sgn', gs') =
adamc@255 3217 case formal of
adamc@255 3218 NONE =>
adamc@255 3219 let
adamc@255 3220 val (str', actual, gs') = elabStr (env, denv) str
adamc@255 3221 in
adamc@255 3222 (str', selfifyAt env {str = str', sgn = actual}, gs')
adamc@255 3223 end
adamc@255 3224 | SOME (formal, gs1) =>
adamc@255 3225 let
adamc@325 3226 val str = wildifyStr env (str, formal)
adamc@255 3227 val (str', actual, gs2) = elabStr (env, denv) str
adamc@255 3228 in
adamc@628 3229 subSgn env (selfifyAt env {str = str', sgn = actual}) formal;
adamc@255 3230 (str', formal, enD gs1 @ gs2)
adamc@255 3231 end
adamc@255 3232
adamc@255 3233 val (env', n) = E.pushStrNamed env x sgn'
adamc@255 3234 in
adamc@255 3235 case #1 (hnormSgn env sgn') of
adamc@255 3236 L'.SgnFun _ =>
adamc@255 3237 (case #1 str' of
adamc@255 3238 L'.StrFun _ => ()
adamc@255 3239 | _ => strError env (FunctorRebind loc))
adamc@255 3240 | _ => ();
adamc@255 3241
adamc@255 3242 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
adamc@255 3243 end
adamc@255 3244
adamc@255 3245 | L.DFfiStr (x, sgn) =>
adamc@255 3246 let
adamc@255 3247 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@255 3248
adamc@255 3249 val (env', n) = E.pushStrNamed env x sgn'
adamc@255 3250 in
adamc@255 3251 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs))
adamc@255 3252 end
adamc@255 3253
adamc@255 3254 | L.DOpen (m, ms) =>
adamc@255 3255 (case E.lookupStr env m of
adamc@255 3256 NONE => (strError env (UnboundStr (loc, m));
adamc@255 3257 ([], (env, denv, gs)))
adamc@255 3258 | SOME (n, sgn) =>
adamc@255 3259 let
adamc@255 3260 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@255 3261 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@255 3262 NONE => (strError env (UnboundStr (loc, m));
adamc@255 3263 (strerror, sgnerror))
adamc@255 3264 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@255 3265 ((L'.StrVar n, loc), sgn) ms
adamc@255 3266
adamc@628 3267 val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn}
adamc@628 3268 val denv' = dopenConstraints (loc, env', denv) {str = m, strs = ms}
adamc@255 3269 in
adamc@255 3270 (ds, (env', denv', gs))
adamc@255 3271 end)
adamc@255 3272
adamc@255 3273 | L.DConstraint (c1, c2) =>
adamc@255 3274 let
adamc@255 3275 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@255 3276 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@255 3277 val gs3 = D.prove env denv (c1', c2', loc)
adamc@255 3278
adamc@628 3279 val denv' = D.assert env denv (c1', c2')
adamc@255 3280 in
adamc@255 3281 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
adamc@255 3282 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
adamc@255 3283
adamc@628 3284 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ gs))
adamc@255 3285 end
adamc@255 3286
adamc@255 3287 | L.DOpenConstraints (m, ms) =>
adamc@255 3288 let
adamc@255 3289 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
adamc@255 3290 in
adamc@255 3291 ([], (env, denv, gs))
adamc@255 3292 end
adamc@255 3293
adamc@255 3294 | L.DExport str =>
adamc@255 3295 let
adamc@255 3296 val (str', sgn, gs') = elabStr (env, denv) str
adamc@255 3297
adamc@255 3298 val sgn =
adamc@255 3299 case #1 (hnormSgn env sgn) of
adamc@255 3300 L'.SgnConst sgis =>
adamc@255 3301 let
adamc@255 3302 fun doOne (all as (sgi, _), env) =
adamc@255 3303 (case sgi of
adamc@255 3304 L'.SgiVal (x, n, t) =>
adamc@325 3305 let
adamc@325 3306 fun doPage (makeRes, ran) =
adamc@628 3307 case hnormCon env ran of
adamc@628 3308 (L'.CApp (tf, arg), _) =>
adamc@628 3309 (case (hnormCon env tf, hnormCon env arg) of
adamc@628 3310 ((L'.CModProj (basis, [], "transaction"), _),
adamc@628 3311 (L'.CApp (tf, arg3), _)) =>
adamc@325 3312 (case (basis = !basis_r,
adamc@628 3313 hnormCon env tf, hnormCon env arg3) of
adamc@325 3314 (true,
adamc@628 3315 (L'.CApp (tf, arg2), _),
adamc@628 3316 ((L'.CRecord (_, []), _))) =>
adamc@628 3317 (case (hnormCon env tf) of
adamc@628 3318 (L'.CApp (tf, arg1), _) =>
adamc@628 3319 (case (hnormCon env tf,
adamc@628 3320 hnormCon env arg1,
adamc@628 3321 hnormCon env arg2) of
adamc@628 3322 (tf, arg1,
adamc@628 3323 (L'.CRecord (_, []), _)) =>
adamc@325 3324 let
adamc@325 3325 val t = (L'.CApp (tf, arg1), loc)
adamc@325 3326 val t = (L'.CApp (t, arg2), loc)
adamc@325 3327 val t = (L'.CApp (t, arg3), loc)
adamc@325 3328 val t = (L'.CApp (
adamc@325 3329 (L'.CModProj
adamc@325 3330 (basis, [], "transaction"), loc),
adamc@325 3331 t), loc)
adamc@325 3332 in
adamc@325 3333 (L'.SgiVal (x, n, makeRes t), loc)
adamc@325 3334 end
adamc@325 3335 | _ => all)
adamc@325 3336 | _ => all)
adamc@325 3337 | _ => all)
adamc@325 3338 | _ => all)
adamc@325 3339 | _ => all
adamc@325 3340 in
adamc@628 3341 case hnormCon env t of
adamc@628 3342 (L'.TFun (dom, ran), _) =>
adamc@628 3343 (case hnormCon env dom of
adamc@628 3344 (L'.TRecord domR, _) =>
adamc@325 3345 doPage (fn t => (L'.TFun ((L'.TRecord domR,
adamc@325 3346 loc),
adamc@325 3347 t), loc), ran)
adamc@325 3348 | _ => all)
adamc@325 3349 | _ => doPage (fn t => t, t)
adamc@325 3350 end
adamc@255 3351 | _ => all,
adamc@255 3352 E.sgiBinds env all)
adamc@255 3353 in
adamc@255 3354 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
adamc@255 3355 end
adamc@255 3356 | _ => sgn
adamc@255 3357 in
adamc@255 3358 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
adamc@255 3359 end
adamc@255 3360
adamc@707 3361 | L.DTable (x, c, pe, ce) =>
adamc@255 3362 let
adamc@707 3363 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
adamc@707 3364
adamc@255 3365 val (c', k, gs') = elabCon (env, denv) c
adamc@707 3366 val pkey = cunif (loc, cstK)
adamc@707 3367 val uniques = cunif (loc, cstK)
adamc@705 3368
adamc@705 3369 val ct = tableOf ()
adamc@705 3370 val ct = (L'.CApp (ct, c'), loc)
adamc@707 3371 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc)
adamc@705 3372
adamc@705 3373 val (env, n) = E.pushENamed env x ct
adamc@707 3374 val (pe', pet, gs'') = elabExp (env, denv) pe
adamc@707 3375 val (ce', cet, gs''') = elabExp (env, denv) ce
adamc@707 3376
adamc@707 3377 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc)
adamc@707 3378 val pst = (L'.CApp (pst, c'), loc)
adamc@707 3379 val pst = (L'.CApp (pst, pkey), loc)
adamc@704 3380
adamc@704 3381 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
adamc@704 3382 val cst = (L'.CApp (cst, c'), loc)
adamc@705 3383 val cst = (L'.CApp (cst, uniques), loc)
adamc@255 3384 in
adamc@255 3385 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
adamc@707 3386 checkCon env pe' pet pst;
adamc@707 3387 checkCon env ce' cet cst;
adamc@707 3388 ([(L'.DTable (!basis_r, x, n, c', pe', pkey, ce', uniques), loc)],
adamc@707 3389 (env, denv, gs''' @ gs'' @ enD gs' @ gs))
adamc@255 3390 end
adamc@338 3391 | L.DSequence x =>
adamc@338 3392 let
adamc@338 3393 val (env, n) = E.pushENamed env x (sequenceOf ())
adamc@338 3394 in
adamc@338 3395 ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs))
adamc@338 3396 end
adamc@255 3397
adamc@563 3398 | L.DClass (x, k, c) =>
adamc@255 3399 let
adamc@623 3400 val k = elabKind env k
adamc@563 3401 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
adamc@280 3402 val (c', ck, gs') = elabCon (env, denv) c
adamc@563 3403 val (env, n) = E.pushCNamed env x k' (SOME c')
adamc@255 3404 val env = E.pushClass env n
adamc@255 3405 in
adamc@563 3406 checkKind env c' ck k';
adamc@563 3407 ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs))
adamc@255 3408 end
adamc@271 3409
adamc@280 3410 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
adamc@280 3411
adamc@459 3412 | L.DCookie (x, c) =>
adamc@459 3413 let
adamc@459 3414 val (c', k, gs') = elabCon (env, denv) c
adamc@459 3415 val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc)
adamc@459 3416 in
adamc@459 3417 checkKind env c' k (L'.KType, loc);
adamc@459 3418 ([(L'.DCookie (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs))
adamc@459 3419 end
adamc@459 3420
adamc@280 3421 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
adamc@255 3422 in
adamc@280 3423 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll),
adamc@514 3424 ("t", PD.string (LargeReal.toString (Time.toReal
adamc@514 3425 (Time.- (Time.now (), befor)))))];*)
adamc@280 3426
adamc@255 3427 r
adamc@255 3428 end
adamc@211 3429
adamc@83 3430 and elabStr (env, denv) (str, loc) =
adamc@31 3431 case str of
adamc@31 3432 L.StrConst ds =>
adamc@31 3433 let
adamc@88 3434 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
adamc@123 3435 val sgis = ListUtil.mapConcat sgiOfDecl ds'
adamc@63 3436
adamc@63 3437 val (sgis, _, _, _, _) =
adamc@64 3438 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
adamc@63 3439 case sgi of
adamc@64 3440 L'.SgiConAbs (x, n, k) =>
adamc@64 3441 let
adamc@64 3442 val (cons, x) =
adamc@64 3443 if SS.member (cons, x) then
adamc@64 3444 (cons, "?" ^ x)
adamc@64 3445 else
adamc@64 3446 (SS.add (cons, x), x)
adamc@64 3447 in
adamc@64 3448 ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 3449 end
adamc@64 3450 | L'.SgiCon (x, n, k, c) =>
adamc@64 3451 let
adamc@64 3452 val (cons, x) =
adamc@64 3453 if SS.member (cons, x) then
adamc@64 3454 (cons, "?" ^ x)
adamc@64 3455 else
adamc@64 3456 (SS.add (cons, x), x)
adamc@64 3457 in
adamc@64 3458 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 3459 end
adamc@191 3460 | L'.SgiDatatype (x, n, xs, xncs) =>
adamc@156 3461 let
adamc@156 3462 val (cons, x) =
adamc@156 3463 if SS.member (cons, x) then
adamc@156 3464 (cons, "?" ^ x)
adamc@156 3465 else
adamc@156 3466 (SS.add (cons, x), x)
adamc@156 3467
adamc@156 3468 val (xncs, vals) =
adamc@156 3469 ListUtil.foldlMap
adamc@156 3470 (fn ((x, n, t), vals) =>
adamc@156 3471 if SS.member (vals, x) then
adamc@156 3472 (("?" ^ x, n, t), vals)
adamc@156 3473 else
adamc@156 3474 ((x, n, t), SS.add (vals, x)))
adamc@156 3475 vals xncs
adamc@156 3476 in
adamc@191 3477 ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
adamc@156 3478 end
adamc@191 3479 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@156 3480 let
adamc@156 3481 val (cons, x) =
adamc@156 3482 if SS.member (cons, x) then
adamc@156 3483 (cons, "?" ^ x)
adamc@156 3484 else
adamc@156 3485 (SS.add (cons, x), x)
adamc@156 3486 in
adamc@191 3487 ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
adamc@156 3488 end
adamc@64 3489 | L'.SgiVal (x, n, c) =>
adamc@64 3490 let
adamc@64 3491 val (vals, x) =
adamc@64 3492 if SS.member (vals, x) then
adamc@64 3493 (vals, "?" ^ x)
adamc@64 3494 else
adamc@64 3495 (SS.add (vals, x), x)
adamc@64 3496 in
adamc@64 3497 ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 3498 end
adamc@64 3499 | L'.SgiSgn (x, n, sgn) =>
adamc@64 3500 let
adamc@64 3501 val (sgns, x) =
adamc@64 3502 if SS.member (sgns, x) then
adamc@64 3503 (sgns, "?" ^ x)
adamc@64 3504 else
adamc@64 3505 (SS.add (sgns, x), x)
adamc@64 3506 in
adamc@64 3507 ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 3508 end
adamc@64 3509
adamc@64 3510 | L'.SgiStr (x, n, sgn) =>
adamc@64 3511 let
adamc@64 3512 val (strs, x) =
adamc@64 3513 if SS.member (strs, x) then
adamc@64 3514 (strs, "?" ^ x)
adamc@64 3515 else
adamc@64 3516 (SS.add (strs, x), x)
adamc@64 3517 in
adamc@64 3518 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@88 3519 end
adamc@203 3520 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
adamc@563 3521 | L'.SgiClassAbs (x, n, k) =>
adamc@211 3522 let
adamc@211 3523 val (cons, x) =
adamc@211 3524 if SS.member (cons, x) then
adamc@211 3525 (cons, "?" ^ x)
adamc@211 3526 else
adamc@211 3527 (SS.add (cons, x), x)
adamc@211 3528 in
adamc@563 3529 ((L'.SgiClassAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
adamc@211 3530 end
adamc@563 3531 | L'.SgiClass (x, n, k, c) =>
adamc@211 3532 let
adamc@211 3533 val (cons, x) =
adamc@211 3534 if SS.member (cons, x) then
adamc@211 3535 (cons, "?" ^ x)
adamc@211 3536 else
adamc@211 3537 (SS.add (cons, x), x)
adamc@211 3538 in
adamc@563 3539 ((L'.SgiClass (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@203 3540 end)
adamc@64 3541
adamc@63 3542 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
adamc@31 3543 in
adamc@83 3544 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)
adamc@31 3545 end
adamc@31 3546 | L.StrVar x =>
adamc@31 3547 (case E.lookupStr env x of
adamc@31 3548 NONE =>
adamc@31 3549 (strError env (UnboundStr (loc, x));
adamc@83 3550 (strerror, sgnerror, []))
adamc@83 3551 | SOME (n, sgn) => ((L'.StrVar n, loc), sgn, []))
adamc@34 3552 | L.StrProj (str, x) =>
adamc@34 3553 let
adamc@83 3554 val (str', sgn, gs) = elabStr (env, denv) str
adamc@34 3555 in
adamc@34 3556 case E.projectStr env {str = str', sgn = sgn, field = x} of
adamc@34 3557 NONE => (strError env (UnboundStr (loc, x));
adamc@83 3558 (strerror, sgnerror, []))
adamc@83 3559 | SOME sgn => ((L'.StrProj (str', x), loc), sgn, gs)
adamc@34 3560 end
adamc@41 3561 | L.StrFun (m, dom, ranO, str) =>
adamc@41 3562 let
adamc@83 3563 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41 3564 val (env', n) = E.pushStrNamed env m dom'
adamc@83 3565 val (str', actual, gs2) = elabStr (env', denv) str
adamc@41 3566
adamc@83 3567 val (formal, gs3) =
adamc@41 3568 case ranO of
adamc@83 3569 NONE => (actual, [])
adamc@41 3570 | SOME ran =>
adamc@41 3571 let
adamc@83 3572 val (ran', gs) = elabSgn (env', denv) ran
adamc@41 3573 in
adamc@628 3574 subSgn env' actual ran';
adamc@83 3575 (ran', gs)
adamc@41 3576 end
adamc@41 3577 in
adamc@41 3578 ((L'.StrFun (m, n, dom', formal, str'), loc),
adamc@83 3579 (L'.SgnFun (m, n, dom', formal), loc),
adamc@228 3580 enD gs1 @ gs2 @ enD gs3)
adamc@41 3581 end
adamc@44 3582 | L.StrApp (str1, str2) =>
adamc@44 3583 let
adamc@83 3584 val (str1', sgn1, gs1) = elabStr (env, denv) str1
adamc@325 3585 val str2 =
adamc@325 3586 case sgn1 of
adamc@325 3587 (L'.SgnFun (_, _, dom, _), _) =>
adamc@325 3588 wildifyStr env (str2, dom)
adamc@325 3589 | _ => str2
adamc@83 3590 val (str2', sgn2, gs2) = elabStr (env, denv) str2
adamc@44 3591 in
adamc@44 3592 case #1 (hnormSgn env sgn1) of
adamc@83 3593 L'.SgnError => (strerror, sgnerror, [])
adamc@44 3594 | L'.SgnFun (m, n, dom, ran) =>
adamc@628 3595 (subSgn env sgn2 dom;
adamc@44 3596 case #1 (hnormSgn env ran) of
adamc@83 3597 L'.SgnError => (strerror, sgnerror, [])
adamc@44 3598 | L'.SgnConst sgis =>
adamc@44 3599 ((L'.StrApp (str1', str2'), loc),
adamc@83 3600 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
adamc@83 3601 gs1 @ gs2)
adamc@44 3602 | _ => raise Fail "Unable to hnormSgn in functor application")
adamc@44 3603 | _ => (strError env (NotFunctor sgn1);
adamc@83 3604 (strerror, sgnerror, []))
adamc@44 3605 end
adamc@31 3606
adamc@325 3607 fun elabFile basis topStr topSgn env file =
adamc@56 3608 let
adamc@83 3609 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
adamc@83 3610 val () = case gs of
adamc@83 3611 [] => ()
adamc@207 3612 | _ => (app (fn (_, env, _, c1, c2) =>
adamc@207 3613 prefaces "Unresolved"
adamc@207 3614 [("c1", p_con env c1),
adamc@207 3615 ("c2", p_con env c2)]) gs;
adamc@207 3616 raise Fail "Unresolved disjointness constraints in Basis")
adamc@83 3617
adamc@56 3618 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
adamc@210 3619 val () = basis_r := basis_n
adamc@56 3620
adamc@628 3621 val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn}
adamc@56 3622
adamc@56 3623 fun discoverC r x =
adamc@56 3624 case E.lookupC env' x of
adamc@56 3625 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
adamc@56 3626 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
adamc@56 3627 | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc)
adamc@56 3628
adamc@56 3629 val () = discoverC int "int"
adamc@56 3630 val () = discoverC float "float"
adamc@56 3631 val () = discoverC string "string"
adamc@203 3632 val () = discoverC table "sql_table"
adamc@56 3633
adamc@325 3634 val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan)
adamc@325 3635 val () = case gs of
adamc@325 3636 [] => ()
adamc@325 3637 | _ => raise Fail "Unresolved disjointness constraints in top.urs"
adamc@325 3638 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
adamc@325 3639 val () = case gs of
adamc@325 3640 [] => ()
adamc@329 3641 | _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
adamc@329 3642 (case D.prove env denv (c1, c2, loc) of
adamc@329 3643 [] => ()
adamc@329 3644 | _ =>
adamc@329 3645 (prefaces "Unresolved constraint in top.ur"
adamc@329 3646 [("loc", PD.string (ErrorMsg.spanToString loc)),
adamc@329 3647 ("c1", p_con env c1),
adamc@329 3648 ("c2", p_con env c2)];
adamc@478 3649 raise Fail "Unresolved constraint in top.ur"))
adamc@564 3650 | TypeClass (env, c, r, loc) =>
adamc@564 3651 let
adamc@564 3652 val c = normClassKey env c
adamc@564 3653 in
adamc@564 3654 case E.resolveClass env c of
adamc@564 3655 SOME e => r := SOME e
adamc@564 3656 | NONE => expError env (Unresolvable (loc, c))
adamc@634 3657 end) gs
adamc@564 3658
adamc@628 3659 val () = subSgn env' topSgn' topSgn
adamc@325 3660
adamc@325 3661 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
adamc@633 3662 val () = top_r := top_n
adamc@325 3663
adamc@628 3664 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
adamc@325 3665
adamc@83 3666 fun elabDecl' (d, (env, gs)) =
adamc@76 3667 let
adamc@76 3668 val () = resetKunif ()
adamc@76 3669 val () = resetCunif ()
adamc@88 3670 val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs))
adamc@76 3671 in
adamc@76 3672 if ErrorMsg.anyErrors () then
adamc@76 3673 ()
adamc@76 3674 else (
adamc@76 3675 if List.exists kunifsInDecl ds then
adamc@91 3676 declError env (KunifsRemain ds)
adamc@76 3677 else
adamc@76 3678 ();
adamc@76 3679
adamc@76 3680 case ListUtil.search cunifsInDecl ds of
adamc@76 3681 NONE => ()
adamc@76 3682 | SOME loc =>
adamc@91 3683 declError env (CunifsRemain ds)
adamc@76 3684 );
adamc@76 3685
adamc@83 3686 (ds, (env, gs))
adamc@76 3687 end
adamc@76 3688
adamc@83 3689 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
adamc@56 3690 in
adamc@84 3691 if ErrorMsg.anyErrors () then
adamc@84 3692 ()
adamc@84 3693 else
adamc@228 3694 app (fn Disjoint (loc, env, denv, c1, c2) =>
adamc@228 3695 (case D.prove env denv (c1, c2, loc) of
adamc@228 3696 [] => ()
adamc@228 3697 | _ =>
adamc@228 3698 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
adamc@228 3699 eprefaces' [("Con 1", p_con env c1),
adamc@228 3700 ("Con 2", p_con env c2),
adamc@228 3701 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
adamc@228 3702 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))]))
adamc@228 3703 | TypeClass (env, c, r, loc) =>
adamc@349 3704 let
adamc@634 3705 fun default () = expError env (Unresolvable (loc, c))
adamc@634 3706
adamc@467 3707 val c = normClassKey env c
adamc@349 3708 in
adamc@349 3709 case E.resolveClass env c of
adamc@349 3710 SOME e => r := SOME e
adamc@634 3711 | NONE =>
adamc@634 3712 case #1 (hnormCon env c) of
adamc@634 3713 L'.CApp (f, x) =>
adamc@634 3714 (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
adamc@634 3715 (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
adamc@634 3716 (case #1 (hnormCon env f) of
adamc@634 3717 L'.CModProj (top_n', [], "folder") =>
adamc@634 3718 if top_n' = top_n then
adamc@634 3719 let
adamc@634 3720 val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
adamc@634 3721 val e = (L'.EKApp (e, k), loc)
adamc@634 3722
adamc@634 3723 val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
adamc@634 3724 let
adamc@634 3725 val e = (L'.EModProj (top_n, ["Folder"],
adamc@634 3726 "cons"), loc)
adamc@634 3727 val e = (L'.EKApp (e, k), loc)
adamc@634 3728 val e = (L'.ECApp (e,
adamc@634 3729 (L'.CRecord (k, xcs),
adamc@634 3730 loc)), loc)
adamc@634 3731 val e = (L'.ECApp (e, x), loc)
adamc@634 3732 val e = (L'.ECApp (e, c), loc)
adamc@634 3733 val e = (L'.EApp (e, folder), loc)
adamc@634 3734 in
adamc@634 3735 (e, (x, c) :: xcs)
adamc@634 3736 end)
adamc@634 3737 (e, []) xcs
adamc@634 3738 in
adamc@634 3739 r := SOME folder
adamc@634 3740 end
adamc@634 3741 else
adamc@634 3742 default ()
adamc@634 3743 | _ => default ())
adamc@634 3744 | _ => default ())
adamc@634 3745 | _ => default ()
adamc@349 3746 end) gs;
adamc@83 3747
adamc@325 3748 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
adamc@325 3749 :: ds
adamc@325 3750 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
adamc@325 3751 :: ds' @ file
adamc@56 3752 end
adamc@2 3753
adamc@2 3754 end