git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/libs/base/Data/HVect.idr
72 lines 2.3 kB history raw
1module Data.HVect
3import Data.Fin
4import Data.Vect
6%access public
7%default total
9||| Heterogeneous vectors where the type index gives, element-wise,
10||| the types of the contents.
11data HVect : Vect k Type -> Type where
12 Nil : HVect []
13 (::) : t -> HVect ts -> HVect (t::ts)
15||| Extract an element from an HVect
16index : (i : Fin k) -> HVect ts -> index i ts
17index FZ (x::xs) = x
18index (FS j) (x::xs) = index j xs
20deleteAt : (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)
21deleteAt FZ (x::xs) = xs
22deleteAt {l = S m} (FS j) (x::xs) = x :: deleteAt j xs
23deleteAt {l = Z} (FS j) (x::xs) = absurd j
24deleteAt _ [] impossible
26replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)
27replaceAt FZ y (x::xs) = y::xs
28replaceAt (FS j) y (x::xs) = x :: replaceAt j y xs
30updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)
31updateAt FZ f (x::xs) = f x :: xs
32updateAt (FS j) f (x::xs) = x :: updateAt j f xs
34||| Append two `HVect`s.
35(++) : HVect ts -> HVect us -> HVect (ts ++ us)
36(++) [] ys = ys
37(++) (x::xs) ys = x :: (xs ++ ys)
39instance Eq (HVect []) where
40 [] == [] = True
42instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where
43 (x::xs) == (y::ys) = x == y && xs == ys
45class Shows (k : Nat) (ts : Vect k Type) where
46 shows : HVect ts -> Vect k String
48instance Shows Z [] where
49 shows [] = []
51instance (Show t, Shows k ts) => Shows (S k) (t::ts) where
52 shows (x::xs) = show x :: shows xs
54instance (Shows k ts) => Show (HVect ts) where
55 show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"
57||| Extract an arbitrary element of the correct type.
58||| @ t the goal type
59get : {default tactics { search 100; } p : Elem t ts} -> HVect ts -> t
60get {p = Here} (x::xs) = x
61get {p = There p'} (x::xs) = get {p = p'} xs
63||| Replace an element with the correct type.
64put : {default tactics { search 100; } p : Elem t ts} -> t -> HVect ts -> HVect ts
65put {p = Here} y (x::xs) = y :: xs
66put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
68||| Update an element with the correct type.
69update : {default tactics { search 100; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
70update {p = Here} f (x::xs) = f x :: xs
71update {p = There p'} f (x::xs) = x :: update {p = p'} f xs