-- | Call patterns.
--
--   A call pattern describes the sequence of objects that are eliminated
--   by some object when we apply it, and before it starts constructing
--   new values. 
--
-- @
-- Constructor (+ve)             Eliminator (-ve)
--  /\x.  (type   abstraction)    \@'    (type   application)
--   \x.  (object abstraction)    \@     (object application) 
--  box   (suspend evaluation)   run   (commence evaluation)
-- @
--   
module DDC.Core.Call 
        ( -- * Call constructors
          Cons (..)
        , isConsType
        , isConsValue
        , isConsBox
        , takeCallConsFromExp
        , takeCallConsFromType
        , splitStdCallCons
        , takeStdCallConsFromTypeArity

          -- * Call eliminators
        , Elim (..)
        , isElimType
        , isElimValue
        , isElimRun
        , takeCallElim
        , applyElim
        , splitStdCallElims

          -- * Matching
        , elimForCons
        , dischargeConsWithElims
        , dischargeTypeWithElims)
where
import DDC.Core.Exp.Annot
import DDC.Type.Transform.SubstituteT


-----------------------------------------------------------------------------
-- | One component of the call pattern of a super.
--   This is the "outer wrapper" of the computation,
-- 
--   With @/\(a : k). \(x : t). box (x + 1)@ the call pattern consists of
--   the two lambdas and the box. These three things need to be eliminated
--   before we can construct any new values.
--
data Cons n
        = -- | A type  lambda that needs a type of this kind.
          ConsType    (Bind n)

          -- | A value lambda that needs a value of this type.
        | ConsValue   (Type n)

          -- | A suspended expression that needs to be run.
        | ConsBox
        deriving (Show)


-- | Check if this is an `ConsType`.
isConsType :: Cons n -> Bool
isConsType cc
 = case cc of
        ConsType{}      -> True
        _               -> False


-- | Check if this is an `ElimType`.
isConsValue :: Cons n -> Bool
isConsValue cc
 = case cc of
        ConsValue{}     -> True
        _               -> False


-- | Check if this is an `ElimType`.
isConsBox :: Cons n -> Bool
isConsBox cc
 = case cc of
        ConsBox{}       -> True
        _               -> False


-- | Get the call pattern of an expression.
takeCallConsFromExp :: Exp a n -> [Cons n]
takeCallConsFromExp xx
 = case xx of
        XLAM _ b x         
         ->     ConsType  b : takeCallConsFromExp x

        XLam _ b x         
         -> let t       = typeOfBind b
            in  ConsValue t : takeCallConsFromExp x

        XCast _ CastBox x
         ->     ConsBox     : takeCallConsFromExp x

        _ -> []


-- | Infer the call pattern of an expression from its type.
--   If the type has a function constructor then we assume there
--   is a corresponding lambda abstraction in the expression, and so on.
takeCallConsFromType :: Type n -> [Cons n]
takeCallConsFromType tt
        | TForall bParam tBody   <- tt
        = ConsType  bParam : takeCallConsFromType tBody

        | Just (tParam, tResult) <- takeTFun tt
        = ConsValue tParam : takeCallConsFromType tResult

        | Just (_, tResult)      <- takeTSusp tt
        = ConsBox          : takeCallConsFromType tResult

        | otherwise
        = []


-- | Like `splitStdCallElim`, but for the constructor side.
--
splitStdCallCons
        :: [Cons n]
        -> Maybe ([Cons n], [Cons n], [Cons n])

splitStdCallCons cs
 = eatTypes [] cs
 where
        eatTypes  accTs (e@ConsType{} : es)
         = eatTypes (e : accTs) es

        eatTypes  accTs es
         = eatValues (reverse accTs) [] es

        eatValues accTs accVs (e@ConsValue{} : es)
         = eatValues accTs (e : accVs) es

        eatValues accTs accVs es
         = eatRuns   accTs (reverse accVs) [] es

        eatRuns  accTs accVs accRs (e@ConsBox{} : es)
         = eatRuns   accTs accVs (e : accRs) es

        eatRuns  accTs accVs accRs []
         = Just (accTs, accVs, reverse accRs)

        eatRuns  _accTs _accVs _accRs _
         = Nothing


-- | Given the type of a super, and the number of type parameters,
--   value parameters and boxings, produce the corresponding list
--   of call constructors.
--
--   Example:
--
-- @
--    takeStdCallConsFromType 
--       [| forall (a : k1) (b : k2). a -> b -> S e b |] 
--       2 2 1
--    => [ ConsType  [|k1|], ConsType  [|k2|]
--       , ConsValue [|a\],  ConsValue [|b|]
--       , ConsBox ]
-- @
--
--   When we're considering the parts of the type, if the given arity
--   does not match what is in the type then `Nothing`.
--
takeStdCallConsFromTypeArity
        :: Type n       -- ^ Type of super
        -> Int          -- ^ Number of type parameters.
        -> Int          -- ^ Number of value parameters.
        -> Int          -- ^ Number of boxings.
        -> Maybe [Cons n]

takeStdCallConsFromTypeArity tt0 nTypes0 nValues0 nBoxes0
 = eatTypes [] tt0 nTypes0
 where
        -- Consider type parameters.
        eatTypes !accTs !tt !nTypes

         -- The arity information tells us to expect a type parameter.
         | nTypes  > 0
         = case tt of
            -- The super type matches.
            TForall b tBody
             -> eatTypes (ConsType b : accTs) tBody (nTypes - 1)

            -- The super type does not match the arity information.
            _ -> Nothing

         -- No more type parameters expected, so consider the value parameters.
         | otherwise
         = eatValues (reverse accTs) [] tt nValues0


        -- Consider value parameters.
        eatValues !accTs !accVs !tt !nValues

         -- The arity information tells us to expect a value parameter.
         | nValues > 0
         = case takeTFun tt of
            -- The super type matches.
            Just (t1, t2) 
              -> eatValues accTs (ConsValue t1 : accVs) t2 (nValues - 1)

            -- The super type does not match the arity information.
            _ -> Nothing

         -- No more value parameters expect, so consider the boxes.
         | otherwise
         = eatBoxes accTs (reverse accVs) [] tt nBoxes0


        -- Consider boxes.
        eatBoxes !accTs !accVs !accBs tt nBoxes

         -- The arity information tells us to expect a boxing.
         | nBoxes > 0
         = case takeTSusp tt of
            -- The super type matches.
            Just (_eff, tBody)
              -> eatBoxes accTs accVs (ConsBox : accBs) tBody (nBoxes - 1)

            -- The super type does not match the arity information.
            _ -> Nothing

         -- No more boxings to expect, so we're done.
         | otherwise
         = return (accTs ++ accVs ++ reverse accBs)


-------------------------------------------------------------------------------
-- | One component of a super call.
data Elim a n
        = -- | Give a type to a type lambda.
          ElimType    a a (Type n)

          -- | Give a value to a value lambda.
        | ElimValue   a (Exp a n)

          -- | Run a suspended computation.
        | ElimRun     a
        deriving (Show)


-- | Check if this is an `ElimType`.
isElimType :: Elim a n -> Bool
isElimType ee
 = case ee of
        ElimType{}      -> True
        _               -> False


-- | Check if this is an `ElimType`.
isElimValue :: Elim a n -> Bool
isElimValue ee
 = case ee of
        ElimValue{}     -> True
        _               -> False


-- | Check if this is an `ElimType`.
isElimRun :: Elim a n -> Bool
isElimRun ee
 = case ee of
        ElimRun{}       -> True
        _               -> False


-- | Apply an eliminator to an expression.
applyElim :: Exp a n -> Elim a n -> Exp a n
applyElim xx e
 = case e of
        ElimType  a at t -> XApp a xx (XType at t)
        ElimValue a x    -> XApp a xx x
        ElimRun   a      -> XCast a CastRun xx


-- | Split the application of some object into the object being
--   applied and its eliminators.
takeCallElim :: Exp a n -> (Exp a n, [Elim a n])
takeCallElim xx
 = case xx of
        XApp a x1 (XType at t2)
         -> let (xF, xArgs)     = takeCallElim x1
            in  (xF, xArgs ++ [ElimType a at t2])

        XApp a x1 x2            
         -> let (xF, xArgs)     = takeCallElim x1
            in  (xF, xArgs ++ [ElimValue a x2])

        XCast a CastRun x1
         -> let (xF, xArgs)     = takeCallElim x1
            in  (xF, xArgs ++ [ElimRun a])

        _ -> (xx, [])


-- | Group eliminators into sets for a standard call.
--
--   The standard call sequence is a list of type arguments, followed
--   by some objects, and optionally running the result suspension.
--
--   @run f [T1] [T2] x1 x2@
--
--   If 'f' is a super, and this is a saturating call then the super header
--   will look like the following:
--
--   @f = (/\t1. /\t2. \v1. \v2. box. body)@

--   If the eliminators are not in the standard call sequence then `Nothing`.
--
splitStdCallElims 
        :: [Elim a n] 
        -> Maybe ([Elim a n], [Elim a n], [Elim a n])

splitStdCallElims ee
 = eatTypes [] ee
 where
        eatTypes  accTs (e@ElimType{} : es)
         = eatTypes (e : accTs) es

        eatTypes  accTs es
         = eatValues (reverse accTs) [] es

        eatValues accTs accVs (e@ElimValue{} : es)
         = eatValues accTs (e : accVs) es

        eatValues accTs accVs es
         = eatRuns   accTs (reverse accVs) [] es

        eatRuns  accTs accVs accRs (e@ElimRun{} : es)
         = eatRuns   accTs accVs (e : accRs) es

        eatRuns  accTs accVs accRs []
         = Just (accTs, accVs, reverse accRs)

        eatRuns  _accTs _accVs _accRs _
         = Nothing


-------------------------------------------------------------------------------
-- | Check if this an eliminator for the given constructor.
--   This only checks the general form of the eliminator 
--   and constructor, not the exact types or kinds.
elimForCons :: Elim a n -> Cons n -> Bool
elimForCons e c
 = case (e, c) of
        (ElimType{},  ConsType{})       -> True
        (ElimValue{}, ConsValue{})      -> True
        (ElimRun{},   ConsBox{})        -> True
        _                               -> False


-- | Given lists of constructors and eliminators, check if the
--   eliminators satisfy the constructors, and return any remaining
--   unmatching constructors and eliminators.
--
--   We assume that the application is well typed and that applying
--   the given eliminators will not cause variable capture.
---
--   ISSUE #347: Avoid name capture in dischargeConsWithElims
--   This process doesn't avoid name capture by ConsTypes earlier
--   in the list, but it's only called from the Curry transform
--   where there shouldn't be any shadowed type binders.
--
dischargeConsWithElims
        :: Ord n
        => [Cons n] 
        -> [Elim a n] 
        -> ([Cons n], [Elim a n])

dischargeConsWithElims (c : cs) (e : es)
 = case (c, e) of
        (ConsType  b1, ElimType  _ _ t2)
          -> dischargeConsWithElims 
                (map (instantiateConsT b1 t2) cs) 
                es

        (ConsValue _t1, ElimValue _ _x2)
          -> dischargeConsWithElims cs es

        (ConsBox,       ElimRun _)
          -> dischargeConsWithElims cs es

        _ -> (c : cs, e : es)

dischargeConsWithElims cs es
 = (cs, es)


instantiateConsT :: Ord n => Bind n -> Type n -> Cons n -> Cons n
instantiateConsT b t cc
 = case cc of
        ConsType{}      -> cc
        ConsValue t'    -> ConsValue (substituteT b t t')
        ConsBox{}       -> cc


-- | Given a type of a function and eliminators, discharge
--   foralls, abstractions and boxes to get the result type
--   of performing the application.
-- 
--   We assume that the application is well typed.
--
dischargeTypeWithElims
        :: Ord n
        => Type n
        -> [Elim a n]
        -> Maybe (Type n)

dischargeTypeWithElims tt (ElimType  _ _ tArg : es)
        | TForall b tBody         <- tt
        = dischargeTypeWithElims 
                (substituteT b tArg tBody) 
                es

dischargeTypeWithElims tt (ElimValue _ _xArg  : es)
        | Just (_tParam, tResult) <- takeTFun tt
        = dischargeTypeWithElims tResult es

dischargeTypeWithElims tt (ElimRun _ : es)
        | Just (_, tBody)         <- takeTSusp tt
        = dischargeTypeWithElims tBody es
 
dischargeTypeWithElims tt []
        = Just tt

dischargeTypeWithElims _tt _es
        = Nothing