Mercurial > urweb

annotate src/elaborate.sml @ 1726:4df4521fbd3b

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