summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 19:24:39 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 19:24:39 -0400
commit17b3f5af99c07d7361fb99124412aff1768cfe13 (patch)
treefcfbcfaf492be1aa13c484eea28cfedaf565ed6c /src/elaborate.sml
parentd66bb9f256db65e3487dec361a4a5a9d7ee238b0 (diff)
Sum demo, minus inference of {Unit}s
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml19
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