Ur/Web: src/elaborate.sml annotate

annotate src/elaborate.sml @ 164:6847741e1f5f

Datatypes through monoize

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 29 Jul 2008 13:32:07 -0400
parents	06a98129b23f
children	a158f8c5aa55

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

Mercurial > urweb

annotate src/elaborate.sml @ 164:6847741e1f5f