{- |
    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 (..), 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.

-- 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
  | TypeApply Type Type
  | TypeArrow Type Type
  | TypeForall [Int] Type
  deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Eq Type
Eq Type =>
(Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
$cp1Ord :: Eq Type
Ord, Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
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 :: Type -> [Type] -> Type
applyType (TypeConstructor tc :: QualIdent
tc) tys :: [Type]
tys
  | QualIdent
tc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qArrowId Bool -> Bool -> Bool
&& [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 2 = Type -> Type -> Type
TypeArrow ([Type]
tys [Type] -> Int -> Type
forall a. [a] -> Int -> a
!! 0) ([Type]
tys [Type] -> Int -> Type
forall a. [a] -> Int -> a
!! 1)
applyType (TypeApply (TypeConstructor tc :: QualIdent
tc) ty :: Type
ty) tys :: [Type]
tys
  | QualIdent
tc QualIdent -> QualIdent -> Bool
forall a. Eq a => a -> a -> Bool
== QualIdent
qArrowId Bool -> Bool -> Bool
&& [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 = Type -> Type -> Type
TypeArrow Type
ty ([Type] -> Type
forall a. [a] -> a
head [Type]
tys)
applyType ty :: Type
ty tys :: [Type]
tys = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
TypeApply Type
ty [Type]
tys

unapplyType :: Bool -> Type -> (Type, [Type])
unapplyType :: Bool -> Type -> (Type, [Type])
unapplyType dflt :: Bool
dflt ty :: Type
ty = Type -> [Type] -> (Type, [Type])
unapply Type
ty []
  where
    unapply :: Type -> [Type] -> (Type, [Type])
unapply (TypeConstructor     tc :: QualIdent
tc) tys :: [Type]
tys  = (QualIdent -> Type
TypeConstructor QualIdent
tc, [Type]
tys)
    unapply (TypeApply      ty1 :: Type
ty1 ty2 :: Type
ty2) tys :: [Type]
tys  = Type -> [Type] -> (Type, [Type])
unapply Type
ty1 (Type
ty2 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
tys)
    unapply (TypeVariable        tv :: Int
tv) tys :: [Type]
tys  = (Int -> Type
TypeVariable Int
tv, [Type]
tys)
    unapply (TypeArrow      ty1 :: Type
ty1 ty2 :: Type
ty2) tys :: [Type]
tys  =
      (QualIdent -> Type
TypeConstructor QualIdent
qArrowId, Type
ty1 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Type
ty2 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
tys)
    unapply (TypeConstrained tys :: [Type]
tys tv :: Int
tv) tys' :: [Type]
tys'
      | Bool
dflt      = Type -> [Type] -> (Type, [Type])
unapply ([Type] -> Type
forall a. [a] -> a
head [Type]
tys) [Type]
tys'
      | Bool
otherwise = ([Type] -> Int -> Type
TypeConstrained [Type]
tys Int
tv, [Type]
tys')
    unapply (TypeForall     tvs :: [Int]
tvs ty' :: Type
ty') tys :: [Type]
tys  = ([Int] -> Type -> Type
TypeForall [Int]
tvs Type
ty', [Type]
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 :: Type -> QualIdent
rootOfType ty :: Type
ty = case (Type, [Type]) -> Type
forall a b. (a, b) -> a
fst (Bool -> Type -> (Type, [Type])
unapplyType Bool
True Type
ty) of
  TypeConstructor tc :: QualIdent
tc -> QualIdent
tc
  _ -> String -> QualIdent
forall a. String -> a
internalError (String -> QualIdent) -> String -> QualIdent
forall a b. (a -> b) -> a -> b
$ "Base.Types.rootOfType: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
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 :: Type -> Bool
isArrowType (TypeArrow _ _) = Bool
True
isArrowType _               = Bool
False

arrowArity :: Type -> Int
arrowArity :: Type -> Int
arrowArity = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length([Type] -> Int) -> (Type -> [Type]) -> Type -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Type]
arrowArgs

arrowArgs :: Type -> [Type]
arrowArgs :: Type -> [Type]
arrowArgs = ([Type], Type) -> [Type]
forall a b. (a, b) -> a
fst (([Type], Type) -> [Type])
-> (Type -> ([Type], Type)) -> Type -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ([Type], Type)
arrowUnapply

arrowBase :: Type -> Type
arrowBase :: Type -> Type
arrowBase = ([Type], Type) -> Type
forall a b. (a, b) -> b
snd(([Type], Type) -> Type)
-> (Type -> ([Type], Type)) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> ([Type], Type)
arrowUnapply

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

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

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

-- The method 'typeVars' returns a list of all type variables occurring in a
-- type t. 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]

instance IsType Type where
  typeVars :: Type -> [Int]
typeVars = Type -> [Int]
typeVars'

typeVars' :: Type -> [Int]
typeVars' :: Type -> [Int]
typeVars' ty :: Type
ty = Type -> [Int] -> [Int]
vars Type
ty [] where
  vars :: Type -> [Int] -> [Int]
vars (TypeConstructor   _) tvs :: [Int]
tvs = [Int]
tvs
  vars (TypeApply   ty1 :: Type
ty1 ty2 :: Type
ty2) tvs :: [Int]
tvs = Type -> [Int] -> [Int]
vars Type
ty1 (Type -> [Int] -> [Int]
vars Type
ty2 [Int]
tvs)
  vars (TypeVariable     tv :: Int
tv) tvs :: [Int]
tvs = Int
tv Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
tvs
  vars (TypeConstrained _ _) tvs :: [Int]
tvs = [Int]
tvs
  vars (TypeArrow   ty1 :: Type
ty1 ty2 :: Type
ty2) tvs :: [Int]
tvs = Type -> [Int] -> [Int]
vars Type
ty1 (Type -> [Int] -> [Int]
vars Type
ty2 [Int]
tvs)
  vars (TypeForall tvs' :: [Int]
tvs' ty' :: Type
ty') tvs :: [Int]
tvs = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
tvs') (Type -> [Int]
typeVars' Type
ty') [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
tvs

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

qualifyType :: ModuleIdent -> Type -> Type
qualifyType :: ModuleIdent -> Type -> Type
qualifyType m :: ModuleIdent
m (TypeConstructor     tc :: QualIdent
tc) = QualIdent -> Type
TypeConstructor (ModuleIdent -> QualIdent -> QualIdent
qualifyTC ModuleIdent
m QualIdent
tc)
qualifyType m :: ModuleIdent
m (TypeApply      ty1 :: Type
ty1 ty2 :: Type
ty2) =
  Type -> Type -> Type
TypeApply (ModuleIdent -> Type -> Type
qualifyType ModuleIdent
m Type
ty1) (ModuleIdent -> Type -> Type
qualifyType ModuleIdent
m Type
ty2)
qualifyType _ tv :: Type
tv@(TypeVariable      _) = Type
tv
qualifyType m :: ModuleIdent
m (TypeConstrained tys :: [Type]
tys tv :: Int
tv) =
  [Type] -> Int -> Type
TypeConstrained ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleIdent -> Type -> Type
qualifyType ModuleIdent
m) [Type]
tys) Int
tv
qualifyType m :: ModuleIdent
m (TypeArrow      ty1 :: Type
ty1 ty2 :: Type
ty2) =
  Type -> Type -> Type
TypeArrow (ModuleIdent -> Type -> Type
qualifyType ModuleIdent
m Type
ty1) (ModuleIdent -> Type -> Type
qualifyType ModuleIdent
m Type
ty2)
qualifyType m :: ModuleIdent
m (TypeForall      tvs :: [Int]
tvs ty :: Type
ty) = [Int] -> Type -> Type
TypeForall [Int]
tvs (ModuleIdent -> Type -> Type
qualifyType ModuleIdent
m Type
ty)

unqualifyType :: ModuleIdent -> Type -> Type
unqualifyType :: ModuleIdent -> Type -> Type
unqualifyType m :: ModuleIdent
m (TypeConstructor     tc :: QualIdent
tc) = QualIdent -> Type
TypeConstructor (ModuleIdent -> QualIdent -> QualIdent
qualUnqualify ModuleIdent
m QualIdent
tc)
unqualifyType m :: ModuleIdent
m (TypeApply      ty1 :: Type
ty1 ty2 :: Type
ty2) =
  Type -> Type -> Type
TypeApply (ModuleIdent -> Type -> Type
unqualifyType ModuleIdent
m Type
ty1) (ModuleIdent -> Type -> Type
unqualifyType ModuleIdent
m Type
ty2)
unqualifyType _ tv :: Type
tv@(TypeVariable      _) = Type
tv
unqualifyType m :: ModuleIdent
m (TypeConstrained tys :: [Type]
tys tv :: Int
tv) =
  [Type] -> Int -> Type
TypeConstrained ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleIdent -> Type -> Type
unqualifyType ModuleIdent
m) [Type]
tys) Int
tv
unqualifyType m :: ModuleIdent
m (TypeArrow      ty1 :: Type
ty1 ty2 :: Type
ty2) =
  Type -> Type -> Type
TypeArrow (ModuleIdent -> Type -> Type
unqualifyType ModuleIdent
m Type
ty1) (ModuleIdent -> Type -> Type
unqualifyType ModuleIdent
m Type
ty2)
unqualifyType m :: ModuleIdent
m (TypeForall      tvs :: [Int]
tvs ty :: Type
ty) = [Int] -> Type -> Type
TypeForall [Int]
tvs (ModuleIdent -> Type -> Type
unqualifyType ModuleIdent
m Type
ty)

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

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

data Pred = Pred QualIdent Type
  deriving (Pred -> Pred -> Bool
(Pred -> Pred -> Bool) -> (Pred -> Pred -> Bool) -> Eq Pred
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pred -> Pred -> Bool
$c/= :: Pred -> Pred -> Bool
== :: Pred -> Pred -> Bool
$c== :: Pred -> Pred -> Bool
Eq, Int -> Pred -> ShowS
[Pred] -> ShowS
Pred -> String
(Int -> Pred -> ShowS)
-> (Pred -> String) -> ([Pred] -> ShowS) -> Show Pred
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Pred] -> ShowS
$cshowList :: [Pred] -> ShowS
show :: Pred -> String
$cshow :: Pred -> String
showsPrec :: Int -> Pred -> ShowS
$cshowsPrec :: Int -> Pred -> ShowS
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 :: QualIdent
qcls1 ty1 :: Type
ty1 compare :: Pred -> Pred -> Ordering
`compare` Pred qcls2 :: QualIdent
qcls2 ty2 :: Type
ty2 = case Type
ty1 Type -> Type -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Type
ty2 of
    LT -> Ordering
LT
    EQ -> QualIdent
qcls1 QualIdent -> QualIdent -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` QualIdent
qcls2
    GT -> Ordering
GT

instance IsType Pred where
  typeVars :: Pred -> [Int]
typeVars (Pred _ ty :: Type
ty) = Type -> [Int]
forall t. IsType t => t -> [Int]
typeVars Type
ty

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

unqualifyPred :: ModuleIdent -> Pred -> Pred
unqualifyPred :: ModuleIdent -> Pred -> Pred
unqualifyPred m :: ModuleIdent
m (Pred qcls :: QualIdent
qcls ty :: Type
ty) =
  QualIdent -> Type -> Pred
Pred (ModuleIdent -> QualIdent -> QualIdent
qualUnqualify ModuleIdent
m QualIdent
qcls) (ModuleIdent -> Type -> Type
unqualifyType ModuleIdent
m Type
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 :: Set a -> [Int]
typeVars = [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Int]] -> [Int]) -> (Set a -> [[Int]]) -> Set a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set [Int] -> [[Int]]
forall a. Set a -> [a]
Set.toList (Set [Int] -> [[Int]]) -> (Set a -> Set [Int]) -> Set a -> [[Int]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> [Int]) -> Set a -> Set [Int]
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map a -> [Int]
forall t. IsType t => t -> [Int]
typeVars

emptyPredSet :: PredSet
emptyPredSet :: PredSet
emptyPredSet = PredSet
forall a. Set a
Set.empty

partitionPredSet :: PredSet -> (PredSet, PredSet)
partitionPredSet :: PredSet -> (PredSet, PredSet)
partitionPredSet = (Pred -> Bool) -> PredSet -> (PredSet, PredSet)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition ((Pred -> Bool) -> PredSet -> (PredSet, PredSet))
-> (Pred -> Bool) -> PredSet -> (PredSet, PredSet)
forall a b. (a -> b) -> a -> b
$ \(Pred _ ty :: Type
ty) -> Type -> Bool
isTypeVariable Type
ty
  where
    isTypeVariable :: Type -> Bool
isTypeVariable (TypeVariable _) = Bool
True
    isTypeVariable (TypeApply ty :: Type
ty _) = Type -> Bool
isTypeVariable Type
ty
    isTypeVariable _                = Bool
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 :: ClassEnv -> PredSet -> PredSet
minPredSet clsEnv :: ClassEnv
clsEnv ps :: PredSet
ps =
  PredSet
ps PredSet -> PredSet -> PredSet
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` (Pred -> PredSet) -> PredSet -> PredSet
forall a b. (Ord a, Ord b) => (a -> Set b) -> Set a -> Set b
Set.concatMap Pred -> PredSet
implied PredSet
ps
  where implied :: Pred -> PredSet
implied (Pred cls :: QualIdent
cls ty :: Type
ty) = [Pred] -> PredSet
forall a. Ord a => [a] -> Set a
Set.fromList
          [QualIdent -> Type -> Pred
Pred QualIdent
cls' Type
ty | QualIdent
cls' <- [QualIdent] -> [QualIdent]
forall a. [a] -> [a]
tail (QualIdent -> ClassEnv -> [QualIdent]
allSuperClasses QualIdent
cls ClassEnv
clsEnv)]

maxPredSet :: ClassEnv -> PredSet -> PredSet
maxPredSet :: ClassEnv -> PredSet -> PredSet
maxPredSet clsEnv :: ClassEnv
clsEnv ps :: PredSet
ps = (Pred -> PredSet) -> PredSet -> PredSet
forall a b. (Ord a, Ord b) => (a -> Set b) -> Set a -> Set b
Set.concatMap Pred -> PredSet
implied PredSet
ps
  where implied :: Pred -> PredSet
implied (Pred cls :: QualIdent
cls ty :: Type
ty) = [Pred] -> PredSet
forall a. Ord a => [a] -> Set a
Set.fromList
          [QualIdent -> Type -> Pred
Pred QualIdent
cls' Type
ty | QualIdent
cls' <- QualIdent -> ClassEnv -> [QualIdent]
allSuperClasses QualIdent
cls ClassEnv
clsEnv]

qualifyPredSet :: ModuleIdent -> PredSet -> PredSet
qualifyPredSet :: ModuleIdent -> PredSet -> PredSet
qualifyPredSet m :: ModuleIdent
m = (Pred -> Pred) -> PredSet -> PredSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (ModuleIdent -> Pred -> Pred
qualifyPred ModuleIdent
m)

unqualifyPredSet :: ModuleIdent -> PredSet -> PredSet
unqualifyPredSet :: ModuleIdent -> PredSet -> PredSet
unqualifyPredSet m :: ModuleIdent
m = (Pred -> Pred) -> PredSet -> PredSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (ModuleIdent -> Pred -> Pred
unqualifyPred ModuleIdent
m)

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

data PredType = PredType PredSet Type
  deriving (PredType -> PredType -> Bool
(PredType -> PredType -> Bool)
-> (PredType -> PredType -> Bool) -> Eq PredType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PredType -> PredType -> Bool
$c/= :: PredType -> PredType -> Bool
== :: PredType -> PredType -> Bool
$c== :: PredType -> PredType -> Bool
Eq, Int -> PredType -> ShowS
[PredType] -> ShowS
PredType -> String
(Int -> PredType -> ShowS)
-> (PredType -> String) -> ([PredType] -> ShowS) -> Show PredType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PredType] -> ShowS
$cshowList :: [PredType] -> ShowS
show :: PredType -> String
$cshow :: PredType -> String
showsPrec :: Int -> PredType -> ShowS
$cshowsPrec :: Int -> PredType -> ShowS
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 -> [Int]
typeVars (PredType ps :: PredSet
ps ty :: Type
ty) = Type -> [Int]
forall t. IsType t => t -> [Int]
typeVars Type
ty [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ PredSet -> [Int]
forall t. IsType t => t -> [Int]
typeVars PredSet
ps

predType :: Type -> PredType
predType :: Type -> PredType
predType = PredSet -> Type -> PredType
PredType PredSet
emptyPredSet

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

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

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

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

-- The type 'DataConstr' is used to represent value or record constructors
-- introduced by data or newtype declarations.

data DataConstr = DataConstr   Ident [Type]
                | RecordConstr Ident [Ident] [Type]
  deriving (DataConstr -> DataConstr -> Bool
(DataConstr -> DataConstr -> Bool)
-> (DataConstr -> DataConstr -> Bool) -> Eq DataConstr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataConstr -> DataConstr -> Bool
$c/= :: DataConstr -> DataConstr -> Bool
== :: DataConstr -> DataConstr -> Bool
$c== :: DataConstr -> DataConstr -> Bool
Eq, Int -> DataConstr -> ShowS
[DataConstr] -> ShowS
DataConstr -> String
(Int -> DataConstr -> ShowS)
-> (DataConstr -> String)
-> ([DataConstr] -> ShowS)
-> Show DataConstr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataConstr] -> ShowS
$cshowList :: [DataConstr] -> ShowS
show :: DataConstr -> String
$cshow :: DataConstr -> String
showsPrec :: Int -> DataConstr -> ShowS
$cshowsPrec :: Int -> DataConstr -> ShowS
Show)

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

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

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

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

tupleData :: [DataConstr]
tupleData :: [DataConstr]
tupleData = [Ident -> [Type] -> DataConstr
DataConstr (Int -> Ident
tupleId Int
n) (Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
take Int
n [Type]
tvs) | Int
n <- [2 ..]]
  where tvs :: [Type]
tvs = (Int -> Type) -> [Int] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Type
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 (ClassMethod -> ClassMethod -> Bool
(ClassMethod -> ClassMethod -> Bool)
-> (ClassMethod -> ClassMethod -> Bool) -> Eq ClassMethod
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ClassMethod -> ClassMethod -> Bool
$c/= :: ClassMethod -> ClassMethod -> Bool
== :: ClassMethod -> ClassMethod -> Bool
$c== :: ClassMethod -> ClassMethod -> Bool
Eq, Int -> ClassMethod -> ShowS
[ClassMethod] -> ShowS
ClassMethod -> String
(Int -> ClassMethod -> ShowS)
-> (ClassMethod -> String)
-> ([ClassMethod] -> ShowS)
-> Show ClassMethod
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ClassMethod] -> ShowS
$cshowList :: [ClassMethod] -> ShowS
show :: ClassMethod -> String
$cshow :: ClassMethod -> String
showsPrec :: Int -> ClassMethod -> ShowS
$cshowsPrec :: Int -> ClassMethod -> ShowS
Show)

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

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

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

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

-- We support only universally quantified type schemes
-- (forall alpha . tau(alpha)). 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' constructor.

data TypeScheme = ForAll Int PredType deriving (TypeScheme -> TypeScheme -> Bool
(TypeScheme -> TypeScheme -> Bool)
-> (TypeScheme -> TypeScheme -> Bool) -> Eq TypeScheme
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypeScheme -> TypeScheme -> Bool
$c/= :: TypeScheme -> TypeScheme -> Bool
== :: TypeScheme -> TypeScheme -> Bool
$c== :: TypeScheme -> TypeScheme -> Bool
Eq, Int -> TypeScheme -> ShowS
[TypeScheme] -> ShowS
TypeScheme -> String
(Int -> TypeScheme -> ShowS)
-> (TypeScheme -> String)
-> ([TypeScheme] -> ShowS)
-> Show TypeScheme
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypeScheme] -> ShowS
$cshowList :: [TypeScheme] -> ShowS
show :: TypeScheme -> String
$cshow :: TypeScheme -> String
showsPrec :: Int -> TypeScheme -> ShowS
$cshowsPrec :: Int -> TypeScheme -> ShowS
Show)

instance IsType TypeScheme where
  typeVars :: TypeScheme -> [Int]
typeVars (ForAll _ pty :: PredType
pty) = [Int
tv | Int
tv <- PredType -> [Int]
forall t. IsType t => t -> [Int]
typeVars PredType
pty, Int
tv Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0]

-- 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 :: Type -> TypeScheme
monoType = Int -> PredType -> TypeScheme
ForAll 0 (PredType -> TypeScheme)
-> (Type -> PredType) -> Type -> TypeScheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> PredType
predType

polyType :: Type -> TypeScheme
polyType :: Type -> TypeScheme
polyType = PredType -> TypeScheme
typeScheme (PredType -> TypeScheme)
-> (Type -> PredType) -> Type -> TypeScheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> PredType
predType

typeScheme :: PredType -> TypeScheme
typeScheme :: PredType -> TypeScheme
typeScheme pty :: PredType
pty = Int -> PredType -> TypeScheme
ForAll ([Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (-1 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: PredType -> [Int]
forall t. IsType t => t -> [Int]
typeVars PredType
pty) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) PredType
pty

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

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

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

primType :: QualIdent -> [Type] -> Type
primType :: QualIdent -> [Type] -> Type
primType = Type -> [Type] -> Type
applyType (Type -> [Type] -> Type)
-> (QualIdent -> Type) -> QualIdent -> [Type] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualIdent -> Type
TypeConstructor

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

unitType :: Type
unitType :: Type
unitType = QualIdent -> [Type] -> Type
primType QualIdent
qUnitId []

predUnitType :: PredType
predUnitType :: PredType
predUnitType = Type -> PredType
predType Type
unitType

boolType :: Type
boolType :: Type
boolType = QualIdent -> [Type] -> Type
primType QualIdent
qBoolId []

predBoolType :: PredType
predBoolType :: PredType
predBoolType = Type -> PredType
predType Type
boolType

charType :: Type
charType :: Type
charType = QualIdent -> [Type] -> Type
primType QualIdent
qCharId []

intType :: Type
intType :: Type
intType = QualIdent -> [Type] -> Type
primType QualIdent
qIntId []

predIntType :: PredType
predIntType :: PredType
predIntType = Type -> PredType
predType Type
intType

floatType :: Type
floatType :: Type
floatType = QualIdent -> [Type] -> Type
primType QualIdent
qFloatId []

predFloatType :: PredType
predFloatType :: PredType
predFloatType = Type -> PredType
predType Type
floatType

stringType :: Type
stringType :: Type
stringType = Type -> Type
listType Type
charType

predStringType :: PredType
predStringType :: PredType
predStringType = Type -> PredType
predType Type
stringType

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

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

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

tupleType :: [Type] -> Type
tupleType :: [Type] -> Type
tupleType tys :: [Type]
tys = QualIdent -> [Type] -> Type
primType (Int -> QualIdent
qTupleId ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys)) [Type]
tys

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

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

fractionalTypes :: [Type]
fractionalTypes :: [Type]
fractionalTypes = Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
drop 1 [Type]
numTypes

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