Mercurial > urweb
diff src/elaborate.sml @ 1345:9e0fa4f6ac93
Fiddly tweaks
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 16 Dec 2010 13:35:40 -0500 |
parents | 91eaa1542c5a |
children | faad7d01b200 |
line wrap: on
line diff
--- a/src/elaborate.sml Thu Dec 16 10:23:37 2010 -0500 +++ b/src/elaborate.sml Thu Dec 16 13:35:40 2010 -0500 @@ -4262,31 +4262,17 @@ val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} - val checks = ref ([] : (unit -> unit) list) - fun elabDecl' (d, (env, gs)) = let val () = resetKunif () val () = resetCunif () - val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs)) + val (ds, (env', _, gs)) = elabDecl (d, (env, D.empty, gs)) in - checks := - (fn () => - (if List.exists kunifsInDecl ds then - declError env (KunifsRemain ds) - else - (); - - case ListUtil.search cunifsInDecl ds of - NONE => () - | SOME loc => - declError env (CunifsRemain ds))) - :: !checks; - - (ds, (env, gs)) + (**) + (ds, (env', gs)) end - val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file + val (file, (env'', gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file fun oneSummaryRound () = if ErrorMsg.anyErrors () then @@ -4390,10 +4376,10 @@ ("Hnormed 1", p_con env c1'), ("Hnormed 2", p_con env c2')]; - app (fn (loc, env, k, s1, s2) => + (*app (fn (loc, env, k, s1, s2) => eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)), ("s2", p_summary env (normalizeRecordSummary env s2))]) - (!delayedUnifs); + (!delayedUnifs);*) if (isUnif c1' andalso maybeAttr c2') orelse (isUnif c2' andalso maybeAttr c1') then @@ -4422,10 +4408,16 @@ (!delayedUnifs); delayedUnifs := []); - if ErrorMsg.anyErrors () then - () - else - app (fn f => f ()) (!checks); + ignore (List.exists (fn d => if kunifsInDecl d then + (declError env'' (KunifsRemain [d]); + true) + else + false) file); + + ignore (List.exists (fn d => case cunifsInDecl d of + NONE => false + | SOME _ => (declError env'' (CunifsRemain [d]); + true)) file); if ErrorMsg.anyErrors () then () @@ -4437,7 +4429,7 @@ (!delayedExhaustives); (*preface ("file", p_file env' file);*) - + (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)