0 | module Data.Linear.Traverse1
5 | import Data.Linear.Ref1
6 | import public Data.Linear.Token
17 | interface Foldable1 (0 f : Type -> Type) where
18 | foldl1 : (a -> e -> F1 s a) -> a -> f e -> F1 s a
19 | foldr1 : (e -> a -> F1 s a) -> a -> f e -> F1 s a
20 | foldMap1 : Monoid m => (a -> F1 s m) -> f a -> F1 s m
21 | traverse1_ : (a -> F1' s) -> f a -> F1' s
25 | for1_ : Foldable1 f => f a -> (a -> F1' s) -> F1' s
26 | for1_ x f = traverse1_ f x
29 | Foldable1 Maybe where
30 | foldl1 f v Nothing t = v # t
31 | foldl1 f v (Just x) t = f v x t
33 | foldr1 f v Nothing t = v # t
34 | foldr1 f v (Just x) t = f x v t
36 | foldMap1 f Nothing t = neutral # t
37 | foldMap1 f (Just x) t = f x t
39 | traverse1_ f Nothing t = () # t
40 | traverse1_ f (Just v) t = f v t
43 | Foldable1 (Either e) where
44 | foldl1 f v (Left _) t = v # t
45 | foldl1 f v (Right x) t = f v x t
47 | foldr1 f v (Left _) t = v # t
48 | foldr1 f v (Right x) t = f x v t
50 | foldMap1 f (Left _) t = neutral # t
51 | foldMap1 f (Right x) t = f x t
53 | traverse1_ f (Left _) t = ()# t
54 | traverse1_ f (Right v) t = f v t
59 | foldl1List : (a -> e -> F1 s a) -> a -> List e -> F1 s a
60 | foldl1List f v [] t = v # t
61 | foldl1List f v (x :: xs) t = let v2 # t1 := f v x t in foldl1List f v2 xs t1
64 | foldr1SnocList : (e -> a -> F1 s a) -> a -> SnocList e -> F1 s a
65 | foldr1SnocList f v [<] t = v # t
66 | foldr1SnocList f v (sx :< x) t = let v2 # t1 := f x v t in foldr1SnocList f v2 sx t1
69 | foldr1List : (e -> a -> F1 s a) -> a -> List e -> F1 s a
70 | foldr1List f v xs = foldr1SnocList f v ([<] <>< xs)
73 | foldl1SnocList : (a -> e -> F1 s a) -> a -> SnocList e -> F1 s a
74 | foldl1SnocList f v sx = foldl1List f v (sx <>> [])
77 | foldMap1List : Monoid m => (a -> F1 s m) -> List a -> F1 s m
78 | foldMap1List f = go neutral
80 | go : m -> List a -> F1 s m
82 | go v (x :: xs) t = let w # t1 := f x t in go (v <+> w) xs t1
85 | foldMap1SnocList : Monoid m => (a -> F1 s m) -> SnocList a -> F1 s m
86 | foldMap1SnocList f = go neutral
88 | go : m -> SnocList a -> F1 s m
90 | go v (sx :< x) t = let w # t1 := f x t in go (w <+> v) sx t1
93 | traverse1_List : (a -> F1' s) -> List a -> F1' s
94 | traverse1_List f [] t = () # t
95 | traverse1_List f (x :: xs) t = let _ # t := f x t in traverse1_List f xs t
98 | traverse1_SnocList : (a -> F1' s) -> SnocList a -> F1' s
99 | traverse1_SnocList f [<] t = () # t
100 | traverse1_SnocList f (sx :< x) t = let _ # t := f x t in traverse1_SnocList f sx t
103 | Foldable1 List where
104 | foldl1 = foldl1List
105 | foldr1 = foldr1List
106 | foldMap1 = foldMap1List
107 | traverse1_ = traverse1_List
110 | Foldable1 SnocList where
111 | foldl1 = foldl1SnocList
112 | foldr1 = foldr1SnocList
113 | foldMap1 = foldMap1SnocList
114 | traverse1_ = traverse1_SnocList
117 | foldl1Vect : (a -> e -> F1 s a) -> a -> Vect n e -> F1 s a
118 | foldl1Vect f v [] t = v # t
119 | foldl1Vect f v (x :: xs) t = let v2 # t1 := f v x t in foldl1Vect f v2 xs t1
121 | ontoSnocList : SnocList a -> Vect n a -> SnocList a
122 | ontoSnocList sx [] = sx
123 | ontoSnocList sx (x::xs) = ontoSnocList (sx :< x) xs
126 | foldr1Vect : (e -> a -> F1 s a) -> a -> Vect n e -> F1 s a
127 | foldr1Vect f v xs = foldr1SnocList f v (ontoSnocList [<] xs)
130 | foldMap1Vect : Monoid m => (a -> F1 s m) -> Vect n a -> F1 s m
131 | foldMap1Vect f = go neutral
133 | go : m -> Vect k a -> F1 s m
135 | go v (x :: xs) t = let w # t1 := f x t in go (v <+> w) xs t1
138 | traverse1_Vect : (a -> F1' s) -> Vect n a -> F1' s
139 | traverse1_Vect f [] t = () # t
140 | traverse1_Vect f (x :: xs) t = let _ # t := f x t in traverse1_Vect f xs t
143 | Foldable1 (Vect n) where
144 | foldl1 = foldl1Vect
145 | foldr1 = foldr1Vect
146 | foldMap1 = foldMap1Vect
147 | traverse1_ = traverse1_Vect
150 | Foldable1 List1 where
151 | foldl1 f v = foldl1List f v . forget
152 | foldr1 f v = foldr1List f v . forget
153 | foldMap1 f = foldMap1List f . forget
154 | traverse1_ f = traverse1_List f . forget
161 | interface Foldable1 f => Traversable1 f where
162 | traverse1 : (a -> F1 s b) -> f a -> F1 s (f b)
165 | Traversable1 Maybe where
166 | traverse1 f Nothing t = Nothing # t
167 | traverse1 f (Just v) t = let w # t1 := f v t in Just w # t1
170 | Traversable1 (Either e) where
171 | traverse1 f (Left v) t = Left v # t
172 | traverse1 f (Right v) t = let w # t1 := f v t in Right w # t1
175 | traverse1List : SnocList b -> (a -> F1 s b) -> List a -> F1 s (List b)
176 | traverse1List sx f [] t = (sx <>> []) # t
177 | traverse1List sx f (x :: xs) t =
178 | let v # t1 := f x t
179 | in traverse1List (sx :< v) f xs t1
182 | traverse1SnocList : List b -> (a -> F1 s b) -> SnocList a -> F1 s (SnocList b)
183 | traverse1SnocList xs f [<] t = ([<] <>< xs) # t
184 | traverse1SnocList xs f (sx :< x) t =
185 | let v # t1 := f x t
186 | in traverse1SnocList (v::xs) f sx t1
188 | ontoVect : (sx : SnocList a) -> Vect n a -> Vect (length sx + n) a
189 | ontoVect [<] xs = xs
190 | ontoVect (sx :< x) xs =
191 | rewrite plusSuccRightSucc (length sx) n in ontoVect sx (x::xs)
198 | -> F1 s (Vect (length sx + n) b)
199 | traverse1Vect sx f [] t = ontoVect sx [] # t
200 | traverse1Vect {n = S k} sx f (x :: xs) t =
201 | let Token.(#) v t1 := f x t
202 | in rewrite sym (plusSuccRightSucc (length sx) k)
203 | in traverse1Vect (sx :< v) f xs t1
206 | Traversable1 List where
207 | traverse1 = traverse1List [<]
210 | Traversable1 SnocList where
211 | traverse1 = traverse1SnocList []
214 | Traversable1 (Vect n) where
215 | traverse1 = traverse1Vect [<]
218 | Traversable1 List1 where
219 | traverse1 f (x:::xs) t =
220 | let w # t1 := f x t
221 | wx # t2 := traverse1 f xs t1
226 | for1 : Traversable1 f => f a -> (a -> F1 s b) -> F1 s (f b)
227 | for1 x f = traverse1 f x
233 | pairIx : (r : Ref s Nat) -> a -> F1 s (Nat,a)
234 | pairIx r v t = mapR1 (,v) (readAndMod1 r S t)
238 | zipWithIndex : Traversable1 f => f a -> f (Nat,a)
239 | zipWithIndex as = withRef1 Z $
\r => (traverse1 (pairIx r) as)