0 | module Data.Vect.Lens
 1 |
 2 | import Data.Vect
 3 | import public Control.Lens
 4 | import Data.Tuple.Lens
 5 | import Data.Profunctor.Traversing
 6 |
 7 | %default total
 8 |
 9 |
10 | ||| An isomorphism between a `Vect` and its reverse.
11 | public export
12 | reversed : Iso (Vect n a) (Vect n b) (Vect n a) (Vect n b)
13 | reversed = iso reverse reverse
14 |
15 |
16 | public export
17 | Ixed Nat a (Vect n a) where
18 |   ix = element
19 |
20 | public export
21 | Ixed' Nat (Fin n) a (Vect n a) where
22 |   ix' n = lens (index n) (flip $ replaceAt n)
23 |
24 | public export
25 | Each (Vect n a) (Vect n b) a b where
26 |   each = traversed
27 |
28 | public export
29 | IEach (Fin n) (Vect n a) (Vect n b) a b where
30 |   ieach = itraversal func
31 |     where
32 |       func : forall n. Applicative f => (Fin n -> a -> f b) -> Vect n a -> f (Vect n b)
33 |       func f [] = pure []
34 |       func f (x :: xs) = [| f FZ x :: func (f . FS) xs |]
35 |
36 |
37 | public export
38 | cons_ : Iso (Vect (S n) a) (Vect (S n) b) (a, Vect n a) (b, Vect n b)
39 | cons_ = iso (\(x :: xs) => (x,xs)) (uncurry (::))
40 |
41 | public export
42 | head_ : Lens' (Vect (S n) a) a
43 | head_ = cons_ . fst_
44 |
45 | public export
46 | tail_ : Lens' (Vect (S n) a) (Vect n a)
47 | tail_ = cons_ . snd_
48 |
49 | public export
50 | snoc_ : Iso (Vect (S n) a) (Vect (S n) b) (Vect n a, a) (Vect n b, b)
51 | snoc_ = iso unsnoc (uncurry snoc)
52 |
53 | public export
54 | init_ : Lens' (Vect (S n) a) (Vect n a)
55 | init_ = snoc_ . fst_
56 |
57 | public export
58 | last_ : Lens' (Vect (S n) a) a
59 | last_ = snoc_ . snd_
60 |