diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-10-21 19:24:39 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-10-21 19:24:39 -0400 |
| commit | 17b3f5af99c07d7361fb99124412aff1768cfe13 (patch) | |
| tree | fcfbcfaf492be1aa13c484eea28cfedaf565ed6c /src/elaborate.sml | |
| parent | d66bb9f256db65e3487dec361a4a5a9d7ee238b0 (diff) | |
Sum demo, minus inference of {Unit}s
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index b965f0da..1ea854cd 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -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 |