@@ -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+