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