-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Session types library
--   
--   This packages provides a deep embedded domain-specific language for
--   writing session typed program. A session typed program is a program
--   annotated with session types. A session type describes a communication
--   protocol at the type-level. The motivation for doing so is that it
--   gives you a static guarantee that a program correctly implements a
--   protocol. It may even guarantee that no deadlocking can occur.
@package sessiontypes
@version 0.1.0


-- | This module provides a collection of types and type families.
--   
--   Specifically it defines the session type data type, capability data
--   type and type families that compute using session types or
--   capabilities as arguments.
module Control.SessionTypes.Types

-- | The session type data type
--   
--   Each constructor denotes a specific session type. Using the
--   <tt>DataKinds</tt> pragma the constructors are promoted to types and
--   <a>ST</a> is promoted to a kind.
data ST a

-- | Send a value
(:?>) :: a -> (ST a) -> ST a

-- | Recv a value
(:!>) :: a -> (ST a) -> ST a

-- | Selection of branches
Sel :: [ST a] -> ST a

-- | Offering of branches
Off :: [ST a] -> ST a

-- | Delimit the scope of recursion
R :: (ST a) -> ST a

-- | Weaken the scope of recursion
Wk :: (ST a) -> ST a

-- | Recursion variable
V :: ST a

-- | End of the session
Eps :: ST a

-- | A capability that stores a context/scope that is a list of session
--   types and a session type
data Cap a
Cap :: [ST a] -> (ST a) -> Cap a

-- | Retrieves the session type from the capability

-- | Retrieves the context from the capability

-- | Type family for calculating the dual of a session type. It may be
--   applied to a capability.
--   
--   We made <a>Dual</a> injective to support calculating the dual of a
--   selection that contains an ambiguous branch. Of course that does
--   require that the dual of that ambiguous branch must be known.

-- | Type family for calculating the dual of a session type. It may be
--   applied to the actual session type.

-- | Type family for calculating the dual of a list of session types.

-- | Type family for removing the send session type from the given session
--   type. It may be applied to a capability.

-- | Type family for removing the send session type from the given session
--   type. It may be applied to a session type.

-- | Type family for removing the send session type from a list of session
--   types.

-- | Type family for removing the receive session type from the given
--   session type. It may be applied to a capability.

-- | Type family for removing the receive session type from a list of
--   session types.

-- | Type family for removing the receive session type from the given
--   session type. It may be applied to a session type.

-- | Type family for applying a constraint to types of kind <a>Type</a> in
--   a session type. It may be applied to a capability.

-- | Type family for applying a constraint to types of kind <a>Type</a> in
--   a list of session types.

-- | Type family for applying a constraint to types of kind <a>Type</a> in
--   a session type. It may be applied to a session type.

-- | Type family for applying zero or more constraints to types of kind
--   <a>Type</a> in a list of session types. It may be applied to a
--   capability.

-- | Promoted <tt>ifThenElse</tt>

-- | Promoted <a>not</a>

-- | Promoted <a>||</a>

-- | Data type that takes a kind as an argument. Its sole constructor takes
--   two capabilities parameterized by the kind argument.
--   
--   This data type is useful if it is necessary for an indexed monad to be
--   indexed by four parameters.
data Prod t
(:*:) :: (Cap t) -> (Cap t) -> Prod t

-- | Type family for returning the first argument of a product.

-- | Type family for returning the second argument of a product.

-- | Data type defining natural numbers
data Nat
Z :: Nat
S :: Nat -> Nat

-- | Data type that can give us proof of membership of an element in a list
--   of elements.
data Ref s xs
[RefZ] :: Ref s (s : xs)
[RefS] :: Ref s (k : xs) -> Ref s (t : (k : xs))

-- | Type family for computing which types in a list of types are equal to
--   a given type.

-- | Promoted <a>++</a>
instance GHC.Classes.Ord Control.SessionTypes.Types.Nat
instance GHC.Classes.Eq Control.SessionTypes.Types.Nat
instance GHC.Show.Show Control.SessionTypes.Types.Nat


-- | This module provides a set of indexed type classes (IxFunctor,
--   IxApplicative, IxMonad, etc..) that correspond to existing type
--   classes (Functor, Applicative, Monad, etc..)
--   
--   The intent of this module is to replace the use of non-indexed type
--   classes with indexed type class.
--   
--   For that reason the indexed type classes expose functions that are
--   named the same as the functions exposed by a corresponding non-indexed
--   type class.
--   
--   There are two ways to use this module:
--   
--   <pre>
--   import           SessionTypes
--   import qualified SessionTypes.Indexed as I
--   
--   prog = send 5 I.&gt;&gt; eps0
--   </pre>
--   
--   <pre>
--   {-# LANGUAGE RebindableSyntax #-}
--   import SessionTypes
--   import SessionTypes.Indexed
--   
--   prog = do
--    send 5
--    eps0
--   </pre>
--   
--   With <tt>RebindableSyntax</tt> we construct a custom do notation by
--   rebinding (&gt;&gt;=) with (&gt;&gt;=) of <a>IxMonad</a>. Rebinding is
--   not limited to only (&gt;&gt;=), but also all other functions in
--   Prelude.
--   
--   We do not want to force importing Prelude if you use
--   <tt>RebindableSyntax</tt>. Therefore this module also exports Prelude
--   that hides functions already defined by the indexed type classes.
module Control.SessionTypes.Indexed
class IxFunctor (f :: p -> p -> Type -> Type)
fmap :: IxFunctor f => (a -> b) -> f j k a -> f j k b
class IxFunctor f => IxApplicative (f :: p -> p -> Type -> Type)
pure :: IxApplicative f => a -> f i i a
(<*>) :: IxApplicative f => f s r (a -> b) -> f r k a -> f s k b
class IxApplicative m => IxMonad (m :: p -> p -> Type -> Type) where m1 >> m2 = m1 >>= \ _ -> m2 fail = error
(>>=) :: IxMonad m => m s t a -> (a -> m t k b) -> m s k b
(>>) :: IxMonad m => m s t a -> m t k b -> m s k b
return :: IxMonad m => a -> m i i a
fail :: IxMonad m => String -> m i i a

-- | Type class for lifting monadic computations
class IxMonad (t m) => IxMonadT t m
lift :: IxMonadT t m => m a -> t m s s a

-- | Type class for lifting indexed monadic computations
class IxMonad (t m) => IxMonadIxT t m
ilift :: IxMonadIxT t m => m s r a -> t m s r a

-- | Type class representing the indexed monad reader
class IxMonad m => IxMonadReader r m | m -> r
ask :: IxMonadReader r m => m s s r
local :: IxMonadReader r m => (r -> r) -> m s t a -> m s t a
reader :: IxMonadReader r m => (r -> a) -> m i i a

-- | Type class for indexed monads in which exceptions may be thrown.
class IxMonad m => IxMonadThrow m s

-- | Provide an <a>Exception</a> to be thrown
throwM :: (IxMonadThrow m s, Exception e) => e -> m s s a

-- | Type class for indexed monads to allow catching of exceptions.
class IxMonadThrow m s => IxMonadCatch m s

-- | Provide a handler to catch exceptions.
catch :: (IxMonadCatch m s, Exception e) => m s s a -> (e -> m s s a) -> m s s a

-- | Type class for indexed monads that may mask asynchronous exceptions.
class IxMonadCatch m s => IxMonadMask m s

-- | run an action that disables asynchronous exceptions. The provided
--   function can be used to restore the occurrence of asynchronous
--   exceptions.
mask :: IxMonadMask m s => ((m s s b -> m s s b) -> m s s b) -> m s s b

-- | Ensures that even interruptible functions may not raise asynchronous
--   exceptions.
uninterruptibleMask :: IxMonadMask m s => ((m s s b -> m s s b) -> m s s b) -> m s s b

-- | Type class for indexed monads that may lift IO computations.
class IxMonadIO m
liftIO :: IxMonadIO m => IO a -> m s s a
ap :: IxMonad m => m s r (a -> b) -> m r k a -> m s k b
ifThenElse :: Bool -> t -> t -> t


-- | This module provides an interface for writing session typed programs
module Control.SessionTypes.MonadSession

-- | The <a>MonadSession</a> type class exposes a set of functions that
--   composed together form a session typed program
--   
--   A type that is an instance of <a>MonadSession</a> must therefore also
--   be an instance of <a>IxMonad</a>.
--   
--   The functions themselves are generally defined as wrappers over
--   corresponding <tt>STTerm</tt> constructors.
class IxMonad m => MonadSession m
send :: MonadSession m => a -> m (Cap ctx (a :!> r)) (Cap ctx r) ()
recv :: MonadSession m => m (Cap ctx (a :?> r)) (Cap ctx r) a
sel1 :: MonadSession m => m (Cap ctx (Sel (s : xs))) (Cap ctx s) ()
sel2 :: MonadSession m => m (Cap ctx (Sel (s : (t : xs)))) (Cap ctx (Sel (t : xs))) ()
offZ :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx (Off '[s])) r a
offS :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx (Off (t : xs))) r a -> m (Cap ctx (Off (s : (t : xs)))) r a
recurse :: MonadSession m => m (Cap (s : ctx) s) r a -> m (Cap ctx (R s)) r a
weaken :: MonadSession m => m (Cap ctx s) r a -> m (Cap (t : ctx) (Wk s)) r a
var :: MonadSession m => m (Cap (s : ctx) s) r a -> m (Cap (s : ctx) V) r a
eps :: MonadSession m => a -> m (Cap ctx Eps) (Cap ctx Eps) a

-- | A session typed program that is polymorphic in its context can often
--   not be used by interpreters.
--   
--   We can apply <a>empty</a> to the session typed program before passing
--   it to an interpreter to instantiate that the context is empty.
empty :: MonadSession m => m (Cap '[] s) r a -> m (Cap '[] s) r a

-- | Monadic composable definition of <a>empty</a>
--   
--   Prefix a session typed program with (empty &gt;&gt;) to instantiate
--   the context to be empty.
empty0 :: MonadSession m => m (Cap '[] r) (Cap '[] r) ()

-- | Allows indexing of selections.
--   
--   The given <a>Ref</a> type can be used as an indexed to select a
--   branch. This circumvents the need to sequence a bunch of <a>sel1</a>
--   and <a>sel2</a> to select a branch.
--   
--   <pre>
--   prog :: MonadSession m =&gt; m ('Cap ctx (Sel '[a,b,c,d])) ('Cap ctx Eps) ()
--   
--   MonadSession m =&gt; m ('Cap ctx b) ('Cap ctx Eps) ()
--   prog2 = prog &gt;&gt; selN (RefS RefZ)
--   </pre>
selN :: MonadSession m => Ref s xs -> m (Cap ctx (Sel xs)) (Cap ctx s) ()

-- | Select the first branch of a selection.
selN1 :: MonadSession m => m (Cap ctx (Sel (s : xs))) (Cap ctx s) ()

-- | Select the second branch of a selection.
selN2 :: MonadSession m => m (Cap ctx (Sel (s : (t : xs)))) (Cap ctx t) ()

-- | Select the third branch of a selection.
selN3 :: MonadSession m => m (Cap ctx (Sel (s : (t : (k : xs))))) (Cap ctx k) ()

-- | Select the fourth branch of a selection.
selN4 :: MonadSession m => m (Cap ctx (Sel (s : (t : (k : (r : xs)))))) (Cap ctx r) ()

-- | Type class for selecting a branch through injection.
--   
--   Selects the first branch that matches the given session type.
--   
--   <pre>
--   prog :: MonadSession m =&gt; m ('Cap ctx (Sel '[Eps, String :!&gt; Eps, Int :!&gt; Eps])) ('Cap ctx Eps) ()
--   prog = sel &gt;&gt; send "c" &gt;&gt;= eps
--   </pre>
--   
--   It should be obvious that you cannot select a branch using <a>sel</a>
--   if that branch has the same session type as a previous branch.
class Select xs s
sel :: (Select xs s, MonadSession m) => m (Cap ctx (Sel xs)) (Cap ctx s) ()

-- | Infix synonym for <a>offS</a>
(<&) :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx (Off (t : xs))) r a -> m (Cap ctx (Off (s : (t : xs)))) r a
infixr 1 <&

-- | Infix synonym for <a>offer</a>
--   
--   Using both <a>&lt;&amp;</a> and <a>&lt;&amp;&gt;</a> we can now
--   construct an offering as follows:
--   
--   <pre>
--   branch1 
--   &lt;&amp; branch2
--   &lt;&amp; branch3
--   &lt;&amp;&gt; branch4
--   </pre>
--   
--   This will be parsed as
--   
--   <pre>
--   (branch1
--    &lt;&amp; (branch2
--    &lt;&amp; (branch3
--    &lt;&amp;&gt; branch4)))
--   </pre>
(<&>) :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a
infix 2 <&>

-- | Takes two session typed programs and constructs an offering consisting
--   of two branches
offer :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a

-- | A fixpoint combinator for recursion
--   
--   The argument function must take a recursion variable as an argument
--   that can be used to denote the point of recursion.
--   
--   For example:
--   
--   <pre>
--   prog = recurseFix \f -&gt; do
--    send 5
--    f
--   </pre>
--   
--   This program will send the number 5 an infinite amount of times.
recurseFix :: MonadSession m => (m (Cap (s : ctx) V) r a -> m (Cap (s : ctx) s) r a) -> m (Cap ctx (R s)) r a

-- | Monadic composable definition of <a>recurse</a>
recurse0 :: MonadSession m => m (Cap ctx (R s)) (Cap (s : ctx) s) ()

-- | Monadic composable definition of <a>weaken</a>
weaken0 :: MonadSession m => m (Cap (t : ctx) (Wk s)) (Cap ctx s) ()

-- | Monadic composable definition of <a>var</a>
var0 :: MonadSession m => m (Cap (s : ctx) V) (Cap (s : ctx) s) ()

-- | Monadic composable definition of <a>eps</a>
eps0 :: MonadSession m => m (Cap ctx Eps) (Cap ctx Eps) ()
instance (tl ~ Control.SessionTypes.Types.TypeEqList xs s, Control.SessionTypes.MonadSession.Select' xs s tl) => Control.SessionTypes.MonadSession.Select xs s
instance Control.SessionTypes.MonadSession.Select' (s : xs) s ('GHC.Types.True : tl)
instance Control.SessionTypes.MonadSession.Select' (r : xs) t tl => Control.SessionTypes.MonadSession.Select' (s : r : xs) t ('GHC.Types.False : tl)


-- | This module defines an interpreter for visualizing session types.
--   
--   Using <a>visualize</a> or <a>visualizeP</a> you can create a diagram
--   that displays a session type using a set of nodes and arrows that
--   connect these nodes.
module Control.SessionTypes.Visualize

-- | Visualizes the session type of a given <tt>STTerm</tt> You may use
--   this function in the following way
--   
--   <pre>
--   main = visualize st
--   </pre>
--   
--   Then the following command will generate a diagram named
--   "sessiontype.png"
--   
--   <pre>
--   stack exec vis-sessiontype -- -o sessiontype.png -w 400
--   </pre>
--   
--   For more information on how to generate a diagram please visit the
--   <a>diagrams</a> package
visualize :: forall m ctx s r a. (MonadSession m, MkDiagram s) => m (Cap ctx s) r a -> IO ()

-- | Visualizes a given session type denoted by a Proxy.
visualizeP :: forall s. MkDiagram s => Proxy s -> IO ()

-- | Type class for constructing a diagram that visualizes the session
--   types
class MkDiagram (s :: ST k) where mkDiagram p = do { dstate <- dstateWNodesIO; (diag, DState n _ _ d g) <- runStateT connectGrid dstate; fmap fst $ runStateT connectRecursions (DState n 0 (0, 0) diag g) } where dstateWNodesIO = fmap snd $ runStateT (placeNodes p) (newDState $ newGrid (getX p) (getY p))
instance GHC.Show.Show Control.SessionTypes.Visualize.NodeType
instance GHC.Classes.Eq Control.SessionTypes.Visualize.NodeType
instance forall k (s :: Control.SessionTypes.Types.ST k). (Control.SessionTypes.Visualize.Coordinates s, Control.SessionTypes.Visualize.PlaceNodes s) => Control.SessionTypes.Visualize.MkDiagram s
instance forall k (r :: Control.SessionTypes.Types.ST k) (a :: k). Control.SessionTypes.Visualize.Coordinates r => Control.SessionTypes.Visualize.Coordinates (a 'Control.SessionTypes.Types.:!> r)
instance forall k (r :: Control.SessionTypes.Types.ST k) (a :: k). Control.SessionTypes.Visualize.Coordinates r => Control.SessionTypes.Visualize.Coordinates (a 'Control.SessionTypes.Types.:?> r)
instance forall k (t :: Control.SessionTypes.Types.ST k). Control.SessionTypes.Visualize.Coordinates t => Control.SessionTypes.Visualize.Coordinates ('Control.SessionTypes.Types.Sel '[t])
instance forall k (s :: Control.SessionTypes.Types.ST k) (t :: Control.SessionTypes.Types.ST k) (xs :: [Control.SessionTypes.Types.ST k]). (Control.SessionTypes.Visualize.Coordinates s, Control.SessionTypes.Visualize.Coordinates ('Control.SessionTypes.Types.Sel (t : xs))) => Control.SessionTypes.Visualize.Coordinates ('Control.SessionTypes.Types.Sel (s : t : xs))
instance forall k (t :: Control.SessionTypes.Types.ST k). Control.SessionTypes.Visualize.Coordinates t => Control.SessionTypes.Visualize.Coordinates ('Control.SessionTypes.Types.Off '[t])
instance forall k (s :: Control.SessionTypes.Types.ST k) (t :: Control.SessionTypes.Types.ST k) (xs :: [Control.SessionTypes.Types.ST k]). (Control.SessionTypes.Visualize.Coordinates s, Control.SessionTypes.Visualize.Coordinates ('Control.SessionTypes.Types.Off (t : xs))) => Control.SessionTypes.Visualize.Coordinates ('Control.SessionTypes.Types.Off (s : t : xs))
instance forall k (s :: Control.SessionTypes.Types.ST k). Control.SessionTypes.Visualize.Coordinates s => Control.SessionTypes.Visualize.Coordinates ('Control.SessionTypes.Types.R s)
instance Control.SessionTypes.Visualize.Coordinates 'Control.SessionTypes.Types.V
instance forall k (s :: Control.SessionTypes.Types.ST k). Control.SessionTypes.Visualize.Coordinates s => Control.SessionTypes.Visualize.Coordinates ('Control.SessionTypes.Types.Wk s)
instance Control.SessionTypes.Visualize.Coordinates 'Control.SessionTypes.Types.Eps
instance forall k (a :: k) (r :: Control.SessionTypes.Types.ST k). (Data.Typeable.Internal.Typeable a, Control.SessionTypes.Visualize.PlaceNodes r) => Control.SessionTypes.Visualize.PlaceNodes (a 'Control.SessionTypes.Types.:!> r)
instance forall k (a :: k) (r :: Control.SessionTypes.Types.ST k). (Data.Typeable.Internal.Typeable a, Control.SessionTypes.Visualize.PlaceNodes r) => Control.SessionTypes.Visualize.PlaceNodes (a 'Control.SessionTypes.Types.:?> r)
instance forall k (s :: Control.SessionTypes.Types.ST k). Control.SessionTypes.Visualize.PlaceNodes s => Control.SessionTypes.Visualize.PlaceNodes ('Control.SessionTypes.Types.Sel '[s])
instance forall k (s :: Control.SessionTypes.Types.ST k) (t :: Control.SessionTypes.Types.ST k) (xs :: [Control.SessionTypes.Types.ST k]). (Control.SessionTypes.Visualize.Coordinates s, Control.SessionTypes.Visualize.PlaceNodes s, Control.SessionTypes.Visualize.PlaceNodes ('Control.SessionTypes.Types.Sel (t : xs))) => Control.SessionTypes.Visualize.PlaceNodes ('Control.SessionTypes.Types.Sel (s : t : xs))
instance forall k (s :: Control.SessionTypes.Types.ST k). Control.SessionTypes.Visualize.PlaceNodes s => Control.SessionTypes.Visualize.PlaceNodes ('Control.SessionTypes.Types.Off '[s])
instance forall k (s :: Control.SessionTypes.Types.ST k) (t :: Control.SessionTypes.Types.ST k) (xs :: [Control.SessionTypes.Types.ST k]). (Control.SessionTypes.Visualize.Coordinates s, Control.SessionTypes.Visualize.PlaceNodes s, Control.SessionTypes.Visualize.PlaceNodes ('Control.SessionTypes.Types.Off (t : xs))) => Control.SessionTypes.Visualize.PlaceNodes ('Control.SessionTypes.Types.Off (s : t : xs))
instance forall k (s :: Control.SessionTypes.Types.ST k). Control.SessionTypes.Visualize.PlaceNodes s => Control.SessionTypes.Visualize.PlaceNodes ('Control.SessionTypes.Types.R s)
instance Control.SessionTypes.Visualize.PlaceNodes 'Control.SessionTypes.Types.V
instance forall k (s :: Control.SessionTypes.Types.ST k). Control.SessionTypes.Visualize.PlaceNodes s => Control.SessionTypes.Visualize.PlaceNodes ('Control.SessionTypes.Types.Wk s)
instance Control.SessionTypes.Visualize.PlaceNodes 'Control.SessionTypes.Types.Eps


-- | This module defines a GADT <a>STTerm</a> that is the very core of this
--   library
--   
--   Session typed programs are constructed by composing the constructors
--   of <a>STTerm</a>.
--   
--   Each constructor is annotated with a specific session type (except for
--   <a>Ret</a> and <a>Lift</a>).
--   
--   By passing a constructor to another constructor as an argument their
--   session types are joined to form a larger session type.
--   
--   We do not recommend explicitly composing the <a>STTerm</a>
--   constructors. Instead make use of the functions defined in the
--   <a>Control.SessionTypes.MonadSession</a> module.
--   
--   Of course a <a>STTerm</a> program in itself is not very useful as it
--   is devoid of any semantics. However, an interpreter function can give
--   meaning to a <a>STTerm</a> program.
--   
--   We define a couple in this library: <a>Control.SessionTypes.Debug</a>,
--   <a>Control.SessionTypes.Interactive</a>,
--   <a>Control.SessionTypes.Normalize</a> and
--   <a>Control.SessionTypes.Visualize</a>.
module Control.SessionTypes.STTerm

-- | The STTerm GADT
--   
--   Although we say that a <a>STTerm</a> is annotated with a session type,
--   it is actually annotated with a capability (<a>Cap</a>).
--   
--   The capability contains a context that is necessary for recursion and
--   the session type.
--   
--   The constructors can be split in four different categories:
--   
--   <ul>
--   <li>Communication: <a>Send</a> and <a>Recv</a> for basic
--   communication</li>
--   <li>Branching: <a>Sel1</a>, <a>Sel2</a>, <a>OffZ</a> and
--   <a>OffS</a></li>
--   <li>Recursion: <a>Rec</a>, <a>Weaken</a> and <a>Var</a></li>
--   <li>Unsession typed: <a>Ret</a> and <a>Lift</a></li>
--   </ul>
data STTerm :: (Type -> Type) -> Cap a -> Cap a -> Type -> Type

-- | The constructor for sending messages. It is annotated with the send
--   session type (<a>:!&gt;</a>).
--   
--   It takes as an argument, the message to send, of type equal to the
--   first argument of <a>:!&gt;</a> and the continuing <a>STTerm</a> that
--   is session typed with the second argument of <a>:!&gt;</a>.
[Send] :: a -> STTerm m (Cap ctx r) r' b -> STTerm m (Cap ctx (a :!> r)) r' b

-- | The constructor for receiving messages. It is annotated with the
--   receive session type (<a>:?&gt;</a>)
--   
--   It takes a continuation that promises to deliver a value that may be
--   used in the rest of the program.
[Recv] :: (a -> STTerm m (Cap ctx r) r' b) -> STTerm m (Cap ctx (a :?> r)) r' b

-- | Selects the first branch in a selection session type.
--   
--   By selecting a branch, that selected session type must then be
--   implemented.
[Sel1] :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Sel (s : xs))) r a

-- | Skips a branch in a selection session type.
--   
--   If the first branch in the selection session type is not the one we
--   want to implement then we may use <a>Sel2</a> to skip this.
[Sel2] :: STTerm m (Cap ctx (Sel (t : xs))) r a -> STTerm m (Cap ctx (Sel (s : (t : xs)))) r a

-- | Dually to selection there is also offering branches.
--   
--   Unlike selection, where we may only implement one branch, an offering
--   asks you to implement all branches. Which is chosen depends on how an
--   interpreter synchronizes selection with offering.
--   
--   This constructor denotes the very last branch that may be offered.
[OffZ] :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Off '[s])) r a

-- | offers a branch and promises at least one more branch to be offered.
[OffS] :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Off (t : xs))) r a -> STTerm m (Cap ctx (Off (s : (t : xs)))) r a

-- | Constructor for delimiting the scope of recursion
--   
--   The recursion constructors also modify or at least make use of the
--   context in the capability.
--   
--   The <a>Rec</a> constructor inserts the session type argument to
--   <a>R</a> into the context of the capability of its <a>STTerm</a>
--   argument.
--   
--   This is necessary such that we remember the session type of the body
--   of code that we may want to recurse over and thus avoiding infinite
--   type occurrence errors.
[Rec] :: STTerm m (Cap (s : ctx) s) r a -> STTerm m (Cap ctx (R s)) r a

-- | Constructor for weakening (expanding) the scope of recusion
--   
--   This constructor does the opposite of <a>R</a> by popping a session
--   type from the context.
--   
--   Use this constructor to essentially exit a recursion
[Weaken] :: STTerm m (Cap ctx t) r a -> STTerm m (Cap (s : ctx) (Wk t)) r a

-- | Constructor that denotes the recursion variable
--   
--   It assumes the context to be non-empty and uses the session type at
--   the top of the context to determine what should be implemented after
--   <a>Var</a>.
[Var] :: STTerm m (Cap (s : ctx) s) t a -> STTerm m (Cap (s : ctx) V) t a

-- | Constructor that makes <a>STTerm</a> a (indexed) monad
[Ret] :: (a :: Type) -> STTerm m s s a

-- | Constructor that makes <a>STTerm</a> a (indexed) monad transformer
[Lift] :: m (STTerm m s r a) -> STTerm m s r a

-- | This function can be used if we do not use <tt>lift</tt> in a program
--   but we must still disambiguate <tt>m</tt>.
inferIdentity :: STTerm Identity s r a -> STTerm Identity s r a
instance forall a (m :: GHC.Types.Type -> GHC.Types.Type) (s :: Control.SessionTypes.Types.Cap a). GHC.Base.Functor (Control.SessionTypes.STTerm.STTerm m s s)
instance forall a (m :: GHC.Types.Type -> GHC.Types.Type) (s :: Control.SessionTypes.Types.Cap a). GHC.Base.Applicative (Control.SessionTypes.STTerm.STTerm m s s)
instance forall a (m :: GHC.Types.Type -> GHC.Types.Type) (s :: Control.SessionTypes.Types.Cap a). GHC.Base.Monad (Control.SessionTypes.STTerm.STTerm m s s)
instance Control.SessionTypes.Indexed.IxFunctor (Control.SessionTypes.STTerm.STTerm m)
instance GHC.Base.Monad m => Control.SessionTypes.Indexed.IxApplicative (Control.SessionTypes.STTerm.STTerm m)
instance GHC.Base.Monad m => Control.SessionTypes.Indexed.IxMonad (Control.SessionTypes.STTerm.STTerm m)
instance GHC.Base.Monad m => Control.SessionTypes.Indexed.IxMonadT Control.SessionTypes.STTerm.STTerm m
instance Control.Monad.IO.Class.MonadIO m => Control.SessionTypes.Indexed.IxMonadIO (Control.SessionTypes.STTerm.STTerm m)
instance GHC.Base.Monad m => Control.SessionTypes.MonadSession.MonadSession (Control.SessionTypes.STTerm.STTerm m)


-- | This module exposes two functions for interactively evaluation a
--   session typed program
--   
--   To run a session you must have two participating actors. In our
--   context, the actors are session typed programs.
--   
--   Using this module the user will act as one of the actors in the
--   session by suppling values to a receive
--   
--   and selecting a branch for offerings.
module Control.SessionTypes.Interactive

-- | For this function tThe user will act as the dual to the given
--   <a>STTerm</a>. User interaction is only required when the given
--   program does a receive or an offer.
--   
--   A possible interaction goes as follows:
--   
--   <pre>
--   prog = do
--    send 5
--    x &lt;- recv
--    offer (eps x) (eps "")
--   
--   main = interactive prog
--   </pre>
--   
--   <pre>
--   &gt; Enter value of type String: "test"
--   &gt; (L)eft or (R)ight: L
--    "test"
--   </pre>
interactive :: (MonadIO m, HasConstraints '[Read, Show, Typeable] s, Show a) => STTerm m s r a -> m a

-- | Different from <a>interactive</a> is that this function gives the user
--   the choice to abort the session after each session typed action.
--   
--   Furthermore, it also prints additional output describing which session
--   typed action occurred.
interactiveStep :: (MonadIO m, HasConstraints '[Read, Show, Typeable] s, Show a) => STTerm m s r a -> m (Maybe a)


-- | This module provides a type class for normalizing session typed
--   programs.
--   
--   With normalizing we mean that we apply rewrites to a session typed
--   program until we can no longer do so and that do not change the
--   semantics of the program.
--   
--   The motivation for this module is that for two session typed programs
--   to run a session they must be dual. Sometimes, one of these programs
--   might not have a session type that is dual to the session type of the
--   other program,
--   
--   but we can rewrite the program and therefore also the session type
--   such that it is. It is of course important that we do not alter the
--   semantics of the program when rewriting it. For that reason, any
--   rewrite that we may apply must be isomorphic.
--   
--   A rewrite is isomorphic if we have two programs p and p', we can do a
--   rewrite from p to p' and from p' to p.
--   
--   For now two types of rewrites are applied: Elimination of recursive
--   types and flattening of branches.
module Control.SessionTypes.Normalize

-- | Type class for rewriting an <a>STTerm</a> to its normal form
--   
--   The type class has a single instance that is constrained with two type
--   classes. One for each type of rewrite.
class Normalize s s'' | s -> s''
normalize :: (Normalize s s'', Monad m) => STTerm m s (Cap '[] Eps) a -> STTerm m s'' (Cap '[] Eps) a

-- | Type class for flattening branches
--   
--   The function <a>flatten</a> takes and traverses a <a>STTerm</a>. If it
--   finds a branching session type that has a branch starting with another
--   branching of the same type, then it will extract the branches of the
--   inner branching and inserts these into the outer branching. This is
--   similar to flattening a list of lists to a larger list.
--   
--   For example:
--   
--   <pre>
--   Sel '[a,b, Sel '[c,d], e]
--   </pre>
--   
--   becomes
--   
--   <pre>
--   Sel '[a,b,c,d,e]
--   </pre>
--   
--   This only works if the inner branching has the same type as the outer
--   branch (Sel in Sel or Off in Off).
--   
--   Also, for now this rewrite only works if one of the branching of the
--   outer branch starts with a new branching.
--   
--   For example:
--   
--   <pre>
--   Sel '[a,b, Int :!&gt; Sel '[c,d],e]
--   </pre>
--   
--   does not become
--   
--   <pre>
--   Sel '[a,b,Int :!&gt; c, Int :!&gt; d, e]
--   </pre>
--   
--   This is something that will be added in the future.
class Flatten s s' | s -> s'
flatten :: (Flatten s s', Monad m) => STTerm m s r a -> STTerm m s' r a

-- | Type class for eliminating unused recursive types.
--   
--   The function <a>elimRec</a> traverses a given <a>STTerm</a>. While
--   doing so, it will attempt to remove constructors annotated with
--   <a>R</a> or <a>Wk</a> from the program if in doing so does not change
--   the behavior of the program.
--   
--   For example, in the following session type we may remove the inner
--   <a>R</a> and the <a>Wk</a>.
--   
--   <pre>
--   R (R (Wk V))
--   </pre>
--   
--   We have that the outer <a>R</a> matches the recursion variable because
--   of the use of <a>Wk</a>.
--   
--   That means the inner <a>R</a> does not match any recursion variable
--   (the <a>R</a> is unused) and therefore may it and its corresponding
--   constructor be removed from the <a>STTerm</a> program.
--   
--   We also remove the <a>Wk</a>, because the session type pushed into the
--   context by the inner <a>R</a> has also been removed.
--   
--   The generated session type is
--   
--   <pre>
--   R V
--   </pre>
class ElimRec s s' | s -> s'
elimRec :: (ElimRec s s', Monad m) => STTerm m s r a -> STTerm m s' r a
instance forall a (s :: Control.SessionTypes.Types.Cap a) (s' :: Control.SessionTypes.Types.Cap a) (s'' :: Control.SessionTypes.Types.Cap a). (Control.SessionTypes.Normalize.Flatten s s', Control.SessionTypes.Normalize.ElimRec s' s'') => Control.SessionTypes.Normalize.Normalize s s''
instance forall a (el :: Control.SessionTypes.Types.Cap GHC.Types.Bool) (s :: Control.SessionTypes.Types.Cap a) (s' :: Control.SessionTypes.Types.Cap a). (el ~ Control.SessionTypes.Normalize.ElimRecAllPath s, Control.SessionTypes.Normalize.ElimRec' s s' el) => Control.SessionTypes.Normalize.ElimRec s s'
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (r :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (r' :: Control.SessionTypes.Types.ST a) (rml :: Control.SessionTypes.Types.Cap GHC.Types.Bool) (a1 :: a). Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx r) ('Control.SessionTypes.Types.Cap ctx' r') rml => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx (a1 'Control.SessionTypes.Types.:!> r)) ('Control.SessionTypes.Types.Cap ctx' (a1 'Control.SessionTypes.Types.:!> r')) rml
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (r :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (r' :: Control.SessionTypes.Types.ST a) (rml :: Control.SessionTypes.Types.Cap GHC.Types.Bool) (a1 :: a). Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx r) ('Control.SessionTypes.Types.Cap ctx' r') rml => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx (a1 'Control.SessionTypes.Types.:?> r)) ('Control.SessionTypes.Types.Cap ctx' (a1 'Control.SessionTypes.Types.:?> r')) rml
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (rmctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rm :: Control.SessionTypes.Types.ST GHC.Types.Bool). Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap rmctx rm) => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel '[s])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel '[s'])) ('Control.SessionTypes.Types.Cap rmctx ('Control.SessionTypes.Types.Sel '[rm]))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (rmctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rm :: Control.SessionTypes.Types.ST GHC.Types.Bool) (t :: Control.SessionTypes.Types.ST a) (xs :: [Control.SessionTypes.Types.ST a]) (t' :: Control.SessionTypes.Types.ST a) (xs' :: [Control.SessionTypes.Types.ST a]) (rmxs :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). (Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap rmctx rm), Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel (t : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel (t' : xs'))) ('Control.SessionTypes.Types.Cap rmctx ('Control.SessionTypes.Types.Sel rmxs))) => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel (s : t : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel (s' : t' : xs'))) ('Control.SessionTypes.Types.Cap rmctx ('Control.SessionTypes.Types.Sel (rm : rmxs)))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (rmctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rm :: Control.SessionTypes.Types.ST GHC.Types.Bool). Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap rmctx rm) => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off '[s])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off '[s'])) ('Control.SessionTypes.Types.Cap rmctx ('Control.SessionTypes.Types.Off '[rm]))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (rmctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rm :: Control.SessionTypes.Types.ST GHC.Types.Bool) (t :: Control.SessionTypes.Types.ST a) (xs :: [Control.SessionTypes.Types.ST a]) (t' :: Control.SessionTypes.Types.ST a) (xs' :: [Control.SessionTypes.Types.ST a]) (rmxs :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). (Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap rmctx rm), Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off (t : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off (t' : xs'))) ('Control.SessionTypes.Types.Cap rmctx ('Control.SessionTypes.Types.Off rmxs))) => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off (s : t : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off (s' : t' : xs'))) ('Control.SessionTypes.Types.Cap rmctx ('Control.SessionTypes.Types.Off (rm : rmxs)))
instance forall a (s :: Control.SessionTypes.Types.ST a) (ctx :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (rml :: Control.SessionTypes.Types.ST GHC.Types.Bool) (rmctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap (s : ctx) s) ('Control.SessionTypes.Types.Cap (s' : ctx') s') ('Control.SessionTypes.Types.Cap (rml : rmctx) rml) => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.R s)) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.R s')) ('Control.SessionTypes.Types.Cap rmctx ('GHC.Types.True 'Control.SessionTypes.Types.:!> rml))
instance forall a (s :: Control.SessionTypes.Types.ST a) (ctx :: [Control.SessionTypes.Types.ST a]) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (rmctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rml :: Control.SessionTypes.Types.ST GHC.Types.Bool). Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap (s : ctx) s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap rmctx rml) => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.R s)) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap rmctx ('GHC.Types.False 'Control.SessionTypes.Types.:!> rml))
instance forall a (t :: Control.SessionTypes.Types.ST a) (rm' :: Control.SessionTypes.Types.ST GHC.Types.Bool) (t' :: Control.SessionTypes.Types.ST a) (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (rmctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rml :: Control.SessionTypes.Types.ST GHC.Types.Bool). (Control.SessionTypes.Normalize.ApplyElimRecPath t rm' ~ t', Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap rmctx rml)) => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap (t : ctx) ('Control.SessionTypes.Types.Wk s)) ('Control.SessionTypes.Types.Cap (t' : ctx') ('Control.SessionTypes.Types.Wk s')) ('Control.SessionTypes.Types.Cap (rm' : rmctx) ('GHC.Types.True 'Control.SessionTypes.Types.:!> rml))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (rmctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rml :: Control.SessionTypes.Types.ST GHC.Types.Bool) (t :: Control.SessionTypes.Types.ST a). Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap rmctx rml) => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap (t : ctx) ('Control.SessionTypes.Types.Wk s)) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap rmctx ('GHC.Types.False 'Control.SessionTypes.Types.:!> rml))
instance forall a (s :: Control.SessionTypes.Types.ST a) (ctx :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (rm :: Control.SessionTypes.Types.ST GHC.Types.Bool) (rmctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap (s : ctx) s) ('Control.SessionTypes.Types.Cap (s' : ctx') s') ('Control.SessionTypes.Types.Cap (rm : rmctx) rm) => Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap (s : ctx) 'Control.SessionTypes.Types.V) ('Control.SessionTypes.Types.Cap (s' : ctx') 'Control.SessionTypes.Types.V) ('Control.SessionTypes.Types.Cap (rm : rmctx) 'Control.SessionTypes.Types.V)
instance Control.SessionTypes.Normalize.ElimRec' ('Control.SessionTypes.Types.Cap '[] 'Control.SessionTypes.Types.Eps) ('Control.SessionTypes.Types.Cap '[] 'Control.SessionTypes.Types.Eps) ('Control.SessionTypes.Types.Cap '[] 'Control.SessionTypes.Types.Eps)
instance forall a (rwl :: Control.SessionTypes.Types.Cap GHC.Types.Bool) (s :: Control.SessionTypes.Types.Cap a) (s' :: Control.SessionTypes.Types.Cap a). (rwl ~ Control.SessionTypes.Normalize.ListRewrites s, Control.SessionTypes.Normalize.Flatten' s s' rwl) => Control.SessionTypes.Normalize.Flatten s s'
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (ys :: [Control.SessionTypes.Types.ST a]) (ctx' :: [Control.SessionTypes.Types.ST a]) (ys' :: [Control.SessionTypes.Types.ST a]) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rwl :: Control.SessionTypes.Types.ST GHC.Types.Bool). Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel ys)) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel ys')) ('Control.SessionTypes.Types.Cap nctx rwl) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel '['Control.SessionTypes.Types.Sel ys])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel ys')) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Sel '['GHC.Types.True 'Control.SessionTypes.Types.:!> rwl]))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (y :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (y' :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rw_y :: Control.SessionTypes.Types.ST GHC.Types.Bool) (x :: Control.SessionTypes.Types.ST a) (xs :: [Control.SessionTypes.Types.ST a]) (x' :: Control.SessionTypes.Types.ST a) (xs' :: [Control.SessionTypes.Types.ST a]) (rw_xs :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). (Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel '[y])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel '[y'])) ('Control.SessionTypes.Types.Cap nctx rw_y), Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel (x : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel (x' : xs'))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Sel rw_xs))) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel ('Control.SessionTypes.Types.Sel '[y] : x : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel (y' : x' : xs'))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Sel ('GHC.Types.True 'Control.SessionTypes.Types.:!> rw_y : rw_xs)))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rw_s :: Control.SessionTypes.Types.ST GHC.Types.Bool) (z :: Control.SessionTypes.Types.ST a) (ys :: [Control.SessionTypes.Types.ST a]) (x :: Control.SessionTypes.Types.ST a) (xs :: [Control.SessionTypes.Types.ST a]) (z' :: Control.SessionTypes.Types.ST a) (xss :: [Control.SessionTypes.Types.ST a]) (rw_ys :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rw_xss :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). (Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel '[s])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel '[s'])) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Sel '[rw_s])), Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel ('Control.SessionTypes.Types.Sel (z : ys) : x : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel (z' : xss))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Sel ('GHC.Types.True 'Control.SessionTypes.Types.:!> 'Control.SessionTypes.Types.Sel rw_ys : rw_xss)))) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel ('Control.SessionTypes.Types.Sel (s : z : ys) : x : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel (s' : z' : xss))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Sel ('GHC.Types.True 'Control.SessionTypes.Types.:!> 'Control.SessionTypes.Types.Sel (rw_s : rw_ys) : rw_xss)))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (ys :: [Control.SessionTypes.Types.ST a]) (ctx' :: [Control.SessionTypes.Types.ST a]) (ys' :: [Control.SessionTypes.Types.ST a]) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rwl :: Control.SessionTypes.Types.ST GHC.Types.Bool). Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off ys)) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off ys')) ('Control.SessionTypes.Types.Cap nctx rwl) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off '['Control.SessionTypes.Types.Off ys])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off ys')) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Off '['GHC.Types.True 'Control.SessionTypes.Types.:!> rwl]))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rwl_s :: Control.SessionTypes.Types.ST GHC.Types.Bool) (x :: Control.SessionTypes.Types.ST a) (xs :: [Control.SessionTypes.Types.ST a]) (x' :: Control.SessionTypes.Types.ST a) (xs' :: [Control.SessionTypes.Types.ST a]) (rwl_xs :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). (Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off '[s])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off '[s'])) ('Control.SessionTypes.Types.Cap nctx rwl_s), Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off (x : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off (x' : xs'))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Off rwl_xs))) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off ('Control.SessionTypes.Types.Off '[s] : x : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off (s' : x' : xs'))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Off ('GHC.Types.True 'Control.SessionTypes.Types.:!> rwl_s : rwl_xs)))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rwl_s :: Control.SessionTypes.Types.ST GHC.Types.Bool) (z :: Control.SessionTypes.Types.ST a) (ys :: [Control.SessionTypes.Types.ST a]) (x :: Control.SessionTypes.Types.ST a) (xs :: [Control.SessionTypes.Types.ST a]) (z' :: Control.SessionTypes.Types.ST a) (xss :: [Control.SessionTypes.Types.ST a]) (rwl_ys :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rw_xs :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). (Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off '[s])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off '[s'])) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Off '[rwl_s])), Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off ('Control.SessionTypes.Types.Off (z : ys) : x : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off (z' : xss))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Off ('GHC.Types.True 'Control.SessionTypes.Types.:!> 'Control.SessionTypes.Types.Off rwl_ys : rw_xs)))) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off ('Control.SessionTypes.Types.Off (s : z : ys) : x : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off (s' : z' : xss))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Off ('GHC.Types.True 'Control.SessionTypes.Types.:!> 'Control.SessionTypes.Types.Off (rwl_s : rwl_ys) : rw_xs)))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rwl :: Control.SessionTypes.Types.ST GHC.Types.Bool). Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap nctx rwl) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel '[s])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel '[s'])) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Sel '['GHC.Types.False 'Control.SessionTypes.Types.:!> rwl]))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rw_s :: Control.SessionTypes.Types.ST GHC.Types.Bool) (r :: Control.SessionTypes.Types.ST a) (xs :: [Control.SessionTypes.Types.ST a]) (r' :: Control.SessionTypes.Types.ST a) (xs' :: [Control.SessionTypes.Types.ST a]) (rw_xs :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). (Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap nctx rw_s), Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel (r : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel (r' : xs'))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Sel rw_xs))) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Sel (s : r : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Sel (s' : r' : xs'))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Sel ('GHC.Types.False 'Control.SessionTypes.Types.:!> rw_s : rw_xs)))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rwl :: Control.SessionTypes.Types.ST GHC.Types.Bool). Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap nctx rwl) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off '[s])) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off '[s'])) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Off '['GHC.Types.False 'Control.SessionTypes.Types.:!> rwl]))
instance forall a (ctx :: [Control.SessionTypes.Types.ST a]) (s :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (s' :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST GHC.Types.Bool]) (rwl_s :: Control.SessionTypes.Types.ST GHC.Types.Bool) (t :: Control.SessionTypes.Types.ST a) (xs :: [Control.SessionTypes.Types.ST a]) (t' :: Control.SessionTypes.Types.ST a) (xs' :: [Control.SessionTypes.Types.ST a]) (rwl_r :: [Control.SessionTypes.Types.ST GHC.Types.Bool]). (Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap nctx rwl_s), Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off (t : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off (t' : xs'))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Off rwl_r))) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.Off (s : t : xs))) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.Off (s' : t' : xs'))) ('Control.SessionTypes.Types.Cap nctx ('Control.SessionTypes.Types.Off ('GHC.Types.False 'Control.SessionTypes.Types.:!> rwl_s : rwl_r)))
instance forall k a (ctx :: [Control.SessionTypes.Types.ST a]) (r :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (r' :: Control.SessionTypes.Types.ST a) (rwl :: k) (a1 :: a). Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx r) ('Control.SessionTypes.Types.Cap ctx' r') rwl => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx (a1 'Control.SessionTypes.Types.:!> r)) ('Control.SessionTypes.Types.Cap ctx' (a1 'Control.SessionTypes.Types.:!> r')) rwl
instance forall k a (ctx :: [Control.SessionTypes.Types.ST a]) (r :: Control.SessionTypes.Types.ST a) (ctx' :: [Control.SessionTypes.Types.ST a]) (r' :: Control.SessionTypes.Types.ST a) (rwl :: k) (a1 :: a). Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx r) ('Control.SessionTypes.Types.Cap ctx' r') rwl => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx (a1 'Control.SessionTypes.Types.:?> r)) ('Control.SessionTypes.Types.Cap ctx' (a1 'Control.SessionTypes.Types.:?> r')) rwl
instance forall a a1 (s :: Control.SessionTypes.Types.ST a1) (ctx :: [Control.SessionTypes.Types.ST a1]) (s' :: Control.SessionTypes.Types.ST a1) (ctx' :: [Control.SessionTypes.Types.ST a1]) (norm :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST a]). Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap (s : ctx) s) ('Control.SessionTypes.Types.Cap (s' : ctx') s') ('Control.SessionTypes.Types.Cap (norm : nctx) norm) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx ('Control.SessionTypes.Types.R s)) ('Control.SessionTypes.Types.Cap ctx' ('Control.SessionTypes.Types.R s')) ('Control.SessionTypes.Types.Cap nctx norm)
instance forall a a1 (t :: Control.SessionTypes.Types.ST a1) (t' :: Control.SessionTypes.Types.ST a1) (ctx :: [Control.SessionTypes.Types.ST a1]) (s :: Control.SessionTypes.Types.ST a1) (ctx' :: [Control.SessionTypes.Types.ST a1]) (s' :: Control.SessionTypes.Types.ST a1) (nctx :: [Control.SessionTypes.Types.ST a]) (norm :: Control.SessionTypes.Types.ST a) (k :: Control.SessionTypes.Types.ST a). (Control.SessionTypes.Normalize.RewriteTypes t ~ t', Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx s) ('Control.SessionTypes.Types.Cap ctx' s') ('Control.SessionTypes.Types.Cap nctx norm)) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap (t : ctx) ('Control.SessionTypes.Types.Wk s)) ('Control.SessionTypes.Types.Cap (t' : ctx') ('Control.SessionTypes.Types.Wk s')) ('Control.SessionTypes.Types.Cap (k : nctx) norm)
instance forall a a1 (s :: Control.SessionTypes.Types.ST a1) (ctx :: [Control.SessionTypes.Types.ST a1]) (s' :: Control.SessionTypes.Types.ST a1) (ctx' :: [Control.SessionTypes.Types.ST a1]) (norm :: Control.SessionTypes.Types.ST a) (nctx :: [Control.SessionTypes.Types.ST a]). Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap (s : ctx) s) ('Control.SessionTypes.Types.Cap (s' : ctx') s') ('Control.SessionTypes.Types.Cap (norm : nctx) norm) => Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap (s : ctx) 'Control.SessionTypes.Types.V) ('Control.SessionTypes.Types.Cap (s' : ctx') 'Control.SessionTypes.Types.V) ('Control.SessionTypes.Types.Cap (norm : nctx) 'Control.SessionTypes.Types.V)
instance forall a a1 (ctx :: [Control.SessionTypes.Types.ST a1]) (nctx :: [Control.SessionTypes.Types.ST a]). Control.SessionTypes.Normalize.Flatten' ('Control.SessionTypes.Types.Cap ctx 'Control.SessionTypes.Types.Eps) ('Control.SessionTypes.Types.Cap ctx 'Control.SessionTypes.Types.Eps) ('Control.SessionTypes.Types.Cap nctx 'Control.SessionTypes.Types.Eps)


-- | This module defines a new type for constructing more efficient
--   <a>STTerm</a> programs.
module Control.SessionTypes.Codensity

-- | We define an indexed codensity monad that allows us to reduce
--   quadratic complexity from repeated use of (&gt;&gt;=) in a session
--   typed program to linear complexity.
newtype IxC m s r a
IxC :: (forall b k. (a -> STTerm m r k b) -> STTerm m s k b) -> IxC m s r a
[runIxC] :: IxC m s r a -> forall b k. (a -> STTerm m r k b) -> STTerm m s k b

-- | Turns the <a>IxC</a> representation of a program to the <a>STTerm</a>
--   representation.
--   
--   The idea is to apply <a>abs</a> on a <a>IxC</a> program to make the
--   resulting <a>STTerm</a> program more efficient.
abs :: Monad m => IxC m s r a -> STTerm m s r a

-- | Transforms an <a>STTerm</a> program into a <a>IxC</a> representation.
--   
--   Note that applying this function to a session typed program and then
--   applying <a>abs</a> to the result will not be more efficient.
--   
--   This is because applying <a>rep</a> already induces quadratic
--   complexity.
rep :: Monad m => STTerm m s r a -> IxC m s r a
instance Control.SessionTypes.Indexed.IxFunctor (Control.SessionTypes.Codensity.IxC m)
instance Control.SessionTypes.Indexed.IxApplicative (Control.SessionTypes.Codensity.IxC m)
instance Control.SessionTypes.Indexed.IxMonad (Control.SessionTypes.Codensity.IxC m)
instance GHC.Base.Monad m => Control.SessionTypes.MonadSession.MonadSession (Control.SessionTypes.Codensity.IxC m)


-- | This packages provides a deep embedded domain-specific language for
--   writing session typed program.
--   
--   A session typed program is a program annotated with session types. A
--   session type describes a communication protocol at the type-level.
--   
--   The motivation for doing so is that it gives you a static guarantee
--   that a program correctly implements a protocol. It may even guarantee
--   that no deadlocking can occur.
--   
--   The following constitutes the most important parts of this library for
--   writing session typed programs.
--   
--   <ul>
--   <li><a>STTerm</a>: A GADT representing the terms of the DSL. The
--   constructors represent the different session types and are annotated
--   with session types.</li>
--   <li><a>ST</a>: A protomoted data type describing the different session
--   types.</li>
--   <li><a>MonadSession</a>: A type class exposing the interface of the
--   DSL.</li>
--   <li><a>Control.SessionTypes.Indexed</a>: A custom prelude module
--   replacing common type classes with indexed type classes</li>
--   </ul>
--   
--   This package also implements a couple interpreters that evaluate an
--   abstract-syntax tree consisting of <a>STTerm</a> constructors:
--   
--   <ul>
--   <li><a>Control.SessionTypes.Debug</a>: Purely evaluation</li>
--   <li><a>Control.SessionTypes.Interactive</a>: Interactive
--   evaluation</li>
--   <li><a>Control.SessionTypes.Normalize</a>: Rewrites <a>STTerm</a>
--   programs to a normal form</li>
--   <li><a>Control.SessionTypes.Visualize</a>: Visualizes a session
--   type</li>
--   </ul>
module Control.SessionTypes

-- | The STTerm GADT
--   
--   Although we say that a <a>STTerm</a> is annotated with a session type,
--   it is actually annotated with a capability (<a>Cap</a>).
--   
--   The capability contains a context that is necessary for recursion and
--   the session type.
--   
--   The constructors can be split in four different categories:
--   
--   <ul>
--   <li>Communication: <a>Send</a> and <a>Recv</a> for basic
--   communication</li>
--   <li>Branching: <a>Sel1</a>, <a>Sel2</a>, <a>OffZ</a> and
--   <a>OffS</a></li>
--   <li>Recursion: <a>Rec</a>, <a>Weaken</a> and <a>Var</a></li>
--   <li>Unsession typed: <a>Ret</a> and <a>Lift</a></li>
--   </ul>
data STTerm :: (Type -> Type) -> Cap a -> Cap a -> Type -> Type

-- | The constructor for sending messages. It is annotated with the send
--   session type (<a>:!&gt;</a>).
--   
--   It takes as an argument, the message to send, of type equal to the
--   first argument of <a>:!&gt;</a> and the continuing <a>STTerm</a> that
--   is session typed with the second argument of <a>:!&gt;</a>.
[Send] :: a -> STTerm m (Cap ctx r) r' b -> STTerm m (Cap ctx (a :!> r)) r' b

-- | The constructor for receiving messages. It is annotated with the
--   receive session type (<a>:?&gt;</a>)
--   
--   It takes a continuation that promises to deliver a value that may be
--   used in the rest of the program.
[Recv] :: (a -> STTerm m (Cap ctx r) r' b) -> STTerm m (Cap ctx (a :?> r)) r' b

-- | Selects the first branch in a selection session type.
--   
--   By selecting a branch, that selected session type must then be
--   implemented.
[Sel1] :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Sel (s : xs))) r a

-- | Skips a branch in a selection session type.
--   
--   If the first branch in the selection session type is not the one we
--   want to implement then we may use <a>Sel2</a> to skip this.
[Sel2] :: STTerm m (Cap ctx (Sel (t : xs))) r a -> STTerm m (Cap ctx (Sel (s : (t : xs)))) r a

-- | Dually to selection there is also offering branches.
--   
--   Unlike selection, where we may only implement one branch, an offering
--   asks you to implement all branches. Which is chosen depends on how an
--   interpreter synchronizes selection with offering.
--   
--   This constructor denotes the very last branch that may be offered.
[OffZ] :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Off '[s])) r a

-- | offers a branch and promises at least one more branch to be offered.
[OffS] :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Off (t : xs))) r a -> STTerm m (Cap ctx (Off (s : (t : xs)))) r a

-- | Constructor for delimiting the scope of recursion
--   
--   The recursion constructors also modify or at least make use of the
--   context in the capability.
--   
--   The <a>Rec</a> constructor inserts the session type argument to
--   <a>R</a> into the context of the capability of its <a>STTerm</a>
--   argument.
--   
--   This is necessary such that we remember the session type of the body
--   of code that we may want to recurse over and thus avoiding infinite
--   type occurrence errors.
[Rec] :: STTerm m (Cap (s : ctx) s) r a -> STTerm m (Cap ctx (R s)) r a

-- | Constructor for weakening (expanding) the scope of recusion
--   
--   This constructor does the opposite of <a>R</a> by popping a session
--   type from the context.
--   
--   Use this constructor to essentially exit a recursion
[Weaken] :: STTerm m (Cap ctx t) r a -> STTerm m (Cap (s : ctx) (Wk t)) r a

-- | Constructor that denotes the recursion variable
--   
--   It assumes the context to be non-empty and uses the session type at
--   the top of the context to determine what should be implemented after
--   <a>Var</a>.
[Var] :: STTerm m (Cap (s : ctx) s) t a -> STTerm m (Cap (s : ctx) V) t a

-- | Constructor that makes <a>STTerm</a> a (indexed) monad
[Ret] :: (a :: Type) -> STTerm m s s a

-- | Constructor that makes <a>STTerm</a> a (indexed) monad transformer
[Lift] :: m (STTerm m s r a) -> STTerm m s r a

-- | This function can be used if we do not use <tt>lift</tt> in a program
--   but we must still disambiguate <tt>m</tt>.
inferIdentity :: STTerm Identity s r a -> STTerm Identity s r a

-- | The <a>MonadSession</a> type class exposes a set of functions that
--   composed together form a session typed program
--   
--   A type that is an instance of <a>MonadSession</a> must therefore also
--   be an instance of <a>IxMonad</a>.
--   
--   The functions themselves are generally defined as wrappers over
--   corresponding <tt>STTerm</tt> constructors.
class IxMonad m => MonadSession m
send :: MonadSession m => a -> m (Cap ctx (a :!> r)) (Cap ctx r) ()
recv :: MonadSession m => m (Cap ctx (a :?> r)) (Cap ctx r) a
sel1 :: MonadSession m => m (Cap ctx (Sel (s : xs))) (Cap ctx s) ()
sel2 :: MonadSession m => m (Cap ctx (Sel (s : (t : xs)))) (Cap ctx (Sel (t : xs))) ()
offZ :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx (Off '[s])) r a
offS :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx (Off (t : xs))) r a -> m (Cap ctx (Off (s : (t : xs)))) r a
recurse :: MonadSession m => m (Cap (s : ctx) s) r a -> m (Cap ctx (R s)) r a
weaken :: MonadSession m => m (Cap ctx s) r a -> m (Cap (t : ctx) (Wk s)) r a
var :: MonadSession m => m (Cap (s : ctx) s) r a -> m (Cap (s : ctx) V) r a
eps :: MonadSession m => a -> m (Cap ctx Eps) (Cap ctx Eps) a

-- | A session typed program that is polymorphic in its context can often
--   not be used by interpreters.
--   
--   We can apply <a>empty</a> to the session typed program before passing
--   it to an interpreter to instantiate that the context is empty.
empty :: MonadSession m => m (Cap '[] s) r a -> m (Cap '[] s) r a

-- | Monadic composable definition of <a>empty</a>
--   
--   Prefix a session typed program with (empty &gt;&gt;) to instantiate
--   the context to be empty.
empty0 :: MonadSession m => m (Cap '[] r) (Cap '[] r) ()

-- | Allows indexing of selections.
--   
--   The given <a>Ref</a> type can be used as an indexed to select a
--   branch. This circumvents the need to sequence a bunch of <a>sel1</a>
--   and <a>sel2</a> to select a branch.
--   
--   <pre>
--   prog :: MonadSession m =&gt; m ('Cap ctx (Sel '[a,b,c,d])) ('Cap ctx Eps) ()
--   
--   MonadSession m =&gt; m ('Cap ctx b) ('Cap ctx Eps) ()
--   prog2 = prog &gt;&gt; selN (RefS RefZ)
--   </pre>
selN :: MonadSession m => Ref s xs -> m (Cap ctx (Sel xs)) (Cap ctx s) ()

-- | Select the first branch of a selection.
selN1 :: MonadSession m => m (Cap ctx (Sel (s : xs))) (Cap ctx s) ()

-- | Select the second branch of a selection.
selN2 :: MonadSession m => m (Cap ctx (Sel (s : (t : xs)))) (Cap ctx t) ()

-- | Select the third branch of a selection.
selN3 :: MonadSession m => m (Cap ctx (Sel (s : (t : (k : xs))))) (Cap ctx k) ()

-- | Select the fourth branch of a selection.
selN4 :: MonadSession m => m (Cap ctx (Sel (s : (t : (k : (r : xs)))))) (Cap ctx r) ()

-- | Type class for selecting a branch through injection.
--   
--   Selects the first branch that matches the given session type.
--   
--   <pre>
--   prog :: MonadSession m =&gt; m ('Cap ctx (Sel '[Eps, String :!&gt; Eps, Int :!&gt; Eps])) ('Cap ctx Eps) ()
--   prog = sel &gt;&gt; send "c" &gt;&gt;= eps
--   </pre>
--   
--   It should be obvious that you cannot select a branch using <a>sel</a>
--   if that branch has the same session type as a previous branch.
class Select xs s
sel :: (Select xs s, MonadSession m) => m (Cap ctx (Sel xs)) (Cap ctx s) ()

-- | Infix synonym for <a>offS</a>
(<&) :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx (Off (t : xs))) r a -> m (Cap ctx (Off (s : (t : xs)))) r a
infixr 1 <&

-- | Infix synonym for <a>offer</a>
--   
--   Using both <a>&lt;&amp;</a> and <a>&lt;&amp;&gt;</a> we can now
--   construct an offering as follows:
--   
--   <pre>
--   branch1 
--   &lt;&amp; branch2
--   &lt;&amp; branch3
--   &lt;&amp;&gt; branch4
--   </pre>
--   
--   This will be parsed as
--   
--   <pre>
--   (branch1
--    &lt;&amp; (branch2
--    &lt;&amp; (branch3
--    &lt;&amp;&gt; branch4)))
--   </pre>
(<&>) :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a
infix 2 <&>

-- | Takes two session typed programs and constructs an offering consisting
--   of two branches
offer :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a

-- | A fixpoint combinator for recursion
--   
--   The argument function must take a recursion variable as an argument
--   that can be used to denote the point of recursion.
--   
--   For example:
--   
--   <pre>
--   prog = recurseFix \f -&gt; do
--    send 5
--    f
--   </pre>
--   
--   This program will send the number 5 an infinite amount of times.
recurseFix :: MonadSession m => (m (Cap (s : ctx) V) r a -> m (Cap (s : ctx) s) r a) -> m (Cap ctx (R s)) r a

-- | Monadic composable definition of <a>recurse</a>
recurse0 :: MonadSession m => m (Cap ctx (R s)) (Cap (s : ctx) s) ()

-- | Monadic composable definition of <a>weaken</a>
weaken0 :: MonadSession m => m (Cap (t : ctx) (Wk s)) (Cap ctx s) ()

-- | Monadic composable definition of <a>var</a>
var0 :: MonadSession m => m (Cap (s : ctx) V) (Cap (s : ctx) s) ()

-- | Monadic composable definition of <a>eps</a>
eps0 :: MonadSession m => m (Cap ctx Eps) (Cap ctx Eps) ()

-- | The session type data type
--   
--   Each constructor denotes a specific session type. Using the
--   <tt>DataKinds</tt> pragma the constructors are promoted to types and
--   <a>ST</a> is promoted to a kind.
data ST a

-- | Send a value
(:?>) :: a -> (ST a) -> ST a

-- | Recv a value
(:!>) :: a -> (ST a) -> ST a

-- | Selection of branches
Sel :: [ST a] -> ST a

-- | Offering of branches
Off :: [ST a] -> ST a

-- | Delimit the scope of recursion
R :: (ST a) -> ST a

-- | Weaken the scope of recursion
Wk :: (ST a) -> ST a

-- | Recursion variable
V :: ST a

-- | End of the session
Eps :: ST a

-- | A capability that stores a context/scope that is a list of session
--   types and a session type
data Cap a
Cap :: [ST a] -> (ST a) -> Cap a

-- | Retrieves the session type from the capability

-- | Retrieves the context from the capability

-- | Type family for calculating the dual of a session type. It may be
--   applied to a capability.
--   
--   We made <a>Dual</a> injective to support calculating the dual of a
--   selection that contains an ambiguous branch. Of course that does
--   require that the dual of that ambiguous branch must be known.

-- | Type family for calculating the dual of a session type. It may be
--   applied to the actual session type.

-- | Type family for calculating the dual of a list of session types.

-- | Type family for removing the send session type from the given session
--   type. It may be applied to a capability.

-- | Type family for removing the send session type from the given session
--   type. It may be applied to a session type.

-- | Type family for removing the send session type from a list of session
--   types.

-- | Type family for removing the receive session type from the given
--   session type. It may be applied to a capability.

-- | Type family for removing the receive session type from a list of
--   session types.

-- | Type family for removing the receive session type from the given
--   session type. It may be applied to a session type.

-- | Type family for applying a constraint to types of kind <a>Type</a> in
--   a session type. It may be applied to a capability.

-- | Type family for applying a constraint to types of kind <a>Type</a> in
--   a list of session types.

-- | Type family for applying a constraint to types of kind <a>Type</a> in
--   a session type. It may be applied to a session type.

-- | Type family for applying zero or more constraints to types of kind
--   <a>Type</a> in a list of session types. It may be applied to a
--   capability.

-- | Promoted <tt>ifThenElse</tt>

-- | Promoted <a>not</a>

-- | Promoted <a>||</a>

-- | Data type that takes a kind as an argument. Its sole constructor takes
--   two capabilities parameterized by the kind argument.
--   
--   This data type is useful if it is necessary for an indexed monad to be
--   indexed by four parameters.
data Prod t
(:*:) :: (Cap t) -> (Cap t) -> Prod t

-- | Type family for returning the first argument of a product.

-- | Type family for returning the second argument of a product.

-- | Data type defining natural numbers
data Nat
Z :: Nat
S :: Nat -> Nat

-- | Data type that can give us proof of membership of an element in a list
--   of elements.
data Ref s xs
[RefZ] :: Ref s (s : xs)
[RefS] :: Ref s (k : xs) -> Ref s (t : (k : xs))

-- | Type family for computing which types in a list of types are equal to
--   a given type.

-- | Promoted <a>++</a>


-- | This module describes an interpreter for purely evaluating session
--   typed programs
--   
--   that is based on the paper <i>Beauty in the beast</i> by <i>Swierstra,
--   W., &amp; Altenkirch, T.</i>
--   
--   Impurity in a session typed programs mainly comes from three things:
--   receives, branching and lifting.
--   
--   Using the session type we can easily determine the type of the message
--   that each receive should expect.
--   
--   This information allows us to define a stream of values of different
--   types that provides input for each receive.
--   
--   In the sessiontyped-distributed library we send and receive booleans
--   to enable branching.
--   
--   It is also possible to provide some kind of input that makes this
--   choice.
--   
--   The current structure of the <a>Lift</a> constructor does not allow us
--   to purely evaluate a <a>Lift</a>.
--   
--   As such a session typed program may not contain a lift for it to be
--   purely evaluated. See <a>runM</a> as an alternative.
module Control.SessionTypes.Debug

-- | Purely evaluates a given <a>STTerm</a> using the input defined by
--   <a>Stream</a>.
--   
--   The output is described in terms of the session type actions within
--   the given program
--   
--   An example of how to use this function goes as follows:
--   
--   <pre>
--   prog :: STTerm Identity ('Cap '[] (Int :!&gt; String :?&gt; Eps)) ('Cap '[] Eps) String
--   prog = send 5 &gt;&gt; recv &gt;&gt;= eps
--   
--   strm = S_Send $ S_Recv "foo" S_Eps
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; run prog strm
--   O_Send 5 $ O_Recv "foo" $ O_Eps "foo"
--   </pre>
run :: HasConstraint Show s => STTerm m s (Cap ctx Eps) a -> Stream s -> Output s a

-- | Instead of describing the session typed actions, it returns a list of
--   the results of all branches of all offerings.
--   
--   <pre>
--   prog = offer (eps 10) (eps 5)
--   strm = S_OffS S_Eps S_Eps
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; runAll prog strm
--   [10,5]
--   </pre>
runAll :: HasConstraint Show s => STTerm m s (Cap ctx Eps) a -> Stream s -> [a]

-- | Same as <a>runAll</a> but applies <a>head</a> to the resulting list
--   
--   <pre>
--   &gt;&gt;&gt; runSingle prog strm
--   10
--   </pre>
runSingle :: HasConstraint Show s => STTerm m s (Cap ctx Eps) a -> Stream s -> a

-- | <a>run</a> cannot deal with lifted computations. This makes it limited
--   to session typed programs without any use of lift.
--   
--   This function allows us to evaluate lifted computations, but as a
--   consequence is no longer entirely pure.
runM :: (Monad m, HasConstraint Show s) => STTerm m s (Cap ctx Eps) a -> Stream s -> m (Output s a)

-- | Monadic version of <a>runAll</a>.
runAllM :: (Monad m, HasConstraint Show s) => STTerm m s (Cap ctx Eps) a -> Stream s -> m [a]

-- | Monad version of <a>runSingle</a>
runSingleM :: (Monad m, HasConstraint Show s) => STTerm m s (Cap ctx Eps) a -> Stream s -> m a

-- | We use the <a>Stream</a> data type to supply input for the receives in
--   a session typed programs.
--   
--   We annotate a <a>Stream</a> with a capability for the following three
--   reasons:
--   
--   <ol>
--   <li>Each <a>recv</a> may return a value of a different type.</li>
--   <li>Given reason 1 and that we can have branching, we must also be
--   able to branch in the stream.</li>
--   <li>We can now write a function that recursively generates input for a
--   recursive program</li>
--   </ol>
--   
--   Similar to <a>STTerm</a>, <a>Stream</a> has a constructor for each
--   session type. Each constructor takes an argument that is another
--   <a>Stream</a> type, except for <a>S_Recv</a> that takes an additional
--   argument that will be used as input, and <a>S_Eps</a> that denotes the
--   end of the stream.
--   
--   At first it might be confusing which constructors and in what order
--   these constructors should be placed to form a <a>Stream</a> that can
--   be used as input for some <a>STTerm</a>.
--   
--   This is actually not that difficult at all. A <a>Stream</a> is session
--   typed and that session type must be equal to the session type of the
--   <a>STTerm</a>. As such one merely needs to create a <a>Stream</a> that
--   has the same session type and if you don't the type checker will tell
--   you what it incorrect.
--   
--   There are two things that you need to be aware of when constructor a
--   <a>Stream</a>.
--   
--   <ul>
--   <li>The <a>Stream</a> constructors for offering (S_OffZ and S_OffS)
--   require that you define input for all branches of the offering. This
--   can be quite cumbersome, so we include a <a>S_Off1</a> and
--   <a>S_Off2</a> constructor that behave similarly to <a>S_Sel1</a> and
--   <a>S_Sel2</a>.</li>
--   <li>You are not guaranteed that a <a>Stream</a> can be used for all
--   session typed programs that have the same session type. Specifically
--   when it comes to selection can we not guarantee this. The session type
--   for selection only tells us about which branches could be selected. It
--   does not tell us which branch was selected as this is runtime
--   dependent.</li>
--   </ul>
data Stream :: Cap Type -> Type
[S_Send] :: Stream (Cap ctx s) -> Stream (Cap ctx (a :!> s))
[S_Recv] :: a -> Stream (Cap ctx s) -> Stream (Cap ctx (a :?> s))
[S_Sel1] :: Stream (Cap ctx s) -> Stream (Cap ctx (Sel (s : xs)))
[S_Sel2] :: Stream (Cap ctx (Sel (t : xs))) -> Stream (Cap ctx (Sel (s : (t : xs))))
[S_OffZ] :: Stream (Cap ctx s) -> Stream (Cap ctx (Off '[s]))
[S_OffS] :: Stream (Cap ctx s) -> Stream (Cap ctx (Off (t : xs))) -> Stream (Cap ctx (Off (s : (t : xs))))
[S_Off1] :: Stream (Cap ctx s) -> Stream (Cap ctx (Off (s : xs)))
[S_Off2] :: Stream (Cap ctx (Off (t : xs))) -> Stream (Cap ctx (Off (s : (t : xs))))
[S_Rec] :: Stream (Cap (s : ctx) s) -> Stream (Cap ctx (R s))
[S_Weaken] :: Stream (Cap ctx s) -> Stream (Cap (t : ctx) (Wk s))
[S_Var] :: Stream (Cap (s : ctx) s) -> Stream (Cap (s : ctx) V)
[S_Eps] :: Stream (Cap '[] Eps)

-- | The <a>Output</a> data type describes the session type actions that
--   were done
data Output :: Cap Type -> Type -> Type
[O_Send] :: a -> Output (Cap ctx r) b -> Output (Cap ctx (a :!> r)) b
[O_Recv] :: a -> Output (Cap ctx r) b -> Output (Cap ctx (a :?> r)) b
[O_Sel1] :: Output (Cap ctx s) b -> Output (Cap ctx (Sel (s : xs))) b
[O_Sel2] :: Output (Cap ctx (Sel xs)) b -> Output (Cap ctx (Sel (s : xs))) b
[O_OffZ] :: Output (Cap ctx s) a -> Output (Cap ctx (Off '[s])) a
[O_OffS] :: Output (Cap ctx s) b -> Output (Cap ctx (Off (t : xs))) b -> Output (Cap ctx (Off (s : (t : xs)))) b
[O_Off1] :: Output (Cap ctx s) a -> Output (Cap ctx (Off (s : xs))) a
[O_Off2] :: Output (Cap ctx (Off (t : xs))) a -> Output (Cap ctx (Off (s : (t : xs)))) a
[O_Rec] :: Output (Cap (s : ctx) s) b -> Output (Cap ctx (R s)) b
[O_Var] :: Output (Cap (s : ctx) s) b -> Output (Cap (s : ctx) V) b
[O_Weaken] :: Output (Cap ctx s) b -> Output (Cap (t : ctx) (Wk s)) b
[O_Eps] :: b -> Output (Cap ctx Eps) b
[O_Lift] :: Output s b -> Output s b
instance (Control.SessionTypes.Types.HasConstraint GHC.Show.Show s, GHC.Show.Show a) => GHC.Show.Show (Control.SessionTypes.Debug.Output s a)
instance (Control.SessionTypes.Types.HasConstraint GHC.Classes.Eq s, GHC.Classes.Eq a) => GHC.Classes.Eq (Control.SessionTypes.Debug.Output s a)
instance Control.SessionTypes.Types.HasConstraint GHC.Show.Show s => GHC.Show.Show (Control.SessionTypes.Debug.Stream s)
instance Control.SessionTypes.Types.HasConstraint GHC.Classes.Eq s => GHC.Classes.Eq (Control.SessionTypes.Debug.Stream s)
instance (Control.SessionTypes.Types.HasConstraint Control.DeepSeq.NFData s, Control.DeepSeq.NFData a) => Control.DeepSeq.NFData (Control.SessionTypes.Debug.Output s a)
instance Control.SessionTypes.Types.HasConstraint Control.DeepSeq.NFData s => Control.DeepSeq.NFData (Control.SessionTypes.Debug.Stream s)