{- |
    Module      :  $Header$
    Description :  Internal representation of types
    Copyright   :  (c) 2002 - 2004 Wolfgang Lux
                                   Martin Engelke
                       2015        Jan Tikovsky
                       2016        Finn Teegen
    License     :  BSD-3-clause

    Maintainer  :  bjp@informatik.uni-kiel.de
    Stability   :  experimental
    Portability :  portable

   This module modules provides the definitions for the internal
   representation of types in the compiler along with some helper functions.
-}

-- TODO: Use MultiParamTypeClasses ?

module Base.Types
  ( -- * Representation of types
    Type (..), applyType, unapplyType, rootOfType
  , isArrowType, arrowArity, arrowArgs, arrowBase, arrowUnapply
  , IsType (..), typeConstrs
  , qualifyType, unqualifyType, qualifyTC
    -- * Representation of predicate, predicate sets and predicated types
  , Pred (..), qualifyPred, unqualifyPred
  , PredSet, emptyPredSet, partitionPredSet, minPredSet, maxPredSet
  , qualifyPredSet, unqualifyPredSet
  , PredType (..), predType, unpredType, qualifyPredType, unqualifyPredType
    -- * Representation of data constructors
  , DataConstr (..), constrIdent, constrTypes, recLabels, recLabelTypes
  , tupleData
    -- * Representation of class methods
  , ClassMethod (..), methodName, methodArity, methodType
    -- * Representation of quantification
  , TypeScheme (..), ExistTypeScheme (..), monoType, polyType, typeScheme
  , rawType
    -- * Predefined types
  , arrowType, unitType, predUnitType, boolType, predBoolType, charType
  , intType, predIntType, floatType, predFloatType, stringType, predStringType
  , listType, consType, ioType, tupleType
  , numTypes, fractionalTypes
  , predefTypes
  ) where

import qualified Data.Set.Extra as Set

import Curry.Base.Ident

import Base.Messages (internalError)

import Env.Class (ClassEnv, allSuperClasses)

-- ---------------------------------------------------------------------------
-- Types
-- ---------------------------------------------------------------------------

-- A type is either a type constructor, a type variable, an application
-- of a type to another type, or an arrow type. Although the latter could
-- be expressed by using 'TypeApply' with the function type constructor,
-- we currently use 'TypeArrow' because arrow types are used so frequently.

-- The 'TypeConstrained' case is used for representing type variables that
-- are restricted to a particular set of types. At present, this is used
-- for typing integer literals, which are restricted to types 'Int' and
-- 'Float'. If the type is not restricted, it defaults to the first type
-- from the constraint list.

-- The case 'TypeSkolem' is used for handling skolem types, which
-- result from the use of existentially quantified data constructors.

-- Type variables are represented with deBruijn style indices. Universally
-- quantified type variables are assigned indices in the order of their
-- occurrence in the type from left to right. This leads to a canonical
-- representation of types where alpha-equivalence of two types
-- coincides with equality of the representation.

-- Note that even though 'TypeConstrained' variables use indices
-- as well, these variables must never be quantified.

-- Note further that the order of constructors is important for the derived
-- 'Ord' instance. In particular, it is essential that the type variable
-- is considered less than the type application (see predicates and predicate
-- sets below for more information).

data Type
  = TypeConstructor QualIdent
  | TypeVariable Int
  | TypeConstrained [Type] Int
  | TypeSkolem Int
  | TypeApply Type Type
  | TypeArrow Type Type
  | TypeForall [Int] Type
  deriving (Eq, Ord, Show)

-- The function 'applyType' applies a type to a list of argument types,
-- whereas applications of the function type constructor to two arguments
-- are converted into an arrow type. The function 'unapplyType' decomposes
-- a type into a root type and a list of argument types.

applyType :: Type -> [Type] -> Type
applyType (TypeConstructor tc) tys
  | tc == qArrowId && length tys == 2 = TypeArrow (tys !! 0) (tys !! 1)
applyType (TypeApply (TypeConstructor tc) ty) tys
  | tc == qArrowId && length tys == 1 = TypeArrow ty (head tys)
applyType ty tys = foldl TypeApply ty tys

unapplyType :: Bool -> Type -> (Type, [Type])
unapplyType dflt ty = unapply ty []
  where
    unapply (TypeConstructor     tc) tys  = (TypeConstructor tc, tys)
    unapply (TypeApply      ty1 ty2) tys  = unapply ty1 (ty2 : tys)
    unapply (TypeVariable        tv) tys  = (TypeVariable tv, tys)
    unapply (TypeArrow      ty1 ty2) tys  =
      (TypeConstructor qArrowId, ty1 : ty2 : tys)
    unapply (TypeConstrained tys tv) tys'
      | dflt      = unapply (head tys) tys'
      | otherwise = (TypeConstrained tys tv, tys')
    unapply (TypeSkolem           k) tys  = (TypeSkolem k, tys)
    unapply (TypeForall     tvs ty') tys  = (TypeForall tvs ty', tys)

-- The function 'rootOfType' returns the name of the type constructor at the
-- root of a type. This function must not be applied to a type whose root is
-- a type variable or a skolem type.

rootOfType :: Type -> QualIdent
rootOfType ty = case fst (unapplyType True ty) of
  TypeConstructor tc -> tc
  _ -> internalError $ "Base.Types.rootOfType: " ++ show ty

-- The function 'isArrowType' checks whether a type is a function
-- type t_1 -> t_2 -> ... -> t_n. The function 'arrowArity' computes
-- the arity n of a function type, 'arrowArgs' computes the types
-- t_1 ... t_n-1 and 'arrowBase' returns the type t_n. 'arrowUnapply'
-- combines 'arrowArgs' and 'arrowBase' in one call.

isArrowType :: Type -> Bool
isArrowType (TypeArrow _ _) = True
isArrowType _               = False

arrowArity :: Type -> Int
arrowArity = length. arrowArgs

arrowArgs :: Type -> [Type]
arrowArgs = fst . arrowUnapply

arrowBase :: Type -> Type
arrowBase = snd. arrowUnapply

arrowUnapply :: Type -> ([Type], Type)
arrowUnapply (TypeArrow ty1 ty2) = (ty1 : tys, ty)
  where (tys, ty) = arrowUnapply ty2
arrowUnapply ty                  = ([], ty)

-- The function 'typeConstrs' returns a list of all type constructors
-- occuring in a type t.

typeConstrs :: Type -> [QualIdent]
typeConstrs ty = constrs ty [] where
  constrs (TypeConstructor  tc) tcs = tc : tcs
  constrs (TypeApply   ty1 ty2) tcs = constrs ty1 (constrs ty2 tcs)
  constrs (TypeVariable      _) tcs = tcs
  constrs (TypeConstrained _ _) tcs = tcs
  constrs (TypeArrow   ty1 ty2) tcs = constrs ty1 (constrs ty2 tcs)
  constrs (TypeSkolem        _) tcs = tcs
  constrs (TypeForall    _ ty') tcs = constrs ty' tcs

-- The methods 'typeVars' and 'typeSkolems' return a list of all type
-- variables and skolems occurring in a type t, respectively. Note that
-- 'TypeConstrained' variables are not included in the set of type
-- variables because they cannot be generalized.

class IsType t where
  typeVars :: t -> [Int]
  typeSkolems :: t -> [Int]

instance IsType Type where
  typeVars = typeVars'
  typeSkolems = typeSkolems'

typeVars' :: Type -> [Int]
typeVars' ty = vars ty [] where
  vars (TypeConstructor   _) tvs = tvs
  vars (TypeApply   ty1 ty2) tvs = vars ty1 (vars ty2 tvs)
  vars (TypeVariable     tv) tvs = tv : tvs
  vars (TypeConstrained _ _) tvs = tvs
  vars (TypeArrow   ty1 ty2) tvs = vars ty1 (vars ty2 tvs)
  vars (TypeSkolem        _) tvs = tvs
  vars (TypeForall tvs' ty') tvs = filter (`notElem` tvs') (typeVars' ty') ++ tvs

typeSkolems' :: Type -> [Int]
typeSkolems' ty = skolems ty [] where
  skolems (TypeConstructor   _) sks = sks
  skolems (TypeApply   ty1 ty2) sks = skolems ty1 (skolems ty2 sks)
  skolems (TypeVariable      _) sks = sks
  skolems (TypeConstrained _ _) sks = sks
  skolems (TypeArrow   ty1 ty2) sks = skolems ty1 (skolems ty2 sks)
  skolems (TypeSkolem        k) sks = k : sks
  skolems (TypeForall    _ ty') sks = skolems ty' sks

-- The functions 'qualifyType' and 'unqualifyType' add/remove the
-- qualification with a module identifier for type constructors.

qualifyType :: ModuleIdent -> Type -> Type
qualifyType m (TypeConstructor     tc) = TypeConstructor (qualifyTC m tc)
qualifyType m (TypeApply      ty1 ty2) =
  TypeApply (qualifyType m ty1) (qualifyType m ty2)
qualifyType _ tv@(TypeVariable      _) = tv
qualifyType m (TypeConstrained tys tv) =
  TypeConstrained (map (qualifyType m) tys) tv
qualifyType m (TypeArrow      ty1 ty2) =
  TypeArrow (qualifyType m ty1) (qualifyType m ty2)
qualifyType _ ts@(TypeSkolem        _) = ts
qualifyType m (TypeForall      tvs ty) = TypeForall tvs (qualifyType m ty)

unqualifyType :: ModuleIdent -> Type -> Type
unqualifyType m (TypeConstructor     tc) = TypeConstructor (qualUnqualify m tc)
unqualifyType m (TypeApply      ty1 ty2) =
  TypeApply (unqualifyType m ty1) (unqualifyType m ty2)
unqualifyType _ tv@(TypeVariable      _) = tv
unqualifyType m (TypeConstrained tys tv) =
  TypeConstrained (map (unqualifyType m) tys) tv
unqualifyType m (TypeArrow      ty1 ty2) =
  TypeArrow (unqualifyType m ty1) (unqualifyType m ty2)
unqualifyType _ ts@(TypeSkolem        _) = ts
unqualifyType m (TypeForall      tvs ty) = TypeForall tvs (unqualifyType m ty)

qualifyTC :: ModuleIdent -> QualIdent -> QualIdent
qualifyTC m tc | isPrimTypeId tc = tc
               | otherwise       = qualQualify m tc

-- ---------------------------------------------------------------------------
-- Predicates
-- ---------------------------------------------------------------------------

data Pred = Pred QualIdent Type
  deriving (Eq, Show)

-- We provide a custom 'Ord' instance for predicates here where we consider
-- the type component of the predicate before the class component (see predicate
-- sets below for more information).

instance Ord Pred where
  Pred qcls1 ty1 `compare` Pred qcls2 ty2 = case ty1 `compare` ty2 of
    LT -> LT
    EQ -> qcls1 `compare` qcls2
    GT -> GT

instance IsType Pred where
  typeVars (Pred _ ty) = typeVars ty
  typeSkolems (Pred _ ty) = typeSkolems ty

qualifyPred :: ModuleIdent -> Pred -> Pred
qualifyPred m (Pred qcls ty) = Pred (qualQualify m qcls) (qualifyType m ty)

unqualifyPred :: ModuleIdent -> Pred -> Pred
unqualifyPred m (Pred qcls ty) =
  Pred (qualUnqualify m qcls) (unqualifyType m ty)

-- ---------------------------------------------------------------------------
-- Predicate sets
-- ---------------------------------------------------------------------------

-- A predicate set is an ordered set of predicates. This way, we do not
-- have to manually take care of duplicate predicates and have automatically
-- achieved a canonical representation (as only original names for type classes
-- are used). Having the order on types and predicates in mind, we have also
-- ensured that a class method's implicit class constraint is always the minimum
-- element of a method's predicate set, thus making it very easy to remove it.

type PredSet = Set.Set Pred

instance (IsType a, Ord a) => IsType (Set.Set a) where
  typeVars = concat . Set.toList . Set.map typeVars
  typeSkolems = concat . Set.toList . Set.map typeSkolems

emptyPredSet :: PredSet
emptyPredSet = Set.empty

partitionPredSet :: PredSet -> (PredSet, PredSet)
partitionPredSet = Set.partition $ \(Pred _ ty) -> isTypeVariable ty
  where
    isTypeVariable (TypeVariable _) = True
    isTypeVariable (TypeApply ty _) = isTypeVariable ty
    isTypeVariable _                = False

-- The function 'minPredSet' transforms a predicate set by removing all
-- predicates from the predicate set which are implied by other predicates
-- according to the super class hierarchy. Inversely, the function 'maxPredSet'
-- adds all predicates to a predicate set which are implied by the predicates
-- in the given predicate set.

minPredSet :: ClassEnv -> PredSet -> PredSet
minPredSet clsEnv ps =
  ps `Set.difference` Set.concatMap implied ps
  where implied (Pred cls ty) = Set.fromList
          [Pred cls' ty | cls' <- tail (allSuperClasses cls clsEnv)]

maxPredSet :: ClassEnv -> PredSet -> PredSet
maxPredSet clsEnv ps = Set.concatMap implied ps
  where implied (Pred cls ty) = Set.fromList
          [Pred cls' ty | cls' <- allSuperClasses cls clsEnv]

qualifyPredSet :: ModuleIdent -> PredSet -> PredSet
qualifyPredSet m = Set.map (qualifyPred m)

unqualifyPredSet :: ModuleIdent -> PredSet -> PredSet
unqualifyPredSet m = Set.map (unqualifyPred m)

-- ---------------------------------------------------------------------------
-- Predicated types
-- ---------------------------------------------------------------------------

data PredType = PredType PredSet Type
  deriving (Eq, Show)

-- When enumarating the type variables and skolems of a predicated type, we
-- consider the type variables occuring in the predicate set after the ones
-- occuring in the type itself.

instance IsType PredType where
  typeVars (PredType ps ty) = typeVars ty ++ typeVars ps
  typeSkolems (PredType ps ty) = typeSkolems ty ++ typeSkolems ps

predType :: Type -> PredType
predType = PredType emptyPredSet

unpredType :: PredType -> Type
unpredType (PredType _ ty) = ty

qualifyPredType :: ModuleIdent -> PredType -> PredType
qualifyPredType m (PredType ps ty) =
  PredType (qualifyPredSet m ps) (qualifyType m ty)

unqualifyPredType :: ModuleIdent -> PredType -> PredType
unqualifyPredType m (PredType ps ty) =
  PredType (unqualifyPredSet m ps) (unqualifyType m ty)

-- ---------------------------------------------------------------------------
-- Data constructors
-- ---------------------------------------------------------------------------

-- The type 'DataConstr' is used to represent value or record constructors
-- introduced by data or newtype declarations. The 'Int' denotes the number
-- of existentially quantified type variables in the types.

data DataConstr = DataConstr   Ident Int PredSet [Type]
                | RecordConstr Ident Int PredSet [Ident] [Type]
  deriving (Eq, Show)

constrIdent :: DataConstr -> Ident
constrIdent (DataConstr     c _ _ _) = c
constrIdent (RecordConstr c _ _ _ _) = c

constrTypes :: DataConstr -> [Type]
constrTypes (DataConstr     _ _ _ tys) = tys
constrTypes (RecordConstr _ _ _ _ tys) = tys

recLabels :: DataConstr -> [Ident]
recLabels (DataConstr      _ _ _ _) = []
recLabels (RecordConstr _ _ _ ls _) = ls

recLabelTypes :: DataConstr -> [Type]
recLabelTypes (DataConstr       _ _ _ _) = []
recLabelTypes (RecordConstr _ _ _ _ tys) = tys

tupleData :: [DataConstr]
tupleData = [DataConstr (tupleId n) 0 emptyPredSet (take n tvs) | n <- [2 ..]]
  where tvs = map TypeVariable [0 ..]

-- ---------------------------------------------------------------------------
-- Class methods
-- ---------------------------------------------------------------------------

-- The type 'ClassMethod' is used to represent class methods introduced
-- by class declarations. The 'Maybe Int' denotes the arity of the provided
-- default implementation.

data ClassMethod = ClassMethod Ident (Maybe Int) PredType
  deriving (Eq, Show)

methodName :: ClassMethod -> Ident
methodName (ClassMethod f _ _) = f

methodArity :: ClassMethod -> Maybe Int
methodArity (ClassMethod _ a _) = a

methodType :: ClassMethod -> PredType
methodType (ClassMethod _ _ pty) = pty

-- ---------------------------------------------------------------------------
-- Quantification
-- ---------------------------------------------------------------------------

-- We support two kinds of quantifications of types here, universally
-- quantified type schemes (forall alpha . tau(alpha)) and universally
-- and existentially quantified type schemes
-- (forall alpha exists eta . tau(alpha,eta)). In both, quantified type
-- variables are assigned ascending indices starting from 0. Therefore it
-- is sufficient to record the numbers of quantified type variables in
-- the 'ForAll' and 'ForAllExist' constructors. In case of
-- the latter, the first of the two numbers is the number of universally
-- quantified variables and the second the number of existentially
-- quantified variables.

data TypeScheme = ForAll Int PredType deriving (Eq, Show)
data ExistTypeScheme = ForAllExist Int Int PredType deriving (Eq, Show)

instance IsType TypeScheme where
  typeVars (ForAll _ pty) = [tv | tv <- typeVars pty, tv < 0]
  typeSkolems (ForAll _ pty) = typeSkolems pty

instance IsType ExistTypeScheme where
  typeVars (ForAllExist _ _ pty) = [tv | tv <- typeVars pty, tv < 0]
  typeSkolems (ForAllExist _ _ pty) = typeSkolems pty

-- The functions 'monoType' and 'polyType' translate a type tau into a
-- monomorphic type scheme and a polymorphic type scheme, respectively.
-- 'polyType' assumes that all universally quantified variables in the type are
-- assigned indices starting with 0 and does not renumber the variables.

monoType :: Type -> TypeScheme
monoType = ForAll 0 . predType

polyType :: Type -> TypeScheme
polyType = typeScheme . predType

typeScheme :: PredType -> TypeScheme
typeScheme pty = ForAll (maximum (-1 : typeVars pty) + 1) pty

-- The function 'rawType' strips the quantifier and predicate set from a
-- type scheme.

rawType :: TypeScheme -> Type
rawType (ForAll _ (PredType _ ty)) = ty

-- ---------------------------------------------------------------------------
-- Predefined types
-- ---------------------------------------------------------------------------

primType :: QualIdent -> [Type] -> Type
primType = applyType . TypeConstructor

arrowType :: Type -> Type -> Type
arrowType ty1 ty2 = primType qArrowId [ty1, ty2]

unitType :: Type
unitType = primType qUnitId []

predUnitType :: PredType
predUnitType = predType unitType

boolType :: Type
boolType = primType qBoolId []

predBoolType :: PredType
predBoolType = predType boolType

charType :: Type
charType = primType qCharId []

intType :: Type
intType = primType qIntId []

predIntType :: PredType
predIntType = predType intType

floatType :: Type
floatType = primType qFloatId []

predFloatType :: PredType
predFloatType = predType floatType

stringType :: Type
stringType = listType charType

predStringType :: PredType
predStringType = predType stringType

listType :: Type -> Type
listType ty = primType qListId [ty]

consType :: Type -> Type
consType ty = TypeArrow ty (TypeArrow (listType ty) (listType ty))

ioType :: Type -> Type
ioType ty = primType qIOId [ty]

tupleType :: [Type] -> Type
tupleType tys = primType (qTupleId (length tys)) tys

-- 'numTypes' and 'fractionalTypes' define the eligible types for
-- numeric literals in patterns.

numTypes :: [Type]
numTypes = [intType, floatType]

fractionalTypes :: [Type]
fractionalTypes = drop 1 numTypes

predefTypes :: [(Type, [DataConstr])]
predefTypes =
  [ (arrowType a b, [])
  , (unitType     , [ DataConstr unitId 0 emptyPredSet [] ])
  , (listType a   , [ DataConstr nilId  0 emptyPredSet []
                    , DataConstr consId 0 emptyPredSet [a, listType a]
                    ])
  ]
  where a = TypeVariable 0
        b = TypeVariable 1