Mercurial > urweb

annotate src/elaborate.sml @ 1076:dcf98ae3c48d

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