Mercurial > urweb

annotate src/elaborate.sml @ 1242:4ed556678214

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