[ new ] Batch of conjunction-related combinators

src/Combinators.idr

@@ -31,6 +31,14 @@ guardM : (Alternative mn, Monad mn) =>
 guardM f p = MkParser (\ mlen, ts => runParser p mlen ts >>= \ s =>
                        choiceMap pure (Success.guardM f s))
 
+guard : (Alternative mn, Monad mn) =>
+        (a -> Bool) -> All (Parser toks tok mn a :-> Parser toks tok mn a)
+guard p = guardM (\ v => if p v then Just v else Nothing)
+
+maybeTok : (Inspect toks tok, Alternative mn, Monad mn) =>
+           (tok -> Maybe a) -> All (Parser toks tok mn a)
+maybeTok p = guardM p anyTok
+
 map : Functor mn =>
       (a -> b) -> All (Parser toks tok mn a :-> Parser toks tok mn b)
 map f p = MkParser (\ le, ts => Functor.map (Success.map f) (runParser p le ts))
@@ -48,4 +56,90 @@ alt p q = MkParser (\ mlen, ts => runParser p mlen ts <|> runParser q mlen ts)
 
 alts : Alternative mn =>
        All (List :. Parser toks tok mn a :-> Parser toks tok mn a)
-alts = foldr (\ p, q => alt p q) fail
+alts = foldr alt fail
+
+andmbind : (Monad mn, Alternative mn) =>
+           All (Parser toks tok mn a :-> (Cst a :-> Box (Parser toks tok mn b)) :->
+                Parser toks tok mn (Pair a (Maybe b)))
+andmbind p q = MkParser (\ mlen, ts =>
+               runParser p mlen ts >>= \ sa =>
+               let salen   = lteTransitive (Small sa) mlen in
+               let combine = Success.map (Functor.map Just) . (Success.and sa) in
+               (Functor.map combine (runParser (call (q (Value sa)) salen) lteRefl (Leftovers sa)))
+               <|> pure (Success.map (flip MkPair Nothing) sa))
+
+andbind : Monad mn =>
+           All (Parser toks tok mn a :-> (Cst a :-> Box (Parser toks tok mn b)) :->
+                Parser toks tok mn (Pair a b))
+andbind p q = MkParser (\ mlen, ts =>
+              runParser p mlen ts >>= \ sa =>
+              let salen  = lteTransitive (Small sa) mlen in
+              let adjust = Functor.map (Success.and sa) in
+              adjust (runParser (call (q (Value sa)) salen) lteRefl (Leftovers sa)))
+
+and : Monad mn =>
+      All (Parser toks tok mn a :-> Box (Parser toks tok mn b) :-> Parser toks tok mn (Pair a b))
+and p q = andbind p (\ _ => q)
+
+andm : (Monad mn, Alternative mn) =>
+       All (Parser toks tok mn a :-> Box (Parser toks tok mn b) :->
+       Parser toks tok mn (Pair a (Maybe b)))
+andm p q = andmbind p (\ _ => q)
+
+mand : (Monad mn, Alternative mn) =>
+       All (Parser toks tok mn a :-> Parser toks tok mn b :-> Parser toks tok mn (Pair (Maybe a) b))
+mand p q = alt (and (map Just p) q) (map (MkPair Nothing) q)
+
+bind : Monad mn =>
+       All (Parser toks tok mn a :-> (Cst a :-> Box (Parser toks tok mn b)) :-> Parser toks tok mn b)
+bind p q = map snd (andbind p q)
+
+land : (Monad mn, Alternative mn) =>
+       All (Parser toks tok mn a :-> Box (Parser toks tok mn b) :-> Parser toks tok mn a)
+land p q = map fst (and p q)
+
+rand : (Monad mn, Alternative mn) =>
+       All (Parser toks tok mn a :-> Box (Parser toks tok mn b) :-> Parser toks tok mn b)
+rand p q = map snd (and p q)
+
+landm : (Monad mn, Alternative mn) =>
+        All (Parser toks tok mn a :-> Box (Parser toks tok mn b) :-> Parser toks tok mn a)
+landm p q = map fst (andm p q)
+
+randm : (Monad mn, Alternative mn) =>
+        All (Parser toks tok mn a :-> Box (Parser toks tok mn b) :-> Parser toks tok mn (Maybe b))
+randm p q = map snd (andm p q)
+
+lmand : (Monad mn, Alternative mn) =>
+        All (Parser toks tok mn a :-> Parser toks tok mn b :-> Parser toks tok mn (Maybe a))
+lmand p q = map fst (mand p q)
+
+rmand : (Monad mn, Alternative mn) =>
+        All (Parser toks tok mn a :-> Parser toks tok mn b :-> Parser toks tok mn b)
+rmand p q = map snd (mand p q)
+
+sum : (Alternative mn) =>
+      All (Parser toks tok mn a :-> Parser toks tok mn b :-> Parser toks tok mn (Either a b))
+sum p q = alt (map Left p) (map Right q)
+
+app : Monad mn =>
+      All (Parser toks tok mn (a -> b) :-> Box (Parser toks tok mn a) :-> Parser toks tok mn b)
+app p q = bind p (\ f => Box.map (map f) q)
+
+exact : (Inspect toks tok, DecEq tok, Monad mn, Alternative mn) =>
+        tok -> All (Parser toks tok mn tok)
+exact t = guard (\ t' => decAsBool (decEq t t')) anyTok
+
+anyOf : (Inspect toks tok, DecEq tok, Monad mn, Alternative mn) =>
+        List tok -> All (Parser toks tok mn tok)
+anyOf ts = alts (map (\ t => exact t) ts)
+
+between : (Monad mn, Alternative mn) =>
+          All (Parser toks tok mn a :-> Box (Parser toks tok mn c) :->
+          Box (Parser toks tok mn b) :-> Parser toks tok mn b)
+between open close p = land (rand open p) close
+
+betweenm : (Monad mn, Alternative mn) =>
+           All (Parser toks tok mn a :-> Box (Parser toks tok mn c) :->
+           Parser toks tok mn b :-> Parser toks tok mn b)
+betweenm open close p = landm (rmand open p) close

src/Indexed.idr

@@ -23,5 +23,8 @@ infixr 4 :.
 (:.) : (t : Type -> Type) -> (a : i -> Type) -> (i -> Type)
 (:.) t a i = t (a i)
 
+Cst : Type -> (i -> Type)
+Cst t i = t
+
 All : (a : i -> Type) -> Type
 All {i} a = {i : i} -> a i

src/Success.idr

@@ -27,7 +27,7 @@ ltLift p = lteLift (lteSuccLeft p)
 
 and : (p : Success toks tok a n) -> Success toks tok b (Size p) ->
       Success toks tok (Pair a b) n
-and p (MkSuccess q s lt ts) = ltLift (Small p) (MkSuccess (Value p, q) s lt ts)
+and p q = ltLift (Small p) (map (MkPair (Value p)) q)
 
 fromView : All (View toks tok :-> Success toks tok tok)
 fromView = go _ where