Mercurial > urweb

annotate src/elaborate.sml @ 223:bbe5899a9585

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Queries back to working as well as before, after start of refactoring to support grouping
author Adam Chlipala <adamc@hcoop.net>
date Thu, 21 Aug 2008 12:49:29 -0400
parents 2b665e822e9a
children 19e5791923d0
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@172 40 structure IM = IntBinaryMap
adamc@175 41
adamc@175 42 structure SK = struct
adamc@175 43 type ord_key = string
adamc@175 44 val compare = String.compare
adamc@175 45 end
adamc@175 46
adamc@175 47 structure SS = BinarySetFn(SK)
adamc@175 48 structure SM = BinaryMapFn(SK)
adamc@62 49
adamc@210 50 val basis_r = ref 0
adamc@210 51
adamc@2 52 fun elabExplicitness e =
adamc@2 53 case e of
adamc@2 54 L.Explicit => L'.Explicit
adamc@2 55 | L.Implicit => L'.Implicit
adamc@2 56
adamc@2 57 fun occursKind r =
adamc@76 58 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
adamc@2 59 | _ => false)
adamc@2 60
adamc@3 61 datatype kunify_error =
adamc@2 62 KOccursCheckFailed of L'.kind * L'.kind
adamc@2 63 | KIncompatible of L'.kind * L'.kind
adamc@2 64
adamc@3 65 exception KUnify' of kunify_error
adamc@3 66
adamc@3 67 fun kunifyError err =
adamc@2 68 case err of
adamc@2 69 KOccursCheckFailed (k1, k2) =>
adamc@3 70 eprefaces "Kind occurs check failed"
adamc@3 71 [("Kind 1", p_kind k1),
adamc@3 72 ("Kind 2", p_kind k2)]
adamc@2 73 | KIncompatible (k1, k2) =>
adamc@3 74 eprefaces "Incompatible kinds"
adamc@3 75 [("Kind 1", p_kind k1),
adamc@3 76 ("Kind 2", p_kind k2)]
adamc@2 77
adamc@3 78 fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
adamc@2 79 let
adamc@3 80 fun err f = raise KUnify' (f (k1All, k2All))
adamc@2 81 in
adamc@2 82 case (k1, k2) of
adamc@2 83 (L'.KType, L'.KType) => ()
adamc@82 84 | (L'.KUnit, L'.KUnit) => ()
adamc@82 85
adamc@2 86 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
adamc@3 87 (unifyKinds' d1 d2;
adamc@3 88 unifyKinds' r1 r2)
adamc@2 89 | (L'.KName, L'.KName) => ()
adamc@3 90 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
adamc@207 91 | (L'.KTuple ks1, L'.KTuple ks2) =>
adamc@207 92 ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2))
adamc@207 93 handle ListPair.UnequalLengths => err KIncompatible)
adamc@2 94
adamc@2 95 | (L'.KError, _) => ()
adamc@2 96 | (_, L'.KError) => ()
adamc@2 97
adamc@76 98 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
adamc@76 99 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
adamc@2 100
adamc@76 101 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
adamc@2 102 if r1 = r2 then
adamc@2 103 ()
adamc@2 104 else
adamc@2 105 r1 := SOME k2All
adamc@2 106
adamc@76 107 | (L'.KUnif (_, _, r), _) =>
adamc@2 108 if occursKind r k2All then
adamc@2 109 err KOccursCheckFailed
adamc@2 110 else
adamc@2 111 r := SOME k2All
adamc@76 112 | (_, L'.KUnif (_, _, r)) =>
adamc@2 113 if occursKind r k1All then
adamc@2 114 err KOccursCheckFailed
adamc@2 115 else
adamc@2 116 r := SOME k1All
adamc@2 117
adamc@2 118 | _ => err KIncompatible
adamc@2 119 end
adamc@2 120
adamc@3 121 exception KUnify of L'.kind * L'.kind * kunify_error
adamc@3 122
adamc@3 123 fun unifyKinds k1 k2 =
adamc@3 124 unifyKinds' k1 k2
adamc@3 125 handle KUnify' err => raise KUnify (k1, k2, err)
adamc@3 126
adamc@3 127 datatype con_error =
adamc@3 128 UnboundCon of ErrorMsg.span * string
adamc@157 129 | UnboundDatatype of ErrorMsg.span * string
adamc@34 130 | UnboundStrInCon of ErrorMsg.span * string
adamc@3 131 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
adamc@67 132 | DuplicateField of ErrorMsg.span * string
adamc@207 133 | ProjBounds of L'.con * int
adamc@207 134 | ProjMismatch of L'.con * L'.kind
adamc@3 135
adamc@5 136 fun conError env err =
adamc@3 137 case err of
adamc@3 138 UnboundCon (loc, s) =>
adamc@3 139 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
adamc@157 140 | UnboundDatatype (loc, s) =>
adamc@157 141 ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
adamc@34 142 | UnboundStrInCon (loc, s) =>
adamc@34 143 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adamc@3 144 | WrongKind (c, k1, k2, kerr) =>
adamc@3 145 (ErrorMsg.errorAt (#2 c) "Wrong kind";
adamc@5 146 eprefaces' [("Constructor", p_con env c),
adamc@5 147 ("Have kind", p_kind k1),
adamc@5 148 ("Need kind", p_kind k2)];
adamc@3 149 kunifyError kerr)
adamc@67 150 | DuplicateField (loc, s) =>
adamc@67 151 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
adamc@207 152 | ProjBounds (c, n) =>
adamc@207 153 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
adamc@207 154 eprefaces' [("Constructor", p_con env c),
adamc@207 155 ("Index", Print.PD.string (Int.toString n))])
adamc@207 156 | ProjMismatch (c, k) =>
adamc@207 157 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
adamc@207 158 eprefaces' [("Constructor", p_con env c),
adamc@207 159 ("Kind", p_kind k)])
adamc@3 160
adamc@5 161 fun checkKind env c k1 k2 =
adamc@3 162 unifyKinds k1 k2
adamc@3 163 handle KUnify (k1, k2, err) =>
adamc@5 164 conError env (WrongKind (c, k1, k2, err))
adamc@3 165
adamc@3 166 val dummy = ErrorMsg.dummySpan
adamc@3 167
adamc@3 168 val ktype = (L'.KType, dummy)
adamc@3 169 val kname = (L'.KName, dummy)
adamc@12 170 val ktype_record = (L'.KRecord ktype, dummy)
adamc@3 171
adamc@3 172 val cerror = (L'.CError, dummy)
adamc@3 173 val kerror = (L'.KError, dummy)
adamc@10 174 val eerror = (L'.EError, dummy)
adamc@31 175 val sgnerror = (L'.SgnError, dummy)
adamc@31 176 val strerror = (L'.StrError, dummy)
adamc@3 177
adamc@56 178 val int = ref cerror
adamc@56 179 val float = ref cerror
adamc@56 180 val string = ref cerror
adamc@203 181 val table = ref cerror
adamc@56 182
adamc@3 183 local
adamc@3 184 val count = ref 0
adamc@3 185 in
adamc@3 186
adamc@3 187 fun resetKunif () = count := 0
adamc@3 188
adamc@76 189 fun kunif loc =
adamc@3 190 let
adamc@3 191 val n = !count
adamc@3 192 val s = if n <= 26 then
adamc@3 193 str (chr (ord #"A" + n))
adamc@3 194 else
adamc@3 195 "U" ^ Int.toString (n - 26)
adamc@3 196 in
adamc@3 197 count := n + 1;
adamc@76 198 (L'.KUnif (loc, s, ref NONE), dummy)
adamc@3 199 end
adamc@3 200
adamc@3 201 end
adamc@3 202
adamc@10 203 local
adamc@10 204 val count = ref 0
adamc@10 205 in
adamc@10 206
adamc@10 207 fun resetCunif () = count := 0
adamc@10 208
adamc@76 209 fun cunif (loc, k) =
adamc@10 210 let
adamc@10 211 val n = !count
adamc@10 212 val s = if n <= 26 then
adamc@10 213 str (chr (ord #"A" + n))
adamc@10 214 else
adamc@10 215 "U" ^ Int.toString (n - 26)
adamc@10 216 in
adamc@10 217 count := n + 1;
adamc@76 218 (L'.CUnif (loc, k, s, ref NONE), dummy)
adamc@10 219 end
adamc@10 220
adamc@10 221 end
adamc@10 222
adamc@18 223 fun elabKind (k, loc) =
adamc@18 224 case k of
adamc@18 225 L.KType => (L'.KType, loc)
adamc@18 226 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
adamc@18 227 | L.KName => (L'.KName, loc)
adamc@18 228 | L.KRecord k => (L'.KRecord (elabKind k), loc)
adamc@82 229 | L.KUnit => (L'.KUnit, loc)
adamc@207 230 | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
adamc@76 231 | L.KWild => kunif loc
adamc@18 232
adamc@67 233 fun foldKind (dom, ran, loc)=
adamc@67 234 (L'.KArrow ((L'.KArrow ((L'.KName, loc),
adamc@67 235 (L'.KArrow (dom,
adamc@67 236 (L'.KArrow (ran, ran), loc)), loc)), loc),
adamc@67 237 (L'.KArrow (ran,
adamc@67 238 (L'.KArrow ((L'.KRecord dom, loc),
adamc@67 239 ran), loc)), loc)), loc)
adamc@67 240
adamc@207 241 fun hnormKind (kAll as (k, _)) =
adamc@207 242 case k of
adamc@207 243 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
adamc@207 244 | _ => kAll
adamc@207 245
adamc@83 246 fun elabCon (env, denv) (c, loc) =
adamc@3 247 case c of
adamc@3 248 L.CAnnot (c, k) =>
adamc@3 249 let
adamc@3 250 val k' = elabKind k
adamc@83 251 val (c', ck, gs) = elabCon (env, denv) c
adamc@3 252 in
adamc@5 253 checkKind env c' ck k';
adamc@83 254 (c', k', gs)
adamc@3 255 end
adamc@3 256
adamc@3 257 | L.TFun (t1, t2) =>
adamc@3 258 let
adamc@83 259 val (t1', k1, gs1) = elabCon (env, denv) t1
adamc@83 260 val (t2', k2, gs2) = elabCon (env, denv) t2
adamc@3 261 in
adamc@5 262 checkKind env t1' k1 ktype;
adamc@5 263 checkKind env t2' k2 ktype;
adamc@83 264 ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2)
adamc@3 265 end
adamc@3 266 | L.TCFun (e, x, k, t) =>
adamc@3 267 let
adamc@3 268 val e' = elabExplicitness e
adamc@3 269 val k' = elabKind k
adamc@3 270 val env' = E.pushCRel env x k'
adamc@83 271 val (t', tk, gs) = elabCon (env', D.enter denv) t
adamc@3 272 in
adamc@5 273 checkKind env t' tk ktype;
adamc@83 274 ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
adamc@3 275 end
adamc@85 276 | L.TDisjoint (c1, c2, c) =>
adamc@85 277 let
adamc@85 278 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@85 279 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@85 280
adamc@85 281 val ku1 = kunif loc
adamc@85 282 val ku2 = kunif loc
adamc@85 283
adamc@90 284 val (denv', gs3) = D.assert env denv (c1', c2')
adamc@90 285 val (c', k, gs4) = elabCon (env, denv') c
adamc@85 286 in
adamc@85 287 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@85 288 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@85 289
adamc@90 290 ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
adamc@85 291 end
adamc@3 292 | L.TRecord c =>
adamc@3 293 let
adamc@83 294 val (c', ck, gs) = elabCon (env, denv) c
adamc@3 295 val k = (L'.KRecord ktype, loc)
adamc@3 296 in
adamc@5 297 checkKind env c' ck k;
adamc@83 298 ((L'.TRecord c', loc), ktype, gs)
adamc@3 299 end
adamc@3 300
adamc@34 301 | L.CVar ([], s) =>
adamc@3 302 (case E.lookupC env s of
adamc@9 303 E.NotBound =>
adamc@5 304 (conError env (UnboundCon (loc, s));
adamc@83 305 (cerror, kerror, []))
adamc@9 306 | E.Rel (n, k) =>
adamc@83 307 ((L'.CRel n, loc), k, [])
adamc@9 308 | E.Named (n, k) =>
adamc@83 309 ((L'.CNamed n, loc), k, []))
adamc@34 310 | L.CVar (m1 :: ms, s) =>
adamc@34 311 (case E.lookupStr env m1 of
adamc@42 312 NONE => (conError env (UnboundStrInCon (loc, m1));
adamc@83 313 (cerror, kerror, []))
adamc@34 314 | SOME (n, sgn) =>
adamc@34 315 let
adamc@34 316 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@34 317 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@34 318 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@34 319 (strerror, sgnerror))
adamc@34 320 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@34 321 ((L'.StrVar n, loc), sgn) ms
adamc@34 322
adamc@34 323 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
adamc@34 324 NONE => (conError env (UnboundCon (loc, s));
adamc@34 325 kerror)
adamc@34 326 | SOME (k, _) => k
adamc@34 327 in
adamc@83 328 ((L'.CModProj (n, ms, s), loc), k, [])
adamc@34 329 end)
adamc@34 330
adamc@3 331 | L.CApp (c1, c2) =>
adamc@3 332 let
adamc@83 333 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@83 334 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@76 335 val dom = kunif loc
adamc@76 336 val ran = kunif loc
adamc@3 337 in
adamc@5 338 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
adamc@5 339 checkKind env c2' k2 dom;
adamc@83 340 ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2)
adamc@3 341 end
adamc@67 342 | L.CAbs (x, ko, t) =>
adamc@3 343 let
adamc@67 344 val k' = case ko of
adamc@76 345 NONE => kunif loc
adamc@67 346 | SOME k => elabKind k
adamc@3 347 val env' = E.pushCRel env x k'
adamc@83 348 val (t', tk, gs) = elabCon (env', D.enter denv) t
adamc@3 349 in
adamc@8 350 ((L'.CAbs (x, k', t'), loc),
adamc@83 351 (L'.KArrow (k', tk), loc),
adamc@83 352 gs)
adamc@3 353 end
adamc@3 354
adamc@84 355 | L.CDisjoint (c1, c2, c) =>
adamc@84 356 let
adamc@84 357 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@84 358 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@84 359
adamc@84 360 val ku1 = kunif loc
adamc@84 361 val ku2 = kunif loc
adamc@84 362
adamc@90 363 val (denv', gs3) = D.assert env denv (c1', c2')
adamc@90 364 val (c', k, gs4) = elabCon (env, denv') c
adamc@84 365 in
adamc@84 366 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@84 367 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@84 368
adamc@90 369 ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
adamc@84 370 end
adamc@84 371
adamc@3 372 | L.CName s =>
adamc@83 373 ((L'.CName s, loc), kname, [])
adamc@3 374
adamc@3 375 | L.CRecord xcs =>
adamc@3 376 let
adamc@76 377 val k = kunif loc
adamc@3 378
adamc@83 379 val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
adamc@83 380 let
adamc@83 381 val (x', xk, gs1) = elabCon (env, denv) x
adamc@83 382 val (c', ck, gs2) = elabCon (env, denv) c
adamc@83 383 in
adamc@83 384 checkKind env x' xk kname;
adamc@83 385 checkKind env c' ck k;
adamc@83 386 ((x', c'), gs1 @ gs2 @ gs)
adamc@83 387 end) [] xcs
adamc@67 388
adamc@67 389 val rc = (L'.CRecord (k, xcs'), loc)
adamc@67 390 (* Add duplicate field checking later. *)
adamc@83 391
adamc@83 392 fun prove (xcs, ds) =
adamc@83 393 case xcs of
adamc@83 394 [] => ds
adamc@83 395 | xc :: rest =>
adamc@83 396 let
adamc@83 397 val r1 = (L'.CRecord (k, [xc]), loc)
adamc@83 398 val ds = foldl (fn (xc', ds) =>
adamc@83 399 let
adamc@83 400 val r2 = (L'.CRecord (k, [xc']), loc)
adamc@83 401 in
adamc@90 402 D.prove env denv (r1, r2, loc) @ ds
adamc@83 403 end)
adamc@83 404 ds rest
adamc@83 405 in
adamc@83 406 prove (rest, ds)
adamc@83 407 end
adamc@3 408 in
adamc@83 409 (rc, (L'.KRecord k, loc), prove (xcs', gs))
adamc@3 410 end
adamc@3 411 | L.CConcat (c1, c2) =>
adamc@3 412 let
adamc@83 413 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@83 414 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@76 415 val ku = kunif loc
adamc@3 416 val k = (L'.KRecord ku, loc)
adamc@3 417 in
adamc@5 418 checkKind env c1' k1 k;
adamc@5 419 checkKind env c2' k2 k;
adamc@83 420 ((L'.CConcat (c1', c2'), loc), k,
adamc@90 421 D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
adamc@3 422 end
adamc@67 423 | L.CFold =>
adamc@67 424 let
adamc@76 425 val dom = kunif loc
adamc@76 426 val ran = kunif loc
adamc@67 427 in
adamc@67 428 ((L'.CFold (dom, ran), loc),
adamc@83 429 foldKind (dom, ran, loc),
adamc@83 430 [])
adamc@67 431 end
adamc@3 432
adamc@83 433 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
adamc@82 434
adamc@207 435 | L.CTuple cs =>
adamc@207 436 let
adamc@207 437 val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) =>
adamc@207 438 let
adamc@207 439 val (c', k, gs') = elabCon (env, denv) c
adamc@207 440 in
adamc@207 441 (c' :: cs', k :: ks, gs' @ gs)
adamc@207 442 end) ([], [], []) cs
adamc@207 443 in
adamc@207 444 ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs)
adamc@207 445 end
adamc@207 446 | L.CProj (c, n) =>
adamc@207 447 let
adamc@207 448 val (c', k, gs) = elabCon (env, denv) c
adamc@207 449 in
adamc@207 450 case hnormKind k of
adamc@207 451 (L'.KTuple ks, _) =>
adamc@207 452 if n <= 0 orelse n > length ks then
adamc@207 453 (conError env (ProjBounds (c', n));
adamc@207 454 (cerror, kerror, []))
adamc@207 455 else
adamc@207 456 ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs)
adamc@207 457 | k => (conError env (ProjMismatch (c', k));
adamc@207 458 (cerror, kerror, []))
adamc@207 459 end
adamc@207 460
adamc@18 461 | L.CWild k =>
adamc@18 462 let
adamc@18 463 val k' = elabKind k
adamc@18 464 in
adamc@83 465 (cunif (loc, k'), k', [])
adamc@18 466 end
adamc@18 467
adamc@6 468 fun kunifsRemain k =
adamc@6 469 case k of
adamc@76 470 L'.KUnif (_, _, ref NONE) => true
adamc@6 471 | _ => false
adamc@10 472 fun cunifsRemain c =
adamc@10 473 case c of
adamc@76 474 L'.CUnif (loc, _, _, ref NONE) => SOME loc
adamc@76 475 | _ => NONE
adamc@6 476
adamc@76 477 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
adamc@76 478 con = fn _ => false,
adamc@76 479 exp = fn _ => false,
adamc@76 480 sgn_item = fn _ => false,
adamc@76 481 sgn = fn _ => false,
adamc@76 482 str = fn _ => false,
adamc@76 483 decl = fn _ => false}
adamc@10 484
adamc@76 485 val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
adamc@76 486 con = cunifsRemain,
adamc@76 487 exp = fn _ => NONE,
adamc@76 488 sgn_item = fn _ => NONE,
adamc@76 489 sgn = fn _ => NONE,
adamc@76 490 str = fn _ => NONE,
adamc@76 491 decl = fn _ => NONE}
adamc@10 492
adamc@10 493 fun occursCon r =
adamc@10 494 U.Con.exists {kind = fn _ => false,
adamc@76 495 con = fn L'.CUnif (_, _, _, r') => r = r'
adamc@10 496 | _ => false}
adamc@10 497
adamc@10 498 datatype cunify_error =
adamc@10 499 CKind of L'.kind * L'.kind * kunify_error
adamc@10 500 | COccursCheckFailed of L'.con * L'.con
adamc@10 501 | CIncompatible of L'.con * L'.con
adamc@10 502 | CExplicitness of L'.con * L'.con
adamc@141 503 | CKindof of L'.kind * L'.con
adamc@153 504 | CRecordFailure of PD.pp_desc * PD.pp_desc
adamc@10 505
adamc@10 506 exception CUnify' of cunify_error
adamc@10 507
adamc@10 508 fun cunifyError env err =
adamc@10 509 case err of
adamc@10 510 CKind (k1, k2, kerr) =>
adamc@10 511 (eprefaces "Kind unification failure"
adamc@10 512 [("Kind 1", p_kind k1),
adamc@10 513 ("Kind 2", p_kind k2)];
adamc@10 514 kunifyError kerr)
adamc@10 515 | COccursCheckFailed (c1, c2) =>
adamc@10 516 eprefaces "Constructor occurs check failed"
adamc@10 517 [("Con 1", p_con env c1),
adamc@10 518 ("Con 2", p_con env c2)]
adamc@10 519 | CIncompatible (c1, c2) =>
adamc@10 520 eprefaces "Incompatible constructors"
adamc@10 521 [("Con 1", p_con env c1),
adamc@10 522 ("Con 2", p_con env c2)]
adamc@10 523 | CExplicitness (c1, c2) =>
adamc@10 524 eprefaces "Differing constructor function explicitness"
adamc@10 525 [("Con 1", p_con env c1),
adamc@10 526 ("Con 2", p_con env c2)]
adamc@141 527 | CKindof (k, c) =>
adamc@147 528 eprefaces "Unexpected kind for kindof calculation"
adamc@141 529 [("Kind", p_kind k),
adamc@141 530 ("Con", p_con env c)]
adamc@153 531 | CRecordFailure (s1, s2) =>
adamc@153 532 eprefaces "Can't unify record constructors"
adamc@153 533 [("Summary 1", s1),
adamc@153 534 ("Summary 2", s2)]
adamc@10 535
adamc@13 536 exception SynUnif = E.SynUnif
adamc@12 537
adamc@81 538 open ElabOps
adamc@43 539
adamc@12 540 type record_summary = {
adamc@12 541 fields : (L'.con * L'.con) list,
adamc@12 542 unifs : (L'.con * L'.con option ref) list,
adamc@12 543 others : L'.con list
adamc@12 544 }
adamc@12 545
adamc@12 546 fun summaryToCon {fields, unifs, others} =
adamc@12 547 let
adamc@12 548 val c = (L'.CRecord (ktype, []), dummy)
adamc@12 549 val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
adamc@12 550 val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
adamc@12 551 in
adamc@12 552 (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
adamc@12 553 end
adamc@12 554
adamc@12 555 fun p_summary env s = p_con env (summaryToCon s)
adamc@12 556
adamc@12 557 exception CUnify of L'.con * L'.con * cunify_error
adamc@12 558
adamc@12 559 fun kindof env (c, loc) =
adamc@12 560 case c of
adamc@12 561 L'.TFun _ => ktype
adamc@12 562 | L'.TCFun _ => ktype
adamc@85 563 | L'.TDisjoint _ => ktype
adamc@12 564 | L'.TRecord _ => ktype
adamc@12 565
adamc@12 566 | L'.CRel xn => #2 (E.lookupCRel env xn)
adamc@12 567 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
adamc@34 568 | L'.CModProj (n, ms, x) =>
adamc@34 569 let
adamc@34 570 val (_, sgn) = E.lookupStrNamed env n
adamc@34 571 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@34 572 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@34 573 NONE => raise Fail "kindof: Unknown substructure"
adamc@34 574 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@34 575 ((L'.StrVar n, loc), sgn) ms
adamc@34 576 in
adamc@34 577 case E.projectCon env {sgn = sgn, str = str, field = x} of
adamc@34 578 NONE => raise Fail "kindof: Unknown con in structure"
adamc@34 579 | SOME (k, _) => k
adamc@34 580 end
adamc@34 581
adamc@12 582 | L'.CApp (c, _) =>
adamc@141 583 (case hnormKind (kindof env c) of
adamc@141 584 (L'.KArrow (_, k), _) => k
adamc@141 585 | (L'.KError, _) => kerror
adamc@141 586 | k => raise CUnify' (CKindof (k, c)))
adamc@12 587 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
adamc@84 588 | L'.CDisjoint (_, _, c) => kindof env c
adamc@12 589
adamc@12 590 | L'.CName _ => kname
adamc@12 591
adamc@12 592 | L'.CRecord (k, _) => (L'.KRecord k, loc)
adamc@12 593 | L'.CConcat (c, _) => kindof env c
adamc@67 594 | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
adamc@12 595
adamc@82 596 | L'.CUnit => (L'.KUnit, loc)
adamc@82 597
adamc@207 598 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
adamc@207 599 | L'.CProj (c, n) =>
adamc@207 600 (case hnormKind (kindof env c) of
adamc@207 601 (L'.KTuple ks, _) => List.nth (ks, n - 1)
adamc@207 602 | k => raise CUnify' (CKindof (k, c)))
adamc@207 603
adamc@12 604 | L'.CError => kerror
adamc@76 605 | L'.CUnif (_, k, _, _) => k
adamc@12 606
adamc@90 607 val hnormCon = D.hnormCon
adamc@86 608
adamc@205 609 datatype con_summary =
adamc@205 610 Nil
adamc@205 611 | Cons
adamc@205 612 | Unknown
adamc@205 613
adamc@205 614 fun compatible cs =
adamc@205 615 case cs of
adamc@205 616 (Unknown, _) => false
adamc@205 617 | (_, Unknown) => false
adamc@205 618 | (s1, s2) => s1 = s2
adamc@205 619
adamc@205 620 fun summarizeCon (env, denv) c =
adamc@205 621 let
adamc@205 622 val (c, gs) = hnormCon (env, denv) c
adamc@205 623 in
adamc@205 624 case #1 c of
adamc@205 625 L'.CRecord (_, []) => (Nil, gs)
adamc@205 626 | L'.CRecord (_, _ :: _) => (Cons, gs)
adamc@205 627 | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
adamc@205 628 | L'.CDisjoint (_, _, c) =>
adamc@205 629 let
adamc@205 630 val (s, gs') = summarizeCon (env, denv) c
adamc@205 631 in
adamc@205 632 (s, gs @ gs')
adamc@205 633 end
adamc@205 634 | _ => (Unknown, gs)
adamc@205 635 end
adamc@205 636
adamc@205 637 fun p_con_summary s =
adamc@205 638 Print.PD.string (case s of
adamc@205 639 Nil => "Nil"
adamc@205 640 | Cons => "Cons"
adamc@205 641 | Unknown => "Unknown")
adamc@205 642
adamc@223 643 exception SummaryFailure
adamc@223 644
adamc@86 645 fun unifyRecordCons (env, denv) (c1, c2) =
adamc@12 646 let
adamc@92 647 fun rkindof c =
adamc@147 648 case hnormKind (kindof env c) of
adamc@92 649 (L'.KRecord k, _) => k
adamc@141 650 | (L'.KError, _) => kerror
adamc@141 651 | k => raise CUnify' (CKindof (k, c))
adamc@92 652
adamc@92 653 val k1 = rkindof c1
adamc@92 654 val k2 = rkindof c2
adamc@86 655
adamc@86 656 val (r1, gs1) = recordSummary (env, denv) c1
adamc@86 657 val (r2, gs2) = recordSummary (env, denv) c2
adamc@12 658 in
adamc@12 659 unifyKinds k1 k2;
adamc@86 660 unifySummaries (env, denv) (k1, r1, r2);
adamc@86 661 gs1 @ gs2
adamc@12 662 end
adamc@12 663
adamc@86 664 and recordSummary (env, denv) c =
adamc@86 665 let
adamc@86 666 val (c, gs) = hnormCon (env, denv) c
adamc@12 667
adamc@86 668 val (sum, gs') =
adamc@86 669 case c of
adamc@86 670 (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, [])
adamc@86 671 | (L'.CConcat (c1, c2), _) =>
adamc@86 672 let
adamc@86 673 val (s1, gs1) = recordSummary (env, denv) c1
adamc@86 674 val (s2, gs2) = recordSummary (env, denv) c2
adamc@86 675 in
adamc@86 676 ({fields = #fields s1 @ #fields s2,
adamc@86 677 unifs = #unifs s1 @ #unifs s2,
adamc@86 678 others = #others s1 @ #others s2},
adamc@86 679 gs1 @ gs2)
adamc@86 680 end
adamc@86 681 | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c
adamc@86 682 | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, [])
adamc@86 683 | c' => ({fields = [], unifs = [], others = [c']}, [])
adamc@86 684 in
adamc@86 685 (sum, gs @ gs')
adamc@86 686 end
adamc@86 687
adamc@86 688 and consEq (env, denv) (c1, c2) =
adamc@209 689 let
adamc@209 690 val gs = unifyCons (env, denv) c1 c2
adamc@209 691 in
adamc@209 692 List.all (fn (loc, env, denv, c1, c2) =>
adamc@209 693 case D.prove env denv (c1, c2, loc) of
adamc@209 694 [] => true
adamc@209 695 | _ => false) gs
adamc@209 696 end
adamc@12 697 handle CUnify _ => false
adamc@12 698
adamc@80 699 and consNeq env (c1, c2) =
adamc@86 700 case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of
adamc@80 701 (L'.CName x1, L'.CName x2) => x1 <> x2
adamc@80 702 | _ => false
adamc@80 703
adamc@86 704 and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) =
adamc@12 705 let
adamc@223 706 val loc = #2 k
adamc@14 707 (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
adamc@223 708 ("#2", p_summary env s2)]*)
adamc@12 709
adamc@12 710 fun eatMatching p (ls1, ls2) =
adamc@12 711 let
adamc@12 712 fun em (ls1, ls2, passed1) =
adamc@12 713 case ls1 of
adamc@12 714 [] => (rev passed1, ls2)
adamc@12 715 | h1 :: t1 =>
adamc@12 716 let
adamc@12 717 fun search (ls2', passed2) =
adamc@12 718 case ls2' of
adamc@12 719 [] => em (t1, ls2, h1 :: passed1)
adamc@12 720 | h2 :: t2 =>
adamc@12 721 if p (h1, h2) then
adamc@12 722 em (t1, List.revAppend (passed2, t2), passed1)
adamc@12 723 else
adamc@12 724 search (t2, h2 :: passed2)
adamc@12 725 in
adamc@12 726 search (ls2, [])
adamc@12 727 end
adamc@12 728 in
adamc@12 729 em (ls1, ls2, [])
adamc@12 730 end
adamc@12 731
adamc@12 732 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
adamc@80 733 not (consNeq env (x1, x2))
adamc@86 734 andalso consEq (env, denv) (c1, c2)
adamc@86 735 andalso consEq (env, denv) (x1, x2))
adamc@79 736 (#fields s1, #fields s2)
adamc@14 737 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
adamc@223 738 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
adamc@12 739 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
adamc@86 740 val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2)
adamc@223 741 (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
adamc@223 742 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
adamc@12 743
adamc@12 744 fun unifFields (fs, others, unifs) =
adamc@12 745 case (fs, others, unifs) of
adamc@12 746 ([], [], _) => ([], [], unifs)
adamc@12 747 | (_, _, []) => (fs, others, [])
adamc@12 748 | (_, _, (_, r) :: rest) =>
adamc@12 749 let
adamc@12 750 val r' = ref NONE
adamc@141 751 val kr = (L'.KRecord k, dummy)
adamc@141 752 val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy)
adamc@12 753
adamc@12 754 val prefix = case (fs, others) of
adamc@12 755 ([], other :: others) =>
adamc@12 756 List.foldl (fn (other, c) =>
adamc@12 757 (L'.CConcat (c, other), dummy))
adamc@12 758 other others
adamc@12 759 | (fs, []) =>
adamc@12 760 (L'.CRecord (k, fs), dummy)
adamc@12 761 | (fs, others) =>
adamc@12 762 List.foldl (fn (other, c) =>
adamc@12 763 (L'.CConcat (c, other), dummy))
adamc@12 764 (L'.CRecord (k, fs), dummy) others
adamc@12 765 in
adamc@12 766 r := SOME (L'.CConcat (prefix, cr'), dummy);
adamc@12 767 ([], [], (cr', r') :: rest)
adamc@12 768 end
adamc@12 769
adamc@12 770 val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
adamc@12 771 val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
adamc@12 772
adamc@223 773 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
adamc@223 774 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
adamc@223 775
adamc@223 776 fun isGuessable (other, fs) =
adamc@223 777 let
adamc@223 778 val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure)
adamc@223 779 in
adamc@223 780 List.all (fn (loc, env, denv, c1, c2) =>
adamc@223 781 case D.prove env denv (c1, c2, loc) of
adamc@223 782 [] => true
adamc@223 783 | _ => false) gs
adamc@223 784 end
adamc@223 785 handle SummaryFailure => false
adamc@223 786
adamc@223 787 val (fs1, fs2, others1, others2) =
adamc@223 788 case (fs1, fs2, others1, others2) of
adamc@223 789 ([], _, [other1], []) =>
adamc@223 790 if isGuessable (other1, fs2) then
adamc@223 791 ([], [], [], [])
adamc@223 792 else
adamc@223 793 (fs1, fs2, others1, others2)
adamc@223 794 | _ => (fs1, fs2, others1, others2)
adamc@223 795
adamc@223 796 (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
adamc@223 797 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
adamc@223 798
adamc@86 799 val clear = case (fs1, others1, fs2, others2) of
adamc@86 800 ([], [], [], []) => true
adamc@12 801 | _ => false
adamc@12 802 val empty = (L'.CRecord (k, []), dummy)
adamc@223 803
adamc@12 804 fun pairOffUnifs (unifs1, unifs2) =
adamc@12 805 case (unifs1, unifs2) of
adamc@12 806 ([], _) =>
adamc@86 807 if clear then
adamc@12 808 List.app (fn (_, r) => r := SOME empty) unifs2
adamc@12 809 else
adamc@153 810 raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2))
adamc@12 811 | (_, []) =>
adamc@86 812 if clear then
adamc@12 813 List.app (fn (_, r) => r := SOME empty) unifs1
adamc@12 814 else
adamc@153 815 raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2))
adamc@12 816 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
adamc@12 817 (r2 := SOME c1;
adamc@12 818 pairOffUnifs (rest1, rest2))
adamc@12 819 in
adamc@12 820 pairOffUnifs (unifs1, unifs2)
adamc@223 821 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
adamc@223 822 ("#2", p_summary env s2)]*)
adamc@223 823 end
adamc@223 824
adamc@223 825 and guessFold (env, denv) (c1, c2, gs, ex) =
adamc@223 826 let
adamc@223 827 val loc = #2 c1
adamc@223 828
adamc@223 829 fun unfold (dom, ran, f, i, r, c) =
adamc@223 830 let
adamc@223 831 val nm = cunif (loc, (L'.KName, loc))
adamc@223 832 val v = cunif (loc, dom)
adamc@223 833 val rest = cunif (loc, (L'.KRecord dom, loc))
adamc@223 834 val acc = (L'.CFold (dom, ran), loc)
adamc@223 835 val acc = (L'.CApp (acc, f), loc)
adamc@223 836 val acc = (L'.CApp (acc, i), loc)
adamc@223 837 val acc = (L'.CApp (acc, rest), loc)
adamc@223 838
adamc@223 839 val (iS, gs3) = summarizeCon (env, denv) i
adamc@223 840
adamc@223 841 val app = (L'.CApp (f, nm), loc)
adamc@223 842 val app = (L'.CApp (app, v), loc)
adamc@223 843 val app = (L'.CApp (app, acc), loc)
adamc@223 844 val (appS, gs4) = summarizeCon (env, denv) app
adamc@223 845
adamc@223 846 val (cS, gs5) = summarizeCon (env, denv) c
adamc@223 847 in
adamc@223 848 (*prefaces "Summaries" [("iS", p_con_summary iS),
adamc@223 849 ("appS", p_con_summary appS),
adamc@223 850 ("cS", p_con_summary cS)];*)
adamc@223 851
adamc@223 852 if compatible (iS, appS) then
adamc@223 853 raise ex
adamc@223 854 else if compatible (cS, iS) then
adamc@223 855 let
adamc@223 856 (*val () = prefaces "Same?" [("i", p_con env i),
adamc@223 857 ("c", p_con env c)]*)
adamc@223 858 val gs6 = unifyCons (env, denv) i c
adamc@223 859 (*val () = TextIO.print "Yes!\n"*)
adamc@223 860
adamc@223 861 val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
adamc@223 862 in
adamc@223 863 gs @ gs3 @ gs5 @ gs6 @ gs7
adamc@223 864 end
adamc@223 865 else if compatible (cS, appS) then
adamc@223 866 let
adamc@223 867 (*val () = prefaces "Same?" [("app", p_con env app),
adamc@223 868 ("c", p_con env c),
adamc@223 869 ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*)
adamc@223 870 val gs6 = unifyCons (env, denv) app c
adamc@223 871 (*val () = TextIO.print "Yes!\n"*)
adamc@223 872
adamc@223 873 val singleton = (L'.CRecord (dom, [(nm, v)]), loc)
adamc@223 874 val concat = (L'.CConcat (singleton, rest), loc)
adamc@223 875 (*val () = prefaces "Pre-crew" [("r", p_con env r),
adamc@223 876 ("concat", p_con env concat)]*)
adamc@223 877 val gs7 = unifyCons (env, denv) r concat
adamc@223 878 in
adamc@223 879 (*prefaces "The crew" [("nm", p_con env nm),
adamc@223 880 ("v", p_con env v),
adamc@223 881 ("rest", p_con env rest)];*)
adamc@223 882
adamc@223 883 gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7
adamc@223 884 end
adamc@223 885 else
adamc@223 886 raise ex
adamc@223 887 end
adamc@223 888 handle _ => raise ex
adamc@223 889 in
adamc@223 890 case (#1 c1, #1 c2) of
adamc@223 891 (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) =>
adamc@223 892 unfold (dom, ran, f, i, r, c2)
adamc@223 893 | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) =>
adamc@223 894 unfold (dom, ran, f, i, r, c1)
adamc@223 895 | _ => raise ex
adamc@12 896 end
adamc@12 897
adamc@86 898 and unifyCons' (env, denv) c1 c2 =
adamc@86 899 let
adamc@86 900 val (c1, gs1) = hnormCon (env, denv) c1
adamc@86 901 val (c2, gs2) = hnormCon (env, denv) c2
adamc@86 902 in
adamc@205 903 let
adamc@205 904 val gs3 = unifyCons'' (env, denv) c1 c2
adamc@205 905 in
adamc@205 906 gs1 @ gs2 @ gs3
adamc@205 907 end
adamc@223 908 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
adamc@86 909 end
adamc@11 910
adamc@205 911 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
adamc@10 912 let
adamc@210 913 fun err f = raise CUnify' (f (c1All, c2All))
adamc@12 914
adamc@86 915 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
adamc@10 916 in
adamc@92 917 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
adamc@92 918 ("c2All", p_con env c2All)];*)
adamc@92 919
adamc@10 920 case (c1, c2) of
adamc@88 921 (L'.CUnit, L'.CUnit) => []
adamc@88 922
adamc@88 923 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
adamc@86 924 unifyCons' (env, denv) d1 d2
adamc@86 925 @ unifyCons' (env, denv) r1 r2
adamc@10 926 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
adamc@10 927 if expl1 <> expl2 then
adamc@10 928 err CExplicitness
adamc@10 929 else
adamc@10 930 (unifyKinds d1 d2;
adamc@86 931 unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2)
adamc@86 932 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2
adamc@10 933
adamc@10 934 | (L'.CRel n1, L'.CRel n2) =>
adamc@10 935 if n1 = n2 then
adamc@86 936 []
adamc@10 937 else
adamc@10 938 err CIncompatible
adamc@10 939 | (L'.CNamed n1, L'.CNamed n2) =>
adamc@10 940 if n1 = n2 then
adamc@86 941 []
adamc@10 942 else
adamc@10 943 err CIncompatible
adamc@10 944
adamc@10 945 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
adamc@86 946 (unifyCons' (env, denv) d1 d2;
adamc@86 947 unifyCons' (env, denv) r1 r2)
adamc@10 948 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
adamc@10 949 (unifyKinds k1 k2;
adamc@86 950 unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
adamc@10 951
adamc@10 952 | (L'.CName n1, L'.CName n2) =>
adamc@10 953 if n1 = n2 then
adamc@86 954 []
adamc@10 955 else
adamc@10 956 err CIncompatible
adamc@10 957
adamc@34 958 | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
adamc@34 959 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
adamc@86 960 []
adamc@34 961 else
adamc@34 962 err CIncompatible
adamc@34 963
adamc@207 964 | (L'.CTuple cs1, L'.CTuple cs2) =>
adamc@207 965 ((ListPair.foldlEq (fn (c1, c2, gs) =>
adamc@207 966 let
adamc@207 967 val gs' = unifyCons' (env, denv) c1 c2
adamc@207 968 in
adamc@207 969 gs' @ gs
adamc@207 970 end) [] (cs1, cs2))
adamc@207 971 handle ListPair.UnequalLengths => err CIncompatible)
adamc@207 972 | (L'.CProj (c1, n1), L'.CProj (c2, n2)) =>
adamc@207 973 if n1 = n2 then
adamc@207 974 unifyCons' (env, denv) c1 c2
adamc@207 975 else
adamc@207 976 err CIncompatible
adamc@207 977
adamc@86 978 | (L'.CError, _) => []
adamc@86 979 | (_, L'.CError) => []
adamc@10 980
adamc@92 981 | (L'.CRecord _, _) => isRecord ()
adamc@92 982 | (_, L'.CRecord _) => isRecord ()
adamc@92 983 | (L'.CConcat _, _) => isRecord ()
adamc@92 984 | (_, L'.CConcat _) => isRecord ()
adamc@10 985
adamc@76 986 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
adamc@10 987 if r1 = r2 then
adamc@86 988 []
adamc@10 989 else
adamc@10 990 (unifyKinds k1 k2;
adamc@86 991 r1 := SOME c2All;
adamc@86 992 [])
adamc@10 993
adamc@76 994 | (L'.CUnif (_, _, _, r), _) =>
adamc@10 995 if occursCon r c2All then
adamc@10 996 err COccursCheckFailed
adamc@10 997 else
adamc@86 998 (r := SOME c2All;
adamc@86 999 [])
adamc@76 1000 | (_, L'.CUnif (_, _, _, r)) =>
adamc@10 1001 if occursCon r c1All then
adamc@10 1002 err COccursCheckFailed
adamc@10 1003 else
adamc@86 1004 (r := SOME c1All;
adamc@86 1005 [])
adamc@10 1006
adamc@71 1007 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) =>
adamc@71 1008 (unifyKinds dom1 dom2;
adamc@86 1009 unifyKinds ran1 ran2;
adamc@86 1010 [])
adamc@71 1011
adamc@10 1012 | _ => err CIncompatible
adamc@10 1013 end
adamc@10 1014
adamc@86 1015 and unifyCons (env, denv) c1 c2 =
adamc@86 1016 unifyCons' (env, denv) c1 c2
adamc@10 1017 handle CUnify' err => raise CUnify (c1, c2, err)
adamc@10 1018 | KUnify args => raise CUnify (c1, c2, CKind args)
adamc@10 1019
adamc@10 1020 datatype exp_error =
adamc@10 1021 UnboundExp of ErrorMsg.span * string
adamc@34 1022 | UnboundStrInExp of ErrorMsg.span * string
adamc@10 1023 | Unify of L'.exp * L'.con * L'.con * cunify_error
adamc@11 1024 | Unif of string * L'.con
adamc@11 1025 | WrongForm of string * L'.exp * L'.con
adamc@92 1026 | IncompatibleCons of L'.con * L'.con
adamc@171 1027 | DuplicatePatternVariable of ErrorMsg.span * string
adamc@171 1028 | PatUnify of L'.pat * L'.con * L'.con * cunify_error
adamc@174 1029 | UnboundConstructor of ErrorMsg.span * string list * string
adamc@171 1030 | PatHasArg of ErrorMsg.span
adamc@171 1031 | PatHasNoArg of ErrorMsg.span
adamc@172 1032 | Inexhaustive of ErrorMsg.span
adamc@175 1033 | DuplicatePatField of ErrorMsg.span * string
adamc@211 1034 | Unresolvable of ErrorMsg.span * L'.con
adamc@220 1035 | OutOfContext of ErrorMsg.span * (L'.exp * L'.con) option
adamc@10 1036
adamc@10 1037 fun expError env err =
adamc@10 1038 case err of
adamc@10 1039 UnboundExp (loc, s) =>
adamc@10 1040 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
adamc@34 1041 | UnboundStrInExp (loc, s) =>
adamc@34 1042 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
adamc@10 1043 | Unify (e, c1, c2, uerr) =>
adamc@10 1044 (ErrorMsg.errorAt (#2 e) "Unification failure";
adamc@10 1045 eprefaces' [("Expression", p_exp env e),
adamc@10 1046 ("Have con", p_con env c1),
adamc@10 1047 ("Need con", p_con env c2)];
adamc@10 1048 cunifyError env uerr)
adamc@11 1049 | Unif (action, c) =>
adamc@11 1050 (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action);
adamc@11 1051 eprefaces' [("Con", p_con env c)])
adamc@11 1052 | WrongForm (variety, e, t) =>
adamc@11 1053 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
adamc@11 1054 eprefaces' [("Expression", p_exp env e),
adamc@11 1055 ("Type", p_con env t)])
adamc@92 1056 | IncompatibleCons (c1, c2) =>
adamc@92 1057 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
adamc@92 1058 eprefaces' [("Con 1", p_con env c1),
adamc@92 1059 ("Con 2", p_con env c2)])
adamc@171 1060 | DuplicatePatternVariable (loc, s) =>
adamc@171 1061 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
adamc@171 1062 | PatUnify (p, c1, c2, uerr) =>
adamc@171 1063 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
adamc@171 1064 eprefaces' [("Pattern", p_pat env p),
adamc@171 1065 ("Have con", p_con env c1),
adamc@171 1066 ("Need con", p_con env c2)];
adamc@171 1067 cunifyError env uerr)
adamc@174 1068 | UnboundConstructor (loc, ms, s) =>
adamc@174 1069 ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
adamc@171 1070 | PatHasArg loc =>
adamc@171 1071 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
adamc@171 1072 | PatHasNoArg loc =>
adamc@171 1073 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
adamc@172 1074 | Inexhaustive loc =>
adamc@172 1075 ErrorMsg.errorAt loc "Inexhaustive 'case'"
adamc@175 1076 | DuplicatePatField (loc, s) =>
adamc@175 1077 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
adamc@220 1078 | OutOfContext (loc, co) =>
adamc@220 1079 (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
adamc@220 1080 Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
adamc@220 1081 ("Type", p_con env c)]) co)
adamc@211 1082 | Unresolvable (loc, c) =>
adamc@211 1083 (ErrorMsg.errorAt loc "Can't resolve type class instance";
adamc@211 1084 eprefaces' [("Class constraint", p_con env c)])
adamc@210 1085
adamc@86 1086 fun checkCon (env, denv) e c1 c2 =
adamc@86 1087 unifyCons (env, denv) c1 c2
adamc@10 1088 handle CUnify (c1, c2, err) =>
adamc@86 1089 (expError env (Unify (e, c1, c2, err));
adamc@86 1090 [])
adamc@10 1091
adamc@171 1092 fun checkPatCon (env, denv) p c1 c2 =
adamc@171 1093 unifyCons (env, denv) c1 c2
adamc@171 1094 handle CUnify (c1, c2, err) =>
adamc@171 1095 (expError env (PatUnify (p, c1, c2, err));
adamc@171 1096 [])
adamc@171 1097
adamc@14 1098 fun primType env p =
adamc@56 1099 case p of
adamc@56 1100 P.Int _ => !int
adamc@56 1101 | P.Float _ => !float
adamc@56 1102 | P.String _ => !string
adamc@14 1103
adamc@71 1104 fun recCons (k, nm, v, rest, loc) =
adamc@71 1105 (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
adamc@71 1106 rest), loc)
adamc@71 1107
adamc@71 1108 fun foldType (dom, loc) =
adamc@71 1109 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
adamc@71 1110 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
adamc@71 1111 (L'.TCFun (L'.Explicit, "v", dom,
adamc@71 1112 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
adamc@71 1113 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
adamc@71 1114 (L'.CApp ((L'.CRel 3, loc),
adamc@71 1115 recCons (dom,
adamc@71 1116 (L'.CRel 2, loc),
adamc@71 1117 (L'.CRel 1, loc),
adamc@71 1118 (L'.CRel 0, loc),
adamc@71 1119 loc)), loc)), loc)),
adamc@71 1120 loc)), loc)), loc),
adamc@71 1121 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
adamc@71 1122 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
adamc@71 1123 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
adamc@71 1124 loc)), loc)), loc)
adamc@71 1125
adamc@86 1126 fun elabHead (env, denv) (e as (_, loc)) t =
adamc@15 1127 let
adamc@15 1128 fun unravel (t, e) =
adamc@86 1129 let
adamc@86 1130 val (t, gs) = hnormCon (env, denv) t
adamc@86 1131 in
adamc@86 1132 case t of
adamc@86 1133 (L'.TCFun (L'.Implicit, x, k, t'), _) =>
adamc@86 1134 let
adamc@86 1135 val u = cunif (loc, k)
adamc@86 1136
adamc@86 1137 val (e, t, gs') = unravel (subConInCon (0, u) t',
adamc@86 1138 (L'.ECApp (e, u), loc))
adamc@86 1139 in
adamc@86 1140 (e, t, gs @ gs')
adamc@86 1141 end
adamc@86 1142 | _ => (e, t, gs)
adamc@86 1143 end
adamc@15 1144 in
adamc@15 1145 unravel (t, e)
adamc@15 1146 end
adamc@15 1147
adamc@174 1148 fun elabPat (pAll as (p, loc), (env, denv, bound)) =
adamc@171 1149 let
adamc@171 1150 val perror = (L'.PWild, loc)
adamc@171 1151 val terror = (L'.CError, loc)
adamc@171 1152 val pterror = (perror, terror)
adamc@171 1153 val rerror = (pterror, (env, bound))
adamc@171 1154
adamc@191 1155 fun pcon (pc, po, xs, to, dn, dk) =
adamc@188 1156 case (po, to) of
adamc@188 1157 (NONE, SOME _) => (expError env (PatHasNoArg loc);
adamc@188 1158 rerror)
adamc@188 1159 | (SOME _, NONE) => (expError env (PatHasArg loc);
adamc@188 1160 rerror)
adamc@191 1161 | (NONE, NONE) =>
adamc@191 1162 let
adamc@191 1163 val k = (L'.KType, loc)
adamc@191 1164 val unifs = map (fn _ => cunif (loc, k)) xs
adamc@191 1165 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
adamc@191 1166 in
adamc@191 1167 (((L'.PCon (dk, pc, unifs, NONE), loc), dn),
adamc@191 1168 (env, bound))
adamc@191 1169 end
adamc@188 1170 | (SOME p, SOME t) =>
adamc@188 1171 let
adamc@188 1172 val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
adamc@191 1173
adamc@191 1174 val k = (L'.KType, loc)
adamc@191 1175 val unifs = map (fn _ => cunif (loc, k)) xs
adamc@194 1176 val nxs = length unifs - 1
adamc@194 1177 val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs
adamc@191 1178 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
adamc@188 1179 in
adamc@191 1180 ignore (checkPatCon (env, denv) p' pt t);
adamc@191 1181 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
adamc@188 1182 (env, bound))
adamc@188 1183 end
adamc@171 1184 in
adamc@171 1185 case p of
adamc@171 1186 L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
adamc@171 1187 (env, bound))
adamc@171 1188 | L.PVar x =>
adamc@171 1189 let
adamc@171 1190 val t = if SS.member (bound, x) then
adamc@171 1191 (expError env (DuplicatePatternVariable (loc, x));
adamc@171 1192 terror)
adamc@171 1193 else
adamc@171 1194 cunif (loc, (L'.KType, loc))
adamc@171 1195 in
adamc@182 1196 (((L'.PVar (x, t), loc), t),
adamc@171 1197 (E.pushERel env x t, SS.add (bound, x)))
adamc@171 1198 end
adamc@173 1199 | L.PPrim p => (((L'.PPrim p, loc), primType env p),
adamc@173 1200 (env, bound))
adamc@171 1201 | L.PCon ([], x, po) =>
adamc@171 1202 (case E.lookupConstructor env x of
adamc@174 1203 NONE => (expError env (UnboundConstructor (loc, [], x));
adamc@171 1204 rerror)
adamc@191 1205 | SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk))
adamc@174 1206 | L.PCon (m1 :: ms, x, po) =>
adamc@174 1207 (case E.lookupStr env m1 of
adamc@174 1208 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@174 1209 rerror)
adamc@174 1210 | SOME (n, sgn) =>
adamc@174 1211 let
adamc@174 1212 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@174 1213 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@182 1214 NONE => raise Fail "elabPat: Unknown substructure"
adamc@174 1215 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@174 1216 ((L'.StrVar n, loc), sgn) ms
adamc@174 1217 in
adamc@174 1218 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
adamc@174 1219 NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
adamc@174 1220 rerror)
adamc@191 1221 | SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk)
adamc@174 1222 end)
adamc@174 1223
adamc@175 1224 | L.PRecord (xps, flex) =>
adamc@175 1225 let
adamc@175 1226 val (xpts, (env, bound, _)) =
adamc@175 1227 ListUtil.foldlMap (fn ((x, p), (env, bound, fbound)) =>
adamc@175 1228 let
adamc@175 1229 val ((p', t), (env, bound)) = elabPat (p, (env, denv, bound))
adamc@175 1230 in
adamc@175 1231 if SS.member (fbound, x) then
adamc@175 1232 expError env (DuplicatePatField (loc, x))
adamc@175 1233 else
adamc@175 1234 ();
adamc@175 1235 ((x, p', t), (env, bound, SS.add (fbound, x)))
adamc@175 1236 end)
adamc@175 1237 (env, bound, SS.empty) xps
adamc@175 1238
adamc@175 1239 val k = (L'.KType, loc)
adamc@175 1240 val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc)
adamc@176 1241 val c =
adamc@175 1242 if flex then
adamc@176 1243 (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc)
adamc@175 1244 else
adamc@176 1245 c
adamc@175 1246 in
adamc@182 1247 (((L'.PRecord xpts, loc),
adamc@175 1248 (L'.TRecord c, loc)),
adamc@175 1249 (env, bound))
adamc@175 1250 end
adamc@175 1251
adamc@171 1252 end
adamc@171 1253
adamc@172 1254 datatype coverage =
adamc@172 1255 Wild
adamc@173 1256 | None
adamc@172 1257 | Datatype of coverage IM.map
adamc@175 1258 | Record of coverage SM.map list
adamc@172 1259
adamc@172 1260 fun exhaustive (env, denv, t, ps) =
adamc@172 1261 let
adamc@172 1262 fun pcCoverage pc =
adamc@172 1263 case pc of
adamc@172 1264 L'.PConVar n => n
adamc@174 1265 | L'.PConProj (m1, ms, x) =>
adamc@174 1266 let
adamc@174 1267 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@174 1268 in
adamc@174 1269 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
adamc@174 1270 NONE => raise Fail "exhaustive: Can't project constructor"
adamc@191 1271 | SOME (_, n, _, _, _) => n
adamc@174 1272 end
adamc@172 1273
adamc@172 1274 fun coverage (p, _) =
adamc@172 1275 case p of
adamc@172 1276 L'.PWild => Wild
adamc@172 1277 | L'.PVar _ => Wild
adamc@173 1278 | L'.PPrim _ => None
adamc@191 1279 | L'.PCon (_, pc, _, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
adamc@191 1280 | L'.PCon (_, pc, _, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
adamc@182 1281 | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) =>
adamc@182 1282 SM.insert (fmap, x, coverage p)) SM.empty xps]
adamc@176 1283
adamc@172 1284 fun merge (c1, c2) =
adamc@172 1285 case (c1, c2) of
adamc@173 1286 (None, _) => c2
adamc@173 1287 | (_, None) => c1
adamc@173 1288
adamc@173 1289 | (Wild, _) => Wild
adamc@172 1290 | (_, Wild) => Wild
adamc@172 1291
adamc@172 1292 | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2))
adamc@172 1293
adamc@175 1294 | (Record fm1, Record fm2) => Record (fm1 @ fm2)
adamc@175 1295
adamc@175 1296 | _ => None
adamc@175 1297
adamc@172 1298 fun combinedCoverage ps =
adamc@172 1299 case ps of
adamc@172 1300 [] => raise Fail "Empty pattern list for coverage checking"
adamc@172 1301 | [p] => coverage p
adamc@172 1302 | p :: ps => merge (coverage p, combinedCoverage ps)
adamc@172 1303
adamc@175 1304 fun enumerateCases t =
adamc@175 1305 let
adamc@175 1306 fun dtype cons =
adamc@175 1307 ListUtil.mapConcat (fn (_, n, to) =>
adamc@175 1308 case to of
adamc@175 1309 NONE => [Datatype (IM.insert (IM.empty, n, Wild))]
adamc@175 1310 | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c)))
adamc@175 1311 (enumerateCases t)) cons
adamc@175 1312 in
adamc@175 1313 case #1 (#1 (hnormCon (env, denv) t)) of
adamc@175 1314 L'.CNamed n =>
adamc@175 1315 (let
adamc@175 1316 val dt = E.lookupDatatype env n
adamc@175 1317 val cons = E.constructors dt
adamc@175 1318 in
adamc@175 1319 dtype cons
adamc@175 1320 end handle E.UnboundNamed _ => [Wild])
adamc@175 1321 | L'.TRecord c =>
adamc@175 1322 (case #1 (#1 (hnormCon (env, denv) c)) of
adamc@175 1323 L'.CRecord (_, xts) =>
adamc@175 1324 let
adamc@175 1325 val xts = map (fn (x, t) => (#1 (hnormCon (env, denv) x), t)) xts
adamc@175 1326
adamc@175 1327 fun exponentiate fs =
adamc@175 1328 case fs of
adamc@175 1329 [] => [SM.empty]
adamc@175 1330 | ((L'.CName x, _), t) :: rest =>
adamc@175 1331 let
adamc@175 1332 val this = enumerateCases t
adamc@175 1333 val rest = exponentiate rest
adamc@175 1334 in
adamc@175 1335 ListUtil.mapConcat (fn fmap =>
adamc@175 1336 map (fn c => SM.insert (fmap, x, c)) this) rest
adamc@175 1337 end
adamc@175 1338 | _ => raise Fail "exponentiate: Not CName"
adamc@175 1339 in
adamc@175 1340 if List.exists (fn ((L'.CName _, _), _) => false
adamc@175 1341 | (c, _) => true) xts then
adamc@175 1342 [Wild]
adamc@175 1343 else
adamc@175 1344 map (fn ls => Record [ls]) (exponentiate xts)
adamc@175 1345 end
adamc@175 1346 | _ => [Wild])
adamc@175 1347 | _ => [Wild]
adamc@175 1348 end
adamc@175 1349
adamc@175 1350 fun coverageImp (c1, c2) =
adamc@175 1351 case (c1, c2) of
adamc@175 1352 (Wild, _) => true
adamc@175 1353
adamc@175 1354 | (Datatype cmap1, Datatype cmap2) =>
adamc@175 1355 List.all (fn (n, c2) =>
adamc@175 1356 case IM.find (cmap1, n) of
adamc@175 1357 NONE => false
adamc@175 1358 | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2)
adamc@175 1359
adamc@175 1360 | (Record fmaps1, Record fmaps2) =>
adamc@175 1361 List.all (fn fmap2 =>
adamc@175 1362 List.exists (fn fmap1 =>
adamc@175 1363 List.all (fn (x, c2) =>
adamc@175 1364 case SM.find (fmap1, x) of
adamc@175 1365 NONE => true
adamc@175 1366 | SOME c1 => coverageImp (c1, c2))
adamc@175 1367 (SM.listItemsi fmap2))
adamc@175 1368 fmaps1) fmaps2
adamc@175 1369
adamc@175 1370 | _ => false
adamc@175 1371
adamc@172 1372 fun isTotal (c, t) =
adamc@172 1373 case c of
adamc@173 1374 None => (false, [])
adamc@173 1375 | Wild => (true, [])
adamc@172 1376 | Datatype cm =>
adamc@172 1377 let
adamc@172 1378 val ((t, _), gs) = hnormCon (env, denv) t
adamc@174 1379
adamc@174 1380 fun dtype cons =
adamc@174 1381 foldl (fn ((_, n, to), (total, gs)) =>
adamc@174 1382 case IM.find (cm, n) of
adamc@174 1383 NONE => (false, gs)
adamc@174 1384 | SOME c' =>
adamc@174 1385 case to of
adamc@174 1386 NONE => (total, gs)
adamc@174 1387 | SOME t' =>
adamc@174 1388 let
adamc@174 1389 val (total, gs') = isTotal (c', t')
adamc@174 1390 in
adamc@174 1391 (total, gs' @ gs)
adamc@174 1392 end)
adamc@174 1393 (true, gs) cons
adamc@191 1394
adamc@191 1395 fun unapp t =
adamc@191 1396 case t of
adamc@191 1397 L'.CApp ((t, _), _) => unapp t
adamc@191 1398 | _ => t
adamc@172 1399 in
adamc@191 1400 case unapp t of
adamc@172 1401 L'.CNamed n =>
adamc@172 1402 let
adamc@172 1403 val dt = E.lookupDatatype env n
adamc@172 1404 val cons = E.constructors dt
adamc@172 1405 in
adamc@174 1406 dtype cons
adamc@174 1407 end
adamc@174 1408 | L'.CModProj (m1, ms, x) =>
adamc@174 1409 let
adamc@174 1410 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@174 1411 in
adamc@174 1412 case E.projectDatatype env {str = str, sgn = sgn, field = x} of
adamc@174 1413 NONE => raise Fail "isTotal: Can't project datatype"
adamc@191 1414 | SOME (_, cons) => dtype cons
adamc@172 1415 end
adamc@172 1416 | L'.CError => (true, gs)
adamc@172 1417 | _ => raise Fail "isTotal: Not a datatype"
adamc@172 1418 end
adamc@175 1419 | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases t), [])
adamc@172 1420 in
adamc@172 1421 isTotal (combinedCoverage ps, t)
adamc@172 1422 end
adamc@172 1423
adamc@217 1424 fun unmodCon env (c, loc) =
adamc@217 1425 case c of
adamc@217 1426 L'.CNamed n =>
adamc@217 1427 (case E.lookupCNamed env n of
adamc@217 1428 (_, _, SOME (c as (L'.CModProj _, _))) => unmodCon env c
adamc@217 1429 | _ => (c, loc))
adamc@217 1430 | L'.CModProj (m1, ms, x) =>
adamc@217 1431 let
adamc@217 1432 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@217 1433 in
adamc@217 1434 case E.projectCon env {str = str, sgn = sgn, field = x} of
adamc@217 1435 NONE => raise Fail "unmodCon: Can't projectCon"
adamc@217 1436 | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c
adamc@217 1437 | _ => (c, loc)
adamc@217 1438 end
adamc@217 1439 | _ => (c, loc)
adamc@217 1440
adamc@217 1441 fun normClassConstraint envs (c, loc) =
adamc@217 1442 case c of
adamc@217 1443 L'.CApp (f, x) =>
adamc@217 1444 let
adamc@217 1445 val f = unmodCon (#1 envs) f
adamc@217 1446 val (x, gs) = hnormCon envs x
adamc@217 1447 in
adamc@217 1448 ((L'.CApp (f, x), loc), gs)
adamc@217 1449 end
adamc@217 1450 | _ => ((c, loc), [])
adamc@216 1451
adamc@92 1452 fun elabExp (env, denv) (eAll as (e, loc)) =
adamc@91 1453 let
adamc@92 1454
adamc@92 1455 in
adamc@92 1456 (*eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
adamc@10 1457
adamc@91 1458 case e of
adamc@91 1459 L.EAnnot (e, t) =>
adamc@91 1460 let
adamc@91 1461 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 1462 val (t', _, gs2) = elabCon (env, denv) t
adamc@91 1463 val gs3 = checkCon (env, denv) e' et t'
adamc@91 1464 in
adamc@91 1465 (e', t', gs1 @ gs2 @ gs3)
adamc@91 1466 end
adamc@34 1467
adamc@91 1468 | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
adamc@91 1469 | L.EVar ([], s) =>
adamc@91 1470 (case E.lookupE env s of
adamc@91 1471 E.NotBound =>
adamc@91 1472 (expError env (UnboundExp (loc, s));
adamc@91 1473 (eerror, cerror, []))
adamc@91 1474 | E.Rel (n, t) => ((L'.ERel n, loc), t, [])
adamc@191 1475 | E.Named (n, t) =>
adamc@191 1476 if Char.isUpper (String.sub (s, 0)) then
adamc@191 1477 elabHead (env, denv) (L'.ENamed n, loc) t
adamc@191 1478 else
adamc@191 1479 ((L'.ENamed n, loc), t, []))
adamc@91 1480 | L.EVar (m1 :: ms, s) =>
adamc@91 1481 (case E.lookupStr env m1 of
adamc@91 1482 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@91 1483 (eerror, cerror, []))
adamc@91 1484 | SOME (n, sgn) =>
adamc@91 1485 let
adamc@91 1486 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@91 1487 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@91 1488 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@91 1489 (strerror, sgnerror))
adamc@91 1490 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@91 1491 ((L'.StrVar n, loc), sgn) ms
adamc@10 1492
adamc@91 1493 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
adamc@91 1494 NONE => (expError env (UnboundExp (loc, s));
adamc@91 1495 cerror)
adamc@91 1496 | SOME t => t
adamc@91 1497 in
adamc@91 1498 ((L'.EModProj (n, ms, s), loc), t, [])
adamc@91 1499 end)
adamc@86 1500
adamc@211 1501 | L.EApp (e1, (L.EWild, _)) =>
adamc@210 1502 let
adamc@210 1503 val (e1', t1, gs1) = elabExp (env, denv) e1
adamc@210 1504 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
adamc@210 1505 val (t1, gs3) = hnormCon (env, denv) t1
adamc@210 1506 in
adamc@210 1507 case t1 of
adamc@211 1508 (L'.TFun (dom, ran), _) =>
adamc@216 1509 let
adamc@216 1510 val (dom, gs4) = normClassConstraint (env, denv) dom
adamc@216 1511 in
adamc@216 1512 case E.resolveClass env dom of
adamc@216 1513 NONE => (expError env (Unresolvable (loc, dom));
adamc@216 1514 (eerror, cerror, []))
adamc@216 1515 | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ gs3 @ gs4)
adamc@216 1516 end
adamc@220 1517 | _ => (expError env (OutOfContext (loc, SOME (e1', t1)));
adamc@211 1518 (eerror, cerror, []))
adamc@210 1519 end
adamc@220 1520 | L.EWild => (expError env (OutOfContext (loc, NONE));
adamc@211 1521 (eerror, cerror, []))
adamc@210 1522
adamc@91 1523 | L.EApp (e1, e2) =>
adamc@91 1524 let
adamc@91 1525 val (e1', t1, gs1) = elabExp (env, denv) e1
adamc@91 1526 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
adamc@91 1527 val (e2', t2, gs3) = elabExp (env, denv) e2
adamc@71 1528
adamc@91 1529 val dom = cunif (loc, ktype)
adamc@91 1530 val ran = cunif (loc, ktype)
adamc@91 1531 val t = (L'.TFun (dom, ran), dummy)
adamc@91 1532
adamc@91 1533 val gs4 = checkCon (env, denv) e1' t1 t
adamc@91 1534 val gs5 = checkCon (env, denv) e2' t2 dom
adamc@205 1535
adamc@205 1536 val gs = gs1 @ gs2 @ gs3 @ gs4 @ gs5
adamc@91 1537 in
adamc@205 1538 ((L'.EApp (e1', e2'), loc), ran, gs)
adamc@91 1539 end
adamc@91 1540 | L.EAbs (x, to, e) =>
adamc@91 1541 let
adamc@91 1542 val (t', gs1) = case to of
adamc@91 1543 NONE => (cunif (loc, ktype), [])
adamc@91 1544 | SOME t =>
adamc@91 1545 let
adamc@91 1546 val (t', tk, gs) = elabCon (env, denv) t
adamc@91 1547 in
adamc@91 1548 checkKind env t' tk ktype;
adamc@91 1549 (t', gs)
adamc@91 1550 end
adamc@91 1551 val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e
adamc@91 1552 in
adamc@91 1553 ((L'.EAbs (x, t', et, e'), loc),
adamc@91 1554 (L'.TFun (t', et), loc),
adamc@91 1555 gs1 @ gs2)
adamc@91 1556 end
adamc@91 1557 | L.ECApp (e, c) =>
adamc@91 1558 let
adamc@91 1559 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 1560 val (e', et, gs2) = elabHead (env, denv) e' et
adamc@91 1561 val (c', ck, gs3) = elabCon (env, denv) c
adamc@91 1562 val ((et', _), gs4) = hnormCon (env, denv) et
adamc@91 1563 in
adamc@91 1564 case et' of
adamc@91 1565 L'.CError => (eerror, cerror, [])
adamc@91 1566 | L'.TCFun (_, _, k, eb) =>
adamc@91 1567 let
adamc@91 1568 val () = checkKind env c' ck k
adamc@91 1569 val eb' = subConInCon (0, c') eb
adamc@91 1570 handle SynUnif => (expError env (Unif ("substitution", eb));
adamc@91 1571 cerror)
adamc@91 1572 in
adamc@91 1573 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
adamc@91 1574 end
adamc@91 1575
adamc@91 1576 | L'.CUnif _ =>
adamc@91 1577 (expError env (Unif ("application", et));
adamc@91 1578 (eerror, cerror, []))
adamc@91 1579
adamc@91 1580 | _ =>
adamc@91 1581 (expError env (WrongForm ("constructor function", e', et));
adamc@91 1582 (eerror, cerror, []))
adamc@91 1583 end
adamc@91 1584 | L.ECAbs (expl, x, k, e) =>
adamc@91 1585 let
adamc@91 1586 val expl' = elabExplicitness expl
adamc@91 1587 val k' = elabKind k
adamc@91 1588 val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
adamc@91 1589 in
adamc@91 1590 ((L'.ECAbs (expl', x, k', e'), loc),
adamc@91 1591 (L'.TCFun (expl', x, k', et), loc),
adamc@91 1592 gs)
adamc@91 1593 end
adamc@91 1594
adamc@91 1595 | L.EDisjoint (c1, c2, e) =>
adamc@91 1596 let
adamc@91 1597 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@91 1598 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@91 1599
adamc@91 1600 val ku1 = kunif loc
adamc@91 1601 val ku2 = kunif loc
adamc@91 1602
adamc@91 1603 val (denv', gs3) = D.assert env denv (c1', c2')
adamc@91 1604 val (e', t, gs4) = elabExp (env, denv') e
adamc@91 1605 in
adamc@91 1606 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@91 1607 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@91 1608
adamc@91 1609 (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
adamc@91 1610 end
adamc@91 1611
adamc@91 1612 | L.ERecord xes =>
adamc@91 1613 let
adamc@91 1614 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
adamc@91 1615 let
adamc@91 1616 val (x', xk, gs1) = elabCon (env, denv) x
adamc@91 1617 val (e', et, gs2) = elabExp (env, denv) e
adamc@91 1618 in
adamc@91 1619 checkKind env x' xk kname;
adamc@91 1620 ((x', e', et), gs1 @ gs2 @ gs)
adamc@91 1621 end)
adamc@91 1622 [] xes
adamc@91 1623
adamc@91 1624 val k = (L'.KType, loc)
adamc@91 1625
adamc@91 1626 fun prove (xets, gs) =
adamc@91 1627 case xets of
adamc@91 1628 [] => gs
adamc@91 1629 | (x, _, t) :: rest =>
adamc@91 1630 let
adamc@91 1631 val xc = (x, t)
adamc@91 1632 val r1 = (L'.CRecord (k, [xc]), loc)
adamc@91 1633 val gs = foldl (fn ((x', _, t'), gs) =>
adamc@91 1634 let
adamc@91 1635 val xc' = (x', t')
adamc@91 1636 val r2 = (L'.CRecord (k, [xc']), loc)
adamc@91 1637 in
adamc@91 1638 D.prove env denv (r1, r2, loc) @ gs
adamc@91 1639 end)
adamc@91 1640 gs rest
adamc@91 1641 in
adamc@91 1642 prove (rest, gs)
adamc@91 1643 end
adamc@91 1644 in
adamc@91 1645 ((L'.ERecord xes', loc),
adamc@91 1646 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
adamc@91 1647 prove (xes', gs))
adamc@91 1648 end
adamc@91 1649
adamc@91 1650 | L.EField (e, c) =>
adamc@91 1651 let
adamc@91 1652 val (e', et, gs1) = elabExp (env, denv) e
adamc@91 1653 val (c', ck, gs2) = elabCon (env, denv) c
adamc@91 1654
adamc@91 1655 val ft = cunif (loc, ktype)
adamc@91 1656 val rest = cunif (loc, ktype_record)
adamc@91 1657 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
adamc@91 1658
adamc@91 1659 val gs3 =
adamc@91 1660 checkCon (env, denv) e' et
adamc@91 1661 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
adamc@91 1662 val gs4 = D.prove env denv (first, rest, loc)
adamc@91 1663 in
adamc@91 1664 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
adamc@91 1665 end
adamc@91 1666
adamc@149 1667 | L.ECut (e, c) =>
adamc@149 1668 let
adamc@149 1669 val (e', et, gs1) = elabExp (env, denv) e
adamc@149 1670 val (c', ck, gs2) = elabCon (env, denv) c
adamc@149 1671
adamc@149 1672 val ft = cunif (loc, ktype)
adamc@149 1673 val rest = cunif (loc, ktype_record)
adamc@149 1674 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
adamc@149 1675
adamc@149 1676 val gs3 =
adamc@149 1677 checkCon (env, denv) e' et
adamc@149 1678 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
adamc@149 1679 val gs4 = D.prove env denv (first, rest, loc)
adamc@149 1680 in
adamc@149 1681 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), gs1 @ gs2 @ gs3 @ gs4)
adamc@149 1682 end
adamc@149 1683
adamc@91 1684 | L.EFold =>
adamc@91 1685 let
adamc@91 1686 val dom = kunif loc
adamc@91 1687 in
adamc@91 1688 ((L'.EFold dom, loc), foldType (dom, loc), [])
adamc@91 1689 end
adamc@170 1690
adamc@171 1691 | L.ECase (e, pes) =>
adamc@171 1692 let
adamc@171 1693 val (e', et, gs1) = elabExp (env, denv) e
adamc@171 1694 val result = cunif (loc, (L'.KType, loc))
adamc@171 1695 val (pes', gs) = ListUtil.foldlMap
adamc@171 1696 (fn ((p, e), gs) =>
adamc@171 1697 let
adamc@174 1698 val ((p', pt), (env, _)) = elabPat (p, (env, denv, SS.empty))
adamc@171 1699
adamc@171 1700 val gs1 = checkPatCon (env, denv) p' pt et
adamc@171 1701 val (e', et, gs2) = elabExp (env, denv) e
adamc@171 1702 val gs3 = checkCon (env, denv) e' et result
adamc@171 1703 in
adamc@171 1704 ((p', e'), gs1 @ gs2 @ gs3 @ gs)
adamc@171 1705 end)
adamc@171 1706 gs1 pes
adamc@172 1707
adamc@172 1708 val (total, gs') = exhaustive (env, denv, et, map #1 pes')
adamc@171 1709 in
adamc@172 1710 if total then
adamc@172 1711 ()
adamc@172 1712 else
adamc@172 1713 expError env (Inexhaustive loc);
adamc@172 1714
adamc@182 1715 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs' @ gs)
adamc@171 1716 end
adamc@91 1717 end
adamc@12 1718
adamc@12 1719
adamc@6 1720 datatype decl_error =
adamc@91 1721 KunifsRemain of L'.decl list
adamc@91 1722 | CunifsRemain of L'.decl list
adamc@91 1723
adamc@91 1724 fun lspan [] = ErrorMsg.dummySpan
adamc@91 1725 | lspan ((_, loc) :: _) = loc
adamc@6 1726
adamc@6 1727 fun declError env err =
adamc@6 1728 case err of
adamc@91 1729 KunifsRemain ds =>
adamc@91 1730 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
adamc@91 1731 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@91 1732 | CunifsRemain ds =>
adamc@91 1733 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
adamc@91 1734 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@6 1735
adamc@31 1736 datatype sgn_error =
adamc@31 1737 UnboundSgn of ErrorMsg.span * string
adamc@31 1738 | UnmatchedSgi of L'.sgn_item
adamc@31 1739 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
adamc@31 1740 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
adamc@156 1741 | SgiMismatchedDatatypes of L'.sgn_item * L'.sgn_item * (L'.con * L'.con * cunify_error) option
adamc@41 1742 | SgnWrongForm of L'.sgn * L'.sgn
adamc@42 1743 | UnWhereable of L'.sgn * string
adamc@75 1744 | WhereWrongKind of L'.kind * L'.kind * kunify_error
adamc@58 1745 | NotIncludable of L'.sgn
adamc@62 1746 | DuplicateCon of ErrorMsg.span * string
adamc@62 1747 | DuplicateVal of ErrorMsg.span * string
adamc@62 1748 | DuplicateSgn of ErrorMsg.span * string
adamc@62 1749 | DuplicateStr of ErrorMsg.span * string
adamc@88 1750 | NotConstraintsable of L'.sgn
adamc@31 1751
adamc@31 1752 fun sgnError env err =
adamc@31 1753 case err of
adamc@31 1754 UnboundSgn (loc, s) =>
adamc@31 1755 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
adamc@31 1756 | UnmatchedSgi (sgi as (_, loc)) =>
adamc@31 1757 (ErrorMsg.errorAt loc "Unmatched signature item";
adamc@31 1758 eprefaces' [("Item", p_sgn_item env sgi)])
adamc@31 1759 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
adamc@31 1760 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
adamc@59 1761 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@59 1762 ("Need", p_sgn_item env sgi2),
adamc@31 1763 ("Kind 1", p_kind k1),
adamc@31 1764 ("Kind 2", p_kind k2)];
adamc@31 1765 kunifyError kerr)
adamc@31 1766 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
adamc@31 1767 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
adamc@59 1768 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@59 1769 ("Need", p_sgn_item env sgi2),
adamc@31 1770 ("Con 1", p_con env c1),
adamc@31 1771 ("Con 2", p_con env c2)];
adamc@31 1772 cunifyError env cerr)
adamc@156 1773 | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
adamc@156 1774 (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
adamc@156 1775 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@156 1776 ("Need", p_sgn_item env sgi2)];
adamc@156 1777 Option.app (fn (c1, c2, ue) =>
adamc@156 1778 (eprefaces "Unification error"
adamc@156 1779 [("Con 1", p_con env c1),
adamc@156 1780 ("Con 2", p_con env c2)];
adamc@156 1781 cunifyError env ue)) cerro)
adamc@41 1782 | SgnWrongForm (sgn1, sgn2) =>
adamc@41 1783 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
adamc@41 1784 eprefaces' [("Sig 1", p_sgn env sgn1),
adamc@41 1785 ("Sig 2", p_sgn env sgn2)])
adamc@42 1786 | UnWhereable (sgn, x) =>
adamc@42 1787 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
adamc@42 1788 eprefaces' [("Signature", p_sgn env sgn),
adamc@42 1789 ("Field", PD.string x)])
adamc@75 1790 | WhereWrongKind (k1, k2, kerr) =>
adamc@75 1791 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
adamc@75 1792 eprefaces' [("Have", p_kind k1),
adamc@75 1793 ("Need", p_kind k2)];
adamc@75 1794 kunifyError kerr)
adamc@58 1795 | NotIncludable sgn =>
adamc@58 1796 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
adamc@58 1797 eprefaces' [("Signature", p_sgn env sgn)])
adamc@62 1798 | DuplicateCon (loc, s) =>
adamc@62 1799 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
adamc@62 1800 | DuplicateVal (loc, s) =>
adamc@62 1801 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
adamc@62 1802 | DuplicateSgn (loc, s) =>
adamc@62 1803 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
adamc@62 1804 | DuplicateStr (loc, s) =>
adamc@62 1805 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
adamc@88 1806 | NotConstraintsable sgn =>
adamc@88 1807 (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
adamc@88 1808 eprefaces' [("Signature", p_sgn env sgn)])
adamc@31 1809
adamc@31 1810 datatype str_error =
adamc@31 1811 UnboundStr of ErrorMsg.span * string
adamc@44 1812 | NotFunctor of L'.sgn
adamc@46 1813 | FunctorRebind of ErrorMsg.span
adamc@61 1814 | UnOpenable of L'.sgn
adamc@75 1815 | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
adamc@156 1816 | DuplicateConstructor of string * ErrorMsg.span
adamc@158 1817 | NotDatatype of ErrorMsg.span
adamc@31 1818
adamc@31 1819 fun strError env err =
adamc@31 1820 case err of
adamc@31 1821 UnboundStr (loc, s) =>
adamc@31 1822 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
adamc@44 1823 | NotFunctor sgn =>
adamc@44 1824 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
adamc@44 1825 eprefaces' [("Signature", p_sgn env sgn)])
adamc@46 1826 | FunctorRebind loc =>
adamc@46 1827 ErrorMsg.errorAt loc "Attempt to rebind functor"
adamc@61 1828 | UnOpenable sgn =>
adamc@61 1829 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
adamc@61 1830 eprefaces' [("Signature", p_sgn env sgn)])
adamc@75 1831 | NotType (k, (k1, k2, ue)) =>
adamc@75 1832 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
adamc@75 1833 eprefaces' [("Kind", p_kind k),
adamc@75 1834 ("Subkind 1", p_kind k1),
adamc@75 1835 ("Subkind 2", p_kind k2)];
adamc@75 1836 kunifyError ue)
adamc@156 1837 | DuplicateConstructor (x, loc) =>
adamc@156 1838 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
adamc@158 1839 | NotDatatype loc =>
adamc@158 1840 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
adamc@31 1841
adamc@42 1842 val hnormSgn = E.hnormSgn
adamc@31 1843
adamc@210 1844 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
adamc@205 1845
adamc@88 1846 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
adamc@76 1847 case sgi of
adamc@76 1848 L.SgiConAbs (x, k) =>
adamc@76 1849 let
adamc@76 1850 val k' = elabKind k
adamc@31 1851
adamc@76 1852 val (env', n) = E.pushCNamed env x k' NONE
adamc@76 1853 in
adamc@88 1854 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs))
adamc@76 1855 end
adamc@31 1856
adamc@76 1857 | L.SgiCon (x, ko, c) =>
adamc@76 1858 let
adamc@76 1859 val k' = case ko of
adamc@76 1860 NONE => kunif loc
adamc@76 1861 | SOME k => elabKind k
adamc@31 1862
adamc@83 1863 val (c', ck, gs') = elabCon (env, denv) c
adamc@76 1864 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@76 1865 in
adamc@76 1866 checkKind env c' ck k';
adamc@31 1867
adamc@88 1868 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
adamc@76 1869 end
adamc@31 1870
adamc@191 1871 | L.SgiDatatype (x, xs, xcs) =>
adamc@157 1872 let
adamc@157 1873 val k = (L'.KType, loc)
adamc@191 1874 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 1875 val (env, n) = E.pushCNamed env x k' NONE
adamc@157 1876 val t = (L'.CNamed n, loc)
adamc@194 1877 val nxs = length xs - 1
adamc@194 1878 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@157 1879
adamc@157 1880 val (xcs, (used, env, gs)) =
adamc@157 1881 ListUtil.foldlMap
adamc@157 1882 (fn ((x, to), (used, env, gs)) =>
adamc@157 1883 let
adamc@157 1884 val (to, t, gs') = case to of
adamc@157 1885 NONE => (NONE, t, gs)
adamc@157 1886 | SOME t' =>
adamc@157 1887 let
adamc@157 1888 val (t', tk, gs') = elabCon (env, denv) t'
adamc@157 1889 in
adamc@157 1890 checkKind env t' tk k;
adamc@157 1891 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
adamc@157 1892 end
adamc@191 1893 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
adamc@157 1894
adamc@157 1895 val (env, n') = E.pushENamed env x t
adamc@157 1896 in
adamc@157 1897 if SS.member (used, x) then
adamc@157 1898 strError env (DuplicateConstructor (x, loc))
adamc@157 1899 else
adamc@157 1900 ();
adamc@157 1901 ((x, n', to), (SS.add (used, x), env, gs'))
adamc@157 1902 end)
adamc@157 1903 (SS.empty, env, []) xcs
adamc@191 1904
adamc@191 1905 val env = E.pushDatatype env n xs xcs
adamc@157 1906 in
adamc@191 1907 ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
adamc@157 1908 end
adamc@156 1909
adamc@158 1910 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
adamc@158 1911
adamc@158 1912 | L.SgiDatatypeImp (x, m1 :: ms, s) =>
adamc@158 1913 (case E.lookupStr env m1 of
adamc@158 1914 NONE => (strError env (UnboundStr (loc, m1));
adamc@158 1915 ([], (env, denv, gs)))
adamc@158 1916 | SOME (n, sgn) =>
adamc@158 1917 let
adamc@158 1918 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@158 1919 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@158 1920 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@158 1921 (strerror, sgnerror))
adamc@158 1922 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@158 1923 ((L'.StrVar n, loc), sgn) ms
adamc@158 1924 in
adamc@161 1925 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
adamc@161 1926 ((L'.CModProj (n, ms, s), _), gs) =>
adamc@161 1927 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
adamc@161 1928 NONE => (conError env (UnboundDatatype (loc, s));
adamc@161 1929 ([], (env, denv, gs)))
adamc@191 1930 | SOME (xs, xncs) =>
adamc@161 1931 let
adamc@161 1932 val k = (L'.KType, loc)
adamc@191 1933 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 1934
adamc@161 1935 val t = (L'.CModProj (n, ms, s), loc)
adamc@191 1936 val (env, n') = E.pushCNamed env x k' (SOME t)
adamc@191 1937 val env = E.pushDatatype env n' xs xncs
adamc@158 1938
adamc@161 1939 val t = (L'.CNamed n', loc)
adamc@161 1940 val env = foldl (fn ((x, n, to), env) =>
adamc@161 1941 let
adamc@161 1942 val t = case to of
adamc@161 1943 NONE => t
adamc@161 1944 | SOME t' => (L'.TFun (t', t), loc)
adamc@191 1945
adamc@191 1946 val t = foldr (fn (x, t) =>
adamc@191 1947 (L'.TCFun (L'.Implicit, x, k, t), loc))
adamc@191 1948 t xs
adamc@161 1949 in
adamc@161 1950 E.pushENamedAs env x n t
adamc@161 1951 end) env xncs
adamc@161 1952 in
adamc@191 1953 ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
adamc@161 1954 end)
adamc@161 1955 | _ => (strError env (NotDatatype loc);
adamc@161 1956 ([], (env, denv, [])))
adamc@158 1957 end)
adamc@156 1958
adamc@76 1959 | L.SgiVal (x, c) =>
adamc@76 1960 let
adamc@83 1961 val (c', ck, gs') = elabCon (env, denv) c
adamc@31 1962
adamc@76 1963 val (env', n) = E.pushENamed env x c'
adamc@218 1964 val (c', gs'') = normClassConstraint (env, denv) c'
adamc@76 1965 in
adamc@76 1966 (unifyKinds ck ktype
adamc@76 1967 handle KUnify ue => strError env (NotType (ck, ue)));
adamc@31 1968
adamc@218 1969 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs'' @ gs))
adamc@76 1970 end
adamc@31 1971
adamc@76 1972 | L.SgiStr (x, sgn) =>
adamc@76 1973 let
adamc@83 1974 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 1975 val (env', n) = E.pushStrNamed env x sgn'
adamc@76 1976 in
adamc@88 1977 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 1978 end
adamc@31 1979
adamc@76 1980 | L.SgiSgn (x, sgn) =>
adamc@76 1981 let
adamc@83 1982 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 1983 val (env', n) = E.pushSgnNamed env x sgn'
adamc@76 1984 in
adamc@88 1985 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 1986 end
adamc@31 1987
adamc@76 1988 | L.SgiInclude sgn =>
adamc@76 1989 let
adamc@83 1990 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 1991 in
adamc@76 1992 case #1 (hnormSgn env sgn') of
adamc@76 1993 L'.SgnConst sgis =>
adamc@88 1994 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs))
adamc@76 1995 | _ => (sgnError env (NotIncludable sgn');
adamc@88 1996 ([], (env, denv, [])))
adamc@88 1997 end
adamc@88 1998
adamc@88 1999 | L.SgiConstraint (c1, c2) =>
adamc@88 2000 let
adamc@88 2001 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@88 2002 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@88 2003
adamc@90 2004 val (denv, gs3) = D.assert env denv (c1', c2')
adamc@88 2005 in
adamc@88 2006 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
adamc@88 2007 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
adamc@88 2008
adamc@90 2009 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
adamc@76 2010 end
adamc@31 2011
adamc@203 2012 | L.SgiTable (x, c) =>
adamc@203 2013 let
adamc@203 2014 val (c', k, gs) = elabCon (env, denv) c
adamc@210 2015 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
adamc@203 2016 in
adamc@203 2017 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
adamc@210 2018 ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs))
adamc@203 2019 end
adamc@203 2020
adamc@211 2021 | L.SgiClassAbs x =>
adamc@211 2022 let
adamc@211 2023 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
adamc@211 2024 val (env, n) = E.pushCNamed env x k NONE
adamc@211 2025 val env = E.pushClass env n
adamc@211 2026 in
adamc@211 2027 ([(L'.SgiClassAbs (x, n), loc)], (env, denv, []))
adamc@211 2028 end
adamc@211 2029
adamc@211 2030 | L.SgiClass (x, c) =>
adamc@211 2031 let
adamc@211 2032 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
adamc@211 2033 val (c', ck, gs) = elabCon (env, denv) c
adamc@211 2034 val (env, n) = E.pushCNamed env x k (SOME c')
adamc@211 2035 val env = E.pushClass env n
adamc@211 2036 in
adamc@211 2037 checkKind env c' ck k;
adamc@211 2038 ([(L'.SgiClass (x, n, c'), loc)], (env, denv, []))
adamc@211 2039 end
adamc@211 2040
adamc@83 2041 and elabSgn (env, denv) (sgn, loc) =
adamc@31 2042 case sgn of
adamc@31 2043 L.SgnConst sgis =>
adamc@31 2044 let
adamc@88 2045 val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis
adamc@62 2046
adamc@62 2047 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) =>
adamc@62 2048 case sgi of
adamc@62 2049 L'.SgiConAbs (x, _, _) =>
adamc@62 2050 (if SS.member (cons, x) then
adamc@62 2051 sgnError env (DuplicateCon (loc, x))
adamc@62 2052 else
adamc@62 2053 ();
adamc@62 2054 (SS.add (cons, x), vals, sgns, strs))
adamc@62 2055 | L'.SgiCon (x, _, _, _) =>
adamc@62 2056 (if SS.member (cons, x) then
adamc@62 2057 sgnError env (DuplicateCon (loc, x))
adamc@62 2058 else
adamc@62 2059 ();
adamc@62 2060 (SS.add (cons, x), vals, sgns, strs))
adamc@191 2061 | L'.SgiDatatype (x, _, _, xncs) =>
adamc@156 2062 let
adamc@156 2063 val vals = foldl (fn ((x, _, _), vals) =>
adamc@156 2064 (if SS.member (vals, x) then
adamc@156 2065 sgnError env (DuplicateVal (loc, x))
adamc@156 2066 else
adamc@156 2067 ();
adamc@156 2068 SS.add (vals, x)))
adamc@156 2069 vals xncs
adamc@156 2070 in
adamc@156 2071 if SS.member (cons, x) then
adamc@156 2072 sgnError env (DuplicateCon (loc, x))
adamc@156 2073 else
adamc@156 2074 ();
adamc@156 2075 (SS.add (cons, x), vals, sgns, strs)
adamc@156 2076 end
adamc@191 2077 | L'.SgiDatatypeImp (x, _, _, _, _, _, _) =>
adamc@156 2078 (if SS.member (cons, x) then
adamc@156 2079 sgnError env (DuplicateCon (loc, x))
adamc@156 2080 else
adamc@156 2081 ();
adamc@156 2082 (SS.add (cons, x), vals, sgns, strs))
adamc@62 2083 | L'.SgiVal (x, _, _) =>
adamc@62 2084 (if SS.member (vals, x) then
adamc@62 2085 sgnError env (DuplicateVal (loc, x))
adamc@62 2086 else
adamc@62 2087 ();
adamc@62 2088 (cons, SS.add (vals, x), sgns, strs))
adamc@62 2089 | L'.SgiSgn (x, _, _) =>
adamc@62 2090 (if SS.member (sgns, x) then
adamc@62 2091 sgnError env (DuplicateSgn (loc, x))
adamc@62 2092 else
adamc@62 2093 ();
adamc@62 2094 (cons, vals, SS.add (sgns, x), strs))
adamc@62 2095 | L'.SgiStr (x, _, _) =>
adamc@62 2096 (if SS.member (strs, x) then
adamc@62 2097 sgnError env (DuplicateStr (loc, x))
adamc@62 2098 else
adamc@62 2099 ();
adamc@88 2100 (cons, vals, sgns, SS.add (strs, x)))
adamc@203 2101 | L'.SgiConstraint _ => (cons, vals, sgns, strs)
adamc@205 2102 | L'.SgiTable (_, x, _, _) =>
adamc@203 2103 (if SS.member (vals, x) then
adamc@203 2104 sgnError env (DuplicateVal (loc, x))
adamc@203 2105 else
adamc@203 2106 ();
adamc@211 2107 (cons, SS.add (vals, x), sgns, strs))
adamc@211 2108 | L'.SgiClassAbs (x, _) =>
adamc@211 2109 (if SS.member (cons, x) then
adamc@211 2110 sgnError env (DuplicateCon (loc, x))
adamc@211 2111 else
adamc@211 2112 ();
adamc@211 2113 (SS.add (cons, x), vals, sgns, strs))
adamc@211 2114 | L'.SgiClass (x, _, _) =>
adamc@211 2115 (if SS.member (cons, x) then
adamc@211 2116 sgnError env (DuplicateCon (loc, x))
adamc@211 2117 else
adamc@211 2118 ();
adamc@211 2119 (SS.add (cons, x), vals, sgns, strs)))
adamc@62 2120 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
adamc@31 2121 in
adamc@83 2122 ((L'.SgnConst sgis', loc), gs)
adamc@31 2123 end
adamc@31 2124 | L.SgnVar x =>
adamc@31 2125 (case E.lookupSgn env x of
adamc@31 2126 NONE =>
adamc@31 2127 (sgnError env (UnboundSgn (loc, x));
adamc@83 2128 ((L'.SgnError, loc), []))
adamc@83 2129 | SOME (n, sgis) => ((L'.SgnVar n, loc), []))
adamc@41 2130 | L.SgnFun (m, dom, ran) =>
adamc@41 2131 let
adamc@83 2132 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41 2133 val (env', n) = E.pushStrNamed env m dom'
adamc@83 2134 val (ran', gs2) = elabSgn (env', denv) ran
adamc@41 2135 in
adamc@83 2136 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
adamc@41 2137 end
adamc@42 2138 | L.SgnWhere (sgn, x, c) =>
adamc@42 2139 let
adamc@83 2140 val (sgn', ds1) = elabSgn (env, denv) sgn
adamc@83 2141 val (c', ck, ds2) = elabCon (env, denv) c
adamc@42 2142 in
adamc@42 2143 case #1 (hnormSgn env sgn') of
adamc@83 2144 L'.SgnError => (sgnerror, [])
adamc@42 2145 | L'.SgnConst sgis =>
adamc@75 2146 if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
adamc@75 2147 x' = x andalso
adamc@75 2148 (unifyKinds k ck
adamc@75 2149 handle KUnify x => sgnError env (WhereWrongKind x);
adamc@42 2150 true)
adamc@42 2151 | _ => false) sgis then
adamc@83 2152 ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2)
adamc@42 2153 else
adamc@42 2154 (sgnError env (UnWhereable (sgn', x));
adamc@83 2155 (sgnerror, []))
adamc@42 2156 | _ => (sgnError env (UnWhereable (sgn', x));
adamc@83 2157 (sgnerror, []))
adamc@42 2158 end
adamc@59 2159 | L.SgnProj (m, ms, x) =>
adamc@59 2160 (case E.lookupStr env m of
adamc@59 2161 NONE => (strError env (UnboundStr (loc, m));
adamc@83 2162 (sgnerror, []))
adamc@59 2163 | SOME (n, sgn) =>
adamc@59 2164 let
adamc@59 2165 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@59 2166 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@59 2167 NONE => (strError env (UnboundStr (loc, m));
adamc@59 2168 (strerror, sgnerror))
adamc@59 2169 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@59 2170 ((L'.StrVar n, loc), sgn) ms
adamc@59 2171 in
adamc@59 2172 case E.projectSgn env {sgn = sgn, str = str, field = x} of
adamc@59 2173 NONE => (sgnError env (UnboundSgn (loc, x));
adamc@83 2174 (sgnerror, []))
adamc@83 2175 | SOME _ => ((L'.SgnProj (n, ms, x), loc), [])
adamc@59 2176 end)
adamc@59 2177
adamc@31 2178
adamc@66 2179 fun selfify env {str, strs, sgn} =
adamc@66 2180 case #1 (hnormSgn env sgn) of
adamc@66 2181 L'.SgnError => sgn
adamc@66 2182 | L'.SgnVar _ => sgn
adamc@66 2183
adamc@66 2184 | L'.SgnConst sgis =>
adamc@66 2185 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
adamc@66 2186 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
adamc@191 2187 | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
adamc@191 2188 (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
adamc@218 2189 | (L'.SgiClassAbs (x, n), loc) =>
adamc@218 2190 (L'.SgiClass (x, n, (L'.CModProj (str, strs, x), loc)), loc)
adamc@66 2191 | (L'.SgiStr (x, n, sgn), loc) =>
adamc@66 2192 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
adamc@66 2193 | x => x) sgis), #2 sgn)
adamc@66 2194 | L'.SgnFun _ => sgn
adamc@66 2195 | L'.SgnWhere _ => sgn
adamc@66 2196 | L'.SgnProj (m, ms, x) =>
adamc@66 2197 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66 2198 (L'.StrVar m, #2 sgn) ms,
adamc@66 2199 sgn = #2 (E.lookupStrNamed env m),
adamc@66 2200 field = x} of
adamc@66 2201 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
adamc@66 2202 | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
adamc@66 2203
adamc@66 2204 fun selfifyAt env {str, sgn} =
adamc@66 2205 let
adamc@66 2206 fun self (str, _) =
adamc@66 2207 case str of
adamc@66 2208 L'.StrVar x => SOME (x, [])
adamc@66 2209 | L'.StrProj (str, x) =>
adamc@66 2210 (case self str of
adamc@66 2211 NONE => NONE
adamc@66 2212 | SOME (m, ms) => SOME (m, ms @ [x]))
adamc@66 2213 | _ => NONE
adamc@66 2214 in
adamc@66 2215 case self str of
adamc@66 2216 NONE => sgn
adamc@66 2217 | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
adamc@66 2218 end
adamc@66 2219
adamc@88 2220 fun dopen (env, denv) {str, strs, sgn} =
adamc@66 2221 let
adamc@66 2222 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66 2223 (L'.StrVar str, #2 sgn) strs
adamc@66 2224 in
adamc@66 2225 case #1 (hnormSgn env sgn) of
adamc@66 2226 L'.SgnConst sgis =>
adamc@88 2227 ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) =>
adamc@162 2228 let
adamc@162 2229 val d =
adamc@162 2230 case sgi of
adamc@162 2231 L'.SgiConAbs (x, n, k) =>
adamc@162 2232 let
adamc@162 2233 val c = (L'.CModProj (str, strs, x), loc)
adamc@162 2234 in
adamc@162 2235 (L'.DCon (x, n, k, c), loc)
adamc@162 2236 end
adamc@162 2237 | L'.SgiCon (x, n, k, c) =>
adamc@162 2238 (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
adamc@191 2239 | L'.SgiDatatype (x, n, xs, xncs) =>
adamc@191 2240 (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
adamc@191 2241 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@191 2242 (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)
adamc@162 2243 | L'.SgiVal (x, n, t) =>
adamc@162 2244 (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)
adamc@162 2245 | L'.SgiStr (x, n, sgn) =>
adamc@162 2246 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
adamc@162 2247 | L'.SgiSgn (x, n, sgn) =>
adamc@162 2248 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
adamc@162 2249 | L'.SgiConstraint (c1, c2) =>
adamc@162 2250 (L'.DConstraint (c1, c2), loc)
adamc@205 2251 | L'.SgiTable (_, x, n, c) =>
adamc@210 2252 (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc),
adamc@203 2253 (L'.EModProj (str, strs, x), loc)), loc)
adamc@211 2254 | L'.SgiClassAbs (x, n) =>
adamc@211 2255 let
adamc@211 2256 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
adamc@211 2257 val c = (L'.CModProj (str, strs, x), loc)
adamc@211 2258 in
adamc@211 2259 (L'.DCon (x, n, k, c), loc)
adamc@211 2260 end
adamc@211 2261 | L'.SgiClass (x, n, _) =>
adamc@211 2262 let
adamc@211 2263 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
adamc@211 2264 val c = (L'.CModProj (str, strs, x), loc)
adamc@211 2265 in
adamc@211 2266 (L'.DCon (x, n, k, c), loc)
adamc@211 2267 end
adamc@162 2268 in
adamc@162 2269 (d, (E.declBinds env' d, denv'))
adamc@162 2270 end)
adamc@88 2271 (env, denv) sgis
adamc@66 2272 | _ => (strError env (UnOpenable sgn);
adamc@88 2273 ([], (env, denv)))
adamc@66 2274 end
adamc@66 2275
adamc@88 2276 fun dopenConstraints (loc, env, denv) {str, strs} =
adamc@88 2277 case E.lookupStr env str of
adamc@88 2278 NONE => (strError env (UnboundStr (loc, str));
adamc@88 2279 denv)
adamc@88 2280 | SOME (n, sgn) =>
adamc@88 2281 let
adamc@88 2282 val (st, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@88 2283 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@88 2284 NONE => (strError env (UnboundStr (loc, m));
adamc@88 2285 (strerror, sgnerror))
adamc@88 2286 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@88 2287 ((L'.StrVar n, loc), sgn) strs
adamc@88 2288
adamc@88 2289 val cso = E.projectConstraints env {sgn = sgn, str = st}
adamc@88 2290
adamc@88 2291 val denv = case cso of
adamc@88 2292 NONE => (strError env (UnboundStr (loc, str));
adamc@88 2293 denv)
adamc@90 2294 | SOME cs => foldl (fn ((c1, c2), denv) =>
adamc@90 2295 let
adamc@90 2296 val (denv, gs) = D.assert env denv (c1, c2)
adamc@90 2297 in
adamc@90 2298 case gs of
adamc@90 2299 [] => ()
adamc@90 2300 | _ => raise Fail "dopenConstraints: Sub-constraints remain";
adamc@90 2301
adamc@90 2302 denv
adamc@90 2303 end) denv cs
adamc@88 2304 in
adamc@88 2305 denv
adamc@88 2306 end
adamc@88 2307
adamc@31 2308 fun sgiOfDecl (d, loc) =
adamc@31 2309 case d of
adamc@123 2310 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
adamc@156 2311 | L'.DDatatype x => [(L'.SgiDatatype x, loc)]
adamc@156 2312 | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)]
adamc@123 2313 | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
adamc@123 2314 | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis
adamc@123 2315 | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
adamc@123 2316 | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
adamc@123 2317 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
adamc@123 2318 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
adamc@123 2319 | L'.DExport _ => []
adamc@205 2320 | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)]
adamc@213 2321 | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)]
adamc@88 2322
adamc@88 2323 fun sgiBindsD (env, denv) (sgi, _) =
adamc@88 2324 case sgi of
adamc@90 2325 L'.SgiConstraint (c1, c2) =>
adamc@90 2326 (case D.assert env denv (c1, c2) of
adamc@90 2327 (denv, []) => denv
adamc@90 2328 | _ => raise Fail "sgiBindsD: Sub-constraints remain")
adamc@88 2329 | _ => denv
adamc@31 2330
adamc@86 2331 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
adamc@35 2332 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
adamc@31 2333 (L'.SgnError, _) => ()
adamc@31 2334 | (_, L'.SgnError) => ()
adamc@31 2335
adamc@31 2336 | (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
adamc@31 2337 let
adamc@156 2338 fun folder (sgi2All as (sgi, loc), (env, denv)) =
adamc@31 2339 let
adamc@31 2340 fun seek p =
adamc@31 2341 let
adamc@88 2342 fun seek (env, denv) ls =
adamc@31 2343 case ls of
adamc@31 2344 [] => (sgnError env (UnmatchedSgi sgi2All);
adamc@88 2345 (env, denv))
adamc@31 2346 | h :: t =>
adamc@31 2347 case p h of
adamc@88 2348 NONE => seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t
adamc@88 2349 | SOME envs => envs
adamc@31 2350 in
adamc@88 2351 seek (env, denv) sgis1
adamc@31 2352 end
adamc@31 2353 in
adamc@31 2354 case sgi of
adamc@31 2355 L'.SgiConAbs (x, n2, k2) =>
adamc@31 2356 seek (fn sgi1All as (sgi1, _) =>
adamc@31 2357 let
adamc@41 2358 fun found (x', n1, k1, co1) =
adamc@41 2359 if x = x' then
adamc@41 2360 let
adamc@41 2361 val () = unifyKinds k1 k2
adamc@41 2362 handle KUnify (k1, k2, err) =>
adamc@41 2363 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
adamc@41 2364 val env = E.pushCNamedAs env x n1 k1 co1
adamc@41 2365 in
adamc@41 2366 SOME (if n1 = n2 then
adamc@41 2367 env
adamc@41 2368 else
adamc@88 2369 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)),
adamc@88 2370 denv)
adamc@41 2371 end
adamc@41 2372 else
adamc@41 2373 NONE
adamc@31 2374 in
adamc@31 2375 case sgi1 of
adamc@41 2376 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
adamc@41 2377 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
adamc@191 2378 | L'.SgiDatatype (x', n1, xs, _) =>
adamc@191 2379 let
adamc@191 2380 val k = (L'.KType, loc)
adamc@191 2381 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 2382 in
adamc@191 2383 found (x', n1, k', NONE)
adamc@191 2384 end
adamc@191 2385 | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) =>
adamc@191 2386 let
adamc@191 2387 val k = (L'.KType, loc)
adamc@191 2388 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 2389 in
adamc@191 2390 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
adamc@191 2391 end
adamc@211 2392 | L'.SgiClassAbs (x', n1) => found (x', n1,
adamc@218 2393 (L'.KArrow ((L'.KType, loc),
adamc@218 2394 (L'.KType, loc)), loc),
adamc@218 2395 NONE)
adamc@211 2396 | L'.SgiClass (x', n1, c) => found (x', n1,
adamc@211 2397 (L'.KArrow ((L'.KType, loc),
adamc@211 2398 (L'.KType, loc)), loc),
adamc@211 2399 SOME c)
adamc@31 2400 | _ => NONE
adamc@31 2401 end)
adamc@31 2402
adamc@31 2403 | L'.SgiCon (x, n2, k2, c2) =>
adamc@31 2404 seek (fn sgi1All as (sgi1, _) =>
adamc@211 2405 let
adamc@211 2406 fun found (x', n1, k1, c1) =
adamc@211 2407 if x = x' then
adamc@211 2408 let
adamc@211 2409 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv)
adamc@211 2410 in
adamc@211 2411 (case unifyCons (env, denv) c1 c2 of
adamc@211 2412 [] => good ()
adamc@211 2413 | _ => NONE)
adamc@211 2414 handle CUnify (c1, c2, err) =>
adamc@211 2415 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@211 2416 good ())
adamc@211 2417 end
adamc@211 2418 else
adamc@211 2419 NONE
adamc@211 2420 in
adamc@211 2421 case sgi1 of
adamc@211 2422 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
adamc@211 2423 | L'.SgiClass (x', n1, c1) =>
adamc@211 2424 found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1)
adamc@211 2425 | _ => NONE
adamc@211 2426 end)
adamc@31 2427
adamc@191 2428 | L'.SgiDatatype (x, n2, xs2, xncs2) =>
adamc@156 2429 seek (fn sgi1All as (sgi1, _) =>
adamc@160 2430 let
adamc@191 2431 fun found (n1, xs1, xncs1) =
adamc@160 2432 let
adamc@160 2433 fun mismatched ue =
adamc@160 2434 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
adamc@160 2435 SOME (env, denv))
adamc@156 2436
adamc@191 2437 val k = (L'.KType, loc)
adamc@191 2438 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
adamc@191 2439
adamc@160 2440 fun good () =
adamc@160 2441 let
adamc@160 2442 val env = E.sgiBinds env sgi2All
adamc@160 2443 val env = if n1 = n2 then
adamc@160 2444 env
adamc@160 2445 else
adamc@160 2446 E.pushCNamedAs env x n1 (L'.KType, loc)
adamc@160 2447 (SOME (L'.CNamed n1, loc))
adamc@160 2448 in
adamc@160 2449 SOME (env, denv)
adamc@160 2450 end
adamc@156 2451
adamc@191 2452 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
adamc@160 2453 fun xncBad ((x1, _, t1), (x2, _, t2)) =
adamc@160 2454 String.compare (x1, x2) <> EQUAL
adamc@160 2455 orelse case (t1, t2) of
adamc@160 2456 (NONE, NONE) => false
adamc@160 2457 | (SOME t1, SOME t2) =>
adamc@160 2458 not (List.null (unifyCons (env, denv) t1 t2))
adamc@160 2459 | _ => true
adamc@160 2460 in
adamc@191 2461 (if xs1 <> xs2
adamc@191 2462 orelse length xncs1 <> length xncs2
adamc@160 2463 orelse ListPair.exists xncBad (xncs1, xncs2) then
adamc@160 2464 mismatched NONE
adamc@160 2465 else
adamc@160 2466 good ())
adamc@160 2467 handle CUnify ue => mismatched (SOME ue)
adamc@160 2468 end
adamc@160 2469 in
adamc@160 2470 case sgi1 of
adamc@191 2471 L'.SgiDatatype (x', n1, xs, xncs1) =>
adamc@160 2472 if x' = x then
adamc@191 2473 found (n1, xs, xncs1)
adamc@160 2474 else
adamc@160 2475 NONE
adamc@191 2476 | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
adamc@162 2477 if x' = x then
adamc@191 2478 found (n1, xs, xncs1)
adamc@162 2479 else
adamc@162 2480 NONE
adamc@160 2481 | _ => NONE
adamc@160 2482 end)
adamc@156 2483
adamc@191 2484 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
adamc@158 2485 seek (fn sgi1All as (sgi1, _) =>
adamc@158 2486 case sgi1 of
adamc@191 2487 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) =>
adamc@158 2488 if x = x' then
adamc@158 2489 let
adamc@158 2490 val k = (L'.KType, loc)
adamc@191 2491 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@158 2492 val t1 = (L'.CModProj (m11, ms1, s1), loc)
adamc@158 2493 val t2 = (L'.CModProj (m12, ms2, s2), loc)
adamc@158 2494
adamc@158 2495 fun good () =
adamc@158 2496 let
adamc@191 2497 val env = E.pushCNamedAs env x n1 k' (SOME t1)
adamc@191 2498 val env = E.pushCNamedAs env x n2 k' (SOME t2)
adamc@158 2499 in
adamc@158 2500 SOME (env, denv)
adamc@158 2501 end
adamc@158 2502 in
adamc@158 2503 (case unifyCons (env, denv) t1 t2 of
adamc@158 2504 [] => good ()
adamc@158 2505 | _ => NONE)
adamc@158 2506 handle CUnify (c1, c2, err) =>
adamc@158 2507 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@158 2508 good ())
adamc@158 2509 end
adamc@158 2510 else
adamc@158 2511 NONE
adamc@158 2512
adamc@158 2513 | _ => NONE)
adamc@156 2514
adamc@32 2515 | L'.SgiVal (x, n2, c2) =>
adamc@32 2516 seek (fn sgi1All as (sgi1, _) =>
adamc@32 2517 case sgi1 of
adamc@41 2518 L'.SgiVal (x', n1, c1) =>
adamc@41 2519 if x = x' then
adamc@86 2520 (case unifyCons (env, denv) c1 c2 of
adamc@88 2521 [] => SOME (env, denv)
adamc@86 2522 | _ => NONE)
adamc@86 2523 handle CUnify (c1, c2, err) =>
adamc@86 2524 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@88 2525 SOME (env, denv))
adamc@41 2526 else
adamc@41 2527 NONE
adamc@205 2528 | L'.SgiTable (_, x', n1, c1) =>
adamc@203 2529 if x = x' then
adamc@210 2530 (case unifyCons (env, denv) (L'.CApp (tableOf (), c1), loc) c2 of
adamc@203 2531 [] => SOME (env, denv)
adamc@203 2532 | _ => NONE)
adamc@203 2533 handle CUnify (c1, c2, err) =>
adamc@203 2534 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@203 2535 SOME (env, denv))
adamc@203 2536 else
adamc@203 2537 NONE
adamc@32 2538 | _ => NONE)
adamc@32 2539
adamc@33 2540 | L'.SgiStr (x, n2, sgn2) =>
adamc@33 2541 seek (fn sgi1All as (sgi1, _) =>
adamc@33 2542 case sgi1 of
adamc@41 2543 L'.SgiStr (x', n1, sgn1) =>
adamc@41 2544 if x = x' then
adamc@66 2545 let
adamc@86 2546 val () = subSgn (env, denv) sgn1 sgn2
adamc@66 2547 val env = E.pushStrNamedAs env x n1 sgn1
adamc@66 2548 val env = if n1 = n2 then
adamc@66 2549 env
adamc@66 2550 else
adamc@66 2551 E.pushStrNamedAs env x n2
adamc@66 2552 (selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
adamc@66 2553 sgn = sgn2})
adamc@66 2554 in
adamc@88 2555 SOME (env, denv)
adamc@66 2556 end
adamc@41 2557 else
adamc@41 2558 NONE
adamc@33 2559 | _ => NONE)
adamc@59 2560
adamc@59 2561 | L'.SgiSgn (x, n2, sgn2) =>
adamc@59 2562 seek (fn sgi1All as (sgi1, _) =>
adamc@59 2563 case sgi1 of
adamc@59 2564 L'.SgiSgn (x', n1, sgn1) =>
adamc@59 2565 if x = x' then
adamc@65 2566 let
adamc@86 2567 val () = subSgn (env, denv) sgn1 sgn2
adamc@86 2568 val () = subSgn (env, denv) sgn2 sgn1
adamc@65 2569
adamc@65 2570 val env = E.pushSgnNamedAs env x n2 sgn2
adamc@65 2571 val env = if n1 = n2 then
adamc@65 2572 env
adamc@65 2573 else
adamc@65 2574 E.pushSgnNamedAs env x n1 sgn2
adamc@65 2575 in
adamc@88 2576 SOME (env, denv)
adamc@65 2577 end
adamc@59 2578 else
adamc@59 2579 NONE
adamc@59 2580 | _ => NONE)
adamc@88 2581
adamc@88 2582 | L'.SgiConstraint (c2, d2) =>
adamc@88 2583 seek (fn sgi1All as (sgi1, _) =>
adamc@88 2584 case sgi1 of
adamc@88 2585 L'.SgiConstraint (c1, d1) =>
adamc@88 2586 if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then
adamc@90 2587 let
adamc@90 2588 val (denv, gs) = D.assert env denv (c2, d2)
adamc@90 2589 in
adamc@90 2590 case gs of
adamc@90 2591 [] => ()
adamc@90 2592 | _ => raise Fail "subSgn: Sub-constraints remain";
adamc@90 2593
adamc@90 2594 SOME (env, denv)
adamc@90 2595 end
adamc@88 2596 else
adamc@88 2597 NONE
adamc@88 2598 | _ => NONE)
adamc@203 2599
adamc@205 2600 | L'.SgiTable (_, x, n2, c2) =>
adamc@203 2601 seek (fn sgi1All as (sgi1, _) =>
adamc@203 2602 case sgi1 of
adamc@205 2603 L'.SgiTable (_, x', n1, c1) =>
adamc@203 2604 if x = x' then
adamc@203 2605 (case unifyCons (env, denv) c1 c2 of
adamc@203 2606 [] => SOME (env, denv)
adamc@203 2607 | _ => NONE)
adamc@203 2608 handle CUnify (c1, c2, err) =>
adamc@203 2609 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@203 2610 SOME (env, denv))
adamc@203 2611 else
adamc@203 2612 NONE
adamc@203 2613 | _ => NONE)
adamc@211 2614
adamc@211 2615 | L'.SgiClassAbs (x, n2) =>
adamc@211 2616 seek (fn sgi1All as (sgi1, _) =>
adamc@211 2617 let
adamc@211 2618 fun found (x', n1, co) =
adamc@211 2619 if x = x' then
adamc@211 2620 let
adamc@211 2621 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
adamc@211 2622 val env = E.pushCNamedAs env x n1 k co
adamc@211 2623 in
adamc@211 2624 SOME (if n1 = n2 then
adamc@211 2625 env
adamc@211 2626 else
adamc@211 2627 E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)),
adamc@211 2628 denv)
adamc@211 2629 end
adamc@211 2630 else
adamc@211 2631 NONE
adamc@211 2632 in
adamc@211 2633 case sgi1 of
adamc@211 2634 L'.SgiClassAbs (x', n1) => found (x', n1, NONE)
adamc@211 2635 | L'.SgiClass (x', n1, c) => found (x', n1, SOME c)
adamc@211 2636 | _ => NONE
adamc@211 2637 end)
adamc@211 2638 | L'.SgiClass (x, n2, c2) =>
adamc@211 2639 seek (fn sgi1All as (sgi1, _) =>
adamc@211 2640 let
adamc@211 2641 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
adamc@211 2642
adamc@211 2643 fun found (x', n1, c1) =
adamc@211 2644 if x = x' then
adamc@211 2645 let
adamc@218 2646 fun good () =
adamc@218 2647 let
adamc@218 2648 val env = E.pushCNamedAs env x n2 k (SOME c2)
adamc@218 2649 val env = if n1 = n2 then
adamc@218 2650 env
adamc@218 2651 else
adamc@218 2652 E.pushCNamedAs env x n1 k (SOME c1)
adamc@218 2653 in
adamc@218 2654 SOME (env, denv)
adamc@218 2655 end
adamc@211 2656 in
adamc@211 2657 (case unifyCons (env, denv) c1 c2 of
adamc@211 2658 [] => good ()
adamc@211 2659 | _ => NONE)
adamc@211 2660 handle CUnify (c1, c2, err) =>
adamc@211 2661 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@211 2662 good ())
adamc@211 2663 end
adamc@211 2664 else
adamc@211 2665 NONE
adamc@211 2666 in
adamc@211 2667 case sgi1 of
adamc@211 2668 L'.SgiClass (x', n1, c1) => found (x', n1, c1)
adamc@211 2669 | _ => NONE
adamc@211 2670 end)
adamc@31 2671 end
adamc@31 2672 in
adamc@88 2673 ignore (foldl folder (env, denv) sgis2)
adamc@31 2674 end
adamc@31 2675
adamc@41 2676 | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
adamc@43 2677 let
adamc@43 2678 val ran1 =
adamc@43 2679 if n1 = n2 then
adamc@43 2680 ran1
adamc@43 2681 else
adamc@43 2682 subStrInSgn (n1, n2) ran1
adamc@43 2683 in
adamc@86 2684 subSgn (env, denv) dom2 dom1;
adamc@86 2685 subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2
adamc@43 2686 end
adamc@41 2687
adamc@41 2688 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
adamc@41 2689
adamc@61 2690
adamc@88 2691 fun elabDecl ((d, loc), (env, denv, gs)) =
adamc@76 2692 case d of
adamc@76 2693 L.DCon (x, ko, c) =>
adamc@76 2694 let
adamc@76 2695 val k' = case ko of
adamc@76 2696 NONE => kunif loc
adamc@76 2697 | SOME k => elabKind k
adamc@76 2698
adamc@83 2699 val (c', ck, gs') = elabCon (env, denv) c
adamc@76 2700 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@76 2701 in
adamc@76 2702 checkKind env c' ck k';
adamc@76 2703
adamc@88 2704 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
adamc@76 2705 end
adamc@191 2706 | L.DDatatype (x, xs, xcs) =>
adamc@156 2707 let
adamc@156 2708 val k = (L'.KType, loc)
adamc@191 2709 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191 2710 val (env, n) = E.pushCNamed env x k' NONE
adamc@156 2711 val t = (L'.CNamed n, loc)
adamc@194 2712 val nxs = length xs - 1
adamc@194 2713 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@191 2714
adamc@191 2715 val (env', denv') = foldl (fn (x, (env', denv')) =>
adamc@191 2716 (E.pushCRel env' x k,
adamc@191 2717 D.enter denv')) (env, denv) xs
adamc@156 2718
adamc@156 2719 val (xcs, (used, env, gs)) =
adamc@156 2720 ListUtil.foldlMap
adamc@156 2721 (fn ((x, to), (used, env, gs)) =>
adamc@156 2722 let
adamc@156 2723 val (to, t, gs') = case to of
adamc@156 2724 NONE => (NONE, t, gs)
adamc@156 2725 | SOME t' =>
adamc@156 2726 let
adamc@191 2727 val (t', tk, gs') = elabCon (env', denv') t'
adamc@156 2728 in
adamc@191 2729 checkKind env' t' tk k;
adamc@156 2730 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
adamc@156 2731 end
adamc@191 2732 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
adamc@156 2733
adamc@156 2734 val (env, n') = E.pushENamed env x t
adamc@156 2735 in
adamc@156 2736 if SS.member (used, x) then
adamc@156 2737 strError env (DuplicateConstructor (x, loc))
adamc@156 2738 else
adamc@156 2739 ();
adamc@156 2740 ((x, n', to), (SS.add (used, x), env, gs'))
adamc@156 2741 end)
adamc@156 2742 (SS.empty, env, []) xcs
adamc@171 2743
adamc@191 2744 val env = E.pushDatatype env n xs xcs
adamc@156 2745 in
adamc@191 2746 ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
adamc@156 2747 end
adamc@156 2748
adamc@157 2749 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
adamc@157 2750
adamc@157 2751 | L.DDatatypeImp (x, m1 :: ms, s) =>
adamc@157 2752 (case E.lookupStr env m1 of
adamc@157 2753 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@157 2754 ([], (env, denv, gs)))
adamc@157 2755 | SOME (n, sgn) =>
adamc@157 2756 let
adamc@157 2757 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@157 2758 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@157 2759 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@157 2760 (strerror, sgnerror))
adamc@157 2761 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@157 2762 ((L'.StrVar n, loc), sgn) ms
adamc@157 2763 in
adamc@158 2764 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
adamc@158 2765 ((L'.CModProj (n, ms, s), _), gs) =>
adamc@158 2766 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
adamc@158 2767 NONE => (conError env (UnboundDatatype (loc, s));
adamc@158 2768 ([], (env, denv, gs)))
adamc@191 2769 | SOME (xs, xncs) =>
adamc@158 2770 let
adamc@158 2771 val k = (L'.KType, loc)
adamc@191 2772 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@158 2773 val t = (L'.CModProj (n, ms, s), loc)
adamc@191 2774 val (env, n') = E.pushCNamed env x k' (SOME t)
adamc@191 2775 val env = E.pushDatatype env n' xs xncs
adamc@157 2776
adamc@158 2777 val t = (L'.CNamed n', loc)
adamc@158 2778 val env = foldl (fn ((x, n, to), env) =>
adamc@158 2779 let
adamc@158 2780 val t = case to of
adamc@158 2781 NONE => t
adamc@158 2782 | SOME t' => (L'.TFun (t', t), loc)
adamc@191 2783
adamc@191 2784 val t = foldr (fn (x, t) =>
adamc@191 2785 (L'.TCFun (L'.Implicit, x, k, t), loc))
adamc@191 2786 t xs
adamc@158 2787 in
adamc@158 2788 E.pushENamedAs env x n t
adamc@158 2789 end) env xncs
adamc@158 2790 in
adamc@191 2791 ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
adamc@158 2792 end)
adamc@158 2793 | _ => (strError env (NotDatatype loc);
adamc@158 2794 ([], (env, denv, [])))
adamc@157 2795 end)
adamc@157 2796
adamc@76 2797 | L.DVal (x, co, e) =>
adamc@76 2798 let
adamc@123 2799 val (c', _, gs1) = case co of
adamc@83 2800 NONE => (cunif (loc, ktype), ktype, [])
adamc@83 2801 | SOME c => elabCon (env, denv) c
adamc@76 2802
adamc@83 2803 val (e', et, gs2) = elabExp (env, denv) e
adamc@217 2804 val gs3 = checkCon (env, denv) e' et c'
adamc@217 2805 val (c', gs4) = normClassConstraint (env, denv) c'
adamc@76 2806 val (env', n) = E.pushENamed env x c'
adamc@76 2807 in
adamc@217 2808 (*prefaces "DVal" [("x", Print.PD.string x),
adamc@217 2809 ("c'", p_con env c')];*)
adamc@217 2810 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs4 @ gs))
adamc@76 2811 end
adamc@123 2812 | L.DValRec vis =>
adamc@123 2813 let
adamc@123 2814 val (vis, gs) = ListUtil.foldlMap
adamc@123 2815 (fn ((x, co, e), gs) =>
adamc@123 2816 let
adamc@123 2817 val (c', _, gs1) = case co of
adamc@123 2818 NONE => (cunif (loc, ktype), ktype, [])
adamc@123 2819 | SOME c => elabCon (env, denv) c
adamc@123 2820 in
adamc@123 2821 ((x, c', e), gs1 @ gs)
adamc@123 2822 end) [] vis
adamc@123 2823
adamc@123 2824 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
adamc@123 2825 let
adamc@123 2826 val (env, n) = E.pushENamed env x c'
adamc@123 2827 in
adamc@123 2828 ((x, n, c', e), env)
adamc@123 2829 end) env vis
adamc@123 2830
adamc@123 2831 val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
adamc@123 2832 let
adamc@123 2833 val (e', et, gs1) = elabExp (env, denv) e
adamc@123 2834
adamc@123 2835 val gs2 = checkCon (env, denv) e' et c'
adamc@123 2836 in
adamc@123 2837 ((x, n, c', e'), gs1 @ gs2 @ gs)
adamc@123 2838 end) gs vis
adamc@123 2839 in
adamc@123 2840 ([(L'.DValRec vis, loc)], (env, denv, gs))
adamc@123 2841 end
adamc@76 2842
adamc@76 2843 | L.DSgn (x, sgn) =>
adamc@76 2844 let
adamc@83 2845 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 2846 val (env', n) = E.pushSgnNamed env x sgn'
adamc@76 2847 in
adamc@88 2848 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 2849 end
adamc@76 2850
adamc@76 2851 | L.DStr (x, sgno, str) =>
adamc@76 2852 let
adamc@93 2853 val () = if x = "Basis" then
adamc@93 2854 raise Fail "Not allowed to redefine structure 'Basis'"
adamc@93 2855 else
adamc@93 2856 ()
adamc@93 2857
adamc@83 2858 val formal = Option.map (elabSgn (env, denv)) sgno
adamc@76 2859
adamc@83 2860 val (str', sgn', gs') =
adamc@78 2861 case formal of
adamc@78 2862 NONE =>
adamc@78 2863 let
adamc@83 2864 val (str', actual, ds) = elabStr (env, denv) str
adamc@78 2865 in
adamc@83 2866 (str', selfifyAt env {str = str', sgn = actual}, ds)
adamc@78 2867 end
adamc@83 2868 | SOME (formal, gs1) =>
adamc@78 2869 let
adamc@78 2870 val str =
adamc@78 2871 case #1 (hnormSgn env formal) of
adamc@78 2872 L'.SgnConst sgis =>
adamc@78 2873 (case #1 str of
adamc@78 2874 L.StrConst ds =>
adamc@78 2875 let
adamc@78 2876 val needed = foldl (fn ((sgi, _), needed) =>
adamc@78 2877 case sgi of
adamc@78 2878 L'.SgiConAbs (x, _, _) => SS.add (needed, x)
adamc@78 2879 | _ => needed)
adamc@78 2880 SS.empty sgis
adamc@78 2881
adamc@78 2882 val needed = foldl (fn ((d, _), needed) =>
adamc@78 2883 case d of
adamc@78 2884 L.DCon (x, _, _) => (SS.delete (needed, x)
adamc@78 2885 handle NotFound => needed)
adamc@218 2886 | L.DClass (x, _) => (SS.delete (needed, x)
adamc@218 2887 handle NotFound => needed)
adamc@78 2888 | L.DOpen _ => SS.empty
adamc@78 2889 | _ => needed)
adamc@78 2890 needed ds
adamc@78 2891 in
adamc@78 2892 case SS.listItems needed of
adamc@78 2893 [] => str
adamc@78 2894 | xs =>
adamc@78 2895 let
adamc@78 2896 val kwild = (L.KWild, #2 str)
adamc@78 2897 val cwild = (L.CWild kwild, #2 str)
adamc@78 2898 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
adamc@78 2899 in
adamc@78 2900 (L.StrConst (ds @ ds'), #2 str)
adamc@78 2901 end
adamc@78 2902 end
adamc@78 2903 | _ => str)
adamc@78 2904 | _ => str
adamc@78 2905
adamc@83 2906 val (str', actual, gs2) = elabStr (env, denv) str
adamc@78 2907 in
adamc@158 2908 subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
adamc@83 2909 (str', formal, gs1 @ gs2)
adamc@78 2910 end
adamc@76 2911
adamc@76 2912 val (env', n) = E.pushStrNamed env x sgn'
adamc@76 2913 in
adamc@76 2914 case #1 (hnormSgn env sgn') of
adamc@76 2915 L'.SgnFun _ =>
adamc@76 2916 (case #1 str' of
adamc@76 2917 L'.StrFun _ => ()
adamc@76 2918 | _ => strError env (FunctorRebind loc))
adamc@76 2919 | _ => ();
adamc@76 2920
adamc@88 2921 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
adamc@76 2922 end
adamc@76 2923
adamc@76 2924 | L.DFfiStr (x, sgn) =>
adamc@76 2925 let
adamc@83 2926 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76 2927
adamc@76 2928 val (env', n) = E.pushStrNamed env x sgn'
adamc@76 2929 in
adamc@88 2930 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76 2931 end
adamc@76 2932
adamc@76 2933 | L.DOpen (m, ms) =>
adamc@88 2934 (case E.lookupStr env m of
adamc@88 2935 NONE => (strError env (UnboundStr (loc, m));
adamc@205 2936 ([], (env, denv, gs)))
adamc@88 2937 | SOME (n, sgn) =>
adamc@88 2938 let
adamc@88 2939 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@88 2940 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@88 2941 NONE => (strError env (UnboundStr (loc, m));
adamc@88 2942 (strerror, sgnerror))
adamc@88 2943 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@88 2944 ((L'.StrVar n, loc), sgn) ms
adamc@83 2945
adamc@88 2946 val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn}
adamc@88 2947 val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
adamc@88 2948 in
adamc@205 2949 (ds, (env', denv', gs))
adamc@88 2950 end)
adamc@88 2951
adamc@88 2952 | L.DConstraint (c1, c2) =>
adamc@88 2953 let
adamc@88 2954 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@88 2955 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@90 2956 val gs3 = D.prove env denv (c1', c2', loc)
adamc@88 2957
adamc@90 2958 val (denv', gs4) = D.assert env denv (c1', c2')
adamc@88 2959 in
adamc@88 2960 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
adamc@88 2961 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
adamc@88 2962
adamc@205 2963 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3 @ gs4 @ gs))
adamc@88 2964 end
adamc@88 2965
adamc@88 2966 | L.DOpenConstraints (m, ms) =>
adamc@88 2967 let
adamc@88 2968 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
adamc@88 2969 in
adamc@205 2970 ([], (env, denv, gs))
adamc@88 2971 end
adamc@3 2972
adamc@109 2973 | L.DExport str =>
adamc@100 2974 let
adamc@205 2975 val (str', sgn, gs') = elabStr (env, denv) str
adamc@100 2976
adamc@109 2977 val sgn =
adamc@109 2978 case #1 (hnormSgn env sgn) of
adamc@109 2979 L'.SgnConst sgis =>
adamc@109 2980 let
adamc@146 2981 fun doOne (all as (sgi, _), env) =
adamc@146 2982 (case sgi of
adamc@146 2983 L'.SgiVal (x, n, t) =>
adamc@146 2984 (case hnormCon (env, denv) t of
adamc@146 2985 ((L'.TFun (dom, ran), _), []) =>
adamc@146 2986 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
adamc@146 2987 (((L'.TRecord domR, _), []),
adamc@146 2988 ((L'.CApp (tf, arg3), _), [])) =>
adamc@146 2989 (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
adamc@146 2990 (((L'.CApp (tf, arg2), _), []),
adamc@146 2991 (((L'.CRecord (_, []), _), []))) =>
adamc@146 2992 (case (hnormCon (env, denv) tf) of
adamc@146 2993 ((L'.CApp (tf, arg1), _), []) =>
adamc@146 2994 (case (hnormCon (env, denv) tf,
adamc@146 2995 hnormCon (env, denv) domR,
adamc@152 2996 hnormCon (env, denv) arg1,
adamc@146 2997 hnormCon (env, denv) arg2) of
adamc@152 2998 ((tf, []), (domR, []), (arg1, []),
adamc@146 2999 ((L'.CRecord (_, []), _), [])) =>
adamc@146 3000 let
adamc@146 3001 val t = (L'.CApp (tf, arg1), loc)
adamc@146 3002 val t = (L'.CApp (t, arg2), loc)
adamc@146 3003 val t = (L'.CApp (t, arg3), loc)
adamc@146 3004 in
adamc@146 3005 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
adamc@146 3006 t),
adamc@146 3007 loc)), loc)
adamc@146 3008 end
adamc@146 3009 | _ => all)
adamc@146 3010 | _ => all)
adamc@146 3011 | _ => all)
adamc@146 3012 | _ => all)
adamc@146 3013 | _ => all)
adamc@146 3014 | _ => all,
adamc@146 3015 E.sgiBinds env all)
adamc@109 3016 in
adamc@146 3017 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
adamc@109 3018 end
adamc@109 3019 | _ => sgn
adamc@100 3020 in
adamc@205 3021 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs))
adamc@100 3022 end
adamc@100 3023
adamc@203 3024 | L.DTable (x, c) =>
adamc@203 3025 let
adamc@205 3026 val (c', k, gs') = elabCon (env, denv) c
adamc@210 3027 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
adamc@203 3028 in
adamc@203 3029 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
adamc@210 3030 ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, gs' @ gs))
adamc@203 3031 end
adamc@203 3032
adamc@211 3033 | L.DClass (x, c) =>
adamc@211 3034 let
adamc@211 3035 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
adamc@211 3036 val (c', ck, gs) = elabCon (env, denv) c
adamc@211 3037 val (env, n) = E.pushCNamed env x k (SOME c')
adamc@211 3038 val env = E.pushClass env n
adamc@211 3039 in
adamc@211 3040 checkKind env c' ck k;
adamc@213 3041 ([(L'.DClass (x, n, c'), loc)], (env, denv, []))
adamc@211 3042 end
adamc@211 3043
adamc@83 3044 and elabStr (env, denv) (str, loc) =
adamc@31 3045 case str of
adamc@31 3046 L.StrConst ds =>
adamc@31 3047 let
adamc@88 3048 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
adamc@123 3049 val sgis = ListUtil.mapConcat sgiOfDecl ds'
adamc@63 3050
adamc@63 3051 val (sgis, _, _, _, _) =
adamc@64 3052 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
adamc@63 3053 case sgi of
adamc@64 3054 L'.SgiConAbs (x, n, k) =>
adamc@64 3055 let
adamc@64 3056 val (cons, x) =
adamc@64 3057 if SS.member (cons, x) then
adamc@64 3058 (cons, "?" ^ x)
adamc@64 3059 else
adamc@64 3060 (SS.add (cons, x), x)
adamc@64 3061 in
adamc@64 3062 ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 3063 end
adamc@64 3064 | L'.SgiCon (x, n, k, c) =>
adamc@64 3065 let
adamc@64 3066 val (cons, x) =
adamc@64 3067 if SS.member (cons, x) then
adamc@64 3068 (cons, "?" ^ x)
adamc@64 3069 else
adamc@64 3070 (SS.add (cons, x), x)
adamc@64 3071 in
adamc@64 3072 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 3073 end
adamc@191 3074 | L'.SgiDatatype (x, n, xs, xncs) =>
adamc@156 3075 let
adamc@156 3076 val (cons, x) =
adamc@156 3077 if SS.member (cons, x) then
adamc@156 3078 (cons, "?" ^ x)
adamc@156 3079 else
adamc@156 3080 (SS.add (cons, x), x)
adamc@156 3081
adamc@156 3082 val (xncs, vals) =
adamc@156 3083 ListUtil.foldlMap
adamc@156 3084 (fn ((x, n, t), vals) =>
adamc@156 3085 if SS.member (vals, x) then
adamc@156 3086 (("?" ^ x, n, t), vals)
adamc@156 3087 else
adamc@156 3088 ((x, n, t), SS.add (vals, x)))
adamc@156 3089 vals xncs
adamc@156 3090 in
adamc@191 3091 ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
adamc@156 3092 end
adamc@191 3093 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@156 3094 let
adamc@156 3095 val (cons, x) =
adamc@156 3096 if SS.member (cons, x) then
adamc@156 3097 (cons, "?" ^ x)
adamc@156 3098 else
adamc@156 3099 (SS.add (cons, x), x)
adamc@156 3100 in
adamc@191 3101 ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
adamc@156 3102 end
adamc@64 3103 | L'.SgiVal (x, n, c) =>
adamc@64 3104 let
adamc@64 3105 val (vals, x) =
adamc@64 3106 if SS.member (vals, x) then
adamc@64 3107 (vals, "?" ^ x)
adamc@64 3108 else
adamc@64 3109 (SS.add (vals, x), x)
adamc@64 3110 in
adamc@64 3111 ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 3112 end
adamc@64 3113 | L'.SgiSgn (x, n, sgn) =>
adamc@64 3114 let
adamc@64 3115 val (sgns, x) =
adamc@64 3116 if SS.member (sgns, x) then
adamc@64 3117 (sgns, "?" ^ x)
adamc@64 3118 else
adamc@64 3119 (SS.add (sgns, x), x)
adamc@64 3120 in
adamc@64 3121 ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@64 3122 end
adamc@64 3123
adamc@64 3124 | L'.SgiStr (x, n, sgn) =>
adamc@64 3125 let
adamc@64 3126 val (strs, x) =
adamc@64 3127 if SS.member (strs, x) then
adamc@64 3128 (strs, "?" ^ x)
adamc@64 3129 else
adamc@64 3130 (SS.add (strs, x), x)
adamc@64 3131 in
adamc@64 3132 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@88 3133 end
adamc@203 3134 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
adamc@205 3135 | L'.SgiTable (tn, x, n, c) =>
adamc@203 3136 let
adamc@203 3137 val (vals, x) =
adamc@203 3138 if SS.member (vals, x) then
adamc@203 3139 (vals, "?" ^ x)
adamc@203 3140 else
adamc@203 3141 (SS.add (vals, x), x)
adamc@203 3142 in
adamc@205 3143 ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@211 3144 end
adamc@211 3145 | L'.SgiClassAbs (x, n) =>
adamc@211 3146 let
adamc@211 3147 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
adamc@211 3148
adamc@211 3149 val (cons, x) =
adamc@211 3150 if SS.member (cons, x) then
adamc@211 3151 (cons, "?" ^ x)
adamc@211 3152 else
adamc@211 3153 (SS.add (cons, x), x)
adamc@211 3154 in
adamc@211 3155 ((L'.SgiClassAbs (x, n), loc) :: sgis, cons, vals, sgns, strs)
adamc@211 3156 end
adamc@211 3157 | L'.SgiClass (x, n, c) =>
adamc@211 3158 let
adamc@211 3159 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
adamc@211 3160
adamc@211 3161 val (cons, x) =
adamc@211 3162 if SS.member (cons, x) then
adamc@211 3163 (cons, "?" ^ x)
adamc@211 3164 else
adamc@211 3165 (SS.add (cons, x), x)
adamc@211 3166 in
adamc@211 3167 ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@203 3168 end)
adamc@64 3169
adamc@63 3170 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
adamc@31 3171 in
adamc@83 3172 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)
adamc@31 3173 end
adamc@31 3174 | L.StrVar x =>
adamc@31 3175 (case E.lookupStr env x of
adamc@31 3176 NONE =>
adamc@31 3177 (strError env (UnboundStr (loc, x));
adamc@83 3178 (strerror, sgnerror, []))
adamc@83 3179 | SOME (n, sgn) => ((L'.StrVar n, loc), sgn, []))
adamc@34 3180 | L.StrProj (str, x) =>
adamc@34 3181 let
adamc@83 3182 val (str', sgn, gs) = elabStr (env, denv) str
adamc@34 3183 in
adamc@34 3184 case E.projectStr env {str = str', sgn = sgn, field = x} of
adamc@34 3185 NONE => (strError env (UnboundStr (loc, x));
adamc@83 3186 (strerror, sgnerror, []))
adamc@83 3187 | SOME sgn => ((L'.StrProj (str', x), loc), sgn, gs)
adamc@34 3188 end
adamc@41 3189 | L.StrFun (m, dom, ranO, str) =>
adamc@41 3190 let
adamc@83 3191 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41 3192 val (env', n) = E.pushStrNamed env m dom'
adamc@83 3193 val (str', actual, gs2) = elabStr (env', denv) str
adamc@41 3194
adamc@83 3195 val (formal, gs3) =
adamc@41 3196 case ranO of
adamc@83 3197 NONE => (actual, [])
adamc@41 3198 | SOME ran =>
adamc@41 3199 let
adamc@83 3200 val (ran', gs) = elabSgn (env', denv) ran
adamc@41 3201 in
adamc@86 3202 subSgn (env', denv) actual ran';
adamc@83 3203 (ran', gs)
adamc@41 3204 end
adamc@41 3205 in
adamc@41 3206 ((L'.StrFun (m, n, dom', formal, str'), loc),
adamc@83 3207 (L'.SgnFun (m, n, dom', formal), loc),
adamc@83 3208 gs1 @ gs2 @ gs3)
adamc@41 3209 end
adamc@44 3210 | L.StrApp (str1, str2) =>
adamc@44 3211 let
adamc@83 3212 val (str1', sgn1, gs1) = elabStr (env, denv) str1
adamc@83 3213 val (str2', sgn2, gs2) = elabStr (env, denv) str2
adamc@44 3214 in
adamc@44 3215 case #1 (hnormSgn env sgn1) of
adamc@83 3216 L'.SgnError => (strerror, sgnerror, [])
adamc@44 3217 | L'.SgnFun (m, n, dom, ran) =>
adamc@86 3218 (subSgn (env, denv) sgn2 dom;
adamc@44 3219 case #1 (hnormSgn env ran) of
adamc@83 3220 L'.SgnError => (strerror, sgnerror, [])
adamc@44 3221 | L'.SgnConst sgis =>
adamc@44 3222 ((L'.StrApp (str1', str2'), loc),
adamc@83 3223 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
adamc@83 3224 gs1 @ gs2)
adamc@44 3225 | _ => raise Fail "Unable to hnormSgn in functor application")
adamc@44 3226 | _ => (strError env (NotFunctor sgn1);
adamc@83 3227 (strerror, sgnerror, []))
adamc@44 3228 end
adamc@31 3229
adamc@56 3230 fun elabFile basis env file =
adamc@56 3231 let
adamc@83 3232 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
adamc@83 3233 val () = case gs of
adamc@83 3234 [] => ()
adamc@207 3235 | _ => (app (fn (_, env, _, c1, c2) =>
adamc@207 3236 prefaces "Unresolved"
adamc@207 3237 [("c1", p_con env c1),
adamc@207 3238 ("c2", p_con env c2)]) gs;
adamc@207 3239 raise Fail "Unresolved disjointness constraints in Basis")
adamc@83 3240
adamc@56 3241 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
adamc@210 3242 val () = basis_r := basis_n
adamc@56 3243
adamc@88 3244 val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn}
adamc@56 3245
adamc@56 3246 fun discoverC r x =
adamc@56 3247 case E.lookupC env' x of
adamc@56 3248 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
adamc@56 3249 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
adamc@56 3250 | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc)
adamc@56 3251
adamc@56 3252 val () = discoverC int "int"
adamc@56 3253 val () = discoverC float "float"
adamc@56 3254 val () = discoverC string "string"
adamc@203 3255 val () = discoverC table "sql_table"
adamc@56 3256
adamc@83 3257 fun elabDecl' (d, (env, gs)) =
adamc@76 3258 let
adamc@76 3259 val () = resetKunif ()
adamc@76 3260 val () = resetCunif ()
adamc@88 3261 val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs))
adamc@76 3262 in
adamc@76 3263 if ErrorMsg.anyErrors () then
adamc@76 3264 ()
adamc@76 3265 else (
adamc@76 3266 if List.exists kunifsInDecl ds then
adamc@91 3267 declError env (KunifsRemain ds)
adamc@76 3268 else
adamc@76 3269 ();
adamc@76 3270
adamc@76 3271 case ListUtil.search cunifsInDecl ds of
adamc@76 3272 NONE => ()
adamc@76 3273 | SOME loc =>
adamc@91 3274 declError env (CunifsRemain ds)
adamc@76 3275 );
adamc@76 3276
adamc@83 3277 (ds, (env, gs))
adamc@76 3278 end
adamc@76 3279
adamc@83 3280 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
adamc@56 3281 in
adamc@84 3282 if ErrorMsg.anyErrors () then
adamc@84 3283 ()
adamc@84 3284 else
adamc@90 3285 app (fn (loc, env, denv, c1, c2) =>
adamc@84 3286 case D.prove env denv (c1, c2, loc) of
adamc@84 3287 [] => ()
adamc@84 3288 | _ =>
adamc@86 3289 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
adamc@84 3290 eprefaces' [("Con 1", p_con env c1),
adamc@90 3291 ("Con 2", p_con env c2),
adamc@90 3292 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
adamc@90 3293 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) gs;
adamc@83 3294
adamc@56 3295 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
adamc@56 3296 end
adamc@2 3297
adamc@2 3298 end