Ur/Web: src/elaborate.sml annotate

annotate src/elaborate.sml @ 175:b2d752455182

Elaborating record patterns

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 31 Jul 2008 13:08:57 -0400
parents	7ee424760d2f
children	33d4a8eea484

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

Mercurial > urweb

annotate src/elaborate.sml @ 175:b2d752455182