0 | module Data.List.Lens
 1 |
 2 | import Data.List
 3 | import Data.Profunctor
 4 | import public Control.Lens
 5 |
 6 | %default total
 7 |
 8 |
 9 | stripPrefix : Eq a => List a -> List a -> Maybe (List a)
10 | stripPrefix [] ys = Just ys
11 | stripPrefix (_ :: _) [] = Nothing
12 | stripPrefix (x :: xs) (y :: ys) = guard (x == y) *> stripPrefix xs ys
13 |
14 | stripSuffix : Eq a => List a -> List a -> Maybe (List a)
15 | stripSuffix qs xs0 = go xs0 zs
16 |   where
17 |     drp : List a -> List a -> List a
18 |     drp (_::ps) (_::xs) = drp ps xs
19 |     drp [] xs = xs
20 |     drp _  [] = []
21 |
22 |     zs : List a
23 |     zs = drp qs xs0
24 |
25 |     go : List a -> List a -> Maybe (List a)
26 |     go (_::xs) (_::ys) = go xs ys
27 |     go xs [] = zipWith const xs0 zs <$ guard (xs == qs)
28 |     go [] _  = Nothing
29 |
30 |
31 | ||| A prism that strips a prefix from a list of values.
32 | public export
33 | prefixed : Eq a => List a -> Prism' (List a) (List a)
34 | prefixed xs = prism' (xs ++) (stripPrefix xs)
35 |
36 | ||| A prism that strips a suffix from a list of values.
37 | public export
38 | suffixed : Eq a => List a -> Prism' (List a) (List a)
39 | suffixed xs = prism' (++ xs) (stripSuffix xs)
40 |
41 |
42 | ||| An isomorphism between a list and its reverse.
43 | public export
44 | reversed : Iso (List a) (List b) (List a) (List b)
45 | reversed = iso reverse reverse
46 |
47 |
48 | public export
49 | Ixed Nat a (List a) where
50 |   ix = element
51 |
52 | public export
53 | Cons (List a) (List b) a b where
54 |   consIso = iso (\case
55 |       [] => Nothing
56 |       x :: xs => Just (x,xs))
57 |     (maybe [] $ uncurry (::))
58 |
59 |   cons_ = prism (uncurry (::)) (\case
60 |     [] => Left []
61 |     x :: xs => Right (x, xs))
62 |
63 | unsnoc : a -> List a -> (List a, a)
64 | unsnoc x [] = ([], x)
65 | unsnoc x (y :: xs) = mapFst (x ::) $ unsnoc y xs
66 |
67 | public export
68 | Snoc (List a) (List b) a b where
69 |   snocIso = iso (\case
70 |       [] => Nothing
71 |       x :: xs => Just $ unsnoc x xs)
72 |     (maybe [] $ uncurry snoc)
73 |
74 |   snoc_ = prism (uncurry snoc) (\case
75 |     [] => Left []
76 |     x :: xs => Right $ unsnoc x xs)
77 |
78 | public export
79 | Each (List a) (List b) a b where
80 |   each = traversed
81 |
82 | public export
83 | Num i => IEach i (List a) (List b) a b where
84 |   ieach = itraversed
85 |