Mercurial > urweb

annotate src/elaborate.sml @ 1659:8de2ea0a0701

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