Mercurial > urweb

comparison src/elaborate.sml @ 209:1487c712eb12

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 =