content: {-# OPTIONS_HADDOCK hide #-}
  
  module DDC.Core.Codec.Text.Parser.Param
          ( ParamSpec     (..)
          , funTypeOfParams
          , expOfParams
          , pBindParamSpecAnnot
          , pBindParamSpec )
  where
  import DDC.Core.Codec.Text.Parser.Type
  import DDC.Core.Codec.Text.Parser.Context
  import DDC.Core.Codec.Text.Parser.Base
  import DDC.Core.Codec.Text.Lexer.Tokens
  import DDC.Core.Exp
  import DDC.Data.Pretty
  import qualified DDC.Type.Exp.Simple    as T
  import qualified DDC.Control.Parser     as P
  
  
  -- | Specification of a function parameter.
  --   We can determine the contribution to the type of the function,
  --   as well as its expression based on the parameter.
  data ParamSpec n
          = ParamType    (Bind n)
          | ParamWitness (Bind n)
          | ParamValue   (Bind n) (Type n) (Type n)
  
  
  -- | Build the expression of a function from specifications of its parameters,
  --   and the expression for the body.
  expOfParams
          :: a
          -> [ParamSpec n]        -- ^ Spec of parameters.
          -> Exp a n              -- ^ Body of function.
          -> Exp a n              -- ^ Expression of whole function.
  
  expOfParams _ [] xBody            = xBody
  expOfParams a (p:ps) xBody
   = case p of
          ParamType b
           -> XLAM a b $ expOfParams a ps xBody
  
          ParamWitness b
           -> XLam a b $ expOfParams a ps xBody
  
          ParamValue b _ _
           -> XLam a b $ expOfParams a ps xBody
  
  
  -- | Build the type of a function from specifications of its parameters,
  --   and the type of the body.
  funTypeOfParams
          :: Context n
          -> [ParamSpec n]        -- ^ Spec of parameters.
          -> Type n               -- ^ Type of body.
          -> Type n               -- ^ Type of whole function.
  
  funTypeOfParams _ [] tBody
   = tBody
  
  funTypeOfParams c (p:ps) tBody
   = case p of
          ParamType  b
           -> TForall b
                  $ funTypeOfParams c ps tBody
  
          ParamWitness b
           -> T.tImpl (T.typeOfBind b)
                  $ funTypeOfParams c ps tBody
  
          ParamValue b _eff _clo
           -> T.tFun (T.typeOfBind b)
                  $ funTypeOfParams c ps tBody
  
  
  -- | Parse a function parameter specification,
  --   with an optional type (or kind) annotation.
  pBindParamSpec
          :: (Ord n, Pretty n)
          => Context n -> Parser n [ParamSpec n]
  
  pBindParamSpec c
   = P.choice
   [      -- Value (or type) binder with a type (or kind) annotation.
          pBindParamSpecAnnot c
  
          -- Value binder without type annotations.
    , do  b       <- pBinder
          return  $  [ ParamValue (T.makeBindFromBinder b (T.tBot T.kData))
                                  (T.tBot T.kEffect) (T.tBot T.kClosure) ]
   ]
  
  
  -- | Parse a function parameter specification,
  --   requiring a full type (or kind) annotation.
  ---
  --       [BIND1 BIND2 .. BINDN : TYPE]
  --   or  (BIND : TYPE)
  --   or  (BIND : TYPE) { EFFECT | CLOSURE }
  --
  pBindParamSpecAnnot
          :: (Ord n, Pretty n)
          => Context n -> Parser n [ParamSpec n]
  
  pBindParamSpecAnnot c
   = P.choice
          -- Type parameter
          -- [BIND1 BIND2 .. BINDN : TYPE]
   [ do   pSym SSquareBra
          bs      <- P.many1 pBinder
          pTok (KOp ":")
          t       <- pType c
          pSym SSquareKet
          return  [ ParamType b
                  | b <- zipWith T.makeBindFromBinder bs (repeat t)]
  
          -- Witness parameter
          -- {BIND : TYPE}
   , do   pSym SBraceBra
          b       <- pBinder
          pTok (KOp ":")
          t       <- pType c
          pSym SBraceKet
          return  [ ParamWitness $ T.makeBindFromBinder b t]
  
          -- Value parameter with type annotations.
          -- (BIND1 BIND2 .. BINDN : TYPE)
          -- (BIND1 BIND2 .. BINDN : TYPE) { TYPE | TYPE }
   , do   pSym SRoundBra
          bs      <- P.many1 pBinder
          pTok (KOp ":")
          t       <- pType c
          pSym SRoundKet
  
          (eff, clo)
           <- P.choice
                  [ do    pSym SBraceBra
                          eff'    <- pType c
                          pSym SBar
                          clo'    <- pType c
                          pSym SBraceKet
                          return  (eff', clo')
  
                  , do    return  (T.tBot T.kEffect, T.tBot T.kClosure) ]
  
          let bLast : bsInit
                  = reverse bs
  
          return  $  [ ParamValue (T.makeBindFromBinder b     t)
                                  (T.tBot T.kEffect) (T.tBot T.kClosure)
                          | b <- reverse bsInit]
                  ++ [ ParamValue (T.makeBindFromBinder bLast t) eff clo]
   ]
  
  