git.iko.soy/Idris-dev
on fbb201c help sign in
Idris-dev/libs/base/Data/Vect.idr
81 lines 3.5 kB history raw
1module Data.Vect
3import Language.Reflection
4import public Data.VectType
6%access public
7%default total
9--------------------------------------------------------------------------------
10-- Elem
11--------------------------------------------------------------------------------
13||| A proof that some element is found in a vector
14data Elem : a -> Vect k a -> Type where
15 Here : Elem x (x::xs)
16 There : Elem x xs -> Elem x (y::xs)
18||| Nothing can be in an empty Vect
19noEmptyElem : {x : a} -> Elem x [] -> Void
20noEmptyElem Here impossible
22||| An item not in the head and not in the tail is not in the Vect at all
23neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
24neitherHereNorThere xneqy xninxs Here = xneqy Refl
25neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs
27||| A decision procedure for Elem
28isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
29isElem x [] = No noEmptyElem
30isElem 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)
36||| A tactic for discovering where, if anywhere, an element is in a vector
37||| @ n how many elements to search before giving up
38findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic
39findElem Z ctxt goal = Refine "Here" `Seq` Solve
40findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
42replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)
43replaceElem (x::xs) Here y = (y :: xs ** Here)
44replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)
45 | (ys ** yinys) = (x :: ys ** There yinys)
47replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t
48replaceByElem (x::xs) Here y = y :: xs
49replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y
51mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
52mapElem Here = Here
53mapElem (There e) = There (mapElem e)
55-- Some convenience functions for testing lengths
57||| If the given Vect is the required length, return a Vect with that
58||| length in its type, otherwise return Nothing
59||| @len the required length
60||| @xs the vector with the desired length
61-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
62-- only know we don't know how to make a Vect n a, not that one can't exist.
63isLength : {m : Nat} -> -- expected at run-time
64 (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
65isLength {m} len xs with (decEq m len)
66 isLength {m = m} m xs | (Yes Refl) = Just xs
67 isLength {m = m} len xs | (No contra) = Nothing
69||| If the given Vect is at least the required length, return a Vect with
70||| at least that length in its type, otherwise return Nothing
71||| @len the required length
72||| @xs the vector with the desired length
73overLength : {m : Nat} -> -- expected at run-time
74 (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
75overLength {m} n xs with (cmp m n)
76 overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing
77 overLength {m = m} m xs | CmpEQ
78 = Just (0 ** xs)
79 overLength {m = plus n (S x)} n xs | (CmpGT x)
80 = Just (S x ** rewrite plusCommutative (S x) n in xs)