comparison 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
comparison
equal deleted inserted replaced
410:c5a3d223f157 411:06fcddcd20d3
819 val gs4 = unifyCons' (env, denv') t1 t2 819 val gs4 = unifyCons' (env, denv') t1 t2
820 in 820 in
821 gs1 @ gs2 @ gs3 @ gs4 821 gs1 @ gs2 @ gs3 @ gs4
822 end 822 end
823 | _ => 823 | _ =>
824 let 824 case (kindof env c1, kindof env c2) of
825 val (c1, gs1) = hnormCon (env, denv) c1 825 ((L'.KUnit, _), (L'.KUnit, _)) => []
826 val (c2, gs2) = hnormCon (env, denv) c2 826 | _ =>
827 in
828 let 827 let
829 val gs3 = unifyCons'' (env, denv) c1 c2 828 val (c1, gs1) = hnormCon (env, denv) c1
829 val (c2, gs2) = hnormCon (env, denv) c2
830 in 830 in
831 gs1 @ gs2 @ gs3 831 let
832 val gs3 = unifyCons'' (env, denv) c1 c2
833 in
834 gs1 @ gs2 @ gs3
835 end
836 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
832 end 837 end
833 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
834 end
835 838
836 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = 839 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
837 let 840 let
838 fun err f = raise CUnify' (f (c1All, c2All)) 841 fun err f = raise CUnify' (f (c1All, c2All))
839 842