TypeDecl.hs revision f26a1fc3851297e6483cf3fb56e9c0967b8f8b13
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : analyse type declarations
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskianalyse type declarations
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , anaTypeItems
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , dataPatToType
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , ana1Datatype
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , anaDatatype
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport qualified Data.Map as Map
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport qualified Data.Set as Set
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | resolve and type check a formula
8e80792f474d154ff11762fac081a422e34f1accChristian MaederanaFormula :: GlobalAnnos -> Annoted Term
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> State Env (Maybe (Annoted Term, Annoted Term))
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaFormula ga at = do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder rt <- resolve ga $ item at
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> return Nothing
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder mt <- typeCheck (Just unitType) t
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder return $ case mt of
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Nothing -> Nothing
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Just e -> Just (at { item = t }, at { item = e })
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederanaVars :: Env -> Vars -> Type -> Result [VarDecl]
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederanaVars te vv t = case vv of
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder Var v -> return [VarDecl v t Other nullRange]
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder VarTuple vs _ -> let
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder (topTy, ts) = getTypeAppl t
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder n = length ts in
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder if n > 1 && lesserType te topTy (toProdType n) then
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder if n == length vs then
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder let lrs = zipWith (anaVars te) vs ts
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder lms = map maybeResult lrs in
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder if all isJust lms then
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder return $ concatMap fromJust lms
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder else Result (concatMap diags lrs) Nothing
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder else mkError "wrong arity" topTy
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder else mkError "product type expected" topTy
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder-- | lift a analysis function to annotated items
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaedermapAnMaybe :: (Monad m) => (a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaedermapAnMaybe f al = do
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder il <- mapAnM f al
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder return $ map ( \ a -> replaceAnnoted (fromJust $ item a) a) $
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder filter (isJust . item) il
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder-- | analyse annotated type items
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederanaTypeItems :: GlobalAnnos -> GenKind -> [Annoted TypeItem]
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder -> State Env [Annoted TypeItem]
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederanaTypeItems ga gk l = do
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ul <- mapAnMaybe ana1TypeItem l
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder tys <- mapM ( \ (Datatype d) -> dataPatToType d) $
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder filter ( \ t -> case t of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Datatype _ -> True
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder _ -> False) $ map item ul
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder rl <- mapAnMaybe (anaTypeItem ga gk tys) ul
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder addDataSen tys
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | add sentences for data type definitions
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederaddDataSen :: [DataPat] -> State Env ()
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederaddDataSen tys = do
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski tm <- gets typeMap
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let tis = map ( \ (DataPat i _ _ _) -> i) tys
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ds = foldr ( \ i dl -> case Map.lookup i tm of
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder Nothing -> dl
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just ti -> case typeDefn ti of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder DatatypeDefn dd -> dd : dl
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder _ -> dl) [] tis
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder sen = (makeNamed ("ga_" ++ showSepList (showString "_") showId tis "")
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder $ DatatypeSen ds) { isDef = True }
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder if null tys then return () else appendSentences [sen]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiana1TypeItem :: TypeItem -> State Env (Maybe TypeItem)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederana1TypeItem t = case t of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Datatype d -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski md <- ana1Datatype d
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ fmap Datatype md
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder _ -> return $ Just t
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederanaTypeDecl :: [TypePattern] -> Kind -> Range -> State Env (Maybe TypeItem)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederanaTypeDecl pats kind ps = do
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder cm <- gets classMap
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let Result cs _ = anaKindM kind cm
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Result ds (Just is) = convertTypePatterns pats
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder addDiags $ cs ++ ds
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder let ak = if null cs then kind else universe
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mis <- mapM (addTypePattern NoTypeDefn ak) is
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let newPats = map toTypePattern $ catMaybes mis
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ if null newPats then Nothing else Just $ TypeDecl newPats ak ps
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaIsoDecl :: [TypePattern] -> Range -> State Env (Maybe TypeItem)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaIsoDecl pats ps = do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let Result ds (Just is) = convertTypePatterns pats
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mis <- mapM (addTypePattern NoTypeDefn universe) is
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder let nis = catMaybes mis
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder mapM_ ( \ i -> mapM_ (addSuperType (TypeName i rStar 0)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder universe) nis) $ map fst nis
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder return $ if null nis then Nothing else
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just $ IsoDecl (map toTypePattern nis) ps
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedersetTypePatternVars :: [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersetTypePatternVars ol = do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder l <- mapM ( \ (i, tArgs) -> do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder newAs <- mapM anaddTypeVarDecl tArgs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return (i, catMaybes newAs)) ol
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let g = group $ map snd l
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski [_ : _] -> do
74d9a385499bf903b24848dff450a153f525bda7Christian Maeder newAs <- mapM anaddTypeVarDecl $ snd $ head l
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ map ( \ (i, _) -> (i, catMaybes newAs)) l
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder addDiags [mkDiag Error
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder "variables must be identical for all types within one item" l]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaSubtypeDecl :: [TypePattern] -> Type -> Range
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> State Env (Maybe TypeItem)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaSubtypeDecl pats t ps = do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let Result ds (Just is) = convertTypePatterns pats
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder tvs <- gets localTypeVars
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder nis <- setTypePatternVars is
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let newPats = map toTypePattern nis
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder putLocalTypeVars tvs
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let Result es mp = anaTypeM (Nothing, t) te
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mapM_ (addTypePattern NoTypeDefn universe) is
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder if null newPats then return Nothing else case t of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder TypeToken tt -> do
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let tid = simpleIdToId tt
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder newT = TypeName tid rStar 0
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder addTypeId False NoTypeDefn rStar universe tid
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder mapM_ (addSuperType newT universe) nis
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder return $ Just $ SubtypeDecl newPats newT ps
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder return $ Just $ TypeDecl newPats universe ps
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder Just ((rk, ks), newT) -> do
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder nonUniqueKind ks t $ \ kind -> do
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder mapM_ (addTypePattern NoTypeDefn kind) is
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder mapM_ (addSuperType newT $ rawToKind rk) nis
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder return $ if null nis then Nothing else
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder Just $ SubtypeDecl newPats newT ps
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederanaSubtypeDefn :: GlobalAnnos -> TypePattern -> Vars -> Type
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder -> (Annoted Term) -> Range -> State Env (Maybe TypeItem)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederanaSubtypeDefn ga pat v t f ps = do
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder let Result ds m = convertTypePattern pat
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Nothing -> return Nothing
ab642ff136ce716af9e609b667e3f06d766c4ad7Christian Maeder Just (i, tArgs) -> do
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder tvs <- gets localTypeVars
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder newAs <- mapM anaddTypeVarDecl tArgs
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder mt <- anaStarType t
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder putLocalTypeVars tvs
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Nothing -> return Nothing
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Just ty -> do
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder let nAs = catMaybes newAs
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder fullKind = typeArgsListToKind nAs universe
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder rk <- anaKind fullKind
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let Result es mvds = anaVars e v $ monoType ty
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder if cyclicType i ty then do
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder addDiags [mkDiag Error
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder "illegal recursive subtype definition" ty]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return Nothing
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder else case mvds of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Nothing -> return Nothing
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Just vds -> do
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder checkUniqueVars vds
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder vs <- gets localVars
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder mapM_ (addLocalVar True) vds
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder mf <- anaFormula ga f
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder putLocalVars vs
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder Nothing -> return Nothing
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Just (newF, _) -> do
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder addTypeId True NoTypeDefn rk fullKind i
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder addSuperType ty universe (i, nAs)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ Just $ SubtypeDefn (TypePattern i nAs nullRange)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederanaAliasType :: TypePattern -> Maybe Kind -> TypeScheme
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -> Range -> State Env (Maybe TypeItem)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaederanaAliasType pat mk sc ps = do
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder let Result ds m = convertTypePattern pat
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> return Nothing
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder Just (i, tArgs) -> do
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder tvs <- gets localTypeVars -- save variables
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder newAs <- mapM anaddTypeVarDecl tArgs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (ik, mt) <- anaPseudoType mk sc
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski putLocalTypeVars tvs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> return Nothing
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder Just (TypeScheme args ty qs) ->
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder if cyclicType i ty then do
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder addDiags [mkDiag Error "illegal recursive type synonym" ty]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return Nothing
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let nAs = catMaybes newAs
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder allArgs = nAs ++ args
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder fullKind = typeArgsListToKind nAs ik
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder allSc = TypeScheme allArgs ty qs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder b <- addAliasType True i allSc fullKind
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ if b then Just $ AliasType
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (TypePattern i [] nullRange) (Just fullKind) allSc ps
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder-- | analyse a 'TypeItem'
99476ac2689c74251219db4782e57fe713a24a52Christian MaederanaTypeItem :: GlobalAnnos -> GenKind -> [DataPat] -> TypeItem
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -> State Env (Maybe TypeItem)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederanaTypeItem ga gk tys itm = case itm of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder TypeDecl pats kind ps -> anaTypeDecl pats kind ps
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder SubtypeDecl pats t ps -> anaSubtypeDecl pats t ps
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder IsoDecl pats ps -> anaIsoDecl pats ps
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder SubtypeDefn pat v t f ps -> anaSubtypeDefn ga pat v t f ps
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder AliasType pat mk sc ps -> anaAliasType pat mk sc ps
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Datatype d -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder mD <- anaDatatype gk tys d
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder Nothing -> return Nothing
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just newD -> return $ Just $ Datatype newD
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder-- | pre-analyse a data type for 'anaDatatype'
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederana1Datatype :: DatatypeDecl -> State Env (Maybe DatatypeDecl)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederana1Datatype (DatatypeDecl pat kind alts derivs ps) = do
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder cm <- gets classMap
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let Result cs (Just rk) = anaKindM kind cm
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder k = if null cs then kind else universe
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder addDiags $ checkKinds pat rStar rk ++ cs
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let rms = map ( \ c -> anaKindM (ClassKind c) cm) derivs
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder mcs = map maybeResult rms
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder jcs = catMaybes mcs
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder newDerivs = map fst $ filter (isJust . snd) $ zip derivs mcs
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Result ds m = convertTypePattern pat
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder addDiags (ds ++ concatMap diags rms)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder addDiags $ concatMap (checkKinds pat rStar) jcs
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Nothing -> return Nothing
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder Just (i, tArgs) -> do
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder tvs <- gets localTypeVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder newAs <- mapM anaddTypeVarDecl tArgs
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder putLocalTypeVars tvs
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let nAs = catMaybes newAs
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder fullKind = typeArgsListToKind nAs k
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder addDiags $ checkUniqueTypevars nAs
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder frk <- anaKind fullKind
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder b <- addTypeId False PreDatatype frk fullKind i
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return $ if b then Just $ DatatypeDecl
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (TypePattern i nAs nullRange) k alts newDerivs ps
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | convert a data type with an analysed type pattern to a data pattern
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederdataPatToType :: DatatypeDecl -> State Env DataPat
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederdataPatToType d = case d of
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder DatatypeDecl (TypePattern i nAs _) k _ _ _ -> do
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder rk <- anaKind k
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder return $ DataPat i nAs rk $ patToType i nAs rk
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder _ -> error "dataPatToType"
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederaddDataSubtype :: DataPat -> Kind -> Type -> State Env ()
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederaddDataSubtype (DataPat _ nAs _ rt) k st = case st of
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder TypeName i _ _ -> addSuperType rt k (i, nAs)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder _ -> addDiags [mkDiag Warning "data subtype ignored" st]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- | analyse a pre-analysed data type given all data patterns of the type item
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederanaDatatype :: GenKind -> [DataPat]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> DatatypeDecl -> State Env (Maybe DatatypeDecl)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederanaDatatype genKind tys d = case d of
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder DatatypeDecl (TypePattern i nAs _) k alts _ _ -> do
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder dt@(DataPat _ _ rk rt) <- dataPatToType d
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let fullKind = typeArgsListToKind nAs k
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder frk <- anaKind fullKind
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder tvs <- gets localTypeVars
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder mapM_ (addTypeVarDecl False) nAs
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder mNewAlts <- fromResult $ anaAlts tys dt (map item alts)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder putLocalTypeVars tvs
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder case mNewAlts of
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Nothing -> return Nothing
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Just newAlts -> do
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder mapM_ (addDataSubtype dt fullKind) $ foldr
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ( \ (Construct mc ts _ _) l -> case mc of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Nothing -> ts ++ l
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder Just _ -> l) [] newAlts
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder let srt = generalize nAs rt
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder gArgs = genTypeArgs nAs
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder mapM_ ( \ (Construct mc tc p sels) -> case mc of
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder Nothing -> return ()
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder let sc = TypeScheme gArgs (getFunType srt p tc) nullRange
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder addOpId c sc [] (ConstructData i)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder mapM_ ( \ (Select ms ts pa) -> case ms of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let selSc = TypeScheme gArgs (getSelType srt pa ts)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder addOpId s selSc [] $ SelectData [ConstrInfo c sc] i
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder Nothing -> return False) $ concat sels) newAlts
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder let de = DataEntry Map.empty i genKind (genTypeArgs nAs) rk newAlts
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder addTypeId True (DatatypeDefn de) frk fullKind i
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder appendSentences $ makeDataSelEqs de srt
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder return $ Just d
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder _ -> error "anaDatatype (not preprocessed)"
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- | analyse a pseudo type (represented as a 'TypeScheme')
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederanaPseudoType :: Maybe Kind -> TypeScheme -> State Env (Kind, Maybe TypeScheme)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederanaPseudoType mk (TypeScheme tArgs ty p) = do
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder cm <- gets classMap
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let k = case mk of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Nothing -> Nothing
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder Just j -> let Result cs _ = anaKindM j cm
44d2a211a352759ee988ed8353026f5fa9511209Christian Maeder in Just $ if null cs then j else universe
44d2a211a352759ee988ed8353026f5fa9511209Christian Maeder nAs <- mapM anaddTypeVarDecl tArgs
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder let ntArgs = catMaybes nAs
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder mp <- anaType (Nothing, ty)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Nothing -> return (universe, Nothing)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Just ((_, sks), newTy) -> case Set.toList sks of
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let newK = typeArgsListToKind ntArgs sk
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder irk <- anaKind newK
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder Nothing -> return ()
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder grk <- anaKind j
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder addDiags $ checkKinds ty grk irk
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return (newK, Just $ TypeScheme ntArgs newTy p)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder _ -> return (universe, Nothing)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder-- | add a type pattern
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederaddTypePattern :: TypeDefn -> Kind -> (Id, [TypeArg])
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder -> State Env (Maybe (Id, [TypeArg]))
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaederaddTypePattern defn kind (i, tArgs) = do
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder tvs <- gets localTypeVars
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder newAs <- mapM anaddTypeVarDecl tArgs
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder putLocalTypeVars tvs
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder let nAs = catMaybes newAs
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder fullKind = typeArgsListToKind nAs kind
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder addDiags $ checkUniqueTypevars nAs
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski frk <- anaKind fullKind
74d9a385499bf903b24848dff450a153f525bda7Christian Maeder b <- addTypeId True defn frk fullKind i
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski return $ if b then Just (i, nAs) else Nothing