Mercurial > urweb
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 |