4a6974c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix ordering of patterns in conversion check

4a6974cEdwin Brady10 years ago

src/Idris/Core/Evaluate.hs+10−8

@@ -640,14 +640,6 @@ convEq ctxt holes topx topy = ceq [] topx topy where

640 | x `elem` holes || y `elem` holes = return True

641 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

642 | otherwise = sameDefs ps x y

643− ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))

644− = ceq ps x (substV (P Bound n t) y)

645− ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y

646− = ceq ps (substV (P Bound n t) x) y

647− ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))

648− | n == n' = ceq ps x y

649− ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y

650− | n == n' = ceq ps x y

651

643

652 ceq ps (Bind n (PVar _ t) sc) y = ceq ps sc y

644 ceq ps (Bind n (PVar _ t) sc) y = ceq ps sc y

653 ceq ps x (Bind n (PVar _ t) sc) = ceq ps x sc

645 ceq ps x (Bind n (PVar _ t) sc) = ceq ps x sc

@@ -668,6 +660,16 @@ convEq ctxt holes topx topy = ceq [] topx topy where

668 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

660 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

669 ceqB ps (Pi r i v t) (Pi r' i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

661 ceqB ps (Pi r i v t) (Pi r' i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

670 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

662 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

663+

664+ ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))

665+ = ceq ps x (substV (P Bound n t) y)

666+ ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y

667+ = ceq ps (substV (P Bound n t) x) y

668+ ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))

669+ | n == n' = ceq ps x y

670+ ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y

671+ | n == n' = ceq ps x y

672+

671 -- Special case for 'case' blocks - size of scope causes complications,

673 -- Special case for 'case' blocks - size of scope causes complications,

672 -- we only want to check the blocks themselves are valid and identical

674 -- we only want to check the blocks themselves are valid and identical

673 -- in the current scope. So, just check the bodies, and the additional

675 -- in the current scope. So, just check the bodies, and the additional