module Checks.InterfaceCheck (interfaceCheck) where
import Control.Monad (unless)
import qualified Control.Monad.State as S
import Data.Maybe (fromMaybe)
import Curry.Base.Ident
import Curry.Base.Position
import Curry.Base.Pretty
import Curry.Syntax
import Base.CurryTypes
import Base.Messages (Message, posMessage, internalError)
import Base.TopEnv
import Base.Types
import Env.OpPrec
import Env.TypeConstructor
import Env.Value
data ICState = ICState
{ moduleIdent :: ModuleIdent
, precEnv :: OpPrecEnv
, tyConsEnv :: TCEnv
, valueEnv :: ValueEnv
, errors :: [Message]
}
type IC = S.State ICState
getModuleIdent :: IC ModuleIdent
getModuleIdent = S.gets moduleIdent
getPrecEnv :: IC OpPrecEnv
getPrecEnv = S.gets precEnv
getTCEnv :: IC TCEnv
getTCEnv = S.gets tyConsEnv
getValueEnv :: IC ValueEnv
getValueEnv = S.gets valueEnv
report :: Message -> IC ()
report msg = S.modify $ \ s -> s { errors = msg : errors s }
ok :: IC ()
ok = return ()
interfaceCheck :: OpPrecEnv -> TCEnv -> ValueEnv -> Interface -> [Message]
interfaceCheck pEnv tcEnv tyEnv (Interface m _ ds) = reverse (errors s)
where s = S.execState (mapM_ checkImport ds) (ICState m pEnv tcEnv tyEnv [])
checkImport :: IDecl -> IC ()
checkImport (IInfixDecl p fix pr op) = checkPrecInfo check p op
where check (PrecInfo op' (OpPrec fix' pr')) =
op == op' && fix == fix' && pr == pr'
checkImport (HidingDataDecl p tc tvs)
= checkTypeInfo "hidden data type" check p tc
where check (DataType tc' n' _)
| tc == tc' && length tvs == n' = Just ok
check (RenamingType tc' n' _)
| tc == tc' && length tvs == n' = Just ok
check _ = Nothing
checkImport (IDataDecl p tc tvs cs _) = checkTypeInfo "data type" check p tc
where check (DataType tc' n' cs')
| tc == tc' && length tvs == n' &&
(null cs || map constrId cs == map constrIdent cs')
= Just (mapM_ (checkConstrImport tc tvs) cs)
check (RenamingType tc' n' _)
| tc == tc' && length tvs == n' && null cs = Just ok
check _ = Nothing
checkImport (INewtypeDecl p tc tvs nc _)
= checkTypeInfo "newtype" check p tc
where check (RenamingType tc' n' nc')
| tc == tc' && length tvs == n' && nconstrId nc == constrIdent nc'
= Just (checkNewConstrImport tc tvs nc)
check _ = Nothing
checkImport (ITypeDecl p tc tvs ty) = do
m <- getModuleIdent
let check (AliasType tc' n' ty')
| tc == tc' && length tvs == n' && toQualType m tvs ty == ty'
= Just ok
check _ = Nothing
checkTypeInfo "synonym type" check p tc
checkImport (IFunctionDecl p f n ty) = do
m <- getModuleIdent
let check (Value f' n' (ForAll _ ty')) =
f == f' && n' == n && toQualType m [] ty == ty'
check _ = False
checkValueInfo "function" check p f
checkConstrImport :: QualIdent -> [Ident] -> ConstrDecl -> IC ()
checkConstrImport tc tvs (ConstrDecl p evs c tys) = do
m <- getModuleIdent
let qc = qualifyLike tc c
checkConstr (DataConstructor c' _ _ (ForAllExist uqvs eqvs ty')) =
qc == c' && length evs == eqvs && length tvs == uqvs &&
toQualTypes m tvs tys == arrowArgs ty'
checkConstr _ = False
checkValueInfo "data constructor" checkConstr p qc
checkConstrImport tc tvs (ConOpDecl p evs ty1 op ty2) = do
m <- getModuleIdent
let qc = qualifyLike tc op
checkConstr (DataConstructor c' _ _ (ForAllExist uqvs eqvs ty')) =
qc == c' && length evs == eqvs && length tvs == uqvs &&
toQualTypes m tvs [ty1,ty2] == arrowArgs ty'
checkConstr _ = False
checkValueInfo "data constructor" checkConstr p qc
checkConstrImport tc tvs (RecordDecl p evs c fs) = do
m <- getModuleIdent
let qc = qualifyLike tc c
(ls, tys) = unzip [(l, ty) | FieldDecl _ labels ty <- fs, l <- labels]
checkConstr (DataConstructor c' _ ls' (ForAllExist uqvs eqvs ty')) =
qc == c' && length evs == eqvs && length tvs == uqvs && ls == ls' &&
toQualTypes m tvs tys == arrowArgs ty'
checkConstr _ = False
checkValueInfo "data constructor" checkConstr p qc
checkNewConstrImport :: QualIdent -> [Ident] -> NewConstrDecl -> IC ()
checkNewConstrImport tc tvs (NewConstrDecl p evs c ty) = do
m <- getModuleIdent
let qc = qualifyLike tc c
checkNewConstr (NewtypeConstructor c' _ (ForAllExist uqvs eqvs ty')) =
qc == c' && length evs == eqvs && length tvs == uqvs &&
toQualType m tvs ty == head (arrowArgs ty')
checkNewConstr _ = False
checkValueInfo "newtype constructor" checkNewConstr p qc
checkNewConstrImport tc tvs (NewRecordDecl p evs c (l, ty)) = do
m <- getModuleIdent
let qc = qualifyLike tc c
checkNewConstr (NewtypeConstructor c' l' (ForAllExist uqvs eqvs ty')) =
qc == c' && length evs == eqvs && length tvs == uqvs && l == l' &&
toQualType m tvs ty == head (arrowArgs ty')
checkNewConstr _ = False
checkValueInfo "newtype constructor" checkNewConstr p qc
checkPrecInfo :: (PrecInfo -> Bool) -> Position -> QualIdent -> IC ()
checkPrecInfo check p op = do
pEnv <- getPrecEnv
let checkInfo m op' = case qualLookupTopEnv op pEnv of
[] -> report $ errNoPrecedence p m op'
[prec] -> unless (check prec)
(report $ errImportConflict p "precedence" m op')
_ -> internalError "checkPrecInfo"
checkImported checkInfo op
checkTypeInfo :: String -> (TypeInfo -> Maybe (IC ())) -> Position
-> QualIdent -> IC ()
checkTypeInfo what check p tc = do
tcEnv <- getTCEnv
let checkInfo m tc' = case qualLookupTopEnv tc tcEnv of
[] -> report $ errNotExported p what m tc'
[ti] -> fromMaybe (report $ errImportConflict p what m tc') (check ti)
_ -> internalError "checkTypeInfo"
checkImported checkInfo tc
checkValueInfo :: String -> (ValueInfo -> Bool) -> Position
-> QualIdent -> IC ()
checkValueInfo what check p x = do
tyEnv <- getValueEnv
let checkInfo m x' = case qualLookupTopEnv x tyEnv of
[] -> report $ errNotExported p what m x'
[vi] -> unless (check vi) (report $ errImportConflict p what m x')
_ -> internalError "checkValueInfo"
checkImported checkInfo x
checkImported :: (ModuleIdent -> Ident -> IC ()) -> QualIdent -> IC ()
checkImported _ (QualIdent Nothing _) = ok
checkImported f (QualIdent (Just m) x) = f m x
errNotExported :: Position -> String -> ModuleIdent -> Ident -> Message
errNotExported p what m x = posMessage p $
text "Inconsistent module interfaces"
$+$ text "Module" <+> text (moduleName m)
<+> text "does not export"<+> text what <+> text (escName x)
errNoPrecedence :: Position -> ModuleIdent -> Ident -> Message
errNoPrecedence p m x = posMessage p $
text "Inconsistent module interfaces"
$+$ text "Module" <+> text (moduleName m)
<+> text "does not define a precedence for" <+> text (escName x)
errImportConflict :: Position -> String -> ModuleIdent -> Ident -> Message
errImportConflict p what m x = posMessage p $
text "Inconsistent module interfaces"
$+$ text "Declaration of" <+> text what <+> text (escName x)
<+> text "does not match its definition in module" <+> text (moduleName m)