DataAna.hs revision 5964438458028e61fdabfa74ca3b4210206cdba6
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiModule : $Header$
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiDescription : analysis of data type declarations
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiMaintainer : Christian.Maeder@dfki.de
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiStability : provisional
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiPortability : portable
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskianalyse alternatives of data types
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ( DataPat(..)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , makeDataSelEqs
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , inVarTypeArg
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiimport qualified Data.Map as Map
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiimport qualified Data.Set as Set
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | description of polymorphic data types
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata DataPat = DataPat Id [TypeArg] RawKind Type
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- make type argument invariant
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiinVarTypeArg :: TypeArg -> TypeArg
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiinVarTypeArg (TypeArg i _ vk rk c o p) = (TypeArg i InVar vk rk c o p)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimkSelId :: Range -> String -> Int -> Int -> Id
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimkSelId p str n m = mkId
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski [Token (str ++ "_" ++ show n ++ "_" ++ show m) p]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimkSelVar :: Int -> Int -> Type -> VarDecl
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimkSelVar n m ty = VarDecl (mkSelId (getRange ty) "x" n m) ty Other nullRange
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigenTuple :: Int -> Int -> [Selector] -> [VarDecl]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigenTuple _ _ [] = []
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigenTuple n m (Select _ ty _ : sels) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski mkSelVar n m ty : genTuple n (m + 1) sels
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigenSelVars :: Int -> [[Selector]] -> [[VarDecl]]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigenSelVars _ [] = []
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigenSelVars n (ts:sels) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski genTuple n 1 ts : genSelVars (n + 1) sels
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeSelTupleEqs :: DataPat -> Term -> Int -> Int -> [Selector] -> [Named Term]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeSelTupleEqs dt@(DataPat _ tArgs _ rt) ct n m (Select mi ty p : sels) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski let sc = TypeScheme (map inVarTypeArg tArgs) (getSelType rt p ty) nullRange
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski in (case mi of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Just i -> let
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski vt = QualVar $ mkSelVar n m ty
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski eq = mkEqTerm eqId nullRange
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (mkApplTerm (mkOpTerm i sc) [ct]) vt
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski in [makeNamed ("ga_select_" ++ show i) eq]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ++ makeSelTupleEqs dt ct n (m + 1) sels
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeSelTupleEqs _ _ _ _ [] = []
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeSelEqs :: DataPat -> Term -> Int -> [[Selector]] -> [Named Term]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeSelEqs dt ct n (sel:sels) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski makeSelTupleEqs dt ct n 1 sel
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ++ makeSelEqs dt ct (n + 1) sels
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeSelEqs _ _ _ _ = []
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeAltSelEqs dt@(DataPat _ args _ rt) (Construct mc ts p sels) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Nothing -> []
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Just c -> let sc = TypeScheme (map inVarTypeArg args)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (getFunType rt p ts) nullRange
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski vars = genSelVars 1 sels
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ars = map ( \ vs -> mkTupleTerm (map QualVar vs) nullRange)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ct = mkApplTerm (mkOpTerm c newSc) ars
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski in map (mapNamed (mkForall (map GenTypeVarDecl args
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ++ map GenVarDecl (concat vars))))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski $ makeSelEqs dt ct 1 sels
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | create selector equations for a data type
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeDataSelEqs :: DataEntry -> Type -> [Named Sentence]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeDataSelEqs (DataEntry _ i _ args rk alts) rt =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski map (mapNamed Formula) $
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski concatMap (makeAltSelEqs $ DataPat i args rk rt) $ Set.toList alts
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | analyse the alternatives of a data type
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaAlts :: [DataPat] -> DataPat -> [Alternative] -> Env -> Result [AltDefn]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaAlts tys dt alts te =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski do l <- mapM (anaAlt tys dt te) alts
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Result (checkUniqueness $ catMaybes $
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski map ( \ (Construct i _ _ _) -> i) l) $ Just ()
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaAlt :: [DataPat] -> DataPat -> Env -> Alternative
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -> Result AltDefn
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaAlt _ _ te (Subtype ts _) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski do l <- mapM ( \ t -> anaStarTypeM t te) ts
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski return $ Construct Nothing (Set.toList $ Set.fromList $ map snd l)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaAlt tys dt te (Constructor i cs p _) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski do newCs <- mapM (anaComps tys dt te) cs
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski let sels = map snd newCs
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Result (checkUniqueness $ catMaybes $
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski map ( \ (Select s _ _) -> s ) $ concat sels) $ Just ()
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski return $ Construct (Just i) (map fst newCs) p sels
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaComps :: [DataPat] -> DataPat -> Env -> [Component]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -> Result (Type, [Selector])
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaComps tys rt te cs =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski do newCs <- mapM (anaComp tys rt te) cs
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski return (mkProductType $ map fst newCs, map snd newCs)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaComp :: [DataPat] -> DataPat -> Env -> Component
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -> Result (Type, Selector)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaComp tys rt te (Selector s _ t _ _) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski do ct <- anaCompType tys rt t te
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski let (p, nct) = case getTypeAppl ct of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (TypeName i _ _, [lt]) | i == lazyTypeId -> (Partial, lt)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski _ -> (Total, ct)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski return (nct, Select (Just s) nct p)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaComp tys rt te (NoSelector t) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski do ct <- anaCompType tys rt t te
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski return (ct, Select Nothing ct Partial)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaCompType :: [DataPat] -> DataPat -> Type -> Env -> Result Type
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskianaCompType tys (DataPat _ tArgs _ _) t te = do
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (_, ct) <- anaStarTypeM t te
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski let ds = unboundTypevars True tArgs ct
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski if null ds then return () else Result ds Nothing
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski mapM (checkMonomorphRecursion ct te) tys
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski return $ generalize tArgs ct
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskicheckMonomorphRecursion :: Type -> Env -> DataPat -> Result ()
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskicheckMonomorphRecursion t te (DataPat i _ _ rt) =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski case filter (\ ty -> not (lesserType te ty rt || lesserType te rt ty))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski $ findSubTypes (typeMap te) i t of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski [] -> return ()
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ty : _ -> Result [Diag Error ("illegal polymorphic recursion"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ++ expected rt ty) $ getRange ty] Nothing
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskifindSubTypes :: TypeMap -> Id -> Type -> [Type]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskifindSubTypes tm i t = case getTypeAppl t of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (TypeName j _ _, args) -> if relatedTypeIds tm i j then [t]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski else concatMap (findSubTypes tm i) args
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (topTy, args) -> concatMap (findSubTypes tm i) $ topTy : args
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskirelatedTypeIds :: TypeMap -> Id -> Id -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskirelatedTypeIds tm i1 i2 =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski not $ Set.null $ Set.intersection (allRelIds tm i1) $ allRelIds tm i2
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiallRelIds :: TypeMap -> Id -> Set.Set Id
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiallRelIds tm i = Set.union (superIds tm i) $ subIds tm i
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskisubIds :: TypeMap -> Id -> Set.Set Id
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskisubIds tm i = foldr ( \ j s ->
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski if Set.member i $ superIds tm j then