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