git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1270 from Melvar/vect-things
b5a0c51Edwin Brady
libs/base/Data/Vect.idr+18
compare with master
unifiedsplit
@@ -15,6 +15,24 @@ using (xs : Vect k a)
15 Here : Elem x (x::xs)
15 Here : Elem x (x::xs)
16 There : Elem x xs -> Elem x (y::xs)
16 There : Elem x xs -> Elem x (y::xs)
17
17
18+||| Nothing can be in an empty Vect
19+noEmptyElem : {x : a} -> Elem x [] -> _|_
20+noEmptyElem Here impossible
21+
22+||| An item not in the head and not in the tail is not in the Vect at all
23+neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
24+neitherHereNorThere xneqy xninxs Here = xneqy refl
25+neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs
26+
27+||| A decision procedure for Elem
28+isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
29+isElem x [] = No noEmptyElem
30+isElem x (y :: xs) with (decEq x y)
31+ isElem x (x :: xs) | (Yes refl) = Yes Here
32+ isElem x (y :: xs) | (No xneqy) with (isElem x xs)
33+ isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
34+ isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
35+
18||| A tactic for discovering where, if anywhere, an element is in a vector
36||| A tactic for discovering where, if anywhere, an element is in a vector
19||| @ n how many elements to search before giving up
37||| @ n how many elements to search before giving up
20findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic
38findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic
libs/prelude/Prelude/Vect.idr+6
@@ -451,6 +451,12 @@ range : Vect n (Fin n)
451range {n=Z} = []
451range {n=Z} = []
452range {n=S _} = fZ :: map fS range
452range {n=S _} = fZ :: map fS range
453
453
454+||| Transpose a Vect of Vects, turning rows into columns and vice versa.
455+|||
456+||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
457+transpose : Vect m (Vect n a) -> Vect n (Vect m a)
458+transpose [] = replicate _ []
459+transpose (x :: xs) = zipWith (::) x (transpose xs)
454
460
455--------------------------------------------------------------------------------
461--------------------------------------------------------------------------------
456-- Properties
462-- Properties
test/reg014/reg014.idr+6−6
@@ -3,10 +3,10 @@ module reg014
3Matrix : Type -> Nat -> Nat -> Type
3Matrix : Type -> Nat -> Nat -> Type
4Matrix a n m = Vect n (Vect m a)
4Matrix a n m = Vect n (Vect m a)
5
5
6−transpose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)
6+mytranspose : Matrix a (S n) (S m) -> Matrix a (S m) (S n)
7−transpose ((x:: []) :: []) = [[x]]
7+mytranspose ((x:: []) :: []) = [[x]]
8−transpose [x :: y :: xs] = [x] :: (transpose [y :: xs])
8+mytranspose [x :: y :: xs] = [x] :: (mytranspose [y :: xs])
9−transpose (x :: y :: xs)
9+mytranspose (x :: y :: xs)
10− = let tx = transpose [x] in
10+ = let tx = mytranspose [x] in
11− let ux = transpose (y :: xs) in zipWith (++) tx ux
11+ let ux = mytranspose (y :: xs) in zipWith (++) tx ux
12
12