@@ -234,11 +234,7 @@ unzip3 ((l,c,r)::xs) with (unzip3 xs)
235instance (Eq a) => Eq (Vect n a) where
235instance (Eq a) => Eq (Vect n a) where
236 (==) [] [] = True
236 (==) [] [] = True
237− (==) (x::xs) (y::ys) =
237+ (==) (x::xs) (y::ys) = x == y && xs == ys
244--------------------------------------------------------------------------------
240--------------------------------------------------------------------------------
@@ -285,7 +281,7 @@ mapMaybe f (x::xs) =
286--------------------------------------------------------------------------------
282--------------------------------------------------------------------------------
288−total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
284+foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
289foldrImpl f e go [] = go e
285foldrImpl f e go [] = go e
290foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
286foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
@@ -326,9 +322,7 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
326||| @ xs the vector to search in
322||| @ xs the vector to search in
327elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool
323elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool
328elemBy p e [] = False
324elemBy p e [] = False
329−elemBy p e (x::xs) with (p e x)
325+elemBy p e (x::xs) = p e x || elemBy p e xs
331− | False = elemBy p e xs
333||| Use the default Boolean equality on elements to search for an item
327||| Use the default Boolean equality on elements to search for an item
334||| @ x what to search for
328||| @ x what to search for
@@ -341,9 +335,7 @@ elem = elemBy (==)
341||| @ e the key to look for
335||| @ e the key to look for
342lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b
336lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b
343lookupBy p e [] = Nothing
337lookupBy p e [] = Nothing
344−lookupBy p e ((l, r)::xs) with (p e l)
338+lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
346− | False = lookupBy p e xs
348||| Find the assocation of some key using the default Boolean equality test
340||| Find the assocation of some key using the default Boolean equality test
349lookup : Eq a => a -> Vect n (a, b) -> Maybe b
341lookup : Eq a => a -> Vect n (a, b) -> Maybe b
@@ -355,9 +347,7 @@ lookup = lookupBy (==)
355||| @ xs what to search for
347||| @ xs what to search for
356hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool
348hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool
357hasAnyBy p elems [] = False
349hasAnyBy p elems [] = False
358−hasAnyBy p elems (x::xs) with (elemBy p x elems)
350+hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
360− | False = hasAnyBy p elems xs
362||| Check if any element of xs is found in elems using the default Boolean equality test
352||| Check if any element of xs is found in elems using the default Boolean equality test
363hasAny : Eq a => Vect m a -> Vect n a -> Bool
353hasAny : Eq a => Vect m a -> Vect n a -> Bool
@@ -371,19 +361,15 @@ hasAny = hasAnyBy (==)
371||| @ p the test to satisfy
361||| @ p the test to satisfy
372find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a
362find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a
373find p [] = Nothing
363find p [] = Nothing
374−find p (x::xs) with (p x)
364+find p (x::xs) = if p x then Just x else find p xs
378||| Find the index of the first element of the vector that satisfies some test
366||| Find the index of the first element of the vector that satisfies some test
379findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)
367findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)
380findIndex p [] = Nothing
368findIndex p [] = Nothing
381−findIndex p (x :: xs) with (p x)
383− | False = map FS (findIndex p xs)
369+findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
385||| Find the indices of all elements that satisfy some test
371||| Find the indices of all elements that satisfy some test
386−total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
372+findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
387findIndices = findIndices' 0
373findIndices = findIndices' 0
389 total findIndices' : Nat -> (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
375 total findIndices' : Nat -> (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
@@ -401,10 +387,10 @@ elemIndexBy p e = findIndex $ p e
401elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
387elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
402elemIndex = elemIndexBy (==)
388elemIndex = elemIndexBy (==)
404−total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)
390+elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)
405elemIndicesBy p e = findIndices $ p e
391elemIndicesBy p e = findIndices $ p e
407−total elemIndices : Eq a => a -> Vect m a -> (p ** Vect p Nat)
393+elemIndices : Eq a => a -> Vect m a -> (p ** Vect p Nat)
408elemIndices = elemIndicesBy (==)
394elemIndices = elemIndicesBy (==)
410--------------------------------------------------------------------------------
396--------------------------------------------------------------------------------
@@ -412,14 +398,14 @@ elemIndices = elemIndicesBy (==)
412--------------------------------------------------------------------------------
398--------------------------------------------------------------------------------
414||| Find all elements of a vector that satisfy some test
400||| Find all elements of a vector that satisfy some test
415−total filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
401+filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
416−filter p [] = ( _ ** [] )
402+filter p [] = ( _ ** [] )
417−filter p (x::xs) with (filter p xs)
403+filter p (x::xs) =
418− | (_ ** tail) =
404+ let (_ ** tail) = filter p xs
419− if p x then
405+ in if p x then
420− (_ ** x::tail)
406+ (_ ** x::tail)
422− (_ ** tail)
408+ (_ ** tail)
424||| Make the elements of some vector unique by some test
410||| Make the elements of some vector unique by some test
425nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
411nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
@@ -473,9 +459,7 @@ partition p (x::xs) =
473isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
459isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
474isPrefixOfBy p [] right = True
460isPrefixOfBy p [] right = True
475isPrefixOfBy p left [] = False
461isPrefixOfBy p left [] = False
476−isPrefixOfBy p (x::xs) (y::ys) with (p x y)
462+isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
477− | True = isPrefixOfBy p xs ys
480isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool
464isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool
481isPrefixOf = isPrefixOfBy (==)
465isPrefixOf = isPrefixOfBy (==)
@@ -490,11 +474,11 @@ isSuffixOf = isSuffixOfBy (==)
490-- Conversions
474-- Conversions
491--------------------------------------------------------------------------------
475--------------------------------------------------------------------------------
493−total maybeToVect : Maybe a -> (p ** Vect p a)
477+maybeToVect : Maybe a -> (p ** Vect p a)
494maybeToVect Nothing = (_ ** [])
478maybeToVect Nothing = (_ ** [])
495maybeToVect (Just j) = (_ ** [j])
479maybeToVect (Just j) = (_ ** [j])
497−total vectToMaybe : Vect n a -> Maybe a
481+vectToMaybe : Vect n a -> Maybe a
498vectToMaybe [] = Nothing
482vectToMaybe [] = Nothing
499vectToMaybe (x::xs) = Just x
483vectToMaybe (x::xs) = Just x
@@ -505,21 +489,22 @@ vectToMaybe (x::xs) = Just x
505catMaybes : Vect n (Maybe a) -> (p ** Vect p a)
489catMaybes : Vect n (Maybe a) -> (p ** Vect p a)
506catMaybes [] = (_ ** [])
490catMaybes [] = (_ ** [])
507catMaybes (Nothing::xs) = catMaybes xs
491catMaybes (Nothing::xs) = catMaybes xs
508−catMaybes ((Just j)::xs) with (catMaybes xs)
492+catMaybes ((Just j)::xs) =
493+ let (_ ** tail) = catMaybes xs
509− | (_ ** tail) = (_ ** j::tail)
494+ in (_ ** j::tail)
511diag : Vect n (Vect n a) -> Vect n a
496diag : Vect n (Vect n a) -> Vect n a
512diag [] = []
497diag [] = []
513diag ((x::xs)::xss) = x :: diag (map tail xss)
498diag ((x::xs)::xss) = x :: diag (map tail xss)
515−range : Vect n (Fin n)
500+range : {n : Nat} -> Vect n (Fin n)
516range {n=Z} = []
501range {n=Z} = []
517range {n=S _} = FZ :: map FS range
502range {n=S _} = FZ :: map FS range
519||| Transpose a Vect of Vects, turning rows into columns and vice versa.
504||| Transpose a Vect of Vects, turning rows into columns and vice versa.
521||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
506||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
522−transpose : Vect m (Vect n a) -> Vect n (Vect m a)
507+transpose : {n : Nat} -> Vect m (Vect n a) -> Vect n (Vect m a)
523transpose [] = replicate _ []
508transpose [] = replicate _ []
524transpose (x :: xs) = zipWith (::) x (transpose xs)
509transpose (x :: xs) = zipWith (::) x (transpose xs)
@@ -569,11 +554,9 @@ vectAppendAssociative (x :: xs) ys zs =
570--------------------------------------------------------------------------------
555--------------------------------------------------------------------------------
573vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
557vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
574vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
558vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
577vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
560vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
578vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
561vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl