Mercurial > urweb

annotate src/elaborate.sml @ 1866:9fc086e3c95a

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