Mercurial > urweb
comparison src/elaborate.sml @ 209:1487c712eb12
Stub WHERE support
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 16 Aug 2008 12:15:38 -0400 |
parents | cc68da3801bc |
children | f4033abd6ab1 |
comparison
equal
deleted
inserted
replaced
208:63a2f2322c1f | 209:1487c712eb12 |
---|---|
680 in | 680 in |
681 (sum, gs @ gs') | 681 (sum, gs @ gs') |
682 end | 682 end |
683 | 683 |
684 and consEq (env, denv) (c1, c2) = | 684 and consEq (env, denv) (c1, c2) = |
685 (case unifyCons (env, denv) c1 c2 of | 685 let |
686 [] => true | 686 val gs = unifyCons (env, denv) c1 c2 |
687 | _ => false) | 687 in |
688 List.all (fn (loc, env, denv, c1, c2) => | |
689 case D.prove env denv (c1, c2, loc) of | |
690 [] => true | |
691 | _ => false) gs | |
692 end | |
688 handle CUnify _ => false | 693 handle CUnify _ => false |
689 | 694 |
690 and consNeq env (c1, c2) = | 695 and consNeq env (c1, c2) = |
691 case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of | 696 case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of |
692 (L'.CName x1, L'.CName x2) => x1 <> x2 | 697 (L'.CName x1, L'.CName x2) => x1 <> x2 |
855 end | 860 end |
856 end | 861 end |
857 | 862 |
858 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = | 863 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = |
859 let | 864 let |
860 fun err f = raise CUnify' (f (c1All, c2All)) | 865 fun err f = (prefaces "unifyCons'' fails" [("c1All", p_con env c1All), |
866 ("c2All", p_con env c2All)]; | |
867 raise CUnify' (f (c1All, c2All))) | |
861 | 868 |
862 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) | 869 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) |
863 in | 870 in |
864 (*eprefaces "unifyCons''" [("c1All", p_con env c1All), | 871 (*eprefaces "unifyCons''" [("c1All", p_con env c1All), |
865 ("c2All", p_con env c2All)];*) | 872 ("c2All", p_con env c2All)];*) |
953 | 960 |
954 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => | 961 | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => |
955 (unifyKinds dom1 dom2; | 962 (unifyKinds dom1 dom2; |
956 unifyKinds ran1 ran2; | 963 unifyKinds ran1 ran2; |
957 []) | 964 []) |
958 | |
959 | 965 |
960 | _ => err CIncompatible | 966 | _ => err CIncompatible |
961 end | 967 end |
962 | 968 |
963 and unifyCons (env, denv) c1 c2 = | 969 and unifyCons (env, denv) c1 c2 = |