Mercurial > urweb
diff src/elaborate.sml @ 411:06fcddcd20d3
Sum demo, minus inference of {Unit}s
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 21 Oct 2008 19:24:39 -0400 |
parents | 8084fa9216de |
children | df4cbd90a26e |
line wrap: on
line diff
--- a/src/elaborate.sml Tue Oct 21 18:44:52 2008 -0400 +++ b/src/elaborate.sml Tue Oct 21 19:24:39 2008 -0400 @@ -821,17 +821,20 @@ gs1 @ gs2 @ gs3 @ gs4 end | _ => - let - val (c1, gs1) = hnormCon (env, denv) c1 - val (c2, gs2) = hnormCon (env, denv) c2 - in + case (kindof env c1, kindof env c2) of + ((L'.KUnit, _), (L'.KUnit, _)) => [] + | _ => let - val gs3 = unifyCons'' (env, denv) c1 c2 + val (c1, gs1) = hnormCon (env, denv) c1 + val (c2, gs2) = hnormCon (env, denv) c2 in - gs1 @ gs2 @ gs3 + let + val gs3 = unifyCons'' (env, denv) c1 c2 + in + gs1 @ gs2 @ gs3 + end + handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) end - handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) - end and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = let