libs/base/Data/Vect.idr · Idris-dev

git.iko.soy/Idris-dev

on bf4e535 help sign in

54 lines 2.2 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)