@@ -5,68 +5,67 @@ import Data.Vect
55%access public
66%default total
77
8−using (k : Nat, ts : Vect k Type)
9− ||| Heterogeneous vectors where the type index gives, element-wise,
10− ||| the types of the contents.
11− data HVect : Vect k Type -> Type where
12− Nil : HVect []
13− (::) : t -> HVect ts -> HVect (t::ts)
14−
15− ||| Extract an element from an HVect
16− index : (i : Fin k) -> HVect ts -> index i ts
17− index fZ (x::xs) = x
18− index (fS j) (x::xs) = index j xs
19−
20− deleteAt : (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)
21− deleteAt fZ (x::xs) = xs
22− deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs
23− deleteAt {l = Z} (fS j) (x::xs) = absurd j
24− deleteAt _ [] impossible
25−
26− replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)
27− replaceAt fZ y (x::xs) = y::xs
28− replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs
29−
30− updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)
31− updateAt fZ f (x::xs) = f x :: xs
32− updateAt (fS j) f (x::xs) = x :: updateAt j f xs
33−
34− ||| Append two `HVect`s.
35− (++) : HVect ts -> HVect us -> HVect (ts ++ us)
36− (++) [] ys = ys
37− (++) (x::xs) ys = x :: (xs ++ ys)
38−
39− instance Eq (HVect []) where
40− [] == [] = True
41−
42− instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where
43− (x::xs) == (y::ys) = x == y && xs == ys
44−
45− class Shows (k : Nat) (ts : Vect k Type) where
46− shows : HVect ts -> Vect k String
47−
48− instance Shows Z [] where
49− shows [] = []
50−
51− instance (Show t, Shows k ts) => Shows (S k) (t::ts) where
52− shows (x::xs) = show x :: shows xs
53−
54− instance (Shows k ts) => Show (HVect ts) where
55− show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"
56−
57− ||| Extract an arbitrary element of the correct type.
58− ||| @ t the goal type
59− get : {default tactics { search 100; } p : Elem t ts} -> HVect ts -> t
60− get {p = Here} (x::xs) = x
61− get {p = There p'} (x::xs) = get {p = p'} xs
62−
63− ||| Replace an element with the correct type.
64− put : {default tactics { search 100; } p : Elem t ts} -> t -> HVect ts -> HVect ts
65− put {p = Here} y (x::xs) = y :: xs
66− put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
67−
68− ||| Update an element with the correct type.
69− update : {default tactics { search 100; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
70− update {p = Here} f (x::xs) = f x :: xs
71− update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
8+||| Heterogeneous vectors where the type index gives, element-wise,
9+||| the types of the contents.
10+data HVect : Vect k Type -> Type where
11+ Nil : HVect []
12+ (::) : t -> HVect ts -> HVect (t::ts)
13+
14+||| Extract an element from an HVect
15+index : (i : Fin k) -> HVect ts -> index i ts
16+index fZ (x::xs) = x
17+index (fS j) (x::xs) = index j xs
18+
19+deleteAt : (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)
20+deleteAt fZ (x::xs) = xs
21+deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs
22+deleteAt {l = Z} (fS j) (x::xs) = absurd j
23+deleteAt _ [] impossible
24+
25+replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)
26+replaceAt fZ y (x::xs) = y::xs
27+replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs
28+
29+updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)
30+updateAt fZ f (x::xs) = f x :: xs
31+updateAt (fS j) f (x::xs) = x :: updateAt j f xs
32+
33+||| Append two `HVect`s.
34+(++) : HVect ts -> HVect us -> HVect (ts ++ us)
35+(++) [] ys = ys
36+(++) (x::xs) ys = x :: (xs ++ ys)
37+
38+instance Eq (HVect []) where
39+ [] == [] = True
40+
41+instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where
42+ (x::xs) == (y::ys) = x == y && xs == ys
43+
44+class Shows (k : Nat) (ts : Vect k Type) where
45+ shows : HVect ts -> Vect k String
46+
47+instance Shows Z [] where
48+ shows [] = []
49+
50+instance (Show t, Shows k ts) => Shows (S k) (t::ts) where
51+ shows (x::xs) = show x :: shows xs
52+
53+instance (Shows k ts) => Show (HVect ts) where
54+ show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"
55+
56+||| Extract an arbitrary element of the correct type.
57+||| @ t the goal type
58+get : {default tactics { search 100; } p : Elem t ts} -> HVect ts -> t
59+get {p = Here} (x::xs) = x
60+get {p = There p'} (x::xs) = get {p = p'} xs
61+
62+||| Replace an element with the correct type.
63+put : {default tactics { search 100; } p : Elem t ts} -> t -> HVect ts -> HVect ts
64+put {p = Here} y (x::xs) = y :: xs
65+put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
66+
67+||| Update an element with the correct type.
68+update : {default tactics { search 100; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
69+update {p = Here} f (x::xs) = f x :: xs
70+update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
7271