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
20 | foldr1 : (e -> a -> F1 s a) -> a -> f e -> F1 s a
22 | let fun # t := Traverse1.foldl1 (\g,el,t => (\x,t => let x2 # t := f el x t;
in g x2 t) # t) Token.(#) v t
25 | foldMap1 : Monoid m => (a -> F1 s m) -> f a -> F1 s m
27 | foldl1 (\m1,el,t => let m2 # t := f el t in (m1<+>m2) # t) neutral v t
29 | traverse1_ : (a -> F1' s) -> f a -> F1' s
30 | traverse1_ f v t = foldl1 (\_,el,t => f el t) () v t
34 | for1_ : Foldable1 f => f a -> (a -> F1' s) -> F1' s
35 | for1_ x f = traverse1_ f x
38 | Foldable1 Maybe where
39 | foldl1 f v Nothing t = v # t
40 | foldl1 f v (Just x) t = f v x t
42 | foldr1 f v Nothing t = v # t
43 | foldr1 f v (Just x) t = f x v t
45 | foldMap1 f Nothing t = neutral # t
46 | foldMap1 f (Just x) t = f x t
48 | traverse1_ f Nothing t = () # t
49 | traverse1_ f (Just v) t = f v t
52 | Foldable1 (Either e) where
53 | foldl1 f v (Left _) t = v # t
54 | foldl1 f v (Right x) t = f v x t
56 | foldr1 f v (Left _) t = v # t
57 | foldr1 f v (Right x) t = f x v t
59 | foldMap1 f (Left _) t = neutral # t
60 | foldMap1 f (Right x) t = f x t
62 | traverse1_ f (Left _) t = ()# t
63 | traverse1_ f (Right v) t = f v t
68 | foldl1List : (a -> e -> F1 s a) -> a -> List e -> F1 s a
69 | foldl1List f v [] t = v # t
70 | foldl1List f v (x :: xs) t = let v2 # t1 := f v x t in foldl1List f v2 xs t1
73 | foldr1SnocList : (e -> a -> F1 s a) -> a -> SnocList e -> F1 s a
74 | foldr1SnocList f v [<] t = v # t
75 | foldr1SnocList f v (sx :< x) t = let v2 # t1 := f x v t in foldr1SnocList f v2 sx t1
78 | foldr1List : (e -> a -> F1 s a) -> a -> List e -> F1 s a
79 | foldr1List f v xs = foldr1SnocList f v ([<] <>< xs)
82 | foldl1SnocList : (a -> e -> F1 s a) -> a -> SnocList e -> F1 s a
83 | foldl1SnocList f v sx = foldl1List f v (sx <>> [])
86 | foldMap1List : Monoid m => (a -> F1 s m) -> List a -> F1 s m
87 | foldMap1List f = go neutral
89 | go : m -> List a -> F1 s m
91 | go v (x :: xs) t = let w # t1 := f x t in go (v <+> w) xs t1
94 | foldMap1SnocList : Monoid m => (a -> F1 s m) -> SnocList a -> F1 s m
95 | foldMap1SnocList f = go neutral
97 | go : m -> SnocList a -> F1 s m
99 | go v (sx :< x) t = let w # t1 := f x t in go (w <+> v) sx t1
102 | traverse1_List : (a -> F1' s) -> List a -> F1' s
103 | traverse1_List f [] t = () # t
104 | traverse1_List f (x :: xs) t = let _ # t := f x t in traverse1_List f xs t
107 | traverse1_SnocList : (a -> F1' s) -> SnocList a -> F1' s
108 | traverse1_SnocList f [<] t = () # t
109 | traverse1_SnocList f (sx :< x) t = let _ # t := f x t in traverse1_SnocList f sx t
112 | Foldable1 List where
113 | foldl1 = foldl1List
114 | foldr1 = foldr1List
115 | foldMap1 = foldMap1List
116 | traverse1_ = traverse1_List
119 | Foldable1 SnocList where
120 | foldl1 = foldl1SnocList
121 | foldr1 = foldr1SnocList
122 | foldMap1 = foldMap1SnocList
123 | traverse1_ = traverse1_SnocList
126 | foldl1Vect : (a -> e -> F1 s a) -> a -> Vect n e -> F1 s a
127 | foldl1Vect f v [] t = v # t
128 | foldl1Vect f v (x :: xs) t = let v2 # t1 := f v x t in foldl1Vect f v2 xs t1
130 | ontoSnocList : SnocList a -> Vect n a -> SnocList a
131 | ontoSnocList sx [] = sx
132 | ontoSnocList sx (x::xs) = ontoSnocList (sx :< x) xs
135 | foldr1Vect : (e -> a -> F1 s a) -> a -> Vect n e -> F1 s a
136 | foldr1Vect f v xs = foldr1SnocList f v (ontoSnocList [<] xs)
139 | foldMap1Vect : Monoid m => (a -> F1 s m) -> Vect n a -> F1 s m
140 | foldMap1Vect f = go neutral
142 | go : m -> Vect k a -> F1 s m
144 | go v (x :: xs) t = let w # t1 := f x t in go (v <+> w) xs t1
147 | traverse1_Vect : (a -> F1' s) -> Vect n a -> F1' s
148 | traverse1_Vect f [] t = () # t
149 | traverse1_Vect f (x :: xs) t = let _ # t := f x t in traverse1_Vect f xs t
152 | Foldable1 (Vect n) where
153 | foldl1 = foldl1Vect
154 | foldr1 = foldr1Vect
155 | foldMap1 = foldMap1Vect
156 | traverse1_ = traverse1_Vect
159 | Foldable1 List1 where
160 | foldl1 f v = foldl1List f v . forget
161 | foldr1 f v = foldr1List f v . forget
162 | foldMap1 f = foldMap1List f . forget
163 | traverse1_ f = traverse1_List f . forget
170 | interface Foldable1 f => Traversable1 f where
171 | traverse1 : (a -> F1 s b) -> f a -> F1 s (f b)
174 | Traversable1 Maybe where
175 | traverse1 f Nothing t = Nothing # t
176 | traverse1 f (Just v) t = let w # t1 := f v t in Just w # t1
179 | Traversable1 (Either e) where
180 | traverse1 f (Left v) t = Left v # t
181 | traverse1 f (Right v) t = let w # t1 := f v t in Right w # t1
184 | traverse1List : SnocList b -> (a -> F1 s b) -> List a -> F1 s (List b)
185 | traverse1List sx f [] t = (sx <>> []) # t
186 | traverse1List sx f (x :: xs) t =
187 | let v # t1 := f x t
188 | in traverse1List (sx :< v) f xs t1
191 | traverse1SnocList : List b -> (a -> F1 s b) -> SnocList a -> F1 s (SnocList b)
192 | traverse1SnocList xs f [<] t = ([<] <>< xs) # t
193 | traverse1SnocList xs f (sx :< x) t =
194 | let v # t1 := f x t
195 | in traverse1SnocList (v::xs) f sx t1
197 | ontoVect : (sx : SnocList a) -> Vect n a -> Vect (length sx + n) a
198 | ontoVect [<] xs = xs
199 | ontoVect (sx :< x) xs =
200 | rewrite plusSuccRightSucc (length sx) n in ontoVect sx (x::xs)
207 | -> F1 s (Vect (length sx + n) b)
208 | traverse1Vect sx f [] t = ontoVect sx [] # t
209 | traverse1Vect {n = S k} sx f (x :: xs) t =
210 | let Token.(#) v t1 := f x t
211 | in rewrite sym (plusSuccRightSucc (length sx) k)
212 | in traverse1Vect (sx :< v) f xs t1
215 | Traversable1 List where
216 | traverse1 = traverse1List [<]
219 | Traversable1 SnocList where
220 | traverse1 = traverse1SnocList []
223 | Traversable1 (Vect n) where
224 | traverse1 = traverse1Vect [<]
227 | Traversable1 List1 where
228 | traverse1 f (x:::xs) t =
229 | let w # t1 := f x t
230 | wx # t2 := traverse1 f xs t1
235 | for1 : Traversable1 f => f a -> (a -> F1 s b) -> F1 s (f b)
236 | for1 x f = traverse1 f x
242 | pairIx : (r : Ref s Nat) -> a -> F1 s (Nat,a)
243 | pairIx r v t = mapR1 (,v) (readAndMod1 r S t)
247 | zipWithIndex : Traversable1 f => f a -> f (Nat,a)
248 | zipWithIndex as = withRef1 Z $
\r => (traverse1 (pairIx r) as)