Ur/Web: src/elaborate.sml annotate

annotate src/elaborate.sml @ 200:5dbba661deab

Urlifying records

author	Adam Chlipala <adamc@hcoop.net>
date	Sat, 09 Aug 2008 20:08:29 -0400
parents	df5fd8f6913a
children	dd82457fda82

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@86	907 fun elabHead (env, denv) (e as (_, loc)) t =
adamc@15	908 let
adamc@15	909 fun unravel (t, e) =
adamc@86	910 let
adamc@86	911 val (t, gs) = hnormCon (env, denv) t
adamc@86	912 in
adamc@86	913 case t of
adamc@86	914 (L'.TCFun (L'.Implicit, x, k, t'), _) =>
adamc@86	915 let
adamc@86	916 val u = cunif (loc, k)
adamc@86	917
adamc@86	918 val (e, t, gs') = unravel (subConInCon (0, u) t',
adamc@86	919 (L'.ECApp (e, u), loc))
adamc@86	920 in
adamc@86	921 (e, t, gs @ gs')
adamc@86	922 end
adamc@86	923 \| _ => (e, t, gs)
adamc@86	924 end
adamc@15	925 in
adamc@15	926 unravel (t, e)
adamc@15	927 end
adamc@15	928
adamc@174	929 fun elabPat (pAll as (p, loc), (env, denv, bound)) =
adamc@171	930 let
adamc@171	931 val perror = (L'.PWild, loc)
adamc@171	932 val terror = (L'.CError, loc)
adamc@171	933 val pterror = (perror, terror)
adamc@171	934 val rerror = (pterror, (env, bound))
adamc@171	935
adamc@191	936 fun pcon (pc, po, xs, to, dn, dk) =
adamc@188	937 case (po, to) of
adamc@188	938 (NONE, SOME _) => (expError env (PatHasNoArg loc);
adamc@188	939 rerror)
adamc@188	940 \| (SOME _, NONE) => (expError env (PatHasArg loc);
adamc@188	941 rerror)
adamc@191	942 \| (NONE, NONE) =>
adamc@191	943 let
adamc@191	944 val k = (L'.KType, loc)
adamc@191	945 val unifs = map (fn _ => cunif (loc, k)) xs
adamc@191	946 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
adamc@191	947 in
adamc@191	948 (((L'.PCon (dk, pc, unifs, NONE), loc), dn),
adamc@191	949 (env, bound))
adamc@191	950 end
adamc@188	951 \| (SOME p, SOME t) =>
adamc@188	952 let
adamc@188	953 val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound))
adamc@191	954
adamc@191	955 val k = (L'.KType, loc)
adamc@191	956 val unifs = map (fn _ => cunif (loc, k)) xs
adamc@194	957 val nxs = length unifs - 1
adamc@194	958 val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs
adamc@191	959 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
adamc@188	960 in
adamc@191	961 ignore (checkPatCon (env, denv) p' pt t);
adamc@191	962 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
adamc@188	963 (env, bound))
adamc@188	964 end
adamc@171	965 in
adamc@171	966 case p of
adamc@171	967 L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
adamc@171	968 (env, bound))
adamc@171	969 \| L.PVar x =>
adamc@171	970 let
adamc@171	971 val t = if SS.member (bound, x) then
adamc@171	972 (expError env (DuplicatePatternVariable (loc, x));
adamc@171	973 terror)
adamc@171	974 else
adamc@171	975 cunif (loc, (L'.KType, loc))
adamc@171	976 in
adamc@182	977 (((L'.PVar (x, t), loc), t),
adamc@171	978 (E.pushERel env x t, SS.add (bound, x)))
adamc@171	979 end
adamc@173	980 \| L.PPrim p => (((L'.PPrim p, loc), primType env p),
adamc@173	981 (env, bound))
adamc@171	982 \| L.PCon ([], x, po) =>
adamc@171	983 (case E.lookupConstructor env x of
adamc@174	984 NONE => (expError env (UnboundConstructor (loc, [], x));
adamc@171	985 rerror)
adamc@191	986 \| SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk))
adamc@174	987 \| L.PCon (m1 :: ms, x, po) =>
adamc@174	988 (case E.lookupStr env m1 of
adamc@174	989 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@174	990 rerror)
adamc@174	991 \| SOME (n, sgn) =>
adamc@174	992 let
adamc@174	993 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@174	994 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@182	995 NONE => raise Fail "elabPat: Unknown substructure"
adamc@174	996 \| SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@174	997 ((L'.StrVar n, loc), sgn) ms
adamc@174	998 in
adamc@174	999 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
adamc@174	1000 NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x));
adamc@174	1001 rerror)
adamc@191	1002 \| SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk)
adamc@174	1003 end)
adamc@174	1004
adamc@175	1005 \| L.PRecord (xps, flex) =>
adamc@175	1006 let
adamc@175	1007 val (xpts, (env, bound, _)) =
adamc@175	1008 ListUtil.foldlMap (fn ((x, p), (env, bound, fbound)) =>
adamc@175	1009 let
adamc@175	1010 val ((p', t), (env, bound)) = elabPat (p, (env, denv, bound))
adamc@175	1011 in
adamc@175	1012 if SS.member (fbound, x) then
adamc@175	1013 expError env (DuplicatePatField (loc, x))
adamc@175	1014 else
adamc@175	1015 ();
adamc@175	1016 ((x, p', t), (env, bound, SS.add (fbound, x)))
adamc@175	1017 end)
adamc@175	1018 (env, bound, SS.empty) xps
adamc@175	1019
adamc@175	1020 val k = (L'.KType, loc)
adamc@175	1021 val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc)
adamc@176	1022 val c =
adamc@175	1023 if flex then
adamc@176	1024 (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc)
adamc@175	1025 else
adamc@176	1026 c
adamc@175	1027 in
adamc@182	1028 (((L'.PRecord xpts, loc),
adamc@175	1029 (L'.TRecord c, loc)),
adamc@175	1030 (env, bound))
adamc@175	1031 end
adamc@175	1032
adamc@171	1033 end
adamc@171	1034
adamc@172	1035 datatype coverage =
adamc@172	1036 Wild
adamc@173	1037 \| None
adamc@172	1038 \| Datatype of coverage IM.map
adamc@175	1039 \| Record of coverage SM.map list
adamc@172	1040
adamc@172	1041 fun exhaustive (env, denv, t, ps) =
adamc@172	1042 let
adamc@172	1043 fun pcCoverage pc =
adamc@172	1044 case pc of
adamc@172	1045 L'.PConVar n => n
adamc@174	1046 \| L'.PConProj (m1, ms, x) =>
adamc@174	1047 let
adamc@174	1048 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@174	1049 in
adamc@174	1050 case E.projectConstructor env {str = str, sgn = sgn, field = x} of
adamc@174	1051 NONE => raise Fail "exhaustive: Can't project constructor"
adamc@191	1052 \| SOME (_, n, _, _, _) => n
adamc@174	1053 end
adamc@172	1054
adamc@172	1055 fun coverage (p, _) =
adamc@172	1056 case p of
adamc@172	1057 L'.PWild => Wild
adamc@172	1058 \| L'.PVar _ => Wild
adamc@173	1059 \| L'.PPrim _ => None
adamc@191	1060 \| L'.PCon (_, pc, _, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild))
adamc@191	1061 \| L'.PCon (_, pc, _, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p))
adamc@182	1062 \| L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) =>
adamc@182	1063 SM.insert (fmap, x, coverage p)) SM.empty xps]
adamc@176	1064
adamc@172	1065 fun merge (c1, c2) =
adamc@172	1066 case (c1, c2) of
adamc@173	1067 (None, _) => c2
adamc@173	1068 \| (_, None) => c1
adamc@173	1069
adamc@173	1070 \| (Wild, _) => Wild
adamc@172	1071 \| (_, Wild) => Wild
adamc@172	1072
adamc@172	1073 \| (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2))
adamc@172	1074
adamc@175	1075 \| (Record fm1, Record fm2) => Record (fm1 @ fm2)
adamc@175	1076
adamc@175	1077 \| _ => None
adamc@175	1078
adamc@172	1079 fun combinedCoverage ps =
adamc@172	1080 case ps of
adamc@172	1081 [] => raise Fail "Empty pattern list for coverage checking"
adamc@172	1082 \| [p] => coverage p
adamc@172	1083 \| p :: ps => merge (coverage p, combinedCoverage ps)
adamc@172	1084
adamc@175	1085 fun enumerateCases t =
adamc@175	1086 let
adamc@175	1087 fun dtype cons =
adamc@175	1088 ListUtil.mapConcat (fn (_, n, to) =>
adamc@175	1089 case to of
adamc@175	1090 NONE => [Datatype (IM.insert (IM.empty, n, Wild))]
adamc@175	1091 \| SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c)))
adamc@175	1092 (enumerateCases t)) cons
adamc@175	1093 in
adamc@175	1094 case #1 (#1 (hnormCon (env, denv) t)) of
adamc@175	1095 L'.CNamed n =>
adamc@175	1096 (let
adamc@175	1097 val dt = E.lookupDatatype env n
adamc@175	1098 val cons = E.constructors dt
adamc@175	1099 in
adamc@175	1100 dtype cons
adamc@175	1101 end handle E.UnboundNamed _ => [Wild])
adamc@175	1102 \| L'.TRecord c =>
adamc@175	1103 (case #1 (#1 (hnormCon (env, denv) c)) of
adamc@175	1104 L'.CRecord (_, xts) =>
adamc@175	1105 let
adamc@175	1106 val xts = map (fn (x, t) => (#1 (hnormCon (env, denv) x), t)) xts
adamc@175	1107
adamc@175	1108 fun exponentiate fs =
adamc@175	1109 case fs of
adamc@175	1110 [] => [SM.empty]
adamc@175	1111 \| ((L'.CName x, _), t) :: rest =>
adamc@175	1112 let
adamc@175	1113 val this = enumerateCases t
adamc@175	1114 val rest = exponentiate rest
adamc@175	1115 in
adamc@175	1116 ListUtil.mapConcat (fn fmap =>
adamc@175	1117 map (fn c => SM.insert (fmap, x, c)) this) rest
adamc@175	1118 end
adamc@175	1119 \| _ => raise Fail "exponentiate: Not CName"
adamc@175	1120 in
adamc@175	1121 if List.exists (fn ((L'.CName _, _), _) => false
adamc@175	1122 \| (c, _) => true) xts then
adamc@175	1123 [Wild]
adamc@175	1124 else
adamc@175	1125 map (fn ls => Record [ls]) (exponentiate xts)
adamc@175	1126 end
adamc@175	1127 \| _ => [Wild])
adamc@175	1128 \| _ => [Wild]
adamc@175	1129 end
adamc@175	1130
adamc@175	1131 fun coverageImp (c1, c2) =
adamc@175	1132 case (c1, c2) of
adamc@175	1133 (Wild, _) => true
adamc@175	1134
adamc@175	1135 \| (Datatype cmap1, Datatype cmap2) =>
adamc@175	1136 List.all (fn (n, c2) =>
adamc@175	1137 case IM.find (cmap1, n) of
adamc@175	1138 NONE => false
adamc@175	1139 \| SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2)
adamc@175	1140
adamc@175	1141 \| (Record fmaps1, Record fmaps2) =>
adamc@175	1142 List.all (fn fmap2 =>
adamc@175	1143 List.exists (fn fmap1 =>
adamc@175	1144 List.all (fn (x, c2) =>
adamc@175	1145 case SM.find (fmap1, x) of
adamc@175	1146 NONE => true
adamc@175	1147 \| SOME c1 => coverageImp (c1, c2))
adamc@175	1148 (SM.listItemsi fmap2))
adamc@175	1149 fmaps1) fmaps2
adamc@175	1150
adamc@175	1151 \| _ => false
adamc@175	1152
adamc@172	1153 fun isTotal (c, t) =
adamc@172	1154 case c of
adamc@173	1155 None => (false, [])
adamc@173	1156 \| Wild => (true, [])
adamc@172	1157 \| Datatype cm =>
adamc@172	1158 let
adamc@172	1159 val ((t, _), gs) = hnormCon (env, denv) t
adamc@174	1160
adamc@174	1161 fun dtype cons =
adamc@174	1162 foldl (fn ((_, n, to), (total, gs)) =>
adamc@174	1163 case IM.find (cm, n) of
adamc@174	1164 NONE => (false, gs)
adamc@174	1165 \| SOME c' =>
adamc@174	1166 case to of
adamc@174	1167 NONE => (total, gs)
adamc@174	1168 \| SOME t' =>
adamc@174	1169 let
adamc@174	1170 val (total, gs') = isTotal (c', t')
adamc@174	1171 in
adamc@174	1172 (total, gs' @ gs)
adamc@174	1173 end)
adamc@174	1174 (true, gs) cons
adamc@191	1175
adamc@191	1176 fun unapp t =
adamc@191	1177 case t of
adamc@191	1178 L'.CApp ((t, _), _) => unapp t
adamc@191	1179 \| _ => t
adamc@172	1180 in
adamc@191	1181 case unapp t of
adamc@172	1182 L'.CNamed n =>
adamc@172	1183 let
adamc@172	1184 val dt = E.lookupDatatype env n
adamc@172	1185 val cons = E.constructors dt
adamc@172	1186 in
adamc@174	1187 dtype cons
adamc@174	1188 end
adamc@174	1189 \| L'.CModProj (m1, ms, x) =>
adamc@174	1190 let
adamc@174	1191 val (str, sgn) = E.chaseMpath env (m1, ms)
adamc@174	1192 in
adamc@174	1193 case E.projectDatatype env {str = str, sgn = sgn, field = x} of
adamc@174	1194 NONE => raise Fail "isTotal: Can't project datatype"
adamc@191	1195 \| SOME (_, cons) => dtype cons
adamc@172	1196 end
adamc@172	1197 \| L'.CError => (true, gs)
adamc@172	1198 \| _ => raise Fail "isTotal: Not a datatype"
adamc@172	1199 end
adamc@175	1200 \| Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases t), [])
adamc@172	1201 in
adamc@172	1202 isTotal (combinedCoverage ps, t)
adamc@172	1203 end
adamc@172	1204
adamc@92	1205 fun elabExp (env, denv) (eAll as (e, loc)) =
adamc@91	1206 let
adamc@92	1207
adamc@92	1208 in
adamc@92	1209 (eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];)
adamc@10	1210
adamc@91	1211 case e of
adamc@91	1212 L.EAnnot (e, t) =>
adamc@91	1213 let
adamc@91	1214 val (e', et, gs1) = elabExp (env, denv) e
adamc@91	1215 val (t', _, gs2) = elabCon (env, denv) t
adamc@91	1216 val gs3 = checkCon (env, denv) e' et t'
adamc@91	1217 in
adamc@91	1218 (e', t', gs1 @ gs2 @ gs3)
adamc@91	1219 end
adamc@34	1220
adamc@91	1221 \| L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
adamc@91	1222 \| L.EVar ([], s) =>
adamc@91	1223 (case E.lookupE env s of
adamc@91	1224 E.NotBound =>
adamc@91	1225 (expError env (UnboundExp (loc, s));
adamc@91	1226 (eerror, cerror, []))
adamc@91	1227 \| E.Rel (n, t) => ((L'.ERel n, loc), t, [])
adamc@191	1228 \| E.Named (n, t) =>
adamc@191	1229 if Char.isUpper (String.sub (s, 0)) then
adamc@191	1230 elabHead (env, denv) (L'.ENamed n, loc) t
adamc@191	1231 else
adamc@191	1232 ((L'.ENamed n, loc), t, []))
adamc@91	1233 \| L.EVar (m1 :: ms, s) =>
adamc@91	1234 (case E.lookupStr env m1 of
adamc@91	1235 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@91	1236 (eerror, cerror, []))
adamc@91	1237 \| SOME (n, sgn) =>
adamc@91	1238 let
adamc@91	1239 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@91	1240 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@91	1241 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@91	1242 (strerror, sgnerror))
adamc@91	1243 \| SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@91	1244 ((L'.StrVar n, loc), sgn) ms
adamc@10	1245
adamc@91	1246 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
adamc@91	1247 NONE => (expError env (UnboundExp (loc, s));
adamc@91	1248 cerror)
adamc@91	1249 \| SOME t => t
adamc@91	1250 in
adamc@91	1251 ((L'.EModProj (n, ms, s), loc), t, [])
adamc@91	1252 end)
adamc@86	1253
adamc@91	1254 \| L.EApp (e1, e2) =>
adamc@91	1255 let
adamc@91	1256 val (e1', t1, gs1) = elabExp (env, denv) e1
adamc@91	1257 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
adamc@91	1258 val (e2', t2, gs3) = elabExp (env, denv) e2
adamc@71	1259
adamc@91	1260 val dom = cunif (loc, ktype)
adamc@91	1261 val ran = cunif (loc, ktype)
adamc@91	1262 val t = (L'.TFun (dom, ran), dummy)
adamc@91	1263
adamc@91	1264 val gs4 = checkCon (env, denv) e1' t1 t
adamc@91	1265 val gs5 = checkCon (env, denv) e2' t2 dom
adamc@91	1266 in
adamc@91	1267 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
adamc@91	1268 end
adamc@91	1269 \| L.EAbs (x, to, e) =>
adamc@91	1270 let
adamc@91	1271 val (t', gs1) = case to of
adamc@91	1272 NONE => (cunif (loc, ktype), [])
adamc@91	1273 \| SOME t =>
adamc@91	1274 let
adamc@91	1275 val (t', tk, gs) = elabCon (env, denv) t
adamc@91	1276 in
adamc@91	1277 checkKind env t' tk ktype;
adamc@91	1278 (t', gs)
adamc@91	1279 end
adamc@91	1280 val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e
adamc@91	1281 in
adamc@91	1282 ((L'.EAbs (x, t', et, e'), loc),
adamc@91	1283 (L'.TFun (t', et), loc),
adamc@91	1284 gs1 @ gs2)
adamc@91	1285 end
adamc@91	1286 \| L.ECApp (e, c) =>
adamc@91	1287 let
adamc@91	1288 val (e', et, gs1) = elabExp (env, denv) e
adamc@91	1289 val (e', et, gs2) = elabHead (env, denv) e' et
adamc@91	1290 val (c', ck, gs3) = elabCon (env, denv) c
adamc@91	1291 val ((et', _), gs4) = hnormCon (env, denv) et
adamc@91	1292 in
adamc@91	1293 case et' of
adamc@91	1294 L'.CError => (eerror, cerror, [])
adamc@91	1295 \| L'.TCFun (_, _, k, eb) =>
adamc@91	1296 let
adamc@91	1297 val () = checkKind env c' ck k
adamc@91	1298 val eb' = subConInCon (0, c') eb
adamc@91	1299 handle SynUnif => (expError env (Unif ("substitution", eb));
adamc@91	1300 cerror)
adamc@91	1301 in
adamc@91	1302 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
adamc@91	1303 end
adamc@91	1304
adamc@91	1305 \| L'.CUnif _ =>
adamc@91	1306 (expError env (Unif ("application", et));
adamc@91	1307 (eerror, cerror, []))
adamc@91	1308
adamc@91	1309 \| _ =>
adamc@91	1310 (expError env (WrongForm ("constructor function", e', et));
adamc@91	1311 (eerror, cerror, []))
adamc@91	1312 end
adamc@91	1313 \| L.ECAbs (expl, x, k, e) =>
adamc@91	1314 let
adamc@91	1315 val expl' = elabExplicitness expl
adamc@91	1316 val k' = elabKind k
adamc@91	1317 val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
adamc@91	1318 in
adamc@91	1319 ((L'.ECAbs (expl', x, k', e'), loc),
adamc@91	1320 (L'.TCFun (expl', x, k', et), loc),
adamc@91	1321 gs)
adamc@91	1322 end
adamc@91	1323
adamc@91	1324 \| L.EDisjoint (c1, c2, e) =>
adamc@91	1325 let
adamc@91	1326 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@91	1327 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@91	1328
adamc@91	1329 val ku1 = kunif loc
adamc@91	1330 val ku2 = kunif loc
adamc@91	1331
adamc@91	1332 val (denv', gs3) = D.assert env denv (c1', c2')
adamc@91	1333 val (e', t, gs4) = elabExp (env, denv') e
adamc@91	1334 in
adamc@91	1335 checkKind env c1' k1 (L'.KRecord ku1, loc);
adamc@91	1336 checkKind env c2' k2 (L'.KRecord ku2, loc);
adamc@91	1337
adamc@91	1338 (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
adamc@91	1339 end
adamc@91	1340
adamc@91	1341 \| L.ERecord xes =>
adamc@91	1342 let
adamc@91	1343 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
adamc@91	1344 let
adamc@91	1345 val (x', xk, gs1) = elabCon (env, denv) x
adamc@91	1346 val (e', et, gs2) = elabExp (env, denv) e
adamc@91	1347 in
adamc@91	1348 checkKind env x' xk kname;
adamc@91	1349 ((x', e', et), gs1 @ gs2 @ gs)
adamc@91	1350 end)
adamc@91	1351 [] xes
adamc@91	1352
adamc@91	1353 val k = (L'.KType, loc)
adamc@91	1354
adamc@91	1355 fun prove (xets, gs) =
adamc@91	1356 case xets of
adamc@91	1357 [] => gs
adamc@91	1358 \| (x, _, t) :: rest =>
adamc@91	1359 let
adamc@91	1360 val xc = (x, t)
adamc@91	1361 val r1 = (L'.CRecord (k, [xc]), loc)
adamc@91	1362 val gs = foldl (fn ((x', _, t'), gs) =>
adamc@91	1363 let
adamc@91	1364 val xc' = (x', t')
adamc@91	1365 val r2 = (L'.CRecord (k, [xc']), loc)
adamc@91	1366 in
adamc@91	1367 D.prove env denv (r1, r2, loc) @ gs
adamc@91	1368 end)
adamc@91	1369 gs rest
adamc@91	1370 in
adamc@91	1371 prove (rest, gs)
adamc@91	1372 end
adamc@91	1373 in
adamc@91	1374 ((L'.ERecord xes', loc),
adamc@91	1375 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
adamc@91	1376 prove (xes', gs))
adamc@91	1377 end
adamc@91	1378
adamc@91	1379 \| L.EField (e, c) =>
adamc@91	1380 let
adamc@91	1381 val (e', et, gs1) = elabExp (env, denv) e
adamc@91	1382 val (c', ck, gs2) = elabCon (env, denv) c
adamc@91	1383
adamc@91	1384 val ft = cunif (loc, ktype)
adamc@91	1385 val rest = cunif (loc, ktype_record)
adamc@91	1386 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
adamc@91	1387
adamc@91	1388 val gs3 =
adamc@91	1389 checkCon (env, denv) e' et
adamc@91	1390 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
adamc@91	1391 val gs4 = D.prove env denv (first, rest, loc)
adamc@91	1392 in
adamc@91	1393 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
adamc@91	1394 end
adamc@91	1395
adamc@149	1396 \| L.ECut (e, c) =>
adamc@149	1397 let
adamc@149	1398 val (e', et, gs1) = elabExp (env, denv) e
adamc@149	1399 val (c', ck, gs2) = elabCon (env, denv) c
adamc@149	1400
adamc@149	1401 val ft = cunif (loc, ktype)
adamc@149	1402 val rest = cunif (loc, ktype_record)
adamc@149	1403 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
adamc@149	1404
adamc@149	1405 val gs3 =
adamc@149	1406 checkCon (env, denv) e' et
adamc@149	1407 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
adamc@149	1408 val gs4 = D.prove env denv (first, rest, loc)
adamc@149	1409 in
adamc@149	1410 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), gs1 @ gs2 @ gs3 @ gs4)
adamc@149	1411 end
adamc@149	1412
adamc@91	1413 \| L.EFold =>
adamc@91	1414 let
adamc@91	1415 val dom = kunif loc
adamc@91	1416 in
adamc@91	1417 ((L'.EFold dom, loc), foldType (dom, loc), [])
adamc@91	1418 end
adamc@170	1419
adamc@171	1420 \| L.ECase (e, pes) =>
adamc@171	1421 let
adamc@171	1422 val (e', et, gs1) = elabExp (env, denv) e
adamc@171	1423 val result = cunif (loc, (L'.KType, loc))
adamc@171	1424 val (pes', gs) = ListUtil.foldlMap
adamc@171	1425 (fn ((p, e), gs) =>
adamc@171	1426 let
adamc@174	1427 val ((p', pt), (env, _)) = elabPat (p, (env, denv, SS.empty))
adamc@171	1428
adamc@171	1429 val gs1 = checkPatCon (env, denv) p' pt et
adamc@171	1430 val (e', et, gs2) = elabExp (env, denv) e
adamc@171	1431 val gs3 = checkCon (env, denv) e' et result
adamc@171	1432 in
adamc@171	1433 ((p', e'), gs1 @ gs2 @ gs3 @ gs)
adamc@171	1434 end)
adamc@171	1435 gs1 pes
adamc@172	1436
adamc@172	1437 val (total, gs') = exhaustive (env, denv, et, map #1 pes')
adamc@171	1438 in
adamc@172	1439 if total then
adamc@172	1440 ()
adamc@172	1441 else
adamc@172	1442 expError env (Inexhaustive loc);
adamc@172	1443
adamc@182	1444 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs' @ gs)
adamc@171	1445 end
adamc@91	1446 end
adamc@12	1447
adamc@12	1448
adamc@6	1449 datatype decl_error =
adamc@91	1450 KunifsRemain of L'.decl list
adamc@91	1451 \| CunifsRemain of L'.decl list
adamc@91	1452
adamc@91	1453 fun lspan [] = ErrorMsg.dummySpan
adamc@91	1454 \| lspan ((_, loc) :: _) = loc
adamc@6	1455
adamc@6	1456 fun declError env err =
adamc@6	1457 case err of
adamc@91	1458 KunifsRemain ds =>
adamc@91	1459 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
adamc@91	1460 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@91	1461 \| CunifsRemain ds =>
adamc@91	1462 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
adamc@91	1463 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
adamc@6	1464
adamc@31	1465 datatype sgn_error =
adamc@31	1466 UnboundSgn of ErrorMsg.span * string
adamc@31	1467 \| UnmatchedSgi of L'.sgn_item
adamc@31	1468 \| SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
adamc@31	1469 \| SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
adamc@156	1470 \| SgiMismatchedDatatypes of L'.sgn_item * L'.sgn_item * (L'.con * L'.con * cunify_error) option
adamc@41	1471 \| SgnWrongForm of L'.sgn * L'.sgn
adamc@42	1472 \| UnWhereable of L'.sgn * string
adamc@75	1473 \| WhereWrongKind of L'.kind * L'.kind * kunify_error
adamc@58	1474 \| NotIncludable of L'.sgn
adamc@62	1475 \| DuplicateCon of ErrorMsg.span * string
adamc@62	1476 \| DuplicateVal of ErrorMsg.span * string
adamc@62	1477 \| DuplicateSgn of ErrorMsg.span * string
adamc@62	1478 \| DuplicateStr of ErrorMsg.span * string
adamc@88	1479 \| NotConstraintsable of L'.sgn
adamc@31	1480
adamc@31	1481 fun sgnError env err =
adamc@31	1482 case err of
adamc@31	1483 UnboundSgn (loc, s) =>
adamc@31	1484 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
adamc@31	1485 \| UnmatchedSgi (sgi as (_, loc)) =>
adamc@31	1486 (ErrorMsg.errorAt loc "Unmatched signature item";
adamc@31	1487 eprefaces' [("Item", p_sgn_item env sgi)])
adamc@31	1488 \| SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
adamc@31	1489 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
adamc@59	1490 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@59	1491 ("Need", p_sgn_item env sgi2),
adamc@31	1492 ("Kind 1", p_kind k1),
adamc@31	1493 ("Kind 2", p_kind k2)];
adamc@31	1494 kunifyError kerr)
adamc@31	1495 \| SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
adamc@31	1496 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
adamc@59	1497 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@59	1498 ("Need", p_sgn_item env sgi2),
adamc@31	1499 ("Con 1", p_con env c1),
adamc@31	1500 ("Con 2", p_con env c2)];
adamc@31	1501 cunifyError env cerr)
adamc@156	1502 \| SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
adamc@156	1503 (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
adamc@156	1504 eprefaces' [("Have", p_sgn_item env sgi1),
adamc@156	1505 ("Need", p_sgn_item env sgi2)];
adamc@156	1506 Option.app (fn (c1, c2, ue) =>
adamc@156	1507 (eprefaces "Unification error"
adamc@156	1508 [("Con 1", p_con env c1),
adamc@156	1509 ("Con 2", p_con env c2)];
adamc@156	1510 cunifyError env ue)) cerro)
adamc@41	1511 \| SgnWrongForm (sgn1, sgn2) =>
adamc@41	1512 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
adamc@41	1513 eprefaces' [("Sig 1", p_sgn env sgn1),
adamc@41	1514 ("Sig 2", p_sgn env sgn2)])
adamc@42	1515 \| UnWhereable (sgn, x) =>
adamc@42	1516 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
adamc@42	1517 eprefaces' [("Signature", p_sgn env sgn),
adamc@42	1518 ("Field", PD.string x)])
adamc@75	1519 \| WhereWrongKind (k1, k2, kerr) =>
adamc@75	1520 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
adamc@75	1521 eprefaces' [("Have", p_kind k1),
adamc@75	1522 ("Need", p_kind k2)];
adamc@75	1523 kunifyError kerr)
adamc@58	1524 \| NotIncludable sgn =>
adamc@58	1525 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
adamc@58	1526 eprefaces' [("Signature", p_sgn env sgn)])
adamc@62	1527 \| DuplicateCon (loc, s) =>
adamc@62	1528 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
adamc@62	1529 \| DuplicateVal (loc, s) =>
adamc@62	1530 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
adamc@62	1531 \| DuplicateSgn (loc, s) =>
adamc@62	1532 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
adamc@62	1533 \| DuplicateStr (loc, s) =>
adamc@62	1534 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
adamc@88	1535 \| NotConstraintsable sgn =>
adamc@88	1536 (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
adamc@88	1537 eprefaces' [("Signature", p_sgn env sgn)])
adamc@31	1538
adamc@31	1539 datatype str_error =
adamc@31	1540 UnboundStr of ErrorMsg.span * string
adamc@44	1541 \| NotFunctor of L'.sgn
adamc@46	1542 \| FunctorRebind of ErrorMsg.span
adamc@61	1543 \| UnOpenable of L'.sgn
adamc@75	1544 \| NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
adamc@156	1545 \| DuplicateConstructor of string * ErrorMsg.span
adamc@158	1546 \| NotDatatype of ErrorMsg.span
adamc@31	1547
adamc@31	1548 fun strError env err =
adamc@31	1549 case err of
adamc@31	1550 UnboundStr (loc, s) =>
adamc@31	1551 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
adamc@44	1552 \| NotFunctor sgn =>
adamc@44	1553 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
adamc@44	1554 eprefaces' [("Signature", p_sgn env sgn)])
adamc@46	1555 \| FunctorRebind loc =>
adamc@46	1556 ErrorMsg.errorAt loc "Attempt to rebind functor"
adamc@61	1557 \| UnOpenable sgn =>
adamc@61	1558 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
adamc@61	1559 eprefaces' [("Signature", p_sgn env sgn)])
adamc@75	1560 \| NotType (k, (k1, k2, ue)) =>
adamc@75	1561 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
adamc@75	1562 eprefaces' [("Kind", p_kind k),
adamc@75	1563 ("Subkind 1", p_kind k1),
adamc@75	1564 ("Subkind 2", p_kind k2)];
adamc@75	1565 kunifyError ue)
adamc@156	1566 \| DuplicateConstructor (x, loc) =>
adamc@156	1567 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
adamc@158	1568 \| NotDatatype loc =>
adamc@158	1569 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
adamc@31	1570
adamc@42	1571 val hnormSgn = E.hnormSgn
adamc@31	1572
adamc@88	1573 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
adamc@76	1574 case sgi of
adamc@76	1575 L.SgiConAbs (x, k) =>
adamc@76	1576 let
adamc@76	1577 val k' = elabKind k
adamc@31	1578
adamc@76	1579 val (env', n) = E.pushCNamed env x k' NONE
adamc@76	1580 in
adamc@88	1581 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs))
adamc@76	1582 end
adamc@31	1583
adamc@76	1584 \| L.SgiCon (x, ko, c) =>
adamc@76	1585 let
adamc@76	1586 val k' = case ko of
adamc@76	1587 NONE => kunif loc
adamc@76	1588 \| SOME k => elabKind k
adamc@31	1589
adamc@83	1590 val (c', ck, gs') = elabCon (env, denv) c
adamc@76	1591 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@76	1592 in
adamc@76	1593 checkKind env c' ck k';
adamc@31	1594
adamc@88	1595 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
adamc@76	1596 end
adamc@31	1597
adamc@191	1598 \| L.SgiDatatype (x, xs, xcs) =>
adamc@157	1599 let
adamc@157	1600 val k = (L'.KType, loc)
adamc@191	1601 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191	1602 val (env, n) = E.pushCNamed env x k' NONE
adamc@157	1603 val t = (L'.CNamed n, loc)
adamc@194	1604 val nxs = length xs - 1
adamc@194	1605 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@157	1606
adamc@157	1607 val (xcs, (used, env, gs)) =
adamc@157	1608 ListUtil.foldlMap
adamc@157	1609 (fn ((x, to), (used, env, gs)) =>
adamc@157	1610 let
adamc@157	1611 val (to, t, gs') = case to of
adamc@157	1612 NONE => (NONE, t, gs)
adamc@157	1613 \| SOME t' =>
adamc@157	1614 let
adamc@157	1615 val (t', tk, gs') = elabCon (env, denv) t'
adamc@157	1616 in
adamc@157	1617 checkKind env t' tk k;
adamc@157	1618 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
adamc@157	1619 end
adamc@191	1620 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
adamc@157	1621
adamc@157	1622 val (env, n') = E.pushENamed env x t
adamc@157	1623 in
adamc@157	1624 if SS.member (used, x) then
adamc@157	1625 strError env (DuplicateConstructor (x, loc))
adamc@157	1626 else
adamc@157	1627 ();
adamc@157	1628 ((x, n', to), (SS.add (used, x), env, gs'))
adamc@157	1629 end)
adamc@157	1630 (SS.empty, env, []) xcs
adamc@191	1631
adamc@191	1632 val env = E.pushDatatype env n xs xcs
adamc@157	1633 in
adamc@191	1634 ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
adamc@157	1635 end
adamc@156	1636
adamc@158	1637 \| L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
adamc@158	1638
adamc@158	1639 \| L.SgiDatatypeImp (x, m1 :: ms, s) =>
adamc@158	1640 (case E.lookupStr env m1 of
adamc@158	1641 NONE => (strError env (UnboundStr (loc, m1));
adamc@158	1642 ([], (env, denv, gs)))
adamc@158	1643 \| SOME (n, sgn) =>
adamc@158	1644 let
adamc@158	1645 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@158	1646 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@158	1647 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@158	1648 (strerror, sgnerror))
adamc@158	1649 \| SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@158	1650 ((L'.StrVar n, loc), sgn) ms
adamc@158	1651 in
adamc@161	1652 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
adamc@161	1653 ((L'.CModProj (n, ms, s), _), gs) =>
adamc@161	1654 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
adamc@161	1655 NONE => (conError env (UnboundDatatype (loc, s));
adamc@161	1656 ([], (env, denv, gs)))
adamc@191	1657 \| SOME (xs, xncs) =>
adamc@161	1658 let
adamc@161	1659 val k = (L'.KType, loc)
adamc@191	1660 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191	1661
adamc@161	1662 val t = (L'.CModProj (n, ms, s), loc)
adamc@191	1663 val (env, n') = E.pushCNamed env x k' (SOME t)
adamc@191	1664 val env = E.pushDatatype env n' xs xncs
adamc@158	1665
adamc@161	1666 val t = (L'.CNamed n', loc)
adamc@161	1667 val env = foldl (fn ((x, n, to), env) =>
adamc@161	1668 let
adamc@161	1669 val t = case to of
adamc@161	1670 NONE => t
adamc@161	1671 \| SOME t' => (L'.TFun (t', t), loc)
adamc@191	1672
adamc@191	1673 val t = foldr (fn (x, t) =>
adamc@191	1674 (L'.TCFun (L'.Implicit, x, k, t), loc))
adamc@191	1675 t xs
adamc@161	1676 in
adamc@161	1677 E.pushENamedAs env x n t
adamc@161	1678 end) env xncs
adamc@161	1679 in
adamc@191	1680 ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
adamc@161	1681 end)
adamc@161	1682 \| _ => (strError env (NotDatatype loc);
adamc@161	1683 ([], (env, denv, [])))
adamc@158	1684 end)
adamc@156	1685
adamc@76	1686 \| L.SgiVal (x, c) =>
adamc@76	1687 let
adamc@83	1688 val (c', ck, gs') = elabCon (env, denv) c
adamc@31	1689
adamc@76	1690 val (env', n) = E.pushENamed env x c'
adamc@76	1691 in
adamc@76	1692 (unifyKinds ck ktype
adamc@76	1693 handle KUnify ue => strError env (NotType (ck, ue)));
adamc@31	1694
adamc@88	1695 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
adamc@76	1696 end
adamc@31	1697
adamc@76	1698 \| L.SgiStr (x, sgn) =>
adamc@76	1699 let
adamc@83	1700 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76	1701 val (env', n) = E.pushStrNamed env x sgn'
adamc@76	1702 in
adamc@88	1703 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76	1704 end
adamc@31	1705
adamc@76	1706 \| L.SgiSgn (x, sgn) =>
adamc@76	1707 let
adamc@83	1708 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76	1709 val (env', n) = E.pushSgnNamed env x sgn'
adamc@76	1710 in
adamc@88	1711 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76	1712 end
adamc@31	1713
adamc@76	1714 \| L.SgiInclude sgn =>
adamc@76	1715 let
adamc@83	1716 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76	1717 in
adamc@76	1718 case #1 (hnormSgn env sgn') of
adamc@76	1719 L'.SgnConst sgis =>
adamc@88	1720 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs))
adamc@76	1721 \| _ => (sgnError env (NotIncludable sgn');
adamc@88	1722 ([], (env, denv, [])))
adamc@88	1723 end
adamc@88	1724
adamc@88	1725 \| L.SgiConstraint (c1, c2) =>
adamc@88	1726 let
adamc@88	1727 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@88	1728 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@88	1729
adamc@90	1730 val (denv, gs3) = D.assert env denv (c1', c2')
adamc@88	1731 in
adamc@88	1732 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
adamc@88	1733 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
adamc@88	1734
adamc@90	1735 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
adamc@76	1736 end
adamc@31	1737
adamc@83	1738 and elabSgn (env, denv) (sgn, loc) =
adamc@31	1739 case sgn of
adamc@31	1740 L.SgnConst sgis =>
adamc@31	1741 let
adamc@88	1742 val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis
adamc@62	1743
adamc@62	1744 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) =>
adamc@62	1745 case sgi of
adamc@62	1746 L'.SgiConAbs (x, _, _) =>
adamc@62	1747 (if SS.member (cons, x) then
adamc@62	1748 sgnError env (DuplicateCon (loc, x))
adamc@62	1749 else
adamc@62	1750 ();
adamc@62	1751 (SS.add (cons, x), vals, sgns, strs))
adamc@62	1752 \| L'.SgiCon (x, _, _, _) =>
adamc@62	1753 (if SS.member (cons, x) then
adamc@62	1754 sgnError env (DuplicateCon (loc, x))
adamc@62	1755 else
adamc@62	1756 ();
adamc@62	1757 (SS.add (cons, x), vals, sgns, strs))
adamc@191	1758 \| L'.SgiDatatype (x, _, _, xncs) =>
adamc@156	1759 let
adamc@156	1760 val vals = foldl (fn ((x, _, _), vals) =>
adamc@156	1761 (if SS.member (vals, x) then
adamc@156	1762 sgnError env (DuplicateVal (loc, x))
adamc@156	1763 else
adamc@156	1764 ();
adamc@156	1765 SS.add (vals, x)))
adamc@156	1766 vals xncs
adamc@156	1767 in
adamc@156	1768 if SS.member (cons, x) then
adamc@156	1769 sgnError env (DuplicateCon (loc, x))
adamc@156	1770 else
adamc@156	1771 ();
adamc@156	1772 (SS.add (cons, x), vals, sgns, strs)
adamc@156	1773 end
adamc@191	1774 \| L'.SgiDatatypeImp (x, _, _, _, _, _, _) =>
adamc@156	1775 (if SS.member (cons, x) then
adamc@156	1776 sgnError env (DuplicateCon (loc, x))
adamc@156	1777 else
adamc@156	1778 ();
adamc@156	1779 (SS.add (cons, x), vals, sgns, strs))
adamc@62	1780 \| L'.SgiVal (x, _, _) =>
adamc@62	1781 (if SS.member (vals, x) then
adamc@62	1782 sgnError env (DuplicateVal (loc, x))
adamc@62	1783 else
adamc@62	1784 ();
adamc@62	1785 (cons, SS.add (vals, x), sgns, strs))
adamc@62	1786 \| L'.SgiSgn (x, _, _) =>
adamc@62	1787 (if SS.member (sgns, x) then
adamc@62	1788 sgnError env (DuplicateSgn (loc, x))
adamc@62	1789 else
adamc@62	1790 ();
adamc@62	1791 (cons, vals, SS.add (sgns, x), strs))
adamc@62	1792 \| L'.SgiStr (x, _, _) =>
adamc@62	1793 (if SS.member (strs, x) then
adamc@62	1794 sgnError env (DuplicateStr (loc, x))
adamc@62	1795 else
adamc@62	1796 ();
adamc@88	1797 (cons, vals, sgns, SS.add (strs, x)))
adamc@88	1798 \| L'.SgiConstraint _ => (cons, vals, sgns, strs))
adamc@62	1799 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
adamc@31	1800 in
adamc@83	1801 ((L'.SgnConst sgis', loc), gs)
adamc@31	1802 end
adamc@31	1803 \| L.SgnVar x =>
adamc@31	1804 (case E.lookupSgn env x of
adamc@31	1805 NONE =>
adamc@31	1806 (sgnError env (UnboundSgn (loc, x));
adamc@83	1807 ((L'.SgnError, loc), []))
adamc@83	1808 \| SOME (n, sgis) => ((L'.SgnVar n, loc), []))
adamc@41	1809 \| L.SgnFun (m, dom, ran) =>
adamc@41	1810 let
adamc@83	1811 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41	1812 val (env', n) = E.pushStrNamed env m dom'
adamc@83	1813 val (ran', gs2) = elabSgn (env', denv) ran
adamc@41	1814 in
adamc@83	1815 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
adamc@41	1816 end
adamc@42	1817 \| L.SgnWhere (sgn, x, c) =>
adamc@42	1818 let
adamc@83	1819 val (sgn', ds1) = elabSgn (env, denv) sgn
adamc@83	1820 val (c', ck, ds2) = elabCon (env, denv) c
adamc@42	1821 in
adamc@42	1822 case #1 (hnormSgn env sgn') of
adamc@83	1823 L'.SgnError => (sgnerror, [])
adamc@42	1824 \| L'.SgnConst sgis =>
adamc@75	1825 if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
adamc@75	1826 x' = x andalso
adamc@75	1827 (unifyKinds k ck
adamc@75	1828 handle KUnify x => sgnError env (WhereWrongKind x);
adamc@42	1829 true)
adamc@42	1830 \| _ => false) sgis then
adamc@83	1831 ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2)
adamc@42	1832 else
adamc@42	1833 (sgnError env (UnWhereable (sgn', x));
adamc@83	1834 (sgnerror, []))
adamc@42	1835 \| _ => (sgnError env (UnWhereable (sgn', x));
adamc@83	1836 (sgnerror, []))
adamc@42	1837 end
adamc@59	1838 \| L.SgnProj (m, ms, x) =>
adamc@59	1839 (case E.lookupStr env m of
adamc@59	1840 NONE => (strError env (UnboundStr (loc, m));
adamc@83	1841 (sgnerror, []))
adamc@59	1842 \| SOME (n, sgn) =>
adamc@59	1843 let
adamc@59	1844 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@59	1845 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@59	1846 NONE => (strError env (UnboundStr (loc, m));
adamc@59	1847 (strerror, sgnerror))
adamc@59	1848 \| SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@59	1849 ((L'.StrVar n, loc), sgn) ms
adamc@59	1850 in
adamc@59	1851 case E.projectSgn env {sgn = sgn, str = str, field = x} of
adamc@59	1852 NONE => (sgnError env (UnboundSgn (loc, x));
adamc@83	1853 (sgnerror, []))
adamc@83	1854 \| SOME _ => ((L'.SgnProj (n, ms, x), loc), [])
adamc@59	1855 end)
adamc@59	1856
adamc@31	1857
adamc@66	1858 fun selfify env {str, strs, sgn} =
adamc@66	1859 case #1 (hnormSgn env sgn) of
adamc@66	1860 L'.SgnError => sgn
adamc@66	1861 \| L'.SgnVar _ => sgn
adamc@66	1862
adamc@66	1863 \| L'.SgnConst sgis =>
adamc@66	1864 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
adamc@66	1865 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
adamc@191	1866 \| (L'.SgiDatatype (x, n, xs, xncs), loc) =>
adamc@191	1867 (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
adamc@66	1868 \| (L'.SgiStr (x, n, sgn), loc) =>
adamc@66	1869 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
adamc@66	1870 \| x => x) sgis), #2 sgn)
adamc@66	1871 \| L'.SgnFun _ => sgn
adamc@66	1872 \| L'.SgnWhere _ => sgn
adamc@66	1873 \| L'.SgnProj (m, ms, x) =>
adamc@66	1874 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66	1875 (L'.StrVar m, #2 sgn) ms,
adamc@66	1876 sgn = #2 (E.lookupStrNamed env m),
adamc@66	1877 field = x} of
adamc@66	1878 NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
adamc@66	1879 \| SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
adamc@66	1880
adamc@66	1881 fun selfifyAt env {str, sgn} =
adamc@66	1882 let
adamc@66	1883 fun self (str, _) =
adamc@66	1884 case str of
adamc@66	1885 L'.StrVar x => SOME (x, [])
adamc@66	1886 \| L'.StrProj (str, x) =>
adamc@66	1887 (case self str of
adamc@66	1888 NONE => NONE
adamc@66	1889 \| SOME (m, ms) => SOME (m, ms @ [x]))
adamc@66	1890 \| _ => NONE
adamc@66	1891 in
adamc@66	1892 case self str of
adamc@66	1893 NONE => sgn
adamc@66	1894 \| SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
adamc@66	1895 end
adamc@66	1896
adamc@88	1897 fun dopen (env, denv) {str, strs, sgn} =
adamc@66	1898 let
adamc@66	1899 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
adamc@66	1900 (L'.StrVar str, #2 sgn) strs
adamc@66	1901 in
adamc@66	1902 case #1 (hnormSgn env sgn) of
adamc@66	1903 L'.SgnConst sgis =>
adamc@88	1904 ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) =>
adamc@162	1905 let
adamc@162	1906 val d =
adamc@162	1907 case sgi of
adamc@162	1908 L'.SgiConAbs (x, n, k) =>
adamc@162	1909 let
adamc@162	1910 val c = (L'.CModProj (str, strs, x), loc)
adamc@162	1911 in
adamc@162	1912 (L'.DCon (x, n, k, c), loc)
adamc@162	1913 end
adamc@162	1914 \| L'.SgiCon (x, n, k, c) =>
adamc@162	1915 (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
adamc@191	1916 \| L'.SgiDatatype (x, n, xs, xncs) =>
adamc@191	1917 (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
adamc@191	1918 \| L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@191	1919 (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)
adamc@162	1920 \| L'.SgiVal (x, n, t) =>
adamc@162	1921 (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)
adamc@162	1922 \| L'.SgiStr (x, n, sgn) =>
adamc@162	1923 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
adamc@162	1924 \| L'.SgiSgn (x, n, sgn) =>
adamc@162	1925 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
adamc@162	1926 \| L'.SgiConstraint (c1, c2) =>
adamc@162	1927 (L'.DConstraint (c1, c2), loc)
adamc@162	1928 in
adamc@162	1929 (d, (E.declBinds env' d, denv'))
adamc@162	1930 end)
adamc@88	1931 (env, denv) sgis
adamc@66	1932 \| _ => (strError env (UnOpenable sgn);
adamc@88	1933 ([], (env, denv)))
adamc@66	1934 end
adamc@66	1935
adamc@88	1936 fun dopenConstraints (loc, env, denv) {str, strs} =
adamc@88	1937 case E.lookupStr env str of
adamc@88	1938 NONE => (strError env (UnboundStr (loc, str));
adamc@88	1939 denv)
adamc@88	1940 \| SOME (n, sgn) =>
adamc@88	1941 let
adamc@88	1942 val (st, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@88	1943 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@88	1944 NONE => (strError env (UnboundStr (loc, m));
adamc@88	1945 (strerror, sgnerror))
adamc@88	1946 \| SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@88	1947 ((L'.StrVar n, loc), sgn) strs
adamc@88	1948
adamc@88	1949 val cso = E.projectConstraints env {sgn = sgn, str = st}
adamc@88	1950
adamc@88	1951 val denv = case cso of
adamc@88	1952 NONE => (strError env (UnboundStr (loc, str));
adamc@88	1953 denv)
adamc@90	1954 \| SOME cs => foldl (fn ((c1, c2), denv) =>
adamc@90	1955 let
adamc@90	1956 val (denv, gs) = D.assert env denv (c1, c2)
adamc@90	1957 in
adamc@90	1958 case gs of
adamc@90	1959 [] => ()
adamc@90	1960 \| _ => raise Fail "dopenConstraints: Sub-constraints remain";
adamc@90	1961
adamc@90	1962 denv
adamc@90	1963 end) denv cs
adamc@88	1964 in
adamc@88	1965 denv
adamc@88	1966 end
adamc@88	1967
adamc@31	1968 fun sgiOfDecl (d, loc) =
adamc@31	1969 case d of
adamc@123	1970 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
adamc@156	1971 \| L'.DDatatype x => [(L'.SgiDatatype x, loc)]
adamc@156	1972 \| L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)]
adamc@123	1973 \| L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)]
adamc@123	1974 \| L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis
adamc@123	1975 \| L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)]
adamc@123	1976 \| L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)]
adamc@123	1977 \| L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
adamc@123	1978 \| L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
adamc@123	1979 \| L'.DExport _ => []
adamc@88	1980
adamc@88	1981 fun sgiBindsD (env, denv) (sgi, _) =
adamc@88	1982 case sgi of
adamc@90	1983 L'.SgiConstraint (c1, c2) =>
adamc@90	1984 (case D.assert env denv (c1, c2) of
adamc@90	1985 (denv, []) => denv
adamc@90	1986 \| _ => raise Fail "sgiBindsD: Sub-constraints remain")
adamc@88	1987 \| _ => denv
adamc@31	1988
adamc@86	1989 fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
adamc@35	1990 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
adamc@31	1991 (L'.SgnError, _) => ()
adamc@31	1992 \| (_, L'.SgnError) => ()
adamc@31	1993
adamc@31	1994 \| (L'.SgnConst sgis1, L'.SgnConst sgis2) =>
adamc@31	1995 let
adamc@156	1996 fun folder (sgi2All as (sgi, loc), (env, denv)) =
adamc@31	1997 let
adamc@31	1998 fun seek p =
adamc@31	1999 let
adamc@88	2000 fun seek (env, denv) ls =
adamc@31	2001 case ls of
adamc@31	2002 [] => (sgnError env (UnmatchedSgi sgi2All);
adamc@88	2003 (env, denv))
adamc@31	2004 \| h :: t =>
adamc@31	2005 case p h of
adamc@88	2006 NONE => seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t
adamc@88	2007 \| SOME envs => envs
adamc@31	2008 in
adamc@88	2009 seek (env, denv) sgis1
adamc@31	2010 end
adamc@31	2011 in
adamc@31	2012 case sgi of
adamc@31	2013 L'.SgiConAbs (x, n2, k2) =>
adamc@31	2014 seek (fn sgi1All as (sgi1, _) =>
adamc@31	2015 let
adamc@41	2016 fun found (x', n1, k1, co1) =
adamc@41	2017 if x = x' then
adamc@41	2018 let
adamc@41	2019 val () = unifyKinds k1 k2
adamc@41	2020 handle KUnify (k1, k2, err) =>
adamc@41	2021 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
adamc@41	2022 val env = E.pushCNamedAs env x n1 k1 co1
adamc@41	2023 in
adamc@41	2024 SOME (if n1 = n2 then
adamc@41	2025 env
adamc@41	2026 else
adamc@88	2027 E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)),
adamc@88	2028 denv)
adamc@41	2029 end
adamc@41	2030 else
adamc@41	2031 NONE
adamc@31	2032 in
adamc@31	2033 case sgi1 of
adamc@41	2034 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE)
adamc@41	2035 \| L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1)
adamc@191	2036 \| L'.SgiDatatype (x', n1, xs, _) =>
adamc@191	2037 let
adamc@191	2038 val k = (L'.KType, loc)
adamc@191	2039 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191	2040 in
adamc@191	2041 found (x', n1, k', NONE)
adamc@191	2042 end
adamc@191	2043 \| L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) =>
adamc@191	2044 let
adamc@191	2045 val k = (L'.KType, loc)
adamc@191	2046 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191	2047 in
adamc@191	2048 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
adamc@191	2049 end
adamc@31	2050 \| _ => NONE
adamc@31	2051 end)
adamc@31	2052
adamc@31	2053 \| L'.SgiCon (x, n2, k2, c2) =>
adamc@31	2054 seek (fn sgi1All as (sgi1, _) =>
adamc@31	2055 case sgi1 of
adamc@41	2056 L'.SgiCon (x', n1, k1, c1) =>
adamc@41	2057 if x = x' then
adamc@41	2058 let
adamc@88	2059 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv)
adamc@41	2060 in
adamc@86	2061 (case unifyCons (env, denv) c1 c2 of
adamc@86	2062 [] => good ()
adamc@86	2063 \| _ => NONE)
adamc@86	2064 handle CUnify (c1, c2, err) =>
adamc@86	2065 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@86	2066 good ())
adamc@41	2067 end
adamc@41	2068 else
adamc@41	2069 NONE
adamc@31	2070 \| _ => NONE)
adamc@31	2071
adamc@191	2072 \| L'.SgiDatatype (x, n2, xs2, xncs2) =>
adamc@156	2073 seek (fn sgi1All as (sgi1, _) =>
adamc@160	2074 let
adamc@191	2075 fun found (n1, xs1, xncs1) =
adamc@160	2076 let
adamc@160	2077 fun mismatched ue =
adamc@160	2078 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue));
adamc@160	2079 SOME (env, denv))
adamc@156	2080
adamc@191	2081 val k = (L'.KType, loc)
adamc@191	2082 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1
adamc@191	2083
adamc@160	2084 fun good () =
adamc@160	2085 let
adamc@160	2086 val env = E.sgiBinds env sgi2All
adamc@160	2087 val env = if n1 = n2 then
adamc@160	2088 env
adamc@160	2089 else
adamc@160	2090 E.pushCNamedAs env x n1 (L'.KType, loc)
adamc@160	2091 (SOME (L'.CNamed n1, loc))
adamc@160	2092 in
adamc@160	2093 SOME (env, denv)
adamc@160	2094 end
adamc@156	2095
adamc@191	2096 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1
adamc@160	2097 fun xncBad ((x1, _, t1), (x2, _, t2)) =
adamc@160	2098 String.compare (x1, x2) <> EQUAL
adamc@160	2099 orelse case (t1, t2) of
adamc@160	2100 (NONE, NONE) => false
adamc@160	2101 \| (SOME t1, SOME t2) =>
adamc@160	2102 not (List.null (unifyCons (env, denv) t1 t2))
adamc@160	2103 \| _ => true
adamc@160	2104 in
adamc@191	2105 (if xs1 <> xs2
adamc@191	2106 orelse length xncs1 <> length xncs2
adamc@160	2107 orelse ListPair.exists xncBad (xncs1, xncs2) then
adamc@160	2108 mismatched NONE
adamc@160	2109 else
adamc@160	2110 good ())
adamc@160	2111 handle CUnify ue => mismatched (SOME ue)
adamc@160	2112 end
adamc@160	2113 in
adamc@160	2114 case sgi1 of
adamc@191	2115 L'.SgiDatatype (x', n1, xs, xncs1) =>
adamc@160	2116 if x' = x then
adamc@191	2117 found (n1, xs, xncs1)
adamc@160	2118 else
adamc@160	2119 NONE
adamc@191	2120 \| L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) =>
adamc@162	2121 if x' = x then
adamc@191	2122 found (n1, xs, xncs1)
adamc@162	2123 else
adamc@162	2124 NONE
adamc@160	2125 \| _ => NONE
adamc@160	2126 end)
adamc@156	2127
adamc@191	2128 \| L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) =>
adamc@158	2129 seek (fn sgi1All as (sgi1, _) =>
adamc@158	2130 case sgi1 of
adamc@191	2131 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) =>
adamc@158	2132 if x = x' then
adamc@158	2133 let
adamc@158	2134 val k = (L'.KType, loc)
adamc@191	2135 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@158	2136 val t1 = (L'.CModProj (m11, ms1, s1), loc)
adamc@158	2137 val t2 = (L'.CModProj (m12, ms2, s2), loc)
adamc@158	2138
adamc@158	2139 fun good () =
adamc@158	2140 let
adamc@191	2141 val env = E.pushCNamedAs env x n1 k' (SOME t1)
adamc@191	2142 val env = E.pushCNamedAs env x n2 k' (SOME t2)
adamc@158	2143 in
adamc@158	2144 SOME (env, denv)
adamc@158	2145 end
adamc@158	2146 in
adamc@158	2147 (case unifyCons (env, denv) t1 t2 of
adamc@158	2148 [] => good ()
adamc@158	2149 \| _ => NONE)
adamc@158	2150 handle CUnify (c1, c2, err) =>
adamc@158	2151 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@158	2152 good ())
adamc@158	2153 end
adamc@158	2154 else
adamc@158	2155 NONE
adamc@158	2156
adamc@158	2157 \| _ => NONE)
adamc@156	2158
adamc@32	2159 \| L'.SgiVal (x, n2, c2) =>
adamc@32	2160 seek (fn sgi1All as (sgi1, _) =>
adamc@32	2161 case sgi1 of
adamc@41	2162 L'.SgiVal (x', n1, c1) =>
adamc@41	2163 if x = x' then
adamc@86	2164 (case unifyCons (env, denv) c1 c2 of
adamc@88	2165 [] => SOME (env, denv)
adamc@86	2166 \| _ => NONE)
adamc@86	2167 handle CUnify (c1, c2, err) =>
adamc@86	2168 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
adamc@88	2169 SOME (env, denv))
adamc@41	2170 else
adamc@41	2171 NONE
adamc@32	2172 \| _ => NONE)
adamc@32	2173
adamc@33	2174 \| L'.SgiStr (x, n2, sgn2) =>
adamc@33	2175 seek (fn sgi1All as (sgi1, _) =>
adamc@33	2176 case sgi1 of
adamc@41	2177 L'.SgiStr (x', n1, sgn1) =>
adamc@41	2178 if x = x' then
adamc@66	2179 let
adamc@86	2180 val () = subSgn (env, denv) sgn1 sgn2
adamc@66	2181 val env = E.pushStrNamedAs env x n1 sgn1
adamc@66	2182 val env = if n1 = n2 then
adamc@66	2183 env
adamc@66	2184 else
adamc@66	2185 E.pushStrNamedAs env x n2
adamc@66	2186 (selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
adamc@66	2187 sgn = sgn2})
adamc@66	2188 in
adamc@88	2189 SOME (env, denv)
adamc@66	2190 end
adamc@41	2191 else
adamc@41	2192 NONE
adamc@33	2193 \| _ => NONE)
adamc@59	2194
adamc@59	2195 \| L'.SgiSgn (x, n2, sgn2) =>
adamc@59	2196 seek (fn sgi1All as (sgi1, _) =>
adamc@59	2197 case sgi1 of
adamc@59	2198 L'.SgiSgn (x', n1, sgn1) =>
adamc@59	2199 if x = x' then
adamc@65	2200 let
adamc@86	2201 val () = subSgn (env, denv) sgn1 sgn2
adamc@86	2202 val () = subSgn (env, denv) sgn2 sgn1
adamc@65	2203
adamc@65	2204 val env = E.pushSgnNamedAs env x n2 sgn2
adamc@65	2205 val env = if n1 = n2 then
adamc@65	2206 env
adamc@65	2207 else
adamc@65	2208 E.pushSgnNamedAs env x n1 sgn2
adamc@65	2209 in
adamc@88	2210 SOME (env, denv)
adamc@65	2211 end
adamc@59	2212 else
adamc@59	2213 NONE
adamc@59	2214 \| _ => NONE)
adamc@88	2215
adamc@88	2216 \| L'.SgiConstraint (c2, d2) =>
adamc@88	2217 seek (fn sgi1All as (sgi1, _) =>
adamc@88	2218 case sgi1 of
adamc@88	2219 L'.SgiConstraint (c1, d1) =>
adamc@88	2220 if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then
adamc@90	2221 let
adamc@90	2222 val (denv, gs) = D.assert env denv (c2, d2)
adamc@90	2223 in
adamc@90	2224 case gs of
adamc@90	2225 [] => ()
adamc@90	2226 \| _ => raise Fail "subSgn: Sub-constraints remain";
adamc@90	2227
adamc@90	2228 SOME (env, denv)
adamc@90	2229 end
adamc@88	2230 else
adamc@88	2231 NONE
adamc@88	2232 \| _ => NONE)
adamc@31	2233 end
adamc@31	2234 in
adamc@88	2235 ignore (foldl folder (env, denv) sgis2)
adamc@31	2236 end
adamc@31	2237
adamc@41	2238 \| (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) =>
adamc@43	2239 let
adamc@43	2240 val ran1 =
adamc@43	2241 if n1 = n2 then
adamc@43	2242 ran1
adamc@43	2243 else
adamc@43	2244 subStrInSgn (n1, n2) ran1
adamc@43	2245 in
adamc@86	2246 subSgn (env, denv) dom2 dom1;
adamc@86	2247 subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2
adamc@43	2248 end
adamc@41	2249
adamc@41	2250 \| _ => sgnError env (SgnWrongForm (sgn1, sgn2))
adamc@41	2251
adamc@61	2252
adamc@88	2253 fun elabDecl ((d, loc), (env, denv, gs)) =
adamc@76	2254 case d of
adamc@76	2255 L.DCon (x, ko, c) =>
adamc@76	2256 let
adamc@76	2257 val k' = case ko of
adamc@76	2258 NONE => kunif loc
adamc@76	2259 \| SOME k => elabKind k
adamc@76	2260
adamc@83	2261 val (c', ck, gs') = elabCon (env, denv) c
adamc@76	2262 val (env', n) = E.pushCNamed env x k' (SOME c')
adamc@76	2263 in
adamc@76	2264 checkKind env c' ck k';
adamc@76	2265
adamc@88	2266 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
adamc@76	2267 end
adamc@191	2268 \| L.DDatatype (x, xs, xcs) =>
adamc@156	2269 let
adamc@156	2270 val k = (L'.KType, loc)
adamc@191	2271 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@191	2272 val (env, n) = E.pushCNamed env x k' NONE
adamc@156	2273 val t = (L'.CNamed n, loc)
adamc@194	2274 val nxs = length xs - 1
adamc@194	2275 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs
adamc@191	2276
adamc@191	2277 val (env', denv') = foldl (fn (x, (env', denv')) =>
adamc@191	2278 (E.pushCRel env' x k,
adamc@191	2279 D.enter denv')) (env, denv) xs
adamc@156	2280
adamc@156	2281 val (xcs, (used, env, gs)) =
adamc@156	2282 ListUtil.foldlMap
adamc@156	2283 (fn ((x, to), (used, env, gs)) =>
adamc@156	2284 let
adamc@156	2285 val (to, t, gs') = case to of
adamc@156	2286 NONE => (NONE, t, gs)
adamc@156	2287 \| SOME t' =>
adamc@156	2288 let
adamc@191	2289 val (t', tk, gs') = elabCon (env', denv') t'
adamc@156	2290 in
adamc@191	2291 checkKind env' t' tk k;
adamc@156	2292 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
adamc@156	2293 end
adamc@191	2294 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs
adamc@156	2295
adamc@156	2296 val (env, n') = E.pushENamed env x t
adamc@156	2297 in
adamc@156	2298 if SS.member (used, x) then
adamc@156	2299 strError env (DuplicateConstructor (x, loc))
adamc@156	2300 else
adamc@156	2301 ();
adamc@156	2302 ((x, n', to), (SS.add (used, x), env, gs'))
adamc@156	2303 end)
adamc@156	2304 (SS.empty, env, []) xcs
adamc@171	2305
adamc@191	2306 val env = E.pushDatatype env n xs xcs
adamc@156	2307 in
adamc@191	2308 ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs))
adamc@156	2309 end
adamc@156	2310
adamc@157	2311 \| L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
adamc@157	2312
adamc@157	2313 \| L.DDatatypeImp (x, m1 :: ms, s) =>
adamc@157	2314 (case E.lookupStr env m1 of
adamc@157	2315 NONE => (expError env (UnboundStrInExp (loc, m1));
adamc@157	2316 ([], (env, denv, gs)))
adamc@157	2317 \| SOME (n, sgn) =>
adamc@157	2318 let
adamc@157	2319 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@157	2320 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@157	2321 NONE => (conError env (UnboundStrInCon (loc, m));
adamc@157	2322 (strerror, sgnerror))
adamc@157	2323 \| SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@157	2324 ((L'.StrVar n, loc), sgn) ms
adamc@157	2325 in
adamc@158	2326 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
adamc@158	2327 ((L'.CModProj (n, ms, s), _), gs) =>
adamc@158	2328 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
adamc@158	2329 NONE => (conError env (UnboundDatatype (loc, s));
adamc@158	2330 ([], (env, denv, gs)))
adamc@191	2331 \| SOME (xs, xncs) =>
adamc@158	2332 let
adamc@158	2333 val k = (L'.KType, loc)
adamc@191	2334 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
adamc@158	2335 val t = (L'.CModProj (n, ms, s), loc)
adamc@191	2336 val (env, n') = E.pushCNamed env x k' (SOME t)
adamc@191	2337 val env = E.pushDatatype env n' xs xncs
adamc@157	2338
adamc@158	2339 val t = (L'.CNamed n', loc)
adamc@158	2340 val env = foldl (fn ((x, n, to), env) =>
adamc@158	2341 let
adamc@158	2342 val t = case to of
adamc@158	2343 NONE => t
adamc@158	2344 \| SOME t' => (L'.TFun (t', t), loc)
adamc@191	2345
adamc@191	2346 val t = foldr (fn (x, t) =>
adamc@191	2347 (L'.TCFun (L'.Implicit, x, k, t), loc))
adamc@191	2348 t xs
adamc@158	2349 in
adamc@158	2350 E.pushENamedAs env x n t
adamc@158	2351 end) env xncs
adamc@158	2352 in
adamc@191	2353 ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs))
adamc@158	2354 end)
adamc@158	2355 \| _ => (strError env (NotDatatype loc);
adamc@158	2356 ([], (env, denv, [])))
adamc@157	2357 end)
adamc@157	2358
adamc@76	2359 \| L.DVal (x, co, e) =>
adamc@76	2360 let
adamc@123	2361 val (c', _, gs1) = case co of
adamc@83	2362 NONE => (cunif (loc, ktype), ktype, [])
adamc@83	2363 \| SOME c => elabCon (env, denv) c
adamc@76	2364
adamc@83	2365 val (e', et, gs2) = elabExp (env, denv) e
adamc@76	2366 val (env', n) = E.pushENamed env x c'
adamc@86	2367
adamc@86	2368 val gs3 = checkCon (env, denv) e' et c'
adamc@76	2369 in
adamc@88	2370 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs))
adamc@76	2371 end
adamc@123	2372 \| L.DValRec vis =>
adamc@123	2373 let
adamc@123	2374 val (vis, gs) = ListUtil.foldlMap
adamc@123	2375 (fn ((x, co, e), gs) =>
adamc@123	2376 let
adamc@123	2377 val (c', _, gs1) = case co of
adamc@123	2378 NONE => (cunif (loc, ktype), ktype, [])
adamc@123	2379 \| SOME c => elabCon (env, denv) c
adamc@123	2380 in
adamc@123	2381 ((x, c', e), gs1 @ gs)
adamc@123	2382 end) [] vis
adamc@123	2383
adamc@123	2384 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
adamc@123	2385 let
adamc@123	2386 val (env, n) = E.pushENamed env x c'
adamc@123	2387 in
adamc@123	2388 ((x, n, c', e), env)
adamc@123	2389 end) env vis
adamc@123	2390
adamc@123	2391 val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
adamc@123	2392 let
adamc@123	2393 val (e', et, gs1) = elabExp (env, denv) e
adamc@123	2394
adamc@123	2395 val gs2 = checkCon (env, denv) e' et c'
adamc@123	2396 in
adamc@123	2397 ((x, n, c', e'), gs1 @ gs2 @ gs)
adamc@123	2398 end) gs vis
adamc@123	2399 in
adamc@123	2400 ([(L'.DValRec vis, loc)], (env, denv, gs))
adamc@123	2401 end
adamc@76	2402
adamc@76	2403 \| L.DSgn (x, sgn) =>
adamc@76	2404 let
adamc@83	2405 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76	2406 val (env', n) = E.pushSgnNamed env x sgn'
adamc@76	2407 in
adamc@88	2408 ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76	2409 end
adamc@76	2410
adamc@76	2411 \| L.DStr (x, sgno, str) =>
adamc@76	2412 let
adamc@93	2413 val () = if x = "Basis" then
adamc@93	2414 raise Fail "Not allowed to redefine structure 'Basis'"
adamc@93	2415 else
adamc@93	2416 ()
adamc@93	2417
adamc@83	2418 val formal = Option.map (elabSgn (env, denv)) sgno
adamc@76	2419
adamc@83	2420 val (str', sgn', gs') =
adamc@78	2421 case formal of
adamc@78	2422 NONE =>
adamc@78	2423 let
adamc@83	2424 val (str', actual, ds) = elabStr (env, denv) str
adamc@78	2425 in
adamc@83	2426 (str', selfifyAt env {str = str', sgn = actual}, ds)
adamc@78	2427 end
adamc@83	2428 \| SOME (formal, gs1) =>
adamc@78	2429 let
adamc@78	2430 val str =
adamc@78	2431 case #1 (hnormSgn env formal) of
adamc@78	2432 L'.SgnConst sgis =>
adamc@78	2433 (case #1 str of
adamc@78	2434 L.StrConst ds =>
adamc@78	2435 let
adamc@78	2436 val needed = foldl (fn ((sgi, _), needed) =>
adamc@78	2437 case sgi of
adamc@78	2438 L'.SgiConAbs (x, _, _) => SS.add (needed, x)
adamc@78	2439 \| _ => needed)
adamc@78	2440 SS.empty sgis
adamc@78	2441
adamc@78	2442 val needed = foldl (fn ((d, _), needed) =>
adamc@78	2443 case d of
adamc@78	2444 L.DCon (x, _, _) => (SS.delete (needed, x)
adamc@78	2445 handle NotFound => needed)
adamc@78	2446 \| L.DOpen _ => SS.empty
adamc@78	2447 \| _ => needed)
adamc@78	2448 needed ds
adamc@78	2449 in
adamc@78	2450 case SS.listItems needed of
adamc@78	2451 [] => str
adamc@78	2452 \| xs =>
adamc@78	2453 let
adamc@78	2454 val kwild = (L.KWild, #2 str)
adamc@78	2455 val cwild = (L.CWild kwild, #2 str)
adamc@78	2456 val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs
adamc@78	2457 in
adamc@78	2458 (L.StrConst (ds @ ds'), #2 str)
adamc@78	2459 end
adamc@78	2460 end
adamc@78	2461 \| _ => str)
adamc@78	2462 \| _ => str
adamc@78	2463
adamc@83	2464 val (str', actual, gs2) = elabStr (env, denv) str
adamc@78	2465 in
adamc@158	2466 subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
adamc@83	2467 (str', formal, gs1 @ gs2)
adamc@78	2468 end
adamc@76	2469
adamc@76	2470 val (env', n) = E.pushStrNamed env x sgn'
adamc@76	2471 in
adamc@76	2472 case #1 (hnormSgn env sgn') of
adamc@76	2473 L'.SgnFun _ =>
adamc@76	2474 (case #1 str' of
adamc@76	2475 L'.StrFun _ => ()
adamc@76	2476 \| _ => strError env (FunctorRebind loc))
adamc@76	2477 \| _ => ();
adamc@76	2478
adamc@88	2479 ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs))
adamc@76	2480 end
adamc@76	2481
adamc@76	2482 \| L.DFfiStr (x, sgn) =>
adamc@76	2483 let
adamc@83	2484 val (sgn', gs') = elabSgn (env, denv) sgn
adamc@76	2485
adamc@76	2486 val (env', n) = E.pushStrNamed env x sgn'
adamc@76	2487 in
adamc@88	2488 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs))
adamc@76	2489 end
adamc@76	2490
adamc@76	2491 \| L.DOpen (m, ms) =>
adamc@88	2492 (case E.lookupStr env m of
adamc@88	2493 NONE => (strError env (UnboundStr (loc, m));
adamc@88	2494 ([], (env, denv, [])))
adamc@88	2495 \| SOME (n, sgn) =>
adamc@88	2496 let
adamc@88	2497 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@88	2498 case E.projectStr env {str = str, sgn = sgn, field = m} of
adamc@88	2499 NONE => (strError env (UnboundStr (loc, m));
adamc@88	2500 (strerror, sgnerror))
adamc@88	2501 \| SOME sgn => ((L'.StrProj (str, m), loc), sgn))
adamc@88	2502 ((L'.StrVar n, loc), sgn) ms
adamc@83	2503
adamc@88	2504 val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn}
adamc@88	2505 val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
adamc@88	2506 in
adamc@88	2507 (ds, (env', denv', []))
adamc@88	2508 end)
adamc@88	2509
adamc@88	2510 \| L.DConstraint (c1, c2) =>
adamc@88	2511 let
adamc@88	2512 val (c1', k1, gs1) = elabCon (env, denv) c1
adamc@88	2513 val (c2', k2, gs2) = elabCon (env, denv) c2
adamc@90	2514 val gs3 = D.prove env denv (c1', c2', loc)
adamc@88	2515
adamc@90	2516 val (denv', gs4) = D.assert env denv (c1', c2')
adamc@88	2517 in
adamc@88	2518 checkKind env c1' k1 (L'.KRecord (kunif loc), loc);
adamc@88	2519 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
adamc@88	2520
adamc@90	2521 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', gs1 @ gs2 @ gs3 @ gs4))
adamc@88	2522 end
adamc@88	2523
adamc@88	2524 \| L.DOpenConstraints (m, ms) =>
adamc@88	2525 let
adamc@88	2526 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
adamc@88	2527 in
adamc@88	2528 ([], (env, denv, []))
adamc@88	2529 end
adamc@3	2530
adamc@109	2531 \| L.DExport str =>
adamc@100	2532 let
adamc@109	2533 val (str', sgn, gs) = elabStr (env, denv) str
adamc@100	2534
adamc@109	2535 val sgn =
adamc@109	2536 case #1 (hnormSgn env sgn) of
adamc@109	2537 L'.SgnConst sgis =>
adamc@109	2538 let
adamc@146	2539 fun doOne (all as (sgi, _), env) =
adamc@146	2540 (case sgi of
adamc@146	2541 L'.SgiVal (x, n, t) =>
adamc@146	2542 (case hnormCon (env, denv) t of
adamc@146	2543 ((L'.TFun (dom, ran), _), []) =>
adamc@146	2544 (case (hnormCon (env, denv) dom, hnormCon (env, denv) ran) of
adamc@146	2545 (((L'.TRecord domR, _), []),
adamc@146	2546 ((L'.CApp (tf, arg3), _), [])) =>
adamc@146	2547 (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of
adamc@146	2548 (((L'.CApp (tf, arg2), _), []),
adamc@146	2549 (((L'.CRecord (_, []), _), []))) =>
adamc@146	2550 (case (hnormCon (env, denv) tf) of
adamc@146	2551 ((L'.CApp (tf, arg1), _), []) =>
adamc@146	2552 (case (hnormCon (env, denv) tf,
adamc@146	2553 hnormCon (env, denv) domR,
adamc@152	2554 hnormCon (env, denv) arg1,
adamc@146	2555 hnormCon (env, denv) arg2) of
adamc@152	2556 ((tf, []), (domR, []), (arg1, []),
adamc@146	2557 ((L'.CRecord (_, []), _), [])) =>
adamc@146	2558 let
adamc@146	2559 val t = (L'.CApp (tf, arg1), loc)
adamc@146	2560 val t = (L'.CApp (t, arg2), loc)
adamc@146	2561 val t = (L'.CApp (t, arg3), loc)
adamc@146	2562 in
adamc@146	2563 (L'.SgiVal (x, n, (L'.TFun ((L'.TRecord domR, loc),
adamc@146	2564 t),
adamc@146	2565 loc)), loc)
adamc@146	2566 end
adamc@146	2567 \| _ => all)
adamc@146	2568 \| _ => all)
adamc@146	2569 \| _ => all)
adamc@146	2570 \| _ => all)
adamc@146	2571 \| _ => all)
adamc@146	2572 \| _ => all,
adamc@146	2573 E.sgiBinds env all)
adamc@109	2574 in
adamc@146	2575 (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc)
adamc@109	2576 end
adamc@109	2577 \| _ => sgn
adamc@100	2578 in
adamc@109	2579 ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs))
adamc@100	2580 end
adamc@100	2581
adamc@83	2582 and elabStr (env, denv) (str, loc) =
adamc@31	2583 case str of
adamc@31	2584 L.StrConst ds =>
adamc@31	2585 let
adamc@88	2586 val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds
adamc@123	2587 val sgis = ListUtil.mapConcat sgiOfDecl ds'
adamc@63	2588
adamc@63	2589 val (sgis, _, _, _, _) =
adamc@64	2590 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
adamc@63	2591 case sgi of
adamc@64	2592 L'.SgiConAbs (x, n, k) =>
adamc@64	2593 let
adamc@64	2594 val (cons, x) =
adamc@64	2595 if SS.member (cons, x) then
adamc@64	2596 (cons, "?" ^ x)
adamc@64	2597 else
adamc@64	2598 (SS.add (cons, x), x)
adamc@64	2599 in
adamc@64	2600 ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
adamc@64	2601 end
adamc@64	2602 \| L'.SgiCon (x, n, k, c) =>
adamc@64	2603 let
adamc@64	2604 val (cons, x) =
adamc@64	2605 if SS.member (cons, x) then
adamc@64	2606 (cons, "?" ^ x)
adamc@64	2607 else
adamc@64	2608 (SS.add (cons, x), x)
adamc@64	2609 in
adamc@64	2610 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64	2611 end
adamc@191	2612 \| L'.SgiDatatype (x, n, xs, xncs) =>
adamc@156	2613 let
adamc@156	2614 val (cons, x) =
adamc@156	2615 if SS.member (cons, x) then
adamc@156	2616 (cons, "?" ^ x)
adamc@156	2617 else
adamc@156	2618 (SS.add (cons, x), x)
adamc@156	2619
adamc@156	2620 val (xncs, vals) =
adamc@156	2621 ListUtil.foldlMap
adamc@156	2622 (fn ((x, n, t), vals) =>
adamc@156	2623 if SS.member (vals, x) then
adamc@156	2624 (("?" ^ x, n, t), vals)
adamc@156	2625 else
adamc@156	2626 ((x, n, t), SS.add (vals, x)))
adamc@156	2627 vals xncs
adamc@156	2628 in
adamc@191	2629 ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
adamc@156	2630 end
adamc@191	2631 \| L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
adamc@156	2632 let
adamc@156	2633 val (cons, x) =
adamc@156	2634 if SS.member (cons, x) then
adamc@156	2635 (cons, "?" ^ x)
adamc@156	2636 else
adamc@156	2637 (SS.add (cons, x), x)
adamc@156	2638 in
adamc@191	2639 ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs)
adamc@156	2640 end
adamc@64	2641 \| L'.SgiVal (x, n, c) =>
adamc@64	2642 let
adamc@64	2643 val (vals, x) =
adamc@64	2644 if SS.member (vals, x) then
adamc@64	2645 (vals, "?" ^ x)
adamc@64	2646 else
adamc@64	2647 (SS.add (vals, x), x)
adamc@64	2648 in
adamc@64	2649 ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
adamc@64	2650 end
adamc@64	2651 \| L'.SgiSgn (x, n, sgn) =>
adamc@64	2652 let
adamc@64	2653 val (sgns, x) =
adamc@64	2654 if SS.member (sgns, x) then
adamc@64	2655 (sgns, "?" ^ x)
adamc@64	2656 else
adamc@64	2657 (SS.add (sgns, x), x)
adamc@64	2658 in
adamc@64	2659 ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@64	2660 end
adamc@64	2661
adamc@64	2662 \| L'.SgiStr (x, n, sgn) =>
adamc@64	2663 let
adamc@64	2664 val (strs, x) =
adamc@64	2665 if SS.member (strs, x) then
adamc@64	2666 (strs, "?" ^ x)
adamc@64	2667 else
adamc@64	2668 (SS.add (strs, x), x)
adamc@64	2669 in
adamc@64	2670 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
adamc@88	2671 end
adamc@88	2672 \| L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs))
adamc@64	2673
adamc@63	2674 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
adamc@31	2675 in
adamc@83	2676 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)
adamc@31	2677 end
adamc@31	2678 \| L.StrVar x =>
adamc@31	2679 (case E.lookupStr env x of
adamc@31	2680 NONE =>
adamc@31	2681 (strError env (UnboundStr (loc, x));
adamc@83	2682 (strerror, sgnerror, []))
adamc@83	2683 \| SOME (n, sgn) => ((L'.StrVar n, loc), sgn, []))
adamc@34	2684 \| L.StrProj (str, x) =>
adamc@34	2685 let
adamc@83	2686 val (str', sgn, gs) = elabStr (env, denv) str
adamc@34	2687 in
adamc@34	2688 case E.projectStr env {str = str', sgn = sgn, field = x} of
adamc@34	2689 NONE => (strError env (UnboundStr (loc, x));
adamc@83	2690 (strerror, sgnerror, []))
adamc@83	2691 \| SOME sgn => ((L'.StrProj (str', x), loc), sgn, gs)
adamc@34	2692 end
adamc@41	2693 \| L.StrFun (m, dom, ranO, str) =>
adamc@41	2694 let
adamc@83	2695 val (dom', gs1) = elabSgn (env, denv) dom
adamc@41	2696 val (env', n) = E.pushStrNamed env m dom'
adamc@83	2697 val (str', actual, gs2) = elabStr (env', denv) str
adamc@41	2698
adamc@83	2699 val (formal, gs3) =
adamc@41	2700 case ranO of
adamc@83	2701 NONE => (actual, [])
adamc@41	2702 \| SOME ran =>
adamc@41	2703 let
adamc@83	2704 val (ran', gs) = elabSgn (env', denv) ran
adamc@41	2705 in
adamc@86	2706 subSgn (env', denv) actual ran';
adamc@83	2707 (ran', gs)
adamc@41	2708 end
adamc@41	2709 in
adamc@41	2710 ((L'.StrFun (m, n, dom', formal, str'), loc),
adamc@83	2711 (L'.SgnFun (m, n, dom', formal), loc),
adamc@83	2712 gs1 @ gs2 @ gs3)
adamc@41	2713 end
adamc@44	2714 \| L.StrApp (str1, str2) =>
adamc@44	2715 let
adamc@83	2716 val (str1', sgn1, gs1) = elabStr (env, denv) str1
adamc@83	2717 val (str2', sgn2, gs2) = elabStr (env, denv) str2
adamc@44	2718 in
adamc@44	2719 case #1 (hnormSgn env sgn1) of
adamc@83	2720 L'.SgnError => (strerror, sgnerror, [])
adamc@44	2721 \| L'.SgnFun (m, n, dom, ran) =>
adamc@86	2722 (subSgn (env, denv) sgn2 dom;
adamc@44	2723 case #1 (hnormSgn env ran) of
adamc@83	2724 L'.SgnError => (strerror, sgnerror, [])
adamc@44	2725 \| L'.SgnConst sgis =>
adamc@44	2726 ((L'.StrApp (str1', str2'), loc),
adamc@83	2727 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
adamc@83	2728 gs1 @ gs2)
adamc@44	2729 \| _ => raise Fail "Unable to hnormSgn in functor application")
adamc@44	2730 \| _ => (strError env (NotFunctor sgn1);
adamc@83	2731 (strerror, sgnerror, []))
adamc@44	2732 end
adamc@31	2733
adamc@56	2734 fun elabFile basis env file =
adamc@56	2735 let
adamc@83	2736 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
adamc@83	2737 val () = case gs of
adamc@83	2738 [] => ()
adamc@83	2739 \| _ => raise Fail "Unresolved disjointness constraints in Basis"
adamc@83	2740
adamc@56	2741 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
adamc@56	2742
adamc@88	2743 val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn}
adamc@56	2744
adamc@56	2745 fun discoverC r x =
adamc@56	2746 case E.lookupC env' x of
adamc@56	2747 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
adamc@56	2748 \| E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
adamc@56	2749 \| E.Named (n, (_, loc)) => r := (L'.CNamed n, loc)
adamc@56	2750
adamc@56	2751 val () = discoverC int "int"
adamc@56	2752 val () = discoverC float "float"
adamc@56	2753 val () = discoverC string "string"
adamc@56	2754
adamc@83	2755 fun elabDecl' (d, (env, gs)) =
adamc@76	2756 let
adamc@76	2757 val () = resetKunif ()
adamc@76	2758 val () = resetCunif ()
adamc@88	2759 val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs))
adamc@76	2760 in
adamc@76	2761 if ErrorMsg.anyErrors () then
adamc@76	2762 ()
adamc@76	2763 else (
adamc@76	2764 if List.exists kunifsInDecl ds then
adamc@91	2765 declError env (KunifsRemain ds)
adamc@76	2766 else
adamc@76	2767 ();
adamc@76	2768
adamc@76	2769 case ListUtil.search cunifsInDecl ds of
adamc@76	2770 NONE => ()
adamc@76	2771 \| SOME loc =>
adamc@91	2772 declError env (CunifsRemain ds)
adamc@76	2773 );
adamc@76	2774
adamc@83	2775 (ds, (env, gs))
adamc@76	2776 end
adamc@76	2777
adamc@83	2778 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
adamc@56	2779 in
adamc@84	2780 if ErrorMsg.anyErrors () then
adamc@84	2781 ()
adamc@84	2782 else
adamc@90	2783 app (fn (loc, env, denv, c1, c2) =>
adamc@84	2784 case D.prove env denv (c1, c2, loc) of
adamc@84	2785 [] => ()
adamc@84	2786 \| _ =>
adamc@86	2787 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
adamc@84	2788 eprefaces' [("Con 1", p_con env c1),
adamc@90	2789 ("Con 2", p_con env c2),
adamc@90	2790 ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)),
adamc@90	2791 ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) gs;
adamc@83	2792
adamc@56	2793 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
adamc@56	2794 end
adamc@2	2795
adamc@2	2796 end

Mercurial > urweb

annotate src/elaborate.sml @ 200:5dbba661deab