45de9ab · Idris-dev · git.iko.soy

37

38||| Show that the length function on vectors in fact calculates the length

39private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n

40−lengthCorrect Z [] = refl

40+lengthCorrect Z [] = refl

41lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in refl

42

43--------------------------------------------------------------------------------

66index : Fin n -> Vect n a -> a

67index fZ (x::xs) = x

68index (fS k) (x::xs) = index k xs

69−index fZ [] impossible

69+index fZ [] impossible

70

71||| Insert an element at a particular index

72insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a

79deleteAt fZ (x::xs) = xs

80deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs

81deleteAt {n = Z} (fS k) (x::xs) = absurd k

82−deleteAt _ [] impossible

82+deleteAt _ [] impossible

83

84||| Replace an element at a particlar index with another

85replaceAt : Fin n -> t -> Vect n t -> Vect n t

101||| Get the first m elements of a Vect

102||| @ m the number of elements to take

103take : (n : Nat) -> Vect (n + m) a -> Vect n a

104−take Z xs = []

104+take Z xs = []

105take (S k) (x :: xs) = x :: take k xs

106

107||| Remove the first m elements of a Vect

108||| @ m the number of elements to remove

109drop : (n : Nat) -> Vect (n + m) a -> Vect m a

110−drop Z xs = xs

110+drop Z xs = xs

111drop (S k) (x :: xs) = drop k xs

112

113--------------------------------------------------------------------------------

115--------------------------------------------------------------------------------

116

117||| Reverse the order of the elements of a vector

118−total reverse : {n : Nat} -> Vect n a -> Vect n a

118+reverse : Vect n a -> Vect n a

119−reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs

119+reverse xs = go [] xs

120− where

120+ where go : Vect n a -> Vect m a -> Vect (n+m) a

121− total reverse' : {m, j, l : Nat} ->

121+ go {n} acc [] = rewrite plusZeroRightNeutral n in acc

122− Vect m a -> (j + m = l) -> Vect j a -> Vect l a

123− reverse' {m} {j = Z } {l} acc prf [] ?= acc

124− reverse' {m} {j = S k} {l} acc prf (x::xs) =

125− let prf1 : (m + (S k) = l) = rewrite plusCommutative m (S k) in prf in

126− let prf2 : (S (m + k) = l) = rewrite plusSuccRightSucc m k in prf1 in

127− let prf3 : (S (k + m) = l) = rewrite plusCommutative k m in prf2 in

128− let prf4 : (k + (S m) = l) = rewrite sym $ plusSuccRightSucc k m in prf3 in

122+ go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m

129− reverse' (x::acc) prf4 xs

123+ in go (x::acc) xs

130

124

131||| Alternate an element between the other elements of a vector

125||| Alternate an element between the other elements of a vector

132||| @ sep the element to intersperse

126||| @ sep the element to intersperse

136intersperse sep (x::xs) = x :: intersperse' sep xs

130intersperse sep (x::xs) = x :: intersperse' sep xs

137 where

131 where

138 intersperse' : a -> Vect n a -> Vect (n + n) a

132 intersperse' : a -> Vect n a -> Vect (n + n) a

139− intersperse' sep [] = []

133+ intersperse' sep [] = []

134+ intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n

140− intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs

135+ in sep :: x :: intersperse' sep xs

141

136

142--------------------------------------------------------------------------------

137--------------------------------------------------------------------------------

143-- Conversion from list (toList is provided by Foldable)

138-- Conversion from list (toList is provided by Foldable)

147fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a

142fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a

148fromList' ys [] = ys

143fromList' ys [] = ys

149fromList' {n} ys (x::xs) =

144fromList' {n} ys (x::xs) =

150− rewrite (plusSuccRightSucc (length xs) n) ==>

145+ rewrite (plusSuccRightSucc (length xs) n) ==>

151 Vect (plus (length xs) (S n)) a in

146 Vect (plus (length xs) (S n)) a in

152 fromList' (x::ys) xs

147 fromList' (x::ys) xs

153

148

212--------------------------------------------------------------------------------

207--------------------------------------------------------------------------------

213

208

214instance Ord a => Ord (Vect n a) where

209instance Ord a => Ord (Vect n a) where

215− compare [] [] = EQ

210+ compare [] [] = EQ

216 compare (x::xs) (y::ys) =

211 compare (x::xs) (y::ys) =

217 if x /= y then

212 if x /= y then

218 compare x y

213 compare x y

228 map f [] = []

223 map f [] = []

229 map f (x::xs) = f x :: map f xs

224 map f (x::xs) = f x :: map f xs

230

225

231−-- XXX: causes Idris to enter an infinite loop when type checking in the REPL

226+

232−--mapMaybe : (a -> Maybe b) -> Vect n a -> (p ** Vect b p)

227+||| Map a partial function across a vector, returning those elements for which

233−--mapMaybe f [] = (_ ** [])

228+||| the function had a value.

234−--mapMaybe f (x::xs) = mapMaybe' (f x)

229+|||

235−-- XXX: working around the type restrictions on case statements

230+||| The first projection of the resulting pair (ie the length) will always be

236−-- where

231+||| at most the length of the input vector. This is not, however, guaranteed

237−-- mapMaybe' : (Maybe b) -> (n ** Vect b n) -> (p ** Vect b p)

232+||| by the type.

238−-- mapMaybe' Nothing (n ** tail) = (n ** tail)

233+|||

239−-- mapMaybe' (Just j) (n ** tail) = (S n ** j::tail)

234+||| @ f the partial function (expressed by returning `Maybe`)

235+||| @ xs the vector to check for results

236+mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)

237+mapMaybe f [] = (_ ** [])

238+mapMaybe f (x::xs) =

239+ let (len ** ys) = mapMaybe f xs

240+ in case f x of

241+ Just y => (S len ** y :: ys)

242+ Nothing => ( len ** ys)

243+

240

244

241--------------------------------------------------------------------------------

245--------------------------------------------------------------------------------

242-- Folds

246-- Folds

451 | (_ ** tail) = (_ ** j::tail)

455 | (_ ** tail) = (_ ** j::tail)

452

456

453diag : Vect n (Vect n a) -> Vect n a

457diag : Vect n (Vect n a) -> Vect n a

454−diag [] = []

458+diag [] = []

455diag ((x::xs)::xss) = x :: diag (map tail xss)

459diag ((x::xs)::xss) = x :: diag (map tail xss)

456

460

457range : Vect n (Fin n)

461range : Vect n (Fin n)

458−range {n=Z} = []

462+range {n=Z} = []

459range {n=S _} = fZ :: map fS range

463range {n=S _} = fZ :: map fS range

460

464

461||| Transpose a Vect of Vects, turning rows into columns and vice versa.

465||| Transpose a Vect of Vects, turning rows into columns and vice versa.

462|||

466|||

463||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.

467||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.

464transpose : Vect m (Vect n a) -> Vect n (Vect m a)

468transpose : Vect m (Vect n a) -> Vect n (Vect m a)

465−transpose [] = replicate _ []

469+transpose [] = replicate _ []

466transpose (x :: xs) = zipWith (::) x (transpose xs)

470transpose (x :: xs) = zipWith (::) x (transpose xs)

467

471

468--------------------------------------------------------------------------------

472--------------------------------------------------------------------------------

483 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

487 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

484

488

485

489

486−--------------------------------------------------------------------------------

487−-- Proofs

488−--------------------------------------------------------------------------------

489−

490−Prelude.Vect.reverse'_lemma_1 = proof {

491− intros;

492− rewrite prf;

493− rewrite sym (plusZeroRightNeutral m);

494− exact value;

495−}

496−

497−Prelude.Vect.intersperse'_lemma_1 = proof {

498− intros;

499− rewrite (plusSuccRightSucc n1 n1);

500− trivial;

501−}