{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QualifiedDo #-}

-- | This module defines a 2-continuation flavour of indexed monads. Having two
-- continuation allows unrestricted backtracking (hence the 'Additive' instance
-- for 'Cont2W' below).
--
-- Most of this module is focused on using the indexed continuation monads for
-- delimited control, hence adopts its terminology. For instance in `'Cont2' w r
-- r'`, `r` and `r'` are called the input and output answer types respectively.
-- They are to be thought as a stack (a stack of `a -> b -> r` being a stack
-- whose two first elements are of type `a` and `b`).
--
-- 'Cont2W' is an indexed monad because the answer type can change along the
-- computation. This is called /answer-type modification/ in the delimited
-- control literature.
module Control.Monad.Indexed.Cont2
  ( -- * Abstract delimited control
    Shifty (..),
    Stacked (..),
    stack,
    pop,
    pop_,
    push,
    (@),

    -- * Comonad-to-indexed-monad transformer
    Cont2W (..),
    shift0,
    yield,
    yield_,

    -- * Bidirectional variants of traditional combinators
    some,
    many,
    optional,
    sepBy,
  )
where

import Control.Additive
import Control.Applicative qualified as Applicative
import Control.Comonad
import Control.Monad qualified as Monad
import Control.Monad.Indexed ((*>), (<*>))
import Control.Monad.Indexed qualified as Indexed
import Prelude hiding (Applicative (..), Monad (..), MonadFail (..))
import Prelude qualified

newtype Cont2W w r r' a = Cont2W {forall (w :: * -> *) r r' a.
Cont2W w r r' a -> w (a -> r' -> r') -> r -> r
runCont2W :: w (a -> r' -> r') -> r -> r}
  deriving stock ((forall a b. (a -> b) -> Cont2W w r r' a -> Cont2W w r r' b)
-> (forall a b. a -> Cont2W w r r' b -> Cont2W w r r' a)
-> Functor (Cont2W w r r')
forall a b. a -> Cont2W w r r' b -> Cont2W w r r' a
forall a b. (a -> b) -> Cont2W w r r' a -> Cont2W w r r' b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (w :: * -> *) r r' a b.
Functor w =>
a -> Cont2W w r r' b -> Cont2W w r r' a
forall (w :: * -> *) r r' a b.
Functor w =>
(a -> b) -> Cont2W w r r' a -> Cont2W w r r' b
$cfmap :: forall (w :: * -> *) r r' a b.
Functor w =>
(a -> b) -> Cont2W w r r' a -> Cont2W w r r' b
fmap :: forall a b. (a -> b) -> Cont2W w r r' a -> Cont2W w r r' b
$c<$ :: forall (w :: * -> *) r r' a b.
Functor w =>
a -> Cont2W w r r' b -> Cont2W w r r' a
<$ :: forall a b. a -> Cont2W w r r' b -> Cont2W w r r' a
Functor)

deriving via (Indexed.FromIndexed (Cont2W w) r r) instance (Comonad w) => Prelude.Applicative (Cont2W w r r)

deriving via (Indexed.FromIndexed (Cont2W w) r r) instance (Comonad w) => Prelude.Monad (Cont2W w r r)

deriving via (Indexed.FromIndexed (Cont2W w) r r) instance (Comonad w) => Applicative.Alternative (Cont2W w r r)

deriving via (Indexed.FromIndexed (Cont2W w) r r) instance (Comonad w) => Monad.MonadPlus (Cont2W w r r)

instance (Comonad w) => Indexed.Applicative (Cont2W w) where
  pure :: forall a i. a -> Cont2W w i i a
pure a
x = (w (a -> i -> i) -> i -> i) -> Cont2W w i i a
forall (w :: * -> *) r r' a.
(w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
Cont2W ((w (a -> i -> i) -> i -> i) -> Cont2W w i i a)
-> (w (a -> i -> i) -> i -> i) -> Cont2W w i i a
forall a b. (a -> b) -> a -> b
$ \w (a -> i -> i)
k -> w (a -> i -> i) -> a -> i -> i
forall a. w a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract w (a -> i -> i)
k a
x

instance (Comonad w) => Indexed.Monad (Cont2W w) where
  Cont2W w (a -> j -> j) -> i -> i
a >>= :: forall i j a k1 b.
Cont2W w i j a -> (a -> Cont2W w j k1 b) -> Cont2W w i k1 b
>>= a -> Cont2W w j k1 b
f = (w (b -> k1 -> k1) -> i -> i) -> Cont2W w i k1 b
forall (w :: * -> *) r r' a.
(w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
Cont2W ((w (b -> k1 -> k1) -> i -> i) -> Cont2W w i k1 b)
-> (w (b -> k1 -> k1) -> i -> i) -> Cont2W w i k1 b
forall a b. (a -> b) -> a -> b
$ \w (b -> k1 -> k1)
wk -> w (a -> j -> j) -> i -> i
a (w (b -> k1 -> k1) -> a -> j -> j
k' (w (b -> k1 -> k1) -> a -> j -> j)
-> w (b -> k1 -> k1) -> w (a -> j -> j)
forall a b. (w a -> b) -> w a -> w b
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
`extend` w (b -> k1 -> k1)
wk)
    where
      k' :: w (b -> k1 -> k1) -> a -> j -> j
k' w (b -> k1 -> k1)
wk a
x = Cont2W w j k1 b -> w (b -> k1 -> k1) -> j -> j
forall (w :: * -> *) r r' a.
Cont2W w r r' a -> w (a -> r' -> r') -> r -> r
runCont2W (a -> Cont2W w j k1 b
f a
x) w (b -> k1 -> k1)
wk

-- | 'shift0' is the most general delimited control operation on 'Cont2W'.
--
-- == __About the name__
-- It's named by analogy with the eponymous delimited control operation from the
-- delimited control literature (see [A Dynamic Interpretation of the CPS
-- Hierarchy](https://link.springer.com/chapter/10.1007/978-3-642-35182-2_21)).
-- The traditional @shift0@ captures all the continuations introduced by nested
-- resets; here we think of the comonad `w` as carrying the information of
-- additional resets.
shift0 :: (Comonad w) => (w (a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
shift0 :: forall (w :: * -> *) a r' r k.
Comonad w =>
(w (a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
shift0 w (a -> r' -> r') -> r -> Cont2W w r k k
f = (w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
forall (w :: * -> *) r r' a.
(w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
Cont2W ((w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a)
-> (w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
forall a b. (a -> b) -> a -> b
$ \w (a -> r' -> r')
wk r
fl -> Cont2W w r k k -> w (k -> k -> k) -> r -> r
forall (w :: * -> *) r r' a.
Cont2W w r r' a -> w (a -> r' -> r') -> r -> r
runCont2W (w (a -> r' -> r') -> r -> Cont2W w r k k
f w (a -> r' -> r')
wk r
fl) ((\a -> r' -> r'
_k k
x k
_ -> k
x) ((a -> r' -> r') -> k -> k -> k)
-> w (a -> r' -> r') -> w (k -> k -> k)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> w (a -> r' -> r')
wk) r
fl

-- | A type class abstracting over delimited control capability for this
-- 2-continuation flavour of monads.
class (Stacked m) => Shifty m where
  shift :: ((a -> r' -> r') -> r -> m r k k) -> m r r' a

instance (Comonad w) => Shifty (Cont2W w) where
  shift :: (Comonad w) => ((a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
  shift :: forall a r' r k.
Comonad w =>
((a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
shift (a -> r' -> r') -> r -> Cont2W w r k k
f = (w (a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
forall (w :: * -> *) a r' r k.
Comonad w =>
(w (a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
shift0 ((w (a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a)
-> (w (a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
forall a b. (a -> b) -> a -> b
$ \w (a -> r' -> r')
wk -> (a -> r' -> r') -> r -> Cont2W w r k k
f (w (a -> r' -> r') -> a -> r' -> r'
forall a. w a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract w (a -> r' -> r')
wk)

instance (Shifty f, Shifty g) => Shifty (f Indexed.:*: g) where
  shift :: forall a r' r k.
((a -> r' -> r') -> r -> (:*:) f g r k k) -> (:*:) f g r r' a
shift (a -> r' -> r') -> r -> (:*:) f g r k k
f = (((a -> r' -> r') -> r -> f r k k) -> f r r' a
forall a r' r k. ((a -> r' -> r') -> r -> f r k k) -> f r r' a
forall (m :: * -> * -> * -> *) a r' r k.
Shifty m =>
((a -> r' -> r') -> r -> m r k k) -> m r r' a
shift (\a -> r' -> r'
k r
fl -> (:*:) f g r k k -> f r k k
forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3 -> *)
       (g :: k1 -> k2 -> k3 -> *) (i :: k1) (j :: k2) (a :: k3).
(:*:) f g i j a -> f i j a
Indexed.fst_star ((a -> r' -> r') -> r -> (:*:) f g r k k
f a -> r' -> r'
k r
fl))) f r r' a -> g r r' a -> (:*:) f g r r' a
forall {k} {k1} {k2} (f :: k -> k1 -> k2 -> *)
       (g :: k -> k1 -> k2 -> *) (i :: k) (j :: k1) (a :: k2).
f i j a -> g i j a -> (:*:) f g i j a
Indexed.:*: (((a -> r' -> r') -> r -> g r k k) -> g r r' a
forall a r' r k. ((a -> r' -> r') -> r -> g r k k) -> g r r' a
forall (m :: * -> * -> * -> *) a r' r k.
Shifty m =>
((a -> r' -> r') -> r -> m r k k) -> m r r' a
shift (\a -> r' -> r'
k r
fl -> (:*:) f g r k k -> g r k k
forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3 -> *)
       (g :: k1 -> k2 -> k3 -> *) (i :: k1) (j :: k2) (a :: k3).
(:*:) f g i j a -> g i j a
Indexed.snd_star ((a -> r' -> r') -> r -> (:*:) f g r k k
f a -> r' -> r'
k r
fl)))

-- | 'pop' pops and returns the top element of the stack. See also the less
-- expressive 'pop_' which doesn't require a full 'Shifty' instance.
pop :: (Indexed.Applicative m, Shifty m) => m (a -> i) i a
pop :: forall (m :: * -> * -> * -> *) a i.
(Applicative m, Shifty m) =>
m (a -> i) i a
pop = ((a -> i -> i) -> (a -> i) -> m (a -> i) (a -> i) (a -> i))
-> m (a -> i) i a
forall a r' r k. ((a -> r' -> r') -> r -> m r k k) -> m r r' a
forall (m :: * -> * -> * -> *) a r' r k.
Shifty m =>
((a -> r' -> r') -> r -> m r k k) -> m r r' a
shift (((a -> i -> i) -> (a -> i) -> m (a -> i) (a -> i) (a -> i))
 -> m (a -> i) i a)
-> ((a -> i -> i) -> (a -> i) -> m (a -> i) (a -> i) (a -> i))
-> m (a -> i) i a
forall a b. (a -> b) -> a -> b
$ \a -> i -> i
k a -> i
fl -> (a -> i) -> m (a -> i) (a -> i) (a -> i)
forall a i. a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure (\a
a -> a -> i -> i
k a
a (a -> i
fl a
a))

-- | @'yield' act@ runs the comonadically effectful action @act@ in the 'Cont2W'
-- monad. See also 'yield_'.
yield :: (Comonad w) => (w (a -> r) -> r) -> Cont2W w r r a
yield :: forall (w :: * -> *) a r.
Comonad w =>
(w (a -> r) -> r) -> Cont2W w r r a
yield w (a -> r) -> r
act = (w (a -> r -> r) -> r -> Cont2W w r r r) -> Cont2W w r r a
forall (w :: * -> *) a r' r k.
Comonad w =>
(w (a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
shift0 ((w (a -> r -> r) -> r -> Cont2W w r r r) -> Cont2W w r r a)
-> (w (a -> r -> r) -> r -> Cont2W w r r r) -> Cont2W w r r a
forall a b. (a -> b) -> a -> b
$ \w (a -> r -> r)
wk r
fl -> r -> Cont2W w r r r
forall a i. a -> Cont2W w i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure (r -> Cont2W w r r r) -> r -> Cont2W w r r r
forall a b. (a -> b) -> a -> b
$ w (a -> r) -> r
act (((a -> r -> r) -> a -> r) -> w (a -> r -> r) -> w (a -> r)
forall a b. (a -> b) -> w a -> w b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a -> r -> r
k a
x -> a -> r -> r
k a
x r
fl) w (a -> r -> r)
wk)

-- | @'yield_' act@ runs the comonadically effectful action @act@ in the
-- 'Cont2W' monad. This is a variant of 'yield' specialised to the case where
-- the action doesn't return a value.
yield_ :: (Comonad w) => (w r -> r) -> Cont2W w r r ()
yield_ :: forall (w :: * -> *) r. Comonad w => (w r -> r) -> Cont2W w r r ()
yield_ w r -> r
act = (w (() -> r -> r) -> r -> Cont2W w r r r) -> Cont2W w r r ()
forall (w :: * -> *) a r' r k.
Comonad w =>
(w (a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
shift0 ((w (() -> r -> r) -> r -> Cont2W w r r r) -> Cont2W w r r ())
-> (w (() -> r -> r) -> r -> Cont2W w r r r) -> Cont2W w r r ()
forall a b. (a -> b) -> a -> b
$ \w (() -> r -> r)
wk r
fl -> r -> Cont2W w r r r
forall a i. a -> Cont2W w i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure (r -> Cont2W w r r r) -> r -> Cont2W w r r r
forall a b. (a -> b) -> a -> b
$ w r -> r
act (((() -> r -> r) -> r) -> w (() -> r -> r) -> w r
forall a b. (a -> b) -> w a -> w b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\() -> r -> r
k -> () -> r -> r
k () r
fl) w (() -> r -> r)
wk)

instance Additive (Cont2W w r r' a) where
  empty :: Cont2W w r r' a
empty = (w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
forall (w :: * -> *) r r' a.
(w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
Cont2W ((w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a)
-> (w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
forall a b. (a -> b) -> a -> b
$ \w (a -> r' -> r')
_ r
fl -> r
fl
  (Cont2W w (a -> r' -> r') -> r -> r
a) <|> :: Cont2W w r r' a -> Cont2W w r r' a -> Cont2W w r r' a
<|> (Cont2W w (a -> r' -> r') -> r -> r
b) = (w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
forall (w :: * -> *) r r' a.
(w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
Cont2W ((w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a)
-> (w (a -> r' -> r') -> r -> r) -> Cont2W w r r' a
forall a b. (a -> b) -> a -> b
$ \w (a -> r' -> r')
wk r
fl -> w (a -> r' -> r') -> r -> r
a w (a -> r' -> r')
wk (w (a -> r' -> r') -> r -> r
b w (a -> r' -> r')
wk r
fl)

instance (Comonad w) => Stacked (Cont2W w) where
  shift_ :: forall r' r r''.
((r' -> r') -> r -> Cont2W w r r'' r'') -> Cont2W w r r' ()
shift_ (r' -> r') -> r -> Cont2W w r r'' r''
f = ((() -> r' -> r') -> r -> Cont2W w r r'' r'') -> Cont2W w r r' ()
forall a r' r k.
((a -> r' -> r') -> r -> Cont2W w r k k) -> Cont2W w r r' a
forall (m :: * -> * -> * -> *) a r' r k.
Shifty m =>
((a -> r' -> r') -> r -> m r k k) -> m r r' a
shift (\() -> r' -> r'
k -> (r' -> r') -> r -> Cont2W w r r'' r''
f (() -> r' -> r'
k ()))

----------------------------------------------------------------------------------------
--
-- Stacked
--
----------------------------------------------------------------------------------------

-- | Restricted delimited control where continuations can be captured but can't
-- return values. This is enough for most stack-manipulating functions (the
-- stack, however, cannot influence the control flow anymore). Compared to
-- 'Shifty' it captures the additional case where the stack doesn't actually
-- exist at runtime ('Indexed.IgnoreIndices').
class Stacked m where
  shift_ :: ((r' -> r') -> r -> m r r'' r'') -> m r r' ()

instance (Stacked f, Stacked g) => Stacked (f Indexed.:*: g) where
  shift_ :: forall r' r r''.
((r' -> r') -> r -> (:*:) f g r r'' r'') -> (:*:) f g r r' ()
shift_ (r' -> r') -> r -> (:*:) f g r r'' r''
f = (((r' -> r') -> r -> f r r'' r'') -> f r r' ()
forall r' r r''. ((r' -> r') -> r -> f r r'' r'') -> f r r' ()
forall (m :: * -> * -> * -> *) r' r r''.
Stacked m =>
((r' -> r') -> r -> m r r'' r'') -> m r r' ()
shift_ (\r' -> r'
s r
fl' -> (:*:) f g r r'' r'' -> f r r'' r''
forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3 -> *)
       (g :: k1 -> k2 -> k3 -> *) (i :: k1) (j :: k2) (a :: k3).
(:*:) f g i j a -> f i j a
Indexed.fst_star ((r' -> r') -> r -> (:*:) f g r r'' r''
f r' -> r'
s r
fl'))) f r r' () -> g r r' () -> (:*:) f g r r' ()
forall {k} {k1} {k2} (f :: k -> k1 -> k2 -> *)
       (g :: k -> k1 -> k2 -> *) (i :: k) (j :: k1) (a :: k2).
f i j a -> g i j a -> (:*:) f g i j a
Indexed.:*: (((r' -> r') -> r -> g r r'' r'') -> g r r' ()
forall r' r r''. ((r' -> r') -> r -> g r r'' r'') -> g r r' ()
forall (m :: * -> * -> * -> *) r' r r''.
Stacked m =>
((r' -> r') -> r -> m r r'' r'') -> m r r' ()
shift_ (\r' -> r'
s r
fl' -> (:*:) f g r r'' r'' -> g r r'' r''
forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3 -> *)
       (g :: k1 -> k2 -> k3 -> *) (i :: k1) (j :: k2) (a :: k3).
(:*:) f g i j a -> g i j a
Indexed.snd_star ((r' -> r') -> r -> (:*:) f g r r'' r''
f r' -> r'
s r
fl')))

instance (Prelude.Applicative m) => Stacked (Indexed.IgnoreIndices m) where
  shift_ :: forall r' r r''.
((r' -> r') -> r -> IgnoreIndices m r r'' r'')
-> IgnoreIndices m r r' ()
shift_ (r' -> r') -> r -> IgnoreIndices m r r'' r''
_ = m () -> IgnoreIndices m r r' ()
forall {k} {k1} {k2} (m :: k -> *) (i :: k1) (j :: k2) (a :: k).
m a -> IgnoreIndices m i j a
Indexed.IgnoreIndices (m () -> IgnoreIndices m r r' ())
-> m () -> IgnoreIndices m r r' ()
forall a b. (a -> b) -> a -> b
$ () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
Prelude.pure ()

-- | 'stack' is a partial mapping operation on the stack.
--
-- In a first approximation it can be thought of as a function with type
--
-- > :: (j -> i) -> m i j ()
--
-- The direction of the arrow is explained by the representation of stack types
-- as function. A function with type
--
-- > ((d -> e -> r) -> (a -> b -> c -> r))
--
-- actually maps three elements @a, b, c@ to two elements @d, e@.
--
-- The additional parameter of type @i@ is a failure continuation. For instance
-- the following always fails to modify the stack:
--
-- > stack (\fl _ -> fl)
--
-- Finally, the extra function of type @(i -> j)@ is called an “unrolling
-- function” and is tasked with restoring the stack in its original state if a
-- later failure causes backtracking.
stack :: (Indexed.Applicative m, Stacked m) => (i -> j -> i) -> (i -> j) -> m i j ()
stack :: forall (m :: * -> * -> * -> *) i j.
(Applicative m, Stacked m) =>
(i -> j -> i) -> (i -> j) -> m i j ()
stack i -> j -> i
f i -> j
unr = ((j -> j) -> i -> m i i i) -> m i j ()
forall r' r r''. ((r' -> r') -> r -> m r r'' r'') -> m r r' ()
forall (m :: * -> * -> * -> *) r' r r''.
Stacked m =>
((r' -> r') -> r -> m r r'' r'') -> m r r' ()
shift_ (((j -> j) -> i -> m i i i) -> m i j ())
-> ((j -> j) -> i -> m i i i) -> m i j ()
forall a b. (a -> b) -> a -> b
$ \j -> j
k i
fl -> i -> m i i i
forall a i. a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure (i -> m i i i) -> i -> m i i i
forall a b. (a -> b) -> a -> b
$ i -> j -> i
f i
fl (j -> j
k (i -> j
unr i
fl))

(@) :: (Indexed.Applicative m, Stacked m) => m (a -> i) j b -> a -> m i j b
m (a -> i) j b
act @ :: forall (m :: * -> * -> * -> *) a i j b.
(Applicative m, Stacked m) =>
m (a -> i) j b -> a -> m i j b
@ a
a = a -> m i (a -> i) ()
forall (m :: * -> * -> * -> *) a i.
(Applicative m, Stacked m) =>
a -> m i (a -> i) ()
push a
a m i (a -> i) () -> m (a -> i) j b -> m i j b
forall i j a k1 b. m i j a -> m j k1 b -> m i k1 b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a (k1 :: k) b.
Applicative f =>
f i j a -> f j k1 b -> f i k1 b
*> m (a -> i) j b
act

infixl 9 @

push :: (Indexed.Applicative m, Stacked m) => a -> m i (a -> i) ()
push :: forall (m :: * -> * -> * -> *) a i.
(Applicative m, Stacked m) =>
a -> m i (a -> i) ()
push a
a = (((a -> i) -> a -> i) -> i -> m i i i) -> m i (a -> i) ()
forall r' r r''. ((r' -> r') -> r -> m r r'' r'') -> m r r' ()
forall (m :: * -> * -> * -> *) r' r r''.
Stacked m =>
((r' -> r') -> r -> m r r'' r'') -> m r r' ()
shift_ ((((a -> i) -> a -> i) -> i -> m i i i) -> m i (a -> i) ())
-> (((a -> i) -> a -> i) -> i -> m i i i) -> m i (a -> i) ()
forall a b. (a -> b) -> a -> b
$ \(a -> i) -> a -> i
k i
fl -> i -> m i i i
forall a i. a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure ((a -> i) -> a -> i
k (i -> a -> i
forall a b. a -> b -> a
const i
fl) a
a)

-- | 'pop_' discards the top element of the stack. It is a less expressive
-- variant of 'pop', but 'pop' requires a 'Shifty' applicative, whereas 'pop_'
-- works on any stacked applicative.
pop_ :: (Indexed.Applicative m, Stacked m) => m (a -> i) i ()
pop_ :: forall (m :: * -> * -> * -> *) a i.
(Applicative m, Stacked m) =>
m (a -> i) i ()
pop_ = ((i -> i) -> (a -> i) -> m (a -> i) (a -> i) (a -> i))
-> m (a -> i) i ()
forall r' r r''. ((r' -> r') -> r -> m r r'' r'') -> m r r' ()
forall (m :: * -> * -> * -> *) r' r r''.
Stacked m =>
((r' -> r') -> r -> m r r'' r'') -> m r r' ()
shift_ (((i -> i) -> (a -> i) -> m (a -> i) (a -> i) (a -> i))
 -> m (a -> i) i ())
-> ((i -> i) -> (a -> i) -> m (a -> i) (a -> i) (a -> i))
-> m (a -> i) i ()
forall a b. (a -> b) -> a -> b
$ \i -> i
k a -> i
fl -> (a -> i) -> m (a -> i) (a -> i) (a -> i)
forall a i. a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure (\a
a -> i -> i
k (a -> i
fl a
a))

-- | @'some' act@ iterates 1 or more times the action @act@ until it fails or
-- run out of input on the stack. See also 'many' which doesn't fail if it can't
-- iterate at least once.
some :: (Indexed.Alternative m, Stacked m) => (forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
some :: forall (m :: * -> * -> * -> *) a b r.
(Alternative m, Stacked m) =>
(forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
some forall r'. m (a -> r') r' b
a = Indexed.do
  (([a] -> r) -> (a -> [a] -> r) -> [a] -> r)
-> (([a] -> r) -> a -> [a] -> r) -> m ([a] -> r) (a -> [a] -> r) ()
forall (m :: * -> * -> * -> *) i j.
(Applicative m, Stacked m) =>
(i -> j -> i) -> (i -> j) -> m i j ()
stack ([a] -> r) -> (a -> [a] -> r) -> [a] -> r
forall {a} {t} {t}. ([a] -> t) -> (t -> [t] -> t) -> [t] -> t
uncons (\[a] -> r
k a
x [a]
xs -> [a] -> r
k (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs))
  (:) (b -> [b] -> [b])
-> m (a -> [a] -> r) ([a] -> r) b
-> m (a -> [a] -> r) ([a] -> r) ([b] -> [b])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (a -> [a] -> r) ([a] -> r) b
forall r'. m (a -> r') r' b
a m (a -> [a] -> r) ([a] -> r) ([b] -> [b])
-> m ([a] -> r) r [b] -> m (a -> [a] -> r) r [b]
forall i j a b k1. m i j (a -> b) -> m j k1 a -> m i k1 b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a b (k1 :: k).
Applicative f =>
f i j (a -> b) -> f j k1 a -> f i k1 b
<*> (forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
forall (m :: * -> * -> * -> *) a b r.
(Alternative m, Stacked m) =>
(forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
many m (a -> r') r' b
forall r'. m (a -> r') r' b
a
  where
    uncons :: ([a] -> t) -> (t -> [t] -> t) -> [t] -> t
uncons [a] -> t
fl t -> [t] -> t
_k [] = [a] -> t
fl []
    uncons [a] -> t
_fl t -> [t] -> t
k (t
x : [t]
xs) = t -> [t] -> t
k t
x [t]
xs

-- | @'many' act@ iterates 0 or more times the action @act@ until it fails or
-- run out of input on the stack. See also 'some' which iterates at least once.
many :: (Indexed.Alternative m, Stacked m) => (forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
many :: forall (m :: * -> * -> * -> *) a b r.
(Alternative m, Stacked m) =>
(forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
many forall r'. m (a -> r') r' b
a = (forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
forall (m :: * -> * -> * -> *) a b r.
(Alternative m, Stacked m) =>
(forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
some m (a -> r') r' b
forall r'. m (a -> r') r' b
a m ([a] -> r) r [b] -> m ([a] -> r) r [b] -> m ([a] -> r) r [b]
forall a. Additive a => a -> a -> a
<|> (m ([a] -> r) r ()
forall (m :: * -> * -> * -> *) a i.
(Applicative m, Stacked m) =>
m (a -> i) i ()
pop_ m ([a] -> r) r () -> m r r [b] -> m ([a] -> r) r [b]
forall i j a k1 b. m i j a -> m j k1 b -> m i k1 b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a (k1 :: k) b.
Applicative f =>
f i j a -> f j k1 b -> f i k1 b
*> [b] -> m r r [b]
forall a i. a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure [])

optional :: (Indexed.Alternative m, Stacked m) => (forall r'. m (a -> r') r' b) -> m (Maybe a -> r) r (Maybe b)
optional :: forall (m :: * -> * -> * -> *) a b r.
(Alternative m, Stacked m) =>
(forall r'. m (a -> r') r' b) -> m (Maybe a -> r) r (Maybe b)
optional forall r'. m (a -> r') r' b
a =
  (m (Maybe a -> r) (a -> r) (b -> Maybe b)
forall {t} {t} {a}. m (Maybe t -> t) (t -> t) (a -> Maybe a)
justLead m (Maybe a -> r) (a -> r) (b -> Maybe b)
-> m (a -> r) r b -> m (Maybe a -> r) r (Maybe b)
forall i j a b k1. m i j (a -> b) -> m j k1 a -> m i k1 b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a b (k1 :: k).
Applicative f =>
f i j (a -> b) -> f j k1 a -> f i k1 b
<*> m (a -> r) r b
forall r'. m (a -> r') r' b
a) m (Maybe a -> r) r (Maybe b)
-> m (Maybe a -> r) r (Maybe b) -> m (Maybe a -> r) r (Maybe b)
forall a. Additive a => a -> a -> a
<|> m (Maybe a -> r) r (Maybe b)
forall {a} {k2} {a}. m (Maybe a -> k2) k2 (Maybe a)
nothingLead
  where
    -- TODO: reorder module so that these can be derived.
    justLead :: m (Maybe t -> t) (t -> t) (a -> Maybe a)
justLead = Indexed.do
      ((Maybe t -> t) -> (t -> t) -> Maybe t -> t)
-> ((Maybe t -> t) -> t -> t) -> m (Maybe t -> t) (t -> t) ()
forall (m :: * -> * -> * -> *) i j.
(Applicative m, Stacked m) =>
(i -> j -> i) -> (i -> j) -> m i j ()
stack (\cases Maybe t -> t
_ t -> t
k (Just t
x) -> t -> t
k t
x; Maybe t -> t
fl t -> t
_ Maybe t
b -> Maybe t -> t
fl Maybe t
b) (\Maybe t -> t
k t
x -> Maybe t -> t
k (t -> Maybe t
forall a. a -> Maybe a
Just t
x))
      (a -> Maybe a) -> m (t -> t) (t -> t) (a -> Maybe a)
forall a i. a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure a -> Maybe a
forall a. a -> Maybe a
Just
    nothingLead :: m (Maybe a -> k2) k2 (Maybe a)
nothingLead = Indexed.do
      ((Maybe a -> k2) -> k2 -> Maybe a -> k2)
-> ((Maybe a -> k2) -> k2) -> m (Maybe a -> k2) k2 ()
forall (m :: * -> * -> * -> *) i j.
(Applicative m, Stacked m) =>
(i -> j -> i) -> (i -> j) -> m i j ()
stack (\cases Maybe a -> k2
_ k2
k Maybe a
Nothing -> k2
k; Maybe a -> k2
fl k2
_ Maybe a
b -> Maybe a -> k2
fl Maybe a
b) (\Maybe a -> k2
k -> Maybe a -> k2
k Maybe a
forall a. Maybe a
Nothing)
      Maybe a -> m k2 k2 (Maybe a)
forall a i. a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure Maybe a
forall a. Maybe a
Nothing

sepBy :: (Indexed.MonadPlus m, Stacked m) => (forall r'. m (a -> r') r' b) -> (forall r'. m r' r' ()) -> m ([a] -> r) r [b]
sepBy :: forall (m :: * -> * -> * -> *) a b r.
(MonadPlus m, Stacked m) =>
(forall r'. m (a -> r') r' b)
-> (forall r'. m r' r' ()) -> m ([a] -> r) r [b]
sepBy forall r'. m (a -> r') r' b
p forall r'. m r' r' ()
sep = Indexed.do
  -- TODO: I don't know whether cheating on the unroll can be a
  -- problem. Replacing by a direct call to shift would solve that I suppose.
  (([a] -> r) -> (Maybe a -> [a] -> r) -> [a] -> r)
-> (([a] -> r) -> Maybe a -> [a] -> r)
-> m ([a] -> r) (Maybe a -> [a] -> r) ()
forall (m :: * -> * -> * -> *) i j.
(Applicative m, Stacked m) =>
(i -> j -> i) -> (i -> j) -> m i j ()
stack (\cases [a] -> r
_ Maybe a -> [a] -> r
k (a
x : [a]
xs) -> Maybe a -> [a] -> r
k (a -> Maybe a
forall a. a -> Maybe a
Just a
x) [a]
xs; [a] -> r
_ Maybe a -> [a] -> r
k [] -> Maybe a -> [a] -> r
k Maybe a
forall a. Maybe a
Nothing ([Char] -> [a]
forall a. HasCallStack => [Char] -> a
error [Char]
"Why did this not pop?")) (\[a] -> r
k Maybe a
_x [a]
xs -> [a] -> r
k [a]
xs)
  Maybe b
r <- (forall r'. m (a -> r') r' b)
-> m (Maybe a -> [a] -> r) ([a] -> r) (Maybe b)
forall (m :: * -> * -> * -> *) a b r.
(Alternative m, Stacked m) =>
(forall r'. m (a -> r') r' b) -> m (Maybe a -> r) r (Maybe b)
optional m (a -> r') r' b
forall r'. m (a -> r') r' b
p
  case Maybe b
r of
    Maybe b
Nothing -> m ([a] -> r) r ()
forall (m :: * -> * -> * -> *) a i.
(Applicative m, Stacked m) =>
m (a -> i) i ()
pop_ m ([a] -> r) r () -> m r r [b] -> m ([a] -> r) r [b]
forall i j a k1 b. m i j a -> m j k1 b -> m i k1 b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a (k1 :: k) b.
Applicative f =>
f i j a -> f j k1 b -> f i k1 b
*> [b] -> m r r [b]
forall a i. a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
Indexed.pure []
    Just b
x -> Indexed.do
      (b
x :) ([b] -> [b]) -> m ([a] -> r) r [b] -> m ([a] -> r) r [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
forall (m :: * -> * -> * -> *) a b r.
(Alternative m, Stacked m) =>
(forall r'. m (a -> r') r' b) -> m ([a] -> r) r [b]
many (m (a -> r') (a -> r') ()
forall r'. m r' r' ()
sep m (a -> r') (a -> r') () -> m (a -> r') r' b -> m (a -> r') r' b
forall i j a k1 b. m i j a -> m j k1 b -> m i k1 b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a (k1 :: k) b.
Applicative f =>
f i j a -> f j k1 b -> f i k1 b
*> m (a -> r') r' b
forall r'. m (a -> r') r' b
p)