SessionTypes.hs

-- | 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.
--
-- * `STTerm`: A GADT representing the terms of the DSL. The constructors represent the different session types and are annotated with session types.
-- * `ST`: A protomoted data type describing the different session types.
-- * `MonadSession`: A type class exposing the interface of the DSL.
-- * "Control.SessionTypes.Indexed": A custom prelude module replacing common type classes with indexed type classes
--
-- This package also implements a couple interpreters that evaluate an abstract-syntax tree consisting of `STTerm` constructors:
--
-- * "Control.SessionTypes.Debug": Purely evaluation
-- * "Control.SessionTypes.Interactive": Interactive evaluation
-- * "Control.SessionTypes.Normalize": Rewrites `STTerm` programs to a normal form
-- * "Control.SessionTypes.Visualize": Visualizes a session type
module Control.SessionTypes (
  -- * STTerm
  STTerm (..),
  inferIdentity,
  -- * MonadSession
  -- ** Primitives
  MonadSession (..),
  -- ** Combinators
  empty,
  empty0,
  selN,
  selN1,
  selN2,
  selN3,
  selN4,
  Select(sel),
  (<&),
  (<&>),
  offer,
  recurseFix,
  recurse0,
  weaken0,
  var0,
  eps0,
  -- * Types
  -- ** Session Types
  ST(..),
  Cap(..),
  GetST,
  GetCtx,
  -- ** Duality
  Dual,
  DualST,
  MapDual,
  -- ** Removing
  RemoveSend,
  RemoveSendST,
  MapRemoveSend,
  RemoveRecv,
  RemoveRecvST,
  MapRemoveRecv,
  -- ** Applying Constraints
  HasConstraint,
  HasConstraintST,
  MapHasConstraint,
  HasConstraints,
  -- ** Boolean functions
  IfThenElse,
  Not,
  Or,
  -- ** Product type
  Prod (..),
  Left,
  Right,
  -- ** Other
  Nat(..),
  Ref(..),
  TypeEqList,
  Append
) where

import Control.SessionTypes.STTerm (
  STTerm (..),
  inferIdentity
  )
import Control.SessionTypes.Types (
  ST(..),
  Cap(..),
  GetST,
  GetCtx,
  Dual,
  DualST,
  MapDual,
  RemoveSend,
  RemoveSendST,
  MapRemoveSend,
  RemoveRecv,
  RemoveRecvST,
  MapRemoveRecv,
  HasConstraint,
  HasConstraintST,
  MapHasConstraint,
  HasConstraints,
  IfThenElse,
  Not,
  Or,
  Prod (..),
  Left,
  Right,
  Nat(..),
  Ref(..),
  TypeEqList,
  Append
  )
import Control.SessionTypes.MonadSession (
  MonadSession (..),
  empty,
  empty0,
  selN,
  selN1,
  selN2,
  selN3,
  selN4,
  Select(sel),
  (<&),
  (<&>),
  offer,
  recurseFix,
  recurse0,
  weaken0,
  var0,
  eps0
  )