Mercurial > urweb

annotate src/elaborate.sml @ 2067:88841212f0ba

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