Commit 34fddcdd authored by Björn Peemöller 's avatar Björn Peemöller
Browse files

A bunch of things!

parent ba21a418
......@@ -39,54 +39,60 @@ Executable cymake
, mtl, old-time, containers, pretty
ghc-options: -Wall
Other-Modules:
Base.Arity
, Base.Eval
Checks
, CompilerEnv
, CompilerOpts
, CurryBuilder
, CurryDeps
, Exports
, Frontend
, Generators
, IL
, Imports
, Interfaces
, Modules
, ModuleSummary
, Records
, Transformations
, Base.CurryTypes
, Base.Expr
, Base.Import
, Base.Module
, Base.OpPrec
, Base.TypeConstructors
, Base.Messages
, Base.SCC
, Base.Subst
, Base.Types
, Base.Value
, Check.InterfaceCheck
, Base.TypeSubst
, Base.Typing
, Base.Utils
, Check.KindCheck
, Check.PrecCheck
, Check.SyntaxCheck
, Check.TypeCheck
, Check.WarnCheck
, Env.CurryEnv
, Env.Arity
, Env.Eval
, Env.Import
, Env.Label
, Env.Module
, Env.NestEnv
, Env.OldScopeEnv
, Env.OpPrec
, Env.ScopeEnv
, Env.TopEnv
, Env.TypeConstructors
, Env.Value
, Gen.GenAbstractCurry
, Gen.GenFlatCurry
, Html.CurryHtml
, Html.SyntaxColoring
, IL
, IL.Pretty
, IL.Type
, IL.XML
, CurryBuilder
, CompilerOpts
, CurryDeps
, CurryToIL
, Exports
, Frontend
, Imports
, Messages
, Modules
, SCC
, Subst
, Transform.CaseCompletion
, Transform.CurryToIL
, Transform.Desugar
, Transform.Lift
, Transform.Qual
, Transform.Simplify
, Types
, TypeSubst
, Typing
, Utils
Library
hs-source-dirs: src
Build-Depends: filepath
......
\paragraph{Types}
The functions \texttt{toType}, \texttt{toTypes}, and \texttt{fromType}
convert Curry type expressions into types and vice versa. The
functions \texttt{qualifyType} and \texttt{unqualifyType} add and
remove module qualifiers in a type, respectively.
When Curry type expression are converted with \texttt{toType} or
\texttt{toTypes}, type variables are assigned ascending indices in the
order of their occurrence. It is possible to pass a list of additional
type variables to both functions which are assigned indices before
those variables occurring in the type. This allows preserving the
order of type variables in the left hand side of a type declaration.
\begin{verbatim}
> module Base.CurryTypes
> ( toQualType, toQualTypes, toType, toTypes, toType', fromQualType, fromType
> ) where
> import Data.List (nub)
> import qualified Data.Map as Map (Map, fromList, lookup)
> import Curry.Base.Ident
> import qualified Curry.Syntax as CS
> import Base.Expr
> import Base.Messages (internalError)
> import Base.Types
> toQualType :: ModuleIdent -> [Ident] -> CS.TypeExpr -> Type
> toQualType m tvs = qualifyType m . toType tvs
> toQualTypes :: ModuleIdent -> [Ident] -> [CS.TypeExpr] -> [Type]
> toQualTypes m tvs = map (qualifyType m) . toTypes tvs
> toType :: [Ident] -> CS.TypeExpr -> Type
> toType tvs ty = toType' (Map.fromList (zip (tvs ++ tvs') [0 ..])) ty
> where tvs' = [tv | tv <- nub (fv ty), tv `notElem` tvs]
> toTypes :: [Ident] -> [CS.TypeExpr] -> [Type]
> toTypes tvs tys = map (toType' (Map.fromList (zip (tvs ++ tvs') [0 ..]))) tys
> where tvs' = [tv | tv <- nub (concatMap fv tys), tv `notElem` tvs]
> toType' :: Map.Map Ident Int -> CS.TypeExpr -> Type
> toType' tvs (CS.ConstructorType tc tys) =
> TypeConstructor tc (map (toType' tvs) tys)
> toType' tvs (CS.VariableType tv) =
> maybe (internalError ("toType " ++ show tv)) TypeVariable (Map.lookup tv tvs)
> toType' tvs (CS.TupleType tys)
> | null tys = TypeConstructor (qualify unitId) []
> | otherwise = TypeConstructor (qualify (tupleId (length tys'))) tys'
> where tys' = map (toType' tvs) tys
> toType' tvs (CS.ListType ty) = TypeConstructor (qualify listId) [toType' tvs ty]
> toType' tvs (CS.ArrowType ty1 ty2) =
> TypeArrow (toType' tvs ty1) (toType' tvs ty2)
> toType' tvs (CS.RecordType fs rty) =
> TypeRecord (concatMap (\ (ls, ty) -> map (\ l -> (l, toType' tvs ty)) ls) fs)
> (maybe Nothing
> (\ ty -> case toType' tvs ty of
> TypeVariable tv -> Just tv
> _ -> internalError ("toType " ++ show ty))
> rty)
> fromQualType :: ModuleIdent -> Type -> CS.TypeExpr
> fromQualType m = fromType . unqualifyType m
> fromType :: Type -> CS.TypeExpr
> fromType (TypeConstructor tc tys)
> | isTupleId c = CS.TupleType tys'
> | c == listId && length tys == 1 = CS.ListType (head tys')
> | c == unitId && null tys = CS.TupleType []
> | otherwise = CS.ConstructorType tc tys'
> where c = unqualify tc
> tys' = map fromType tys
> fromType (TypeVariable tv) = CS.VariableType
> (if tv >= 0 then identSupply !! tv else mkIdent ('_' : show (-tv)))
> fromType (TypeConstrained tys _) = fromType (head tys)
> fromType (TypeArrow ty1 ty2) = CS.ArrowType (fromType ty1) (fromType ty2)
> fromType (TypeSkolem k) = CS.VariableType (mkIdent ("_?" ++ show k))
> fromType (TypeRecord fs rty) = CS.RecordType
> (map (\ (l, ty) -> ([l], fromType ty)) fs)
> (maybe Nothing (Just . fromType . TypeVariable) rty)
module Messages
module Base.Messages
( info, status
, putErrLn, putErrsLn, abortWith
, internalError, errorAt, errorAt'
......
\paragraph{Interfaces}
The compiler maintains a global environment holding all (directly or
indirectly) imported interfaces.
The function \texttt{bindFlatInterface} transforms FlatInterface
information (type \texttt{FlatCurry.Prog} to MCC interface declarations
(type \texttt{CurrySyntax.IDecl}. This is necessary to process
FlatInterfaces instead of ".icurry" files when using MCC as frontend
for PAKCS.
\begin{verbatim}
> module Base.Module (ModuleEnv, lookupModule) where
> import qualified Data.Map as Map
> import Curry.Base.Ident (ModuleIdent)
> import qualified Curry.Syntax as CS (IDecl)
> type ModuleEnv = Map.Map ModuleIdent [CS.IDecl]
> lookupModule :: ModuleIdent -> ModuleEnv -> Maybe [CS.IDecl]
> lookupModule = Map.lookup
\end{verbatim}
......@@ -20,7 +20,7 @@ unique number. The latter is only used to provide a trivial ordering
so that the declarations can be used as set elements.
\begin{verbatim}
> module SCC (scc) where
> module Base.SCC (scc) where
> import qualified Data.Set as Set (empty, member, insert)
......
......@@ -12,7 +12,7 @@ In order to implement substitutions efficiently, composed substitutions are
marked with a boolean flag (see below).
\begin{verbatim}
> module Subst
> module Base.Subst
> ( Subst (..), IntSubst (..), idSubst, substToList, bindSubst, unbindSubst
> , compose, substVar', isubstVar, restrictSubstTo
> )where
......
......@@ -9,15 +9,17 @@
This module implements substitutions on types.
\begin{verbatim}
> module TypeSubst (module TypeSubst, idSubst, bindSubst, compose) where
> module Base.TypeSubst (module Base.TypeSubst, idSubst, bindSubst, compose) where
> import Data.Maybe
> import Data.List
> import Data.List (nub)
> import Data.Maybe (fromJust, isJust)
> import Base.Value (ValueInfo (..))
> import Subst
> import Types
> import Env.TopEnv
> import Env.Value (ValueInfo (..))
> import Base.Subst
> import Base.Types
> type TypeSubst = Subst Int Type
......
\paragraph{Types}
The functions \texttt{toType}, \texttt{toTypes}, and \texttt{fromType}
convert Curry type expressions into types and vice versa. The
functions \texttt{qualifyType} and \texttt{unqualifyType} add and
remove module qualifiers in a type, respectively.
When Curry type expression are converted with \texttt{toType} or
\texttt{toTypes}, type variables are assigned ascending indices in the
order of their occurrence. It is possible to pass a list of additional
type variables to both functions which are assigned indices before
those variables occurring in the type. This allows preserving the
order of type variables in the left hand side of a type declaration.
% $Id: Types.lhs,v 1.11 2004/02/08 22:14:02 wlux Exp $
%
% Copyright (c) 2002, Wolfgang Lux
% See LICENSE for the full license.
%
% Modified by Martin Engelke (men@informatik.uni-kiel.de)
%
\nwfilename{Types.lhs}
\section{Types}
This module modules provides the definitions for the internal
representation of types in the compiler.
\begin{verbatim}
> module Base.Types
> ( toQualType, toQualTypes, toType, toTypes, toType', fromQualType, fromType
> ) where
> ( Type (..), DataConstr (..), isArrowType, arrowArity, arrowArgs, arrowBase
> , typeVars, typeConstrs, typeSkolems, equTypes, TypeScheme (..)
> , ExistTypeScheme (..), monoType, polyType
> , unitType, boolType, charType, intType, floatType, stringType
> , successType, listType, ioType, tupleType, primType
> , typeVar, predefTypes, qualifyType, unqualifyType
> ) where
> import Data.List (nub)
> import qualified Data.Map as Map (Map, fromList, lookup)
> import Data.Maybe (fromJust, isJust, isNothing)
> import Curry.Base.Ident
> import qualified Curry.Syntax as CS
> import Base.Expr
> import Messages (internalError)
> import Types
> toQualType :: ModuleIdent -> [Ident] -> CS.TypeExpr -> Type
> toQualType m tvs = qualifyType m . toType tvs
> toQualTypes :: ModuleIdent -> [Ident] -> [CS.TypeExpr] -> [Type]
> toQualTypes m tvs = map (qualifyType m) . toTypes tvs
> toType :: [Ident] -> CS.TypeExpr -> Type
> toType tvs ty = toType' (Map.fromList (zip (tvs ++ tvs') [0 ..])) ty
> where tvs' = [tv | tv <- nub (fv ty), tv `notElem` tvs]
> toTypes :: [Ident] -> [CS.TypeExpr] -> [Type]
> toTypes tvs tys = map (toType' (Map.fromList (zip (tvs ++ tvs') [0 ..]))) tys
> where tvs' = [tv | tv <- nub (concatMap fv tys), tv `notElem` tvs]
> toType' :: Map.Map Ident Int -> CS.TypeExpr -> Type
> toType' tvs (CS.ConstructorType tc tys) =
> TypeConstructor tc (map (toType' tvs) tys)
> toType' tvs (CS.VariableType tv) =
> maybe (internalError ("toType " ++ show tv)) TypeVariable (Map.lookup tv tvs)
> toType' tvs (CS.TupleType tys)
> | null tys = TypeConstructor (qualify unitId) []
> | otherwise = TypeConstructor (qualify (tupleId (length tys'))) tys'
> where tys' = map (toType' tvs) tys
> toType' tvs (CS.ListType ty) = TypeConstructor (qualify listId) [toType' tvs ty]
> toType' tvs (CS.ArrowType ty1 ty2) =
> TypeArrow (toType' tvs ty1) (toType' tvs ty2)
> toType' tvs (CS.RecordType fs rty) =
> TypeRecord (concatMap (\ (ls, ty) -> map (\ l -> (l, toType' tvs ty)) ls) fs)
> (maybe Nothing
> (\ ty -> case toType' tvs ty of
> TypeVariable tv -> Just tv
> _ -> internalError ("toType " ++ show ty))
> rty)
> fromQualType :: ModuleIdent -> Type -> CS.TypeExpr
> fromQualType m = fromType . unqualifyType m
> fromType :: Type -> CS.TypeExpr
> fromType (TypeConstructor tc tys)
> | isTupleId c = CS.TupleType tys'
> | c == listId && length tys == 1 = CS.ListType (head tys')
> | c == unitId && null tys = CS.TupleType []
> | otherwise = CS.ConstructorType tc tys'
> where c = unqualify tc
> tys' = map fromType tys
> fromType (TypeVariable tv) =
> CS.VariableType (if tv >= 0 then identSupply !! tv
> else mkIdent ('_' : show (-tv)))
> fromType (TypeConstrained tys _) = fromType (head tys)
> fromType (TypeArrow ty1 ty2) = CS.ArrowType (fromType ty1) (fromType ty2)
> fromType (TypeSkolem k) = CS.VariableType (mkIdent ("_?" ++ show k))
> fromType (TypeRecord fs rty) =
> CS.RecordType (map (\ (l, ty) -> ([l], fromType ty)) fs)
> (maybe Nothing (Just . fromType . TypeVariable) rty)
\end{verbatim}
A type is either a type variable, an application of a type constructor
to a list of arguments, or an arrow type. The \texttt{TypeConstrained}
case is used for representing type variables that are restricted to a
particular set of types. At present, this is used for typing guard
expressions, which are restricted to be either of type \texttt{Bool}
or of type \texttt{Success}, and integer literals, which are
restricted to types \texttt{Int} and \texttt{Float}. If the type is
not restricted, it defaults to the first type from the constraint list.
The case \texttt{TypeSkolem} is used for handling skolem types, which
result from the use of existentially quantified data constructors.
Finally, \texttt{TypeRecord} is used for records.
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 \texttt{TypeConstrained} variables use indices
as well, these variables must never be quantified.
\begin{verbatim}
> data Type
> = TypeVariable Int
> | TypeConstructor QualIdent [Type]
> | TypeArrow Type Type
> | TypeConstrained [Type] Int
> | TypeSkolem Int
> | TypeRecord [(Ident,Type)] (Maybe Int)
> deriving (Eq, Show)
\end{verbatim}
The type \texttt{Data} is used to represent value constructors introduced
by data or newtype declarations.
\begin{verbatim}
> data DataConstr = DataConstr Ident Int [Type]
> deriving (Eq, Show)
\end{verbatim}
The function \texttt{isArrowType} checks whether a type is a function
type $t_1 \rightarrow t_2 \rightarrow \dots \rightarrow t_n$ . The
function \texttt{arrowArity} computes the arity $n$ of a function type,
\texttt{arrowArgs} computes the types $t_1 \dots t_{n-1}$
and \texttt{arrowBase} returns the type $t_n$.
\begin{verbatim}
> 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
\end{verbatim}
The functions \texttt{typeVars}, \texttt{typeConstrs},
\texttt{typeSkolems} return a list of all type variables, type
constructors, or skolems occurring in a type $t$, respectively. Note
that \texttt{TypeConstrained} variables are not included in the set of
type variables because they cannot be generalized.
\begin{verbatim}
> 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
> vars (TypeRecord fs rtv) tvs =
> foldr vars (maybe tvs (: tvs) rtv) (map snd fs)
> 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
> constrs (TypeRecord fs _) tcs = foldr constrs tcs (map snd fs)
> 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
> skolems (TypeRecord fs _) sks = foldr skolems sks (map snd fs)
> 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)
> = maybe (True, (i1,i2):is)
> (\ i2' -> (i2 == i2', is))
> (lookup i1 is)
> equ is (TypeConstrained ts1 i1) (TypeConstrained ts2 i2)
> = let (res, is') = equs is ts1 ts2
> in maybe (res, (i1,i2):is')
> (\ i2' -> (res && i2 == i2', is'))
> (lookup i1 is')
> 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)
> = maybe (True, (i1,i2):is)
> (\ i2' -> (i2 == i2', is))
> (lookup i1 is)
> equ is (TypeRecord fs1 r1) (TypeRecord fs2 r2)
> | isJust r1 && isJust r2
> = let (res1, is1) = equ is (TypeVariable (fromJust r1))
> (TypeVariable (fromJust r2))
> (res2, is2) = equRecords is1 fs1 fs2
> in (res1 && res2, is2)
> | isNothing r1 && isNothing r2 = equRecords is fs1 fs2
> | otherwise = (False, is)
> equ is _ _ = (False, is)
>
> equRecords is fs1 fs2 | length fs1 == length fs2 = equrec is fs1 fs2
> | otherwise = (False, is)
> where
> equrec is' [] _ = (True, is')
> equrec is' ((l,t):fs1') fs2'
> = let (res1, is1) = maybe (False,is') (equ is' t) (lookup l fs2')
> (res2, is2) = equrec is1 fs1' fs2'
> in (res1 && res2, is2)
>
> equs is [] [] = (True, is)
> equs _ [] _ = error "pattern not defined" -- TODO
> equs _ _ [] = error "pattern not defined" -- TODO
> equs is (t1':ts1) (t2':ts2)
> = let (res1, is1) = equ is t1' t2'
> (res2, is2) = equs is1 ts1 ts2
> in (res1 && res2, is2)
\end{verbatim}
We support two kinds of quantifications of types here, universally
quantified type schemes $\forall\overline{\alpha} .
\tau(\overline{\alpha})$ and universally and existentially quantified
type schemes $\forall\overline{\alpha} \exists\overline{\eta} .
\tau(\overline{\alpha},\overline{\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 \texttt{ForAll} and \texttt{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.
\begin{verbatim}
> data TypeScheme = ForAll Int Type deriving (Show, Eq)
> data ExistTypeScheme = ForAllExist Int Int Type deriving (Show, Eq)
\end{verbatim}
The functions \texttt{monoType} and \texttt{polyType} translate a type
$\tau$ into a monomorphic type scheme $\forall.\tau$ and a polymorphic
type scheme $\forall\overline{\alpha}.\tau$ where $\overline{\alpha} =
\textrm{fv}(\tau)$, respectively. \texttt{polyType} assumes that all
universally quantified variables in the type are assigned indices
starting with 0 and does not renumber the variables.
\begin{verbatim}
> monoType :: Type -> TypeScheme
> monoType ty = ForAll 0 ty
> polyType :: Type -> TypeScheme
> polyType ty = ForAll (maximum (-1 : typeVars ty) + 1) ty
\end{verbatim}
There are a few predefined types:
\begin{verbatim}
> unitType :: Type
> unitType = primType unitId []
> boolType :: Type
> boolType = primType boolId []
> charType :: Type
> charType = primType charId []
> intType :: Type
> intType = primType intId []
> floatType :: Type
> floatType = primType floatId []
> stringType :: Type
> stringType = listType charType
> successType :: Type
> successType = primType successId []
> listType :: Type -> Type
> listType ty = primType listId [ty]
> ioType :: Type -> Type
> ioType ty = primType ioId [ty]
> tupleType :: [Type] -> Type
> tupleType tys = primType (tupleId (length tys)) tys
> primType :: Ident -> [Type] -> Type
> primType = TypeConstructor . qualifyWith preludeMIdent
> typeVar :: Int -> Type
> typeVar = TypeVariable
> predefTypes :: [(Type, [DataConstr])]
> predefTypes = let a = typeVar 0 in
> [ (unitType , [ DataConstr unitId 0 [] ])
> , (listType a, [ DataConstr nilId 0 []
> , DataConstr consId 0 [a, listType a]])
> ]
> 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 _ (TypeVariable 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 _ (TypeSkolem k) = TypeSkolem k
> qualifyType m (TypeRecord fs rty) =
> TypeRecord (map (\ (l,ty) -> (l, qualifyType m ty)) fs) rty
> unqualifyType :: ModuleIdent -> Type -> Type
> unqualifyType m (TypeConstructor tc tys) =
> TypeConstructor (qualUnqualify m tc) (map (unqualifyType m) tys)
> unqualifyType _ (TypeVariable tv) = TypeVariable tv
> unqualifyType m (TypeConstrained tys tv) =