module Base.Types
(
Type (..), isArrowType, arrowArity, arrowArgs, arrowBase, arrowUnapply
, typeVars, typeConstrs, typeSkolems, equTypes, qualifyType, unqualifyType
, DataConstr (..), constrIdent, constrTypes, recLabels, recLabelTypes
, tupleData
, TypeScheme (..), ExistTypeScheme (..), monoType, polyType
, unitType, boolType, charType, intType, floatType, stringType
, listType, ioType, tupleType, typeVar, predefTypes
) where
import Curry.Base.Ident
data Type
= TypeVariable Int
| TypeConstructor QualIdent [Type]
| TypeArrow Type Type
| TypeConstrained [Type] Int
| TypeSkolem Int
deriving (Eq, Show)
isArrowType :: Type -> Bool
isArrowType (TypeArrow _ _) = True
isArrowType _ = False
arrowArity :: Type -> Int
arrowArity (TypeArrow _ ty) = 1 + arrowArity ty
arrowArity _ = 0
arrowArgs :: Type -> [Type]
arrowArgs (TypeArrow ty1 ty2) = ty1 : arrowArgs ty2
arrowArgs _ = []
arrowBase :: Type -> Type
arrowBase (TypeArrow _ ty) = arrowBase ty
arrowBase ty = ty
arrowUnapply :: Type -> ([Type], Type)
arrowUnapply (TypeArrow ty1 ty2) = (ty1 : tys, ty)
where (tys, ty) = arrowUnapply ty2
arrowUnapply ty = ([], ty)
typeVars :: Type -> [Int]
typeVars ty = vars ty [] where
vars (TypeConstructor _ tys) tvs = foldr vars tvs tys
vars (TypeVariable tv) tvs = tv : tvs
vars (TypeConstrained _ _) tvs = tvs
vars (TypeArrow ty1 ty2) tvs = vars ty1 (vars ty2 tvs)
vars (TypeSkolem _) tvs = tvs
typeConstrs :: Type -> [QualIdent]
typeConstrs ty = constrs ty [] where
constrs (TypeConstructor tc tys) tcs = tc : foldr constrs tcs tys
constrs (TypeVariable _) tcs = tcs
constrs (TypeConstrained _ _) tcs = tcs
constrs (TypeArrow ty1 ty2) tcs = constrs ty1 (constrs ty2 tcs)
constrs (TypeSkolem _) tcs = tcs
typeSkolems :: Type -> [Int]
typeSkolems ty = skolems ty [] where
skolems (TypeConstructor _ tys) sks = foldr skolems sks tys
skolems (TypeVariable _) sks = sks
skolems (TypeConstrained _ _) sks = sks
skolems (TypeArrow ty1 ty2) sks = skolems ty1 (skolems ty2 sks)
skolems (TypeSkolem k) sks = k : sks
equTypes :: Type -> Type -> Bool
equTypes t1 t2 = fst (equ [] t1 t2)
where
equ is (TypeConstructor qid1 ts1) (TypeConstructor qid2 ts2)
| qid1 == qid2 = equs is ts1 ts2
| otherwise = (False, is)
equ is (TypeVariable i1) (TypeVariable i2)
= equVar is i1 i2
equ is (TypeConstrained ts1 i1) (TypeConstrained ts2 i2)
= let (res , is1) = equs is ts1 ts2
(res2, is2) = equVar is1 i1 i2
in (res && res2, is2)
equ is (TypeArrow tf1 tt1) (TypeArrow tf2 tt2)
= let (res1, is1) = equ is tf1 tf2
(res2, is2) = equ is1 tt1 tt2
in (res1 && res2, is2)
equ is (TypeSkolem i1) (TypeSkolem i2)
= equVar is i1 i2
equ is _ _
= (False, is)
equVar is i1 i2 = case lookup i1 is of
Nothing -> (True, (i1, i2) : is)
Just i2' -> (i2 == i2', is)
equs is [] [] = (True , is)
equs is (t1':ts1) (t2':ts2)
= let (res1, is1) = equ is t1' t2'
(res2, is2) = equs is1 ts1 ts2
in (res1 && res2, is2)
equs is _ _ = (False, is)
qualifyType :: ModuleIdent -> Type -> Type
qualifyType m (TypeConstructor tc tys)
| isTupleId tc' = tupleType tys'
| tc' == unitId && n == 0 = unitType
| tc' == listId && n == 1 = listType (head tys')
| otherwise = TypeConstructor (qualQualify m tc) tys'
where n = length tys'
tc' = unqualify tc
tys' = map (qualifyType m) tys
qualifyType _ var@(TypeVariable _) = var
qualifyType m (TypeConstrained tys tv) =
TypeConstrained (map (qualifyType m) tys) tv
qualifyType m (TypeArrow ty1 ty2) =
TypeArrow (qualifyType m ty1) (qualifyType m ty2)
qualifyType _ skol@(TypeSkolem _) = skol
unqualifyType :: ModuleIdent -> Type -> Type
unqualifyType m (TypeConstructor tc tys) =
TypeConstructor (qualUnqualify m tc) (map (unqualifyType m) tys)
unqualifyType _ var@(TypeVariable _) = var
unqualifyType m (TypeConstrained tys tv) =
TypeConstrained (map (unqualifyType m) tys) tv
unqualifyType m (TypeArrow ty1 ty2) =
TypeArrow (unqualifyType m ty1) (unqualifyType m ty2)
unqualifyType _ skol@(TypeSkolem _) = skol
data DataConstr = DataConstr Ident Int [Type]
| RecordConstr Ident Int [Ident] [Type]
deriving (Eq, Show)
constrIdent :: DataConstr -> Ident
constrIdent (DataConstr c _ _) = c
constrIdent (RecordConstr c _ _ _) = c
constrTypes :: DataConstr -> [Type]
constrTypes (DataConstr _ _ ty) = ty
constrTypes (RecordConstr _ _ _ ty) = ty
recLabels :: DataConstr -> [Ident]
recLabels (DataConstr _ _ _) = []
recLabels (RecordConstr _ _ ls _) = ls
recLabelTypes :: DataConstr -> [Type]
recLabelTypes (DataConstr _ _ _) = []
recLabelTypes (RecordConstr _ _ _ tys) = tys
data TypeScheme = ForAll Int Type deriving (Eq, Show)
data ExistTypeScheme = ForAllExist Int Int Type deriving (Eq, Show)
monoType :: Type -> TypeScheme
monoType ty = ForAll 0 ty
polyType :: Type -> TypeScheme
polyType ty = ForAll (maximum (1 : typeVars ty) + 1) ty
unitType :: Type
unitType = primType qUnitId []
boolType :: Type
boolType = primType qBoolId []
charType :: Type
charType = primType qCharId []
intType :: Type
intType = primType qIntId []
floatType :: Type
floatType = primType qFloatId []
stringType :: Type
stringType = listType charType
listType :: Type -> Type
listType ty = primType qListId [ty]
ioType :: Type -> Type
ioType ty = primType qIOId [ty]
tupleType :: [Type] -> Type
tupleType tys = primType (qTupleId (length tys)) tys
typeVar :: Int -> Type
typeVar = TypeVariable
primType :: QualIdent -> [Type] -> Type
primType = TypeConstructor
predefTypes :: [(Type, [DataConstr])]
predefTypes = let a = typeVar 0 in
[ (unitType , [ DataConstr unitId 0 [] ])
, (listType a, [ DataConstr nilId 0 []
, DataConstr consId 0 [a, listType a]
])
]
tupleData :: [DataConstr]
tupleData = [DataConstr (tupleId n) n (take n tvs) | n <- [2 ..]]
where tvs = map typeVar [0 ..]