0 | module Control.Monad.Either.Extra
 1 |
 2 | import public Control.Monad.Error.Either
 3 | import Data.Vect
 4 |
 5 | %default total
 6 |
 7 | --------------------------------------------------------------------------------
 8 | --          List Traversal
 9 | --------------------------------------------------------------------------------
10 |
11 | implList_ : (t -> EitherT e IO ()) -> List t -> PrimIO (Either e ())
12 | implList_ f []        w = MkIORes (Right ()) w
13 | implList_ f (x :: xs) w =
14 |   let MkIORes (Right ()) w2 := toPrim (runEitherT (f x)) w
15 |         | MkIORes (Left err) w2 => MkIORes (Left err) w2
16 |    in implList_ f xs w2
17 |
18 | implList :
19 |      SnocList a
20 |   -> (t -> EitherT e IO a)
21 |   -> List t
22 |   -> PrimIO (Either e $ List a)
23 | implList sa f []        w = MkIORes (Right $ sa <>> []) w
24 | implList sa f (x :: xs) w =
25 |   let MkIORes (Right v) w2 := toPrim (runEitherT (f x)) w
26 |         | MkIORes (Left err) w2 => MkIORes (Left err) w2
27 |    in implList (sa :< v) f xs w2
28 |
29 | ||| Specialized, stack-safe list traversal.
30 | export
31 | traverseList_ : (t -> EitherT e IO ()) -> List t -> EitherT e IO ()
32 | traverseList_ f xs = MkEitherT $ fromPrim $ implList_ f xs
33 |
34 | ||| Specialized, stack-safe list traversal.
35 | export
36 | traverseList : (t -> EitherT e IO a) -> List t -> EitherT e IO (List a)
37 | traverseList f xs = MkEitherT $ fromPrim $ implList [<] f xs
38 |
39 | ||| Specialized, stack-safe list traversal.
40 | export %inline
41 | forList_ : List t -> (t -> EitherT e IO ()) -> EitherT e IO ()
42 | forList_ as f = traverseList_ f as
43 |
44 | ||| Specialized, stack-safe list traversal.
45 | export %inline
46 | forList : List t -> (t -> EitherT e IO a) -> EitherT e IO (List a)
47 | forList as f = traverseList f as
48 |
49 | --------------------------------------------------------------------------------
50 | --          SnocList Traversal
51 | --------------------------------------------------------------------------------
52 |
53 | implSnocList_ : (t -> EitherT e IO ()) -> SnocList t -> PrimIO (Either e ())
54 | implSnocList_ f [<]       w = MkIORes (Right ()) w
55 | implSnocList_ f (sx :< x) w =
56 |   let MkIORes (Right ()) w2 := toPrim (runEitherT (f x)) w
57 |         | MkIORes (Left err) w2 => MkIORes (Left err) w2
58 |    in implSnocList_ f sx w2
59 |
60 | implSnocList :
61 |      List a
62 |   -> (t -> EitherT e IO a)
63 |   -> SnocList t
64 |   -> PrimIO (Either e $ SnocList a)
65 | implSnocList as f [<]       w = MkIORes (Right $ [<] <>< as) w
66 | implSnocList as f (sx :< x) w =
67 |   let MkIORes (Right v) w2 := toPrim (runEitherT (f x)) w
68 |         | MkIORes (Left err) w2 => MkIORes (Left err) w2
69 |    in implSnocList (v::as) f sx w2
70 |
71 | ||| Specialized, stack-safe list traversal.
72 | export
73 | traverseSnocList_ : (t -> EitherT e IO ()) -> SnocList t -> EitherT e IO ()
74 | traverseSnocList_ f sx = MkEitherT $ fromPrim $ implSnocList_ f sx
75 |
76 | ||| Specialized, stack-safe list traversal.
77 | export
78 | traverseSnocList : (t -> EitherT e IO a) -> SnocList t -> EitherT e IO (SnocList a)
79 | traverseSnocList f sx = MkEitherT $ fromPrim $ implSnocList [] f sx
80 |
81 | ||| Specialized, stack-safe list traversal.
82 | export %inline
83 | forSnocList_ : SnocList t -> (t -> EitherT e IO ()) -> EitherT e IO ()
84 | forSnocList_ sa f = traverseSnocList_ f sa
85 |
86 | ||| Specialized, stack-safe list traversal.
87 | export %inline
88 | forSnocList : SnocList t -> (t -> EitherT e IO a) -> EitherT e IO (SnocList a)
89 | forSnocList sa f = traverseSnocList f sa
90 |