Mercurial > urweb

annotate src/elaborate.sml @ 1657:2b7d3d99dc42

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