-- | Abstract syntax for the Disciple core language.
module DDC.Core.Exp 
        ( module DDC.Type.Exp

          -- * Computation expressions
        , Exp     (..)
        , Cast    (..)
        , Lets    (..)
        , LetMode (..)
        , Alt     (..)
        , Pat     (..)
                        
          -- * Witnesses expressions
        , Witness (..)
        , WiCon   (..)
        , WbCon   (..))
where
import DDC.Type.Exp
import DDC.Type.Sum             ()


-- Values ---------------------------------------------------------------------
-- | Well-typed expressions live in the Data universe, and their types always
--   have kind '*'. 
-- 
--   Expressions do something useful at runtime, and might diverge or cause
--   side effects.
data Exp a n
        -- | Value variable   or primitive operation.
        = XVar  a  (Bound n)

        -- | Data constructor or literal.
        | XCon  a  (Bound 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 n)   (Exp a n)

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

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


-- | Type casts.
data Cast n
        -- | Weaken the effect of an expression.
        = CastWeakenEffect  (Effect n)
        
        -- | Weaken the closure of an expression.
        | CastWeakenClosure (Closure n)

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

        -- | Hide sharing of the closure of an expression.
        | CastForget (Witness n)
        deriving (Eq, Show)


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

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

        -- | Bind a local region variable,
        --   and witnesses to its properties.
        | LLetRegion  (Bind n) [Bind n]
        
        -- | Holds a region handle during evaluation.
        | LWithRegion (Bound n)
        deriving (Eq, Show)


-- | Describes how a let binding should be evaluated.
data LetMode n
        -- | Evaluate binding before substituting the result.
        = LetStrict

        -- | Use lazy evaluation. 
        --   The witness shows that the head region of the bound expression
        --   can contain thunks (is lazy), or Nothing if there is no head region.
        | LetLazy (Maybe (Witness n))
        deriving (Eq, Show)


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


-- | Pattern matching.
data Pat n
        -- | The default pattern always succeeds.
        = PDefault
        
        -- | Match a data constructor and bind its arguments.
        | PData (Bound n) [Bind n]
        deriving (Eq, Show)
        

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

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

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


-- | Witness constructors.
data WiCon n
        -- | Witness constructors baked into the language.
        = WiConBuiltin WbCon

        -- | Witness constructors defined in the environment.
        --   In the interpreter we use this to hold runtime capabilities.
        | WiConBound (Bound n)
        deriving (Eq, Show)


-- | Built-in witness constructors.
--
--   These are used to convert a runtime capability into a witness that
--   the corresponding property is true.
data WbCon
        -- | (axiom) The pure effect is pure.
        -- 
        --   @pure     :: Pure !0@
        = WbConPure 

        -- | (axiom) The empty closure is empty.
        --
        --   @empty    :: Empty $0@
        | WbConEmpty

        -- | Convert a capability guaranteeing that a region is in the global
        --   heap into a witness that a closure using this region is empty.
        --   This lets us rely on the garbage collector to reclaim objects
        --   in the region. It is needed when we suspend the evaluation of 
        --   expressions that have a region in their closure, because the
        --   type of the returned thunk may not reveal that it references
        --   objects in that region.
        -- 
        --  @use      :: [r: %]. Global r => Empty (Use r)@
        | WbConUse      

        -- | Convert a capability guaranteeing the constancy of a region into
        --   a witness that a read from that region is pure.
        --   This lets us suspend applications that read constant objects,
        --   because it doesn't matter if the read is delayed, we'll always
        --   get the same result.
        --
        --   @read     :: [r: %]. Const r  => Pure (Read r)@
        | WbConRead     

        -- | Convert a capability guaranteeing the constancy of a region into
        --   a witness that allocation into that region is pure.
        --   This lets us increase the sharing of constant objects,
        --   because we can't tell constant objects of the same value apart.
        -- 
        --  @alloc    :: [r: %]. Const r  => Pure (Alloc r)@
        | WbConAlloc
        deriving (Eq, Show)