0 | ||| A system for type-safe, traversal-based zippers into arbitrary datatypes.
  1 | module Control.Zipper
  2 |
  3 | import Data.Maybe
  4 | import Data.List
  5 | import Control.Lens
  6 |
  7 | %default total
  8 |
  9 |
 10 | ------------------------------------------------------------------------------
 11 | -- Pointer
 12 | ------------------------------------------------------------------------------
 13 |
 14 |
 15 | ||| The pointer stores the values on the current layer other than the focused one,
 16 | ||| indirectly pointing to the focused value.
 17 | Pointer : (i, a : Type) -> Type
 18 | Pointer i a = (SnocList (i, a), List (i, a))
 19 |
 20 | fromPointer : i -> a -> Pointer i a -> List (i, a)
 21 | fromPointer k x (l, r) = l <>> (k,x) :: r
 22 |
 23 |
 24 | ------------------------------------------------------------------------------
 25 | -- Zipper
 26 | ------------------------------------------------------------------------------
 27 |
 28 |
 29 | export infix 9 @>
 30 |
 31 | ||| A simple type that represents a layer of the zipper as it moves downwards.
 32 | |||
 33 | ||| It also carries an index for that particular layer, if an indexed lens was
 34 | ||| used to create it.
 35 | public export
 36 | data ZipLayer : Type where
 37 |   (@>) : (i, a : Type) -> ZipLayer
 38 |
 39 | ||| Get the type from a layer of a zipper.
 40 | public export
 41 | getTy : ZipLayer -> Type
 42 | getTy (_ @> a) = a
 43 |
 44 |
 45 | ||| The coil keeps track of the data not being focused on by the zipper, and
 46 | ||| allows the final value to be repackaged at the end.
 47 | data Coil : List ZipLayer -> Type -> Type -> Type where
 48 |   Nil  : Coil [] i a
 49 |   Cons : Pointer j s -> j -> (List (i, a) -> s) ->
 50 |           Coil hs j s -> Coil (j @> s :: hs) i a
 51 |
 52 |
 53 | ||| A zipper is a temporary data structure that can be "opened" on a particular
 54 | ||| value, and allows one to move through its structure and operate on any
 55 | ||| part of it.
 56 | ||| A zipper can be opened from *any* value using `zipper`.
 57 | |||
 58 | ||| Rather than being defined for a particular data structure, this zipper type
 59 | ||| uses lenses to traverse through its value. The zipper can be moved down
 60 | ||| through a traversal or lens, up out of one, or left and right between the
 61 | ||| focuses of a traversal.
 62 | |||
 63 | ||| You can use `rezip` to repackage the zipper back into a regular value.
 64 | export
 65 | data Zipper : List ZipLayer -> Type -> Type -> Type where
 66 |   MkZipper : Coil hs i a -> Pointer i a -> i -> a -> Zipper hs i a
 67 |
 68 |
 69 | ||| Open a zipper from a value.
 70 | export
 71 | zipper : a -> Zipper [] () a
 72 | zipper x = MkZipper Nil ([<], []) () x
 73 |
 74 | ||| A lens that points to the current focus of the zipper.
 75 | export
 76 | focus : IndexedLens' i (Zipper hs i a) a
 77 | focus = ilens (\(MkZipper _ _ i x) => (i, x))
 78 |               (\(MkZipper coil p i _),x => MkZipper coil p i x)
 79 |
 80 |
 81 | ------------------------------------------------------------------------------
 82 | -- Zipper movement
 83 | ------------------------------------------------------------------------------
 84 |
 85 |
 86 | ||| Move up a layer of the zipper.
 87 | export
 88 | upward : Zipper (j @> s :: hs) i a -> Zipper hs j s
 89 | upward (MkZipper (Cons p j k coil) q i x) =
 90 |   MkZipper coil p j $ k $ fromPointer i x q
 91 |
 92 | ||| Perform an action on a zipper, but leave the zipper's state unchanged if the
 93 | ||| action fails.
 94 | |||
 95 | ||| This is intended to be used as `tug rightward`, `tug leftward`, etc.
 96 | export
 97 | tug : (a -> Maybe a) -> a -> a
 98 | tug f x = fromMaybe x (f x)
 99 |
100 | ||| Move right one value in the current layer. This will fail if already at the
101 | ||| rightmost value.
102 | export
103 | rightward : Alternative f => Zipper hs i a -> f (Zipper hs i a)
104 | rightward (MkZipper _ (_, []) _ _) = empty
105 | rightward (MkZipper coil (l, (j,y) :: r) i x) =
106 |   pure $ MkZipper coil (l :< (i,x), r) j y
107 |
108 | ||| Move left one value in the current layer. This will fail if already at the
109 | ||| leftmost value.
110 | export
111 | leftward : Alternative f => Zipper hs i a -> f (Zipper hs i a)
112 | leftward (MkZipper _ ([<], _) _ _) = empty
113 | leftward (MkZipper coil (l :< (j,y), r) i x) =
114 |   pure $ MkZipper coil (l, (i,x) :: r) j y
115 |
116 | ||| Move to the rightmost value in the current layer.
117 | export
118 | rightmost : Zipper hs i a -> Zipper hs i a
119 | rightmost (MkZipper coil (l,r) i x) =
120 |   case l :< (i,x) <>< r of
121 |     xs :< (j,y) => MkZipper coil (xs, []) j y
122 |     -- Too lazy to prove this impossible for now
123 |     [<] => assert_total $ idris_crash "Unreachable"
124 |
125 | ||| Move to the leftmost value in the current layer.
126 | export
127 | leftmost : Zipper hs i a -> Zipper hs i a
128 | leftmost (MkZipper coil p i x) =
129 |   case fromPointer i x p of
130 |     (j,y) :: xs => MkZipper coil ([<], xs) j y
131 |     -- Too lazy to prove this impossible for now
132 |     [] => assert_total $ idris_crash "Unreachable"
133 |
134 |
135 | ||| Move downward through an indexed lens.
136 | |||
137 | ||| This cannot fail, since a lens always contains a value.
138 | export
139 | idownward : IndexedLens' i s a -> Zipper hs j s -> Zipper (j @> s :: hs) i a
140 | idownward l (MkZipper coil p j y) =
141 |   let (i,x) = iview l y
142 |   in MkZipper (Cons p j (go . map snd) coil) ([<],[]) i x
143 |   where
144 |     go : List a -> s
145 |     go ls = set (partsOf l) ls y
146 |
147 | ||| Move downward through a lens.
148 | |||
149 | ||| This cannot fail, since a lens always contains a value.
150 | export
151 | downward : Lens' s a -> Zipper hs j s -> Zipper (j @> s :: hs) () a
152 | downward l (MkZipper coil p i x) =
153 |   MkZipper (Cons p i (go . map snd) coil) ([<], []) () (x ^. l)
154 |   where
155 |     go : List a -> s
156 |     go ls = set (partsOf l) ls x
157 |
158 | ||| Move downward through an indexed traversal. This will fail if the traversal
159 | ||| has no focuses.
160 | |||
161 | ||| If the traversal has multiple values, the zipper will focus on the leftmost one.
162 | export
163 | iwithin : Alternative f => IndexedTraversal' i s a -> Zipper hs j s -> f (Zipper (j @> s :: hs) i a)
164 | iwithin l (MkZipper coil p j y) =
165 |   case itoListOf l y of
166 |     (i,x) :: xs => pure $ MkZipper (Cons p j (go . map snd) coil) ([<], xs) i x
167 |     [] => empty
168 |   where
169 |     go : List a -> s
170 |     go ls = set (partsOf l) ls y
171 |
172 | ||| Move downward through a traversal. This will fail if the traversal has no
173 | ||| focuses.
174 | |||
175 | ||| If the traversal has multiple values, the zipper will focus on the leftmost one.
176 | export
177 | within : Alternative f => Traversal' s a -> Zipper hs j s -> f (Zipper (j @> s :: hs) Nat a)
178 | within = iwithin . iordinal
179 |
180 |
181 | recoil : Coil hs i a -> List (i, a) -> getTy $ last (i @> a :: hs)
182 | recoil Nil xs = assert_total $ case xs of (_,x) :: _ => x
183 | recoil (Cons p i f coil) xs = recoil coil $ fromPointer i (f xs) p
184 |
185 | ||| Close a zipper, repackaging it back into a value of its original type.
186 | export
187 | rezip : Zipper hs i a -> getTy $ last (i @> a :: hs)
188 | rezip (MkZipper coil p i x) = recoil coil $ fromPointer i x p
189 |