Mercurial > urweb

annotate src/elaborate.sml @ 2043:e762c96fffb7

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