Mercurial > urweb

comparison src/elaborate.sml @ 1345:9e0fa4f6ac93

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fiddly tweaks
author Adam Chlipala <adam@chlipala.net>
date Thu, 16 Dec 2010 13:35:40 -0500
parents 91eaa1542c5a
children faad7d01b200
comparison
equal deleted inserted replaced
1344:660a2715e2bd 1345:9e0fa4f6ac93
4260 val (env', top_n) = E.pushStrNamed env' "Top" topSgn 4260 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
4261 val () = top_r := top_n 4261 val () = top_r := top_n
4262 4262
4263 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} 4263 val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn}
4264 4264
4265 val checks = ref ([] : (unit -> unit) list)
4266
4267 fun elabDecl' (d, (env, gs)) = 4265 fun elabDecl' (d, (env, gs)) =
4268 let 4266 let
4269 val () = resetKunif () 4267 val () = resetKunif ()
4270 val () = resetCunif () 4268 val () = resetCunif ()
4271 val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs)) 4269 val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs))
4272 in 4270 in
4273 checks := 4271 (**)
4274 (fn () => 4272 (ds, (env', gs))
4275 (if List.exists kunifsInDecl ds then
4276 declError env (KunifsRemain ds)
4277 else
4278 ();
4279
4280 case ListUtil.search cunifsInDecl ds of
4281 NONE => ()
4282 | SOME loc =>
4283 declError env (CunifsRemain ds)))
4284 :: !checks;
4285
4286 (ds, (env, gs))
4287 end 4273 end
4288 4274
4289 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file 4275 val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
4290 4276
4291 fun oneSummaryRound () = 4277 fun oneSummaryRound () =
4292 if ErrorMsg.anyErrors () then 4278 if ErrorMsg.anyErrors () then
4293 () 4279 ()
4294 else 4280 else
4388 eprefaces' [("Con 1", p_con env c1), 4374 eprefaces' [("Con 1", p_con env c1),
4389 ("Con 2", p_con env c2), 4375 ("Con 2", p_con env c2),
4390 ("Hnormed 1", p_con env c1'), 4376 ("Hnormed 1", p_con env c1'),
4391 ("Hnormed 2", p_con env c2')]; 4377 ("Hnormed 2", p_con env c2')];
4392 4378
4393 app (fn (loc, env, k, s1, s2) => 4379 (*app (fn (loc, env, k, s1, s2) =>
4394 eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)), 4380 eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)),
4395 ("s2", p_summary env (normalizeRecordSummary env s2))]) 4381 ("s2", p_summary env (normalizeRecordSummary env s2))])
4396 (!delayedUnifs); 4382 (!delayedUnifs);*)
4397 4383
4398 if (isUnif c1' andalso maybeAttr c2') 4384 if (isUnif c1' andalso maybeAttr c2')
4399 orelse (isUnif c2' andalso maybeAttr c1') then 4385 orelse (isUnif c2' andalso maybeAttr c1') then
4400 TextIO.output (TextIO.stdErr, 4386 TextIO.output (TextIO.stdErr,
4401 "You may be using a disallowed attribute with an HTML tag.\n") 4387 "You may be using a disallowed attribute with an HTML tag.\n")
4420 handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification"; 4406 handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification";
4421 cunifyError env err)) 4407 cunifyError env err))
4422 (!delayedUnifs); 4408 (!delayedUnifs);
4423 delayedUnifs := []); 4409 delayedUnifs := []);
4424 4410
4425 if ErrorMsg.anyErrors () then 4411 ignore (List.exists (fn d => if kunifsInDecl d then
4426 () 4412 (declError env'' (KunifsRemain [d]);
4427 else 4413 true)
4428 app (fn f => f ()) (!checks); 4414 else
4415 false) file);
4416
4417 ignore (List.exists (fn d => case cunifsInDecl d of
4418 NONE => false
4419 | SOME _ => (declError env'' (CunifsRemain [d]);
4420 true)) file);
4429 4421
4430 if ErrorMsg.anyErrors () then 4422 if ErrorMsg.anyErrors () then
4431 () 4423 ()
4432 else 4424 else
4433 app (fn all as (env, _, _, loc) => 4425 app (fn all as (env, _, _, loc) =>
4435 NONE => () 4427 NONE => ()
4436 | SOME p => expError env (Inexhaustive (loc, p))) 4428 | SOME p => expError env (Inexhaustive (loc, p)))
4437 (!delayedExhaustives); 4429 (!delayedExhaustives);
4438 4430
4439 (*preface ("file", p_file env' file);*) 4431 (*preface ("file", p_file env' file);*)
4440 4432
4441 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) 4433 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
4442 :: ds 4434 :: ds
4443 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) 4435 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
4444 :: ds' @ file 4436 :: ds' @ file
4445 end 4437 end