TypeDecl.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant{- |
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantModule : $Header$
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantDescription : analyse type declarations
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantLicense : GPLv2 or higher
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantMaintainer : Christian.Maeder@dfki.de
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantStability : provisional
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantPortability : portable
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignacanalyse type declarations
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignac-}
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantmodule HasCASL.TypeDecl
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant ( anaFormula
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant , mapAnMaybe
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignac , anaTypeItems
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignac , dataPatToType
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignac , ana1Datatype
3437829f938dbb44527d91fbbc5f430a1243c5a5JnRouvignac , anaDatatype
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant , addDataSen
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant ) where
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport Common.Id
d81f6d00c343633159fc5ea08599d145135612c0ludovicpimport Common.AS_Annotation
43cf232e238dd2e98c8b2badc91071b6ada52956gary.williamsimport Common.Lib.State
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport qualified Data.Map as Map
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport qualified Data.Set as Set
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport Common.Result
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.As
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.AsUtils
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.Builtin
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.Le
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.ClassAna
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.TypeAna
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.ConvertTypePattern
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.DataAna
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.Unify
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.VarDecl
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.SubtypeDecl
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.MixAna
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport HasCASL.TypeCheck
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport Control.Monad
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport Data.Maybe
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantimport Data.List(group)
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant-- | resolve and type check a formula
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaFormula :: Annoted Term -> State Env (Maybe (Annoted Term, Annoted Term))
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaFormula at = do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant rt <- resolve $ item at
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant case rt of
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Nothing -> return Nothing
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Just t -> do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant mt <- typeCheck (mkLazyType unitType) t
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant return $ case mt of
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Nothing -> Nothing
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Just e -> Just (at { item = t }, at { item = e })
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaVars :: Env -> Vars -> Type -> Result Term
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaVars te vv t = case vv of
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Var v -> return $ QualVar $ VarDecl v t Other $ posOfId v
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant VarTuple vs ps -> let
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant (topTy, ts) = getTypeAppl t
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant n = length ts in
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant if n > 1 && lesserType te topTy (toProdType n nullRange) then
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant if n == length vs then
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant let lrs = zipWith (anaVars te) vs ts
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant lms = map maybeResult lrs in
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant if all isJust lms then
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant return $ TupleTerm (map fromJust lms) ps
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant else Result (concatMap diags lrs) Nothing
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant else mkError "wrong arity" topTy
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant else mkError "product type expected" topTy
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant-- | lift a analysis function to annotated items
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantmapAnMaybe :: (Monad m) => (Annoted a -> m (Maybe b)) -> [Annoted a]
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant -> m [Annoted b]
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantmapAnMaybe f al = do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant il <- mapM f al
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant return $ map ( \ (i, a) -> replaceAnnoted (fromJust i) a) $
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant filter (isJust . fst) $ zip il al
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant-- | analyse annotated type items
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaTypeItems :: GenKind -> [Annoted TypeItem] -> State Env [Annoted TypeItem]
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaTypeItems gk l = do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant ul <- mapAnMaybe ana1TypeItem l
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant tys <- mapM ( \ (Datatype d) -> dataPatToType d) $
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant filter ( \ t -> case t of
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Datatype _ -> True
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant _ -> False) $ map item ul
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant rl <- mapAnMaybe (anaTypeItem gk tys) ul
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant addDataSen tys
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant return rl
d81f6d00c343633159fc5ea08599d145135612c0ludovicp
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant-- | add sentences for data type definitions
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantaddDataSen :: [DataPat] -> State Env ()
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantaddDataSen tys = do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant tm <- gets typeMap
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant let tis = map ( \ (DataPat _ i _ _ _) -> i) tys
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant ds = foldr ( \ i dl -> case Map.lookup i tm of
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Nothing -> dl
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Just ti -> case typeDefn ti of
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant DatatypeDefn dd -> dd : dl
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant _ -> dl) [] tis
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant sen = (makeNamed ("ga_" ++ showSepList (showString "_") showId tis "")
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant $ DatatypeSen ds) { isDef = True }
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant unless (null tys) $ appendSentences [sen]
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantana1TypeItem :: Annoted TypeItem -> State Env (Maybe TypeItem)
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantana1TypeItem t = case item t of
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Datatype d -> do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant md <- ana1Datatype $ replaceAnnoted d t
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant return $ fmap Datatype md
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant i -> return $ Just i
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaTypeDecl :: [TypePattern] -> Kind -> Range -> State Env (Maybe TypeItem)
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaTypeDecl pats kind ps = do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant cm <- gets classMap
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant let Result cs _ = anaKindM kind cm
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant Result ds (Just is) = convertTypePatterns pats
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant addDiags $ cs ++ ds
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant let ak = if null cs then kind else universe
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant mis <- mapM (addTypePattern NoTypeDefn ak) is
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant let newPats = map toTypePattern $ catMaybes mis
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant return $ if null newPats then Nothing else Just $ TypeDecl newPats ak ps
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaIsoDecl :: [TypePattern] -> Range -> State Env (Maybe TypeItem)
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantanaIsoDecl pats ps = do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant let Result ds (Just is) = convertTypePatterns pats
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant addDiags ds
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant mis <- mapM (addTypePattern NoTypeDefn universe) is
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant case catMaybes mis of
43cf232e238dd2e98c8b2badc91071b6ada52956gary.williams [] -> return Nothing
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant nis -> do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant let (i, _) : ris = reverse nis
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant mapM_ (\ (j, _) -> addAliasType False j
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant (TypeScheme [] (TypeName i rStar 0) $ posOfId j) universe) ris
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant return $ Just $ IsoDecl (map toTypePattern nis) ps
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantsetTypePatternVars :: [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovantsetTypePatternVars ol = do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant l <- mapM ( \ (i, tArgs) -> do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant e <- get
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant newAs <- mapM anaddTypeVarDecl tArgs
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant put e
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant return (i, catMaybes newAs)) ol
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant let g = group $ map snd l
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant case g of
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant [_ : _] -> do
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant newAs <- mapM anaddTypeVarDecl $ snd $ head l
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant return $ map ( \ (i, _) -> (i, catMaybes newAs)) l
bc36152ff9a3ea2c2fa75ba2a64becfae0d96e5ecsovant _ -> do
addDiags [mkDiag Error
"variables must be identical for all types within one item" l]
return []
anaSubtypeDecl :: [TypePattern] -> Type -> Range -> State Env (Maybe TypeItem)
anaSubtypeDecl pats t ps = do
let Result ds (Just is) = convertTypePatterns pats
addDiags ds
tvs <- gets localTypeVars
nis <- setTypePatternVars is
let newPats = map toTypePattern nis
te <- get
putLocalTypeVars tvs
let Result es mp = anaTypeM (Nothing, t) te
case mp of
Nothing -> do
mapM_ (addTypePattern NoTypeDefn universe) is
if null newPats then return Nothing else case t of
TypeToken tt -> do
let tid = simpleIdToId tt
newT = TypeName tid rStar 0
addTypeId False NoTypeDefn universe tid
mapM_ (addSuperType newT universe) nis
return $ Just $ SubtypeDecl newPats newT ps
_ -> do
addDiags es
return $ Just $ TypeDecl newPats universe ps
Just ((rk, ks), newT) -> nonUniqueKind ks rk t $ \ kind -> do
mapM_ (addTypePattern NoTypeDefn kind) is
mapM_ (addSuperType newT $ rawToKind rk) nis
return $ if null nis then Nothing else
Just $ SubtypeDecl newPats newT ps
anaSubtypeDefn :: Annoted TypeItem -> TypePattern -> Vars -> Type
-> (Annoted Term) -> Range -> State Env (Maybe TypeItem)
anaSubtypeDefn aitm pat v t f ps = do
let Result ds m = convertTypePattern pat
addDiags ds
case m of
Nothing -> return Nothing
Just (i, tArgs) -> do
tvs <- gets localTypeVars
newAs <- mapM anaddTypeVarDecl tArgs
mt <- anaStarType t
putLocalTypeVars tvs
case mt of
Nothing -> return Nothing
Just ty -> do
let nAs = catMaybes newAs
fullKind = typeArgsListToKind nAs universe
jTy = TypeName i (typeArgsListToRawKind nAs rStar) 0
aTy = mkTypeAppl jTy $ map typeArgToType nAs
e <- get
let Result es mvds = anaVars e v $ monoType ty
addDiags es
if cyclicType i ty then do
addDiags [mkDiag Error
"illegal recursive subtype definition" ty]
return Nothing
else case mvds of
Nothing -> return Nothing
Just vtt -> do
let vds = extractVars vtt
checkUniqueVars vds
vs <- gets localVars
mapM_ (addLocalVar True) vds
mf <- anaFormula f
putLocalVars vs
case mf of
Nothing -> return Nothing
Just (newF, resF) -> do
addTypeId True NoTypeDefn fullKind i
addSuperType ty universe (i, nAs)
let lab1 = getRLabel resF
lab = if null lab1 then getRLabel aitm else lab1
appendSentences [makeNamed lab
$ Formula $ mkEnvForall e (
mkForall (map GenVarDecl vds)
$ mkLogTerm eqvId ps
(TypedTerm vtt InType aTy ps) $ item resF) ps]
return $ Just $ SubtypeDefn (TypePattern i nAs nullRange)
v ty newF ps
anaAliasType :: TypePattern -> Maybe Kind -> TypeScheme
-> Range -> State Env (Maybe TypeItem)
anaAliasType pat mk sc ps = do
let Result ds m = convertTypePattern pat
addDiags ds
case m of
Nothing -> return Nothing
Just (i, tArgs) -> do
tvs <- gets localTypeVars -- save variables
newAs <- mapM anaddTypeVarDecl tArgs
(ik, mt) <- anaPseudoType mk sc
putLocalTypeVars tvs
case mt of
Nothing -> return Nothing
Just (TypeScheme args ty qs) ->
if cyclicType i ty then do
addDiags [mkDiag Error "illegal recursive type synonym" ty]
return Nothing
else do
let nAs = catMaybes newAs
allArgs = nAs ++ args
fullKind = typeArgsListToKind nAs ik
allSc = TypeScheme allArgs ty qs
b <- addAliasType True i allSc fullKind
tm <- gets typeMap
putTypeMap $ Map.map ( \ ti -> case typeDefn ti of
AliasTypeDefn y -> ti
{ typeDefn = AliasTypeDefn $ expandAux tm y }
_ -> ti) tm
return $ if b then Just $ AliasType
(TypePattern i [] nullRange) (Just fullKind) allSc ps
else Nothing
-- | analyse a 'TypeItem'
anaTypeItem :: GenKind -> [DataPat] -> Annoted TypeItem
-> State Env (Maybe TypeItem)
anaTypeItem gk tys aitm = case item aitm of
TypeDecl pats kind ps -> anaTypeDecl pats kind ps
SubtypeDecl pats t ps -> anaSubtypeDecl pats t ps
IsoDecl pats ps -> anaIsoDecl pats ps
SubtypeDefn pat v t f ps -> anaSubtypeDefn aitm pat v t f ps
AliasType pat mk sc ps -> anaAliasType pat mk sc ps
Datatype d -> do
mD <- anaDatatype gk tys $ replaceAnnoted d aitm
case mD of
Nothing -> return Nothing
Just newD -> return $ Just $ Datatype newD
-- | pre-analyse a data type for 'anaDatatype'
ana1Datatype :: Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
ana1Datatype aitm = do
let DatatypeDecl pat kind alts derivs ps = item aitm
cm <- gets classMap
let Result cs (Just rk) = anaKindM kind cm
k = if null cs then kind else universe
addDiags $ checkKinds pat rStar rk ++ cs
let rms = map ( \ c -> anaKindM (ClassKind c) cm) derivs
mcs = map maybeResult rms
jcs = catMaybes mcs
newDerivs = map fst $ filter (isJust . snd) $ zip derivs mcs
Result ds m = convertTypePattern pat
addDiags (ds ++ concatMap diags rms)
addDiags $ concatMap (checkKinds pat rStar) jcs
case m of
Nothing -> return Nothing
Just (i, tArgs) -> do
tvs <- gets localTypeVars
newAs <- mapM anaddTypeVarDecl tArgs
putLocalTypeVars tvs
let nAs = catMaybes newAs
fullKind = typeArgsListToKind nAs k
addDiags $ checkUniqueTypevars nAs
b <- addTypeId False PreDatatype fullKind i
return $ if b then Just $ DatatypeDecl
(TypePattern i nAs nullRange) k alts newDerivs ps
else Nothing
-- | convert a data type with an analysed type pattern to a data pattern
dataPatToType :: DatatypeDecl -> State Env DataPat
dataPatToType d = case d of
DatatypeDecl (TypePattern i nAs _) k _ _ _ -> do
rk <- anaKind k
return $ DataPat Map.empty i nAs rk $ patToType i nAs rk
_ -> error "dataPatToType"
addDataSubtype :: DataPat -> Kind -> Type -> State Env ()
addDataSubtype (DataPat _ _ nAs _ rt) k st = case st of
TypeName i _ _ -> addSuperType rt k (i, nAs)
_ -> addDiags [mkDiag Warning "data subtype ignored" st]
-- | analyse a pre-analysed data type given all data patterns of the type item
anaDatatype :: GenKind -> [DataPat]
-> Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
anaDatatype genKind tys d = case item d of
itd@(DatatypeDecl (TypePattern i nAs _) k alts _ _) -> do
-- recompute data pattern rather than looking it up in tys
dt@(DataPat _ _ _ rk _) <- dataPatToType itd
let fullKind = typeArgsListToKind nAs k
tvs <- gets localTypeVars
mapM_ (addTypeVarDecl False . nonVarTypeArg) nAs
mNewAlts <- fromResult $ anaAlts genKind tys dt (map item alts)
putLocalTypeVars tvs
case mNewAlts of
Nothing -> return Nothing
Just newAlts -> do
mapM_ (addDataSubtype dt fullKind) $ foldr
( \ (Construct mc ts _ _) l -> case mc of
Nothing -> ts ++ l
Just _ -> l) [] newAlts
let gArgs = genTypeArgs nAs
iMap = Map.fromList $ map (\ (DataPat _ j _ _ _) -> (j, j)) tys
de = DataEntry iMap i genKind gArgs rk
$ Set.fromList newAlts
dp = toDataPat de
mapM_ ( \ (Construct mc tc p sels) -> case mc of
Nothing -> return ()
Just c -> do
let sc = getConstrScheme dp p tc
addOpId c sc Set.empty (ConstructData i)
mapM_ ( \ (Select ms ts pa) -> case ms of
Just s ->
addOpId s (getSelScheme dp pa ts) Set.empty $ SelectData
(Set.singleton $ ConstrInfo c sc) i
Nothing -> return False) $ concat sels) newAlts
addTypeId True (DatatypeDefn de) fullKind i
appendSentences $ makeDataSelEqs dp newAlts
return $ Just itd
_ -> error "anaDatatype (not preprocessed)"
-- | analyse a pseudo type (represented as a 'TypeScheme')
anaPseudoType :: Maybe Kind -> TypeScheme -> State Env (Kind, Maybe TypeScheme)
anaPseudoType mk (TypeScheme tArgs ty p) = do
cm <- gets classMap
let k = case mk of
Nothing -> Nothing
Just j -> let Result cs _ = anaKindM j cm
in Just $ if null cs then j else universe
nAs <- mapM anaddTypeVarDecl tArgs
let ntArgs = catMaybes nAs
mp <- anaType (Nothing, ty)
case mp of
Nothing -> return (universe, Nothing)
Just ((_, sks), newTy) -> case Set.toList sks of
[sk] -> do
let newK = typeArgsListToKind ntArgs sk
irk <- anaKind newK
case k of
Nothing -> return ()
Just j -> do
grk <- anaKind j
addDiags $ checkKinds ty grk irk
return (newK, Just $ TypeScheme ntArgs newTy p)
_ -> return (universe, Nothing)
-- | add a type pattern
addTypePattern :: TypeDefn -> Kind -> (Id, [TypeArg])
-> State Env (Maybe (Id, [TypeArg]))
addTypePattern defn kind (i, tArgs) = do
tvs <- gets localTypeVars
newAs <- mapM anaddTypeVarDecl tArgs
putLocalTypeVars tvs
let nAs = catMaybes newAs
fullKind = typeArgsListToKind nAs kind
addDiags $ checkUniqueTypevars nAs
b <- addTypeId True defn fullKind i
return $ if b then Just (i, nAs) else Nothing