08ddbaa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Reformulate decEq for Vect.

08ddbaaMatus Tejiscak13 years ago

libs/prelude/Decidable/Equality.idr+11−1

compare with master

unifiedsplit

@@ -174,13 +174,23 @@ total

174vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys

175vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl

176

177+instance DecEq a => DecEq (Vect n a) where

178+ decEq [] [] = Yes refl

179+ decEq (x :: xs) (y :: ys) with (decEq x y)

180+ decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)

181+ decEq (x :: xs) (x :: xs) | Yes refl | Yes refl = Yes refl

182+ decEq (x :: xs) (x :: ys) | Yes refl | No neq = No (neq . vectInjective2)

183+ decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)

184+

185+{- The following definition is elaborated in a wrong case-tree. Examination pending.

186+

177instance DecEq a => DecEq (Vect n a) where

187instance DecEq a => DecEq (Vect n a) where

178 decEq [] [] = Yes refl

188 decEq [] [] = Yes refl

179 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

189 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

180 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl

190 decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl

181 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))

191 decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))

182 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))

192 decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))

183−

193+-}

184

194

185-- For the primitives, we have to cheat because we don't have access to their

195-- For the primitives, we have to cheat because we don't have access to their

186-- internal implementations.

196-- internal implementations.

src/Idris/Core/CaseTree.hs+2−1

@@ -19,7 +19,7 @@ data CaseDef = CaseDef [Name] !SC [Term]

19-- in other words, it never inspects anything else than variables.

20--

21-- ProjCase is a special powerful case construct that allows inspection

22−-- of compound terms. Occurences of ProjCase arise no earlier than

22+-- of compound terms. Occurrences of ProjCase arise no earlier than

23-- in the function `prune` as a means of optimisation

24-- of already built case trees.

25--

@@ -603,6 +603,7 @@ prune proj (Case n alts) = case alts' of

603 -- f x = ... x!0 ...

604 --

605 -- Hence, we disable this step.

606+ -- TODO: re-enable this in toIR

606 --

607 --

607 -- as@[ConCase cn i args sc]

608 -- as@[ConCase cn i args sc]

608 -- | proj -> mkProj n 0 args (prune proj sc)

609 -- | proj -> mkProj n 0 args (prune proj sc)