-- | This module contains the definition of type expressions of our
--   lifted intermediate language.
module FreeC.LiftedIR.Syntax.Type where

import           FreeC.IR.SrcSpan           ( SrcSpan )
import           FreeC.LiftedIR.Syntax.Name

-- | A type expression.
--
--   Types are represented as fully applied type constructors or type variables
--   of kind @*@. In contrast to the 'FreeC.IR.Type' from the intermediate
--   representation, @Free@ is modelled explicitly.
data Type
  = -- | A type variable.
    TypeVar { typeSrcSpan :: SrcSpan, typeVarIdent :: TypeVarIdent }
    -- | A fully applied n-ary type constructor application.
  | TypeCon
      { typeSrcSpan :: SrcSpan
      , typeConName :: TypeConName
      , typeConArgs :: [Type]
      , typeIsDec   :: Bool
        -- ^ Marks this type as a decreasing element of a type signature.
        --
        --   E.g., recursive constructor arguments or decreasing function
        --   argument. This field is used by the Agda back end to place sized
        --   type annotations.
      }
    -- | A function type.
  | FuncType { typeSrcSpan :: SrcSpan
             , funcTypeArg :: Type
             , funcTypeRes :: Type
             }
    -- | A type constructor for the free monad.
  | FreeTypeCon { typeSrcSpan :: SrcSpan, typeFreeArg :: Type }
 deriving ( Eq, Show )

-------------------------------------------------------------------------------
-- Utility                                                                   --
-------------------------------------------------------------------------------
-- | Creates a function type with the given argument and return types.
funcType :: SrcSpan -> [Type] -> Type -> Type
funcType srcSpan = flip (foldr (FuncType srcSpan))

-- | Decides whether a type contains a decreasing argument.
decreasing :: Type -> Bool
decreasing (TypeCon _ _ _ dec) = dec
decreasing (FuncType _ l r)    = decreasing l || decreasing r
decreasing (FreeTypeCon _ t)   = decreasing t
decreasing (TypeVar _ _)       = False