@@ -0,0 +1,160 @@
1+||| A Zipper implementation for Lists
2+||| inspired by
3+||| https://hackage.haskell.org/package/ListZipper-1.2.0.2/docs/src/Data-List-Zipper.html
4+module Data.List.Zipper
5+
6+%default total
7+%access public export
8+
9+||| A Zipper for Lists
10+data Zipper: Type -> Type where
11+ Zip: List a -> List a -> Zipper a
12+
13+%name Zipper z1, z2
14+
15+-- Implementations
16+--------------------------------------------------------------------------------
17+
18+Functor Zipper where
19+ map f (Zip xs ys) = Zip (map f xs) (map f ys)
20+
21+Foldable Zipper where
22+ foldr f acc (Zip xs ys) = foldr f acc (reverse xs ++ ys)
23+
24+Show a => Show (Zipper a) where
25+ show (Zip xs []) = show $ reverse xs
26+ show (Zip xs (x :: ys)) = unwords [show $ reverse xs, "-", show x, "-", show ys]
27+
28+||| Equality for Zippers
29+||| Two zipper are equal if they zip the same list and point to the same cursor
30+Eq a => Eq (Zipper a) where
31+ (==) (Zip xs ys) (Zip zs ws) = (xs == zs) && (ys == ws)
32+-- Functions
33+--------------------------------------------------------------------------------
34+
35+||| creates an empty Zipper
36+||| ```idris example
37+||| empty {a = Nat}
38+||| ```
39+empty: Zipper a
40+empty = Zip [] []
41+
42+||| checks whether this Zipper is empty
43+||| ```idris example
44+||| isEmpty empty {a = Nat}
45+||| ```
46+isEmpty: Zipper a -> Bool
47+isEmpty (Zip [] []) = True
48+isEmpty _ = False
49+
50+||| creates a Zipper from a List
51+||| ```idris example
52+||| show $ fromList [1,2,3,4,5]
53+||| ```
54+fromList: List a -> Zipper a
55+fromList xs = Zip [] xs
56+
57+||| moves the cursor to the right or leaves the cursor unchanged
58+||| ```idris example
59+||| show $ right $ fromList [1,2,3,4,5]
60+||| ```
61+right: Zipper a -> Zipper a
62+right (Zip xs (x :: ys)) = Zip (x :: xs) ys
63+right z = z
64+
65+||| moves the cursor to the left or leaves the cursor unchanged
66+||| ```idris example
67+||| show $ left $ fromList [1,2,3,4,5]
68+||| ```
69+left: Zipper a -> Zipper a
70+left (Zip (x :: xs) ys) = Zip xs (x :: ys)
71+left z = z
72+
73+||| gets the element at the current cursor
74+||| ```idris example
75+||| cursor $ fromList [1,2,3,4,5]
76+||| ```
77+cursor: Zipper a -> Maybe a
78+cursor (Zip xs ys) = listToMaybe ys
79+
80+||| move the cursor to the start of the Zipper
81+||| ```idris example
82+||| show $ start $ fromList [1,2,3,4,5]
83+||| ```
84+start: Zipper a -> Zipper a
85+start (Zip xs ys) = Zip [] (reverse xs ++ ys)
86+
87+||| move the cursor to the end of the Zipper
88+||| ```idris example
89+||| show $ end $ fromList [1,2,3,4,5]
90+||| ```
91+end: Zipper a -> Zipper a
92+end (Zip xs ys) = Zip (reverse ys ++ xs) []
93+
94+||| checks whether the cursor is at the start of the Zipper
95+||| ```idris example
96+||| startp $ fromList [1,2,3,4,5]
97+||| ```
98+startp: Zipper a -> Bool
99+startp (Zip [] ys) = True
100+startp _ = False
101+
102+||| checks whether the cursor is at the end of the Zipper
103+||| ```idris example
104+||| endp $ fromList [1,2,3,4,5]
105+||| ```
106+endp: Zipper a -> Bool
107+endp (Zip xs []) = True
108+endp _ = False
109+
110+||| inserts an element at the current cursor
111+||| ```idris example
112+||| show $ insert 0 $ fromList [1,2,3,4,5]
113+||| ```
114+insert: a -> Zipper a -> Zipper a
115+insert x (Zip xs ys) = Zip xs (x :: ys)
116+
117+||| push an element into the Zipper and move the cursor past it
118+||| ```idris example
119+||| show $ push 0 $ fromList [1,2,3,4,5]
120+||| ```
121+push: a -> Zipper a -> Zipper a
122+push x (Zip xs ys) = Zip (x :: xs) (ys)
123+
124+||| pop an element from the Zipper
125+||| ```idris example
126+||| show $ pop $ right $ fromList [1,2,3,4,5]
127+||| ```
128+pop: Zipper a -> Zipper a
129+pop (Zip (_ :: xs) ys) = Zip xs ys
130+pop z = z
131+
132+||| delete the element at the current cursor
133+||| ```idris example
134+||| show $ Data.List.Zipper.delete $ fromList [1,2,3,4,5]
135+||| ```
136+delete: Zipper a -> Zipper a
137+delete (Zip xs (x :: ys)) = Zip xs ys
138+delete z = z
139+
140+||| remove an element from the zipper
141+||| ```idris example
142+||| show $ replace 9 $ fromList[1,2,3,4,5]
143+||| ```
144+replace: a -> Zipper a -> Zipper a
145+replace x (Zip xs (_ :: ys)) = Zip xs (x :: ys)
146+replace _ z1 = z1
147+
148+||| Return the index of the current cursor
149+||| ```idris example
150+||| index $ fromList [1,2,3,4,5]
151+||| ```
152+index: Zipper a -> Nat
153+index (Zip xs ys) = length xs
154+
155+||| convert this Zipper to a list
156+||| ```idris example
157+||| toList $ fromList[1,2,3,4,5]
158+||| ```
159+toList: Zipper a -> List a
160+toList (Zip xs ys) = reverse xs ++ ys