b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt{- |

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntModule : $Header$

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntCopyright : (c) Christian Maeder and Uni Bremen 2002-2005

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntMaintainer : Christian.Maeder@dfki.de

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntStability : provisional

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntPortability : portable

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntanalyse type declarations

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-}

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntmodule HasCASL.TypeDecl

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ( anaFormula

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt , mapAnMaybe

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt , anaTypeItems

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt , dataPatToType

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt , ana1Datatype

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt , anaDatatype

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt , addDataSen

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ) where

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Data.Maybe

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Data.List(group)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.Id

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.AS_Annotation

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.Lib.State

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport qualified Data.Map as Map

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.Result

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport Common.GlobalAnnotations

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.As

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.AsUtils

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.Le

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.ClassAna

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.TypeAna

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.ConvertTypePattern

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.DataAna

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.Unify

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.VarDecl

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.SubtypeDecl

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.MixAna

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntimport HasCASL.TypeCheck

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | resolve and type check a formula

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaFormula :: GlobalAnnos -> Annoted Term

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt -> State Env (Maybe (Annoted Term, Annoted Term))

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaFormula ga at = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt rt <- resolve ga $ item at

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case rt of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just t -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mt <- typeCheck (Just unitType) t

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ case mt of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just e -> Just (at { item = t }, at { item = e })

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaVars :: TypeEnv -> Vars -> Type -> Result [VarDecl]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaVars te vv t = case vv of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Var v -> return [VarDecl v t Other nullRange]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt VarTuple vs _ -> let

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt (topTy, ts) = getTypeAppl t

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt n = length ts in

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt if n > 1 && lesserType te topTy (toType $ productId n) then

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt if n == length vs then

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let lrs = zipWith (anaVars te) vs ts

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt lms = map maybeResult lrs in

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt if all isJust lms then

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ concatMap fromJust lms

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else Result (concatMap diags lrs) Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else mkError "wrong arity" topTy

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else mkError "product type expected" topTy

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | lift a analysis function to annotated items

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntmapAnMaybe :: (Monad m) => (a -> m (Maybe b)) -> [Annoted a] -> m [Annoted b]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntmapAnMaybe f al = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt il <- mapAnM f al

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ map ( \ a -> replaceAnnoted (fromJust $ item a) a) $

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt filter (isJust . item) il

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | analyse annotated type items

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaTypeItems :: GlobalAnnos -> GenKind -> [Annoted TypeItem]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt -> State Env [Annoted TypeItem]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaTypeItems ga gk l = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ul <- mapAnMaybe ana1TypeItem l

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt tys <- mapM ( \ (Datatype d) -> dataPatToType d) $

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt filter ( \ t -> case t of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Datatype _ -> True

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> False) $ map item ul

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt rl <- mapAnMaybe (anaTypeItem ga gk tys) ul

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDataSen tys

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return rl

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | add sentences for data type definitions

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntaddDataSen :: [DataPat] -> State Env ()

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntaddDataSen tys = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt tm <- gets typeMap

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let tis = map ( \ (DataPat i _ _ _) -> i) tys

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt ds = foldr ( \ i dl -> case Map.lookup i tm of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> dl

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just ti -> case typeDefn ti of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt DatatypeDefn dd -> dd : dl

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> dl) [] tis

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt sen = (makeNamed ("ga_" ++ showSepList (showString "_") showId tis "")

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt $ DatatypeSen ds) { isDef = True }

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt if null tys then return () else appendSentences [sen]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntana1TypeItem :: TypeItem -> State Env (Maybe TypeItem)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntana1TypeItem t = case t of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Datatype d -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt md <- ana1Datatype d

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ fmap Datatype md

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> return $ Just t

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaTypeDecl :: [TypePattern] -> Kind -> Range -> State Env (Maybe TypeItem)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaTypeDecl pats kind ps = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt cm <- gets classMap

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let Result cs _ = anaKindM kind cm

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Result ds (Just is) = convertTypePatterns pats

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags $ cs ++ ds

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let ak = if null cs then kind else universe

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mis <- mapM (addTypePattern NoTypeDefn ak) is

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let newPats = map toTypePattern $ catMaybes mis

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ if null newPats then Nothing else Just $ TypeDecl newPats ak ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaIsoDecl :: [TypePattern] -> Range -> State Env (Maybe TypeItem)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaIsoDecl pats ps = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let Result ds (Just is) = convertTypePatterns pats

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags ds

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mis <- mapM (addTypePattern NoTypeDefn universe) is

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let nis = catMaybes mis

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mapM_ ( \ i -> mapM_ (addSuperType (TypeName i rStar 0)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt universe) nis) $ map fst nis

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ if null nis then Nothing else

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just $ IsoDecl (map toTypePattern nis) ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntsetTypePatternVars :: [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntsetTypePatternVars ol = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt l <- mapM ( \ (i, tArgs) -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt e <- get

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt newAs <- mapM anaddTypeVarDecl tArgs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt put e

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return (i, catMaybes newAs)) ol

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let g = group $ map snd l

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case g of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt [_ : _] -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt newAs <- mapM anaddTypeVarDecl $ snd $ head l

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ map ( \ (i, _) -> (i, catMaybes newAs)) l

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags [mkDiag Error

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt "variables must be identical for all types within one item" l]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return []

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaSubtypeDecl :: [TypePattern] -> Type -> Range

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt -> State Env (Maybe TypeItem)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaSubtypeDecl pats t ps = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let Result ds (Just is) = convertTypePatterns pats

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags ds

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt tvs <- gets localTypeVars

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt nis <- setTypePatternVars is

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let newPats = map toTypePattern nis

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt te <- get

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt putLocalTypeVars tvs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let Result es mp = anaTypeM (Nothing, t) te

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case mp of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mapM_ (addTypePattern NoTypeDefn universe) is

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt if null newPats then return Nothing else case t of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypeToken tt -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let tid = simpleIdToId tt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt newT = TypeName tid rStar 0

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addTypeId False NoTypeDefn rStar universe tid

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mapM_ (addSuperType newT universe) nis

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ Just $ SubtypeDecl newPats newT ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags es

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ Just $ TypeDecl newPats universe ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just ((rk, ks), newT) -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt nonUniqueKind ks t $ \ kind -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mapM_ (addTypePattern NoTypeDefn kind) is

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mapM_ (addSuperType newT $ rawToKind rk) nis

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ if null nis then Nothing else

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just $ SubtypeDecl newPats newT ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaSubtypeDefn :: GlobalAnnos -> TypePattern -> Vars -> Type

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt -> (Annoted Term) -> Range -> State Env (Maybe TypeItem)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaSubtypeDefn ga pat v t f ps = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let Result ds m = convertTypePattern pat

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags ds

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case m of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just (i, tArgs) -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt tvs <- gets localTypeVars

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt newAs <- mapM anaddTypeVarDecl tArgs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mt <- anaStarType t

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt putLocalTypeVars tvs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case mt of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just ty -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let nAs = catMaybes newAs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt fullKind = typeArgsListToKind nAs universe

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt rk <- anaKind fullKind

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt e <- get

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let Result es mvds = anaVars e v $ monoType ty

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags es

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt if cyclicType i ty then do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags [mkDiag Error

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt "illegal recursive subtype definition" ty]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else case mvds of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just vds -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt checkUniqueVars vds

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt vs <- gets localVars

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mapM_ (addLocalVar True) vds

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mf <- anaFormula ga f

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt putLocalVars vs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case mf of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just (newF, _) -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addTypeId True NoTypeDefn rk fullKind i

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addSuperType ty universe (i, nAs)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ Just $ SubtypeDefn (TypePattern i nAs nullRange)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt v ty newF ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaAliasType :: TypePattern -> Maybe Kind -> TypeScheme

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt -> Range -> State Env (Maybe TypeItem)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaAliasType pat mk sc ps = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let Result ds m = convertTypePattern pat

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags ds

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case m of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just (i, tArgs) -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt tvs <- gets localTypeVars -- save variables

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt newAs <- mapM anaddTypeVarDecl tArgs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt (ik, mt) <- anaPseudoType mk sc

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt putLocalTypeVars tvs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case mt of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just (TypeScheme args ty qs) ->

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt if cyclicType i ty then do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags [mkDiag Error "illegal recursive type synonym" ty]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let nAs = catMaybes newAs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt allArgs = nAs ++ args

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt fullKind = typeArgsListToKind nAs ik

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt allSc = TypeScheme allArgs ty qs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt b <- addAliasType True i allSc fullKind

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ if b then Just $ AliasType

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt (TypePattern i [] nullRange) (Just fullKind) allSc ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | analyse a 'TypeItem'

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaTypeItem :: GlobalAnnos -> GenKind -> [DataPat] -> TypeItem

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt -> State Env (Maybe TypeItem)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaTypeItem ga gk tys itm = case itm of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypeDecl pats kind ps -> anaTypeDecl pats kind ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt SubtypeDecl pats t ps -> anaSubtypeDecl pats t ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt IsoDecl pats ps -> anaIsoDecl pats ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt SubtypeDefn pat v t f ps -> anaSubtypeDefn ga pat v t f ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt AliasType pat mk sc ps -> anaAliasType pat mk sc ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Datatype d -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mD <- anaDatatype gk tys d

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case mD of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just newD -> return $ Just $ Datatype newD

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | pre-analyse a data type for 'anaDatatype'

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntana1Datatype :: DatatypeDecl -> State Env (Maybe DatatypeDecl)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Huntana1Datatype (DatatypeDecl pat kind alts derivs ps) = do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt cm <- gets classMap

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let Result cs (Just rk) = anaKindM kind cm

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt k = if null cs then kind else universe

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags $ checkKinds pat rStar rk ++ cs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let rms = map ( \ c -> anaKindM (ClassKind c) cm) derivs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt mcs = map maybeResult rms

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt jcs = catMaybes mcs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt newDerivs = map fst $ filter (isJust . snd) $ zip derivs mcs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Result ds m = convertTypePattern pat

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags (ds ++ concatMap diags rms)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags $ concatMap (checkKinds pat rStar) jcs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt case m of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Nothing -> return Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt Just (i, tArgs) -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt tvs <- gets localTypeVars

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt newAs <- mapM anaddTypeVarDecl tArgs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt putLocalTypeVars tvs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let nAs = catMaybes newAs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt fullKind = typeArgsListToKind nAs k

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt addDiags $ checkUniqueTypevars nAs

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt frk <- anaKind fullKind

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt b <- addTypeId False PreDatatype frk fullKind i

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ if b then Just $ DatatypeDecl

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt (TypePattern i nAs nullRange) k alts newDerivs ps

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt else Nothing

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | convert a data type with an analysed type pattern to a data pattern

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntdataPatToType :: DatatypeDecl -> State Env DataPat

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntdataPatToType d = case d of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt DatatypeDecl (TypePattern i nAs _) k _ _ _ -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt rk <- anaKind k

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt return $ DataPat i nAs rk $ patToType i nAs rk

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> error "dataPatToType"

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntaddDataSubtype :: DataPat -> Kind -> Type -> State Env ()

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntaddDataSubtype (DataPat _ nAs _ rt) k st = case st of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt TypeName i _ _ -> addSuperType rt k (i, nAs)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt _ -> addDiags [mkDiag Warning "data subtype ignored" st]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt-- | analyse a pre-analysed data type given all data patterns of the type item

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaDatatype :: GenKind -> [DataPat]

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt -> DatatypeDecl -> State Env (Maybe DatatypeDecl)

b66b333f59cf51ef87f973084a5023acd9317fb2Evan HuntanaDatatype genKind tys d = case d of

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt DatatypeDecl (TypePattern i nAs _) k alts _ _ -> do

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt dt@(DataPat _ _ rk rt) <- dataPatToType d

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt let fullKind = typeArgsListToKind nAs k

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt frk <- anaKind fullKind

b66b333f59cf51ef87f973084a5023acd9317fb2Evan Hunt tvs <- gets localTypeVars

mapM_ (addTypeVarDecl False) nAs

mNewAlts <- fromResult $ anaAlts 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 srt = generalize nAs rt

mapM_ ( \ (Construct mc tc p sels) -> case mc of

Nothing -> return ()

Just c -> do

let sc = TypeScheme nAs (getFunType srt p tc) nullRange

addOpId c sc [] (ConstructData i)

mapM_ ( \ (Select ms ts pa) -> case ms of

Just s -> do

let selSc = TypeScheme nAs (getSelType srt pa ts)

nullRange

addOpId s selSc [] $ SelectData [ConstrInfo c sc] i

Nothing -> return False) $ concat sels) newAlts

let de = DataEntry Map.empty i genKind (genTypeArgs nAs) rk newAlts

addTypeId True (DatatypeDefn de) frk fullKind i

appendSentences $ makeDataSelEqs de srt

return $ Just d

_ -> 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 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

frk <- anaKind fullKind

b <- addTypeId True defn frk fullKind i

return $ if b then Just (i, nAs) else Nothing