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

Source checks are now chained and no longer call error functions

parent 12ccd1f1
......@@ -13,8 +13,8 @@ marked with a boolean flag (see below).
\begin{verbatim}
> module Base.Subst
> ( Subst (..), IntSubst (..), idSubst, substToList, bindSubst, unbindSubst
> , compose, substVar', isubstVar, restrictSubstTo
> ( Subst (..), IntSubst (..), idSubst, singleSubst, bindSubst, unbindSubst
> , substToList, compose, substVar', isubstVar, restrictSubstTo
> ) where
> import qualified Data.Map as Map
......@@ -27,6 +27,9 @@ marked with a boolean flag (see below).
> substToList :: Ord v => Subst v e -> [(v, e)]
> substToList (Subst _ sigma) = Map.toList sigma
> singleSubst :: Ord v => v -> e -> Subst v e
> singleSubst v e = bindSubst v e idSubst
> bindSubst :: Ord v => v -> e -> Subst v e -> Subst v e
> bindSubst v e (Subst comp sigma) = Subst comp $ Map.insert v e sigma
......
......@@ -10,7 +10,7 @@ This module implements substitutions on types.
\begin{verbatim}
> module Base.TypeSubst
> ( module Base.TypeSubst, idSubst, bindSubst, compose
> ( module Base.TypeSubst, idSubst, singleSubst, bindSubst, compose
> ) where
> import Data.List (nub)
......
......@@ -27,6 +27,19 @@ import qualified Checks.WarnCheck as WC (warnCheck)
import CompilerEnv
import CompilerOpts
data CheckResult a
= CheckSuccess a
| CheckFailed [Message]
instance Monad CheckResult where
return = CheckSuccess
(>>=) = thenCheck
thenCheck :: CheckResult a -> (a -> CheckResult b) -> CheckResult b
thenCheck chk cont = case chk of
CheckSuccess a -> cont a
CheckFailed errs -> CheckFailed errs
-- TODO: More documentation
-- |Check the kinds of type definitions and signatures.
......@@ -34,10 +47,10 @@ import CompilerOpts
-- * Declarations: Nullary type constructors and type variables are
-- disambiguated
-- * Environment: remains unchanged
kindCheck :: CompilerEnv -> Module -> (CompilerEnv, Module)
kindCheck :: CompilerEnv -> Module -> CheckResult (CompilerEnv, Module)
kindCheck env (Module m es is ds)
| null msgs = (env, Module m es is ds')
| otherwise = errorMessages msgs
| null msgs = CheckSuccess (env, Module m es is ds')
| otherwise = CheckFailed msgs
where (ds', msgs) = KC.kindCheck (moduleIdent env) (tyConsEnv env) ds
-- |Check for a correct syntax.
......@@ -45,36 +58,37 @@ kindCheck env (Module m es is ds)
-- * Declarations: Nullary data constructors and variables are
-- disambiguated
-- * Environment: remains unchanged
syntaxCheck :: Options -> CompilerEnv -> Module -> (CompilerEnv, Module)
syntaxCheck :: Options -> CompilerEnv -> Module -> CheckResult (CompilerEnv, Module)
syntaxCheck opts env (Module m es is ds)
| null msgs = (env, Module m es is ds')
| otherwise = errorMessages msgs
| null msgs = CheckSuccess (env, Module m es is ds')
| otherwise = CheckFailed msgs
where (ds', msgs) = SC.syntaxCheck opts (moduleIdent env)
(valueEnv env) (tyConsEnv env) ds
-- |Check the precedences of infix operators.
-- In addition, the abstract syntax tree is rearranged to reflect the
-- relative precedences; the operator precedence environment is updated.
precCheck :: CompilerEnv -> Module -> (CompilerEnv, Module)
precCheck :: CompilerEnv -> Module -> CheckResult (CompilerEnv, Module)
precCheck env (Module m es is ds)
| null msgs = (env { opPrecEnv = pEnv' }, Module m es is ds')
| otherwise = errorMessages msgs
| null msgs = CheckSuccess (env { opPrecEnv = pEnv' }, Module m es is ds')
| otherwise = CheckFailed msgs
where (ds', pEnv', msgs) = PC.precCheck (moduleIdent env) (opPrecEnv env) ds
-- |Apply the correct typing of the module.
-- The declarations remain unchanged; the type constructor and value
-- environments are updated.
typeCheck :: CompilerEnv -> Module -> (CompilerEnv, Module)
typeCheck env mdl@(Module _ _ _ ds) =
(env { tyConsEnv = tcEnv', valueEnv = tyEnv' }, mdl)
where (tcEnv', tyEnv') = TC.typeCheck (moduleIdent env)
(tyConsEnv env) (valueEnv env) ds
typeCheck :: CompilerEnv -> Module -> CheckResult (CompilerEnv, Module)
typeCheck env mdl@(Module _ _ _ ds)
| null msgs = CheckSuccess (env { tyConsEnv = tcEnv', valueEnv = tyEnv' }, mdl)
| otherwise = CheckFailed msgs
where (tcEnv', tyEnv', msgs) = TC.typeCheck (moduleIdent env)
(tyConsEnv env) (valueEnv env) ds
-- |Check the export specification
exportCheck :: CompilerEnv -> Module -> (CompilerEnv, Module)
exportCheck :: CompilerEnv -> Module -> CheckResult (CompilerEnv, Module)
exportCheck env (Module m es is ds)
| null msgs = (env, Module m es' is ds)
| otherwise = errorMessages msgs
| null msgs = CheckSuccess (env, Module m es' is ds)
| otherwise = CheckFailed msgs
where (es', msgs) = EC.exportCheck (moduleIdent env) (aliasEnv env)
(tyConsEnv env) (valueEnv env) es
......
......@@ -23,8 +23,8 @@ type annotation is present.
> module Checks.TypeCheck (typeCheck) where
> import Control.Monad (liftM, replicateM, unless)
> import qualified Control.Monad.State as S (State, runState, gets, modify)
> import Control.Monad (liftM, liftM2, liftM3, replicateM, unless)
> import qualified Control.Monad.State as S (State, execState, gets, modify)
> import Data.List (nub, partition)
> import qualified Data.Map as Map (Map, empty, insert, lookup)
> import Data.Maybe (catMaybes, fromJust, fromMaybe, isJust, listToMaybe, maybeToList)
......@@ -38,7 +38,7 @@ type annotation is present.
> import Base.CurryTypes (fromQualType, toType, toTypes)
> import Base.Expr
> import Base.Messages (errorAt, errorAt', internalError)
> import Base.Messages (Message, toMessage, posErr, internalError)
> import Base.SCC
> import Base.TopEnv
> import Base.Types
......@@ -61,18 +61,21 @@ environment is initialized by adding all types defined in the current
module. Next, the types of all data constructors and field labels
are entered into the type environment and then a type inference
for all function and value definitions is performed.
The type checker returns the resulting type
constructor and type environments.
The type checker returns the resulting type constructor and type environments.
\begin{verbatim}
> typeCheck :: ModuleIdent -> TCEnv -> ValueEnv -> [Decl] -> (TCEnv, ValueEnv)
> typeCheck m tcEnv tyEnv decls = (tcEnv', subst theta tyEnv')
> typeCheck :: ModuleIdent -> TCEnv -> ValueEnv -> [Decl]
> -> (TCEnv, ValueEnv, [Message])
> typeCheck m tcEnv tyEnv decls = execTCM check initState
> where
> (_, theta, tyEnv') = runTCM (tcDecls m tcEnv' emptySigEnv vds) initState
> tcEnv' = bindTypes m tds tcEnv
> (tds, vds) = partition isTypeDecl decls
> initState = TcState 0 idSubst initEnv
> initEnv = bindLabels tcEnv' $ bindConstrs m tcEnv' tyEnv
> check = do
> checkTypeSynonyms m tds
> bindTypes tds
> bindConstrs
> bindLabels
> tcDecls vds
> (tds, vds) = partition isTypeDecl decls
> initState = TcState m tcEnv tyEnv idSubst emptySigEnv 0 []
\end{verbatim}
......@@ -82,21 +85,28 @@ generating fresh type variables.
\begin{verbatim}
> data TcState = TcState
> { nextId :: Int
> , typeSubst :: TypeSubst
> , valueEnv :: ValueEnv
> { moduleIdent :: ModuleIdent
> , tyConsEnv :: TCEnv
> , valueEnv :: ValueEnv
> , typeSubst :: TypeSubst
> , sigEnv :: SigEnv
> , nextId :: Int
> , errors :: [Message]
> }
> type TCM = S.State TcState
> getNextId :: TCM Int
> getNextId = do
> nid <- S.gets nextId
> S.modify $ \ s -> s { nextId = succ nid }
> return nid
> getModuleIdent :: TCM ModuleIdent
> getModuleIdent = S.gets moduleIdent
> modifyTypeSubst :: (TypeSubst -> TypeSubst) -> TCM ()
> modifyTypeSubst f = S.modify $ \ s -> s { typeSubst = f $ typeSubst s }
> getTyConsEnv :: TCM TCEnv
> getTyConsEnv = S.gets tyConsEnv
> setTyConsEnv :: TCEnv -> TCM ()
> setTyConsEnv tcEnv = S.modify $ \ s -> s { tyConsEnv = tcEnv }
> getValueEnv :: TCM ValueEnv
> getValueEnv = S.gets valueEnv
> modifyValueEnv :: (ValueEnv -> ValueEnv) -> TCM ()
> modifyValueEnv f = S.modify $ \ s -> s { valueEnv = f $ valueEnv s }
......@@ -104,12 +114,30 @@ generating fresh type variables.
> getTypeSubst :: TCM TypeSubst
> getTypeSubst = S.gets typeSubst
> getValueEnv :: TCM ValueEnv
> getValueEnv = S.gets valueEnv
> modifyTypeSubst :: (TypeSubst -> TypeSubst) -> TCM ()
> modifyTypeSubst f = S.modify $ \ s -> s { typeSubst = f $ typeSubst s }
> getSigEnv :: TCM SigEnv
> getSigEnv = S.gets sigEnv
> modifySigEnv :: (SigEnv -> SigEnv) -> TCM ()
> modifySigEnv f = S.modify $ \ s -> s { sigEnv = f $ sigEnv s }
> getNextId :: TCM Int
> getNextId = do
> nid <- S.gets nextId
> S.modify $ \ s -> s { nextId = succ nid }
> return nid
> runTCM :: TCM a -> TcState -> (a, TypeSubst, ValueEnv)
> runTCM tcm s = let (a, s') = S.runState tcm s
> in (a, typeSubst s', valueEnv s')
> report :: Message -> TCM ()
> report err = S.modify $ \ s -> s { errors = err : errors s }
> execTCM :: TCM a -> TcState -> (TCEnv, ValueEnv, [Message])
> execTCM tcm s = let s' = S.execState tcm s
> in ( tyConsEnv s'
> , typeSubst s' `subst` valueEnv s'
> , reverse $ errors s'
> )
\end{verbatim}
\paragraph{Defining Types}
......@@ -137,60 +165,66 @@ side by \texttt{anonId} before passing them to \texttt{expandMonoType}
and \texttt{expandMonoTypes}, respectively.
\begin{verbatim}
> bindTypes :: ModuleIdent -> [Decl] -> TCEnv -> TCEnv
> bindTypes m ds tcEnv = tcEnv'
> where tcEnv' = foldr (bindTC m tcEnv') tcEnv (sortTypeDecls m ds)
> checkTypeSynonyms :: ModuleIdent -> [Decl] -> TCM ()
> checkTypeSynonyms m = mapM_ (checkTypeDecls m) . scc bound free
> where
> bound (DataDecl _ tc _ _) = [tc]
> bound (NewtypeDecl _ tc _ _) = [tc]
> bound (TypeDecl _ tc _ _) = [tc]
> bound _ = []
> free (DataDecl _ _ _ _) = []
> free (NewtypeDecl _ _ _ _) = []
> free (TypeDecl _ _ _ ty) = ft m ty []
> free _ = []
> checkTypeDecls :: ModuleIdent -> [Decl] -> TCM ()
> checkTypeDecls _ [] =
> internalError "TypeCheck.checkTypeDecls: empty list"
> checkTypeDecls _ [DataDecl _ _ _ _] = return ()
> checkTypeDecls _ [NewtypeDecl _ _ _ _] = return ()
> checkTypeDecls m [TypeDecl _ tc _ ty]
> | tc `elem` ft m ty [] = report $ errRecursiveTypes [tc]
> | otherwise = return ()
> checkTypeDecls _ (TypeDecl _ tc _ _ : ds) =
> report $ errRecursiveTypes $ tc : [tc' | TypeDecl _ tc' _ _ <- ds]
> checkTypeDecls _ _ =
> internalError "TypeCheck.checkTypeDecls: no type synonym"
> ft :: ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
> ft m (ConstructorType tc tys) tcs =
> maybe id (:) (localIdent m tc) (foldr (ft m) tcs tys)
> ft _ (VariableType _) tcs = tcs
> ft m (TupleType tys) tcs = foldr (ft m) tcs tys
> ft m (ListType ty) tcs = ft m ty tcs
> ft m (ArrowType ty1 ty2) tcs = ft m ty1 $ ft m ty2 $ tcs
> ft m (RecordType fs rty) tcs =
> foldr (ft m) (maybe tcs (\ty -> ft m ty tcs) rty) (map snd fs)
> bindTypes :: [Decl] -> TCM ()
> bindTypes ds = do
> m <- getModuleIdent
> tcEnv <- getTyConsEnv
> let tcEnv' = foldr (bindTC m tcEnv') tcEnv ds
> setTyConsEnv tcEnv'
> bindTC :: ModuleIdent -> TCEnv -> Decl -> TCEnv -> TCEnv
> bindTC m tcEnv (DataDecl _ tc tvs cs) =
> bindTypeInfo DataType m tc tvs (map (Just . mkData) cs)
> where
> mkData (ConstrDecl _ evs c tys) = DataConstr c (length evs) tys'
> where tys' = expandMonoTypes m tcEnv (cleanTVars tvs evs) tys
> mkData (ConOpDecl _ evs ty1 op ty2) = DataConstr op (length evs) tys'
> where tys' = expandMonoTypes m tcEnv (cleanTVars tvs evs) [ty1,ty2]
> mkData (ConstrDecl _ evs c tys) = mkData' evs c tys
> mkData (ConOpDecl _ evs ty1 op ty2) = mkData' evs op [ty1, ty2]
> mkData' evs c tys = DataConstr c (length evs) $
> expandMonoTypes m tcEnv (cleanTVars tvs evs) tys
> bindTC m tcEnv (NewtypeDecl _ tc tvs (NewConstrDecl _ evs c ty)) =
> bindTypeInfo RenamingType m tc tvs (DataConstr c (length evs) [ty'])
> where ty' = expandMonoType m tcEnv (cleanTVars tvs evs) ty
> where ty' = expandMonoType' m tcEnv (cleanTVars tvs evs) ty
> bindTC m tcEnv (TypeDecl _ tc tvs ty) =
> bindTypeInfo AliasType m tc tvs (expandMonoType m tcEnv tvs ty)
> bindTypeInfo AliasType m tc tvs (expandMonoType' m tcEnv tvs ty)
> bindTC _ _ _ = id
> cleanTVars :: [Ident] -> [Ident] -> [Ident]
> cleanTVars tvs evs = [if tv `elem` evs then anonId else tv | tv <- tvs]
> sortTypeDecls :: ModuleIdent -> [Decl] -> [Decl]
> sortTypeDecls m = map (typeDecl m) . scc bound free
> where bound (DataDecl _ tc _ _) = [tc]
> bound (NewtypeDecl _ tc _ _) = [tc]
> bound (TypeDecl _ tc _ _) = [tc]
> bound _ = internalError "TypeCheck.sortTypeDecls: no type decl"
> free (DataDecl _ _ _ _) = []
> free (NewtypeDecl _ _ _ _) = []
> free (TypeDecl _ _ _ ty) = ft m ty []
> free _ = internalError "TypeCheck.sortTypeDecls: no type decl"
> typeDecl :: ModuleIdent -> [Decl] -> Decl
> typeDecl _ [] = internalError "TypeCheck.typeDecl"
> typeDecl _ [d@(DataDecl _ _ _ _)] = d
> typeDecl _ [d@(NewtypeDecl _ _ _ _)] = d
> typeDecl m [d@(TypeDecl _ tc _ ty)]
> | tc `elem` ft m ty [] = errorAt' $ errRecursiveTypes [tc]
> | otherwise = d
> typeDecl _ (TypeDecl _ tc _ _ : ds) =
> errorAt' $ errRecursiveTypes $ tc : [tc' | TypeDecl _ tc' _ _ <- ds]
> typeDecl _ _ = internalError "TypeCheck.typeDecl: no pattern match"
> ft :: ModuleIdent -> TypeExpr -> [Ident] -> [Ident]
> ft m (ConstructorType tc tys) tcs =
> maybe id (:) (localIdent m tc) (foldr (ft m) tcs tys)
> ft _ (VariableType _) tcs = tcs
> ft m (TupleType tys) tcs = foldr (ft m) tcs tys
> ft m (ListType ty) tcs = ft m ty tcs
> ft m (ArrowType ty1 ty2) tcs = ft m ty1 $ ft m ty2 $ tcs
> ft m (RecordType fs rty) tcs =
> foldr (ft m) (maybe tcs (\ty -> ft m ty tcs) rty) (map snd fs)
\end{verbatim}
\paragraph{Defining Data Constructors}
In the next step, the types of all data constructors are entered into
......@@ -199,8 +233,14 @@ constructor environment. Thus, we can be sure that all type variables
have been properly renamed and all type synonyms are already expanded.
\begin{verbatim}
> bindConstrs :: ModuleIdent -> TCEnv -> ValueEnv -> ValueEnv
> bindConstrs m tcEnv tyEnv = foldr (bindData . snd) tyEnv
> bindConstrs :: TCM ()
> bindConstrs = do
> m <- getModuleIdent
> tcEnv <- getTyConsEnv
> modifyValueEnv $ bindConstrs' m tcEnv
> bindConstrs' :: ModuleIdent -> TCEnv -> ValueEnv -> ValueEnv
> bindConstrs' m tcEnv tyEnv = foldr (bindData . snd) tyEnv
> $ localBindings tcEnv
> where
> bindData (DataType tc n cs) tyEnv' =
......@@ -227,9 +267,14 @@ again, we can be sure that all type variables
have been properly renamed and all type synonyms are already expanded.
\begin{verbatim}
> bindLabels :: TCEnv -> ValueEnv -> ValueEnv
> bindLabels tcEnv tyEnv = foldr (bindFieldLabels . snd) tyEnv
> $ localBindings tcEnv
> bindLabels :: TCM ()
> bindLabels = do
> tcEnv <- getTyConsEnv
> modifyValueEnv $ bindLabels' tcEnv
> bindLabels' :: TCEnv -> ValueEnv -> ValueEnv
> bindLabels' tcEnv tyEnv = foldr (bindFieldLabels . snd) tyEnv
> $ localBindings tcEnv
> where
> bindFieldLabels (AliasType r _ (TypeRecord fs _)) env =
> foldr (bindField r) env fs
......@@ -320,26 +365,26 @@ either one of the basic types or \texttt{()}.
Addendum.~\cite{Chakravarty03:FFI}}
\begin{verbatim}
> tcDecls :: ModuleIdent -> TCEnv -> SigEnv -> [Decl] -> TCM ()
> tcDecls m tcEnv sigs ds =
> mapM_ (tcDeclGroup m tcEnv (foldr bindTypeSigs sigs ods))
> (scc bv (qfv m) vds)
> tcDecls :: [Decl] -> TCM ()
> tcDecls ds = do
> m <- getModuleIdent
> oldSig <- getSigEnv
> modifySigEnv $ \ sigs -> foldr bindTypeSigs sigs ods
> mapM_ tcDeclGroup $ scc bv (qfv m) vds
> modifySigEnv (const oldSig)
> where (vds, ods) = partition isValueDecl ds
> tcDeclGroup :: ModuleIdent -> TCEnv -> SigEnv -> [Decl] -> TCM ()
> tcDeclGroup m tcEnv _ [ExternalDecl _ _ _ f ty] =
> tcExternal m tcEnv f ty
> tcDeclGroup m tcEnv sigs [FlatExternalDecl _ fs] =
> mapM_ (tcFlatExternal m tcEnv sigs) fs
> tcDeclGroup m tcEnv sigs [ExtraVariables _ vs] =
> mapM_ (tcExtraVar m tcEnv sigs) vs
> tcDeclGroup m tcEnv sigs ds = do
> tcDeclGroup :: [Decl] -> TCM ()
> tcDeclGroup [ExternalDecl _ _ _ f ty] = tcExternal f ty
> tcDeclGroup [FlatExternalDecl _ fs] = mapM_ tcFlatExternal fs
> tcDeclGroup [ExtraVariables _ vs] = mapM_ tcExtraVar vs
> tcDeclGroup ds = do
> tyEnv0 <- getValueEnv
> tysLhs <- mapM (tcDeclLhs m tcEnv sigs) ds
> tysRhs <- mapM (tcDeclRhs m tcEnv tyEnv0 sigs) ds
> sequence_ (zipWith3 (unifyDecl m) ds tysLhs tysRhs)
> tysLhs <- mapM tcDeclLhs ds
> tysRhs <- mapM (tcDeclRhs tyEnv0) ds
> sequence_ (zipWith3 unifyDecl ds tysLhs tysRhs)
> theta <- getTypeSubst
> mapM_ (genDecl m tcEnv sigs (fvEnv (subst theta tyEnv0)) theta) ds
> mapM_ (genDecl (fvEnv (subst theta tyEnv0)) theta) ds
> --tcDeclGroup m tcEnv _ [ForeignDecl p cc _ f ty] =
> -- tcForeignFunct m tcEnv p cc f ty
......@@ -364,51 +409,57 @@ either one of the basic types or \texttt{()}.
> -- isCResultType _ = False
> -- basicTypeId = [qBoolId,qCharId,qIntId,qFloatId]
> tcExternal :: ModuleIdent -> TCEnv -> Ident -> TypeExpr -> TCM ()
> tcExternal m tcEnv f ty = modifyValueEnv $ bindFun m f (arrowArity ty') tySc
> where tySc@(ForAll _ ty') = expandPolyType m tcEnv ty
> tcFlatExternal :: ModuleIdent -> TCEnv -> SigEnv -> Ident -> TCM ()
> tcFlatExternal m tcEnv sigs f = case lookupTypeSig f sigs of
> Nothing -> internalError "TypeCheck.tcFlatExternal"
> Just ty -> do
> let tySc@(ForAll _ ty') = expandPolyType m tcEnv ty
> modifyValueEnv $ bindFun m f (arrowArity ty') tySc
> tcExtraVar :: ModuleIdent -> TCEnv -> SigEnv -> Ident -> TCM ()
> tcExtraVar m tcEnv sigs v = case lookupTypeSig v sigs of
> Nothing -> do
> ty <- freshTypeVar
> modifyValueEnv $ bindFun m v (arrowArity ty) $ monoType ty
> Just ty
> | n == 0 -> modifyValueEnv $ bindFun m v (arrowArity ty') $ monoType ty'
> | otherwise -> errorAt' $ errPolymorphicFreeVar v
> where ForAll n ty' = expandPolyType m tcEnv ty
> tcDeclLhs :: ModuleIdent -> TCEnv -> SigEnv -> Decl -> TCM Type
> tcDeclLhs m tcEnv sigs (FunctionDecl p f _) =
> tcConstrTerm m tcEnv sigs p (VariablePattern f)
> tcDeclLhs m tcEnv sigs (PatternDecl p t _) = tcConstrTerm m tcEnv sigs p t
> tcDeclLhs _ _ _ _ = internalError "TypeCheck.tcDeclLhs: no pattern match"
> tcDeclRhs :: ModuleIdent -> TCEnv -> ValueEnv -> SigEnv -> Decl -> TCM Type
> tcDeclRhs m tcEnv tyEnv0 sigs (FunctionDecl _ f (eq:eqs)) =
> tcEquation m tcEnv tyEnv0 sigs eq >>= flip tcEqns eqs
> tcExternal :: Ident -> TypeExpr -> TCM ()
> tcExternal f ty = do
> m <- getModuleIdent
> tySc@(ForAll _ ty') <- expandPolyType ty
> modifyValueEnv $ bindFun m f (arrowArity ty') tySc
> tcFlatExternal :: Ident -> TCM ()
> tcFlatExternal f = do
> sigs <- getSigEnv
> case lookupTypeSig f sigs of
> Nothing -> internalError "TypeCheck.tcFlatExternal"
> Just ty -> do
> m <- getModuleIdent
> tySc@(ForAll _ ty') <- expandPolyType ty
> modifyValueEnv $ bindFun m f (arrowArity ty') tySc
> tcExtraVar :: Ident -> TCM ()
> tcExtraVar v = do
> sigs <- getSigEnv
> m <- getModuleIdent
> case lookupTypeSig v sigs of
> Nothing -> do
> ty <- freshTypeVar
> modifyValueEnv $ bindFun m v (arrowArity ty) $ monoType ty
> Just ty -> do
> ForAll n ty' <- expandPolyType ty
> unless (n == 0) $ report $ errPolymorphicFreeVar v
> modifyValueEnv $ bindFun m v (arrowArity ty') $ monoType ty'
> tcDeclLhs :: Decl -> TCM Type
> tcDeclLhs (FunctionDecl p f _) = tcConstrTerm p (VariablePattern f)
> tcDeclLhs (PatternDecl p t _) = tcConstrTerm p t
> tcDeclLhs _ = internalError "TypeCheck.tcDeclLhs: no pattern match"
> tcDeclRhs :: ValueEnv -> Decl -> TCM Type
> tcDeclRhs tyEnv0 (FunctionDecl _ f (eq:eqs)) = do
> tcEquation tyEnv0 eq >>= flip tcEqns eqs
> where tcEqns ty [] = return ty
> tcEqns ty (eq1@(Equation p _ _):eqs1) =
> tcEquation m tcEnv tyEnv0 sigs eq1 >>=
> unify p "equation" (ppDecl (FunctionDecl p f [eq1])) m ty >>
> tcEqns ty eqs1
> tcDeclRhs m tcEnv tyEnv0 sigs (PatternDecl _ _ rhs) =
> tcRhs m tcEnv tyEnv0 sigs rhs
> tcDeclRhs _ _ _ _ _ = internalError "TypeCheck.tcDeclRhs: no pattern match"
> unifyDecl :: ModuleIdent -> Decl -> Type -> Type -> TCM ()
> unifyDecl m (FunctionDecl p f _) =
> unify p "function binding" (text "Function:" <+> ppIdent f) m
> unifyDecl m (PatternDecl p t _) =
> unify p "pattern binding" (ppConstrTerm 0 t) m
> unifyDecl _ _ = internalError "TypeCheck.unifyDecl: no pattern match"
> tcEqns ty (eq1@(Equation p _ _):eqs1) = do
> tcEquation tyEnv0 eq1 >>=
> unify p "equation" (ppDecl (FunctionDecl p f [eq1])) ty >>
> tcEqns ty eqs1
> tcDeclRhs tyEnv0 (PatternDecl _ _ rhs) = tcRhs tyEnv0 rhs
> tcDeclRhs _ _ = internalError "TypeCheck.tcDeclRhs: no pattern match"
> unifyDecl :: Decl -> Type -> Type -> TCM ()
> unifyDecl (FunctionDecl p f _) =
> unify p "function binding" (text "Function:" <+> ppIdent f)
> unifyDecl (PatternDecl p t _) =
> unify p "pattern binding" (ppConstrTerm 0 t)
> unifyDecl _ = internalError "TypeCheck.unifyDecl: no pattern match"
\end{verbatim}
In Curry we cannot generalize the types of let-bound variables because
......@@ -434,132 +485,140 @@ specific. Therefore, if the inferred type does not match the type
signature the declared type must be too general.
\begin{verbatim}
> genDecl :: ModuleIdent -> TCEnv -> SigEnv -> Set.Set Int -> TypeSubst -> Decl
> -> TCM ()
> genDecl m tcEnv sigs lvs theta (FunctionDecl _ f (Equation _ lhs _ : _)) =
> modifyValueEnv (genVar True m tcEnv sigs lvs theta arity f)
> genDecl :: Set.Set Int -> TypeSubst -> Decl -> TCM ()
> genDecl lvs theta (FunctionDecl _ f (Equation _ lhs _ : _)) =
> genVar True lvs theta arity f
> where arity = Just $ length $ snd $ flatLhs lhs
> genDecl m tcEnv sigs lvs theta (PatternDecl _ t _) =
> mapM_ (modifyValueEnv . genVar False m tcEnv sigs lvs theta Nothing) (bv t)
> genDecl _ _ _ _ _ _ = internalError "TypeCheck.genDecl: no pattern match"
> genVar :: Bool -> ModuleIdent -> TCEnv -> SigEnv -> Set.Set Int -> TypeSubst
> -> Maybe Int -> Ident -> ValueEnv -> ValueEnv
> genVar poly m tcEnv sigs lvs theta ma v tyEnv = case lookupTypeSig v sigs of
> Just sigTy
> | cmpTypes sigma (expandPolyType m tcEnv sigTy) -> tyEnv'
> | otherwise -> errorAt (positionOfIdent v)
> (errTypeSigTooGeneral m what sigTy sigma)
> Nothing -> tyEnv'
> where what = text (if poly then "Function:" else "Variable:") <+> ppIdent v
> tyEnv' = rebindFun m v arity sigma tyEnv
> arity = fromMaybe (varArity v tyEnv) ma
> sigma = genType poly (subst theta (varType v tyEnv))
> genType poly' (ForAll n ty)
> | n > 0 = internalError $ "TypeCheck.genVar: " ++ showLine (positionOfIdent v) ++ show v ++ " :: " ++ show ty
> | poly' = gen lvs ty
> | otherwise = monoType ty
> cmpTypes (ForAll _ t1) (ForAll _ t2) = equTypes t1 t2
> tcEquation :: ModuleIdent -> TCEnv -> ValueEnv -> SigEnv -> Equation
> -> TCM Type
> tcEquation m tcEnv tyEnv0 sigs (Equation p lhs rhs) = do
> tys <- mapM (tcConstrTerm m tcEnv sigs p) ts
> ty <- tcRhs m tcEnv tyEnv0 sigs rhs
> checkSkolems p m (text "Function: " <+> ppIdent f) tyEnv0
> (foldr TypeArrow ty tys)
> genDecl lvs theta (PatternDecl _ t _) =
> mapM_ (genVar False lvs theta Nothing) (bv t)
> genDecl _ _ _ = internalError "TypeCheck.genDecl: no pattern match"
> genVar :: Bool -> Set.Set Int -> TypeSubst -> Maybe Int -> Ident -> TCM ()
> genVar poly lvs theta ma v = do
> sigs <- getSigEnv
> m <- getModuleIdent
> tyEnv <- getValueEnv
> let sigma = genType poly $ subst theta $ varType v tyEnv
> arity = fromMaybe (varArity v tyEnv) ma
> case lookupTypeSig v sigs of
> Nothing -> modifyValueEnv $ rebindFun m v arity sigma
> Just sigTy -> do
> sigma' <- expandPolyType sigTy