-- | Core language AST that includes an annotation on every node of 
--   an expression.
--
--   This is the default representation for Disciple Core, and should be preferred
--   over the 'Simple' version of the AST in most cases. 
--
--   * Local transformations on this AST should propagate the annotations in a way that
--   would make sense if they were source position identifiers that tracked the provenance
--   of each code snippet. If the specific annotations attached to the AST would not make
--   sense after such a transformation, then the client should erase them to @()@ beforehand
--   using the `reannotate` transform.
--
--   * Global transformations that drastically change the provenance of code snippets should
--     accept an AST with an arbitrary annotation type, but produce one with the annotations
--     set to @()@.
--
module DDC.Core.Exp.Annot 
        ( module DDC.Type.Exp

         -- * Expressions
        , Exp           (..)
        , Lets          (..)
        , Alt           (..)
        , Pat           (..)
        , Cast          (..)

          -- * Witnesses
        , Witness       (..)

          -- * Data Constructors
        , DaCon         (..)

          -- * Witness Constructors
        , WiCon         (..)
        , WbCon         (..))
where
import DDC.Core.Exp.WiCon
import DDC.Core.Exp.DaCon
import DDC.Core.Exp.Pat
import DDC.Type.Exp
import DDC.Type.Sum             ()
import Control.DeepSeq


-- Values ---------------------------------------------------------------------
-- | Well-typed expressions have types of kind `Data`.
data Exp a n
        -- | Value variable   or primitive operation.
        = XVar     !a !(Bound n)

        -- | Data constructor or literal.
        | XCon     !a !(DaCon n)

        -- | Type abstraction (level-1).
        | XLAM     !a !(Bind n)   !(Exp a n)

        -- | Value and Witness abstraction (level-0).
        | XLam     !a !(Bind n)   !(Exp a n)

        -- | Application.
        | XApp     !a !(Exp a n)  !(Exp a n)

        -- | Possibly recursive bindings.
        | XLet     !a !(Lets a n) !(Exp a n)

        -- | Case branching.
        | XCase    !a !(Exp a n)  ![Alt a n]

        -- | Type cast.
        | XCast    !a !(Cast a n) !(Exp a n)

        -- | Type can appear as the argument of an application.
        | XType    !a !(Type n)

        -- | Witness can appear as the argument of an application.
        | XWitness !a !(Witness a n)
        deriving (Show, Eq)


-- | Possibly recursive bindings.
data Lets a n
        -- | Non-recursive expression binding.
        = LLet     !(Bind n) !(Exp a n)

        -- | Recursive binding of lambda abstractions.
        | LRec     ![(Bind n, Exp a n)]

        -- | Bind a private region variable,
        --   and witnesses to its properties.
        | LPrivate ![Bind n] !(Maybe (Type n)) ![Bind n]
        
        -- | Holds a region handle during evaluation.
        | LWithRegion !(Bound n)
        deriving (Show, Eq)


-- | Case alternatives.
data Alt a n
        = AAlt !(Pat n) !(Exp a n)
        deriving (Show, Eq)


-- | Type casts.
data Cast a n
        -- | Weaken the effect of an expression.
        --   The given effect is added to the effect
        --   of the body.
        = CastWeakenEffect  !(Effect n)
        
        -- | Weaken the closure of an expression.
        --   The closures of these expressions are added to the closure
        --   of the body.
        | CastWeakenClosure ![Exp a n]

        -- | Purify the effect (action) of an expression.
        | CastPurify !(Witness a n)

        -- | Forget about the closure (sharing) of an expression.
        | CastForget !(Witness a n)

        -- | Box up a computation, 
        --   capturing its effects in the S computation type.
        | CastBox 

        -- | Run a computation,
        --   releasing its effects into the environment.
        | CastRun
        deriving (Show, Eq)


-- | When a witness exists in the program it guarantees that a
--   certain property of the program is true.
data Witness a n
        -- | Witness variable.
        = WVar  a !(Bound n)
        
        -- | Witness constructor.
        | WCon  a !(WiCon n)
        
        -- | Witness application.
        | WApp  a !(Witness a n) !(Witness a n)

        -- | Joining of witnesses.
        | WJoin a !(Witness a n) !(Witness a n)

        -- | Type can appear as the argument of an application.
        | WType a !(Type n)
        deriving (Show, Eq)


-- NFData ---------------------------------------------------------------------
instance (NFData a, NFData n) => NFData (Exp a n) where
 rnf xx
  = case xx of
        XVar  a u       -> rnf a `seq` rnf u
        XCon  a dc      -> rnf a `seq` rnf dc
        XLAM  a b x     -> rnf a `seq` rnf b   `seq` rnf x
        XLam  a b x     -> rnf a `seq` rnf b   `seq` rnf x
        XApp  a x1 x2   -> rnf a `seq` rnf x1  `seq` rnf x2
        XLet  a lts x   -> rnf a `seq` rnf lts `seq` rnf x
        XCase a x alts  -> rnf a `seq` rnf x   `seq` rnf alts
        XCast a c x     -> rnf a `seq` rnf c   `seq` rnf x
        XType a t       -> rnf a `seq` rnf t
        XWitness a w    -> rnf a `seq` rnf w


instance (NFData a, NFData n) => NFData (Cast a n) where
 rnf cc
  = case cc of
        CastWeakenEffect e      -> rnf e
        CastWeakenClosure xs    -> rnf xs
        CastPurify w            -> rnf w
        CastForget w            -> rnf w
        CastBox                 -> ()
        CastRun                 -> ()


instance (NFData a, NFData n) => NFData (Lets a n) where
 rnf lts
  = case lts of
        LLet b x                -> rnf b `seq` rnf x
        LRec bxs                -> rnf bxs
        LPrivate bs1 u2 bs3     -> rnf bs1 `seq` rnf u2 `seq` rnf bs3
        LWithRegion u           -> rnf u


instance (NFData a, NFData n) => NFData (Alt a n) where
 rnf aa
  = case aa of
        AAlt w x                -> rnf w `seq` rnf x


instance (NFData a, NFData n) => NFData (Witness a n) where
 rnf ww
  = case ww of
        WVar  a u                 -> rnf a `seq` rnf u
        WCon  a c                 -> rnf a `seq` rnf c
        WApp  a w1 w2             -> rnf a `seq` rnf w1 `seq` rnf w2
        WJoin a w1 w2             -> rnf a `seq` rnf w1 `seq` rnf w2
        WType a tt                -> rnf a `seq` rnf tt