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