Mercurial > urweb

annotate src/elaborate.sml @ 109:813e5a52063d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove closure conversion in favor of zany fun with modules, which also replaces 'page'
author Adam Chlipala <adamc@hcoop.net>
date Sun, 13 Jul 2008 10:17:06 -0400
parents f0f59e918cac
children 3739af9e727a
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 * All rights reserved.
adamc@2 3 *
adamc@2 4 * Redistribution and use in source and binary forms, with or without
adamc@2 5 * modification, are permitted provided that the following conditions are met:
adamc@2 6 *
adamc@2 7 * - Redistributions of source code must retain the above copyright notice,
adamc@2 8 * this list of conditions and the following disclaimer.
adamc@2 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@2 10 * this list of conditions and the following disclaimer in the documentation
adamc@2 11 * and/or other materials provided with the distribution.
adamc@2 12 * - The names of contributors may not be used to endorse or promote products
adamc@2 13 * derived from this software without specific prior written permission.
adamc@2 14 *
adamc@2 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@2 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@2 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@2 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@2 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@2 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@2 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@2 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@2 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@2 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@2 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@2 26 *)
adamc@2 27
adamc@2 28 structure Elaborate :> ELABORATE = struct
adamc@2 29
adamc@14 30 structure P = Prim
adamc@4 31 structure L = Source
adamc@2 32 structure L' = Elab
adamc@2 33 structure E = ElabEnv
adamc@2 34 structure U = ElabUtil
adamc@82 35 structure D = Disjoint
adamc@2 36
adamc@3 37 open Print
adamc@3 38 open ElabPrint
adamc@3 39
adamc@62 40 structure SS = BinarySetFn(struct
adamc@62 41 type ord_key = string
adamc@62 42 val compare = String.compare
adamc@62 43 end)
adamc@62 44
adamc@2 45 fun elabExplicitness e =
adamc@2 46 case e of
adamc@2 47 L.Explicit => L'.Explicit
adamc@2 48 | L.Implicit => L'.Implicit
adamc@2 49
adamc@2 50 fun occursKind r =
adamc@76 51 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
adamc@2 52 | _ => false)
adamc@2 53
adamc@3 54 datatype kunify_error =
adamc@2 55 KOccursCheckFailed of L'.kind * L'.kind
adamc@2 56 | KIncompatible of L'.kind * L'.kind
adamc@2 57
adamc@3 58 exception KUnify' of kunify_error
adamc@3 59
adamc@3 60 fun kunifyError err =
adamc@2 61 case err of
adamc@2 62 KOccursCheckFailed (k1, k2) =>
adamc@3 63 eprefaces "Kind occurs check failed"
adamc@3 64 [("Kind 1", p_kind k1),
adamc@3 65 ("Kind 2", p_kind k2)]
adamc@2 66 | KIncompatible (k1, k2) =>
adamc@3 67 eprefaces "Incompatible kinds"
adamc@3 68 [("Kind 1", p_kind k1),
adamc@3 69 ("Kind 2", p_kind k2)]
adamc@2 70
adamc@3 71 fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
adamc@2 72 let
adamc@3 73 fun err f = raise KUnify' (f (k1All, k2All))
adamc@2 74 in
adamc@2 75 case (k1, k2) of
adamc@2 76 (L'.KType, L'.KType) => ()
adamc@82 77 | (L'.KUnit, L'.KUnit) => ()
adamc@82 78
adamc@2 79 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
adamc@3 80 (unifyKinds' d1 d2;
adamc@3 81 unifyKinds' r1 r2)
adamc@2 82 | (L'.KName, L'.KName) => ()
adamc@3 83 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
adamc@2 84
adamc@2 85 | (L'.KError, _) => ()
adamc@2 86 | (_, L'.KError) => ()
adamc@2 87
adamc@76 88 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
adamc@76 89 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
adamc@2 90
adamc@76 91 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
adamc@2 92 if r1 = r2 then
adamc@2 93 ()
adamc@2 94 else
adamc@2 95 r1 := SOME k2All
adamc@2 96
adamc@76 97 | (L'.KUnif (_, _, r), _) =>
adamc@2 98 if occursKind r k2All then
adamc@2 99 err KOccursCheckFailed
adamc@2 100 else
adamc@2 101 r := SOME k2All
adamc@76 102 | (_, L'.KUnif (_, _, r)) =>
adamc@2 103 if occursKind r k1All then
adamc@2 104 err KOccursCheckFailed
adamc@2 105 else
adamc@2 106 r := SOME k1All
adamc@2 107
adamc@2 108 | _ => err KIncompatible
adamc@2 109 end
adamc@2 110
adamc@3 111 exception KUnify of L'.kind * L'.kind * kunify_error
adamc@3 112
adamc@3 113 fun unifyKinds k1 k2 =
adamc@3 114 unifyKinds' k1 k2
adamc@3 115 handle KUnify' err => raise KUnify (k1, k2, err)
adamc@3 116
adamc@3 117 datatype con_error =
adamc@3 118 UnboundCon of ErrorMsg.span * string
adamc@34 119 | UnboundStrInCon of ErrorMsg.span * string
adamc@3 120 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
adamc@67 121 | DuplicateField of ErrorMsg.span * string
adamc@3 122
adamc@5 123 fun conError env err =
adamc@3 124 case err of
adamc@3 125 UnboundCon (loc, s) =>
adamc@3 126 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
adamc@34 127 | UnboundStrInCon (loc, s) =>
adamc@34 128 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adamc@3 129 | WrongKind (c, k1, k2, kerr) =>
adamc@3 130 (ErrorMsg.errorAt (#2 c) "Wrong kind";
adamc@5 131 eprefaces' [("Constructor", p_con env c),
adamc@5 132 ("Have kind", p_kind k1),
adamc@5 133 ("Need kind", p_kind k2)];
adamc@3 134 kunifyError kerr)
adamc@67 135 | DuplicateField (loc, s) =>
adamc@67 136 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
adamc@3 137
adamc@5 138 fun checkKind env c k1 k2 =
adamc@3 139 unifyKinds k1 k2
adamc@3 140 handle KUnify (k1, k2, err) =>
adamc@5 141 conError env (WrongKind (c, k1, k2, err))
adamc@3 142
adamc@3 143 val dummy = ErrorMsg.dummySpan
adamc@3 144
adamc@3 145 val ktype = (L'.KType, dummy)
adamc@3 146 val kname = (L'.KName, dummy)
adamc@12 147 val ktype_record = (L'.KRecord ktype, dummy)
adamc@3 148
adamc@3 149 val cerror = (L'.CError, dummy)
adamc@3 150 val kerror = (L'.KError, dummy)
adamc@10 151 val eerror = (L'.EError, dummy)
adamc@31 152 val sgnerror = (L'.SgnError, dummy)
adamc@31 153 val strerror = (L'.StrError, dummy)
adamc@3 154
adamc@56 155 val int = ref cerror
adamc@56 156 val float = ref cerror
adamc@56 157 val string = ref cerror
adamc@56 158
adamc@3 159 local
adamc@3 160 val count = ref 0
adamc@3 161 in
adamc@3 162
adamc@3 163 fun resetKunif () = count := 0
adamc@3 164
adamc@76 165 fun kunif loc =
adamc@3 166 let
adamc@3 167 val n = !count
adamc@3 168 val s = if n <= 26 then
adamc@3 169 str (chr (ord #"A" + n))
adamc@3 170 else
adamc@3 171 "U" ^ Int.toString (n - 26)
adamc@3 172 in
adamc@3 173 count := n + 1;
adamc@76 174 (L'.KUnif (loc, s, ref NONE), dummy)
adamc@3 175 end
adamc@3 176
adamc@3 177 end
adamc@3 178
adamc@10 179 local
adamc@10 180 val count = ref 0
adamc@10 181 in
adamc@10 182
adamc@10 183 fun resetCunif () = count := 0
adamc@10 184
adamc@76 185 fun cunif (loc, k) =
adamc@10 186 let
adamc@10 187 val n = !count
adamc@10 188 val s = if n <= 26 then
adamc@10 189 str (chr (ord #"A" + n))
adamc@10 190 else
adamc@10 191 "U" ^ Int.toString (n - 26)
adamc@10 192 in
adamc@10 193 count := n + 1;
adamc@76 194 (L'.CUnif (loc, k, s, ref NONE), dummy)
adamc@10 195 end
adamc@10 196
adamc@10 197 end
adamc@10 198
adamc@18 199 fun elabKind (k, loc) =
adamc@18 200 case k of
adamc@18 201 L.KType => (L'.KType, loc)
adamc@18 202 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
adamc@18 203 | L.KName => (L'.KName, loc)
adamc@18 204 | L.KRecord k => (L'.KRecord (elabKind k), loc)
adamc@82 205 | L.KUnit => (L'.KUnit, loc)
adamc@76 206 | L.KWild => kunif loc
adamc@18 207
adamc@67 208 fun foldKind (dom, ran, loc)=
adamc@67 209 (L'.KArrow ((L'.KArrow ((L'.KName, loc),
adamc@67 210 (L'.KArrow (dom,
adamc@67 211 (L'.KArrow (ran, ran), loc)), loc)), loc),
adamc@67 212 (L'.KArrow (ran,
adamc@67 213 (L'.KArrow ((L'.KRecord dom, loc),
adamc@67 214 ran), loc)), loc)), loc)
adamc@67 215
adamc@83 216 fun elabCon (env, denv) (c, loc) =
adamc@3 217 case c of
adamc@3 218 L.CAnnot (c, k) =>
adamc@3 219 let
adamc@3 220 val k' = elabKind k
adamc@83 221 val (c', ck, gs) = elabCon (env, denv) c
adamc@3 222 in
adamc@5 223 checkKind env c' ck k';
adamc@83 224 (c', k', gs)
adamc@3 225 end
adamc@3 226
adamc@3 227 | L.TFun (t1, t2) =>
adamc@3 228 let
adamc@83 229 val (t1', k1, gs1) = elabCon (env, denv) t1
adamc@83 230 val (t2', k2, gs2) = elabCon (env, denv) t2
adamc@3 231 in
adamc@5 232 checkKind env t1' k1 ktype;
adamc@5 233 checkKind env t2' k2 ktype;
adamc@83 234 ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2)
adamc@3 235 end
adamc@3 236 | L.TCFun (e, x, k, t) =>
adamc@3 237 let
adamc@3 238 val e' = elabExplicitness e
adamc@3 239 val k' = elabKind k
adamc@3 240 val env' = E.pushCRel env x k'
adamc@83 241 val (t', tk, gs) = elabCon (env', D.enter denv) t
adamc@3 242 in
adamc@5 243 checkKind env t' tk ktype;
adamc@83 244 ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
adamc@3 245 end
adamc@85 246 | L.TDisjoint (c1, c2, c) =>
adamc@85 247 let
adamc@85 248 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@85 249 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@85 250
adamc@85 251 val ku1 = kunif loc
adamc@85 252 val ku2 = kunif loc
adamc@85 253
adamc@90 254 val (denv', gs3) = D.assert env denv (c1', c2')
adamc@90 255 val (c', k, gs4) = elabCon (env, denv') c
adamc@85 256 in
adamc@85 257 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@85 258 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@85 259
adamc@90 260 ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
adamc@85 261 end
adamc@3 262 | L.TRecord c =>
adamc@3 263 let
adamc@83 264 val (c', ck, gs) = elabCon (env, denv) c
adamc@3 265 val k = (L'.KRecord ktype, loc)
adamc@3 266 in
adamc@5 267 checkKind env c' ck k;
adamc@83 268 ((L'.TRecord c', loc), ktype, gs)
adamc@3 269 end
adamc@3 270
adamc@34 271 | L.CVar ([], s) =>
adamc@3 272 (case E.lookupC env s of
adamc@9 273 E.NotBound =>
adamc@5 274 (conError env (UnboundCon (loc, s));
adamc@83 275 (cerror, kerror, []))
adamc@9 276 | E.Rel (n, k) =>
adamc@83 277 ((L'.CRel n, loc), k, [])
adamc@9 278 | E.Named (n, k) =>
adamc@83 279 ((L'.CNamed n, loc), k, []))
adamc@34 280 | L.CVar (m1 :: ms, s) =>
adamc@34 281 (case E.lookupStr env m1 of
adamc@42 282 NONE => (conError env (UnboundStrInCon (loc, m1));
adamc@83 283 (cerror, kerror, []))
adamc@34 284 | SOME (n, sgn) =>
adamc@34 285 let
adamc@34 286 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@34 287 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@34 288 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@34 289 (strerror, sgnerror))
adamc@34 290 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@34 291 ((L'.StrVar n, loc), sgn) ms
adamc@34 292
adamc@34 293 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
adamc@34 294 NONE => (conError env (UnboundCon (loc, s));
adamc@34 295 kerror)
adamc@34 296 | SOME (k, _) => k
adamc@34 297 in
adamc@83 298 ((L'.CModProj (n, ms, s), loc), k, [])
adamc@34 299 end)
adamc@34 300
adamc@3 301 | L.CApp (c1, c2) =>
adamc@3 302 let
adamc@83 303 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@83 304 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@76 305 val dom = kunif loc
adamc@76 306 val ran = kunif loc
adamc@3 307 in
adamc@5 308 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
adamc@5 309 checkKind env c2' k2 dom;
adamc@83 310 ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2)
adamc@3 311 end
adamc@67 312 | L.CAbs (x, ko, t) =>
adamc@3 313 let
adamc@67 314 val k' = case ko of
adamc@76 315 NONE => kunif loc
adamc@67 316 | SOME k => elabKind k
adamc@3 317 val env' = E.pushCRel env x k'
adamc@83 318 val (t', tk, gs) = elabCon (env', D.enter denv) t
adamc@3 319 in
adamc@8 320 ((L'.CAbs (x, k', t'), loc),
adamc@83 321 (L'.KArrow (k', tk), loc),
adamc@83 322 gs)
adamc@3 323 end
adamc@3 324
adamc@84 325 | L.CDisjoint (c1, c2, c) =>
adamc@84 326 let
adamc@84 327 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@84 328 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@84 329
adamc@84 330 val ku1 = kunif loc
adamc@84 331 val ku2 = kunif loc
adamc@84 332
adamc@90 333 val (denv', gs3) = D.assert env denv (c1', c2')
adamc@90 334 val (c', k, gs4) = elabCon (env, denv') c
adamc@84 335 in
adamc@84 336 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@84 337 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@84 338
adamc@90 339 ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
adamc@84 340 end
adamc@84 341
adamc@3 342 | L.CName s =>
adamc@83 343 ((L'.CName s, loc), kname, [])
adamc@3 344
adamc@3 345 | L.CRecord xcs =>
adamc@3 346 let
adamc@76 347 val k = kunif loc
adamc@3 348
adamc@83 349 val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
adamc@83 350 let
adamc@83 351 val (x', xk, gs1) = elabCon (env, denv) x
adamc@83 352 val (c', ck, gs2) = elabCon (env, denv) c
adamc@83 353 in
adamc@83 354 checkKind env x' xk kname;
adamc@83 355 checkKind env c' ck k;
adamc@83 356 ((x', c'), gs1 @ gs2 @ gs)
adamc@83 357 end) [] xcs
adamc@67 358
adamc@67 359 val rc = (L'.CRecord (k, xcs'), loc)
adamc@67 360 (* Add duplicate field checking later. *)
adamc@83 361
adamc@83 362 fun prove (xcs, ds) =
adamc@83 363 case xcs of
adamc@83 364 [] => ds
adamc@83 365 | xc :: rest =>
adamc@83 366 let
adamc@83 367 val r1 = (L'.CRecord (k, [xc]), loc)
adamc@83 368 val ds = foldl (fn (xc', ds) =>
adamc@83 369 let
adamc@83 370 val r2 = (L'.CRecord (k, [xc']), loc)
adamc@83 371 in
adamc@90 372 D.prove env denv (r1, r2, loc) @ ds
adamc@83 373 end)
adamc@83 374 ds rest
adamc@83 375 in
adamc@83 376 prove (rest, ds)
adamc@83 377 end
adamc@3 378 in
adamc@83 379 (rc, (L'.KRecord k, loc), prove (xcs', gs))
adamc@3 380 end
adamc@3 381 | L.CConcat (c1, c2) =>
adamc@3 382 let
adamc@83 383 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@83 384 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@76 385 val ku = kunif loc
adamc@3 386 val k = (L'.KRecord ku, loc)
adamc@3 387 in
adamc@5 388 checkKind env c1' k1 k;
adamc@5 389 checkKind env c2' k2 k;
adamc@83 390 ((L'.CConcat (c1', c2'), loc), k,
adamc@90 391 D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
adamc@3 392 end
adamc@67 393 | L.CFold =>
adamc@67 394 let
adamc@76 395 val dom = kunif loc
adamc@76 396 val ran = kunif loc
adamc@67 397 in
adamc@67 398 ((L'.CFold (dom, ran), loc),
adamc@83 399 foldKind (dom, ran, loc),
adamc@83 400 [])
adamc@67 401 end
adamc@3 402
adamc@83 403 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
adamc@82 404
adamc@18 405 | L.CWild k =>
adamc@18 406 let
adamc@18 407 val k' = elabKind k
adamc@18 408 in
adamc@83 409 (cunif (loc, k'), k', [])
adamc@18 410 end
adamc@18 411
adamc@6 412 fun kunifsRemain k =
adamc@6 413 case k of
adamc@76 414 L'.KUnif (_, _, ref NONE) => true
adamc@6 415 | _ => false
adamc@10 416 fun cunifsRemain c =
adamc@10 417 case c of
adamc@76 418 L'.CUnif (loc, _, _, ref NONE) => SOME loc
adamc@76 419 | _ => NONE
adamc@6 420
adamc@76 421 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
adamc@76 422 con = fn _ => false,
adamc@76 423 exp = fn _ => false,
adamc@76 424 sgn_item = fn _ => false,
adamc@76 425 sgn = fn _ => false,
adamc@76 426 str = fn _ => false,
adamc@76 427 decl = fn _ => false}
adamc@10 428
adamc@76 429 val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
adamc@76 430 con = cunifsRemain,
adamc@76 431 exp = fn _ => NONE,
adamc@76 432 sgn_item = fn _ => NONE,
adamc@76 433 sgn = fn _ => NONE,
adamc@76 434 str = fn _ => NONE,
adamc@76 435 decl = fn _ => NONE}
adamc@10 436
adamc@10 437 fun occursCon r =
adamc@10 438 U.Con.exists {kind = fn _ => false,
adamc@76 439 con = fn L'.CUnif (_, _, _, r') => r = r'
adamc@10 440 | _ => false}
adamc@10 441
adamc@10 442 datatype cunify_error =
adamc@10 443 CKind of L'.kind * L'.kind * kunify_error
adamc@10 444 | COccursCheckFailed of L'.con * L'.con
adamc@10 445 | CIncompatible of L'.con * L'.con
adamc@10 446 | CExplicitness of L'.con * L'.con
adamc@12 447 | CKindof of L'.con
adamc@12 448 | CRecordFailure
adamc@10 449
adamc@10 450 exception CUnify' of cunify_error
adamc@10 451
adamc@10 452 fun cunifyError env err =
adamc@10 453 case err of
adamc@10 454 CKind (k1, k2, kerr) =>
adamc@10 455 (eprefaces "Kind unification failure"
adamc@10 456 [("Kind 1", p_kind k1),
adamc@10 457 ("Kind 2", p_kind k2)];
adamc@10 458 kunifyError kerr)
adamc@10 459 | COccursCheckFailed (c1, c2) =>
adamc@10 460 eprefaces "Constructor occurs check failed"
adamc@10 461 [("Con 1", p_con env c1),
adamc@10 462 ("Con 2", p_con env c2)]
adamc@10 463 | CIncompatible (c1, c2) =>
adamc@10 464 eprefaces "Incompatible constructors"
adamc@10 465 [("Con 1", p_con env c1),
adamc@10 466 ("Con 2", p_con env c2)]
adamc@10 467 | CExplicitness (c1, c2) =>
adamc@10 468 eprefaces "Differing constructor function explicitness"
adamc@10 469 [("Con 1", p_con env c1),
adamc@10 470 ("Con 2", p_con env c2)]
adamc@12 471 | CKindof c =>
adamc@12 472 eprefaces "Kind unification variable blocks kindof calculation"
adamc@12 473 [("Con", p_con env c)]
adamc@12 474 | CRecordFailure =>
adamc@12 475 eprefaces "Can't unify record constructors" []
adamc@10 476
adamc@13 477 exception SynUnif = E.SynUnif
adamc@12 478
adamc@81 479 open ElabOps
adamc@43 480
adamc@12 481 type record_summary = {
adamc@12 482 fields : (L'.con * L'.con) list,
adamc@12 483 unifs : (L'.con * L'.con option ref) list,
adamc@12 484 others : L'.con list
adamc@12 485 }
adamc@12 486
adamc@12 487 fun summaryToCon {fields, unifs, others} =
adamc@12 488 let
adamc@12 489 val c = (L'.CRecord (ktype, []), dummy)
adamc@12 490 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
adamc@12 491 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
adamc@12 492 in
adamc@12 493 (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
adamc@12 494 end
adamc@12 495
adamc@12 496 fun p_summary env s = p_con env (summaryToCon s)
adamc@12 497
adamc@12 498 exception CUnify of L'.con * L'.con * cunify_error
adamc@12 499
adamc@12 500 fun hnormKind (kAll as (k, _)) =
adamc@12 501 case k of
adamc@76 502 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
adamc@12 503 | _ => kAll
adamc@12 504
adamc@12 505 fun kindof env (c, loc) =
adamc@12 506 case c of
adamc@12 507 L'.TFun _ => ktype
adamc@12 508 | L'.TCFun _ => ktype
adamc@85 509 | L'.TDisjoint _ => ktype
adamc@12 510 | L'.TRecord _ => ktype
adamc@12 511
adamc@12 512 | L'.CRel xn => #2 (E.lookupCRel env xn)
adamc@12 513 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
adamc@34 514 | L'.CModProj (n, ms, x) =>
adamc@34 515 let
adamc@34 516 val (_, sgn) = E.lookupStrNamed env n
adamc@34 517 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@34 518 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@34 519 NONE => raise Fail "kindof: Unknown substructure"
adamc@34 520 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@34 521 ((L'.StrVar n, loc), sgn) ms
adamc@34 522 in
adamc@34 523 case E.projectCon env {sgn = sgn, str = str, field = x} of
adamc@34 524 NONE => raise Fail "kindof: Unknown con in structure"
adamc@34 525 | SOME (k, _) => k
adamc@34 526 end
adamc@34 527
adamc@12 528 | L'.CApp (c, _) =>
adamc@12 529 (case #1 (hnormKind (kindof env c)) of
adamc@12 530 L'.KArrow (_, k) => k
adamc@12 531 | L'.KError => kerror
adamc@12 532 | _ => raise CUnify' (CKindof c))
adamc@12 533 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
adamc@84 534 | L'.CDisjoint (_, _, c) => kindof env c
adamc@12 535
adamc@12 536 | L'.CName _ => kname
adamc@12 537
adamc@12 538 | L'.CRecord (k, _) => (L'.KRecord k, loc)
adamc@12 539 | L'.CConcat (c, _) => kindof env c
adamc@67 540 | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
adamc@12 541
adamc@82 542 | L'.CUnit => (L'.KUnit, loc)
adamc@82 543
adamc@12 544 | L'.CError => kerror
adamc@76 545 | L'.CUnif (_, k, _, _) => k
adamc@12 546
adamc@90 547 val hnormCon = D.hnormCon
adamc@86 548
adamc@86 549 fun unifyRecordCons (env, denv) (c1, c2) =
adamc@12 550 let
adamc@92 551 fun rkindof c =
adamc@92 552 case kindof env c of
adamc@92 553 (L'.KRecord k, _) => k
adamc@92 554 | _ => raise CUnify' (CKindof c)
adamc@92 555
adamc@92 556 val k1 = rkindof c1
adamc@92 557 val k2 = rkindof c2
adamc@86 558
adamc@86 559 val (r1, gs1) = recordSummary (env, denv) c1
adamc@86 560 val (r2, gs2) = recordSummary (env, denv) c2
adamc@12 561 in
adamc@12 562 unifyKinds k1 k2;
adamc@86 563 unifySummaries (env, denv) (k1, r1, r2);
adamc@86 564 gs1 @ gs2
adamc@12 565 end
adamc@12 566
adamc@86 567 and recordSummary (env, denv) c =
adamc@86 568 let
adamc@86 569 val (c, gs) = hnormCon (env, denv) c
adamc@12 570
adamc@86 571 val (sum, gs') =
adamc@86 572 case c of
adamc@86 573 (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, [])
adamc@86 574 | (L'.CConcat (c1, c2), _) =>
adamc@86 575 let
adamc@86 576 val (s1, gs1) = recordSummary (env, denv) c1
adamc@86 577 val (s2, gs2) = recordSummary (env, denv) c2
adamc@86 578 in
adamc@86 579 ({fields = #fields s1 @ #fields s2,
adamc@86 580 unifs = #unifs s1 @ #unifs s2,
adamc@86 581 others = #others s1 @ #others s2},
adamc@86 582 gs1 @ gs2)
adamc@86 583 end
adamc@86 584 | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c
adamc@86 585 | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, [])
adamc@86 586 | c' => ({fields = [], unifs = [], others = [c']}, [])
adamc@86 587 in
adamc@86 588 (sum, gs @ gs')
adamc@86 589 end
adamc@86 590
adamc@86 591 and consEq (env, denv) (c1, c2) =
adamc@86 592 (case unifyCons (env, denv) c1 c2 of
adamc@86 593 [] => true
adamc@86 594 | _ => false)
adamc@12 595 handle CUnify _ => false
adamc@12 596
adamc@80 597 and consNeq env (c1, c2) =
adamc@86 598 case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of
adamc@80 599 (L'.CName x1, L'.CName x2) => x1 <> x2
adamc@80 600 | _ => false
adamc@80 601
adamc@86 602 and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
adamc@12 603 let
adamc@14 604 (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
adamc@14 605 ("#2", p_summary env s2)]*)
adamc@12 606
adamc@12 607 fun eatMatching p (ls1, ls2) =
adamc@12 608 let
adamc@12 609 fun em (ls1, ls2, passed1) =
adamc@12 610 case ls1 of
adamc@12 611 [] => (rev passed1, ls2)
adamc@12 612 | h1 :: t1 =>
adamc@12 613 let
adamc@12 614 fun search (ls2', passed2) =
adamc@12 615 case ls2' of
adamc@12 616 [] => em (t1, ls2, h1 :: passed1)
adamc@12 617 | h2 :: t2 =>
adamc@12 618 if p (h1, h2) then
adamc@12 619 em (t1, List.revAppend (passed2, t2), passed1)
adamc@12 620 else
adamc@12 621 search (t2, h2 :: passed2)
adamc@12 622 in
adamc@12 623 search (ls2, [])
adamc@12 624 end
adamc@12 625 in
adamc@12 626 em (ls1, ls2, [])
adamc@12 627 end
adamc@12 628
adamc@12 629 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
adamc@80 630 not (consNeq env (x1, x2))
adamc@86 631 andalso consEq (env, denv) (c1, c2)
adamc@86 632 andalso consEq (env, denv) (x1, x2))
adamc@79 633 (#fields s1, #fields s2)
adamc@14 634 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
adamc@14 635 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
adamc@12 636 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
adamc@86 637 val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2)
adamc@12 638
adamc@12 639 fun unifFields (fs, others, unifs) =
adamc@12 640 case (fs, others, unifs) of
adamc@12 641 ([], [], _) => ([], [], unifs)
adamc@12 642 | (_, _, []) => (fs, others, [])
adamc@12 643 | (_, _, (_, r) :: rest) =>
adamc@12 644 let
adamc@12 645 val r' = ref NONE
adamc@76 646 val cr' = (L'.CUnif (dummy, k, "recd", r'), dummy)
adamc@12 647
adamc@12 648 val prefix = case (fs, others) of
adamc@12 649 ([], other :: others) =>
adamc@12 650 List.foldl (fn (other, c) =>
adamc@12 651 (L'.CConcat (c, other), dummy))
adamc@12 652 other others
adamc@12 653 | (fs, []) =>
adamc@12 654 (L'.CRecord (k, fs), dummy)
adamc@12 655 | (fs, others) =>
adamc@12 656 List.foldl (fn (other, c) =>
adamc@12 657 (L'.CConcat (c, other), dummy))
adamc@12 658 (L'.CRecord (k, fs), dummy) others
adamc@12 659 in
adamc@12 660 r := SOME (L'.CConcat (prefix, cr'), dummy);
adamc@12 661 ([], [], (cr', r') :: rest)
adamc@12 662 end
adamc@12 663
adamc@12 664 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
adamc@12 665 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
adamc@12 666
adamc@86 667 val clear = case (fs1, others1, fs2, others2) of
adamc@86 668 ([], [], [], []) => true
adamc@12 669 | _ => false
adamc@12 670 val empty = (L'.CRecord (k, []), dummy)
adamc@12 671 fun pairOffUnifs (unifs1, unifs2) =
adamc@12 672 case (unifs1, unifs2) of
adamc@12 673 ([], _) =>
adamc@86 674 if clear then
adamc@12 675 List.app (fn (_, r) => r := SOME empty) unifs2
adamc@12 676 else
adamc@12 677 raise CUnify' CRecordFailure
adamc@12 678 | (_, []) =>
adamc@86 679 if clear then
adamc@12 680 List.app (fn (_, r) => r := SOME empty) unifs1
adamc@12 681 else
adamc@12 682 raise CUnify' CRecordFailure
adamc@12 683 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
adamc@12 684 (r2 := SOME c1;
adamc@12 685 pairOffUnifs (rest1, rest2))
adamc@12 686 in
adamc@12 687 pairOffUnifs (unifs1, unifs2)
adamc@12 688 end
adamc@12 689
adamc@86 690 and unifyCons' (env, denv) c1 c2 =
adamc@86 691 let
adamc@86 692 val (c1, gs1) = hnormCon (env, denv) c1
adamc@86 693 val (c2, gs2) = hnormCon (env, denv) c2
adamc@90 694 val gs3 = unifyCons'' (env, denv) c1 c2
adamc@86 695 in
adamc@90 696 gs1 @ gs2 @ gs3
adamc@86 697 end
adamc@11 698
adamc@86 699 and unifyCons'' (env, denv) (c1All as (c1, _)) (c2All as (c2, _)) =
adamc@10 700 let
adamc@10 701 fun err f = raise CUnify' (f (c1All, c2All))
adamc@12 702
adamc@86 703 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
adamc@10 704 in
adamc@92 705 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
adamc@92 706 ("c2All", p_con env c2All)];*)
adamc@92 707
adamc@10 708 case (c1, c2) of
adamc@88 709 (L'.CUnit, L'.CUnit) => []
adamc@88 710
adamc@88 711 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
adamc@86 712 unifyCons' (env, denv) d1 d2
adamc@86 713 @ unifyCons' (env, denv) r1 r2
adamc@10 714 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
adamc@10 715 if expl1 <> expl2 then
adamc@10 716 err CExplicitness
adamc@10 717 else
adamc@10 718 (unifyKinds d1 d2;
adamc@86 719 unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2)
adamc@86 720 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2
adamc@10 721
adamc@10 722 | (L'.CRel n1, L'.CRel n2) =>
adamc@10 723 if n1 = n2 then
adamc@86 724 []
adamc@10 725 else
adamc@10 726 err CIncompatible
adamc@10 727 | (L'.CNamed n1, L'.CNamed n2) =>
adamc@10 728 if n1 = n2 then
adamc@86 729 []
adamc@10 730 else
adamc@10 731 err CIncompatible
adamc@10 732
adamc@10 733 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
adamc@86 734 (unifyCons' (env, denv) d1 d2;
adamc@86 735 unifyCons' (env, denv) r1 r2)
adamc@10 736 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
adamc@10 737 (unifyKinds k1 k2;
adamc@86 738 unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
adamc@10 739
adamc@10 740 | (L'.CName n1, L'.CName n2) =>
adamc@10 741 if n1 = n2 then
adamc@86 742 []
adamc@10 743 else
adamc@10 744 err CIncompatible
adamc@10 745
adamc@34 746 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
adamc@34 747 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
adamc@86 748 []
adamc@34 749 else
adamc@34 750 err CIncompatible
adamc@34 751
adamc@86 752 | (L'.CError, _) => []
adamc@86 753 | (_, L'.CError) => []
adamc@10 754
adamc@92 755 | (L'.CRecord _, _) => isRecord ()
adamc@92 756 | (_, L'.CRecord _) => isRecord ()
adamc@92 757 | (L'.CConcat _, _) => isRecord ()
adamc@92 758 | (_, L'.CConcat _) => isRecord ()
adamc@92 759 (*| (L'.CUnif (_, (L'.KRecord _, _), _, _), _) => isRecord ()
adamc@92 760 | (_, L'.CUnif (_, (L'.KRecord _, _), _, _)) => isRecord ()*)
adamc@10 761
adamc@76 762 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
adamc@10 763 if r1 = r2 then
adamc@86 764 []
adamc@10 765 else
adamc@10 766 (unifyKinds k1 k2;
adamc@86 767 r1 := SOME c2All;
adamc@86 768 [])
adamc@10 769
adamc@76 770 | (L'.CUnif (_, _, _, r), _) =>
adamc@10 771 if occursCon r c2All then
adamc@10 772 err COccursCheckFailed
adamc@10 773 else
adamc@86 774 (r := SOME c2All;
adamc@86 775 [])
adamc@76 776 | (_, L'.CUnif (_, _, _, r)) =>
adamc@10 777 if occursCon r c1All then
adamc@10 778 err COccursCheckFailed
adamc@10 779 else
adamc@86 780 (r := SOME c1All;
adamc@86 781 [])
adamc@10 782
adamc@12 783
adamc@71 784 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
adamc@71 785 (unifyKinds dom1 dom2;
adamc@86 786 unifyKinds ran1 ran2;
adamc@86 787 [])
adamc@71 788
adamc@10 789 | _ => err CIncompatible
adamc@10 790 end
adamc@10 791
adamc@86 792 and unifyCons (env, denv) c1 c2 =
adamc@86 793 unifyCons' (env, denv) c1 c2
adamc@10 794 handle CUnify' err => raise CUnify (c1, c2, err)
adamc@10 795 | KUnify args => raise CUnify (c1, c2, CKind args)
adamc@10 796
adamc@10 797 datatype exp_error =
adamc@10 798 UnboundExp of ErrorMsg.span * string
adamc@34 799 | UnboundStrInExp of ErrorMsg.span * string
adamc@10 800 | Unify of L'.exp * L'.con * L'.con * cunify_error
adamc@11 801 | Unif of string * L'.con
adamc@11 802 | WrongForm of string * L'.exp * L'.con
adamc@92 803 | IncompatibleCons of L'.con * L'.con
adamc@10 804
adamc@10 805 fun expError env err =
adamc@10 806 case err of
adamc@10 807 UnboundExp (loc, s) =>
adamc@10 808 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
adamc@34 809 | UnboundStrInExp (loc, s) =>
adamc@34 810 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adamc@10 811 | Unify (e, c1, c2, uerr) =>
adamc@10 812 (ErrorMsg.errorAt (#2 e) "Unification failure";
adamc@10 813 eprefaces' [("Expression", p_exp env e),
adamc@10 814 ("Have con", p_con env c1),
adamc@10 815 ("Need con", p_con env c2)];
adamc@10 816 cunifyError env uerr)
adamc@11 817 | Unif (action, c) =>
adamc@11 818 (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action);
adamc@11 819 eprefaces' [("Con", p_con env c)])
adamc@11 820 | WrongForm (variety, e, t) =>
adamc@11 821 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
adamc@11 822 eprefaces' [("Expression", p_exp env e),
adamc@11 823 ("Type", p_con env t)])
adamc@92 824 | IncompatibleCons (c1, c2) =>
adamc@92 825 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
adamc@92 826 eprefaces' [("Con 1", p_con env c1),
adamc@92 827 ("Con 2", p_con env c2)])
adamc@10 828
adamc@86 829 fun checkCon (env, denv) e c1 c2 =
adamc@86 830 unifyCons (env, denv) c1 c2
adamc@10 831 handle CUnify (c1, c2, err) =>
adamc@86 832 (expError env (Unify (e, c1, c2, err));
adamc@86 833 [])
adamc@10 834
adamc@14 835 fun primType env p =
adamc@56 836 case p of
adamc@56 837 P.Int _ => !int
adamc@56 838 | P.Float _ => !float
adamc@56 839 | P.String _ => !string
adamc@14 840
adamc@71 841 fun recCons (k, nm, v, rest, loc) =
adamc@71 842 (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
adamc@71 843 rest), loc)
adamc@71 844
adamc@71 845 fun foldType (dom, loc) =
adamc@71 846 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
adamc@71 847 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
adamc@71 848 (L'.TCFun (L'.Explicit, "v", dom,
adamc@71 849 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
adamc@71 850 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
adamc@71 851 (L'.CApp ((L'.CRel 3, loc),
adamc@71 852 recCons (dom,
adamc@71 853 (L'.CRel 2, loc),
adamc@71 854 (L'.CRel 1, loc),
adamc@71 855 (L'.CRel 0, loc),
adamc@71 856 loc)), loc)), loc)),
adamc@71 857 loc)), loc)), loc),
adamc@71 858 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
adamc@71 859 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
adamc@71 860 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
adamc@71 861 loc)), loc)), loc)
adamc@71 862
adamc@15 863 fun typeof env (e, loc) =
adamc@15 864 case e of
adamc@56 865 L'.EPrim p => primType env p
adamc@15 866 | L'.ERel n => #2 (E.lookupERel env n)
adamc@15 867 | L'.ENamed n => #2 (E.lookupENamed env n)
adamc@34 868 | L'.EModProj (n, ms, x) =>
adamc@34 869 let
adamc@34 870 val (_, sgn) = E.lookupStrNamed env n
adamc@34 871 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@34 872 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@34 873 NONE => raise Fail "kindof: Unknown substructure"
adamc@34 874 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@34 875 ((L'.StrVar n, loc), sgn) ms
adamc@34 876 in
adamc@34 877 case E.projectVal env {sgn = sgn, str = str, field = x} of
adamc@34 878 NONE => raise Fail "typeof: Unknown val in structure"
adamc@34 879 | SOME t => t
adamc@34 880 end
adamc@34 881
adamc@15 882 | L'.EApp (e1, _) =>
adamc@15 883 (case #1 (typeof env e1) of
adamc@15 884 L'.TFun (_, c) => c
adamc@15 885 | _ => raise Fail "typeof: Bad EApp")
adamc@26 886 | L'.EAbs (_, _, ran, _) => ran
adamc@15 887 | L'.ECApp (e1, c) =>
adamc@15 888 (case #1 (typeof env e1) of
adamc@15 889 L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1
adamc@15 890 | _ => raise Fail "typeof: Bad ECApp")
adamc@15 891 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc)
adamc@15 892
adamc@29 893 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc)
adamc@15 894 | L'.EField (_, _, {field, ...}) => field
adamc@71 895 | L'.EFold dom => foldType (dom, loc)
adamc@15 896
adamc@15 897 | L'.EError => cerror
adamc@15 898
adamc@86 899 fun elabHead (env, denv) (e as (_, loc)) t =
adamc@15 900 let
adamc@15 901 fun unravel (t, e) =
adamc@86 902 let
adamc@86 903 val (t, gs) = hnormCon (env, denv) t
adamc@86 904 in
adamc@86 905 case t of
adamc@86 906 (L'.TCFun (L'.Implicit, x, k, t'), _) =>
adamc@86 907 let
adamc@86 908 val u = cunif (loc, k)
adamc@86 909
adamc@86 910 val (e, t, gs') = unravel (subConInCon (0, u) t',
adamc@86 911 (L'.ECApp (e, u), loc))
adamc@86 912 in
adamc@86 913 (e, t, gs @ gs')
adamc@86 914 end
adamc@86 915 | _ => (e, t, gs)
adamc@86 916 end
adamc@15 917 in
adamc@15 918 unravel (t, e)
adamc@15 919 end
adamc@15 920
adamc@92 921 fun elabExp (env, denv) (eAll as (e, loc)) =
adamc@91 922 let
adamc@92 923
adamc@92 924 in
adamc@92 925 (*eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
adamc@10 926
adamc@91 927 case e of
adamc@91 928 L.EAnnot (e, t) =>
adamc@91 929 let
adamc@91 930 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 931 val (t', _, gs2) = elabCon (env, denv) t
adamc@91 932 val gs3 = checkCon (env, denv) e' et t'
adamc@91 933 in
adamc@91 934 (e', t', gs1 @ gs2 @ gs3)
adamc@91 935 end
adamc@34 936
adamc@91 937 | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
adamc@91 938 | L.EVar ([], s) =>
adamc@91 939 (case E.lookupE env s of
adamc@91 940 E.NotBound =>
adamc@91 941 (expError env (UnboundExp (loc, s));
adamc@91 942 (eerror, cerror, []))
adamc@91 943 | E.Rel (n, t) => ((L'.ERel n, loc), t, [])
adamc@91 944 | E.Named (n, t) => ((L'.ENamed n, loc), t, []))
adamc@91 945 | L.EVar (m1 :: ms, s) =>
adamc@91 946 (case E.lookupStr env m1 of
adamc@91 947 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@91 948 (eerror, cerror, []))
adamc@91 949 | SOME (n, sgn) =>
adamc@91 950 let
adamc@91 951 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@91 952 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@91 953 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@91 954 (strerror, sgnerror))
adamc@91 955 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@91 956 ((L'.StrVar n, loc), sgn) ms
adamc@10 957
adamc@91 958 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
adamc@91 959 NONE => (expError env (UnboundExp (loc, s));
adamc@91 960 cerror)
adamc@91 961 | SOME t => t
adamc@91 962 in
adamc@91 963 ((L'.EModProj (n, ms, s), loc), t, [])
adamc@91 964 end)
adamc@86 965
adamc@91 966 | L.EApp (arg as ((L.EApp ((L.ECApp ((L.EVar (["Basis"], "join"), _), (L.CWild _, _)), _), xml1), _), xml2)) =>
adamc@91 967 let
adamc@91 968 val (xml1', t1, gs1) = elabExp (env, denv) xml1
adamc@91 969 val (xml2', t2, gs2) = elabExp (env, denv) xml2
adamc@11 970
adamc@91 971 val kunit = (L'.KUnit, loc)
adamc@91 972 val k = (L'.KRecord kunit, loc)
adamc@11 973
adamc@91 974 val basis =
adamc@91 975 case E.lookupStr env "Basis" of
adamc@91 976 NONE => raise Fail "elabExp: Unbound Basis"
adamc@91 977 | SOME (n, _) => n
adamc@6 978
adamc@91 979 fun xml () =
adamc@91 980 let
adamc@91 981 val ns = cunif (loc, k)
adamc@91 982 in
adamc@91 983 (ns, (L'.CApp ((L'.CModProj (basis, [], "xml"), loc), ns), loc))
adamc@91 984 end
adamc@85 985
adamc@91 986 val (ns1, c1) = xml ()
adamc@91 987 val (ns2, c2) = xml ()
adamc@85 988
adamc@91 989 val gs3 = checkCon (env, denv) xml1' t1 c1
adamc@91 990 val gs4 = checkCon (env, denv) xml2' t2 c2
adamc@85 991
adamc@91 992 val (ns1, gs5) = hnormCon (env, denv) ns1
adamc@91 993 val (ns2, gs6) = hnormCon (env, denv) ns2
adamc@85 994
adamc@91 995 val cemp = (L'.CRecord (kunit, []), loc)
adamc@86 996
adamc@91 997 val (shared, ctx1, ctx2) =
adamc@91 998 case (#1 ns1, #1 ns2) of
adamc@91 999 (L'.CRecord (_, ns1), L'.CRecord (_, ns2)) =>
adamc@91 1000 let
adamc@91 1001 val ns = List.filter (fn ((nm, _), _) =>
adamc@91 1002 case nm of
adamc@91 1003 L'.CName s =>
adamc@91 1004 List.exists (fn ((L'.CName s', _), _) => s' = s
adamc@91 1005 | _ => false) ns2
adamc@91 1006 | _ => false) ns1
adamc@91 1007 in
adamc@91 1008 ((L'.CRecord (kunit, ns), loc), cunif (loc, k), cunif (loc, k))
adamc@91 1009 end
adamc@91 1010 | (_, L'.CRecord _) => (ns2, cemp, cemp)
adamc@91 1011 | _ => (ns1, cemp, cemp)
adamc@86 1012
adamc@91 1013 val ns1' = (L'.CConcat (shared, ctx1), loc)
adamc@91 1014 val ns2' = (L'.CConcat (shared, ctx2), loc)
adamc@91 1015
adamc@91 1016 val e = (L'.EModProj (basis, [], "join"), loc)
adamc@91 1017 val e = (L'.ECApp (e, shared), loc)
adamc@91 1018 val e = (L'.ECApp (e, ctx1), loc)
adamc@91 1019 val e = (L'.ECApp (e, ctx2), loc)
adamc@91 1020 val e = (L'.EApp (e, xml1'), loc)
adamc@91 1021 val e = (L'.EApp (e, xml2'), loc)
adamc@91 1022
adamc@91 1023 val t = (L'.CApp ((L'.CModProj (basis, [], "xml"), loc), shared), loc)
adamc@91 1024
adamc@91 1025 fun doUnify (ns, ns') =
adamc@86 1026 let
adamc@91 1027 fun setEmpty c =
adamc@91 1028 let
adamc@91 1029 val ((c, _), gs) = hnormCon (env, denv) c
adamc@91 1030 in
adamc@91 1031 case c of
adamc@91 1032 L'.CUnif (_, _, _, r) =>
adamc@91 1033 (r := SOME cemp;
adamc@91 1034 gs)
adamc@91 1035 | L'.CConcat (_, c') => setEmpty c' @ gs
adamc@91 1036 | _ => gs
adamc@91 1037 end
adamc@91 1038
adamc@91 1039 val gs1 = unifyCons (env, denv) ns ns'
adamc@91 1040 val gs2 = setEmpty ns'
adamc@91 1041 val gs3 = unifyCons (env, denv) ns ns'
adamc@86 1042 in
adamc@91 1043 gs1 @ gs2 @ gs3
adamc@92 1044 end handle CUnify _ => (expError env (IncompatibleCons (ns, ns'));
adamc@92 1045 [])
adamc@12 1046
adamc@91 1047 val gs7 = doUnify (ns1, ns1')
adamc@91 1048 val gs8 = doUnify (ns2, ns2')
adamc@91 1049 in
adamc@91 1050 (e, t, (loc, env, denv, shared, ctx1)
adamc@91 1051 :: (loc, env, denv, shared, ctx2)
adamc@91 1052 :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 @ gs8)
adamc@91 1053 end
adamc@12 1054
adamc@91 1055 | L.EApp (e1, e2) =>
adamc@91 1056 let
adamc@91 1057 val (e1', t1, gs1) = elabExp (env, denv) e1
adamc@91 1058 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
adamc@91 1059 val (e2', t2, gs3) = elabExp (env, denv) e2
adamc@71 1060
adamc@91 1061 val dom = cunif (loc, ktype)
adamc@91 1062 val ran = cunif (loc, ktype)
adamc@91 1063 val t = (L'.TFun (dom, ran), dummy)
adamc@91 1064
adamc@91 1065 val gs4 = checkCon (env, denv) e1' t1 t
adamc@91 1066 val gs5 = checkCon (env, denv) e2' t2 dom
adamc@91 1067 in
adamc@91 1068 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
adamc@91 1069 end
adamc@91 1070 | L.EAbs (x, to, e) =>
adamc@91 1071 let
adamc@91 1072 val (t', gs1) = case to of
adamc@91 1073 NONE => (cunif (loc, ktype), [])
adamc@91 1074 | SOME t =>
adamc@91 1075 let
adamc@91 1076 val (t', tk, gs) = elabCon (env, denv) t
adamc@91 1077 in
adamc@91 1078 checkKind env t' tk ktype;
adamc@91 1079 (t', gs)
adamc@91 1080 end
adamc@91 1081 val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e
adamc@91 1082 in
adamc@91 1083 ((L'.EAbs (x, t', et, e'), loc),
adamc@91 1084 (L'.TFun (t', et), loc),
adamc@91 1085 gs1 @ gs2)
adamc@91 1086 end
adamc@91 1087 | L.ECApp (e, c) =>
adamc@91 1088 let
adamc@91 1089 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 1090 val (e', et, gs2) = elabHead (env, denv) e' et
adamc@91 1091 val (c', ck, gs3) = elabCon (env, denv) c
adamc@91 1092 val ((et', _), gs4) = hnormCon (env, denv) et
adamc@91 1093 in
adamc@91 1094 case et' of
adamc@91 1095 L'.CError => (eerror, cerror, [])
adamc@91 1096 | L'.TCFun (_, _, k, eb) =>
adamc@91 1097 let
adamc@91 1098 val () = checkKind env c' ck k
adamc@91 1099 val eb' = subConInCon (0, c') eb
adamc@91 1100 handle SynUnif => (expError env (Unif ("substitution", eb));
adamc@91 1101 cerror)
adamc@91 1102 in
adamc@91 1103 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
adamc@91 1104 end
adamc@91 1105
adamc@91 1106 | L'.CUnif _ =>
adamc@91 1107 (expError env (Unif ("application", et));
adamc@91 1108 (eerror, cerror, []))
adamc@91 1109
adamc@91 1110 | _ =>
adamc@91 1111 (expError env (WrongForm ("constructor function", e', et));
adamc@91 1112 (eerror, cerror, []))
adamc@91 1113 end
adamc@91 1114 | L.ECAbs (expl, x, k, e) =>
adamc@91 1115 let
adamc@91 1116 val expl' = elabExplicitness expl
adamc@91 1117 val k' = elabKind k
adamc@91 1118 val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
adamc@91 1119 in
adamc@91 1120 ((L'.ECAbs (expl', x, k', e'), loc),
adamc@91 1121 (L'.TCFun (expl', x, k', et), loc),
adamc@91 1122 gs)
adamc@91 1123 end
adamc@91 1124
adamc@91 1125 | L.EDisjoint (c1, c2, e) =>
adamc@91 1126 let
adamc@91 1127 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@91 1128 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@91 1129
adamc@91 1130 val ku1 = kunif loc
adamc@91 1131 val ku2 = kunif loc
adamc@91 1132
adamc@91 1133 val (denv', gs3) = D.assert env denv (c1', c2')
adamc@91 1134 val (e', t, gs4) = elabExp (env, denv') e
adamc@91 1135 in
adamc@91 1136 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@91 1137 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@91 1138
adamc@91 1139 (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
adamc@91 1140 end
adamc@91 1141
adamc@91 1142 | L.ERecord xes =>
adamc@91 1143 let
adamc@91 1144 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
adamc@91 1145 let
adamc@91 1146 val (x', xk, gs1) = elabCon (env, denv) x
adamc@91 1147 val (e', et, gs2) = elabExp (env, denv) e
adamc@91 1148 in
adamc@91 1149 checkKind env x' xk kname;
adamc@91 1150 ((x', e', et), gs1 @ gs2 @ gs)
adamc@91 1151 end)
adamc@91 1152 [] xes
adamc@91 1153
adamc@91 1154 val k = (L'.KType, loc)
adamc@91 1155
adamc@91 1156 fun prove (xets, gs) =
adamc@91 1157 case xets of
adamc@91 1158 [] => gs
adamc@91 1159 | (x, _, t) :: rest =>
adamc@91 1160 let
adamc@91 1161 val xc = (x, t)
adamc@91 1162 val r1 = (L'.CRecord (k, [xc]), loc)
adamc@91 1163 val gs = foldl (fn ((x', _, t'), gs) =>
adamc@91 1164 let
adamc@91 1165 val xc' = (x', t')
adamc@91 1166 val r2 = (L'.CRecord (k, [xc']), loc)
adamc@91 1167 in
adamc@91 1168 D.prove env denv (r1, r2, loc) @ gs
adamc@91 1169 end)
adamc@91 1170 gs rest
adamc@91 1171 in
adamc@91 1172 prove (rest, gs)
adamc@91 1173 end
adamc@91 1174 in
adamc@91 1175 ((L'.ERecord xes', loc),
adamc@91 1176 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
adamc@91 1177 prove (xes', gs))
adamc@91 1178 end
adamc@91 1179
adamc@91 1180 | L.EField (e, c) =>
adamc@91 1181 let
adamc@91 1182 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 1183 val (c', ck, gs2) = elabCon (env, denv) c
adamc@91 1184
adamc@91 1185 val ft = cunif (loc, ktype)
adamc@91 1186 val rest = cunif (loc, ktype_record)
adamc@91 1187 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
adamc@91 1188
adamc@91 1189 val gs3 =
adamc@91 1190 checkCon (env, denv) e' et
adamc@91 1191 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
adamc@91 1192 val gs4 = D.prove env denv (first, rest, loc)
adamc@91 1193 in
adamc@91 1194 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
adamc@91 1195 end
adamc@91 1196
adamc@91 1197 | L.EFold =>
adamc@91 1198 let
adamc@91 1199 val dom = kunif loc
adamc@91 1200 in
adamc@91 1201 ((L'.EFold dom, loc), foldType (dom, loc), [])
adamc@91 1202 end
adamc@91 1203 end
adamc@12 1204
adamc@12 1205
adamc@6 1206 datatype decl_error =
adamc@91 1207 KunifsRemain of L'.decl list
adamc@91 1208 | CunifsRemain of L'.decl list
adamc@91 1209
adamc@91 1210 fun lspan [] = ErrorMsg.dummySpan
adamc@91 1211 | lspan ((_, loc) :: _) = loc
adamc@6 1212
adamc@6 1213 fun declError env err =
adamc@6 1214 case err of
adamc@91 1215 KunifsRemain ds =>
adamc@91 1216 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
adamc@91 1217 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@91 1218 | CunifsRemain ds =>
adamc@91 1219 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
adamc@91 1220 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@6 1221
adamc@31 1222 datatype sgn_error =
adamc@31 1223 UnboundSgn of ErrorMsg.span * string
adamc@31 1224 | UnmatchedSgi of L'.sgn_item
adamc@31 1225 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
adamc@31 1226 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
adamc@41 1227 | SgnWrongForm of L'.sgn * L'.sgn
adamc@42 1228 | UnWhereable of L'.sgn * string
adamc@75 1229 | WhereWrongKind of L'.kind * L'.kind * kunify_error
adamc@58 1230 | NotIncludable of L'.sgn
adamc@62 1231 | DuplicateCon of ErrorMsg.span * string
adamc@62 1232 | DuplicateVal of ErrorMsg.span * string
adamc@62 1233 | DuplicateSgn of ErrorMsg.span * string
adamc@62 1234 | DuplicateStr of ErrorMsg.span * string
adamc@88 1235 | NotConstraintsable of L'.sgn
adamc@31 1236
adamc@31 1237 fun sgnError env err =
adamc@31 1238 case err of
adamc@31 1239 UnboundSgn (loc, s) =>
adamc@31 1240 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
adamc@31 1241 | UnmatchedSgi (sgi as (_, loc)) =>
adamc@31 1242 (ErrorMsg.errorAt loc "Unmatched signature item";
adamc@31 1243 eprefaces' [("Item", p_sgn_item env sgi)])
adamc@31 1244 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
adamc@31 1245 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
adamc@59 1246 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@59 1247 ("Need", p_sgn_item env sgi2),
adamc@31 1248 ("Kind 1", p_kind k1),
adamc@31 1249 ("Kind 2", p_kind k2)];
adamc@31 1250 kunifyError kerr)
adamc@31 1251 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
adamc@31 1252 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
adamc@59 1253 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@59 1254 ("Need", p_sgn_item env sgi2),
adamc@31 1255 ("Con 1", p_con env c1),
adamc@31 1256 ("Con 2", p_con env c2)];
adamc@31 1257 cunifyError env cerr)
adamc@41 1258 | SgnWrongForm (sgn1, sgn2) =>
adamc@41 1259 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
adamc@41 1260 eprefaces' [("Sig 1", p_sgn env sgn1),
adamc@41 1261 ("Sig 2", p_sgn env sgn2)])
adamc@42 1262 | UnWhereable (sgn, x) =>
adamc@42 1263 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
adamc@42 1264 eprefaces' [("Signature", p_sgn env sgn),
adamc@42 1265 ("Field", PD.string x)])
adamc@75 1266 | WhereWrongKind (k1, k2, kerr) =>
adamc@75 1267 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
adamc@75 1268 eprefaces' [("Have", p_kind k1),
adamc@75 1269 ("Need", p_kind k2)];
adamc@75 1270 kunifyError kerr)
adamc@58 1271 | NotIncludable sgn =>
adamc@58 1272 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
adamc@58 1273 eprefaces' [("Signature", p_sgn env sgn)])
adamc@62 1274 | DuplicateCon (loc, s) =>
adamc@62 1275 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
adamc@62 1276 | DuplicateVal (loc, s) =>
adamc@62 1277 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
adamc@62 1278 | DuplicateSgn (loc, s) =>
adamc@62 1279 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
adamc@62 1280 | DuplicateStr (loc, s) =>
adamc@62 1281 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
adamc@88 1282 | NotConstraintsable sgn =>
adamc@88 1283 (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
adamc@88 1284 eprefaces' [("Signature", p_sgn env sgn)])
adamc@31 1285
adamc@31 1286 datatype str_error =
adamc@31 1287 UnboundStr of ErrorMsg.span * string
adamc@44 1288 | NotFunctor of L'.sgn
adamc@46 1289 | FunctorRebind of ErrorMsg.span
adamc@61 1290 | UnOpenable of L'.sgn
adamc@75 1291 | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
adamc@31 1292
adamc@31 1293 fun strError env err =
adamc@31 1294 case err of
adamc@31 1295 UnboundStr (loc, s) =>
adamc@31 1296 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
adamc@44 1297 | NotFunctor sgn =>
adamc@44 1298 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
adamc@44 1299 eprefaces' [("Signature", p_sgn env sgn)])
adamc@46 1300 | FunctorRebind loc =>
adamc@46 1301 ErrorMsg.errorAt loc "Attempt to rebind functor"
adamc@61 1302 | UnOpenable sgn =>
adamc@61 1303 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
adamc@61 1304 eprefaces' [("Signature", p_sgn env sgn)])
adamc@75 1305 | NotType (k, (k1, k2, ue)) =>
adamc@75 1306 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
adamc@75 1307 eprefaces' [("Kind", p_kind k),
adamc@75 1308 ("Subkind 1", p_kind k1),
adamc@75 1309 ("Subkind 2", p_kind k2)];
adamc@75 1310 kunifyError ue)
adamc@31 1311
adamc@42 1312 val hnormSgn = E.hnormSgn
adamc@31 1313
adamc@88 1314 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
adamc@76 1315 case sgi of
adamc@76 1316 L.SgiConAbs (x, k) =>
adamc@76 1317 let
adamc@76 1318 val k' = elabKind k
adamc@31 1319
adamc@76 1320 val (env', n) = E.pushCNamed env x k' NONE
adamc@76 1321 in
adamc@88 1322 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs))
adamc@76 1323 end
adamc@31 1324
adamc@76 1325 | L.SgiCon (x, ko, c) =>
adamc@76 1326 let
adamc@76 1327 val k' = case ko of
adamc@76 1328 NONE => kunif loc
adamc@76 1329 | SOME k => elabKind k
adamc@31 1330
adamc@83 1331 val (c', ck, gs') = elabCon (env, denv) c
adamc@76 1332 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@76 1333 in
adamc@76 1334 checkKind env c' ck k';
adamc@31 1335
adamc@88 1336 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
adamc@76 1337 end
adamc@31 1338
adamc@76 1339 | L.SgiVal (x, c) =>
adamc@76 1340 let
adamc@83 1341 val (c', ck, gs') = elabCon (env, denv) c
adamc@31 1342
adamc@76 1343 val (env', n) = E.pushENamed env x c'
adamc@76 1344 in
adamc@76 1345 (unifyKinds ck ktype
adamc@76 1346 handle KUnify ue => strError env (NotType (ck, ue)));
adamc@31 1347
adamc@88 1348 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
adamc@76 1349 end
adamc@31 1350
adamc@76 1351 | L.SgiStr (x, sgn) =>
adamc@76 1352 let
adamc@83 1353 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 1354 val (env', n) = E.pushStrNamed env x sgn'
adamc@76 1355 in
adamc@88 1356 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 1357 end
adamc@31 1358
adamc@76 1359 | L.SgiSgn (x, sgn) =>
adamc@76 1360 let
adamc@83 1361 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 1362 val (env', n) = E.pushSgnNamed env x sgn'
adamc@76 1363 in
adamc@88 1364 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 1365 end
adamc@31 1366
adamc@76 1367 | L.SgiInclude sgn =>
adamc@76 1368 let
adamc@83 1369 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 1370 in
adamc@76 1371 case #1 (hnormSgn env sgn') of
adamc@76 1372 L'.SgnConst sgis =>
adamc@88 1373 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs))
adamc@76 1374 | _ => (sgnError env (NotIncludable sgn');
adamc@88 1375 ([], (env, denv, [])))
adamc@88 1376 end
adamc@88 1377
adamc@88 1378 | L.SgiConstraint (c1, c2) =>
adamc@88 1379 let
adamc@88 1380 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@88 1381 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@88 1382
adamc@90 1383 val (denv, gs3) = D.assert env denv (c1', c2')
adamc@88 1384 in
adamc@88 1385 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
adamc@88 1386 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
adamc@88 1387
adamc@90 1388 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
adamc@76 1389 end
adamc@31 1390
adamc@83 1391 and elabSgn (env, denv) (sgn, loc) =
adamc@31 1392 case sgn of
adamc@31 1393 L.SgnConst sgis =>
adamc@31 1394 let
adamc@88 1395 val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis
adamc@62 1396
adamc@62 1397 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) =>
adamc@62 1398 case sgi of
adamc@62 1399 L'.SgiConAbs (x, _, _) =>
adamc@62 1400 (if SS.member (cons, x) then
adamc@62 1401 sgnError env (DuplicateCon (loc, x))
adamc@62 1402 else
adamc@62 1403 ();
adamc@62 1404 (SS.add (cons, x), vals, sgns, strs))
adamc@62 1405 | L'.SgiCon (x, _, _, _) =>
adamc@62 1406 (if SS.member (cons, x) then
adamc@62 1407 sgnError env (DuplicateCon (loc, x))
adamc@62 1408 else
adamc@62 1409 ();
adamc@62 1410 (SS.add (cons, x), vals, sgns, strs))
adamc@62 1411 | L'.SgiVal (x, _, _) =>
adamc@62 1412 (if SS.member (vals, x) then
adamc@62 1413 sgnError env (DuplicateVal (loc, x))
adamc@62 1414 else
adamc@62 1415 ();
adamc@62 1416 (cons, SS.add (vals, x), sgns, strs))
adamc@62 1417 | L'.SgiSgn (x, _, _) =>
adamc@62 1418 (if SS.member (sgns, x) then
adamc@62 1419 sgnError env (DuplicateSgn (loc, x))
adamc@62 1420 else
adamc@62 1421 ();
adamc@62 1422 (cons, vals, SS.add (sgns, x), strs))
adamc@62 1423 | L'.SgiStr (x, _, _) =>
adamc@62 1424 (if SS.member (strs, x) then
adamc@62 1425 sgnError env (DuplicateStr (loc, x))
adamc@62 1426 else
adamc@62 1427 ();
adamc@88 1428 (cons, vals, sgns, SS.add (strs, x)))
adamc@88 1429 | L'.SgiConstraint _ => (cons, vals, sgns, strs))
adamc@62 1430 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
adamc@31 1431 in
adamc@83 1432 ((L'.SgnConst sgis', loc), gs)
adamc@31 1433 end
adamc@31 1434 | L.SgnVar x =>
adamc@31 1435 (case E.lookupSgn env x of
adamc@31 1436 NONE =>
adamc@31 1437 (sgnError env (UnboundSgn (loc, x));
adamc@83 1438 ((L'.SgnError, loc), []))
adamc@83 1439 | SOME (n, sgis) => ((L'.SgnVar n, loc), []))
adamc@41 1440 | L.SgnFun (m, dom, ran) =>
adamc@41 1441 let
adamc@83 1442 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41 1443 val (env', n) = E.pushStrNamed env m dom'
adamc@83 1444 val (ran', gs2) = elabSgn (env', denv) ran
adamc@41 1445 in
adamc@83 1446 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
adamc@41 1447 end
adamc@42 1448 | L.SgnWhere (sgn, x, c) =>
adamc@42 1449 let
adamc@83 1450 val (sgn', ds1) = elabSgn (env, denv) sgn
adamc@83 1451 val (c', ck, ds2) = elabCon (env, denv) c
adamc@42 1452 in
adamc@42 1453 case #1 (hnormSgn env sgn') of
adamc@83 1454 L'.SgnError => (sgnerror, [])
adamc@42 1455 | L'.SgnConst sgis =>
adamc@75 1456 if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
adamc@75 1457 x' = x andalso
adamc@75 1458 (unifyKinds k ck
adamc@75 1459 handle KUnify x => sgnError env (WhereWrongKind x);
adamc@42 1460 true)
adamc@42 1461 | _ => false) sgis then
adamc@83 1462 ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2)
adamc@42 1463 else
adamc@42 1464 (sgnError env (UnWhereable (sgn', x));
adamc@83 1465 (sgnerror, []))
adamc@42 1466 | _ => (sgnError env (UnWhereable (sgn', x));
adamc@83 1467 (sgnerror, []))
adamc@42 1468 end
adamc@59 1469 | L.SgnProj (m, ms, x) =>
adamc@59 1470 (case E.lookupStr env m of
adamc@59 1471 NONE => (strError env (UnboundStr (loc, m));
adamc@83 1472 (sgnerror, []))
adamc@59 1473 | SOME (n, sgn) =>
adamc@59 1474 let
adamc@59 1475 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@59 1476 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@59 1477 NONE => (strError env (UnboundStr (loc, m));
adamc@59 1478 (strerror, sgnerror))
adamc@59 1479 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@59 1480 ((L'.StrVar n, loc), sgn) ms
adamc@59 1481 in
adamc@59 1482 case E.projectSgn env {sgn = sgn, str = str, field = x} of
adamc@59 1483 NONE => (sgnError env (UnboundSgn (loc, x));
adamc@83 1484 (sgnerror, []))
adamc@83 1485 | SOME _ => ((L'.SgnProj (n, ms, x), loc), [])
adamc@59 1486 end)
adamc@59 1487
adamc@31 1488
adamc@66 1489 fun selfify env {str, strs, sgn} =
adamc@66 1490 case #1 (hnormSgn env sgn) of
adamc@66 1491 L'.SgnError => sgn
adamc@66 1492 | L'.SgnVar _ => sgn
adamc@66 1493
adamc@66 1494 | L'.SgnConst sgis =>
adamc@66 1495 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
adamc@66 1496 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
adamc@66 1497 | (L'.SgiStr (x, n, sgn), loc) =>
adamc@66 1498 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
adamc@66 1499 | x => x) sgis), #2 sgn)
adamc@66 1500 | L'.SgnFun _ => sgn
adamc@66 1501 | L'.SgnWhere _ => sgn
adamc@66 1502 | L'.SgnProj (m, ms, x) =>
adamc@66 1503 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66 1504 (L'.StrVar m, #2 sgn) ms,
adamc@66 1505 sgn = #2 (E.lookupStrNamed env m),
adamc@66 1506 field = x} of
adamc@66 1507 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
adamc@66 1508 | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
adamc@66 1509
adamc@66 1510 fun selfifyAt env {str, sgn} =
adamc@66 1511 let
adamc@66 1512 fun self (str, _) =
adamc@66 1513 case str of
adamc@66 1514 L'.StrVar x => SOME (x, [])
adamc@66 1515 | L'.StrProj (str, x) =>
adamc@66 1516 (case self str of
adamc@66 1517 NONE => NONE
adamc@66 1518 | SOME (m, ms) => SOME (m, ms @ [x]))
adamc@66 1519 | _ => NONE
adamc@66 1520 in
adamc@66 1521 case self str of
adamc@66 1522 NONE => sgn
adamc@66 1523 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
adamc@66 1524 end
adamc@66 1525
adamc@88 1526 fun dopen (env, denv) {str, strs, sgn} =
adamc@66 1527 let
adamc@66 1528 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66 1529 (L'.StrVar str, #2 sgn) strs
adamc@66 1530 in
adamc@66 1531 case #1 (hnormSgn env sgn) of
adamc@66 1532 L'.SgnConst sgis =>
adamc@88 1533 ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) =>
adamc@66 1534 case sgi of
adamc@66 1535 L'.SgiConAbs (x, n, k) =>
adamc@88 1536 let
adamc@88 1537 val c = (L'.CModProj (str, strs, x), loc)
adamc@88 1538 in
adamc@88 1539 ((L'.DCon (x, n, k, c), loc),
adamc@88 1540 (E.pushCNamedAs env' x n k (SOME c), denv'))
adamc@88 1541 end
adamc@66 1542 | L'.SgiCon (x, n, k, c) =>
adamc@66 1543 ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc),
adamc@88 1544 (E.pushCNamedAs env' x n k (SOME c), denv'))
adamc@66 1545 | L'.SgiVal (x, n, t) =>
adamc@66 1546 ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc),
adamc@88 1547 (E.pushENamedAs env' x n t, denv'))
adamc@66 1548 | L'.SgiStr (x, n, sgn) =>
adamc@66 1549 ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc),
adamc@88 1550 (E.pushStrNamedAs env' x n sgn, denv'))
adamc@66 1551 | L'.SgiSgn (x, n, sgn) =>
adamc@66 1552 ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc),
adamc@88 1553 (E.pushSgnNamedAs env' x n sgn, denv'))
adamc@88 1554 | L'.SgiConstraint (c1, c2) =>
adamc@88 1555 ((L'.DConstraint (c1, c2), loc),
adamc@88 1556 (env', denv (* D.assert env denv (c1, c2) *) )))
adamc@88 1557 (env, denv) sgis
adamc@66 1558 | _ => (strError env (UnOpenable sgn);
adamc@88 1559 ([], (env, denv)))
adamc@66 1560 end
adamc@66 1561
adamc@88 1562 fun dopenConstraints (loc, env, denv) {str, strs} =
adamc@88 1563 case E.lookupStr env str of
adamc@88 1564 NONE => (strError env (UnboundStr (loc, str));
adamc@88 1565 denv)
adamc@88 1566 | SOME (n, sgn) =>
adamc@88 1567 let
adamc@88 1568 val (st, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@88 1569 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@88 1570 NONE => (strError env (UnboundStr (loc, m));
adamc@88 1571 (strerror, sgnerror))
adamc@88 1572 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@88 1573 ((L'.StrVar n, loc), sgn) strs
adamc@88 1574
adamc@88 1575 val cso = E.projectConstraints env {sgn = sgn, str = st}
adamc@88 1576
adamc@88 1577 val denv = case cso of
adamc@88 1578 NONE => (strError env (UnboundStr (loc, str));
adamc@88 1579 denv)
adamc@90 1580 | SOME cs => foldl (fn ((c1, c2), denv) =>
adamc@90 1581 let
adamc@90 1582 val (denv, gs) = D.assert env denv (c1, c2)
adamc@90 1583 in
adamc@90 1584 case gs of
adamc@90 1585 [] => ()
adamc@90 1586 | _ => raise Fail "dopenConstraints: Sub-constraints remain";
adamc@90 1587
adamc@90 1588 denv
adamc@90 1589 end) denv cs
adamc@88 1590 in
adamc@88 1591 denv
adamc@88 1592 end
adamc@88 1593
adamc@31 1594 fun sgiOfDecl (d, loc) =
adamc@31 1595 case d of
adamc@100 1596 L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc)
adamc@100 1597 | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc)
adamc@100 1598 | L'.DSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, sgn), loc)
adamc@100 1599 | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
adamc@100 1600 | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc)
adamc@100 1601 | L'.DConstraint cs => SOME (L'.SgiConstraint cs, loc)
adamc@109 1602 | L'.DExport _ => NONE
adamc@88 1603
adamc@88 1604 fun sgiBindsD (env, denv) (sgi, _) =
adamc@88 1605 case sgi of
adamc@90 1606 L'.SgiConstraint (c1, c2) =>
adamc@90 1607 (case D.assert env denv (c1, c2) of
adamc@90 1608 (denv, []) => denv
adamc@90 1609 | _ => raise Fail "sgiBindsD: Sub-constraints remain")
adamc@88 1610 | _ => denv
adamc@31 1611
adamc@86 1612 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
adamc@35 1613 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
adamc@31 1614 (L'.SgnError, _) => ()
adamc@31 1615 | (_, L'.SgnError) => ()
adamc@31 1616
adamc@31 1617 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
adamc@31 1618 let
adamc@88 1619 fun folder (sgi2All as (sgi, _), (env, denv)) =
adamc@31 1620 let
adamc@31 1621 fun seek p =
adamc@31 1622 let
adamc@88 1623 fun seek (env, denv) ls =
adamc@31 1624 case ls of
adamc@31 1625 [] => (sgnError env (UnmatchedSgi sgi2All);
adamc@88 1626 (env, denv))
adamc@31 1627 | h :: t =>
adamc@31 1628 case p h of
adamc@88 1629 NONE => seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t
adamc@88 1630 | SOME envs => envs
adamc@31 1631 in
adamc@88 1632 seek (env, denv) sgis1
adamc@31 1633 end
adamc@31 1634 in
adamc@31 1635 case sgi of
adamc@31 1636 L'.SgiConAbs (x, n2, k2) =>
adamc@31 1637 seek (fn sgi1All as (sgi1, _) =>
adamc@31 1638 let
adamc@41 1639 fun found (x', n1, k1, co1) =
adamc@41 1640 if x = x' then
adamc@41 1641 let
adamc@41 1642 val () = unifyKinds k1 k2
adamc@41 1643 handle KUnify (k1, k2, err) =>
adamc@41 1644 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
adamc@41 1645 val env = E.pushCNamedAs env x n1 k1 co1
adamc@41 1646 in
adamc@41 1647 SOME (if n1 = n2 then
adamc@41 1648 env
adamc@41 1649 else
adamc@88 1650 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)),
adamc@88 1651 denv)
adamc@41 1652 end
adamc@41 1653 else
adamc@41 1654 NONE
adamc@31 1655 in
adamc@31 1656 case sgi1 of
adamc@41 1657 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
adamc@41 1658 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
adamc@31 1659 | _ => NONE
adamc@31 1660 end)
adamc@31 1661
adamc@31 1662 | L'.SgiCon (x, n2, k2, c2) =>
adamc@31 1663 seek (fn sgi1All as (sgi1, _) =>
adamc@31 1664 case sgi1 of
adamc@41 1665 L'.SgiCon (x', n1, k1, c1) =>
adamc@41 1666 if x = x' then
adamc@41 1667 let
adamc@88 1668 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv)
adamc@41 1669 in
adamc@86 1670 (case unifyCons (env, denv) c1 c2 of
adamc@86 1671 [] => good ()
adamc@86 1672 | _ => NONE)
adamc@86 1673 handle CUnify (c1, c2, err) =>
adamc@86 1674 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@86 1675 good ())
adamc@41 1676 end
adamc@41 1677 else
adamc@41 1678 NONE
adamc@31 1679 | _ => NONE)
adamc@31 1680
adamc@32 1681 | L'.SgiVal (x, n2, c2) =>
adamc@32 1682 seek (fn sgi1All as (sgi1, _) =>
adamc@32 1683 case sgi1 of
adamc@41 1684 L'.SgiVal (x', n1, c1) =>
adamc@41 1685 if x = x' then
adamc@86 1686 (case unifyCons (env, denv) c1 c2 of
adamc@88 1687 [] => SOME (env, denv)
adamc@86 1688 | _ => NONE)
adamc@86 1689 handle CUnify (c1, c2, err) =>
adamc@86 1690 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@88 1691 SOME (env, denv))
adamc@41 1692 else
adamc@41 1693 NONE
adamc@32 1694 | _ => NONE)
adamc@32 1695
adamc@33 1696 | L'.SgiStr (x, n2, sgn2) =>
adamc@33 1697 seek (fn sgi1All as (sgi1, _) =>
adamc@33 1698 case sgi1 of
adamc@41 1699 L'.SgiStr (x', n1, sgn1) =>
adamc@41 1700 if x = x' then
adamc@66 1701 let
adamc@86 1702 val () = subSgn (env, denv) sgn1 sgn2
adamc@66 1703 val env = E.pushStrNamedAs env x n1 sgn1
adamc@66 1704 val env = if n1 = n2 then
adamc@66 1705 env
adamc@66 1706 else
adamc@66 1707 E.pushStrNamedAs env x n2
adamc@66 1708 (selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
adamc@66 1709 sgn = sgn2})
adamc@66 1710 in
adamc@88 1711 SOME (env, denv)
adamc@66 1712 end
adamc@41 1713 else
adamc@41 1714 NONE
adamc@33 1715 | _ => NONE)
adamc@59 1716
adamc@59 1717 | L'.SgiSgn (x, n2, sgn2) =>
adamc@59 1718 seek (fn sgi1All as (sgi1, _) =>
adamc@59 1719 case sgi1 of
adamc@59 1720 L'.SgiSgn (x', n1, sgn1) =>
adamc@59 1721 if x = x' then
adamc@65 1722 let
adamc@86 1723 val () = subSgn (env, denv) sgn1 sgn2
adamc@86 1724 val () = subSgn (env, denv) sgn2 sgn1
adamc@65 1725
adamc@65 1726 val env = E.pushSgnNamedAs env x n2 sgn2
adamc@65 1727 val env = if n1 = n2 then
adamc@65 1728 env
adamc@65 1729 else
adamc@65 1730 E.pushSgnNamedAs env x n1 sgn2
adamc@65 1731 in
adamc@88 1732 SOME (env, denv)
adamc@65 1733 end
adamc@59 1734 else
adamc@59 1735 NONE
adamc@59 1736 | _ => NONE)
adamc@88 1737
adamc@88 1738 | L'.SgiConstraint (c2, d2) =>
adamc@88 1739 seek (fn sgi1All as (sgi1, _) =>
adamc@88 1740 case sgi1 of
adamc@88 1741 L'.SgiConstraint (c1, d1) =>
adamc@88 1742 if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then
adamc@90 1743 let
adamc@90 1744 val (denv, gs) = D.assert env denv (c2, d2)
adamc@90 1745 in
adamc@90 1746 case gs of
adamc@90 1747 [] => ()
adamc@90 1748 | _ => raise Fail "subSgn: Sub-constraints remain";
adamc@90 1749
adamc@90 1750 SOME (env, denv)
adamc@90 1751 end
adamc@88 1752 else
adamc@88 1753 NONE
adamc@88 1754 | _ => NONE)
adamc@31 1755 end
adamc@31 1756 in
adamc@88 1757 ignore (foldl folder (env, denv) sgis2)
adamc@31 1758 end
adamc@31 1759
adamc@41 1760 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
adamc@43 1761 let
adamc@43 1762 val ran1 =
adamc@43 1763 if n1 = n2 then
adamc@43 1764 ran1
adamc@43 1765 else
adamc@43 1766 subStrInSgn (n1, n2) ran1
adamc@43 1767 in
adamc@86 1768 subSgn (env, denv) dom2 dom1;
adamc@86 1769 subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2
adamc@43 1770 end
adamc@41 1771
adamc@41 1772 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
adamc@41 1773
adamc@61 1774
adamc@88 1775 fun elabDecl ((d, loc), (env, denv, gs)) =
adamc@76 1776 case d of
adamc@76 1777 L.DCon (x, ko, c) =>
adamc@76 1778 let
adamc@76 1779 val k' = case ko of
adamc@76 1780 NONE => kunif loc
adamc@76 1781 | SOME k => elabKind k
adamc@76 1782
adamc@83 1783 val (c', ck, gs') = elabCon (env, denv) c
adamc@76 1784 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@76 1785 in
adamc@76 1786 checkKind env c' ck k';
adamc@76 1787
adamc@88 1788 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
adamc@76 1789 end
adamc@76 1790 | L.DVal (x, co, e) =>
adamc@76 1791 let
adamc@83 1792 val (c', ck, gs1) = case co of
adamc@83 1793 NONE => (cunif (loc, ktype), ktype, [])
adamc@83 1794 | SOME c => elabCon (env, denv) c
adamc@76 1795
adamc@83 1796 val (e', et, gs2) = elabExp (env, denv) e
adamc@76 1797 val (env', n) = E.pushENamed env x c'
adamc@86 1798
adamc@86 1799 val gs3 = checkCon (env, denv) e' et c'
adamc@76 1800 in
adamc@88 1801 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs))
adamc@76 1802 end
adamc@76 1803
adamc@76 1804 | L.DSgn (x, sgn) =>
adamc@76 1805 let
adamc@83 1806 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 1807 val (env', n) = E.pushSgnNamed env x sgn'
adamc@76 1808 in
adamc@88 1809 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 1810 end
adamc@76 1811
adamc@76 1812 | L.DStr (x, sgno, str) =>
adamc@76 1813 let
adamc@93 1814 val () = if x = "Basis" then
adamc@93 1815 raise Fail "Not allowed to redefine structure 'Basis'"
adamc@93 1816 else
adamc@93 1817 ()
adamc@93 1818
adamc@83 1819 val formal = Option.map (elabSgn (env, denv)) sgno
adamc@76 1820
adamc@83 1821 val (str', sgn', gs') =
adamc@78 1822 case formal of
adamc@78 1823 NONE =>
adamc@78 1824 let
adamc@83 1825 val (str', actual, ds) = elabStr (env, denv) str
adamc@78 1826 in
adamc@83 1827 (str', selfifyAt env {str = str', sgn = actual}, ds)
adamc@78 1828 end
adamc@83 1829 | SOME (formal, gs1) =>
adamc@78 1830 let
adamc@78 1831 val str =
adamc@78 1832 case #1 (hnormSgn env formal) of
adamc@78 1833 L'.SgnConst sgis =>
adamc@78 1834 (case #1 str of
adamc@78 1835 L.StrConst ds =>
adamc@78 1836 let
adamc@78 1837 val needed = foldl (fn ((sgi, _), needed) =>
adamc@78 1838 case sgi of
adamc@78 1839 L'.SgiConAbs (x, _, _) => SS.add (needed, x)
adamc@78 1840 | _ => needed)
adamc@78 1841 SS.empty sgis
adamc@78 1842
adamc@78 1843 val needed = foldl (fn ((d, _), needed) =>
adamc@78 1844 case d of
adamc@78 1845 L.DCon (x, _, _) => (SS.delete (needed, x)
adamc@78 1846 handle NotFound => needed)
adamc@78 1847 | L.DOpen _ => SS.empty
adamc@78 1848 | _ => needed)
adamc@78 1849 needed ds
adamc@78 1850 in
adamc@78 1851 case SS.listItems needed of
adamc@78 1852 [] => str
adamc@78 1853 | xs =>
adamc@78 1854 let
adamc@78 1855 val kwild = (L.KWild, #2 str)
adamc@78 1856 val cwild = (L.CWild kwild, #2 str)
adamc@78 1857 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
adamc@78 1858 in
adamc@78 1859 (L.StrConst (ds @ ds'), #2 str)
adamc@78 1860 end
adamc@78 1861 end
adamc@78 1862 | _ => str)
adamc@78 1863 | _ => str
adamc@78 1864
adamc@83 1865 val (str', actual, gs2) = elabStr (env, denv) str
adamc@78 1866 in
adamc@86 1867 subSgn (env, denv) actual formal;
adamc@83 1868 (str', formal, gs1 @ gs2)
adamc@78 1869 end
adamc@76 1870
adamc@76 1871 val (env', n) = E.pushStrNamed env x sgn'
adamc@76 1872 in
adamc@76 1873 case #1 (hnormSgn env sgn') of
adamc@76 1874 L'.SgnFun _ =>
adamc@76 1875 (case #1 str' of
adamc@76 1876 L'.StrFun _ => ()
adamc@76 1877 | _ => strError env (FunctorRebind loc))
adamc@76 1878 | _ => ();
adamc@76 1879
adamc@88 1880 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
adamc@76 1881 end
adamc@76 1882
adamc@76 1883 | L.DFfiStr (x, sgn) =>
adamc@76 1884 let
adamc@83 1885 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 1886
adamc@76 1887 val (env', n) = E.pushStrNamed env x sgn'
adamc@76 1888 in
adamc@88 1889 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 1890 end
adamc@76 1891
adamc@76 1892 | L.DOpen (m, ms) =>
adamc@88 1893 (case E.lookupStr env m of
adamc@88 1894 NONE => (strError env (UnboundStr (loc, m));
adamc@88 1895 ([], (env, denv, [])))
adamc@88 1896 | SOME (n, sgn) =>
adamc@88 1897 let
adamc@88 1898 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@88 1899 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@88 1900 NONE => (strError env (UnboundStr (loc, m));
adamc@88 1901 (strerror, sgnerror))
adamc@88 1902 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@88 1903 ((L'.StrVar n, loc), sgn) ms
adamc@83 1904
adamc@88 1905 val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn}
adamc@88 1906 val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
adamc@88 1907 in
adamc@88 1908 (ds, (env', denv', []))
adamc@88 1909 end)
adamc@88 1910
adamc@88 1911 | L.DConstraint (c1, c2) =>
adamc@88 1912 let
adamc@88 1913 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@88 1914 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@90 1915 val gs3 = D.prove env denv (c1', c2', loc)
adamc@88 1916
adamc@90 1917 val (denv', gs4) = D.assert env denv (c1', c2')
adamc@88 1918 in
adamc@88 1919 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
adamc@88 1920 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
adamc@88 1921
adamc@90 1922 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3 @ gs4))
adamc@88 1923 end
adamc@88 1924
adamc@88 1925 | L.DOpenConstraints (m, ms) =>
adamc@88 1926 let
adamc@88 1927 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
adamc@88 1928 in
adamc@88 1929 ([], (env, denv, []))
adamc@88 1930 end
adamc@3 1931
adamc@109 1932 | L.DExport str =>
adamc@100 1933 let
adamc@109 1934 val (str', sgn, gs) = elabStr (env, denv) str
adamc@100 1935
adamc@109 1936 val sgn =
adamc@109 1937 case #1 (hnormSgn env sgn) of
adamc@109 1938 L'.SgnConst sgis =>
adamc@109 1939 let
adamc@109 1940 fun doOne (all as (sgi, _)) =
adamc@109 1941 case sgi of
adamc@109 1942 L'.SgiVal (x, n, t) =>
adamc@109 1943 (case hnormCon (env, denv) t of
adamc@109 1944 ((L'.TFun (dom, ran), _), []) =>
adamc@109 1945 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
adamc@109 1946 (((L'.TRecord domR, _), []),
adamc@109 1947 ((L'.CApp (tf, ranR), _), [])) =>
adamc@109 1948 (case hnormCon (env, denv) ranR of
adamc@109 1949 (ranR, []) =>
adamc@109 1950 (case (hnormCon (env, denv) domR, hnormCon (env, denv) ranR) of
adamc@109 1951 ((domR, []), (ranR, [])) =>
adamc@109 1952 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
adamc@109 1953 (L'.CApp (tf,
adamc@109 1954 (L'.TRecord ranR, loc)), loc)),
adamc@109 1955 loc)), loc)
adamc@109 1956 | _ => all)
adamc@109 1957 | _ => all)
adamc@109 1958 | _ => all)
adamc@109 1959 | _ => all)
adamc@109 1960 | _ => all
adamc@109 1961 in
adamc@109 1962 (L'.SgnConst (map doOne sgis), loc)
adamc@109 1963 end
adamc@109 1964 | _ => sgn
adamc@100 1965 in
adamc@109 1966 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs))
adamc@100 1967 end
adamc@100 1968
adamc@83 1969 and elabStr (env, denv) (str, loc) =
adamc@31 1970 case str of
adamc@31 1971 L.StrConst ds =>
adamc@31 1972 let
adamc@88 1973 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
adamc@100 1974 val sgis = List.mapPartial sgiOfDecl ds'
adamc@63 1975
adamc@63 1976 val (sgis, _, _, _, _) =
adamc@64 1977 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
adamc@63 1978 case sgi of
adamc@64 1979 L'.SgiConAbs (x, n, k) =>
adamc@64 1980 let
adamc@64 1981 val (cons, x) =
adamc@64 1982 if SS.member (cons, x) then
adamc@64 1983 (cons, "?" ^ x)
adamc@64 1984 else
adamc@64 1985 (SS.add (cons, x), x)
adamc@64 1986 in
adamc@64 1987 ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 1988 end
adamc@64 1989 | L'.SgiCon (x, n, k, c) =>
adamc@64 1990 let
adamc@64 1991 val (cons, x) =
adamc@64 1992 if SS.member (cons, x) then
adamc@64 1993 (cons, "?" ^ x)
adamc@64 1994 else
adamc@64 1995 (SS.add (cons, x), x)
adamc@64 1996 in
adamc@64 1997 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 1998 end
adamc@64 1999 | L'.SgiVal (x, n, c) =>
adamc@64 2000 let
adamc@64 2001 val (vals, x) =
adamc@64 2002 if SS.member (vals, x) then
adamc@64 2003 (vals, "?" ^ x)
adamc@64 2004 else
adamc@64 2005 (SS.add (vals, x), x)
adamc@64 2006 in
adamc@64 2007 ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 2008 end
adamc@64 2009 | L'.SgiSgn (x, n, sgn) =>
adamc@64 2010 let
adamc@64 2011 val (sgns, x) =
adamc@64 2012 if SS.member (sgns, x) then
adamc@64 2013 (sgns, "?" ^ x)
adamc@64 2014 else
adamc@64 2015 (SS.add (sgns, x), x)
adamc@64 2016 in
adamc@64 2017 ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 2018 end
adamc@64 2019
adamc@64 2020 | L'.SgiStr (x, n, sgn) =>
adamc@64 2021 let
adamc@64 2022 val (strs, x) =
adamc@64 2023 if SS.member (strs, x) then
adamc@64 2024 (strs, "?" ^ x)
adamc@64 2025 else
adamc@64 2026 (SS.add (strs, x), x)
adamc@64 2027 in
adamc@64 2028 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@88 2029 end
adamc@88 2030 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs))
adamc@64 2031
adamc@63 2032 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
adamc@31 2033 in
adamc@83 2034 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)
adamc@31 2035 end
adamc@31 2036 | L.StrVar x =>
adamc@31 2037 (case E.lookupStr env x of
adamc@31 2038 NONE =>
adamc@31 2039 (strError env (UnboundStr (loc, x));
adamc@83 2040 (strerror, sgnerror, []))
adamc@83 2041 | SOME (n, sgn) => ((L'.StrVar n, loc), sgn, []))
adamc@34 2042 | L.StrProj (str, x) =>
adamc@34 2043 let
adamc@83 2044 val (str', sgn, gs) = elabStr (env, denv) str
adamc@34 2045 in
adamc@34 2046 case E.projectStr env {str = str', sgn = sgn, field = x} of
adamc@34 2047 NONE => (strError env (UnboundStr (loc, x));
adamc@83 2048 (strerror, sgnerror, []))
adamc@83 2049 | SOME sgn => ((L'.StrProj (str', x), loc), sgn, gs)
adamc@34 2050 end
adamc@41 2051 | L.StrFun (m, dom, ranO, str) =>
adamc@41 2052 let
adamc@83 2053 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41 2054 val (env', n) = E.pushStrNamed env m dom'
adamc@83 2055 val (str', actual, gs2) = elabStr (env', denv) str
adamc@41 2056
adamc@83 2057 val (formal, gs3) =
adamc@41 2058 case ranO of
adamc@83 2059 NONE => (actual, [])
adamc@41 2060 | SOME ran =>
adamc@41 2061 let
adamc@83 2062 val (ran', gs) = elabSgn (env', denv) ran
adamc@41 2063 in
adamc@86 2064 subSgn (env', denv) actual ran';
adamc@83 2065 (ran', gs)
adamc@41 2066 end
adamc@41 2067 in
adamc@41 2068 ((L'.StrFun (m, n, dom', formal, str'), loc),
adamc@83 2069 (L'.SgnFun (m, n, dom', formal), loc),
adamc@83 2070 gs1 @ gs2 @ gs3)
adamc@41 2071 end
adamc@44 2072 | L.StrApp (str1, str2) =>
adamc@44 2073 let
adamc@83 2074 val (str1', sgn1, gs1) = elabStr (env, denv) str1
adamc@83 2075 val (str2', sgn2, gs2) = elabStr (env, denv) str2
adamc@44 2076 in
adamc@44 2077 case #1 (hnormSgn env sgn1) of
adamc@83 2078 L'.SgnError => (strerror, sgnerror, [])
adamc@44 2079 | L'.SgnFun (m, n, dom, ran) =>
adamc@86 2080 (subSgn (env, denv) sgn2 dom;
adamc@44 2081 case #1 (hnormSgn env ran) of
adamc@83 2082 L'.SgnError => (strerror, sgnerror, [])
adamc@44 2083 | L'.SgnConst sgis =>
adamc@44 2084 ((L'.StrApp (str1', str2'), loc),
adamc@83 2085 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
adamc@83 2086 gs1 @ gs2)
adamc@44 2087 | _ => raise Fail "Unable to hnormSgn in functor application")
adamc@44 2088 | _ => (strError env (NotFunctor sgn1);
adamc@83 2089 (strerror, sgnerror, []))
adamc@44 2090 end
adamc@31 2091
adamc@56 2092 fun elabFile basis env file =
adamc@56 2093 let
adamc@83 2094 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
adamc@83 2095 val () = case gs of
adamc@83 2096 [] => ()
adamc@83 2097 | _ => raise Fail "Unresolved disjointness constraints in Basis"
adamc@83 2098
adamc@56 2099 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
adamc@56 2100
adamc@88 2101 val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn}
adamc@56 2102
adamc@56 2103 fun discoverC r x =
adamc@56 2104 case E.lookupC env' x of
adamc@56 2105 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
adamc@56 2106 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
adamc@56 2107 | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc)
adamc@56 2108
adamc@56 2109 val () = discoverC int "int"
adamc@56 2110 val () = discoverC float "float"
adamc@56 2111 val () = discoverC string "string"
adamc@56 2112
adamc@83 2113 fun elabDecl' (d, (env, gs)) =
adamc@76 2114 let
adamc@76 2115 val () = resetKunif ()
adamc@76 2116 val () = resetCunif ()
adamc@88 2117 val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs))
adamc@76 2118 in
adamc@76 2119 if ErrorMsg.anyErrors () then
adamc@76 2120 ()
adamc@76 2121 else (
adamc@76 2122 if List.exists kunifsInDecl ds then
adamc@91 2123 declError env (KunifsRemain ds)
adamc@76 2124 else
adamc@76 2125 ();
adamc@76 2126
adamc@76 2127 case ListUtil.search cunifsInDecl ds of
adamc@76 2128 NONE => ()
adamc@76 2129 | SOME loc =>
adamc@91 2130 declError env (CunifsRemain ds)
adamc@76 2131 );
adamc@76 2132
adamc@83 2133 (ds, (env, gs))
adamc@76 2134 end
adamc@76 2135
adamc@83 2136 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
adamc@56 2137 in
adamc@84 2138 if ErrorMsg.anyErrors () then
adamc@84 2139 ()
adamc@84 2140 else
adamc@90 2141 app (fn (loc, env, denv, c1, c2) =>
adamc@84 2142 case D.prove env denv (c1, c2, loc) of
adamc@84 2143 [] => ()
adamc@84 2144 | _ =>
adamc@86 2145 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
adamc@84 2146 eprefaces' [("Con 1", p_con env c1),
adamc@90 2147 ("Con 2", p_con env c2),
adamc@90 2148 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
adamc@90 2149 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) gs;
adamc@83 2150
adamc@56 2151 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
adamc@56 2152 end
adamc@2 2153
adamc@2 2154 end