git.iko.soy/Idris-dev
on master help sign in
Merge pull request #351 from Melvar/hvect
115783cEdwin Brady
lib/Data/HVect.idrnew file+63
compare with master
unifiedsplit
@@ -0,0 +1,63 @@
1+module Data.HVect
2+
3+import Data.Vect
4+
5+%access public
6+%default total
7+
8+using (k : Nat, ts : Vect Type k)
9+ data HVect : Vect Type k -> Type where
10+ Nil : HVect []
11+ (::) : t -> HVect ts -> HVect (t::ts)
12+
13+ index : (i : Fin k) -> HVect ts -> index i ts
14+ index fO (x::xs) = x
15+ index (fS j) (x::xs) = index j xs
16+
17+ deleteAt : {us : Vect Type (S l)} -> (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)
18+ deleteAt fO (x::xs) = xs
19+ deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs
20+ deleteAt _ [] impossible
21+
22+ replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)
23+ replaceAt fO y (x::xs) = y::xs
24+ replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs
25+
26+ updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)
27+ updateAt fO f (x::xs) = f x :: xs
28+ updateAt (fS j) f (x::xs) = x :: updateAt j f xs
29+
30+ (++) : {us : Vect Type l} -> HVect ts -> HVect us -> HVect (ts ++ us)
31+ (++) [] ys = ys
32+ (++) (x::xs) ys = x :: (xs ++ ys)
33+
34+ instance Eq (HVect []) where
35+ [] == [] = True
36+
37+ instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where
38+ (x::xs) == (y::ys) = x == y && xs == ys
39+
40+ class Shows (k : Nat) (ts : Vect Type k) where
41+ shows : HVect ts -> Vect String k
42+
43+ instance Shows O [] where
44+ shows [] = []
45+
46+ instance (Show t, Shows k ts) => Shows (S k) (t::ts) where
47+ shows (x::xs) = show x :: shows xs
48+
49+ instance (Shows k ts) => Show (HVect ts) where
50+ show xs = show (shows xs)
51+
52+ get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
53+ get {p = Here} (x::xs) = x
54+ get {p = There p'} (x::xs) = get {p = p'} xs
55+
56+ put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
57+ put {p = Here} y (x::xs) = y :: xs
58+ put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
59+
60+ update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
61+ update {p = Here} f (x::xs) = f x :: xs
62+ update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
63+
lib/Data/Vect.idrnew file+32
@@ -0,0 +1,32 @@
1+module Data.Vect
2+
3+import Language.Reflection
4+
5+%access public
6+%default total
7+
8+--------------------------------------------------------------------------------
9+-- Elem
10+--------------------------------------------------------------------------------
11+
12+data Elem : a -> Vect a k -> Type where
13+ Here : {xs : Vect a k} -> Elem x (x::xs)
14+ There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs)
15+
16+findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic
17+findElem O ctxt goal = Refine "Here" `Seq` Solve
18+findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
19+
20+replaceElem : (xs : Vect t k) -> Elem x xs -> (y : t) -> (ys : Vect t k ** Elem y ys)
21+replaceElem (x::xs) Here y = (y :: xs ** Here)
22+replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)
23+ | (ys ** yinys) = (x :: ys ** There yinys)
24+
25+replaceByElem : (xs : Vect t k) -> Elem x xs -> t -> Vect t k
26+replaceByElem (x::xs) Here y = y :: xs
27+replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y
28+
29+mapElem : {xs : Vect t k} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
30+mapElem Here = Here
31+mapElem (There e) = There (mapElem e)
32+
lib/Prelude/Vect.idr+4
@@ -41,6 +41,10 @@ deleteAt fO (x::xs) = xs
41deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
41deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
42deleteAt _ [] impossible
42deleteAt _ [] impossible
43
43
44+replaceAt : Fin n -> t -> Vect t n -> Vect t n
45+replaceAt fO y (x::xs) = y::xs
46+replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
47+
44--------------------------------------------------------------------------------
48--------------------------------------------------------------------------------
45-- Subvectors
49-- Subvectors
46--------------------------------------------------------------------------------
50--------------------------------------------------------------------------------
lib/base.ipkg+1−1
@@ -25,7 +25,7 @@ modules = Builtins, Prelude, IO, System,
25 Data.Bits, Data.Mod2,
25 Data.Bits, Data.Mod2,
26 Data.Z, Data.Sign,
26 Data.Z, Data.Sign,
27 Data.SortedMap, Data.SortedSet, Data.BoundedList,
27 Data.SortedMap, Data.SortedSet, Data.BoundedList,
28− Data.Vect.Quantifiers,
28+ Data.Vect, Data.HVect, Data.Vect.Quantifiers,
29
29
30 Control.Monad.Identity, Control.Monad.State, Control.Category,
30 Control.Monad.Identity, Control.Monad.State, Control.Category,
31 Control.Arrow,
31 Control.Arrow,