module DDC.Type.Exp.Simple.Exp
        ( Binder        (..)
        , Bind          (..)
        , Bound         (..)
        , Type          (..)
        , Sort
        , Kind
        , Region
        , Effect
        , Closure
        , TypeSum       (..)
        , TyConHash     (..)
        , TypeSumVarCon (..)
        , TyCon         (..)
        , SoCon         (..)
        , KiCon         (..)
        , TwCon         (..)
        , TcCon         (..))
where
import DDC.Type.Exp.TyCon
import Data.Array
import Data.Map.Strict  (Map)
import Data.Set         (Set)


-- Binder ---------------------------------------------------------------------
data Binder n
        = RNone
        | RAnon
        | RName !n
        deriving Show


-- Bind -----------------------------------------------------------------------
-- | A variable binder with its type.
data Bind n
        -- | A variable with no uses in the body doesn't need a name.
        = BNone     !(Type n)

        -- | Nameless variable on the deBruijn stack.
        | BAnon     !(Type n)

        -- | Named variable in the environment.
        | BName n   !(Type n)
        deriving Show



-- | A bound occurrence of a variable, with its type.
--
--   If variable hasn't been annotated with its real type then this 
--   can be `tBot` (an empty sum).

data Bound n
        -- | Nameless variable that should be on the deBruijn stack.
        = UIx   !Int   

        -- | Named variable that should be in the environment.
        | UName !n

        -- | Named primitive that has its type attached to it.
        --   The types of primitives must be closed.
        | UPrim !n !(Type n)
        deriving Show


-- Types ----------------------------------------------------------------------
-- | A value type, kind, or sort.
--
--   We use the same data type to represent all three universes, as they have
--   a similar algebraic structure.
--
data Type n
        -- | Constructor.
        = TCon    !(TyCon n)

        -- | Variable.
        | TVar    !(Bound n)

        -- | Abstraction.
        | TAbs    !(Bind  n) !(Type  n)
        
        -- | Application.
        | TApp    !(Type  n) !(Type  n)

        -- | Universal Quantification.
        | TForall !(Bind  n) !(Type  n)

        -- | Least upper bound.
        | TSum    !(TypeSum n)
        deriving Show


-- | Sorts are types at level 3.
type Sort    n = Type n

-- | Kinds are types at level 2
type Kind    n = Type n

-- | Alias for region types.
type Region  n = Type n

-- | Alias for effect types.
type Effect  n = Type n

-- | Alias for closure types.
type Closure n = Type n


-- Type Sums ------------------------------------------------------------------
-- | A least upper bound of several types.
-- 
--   We keep type sums in this normalised format instead of joining them
--   together with a binary operator (like @(+)@). This makes sums easier to work
--   with, as a given sum type often only has a single physical representation.
data TypeSum n
        = TypeSumBot
        { typeSumKind           :: !(Kind n) }

        | TypeSumSet
        { -- | The kind of the elements in this sum.
          typeSumKind           :: !(Kind n)

          -- | Where we can see the outer constructor of a type, its argument
          --   is inserted into this array. This handles common cases like
          --   Read, Write, Alloc effects.
        , typeSumElems          :: !(Array TyConHash (Set (TypeSumVarCon n)))

          -- | A map for named type variables.
        , typeSumBoundNamed     :: !(Map n   (Kind n))

          -- | A map for anonymous type variables.
        , typeSumBoundAnon      :: !(Map Int (Kind n))

          -- | Types that can't be placed in the other fields go here.
          -- 
          --   INVARIANT: this list doesn't contain more `TSum`s.
        , typeSumSpill          :: ![Type n] }
        deriving Show
        

-- | Hash value used to insert types into the `typeSumElems` array of a `TypeSum`.
data TyConHash 
        = TyConHash !Int
        deriving (Eq, Show, Ord, Ix)


-- | Wraps a variable or constructor that can be added the `typeSumElems` array.
data TypeSumVarCon n
        = TypeSumVar !(Bound n)
        | TypeSumCon !(Bound n) !(Kind n)
        deriving Show


-- TyCon ----------------------------------------------------------------------
-- | Kind, type and witness constructors.
--
--   These are grouped to make it easy to determine the universe that they
--   belong to.
-- 
data TyCon n
        -- | (level 3) Builtin Sort constructors.
        = TyConSort     !SoCon

        -- | (level 2) Builtin Kind constructors.
        | TyConKind     !KiCon

        -- | (level 1) Builtin Spec constructors for the types of witnesses.
        | TyConWitness  !TwCon

        -- | (level 1) Builtin Spec constructors for types of other kinds.
        | TyConSpec     !TcCon

        -- | User defined type constructor.
        | TyConBound    !(Bound n) !(Kind n)

        -- | An existentially quantified name, with its kind.
        --   Used during type checking, but not accepted in source programs.
        | TyConExists   !Int       !(Kind n)
        deriving Show