Mercurial > urweb

annotate src/elaborate.sml @ 904:6d9538ce94d8

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