DataAna.hs revision 0ea85310d2beb8aa03cac481ad2a6564e6b8ddbc
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly{- |
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyModule : $Header$
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyDescription : analysis of data type declarations
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillyCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillyLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyMaintainer : Christian.Maeder@dfki.de
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyStability : provisional
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyPortability : portable
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillyanalyse alternatives of data types
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-}
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillymodule HasCASL.DataAna
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly ( DataPat(..)
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly , anaAlts
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly , makeDataSelEqs
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly , inVarTypeArg
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly ) where
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reillyimport Data.Maybe
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reillyimport qualified Data.Map as Map
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillyimport qualified Data.Set as Set
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillyimport Common.Id
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillyimport Common.Result
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillyimport Common.AS_Annotation
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillyimport HasCASL.As
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillyimport HasCASL.Le
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillyimport HasCASL.TypeAna
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reillyimport HasCASL.AsUtils
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport HasCASL.Builtin
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport HasCASL.Unify
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly-- | description of polymorphic data types
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reillydata DataPat = DataPat Id [TypeArg] RawKind Type
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly-- make type argument invariant
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinVarTypeArg :: TypeArg -> TypeArg
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinVarTypeArg (TypeArg i _ vk rk c o p) = (TypeArg i InVar vk rk c o p)
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillymkSelId :: Range -> String -> Int -> Int -> Id
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillymkSelId p str n m = mkId
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly [Token (str ++ "_" ++ show n ++ "_" ++ show m) p]
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillymkSelVar :: Int -> Int -> Type -> VarDecl
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillymkSelVar n m ty = VarDecl (mkSelId (getRange ty) "x" n m) ty Other nullRange
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillygenTuple :: Int -> Int -> [Selector] -> [VarDecl]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillygenTuple _ _ [] = []
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillygenTuple n m (Select _ ty _ : sels) =
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly mkSelVar n m ty : genTuple n (m + 1) sels
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillygenSelVars :: Int -> [[Selector]] -> [[VarDecl]]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillygenSelVars _ [] = []
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillygenSelVars n (ts:sels) =
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly genTuple n 1 ts : genSelVars (n + 1) sels
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillymakeSelTupleEqs :: DataPat -> Term -> Int -> Int -> [Selector] -> [Named Term]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillymakeSelTupleEqs dt@(DataPat _ tArgs _ rt) ct n m (Select mi ty p : sels) =
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly let sc = TypeScheme (map inVarTypeArg tArgs) (getSelType rt p ty) nullRange
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly in (case mi of
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly Just i -> let
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly vt = QualVar $ mkSelVar n m ty
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly eq = mkEqTerm eqId nullRange
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly (mkApplTerm (mkOpTerm i sc) [ct]) vt
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly in [makeNamed ("ga_select_" ++ show i) eq]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> [])
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly ++ makeSelTupleEqs dt ct n (m + 1) sels
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillymakeSelTupleEqs _ _ _ _ [] = []
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillymakeSelEqs :: DataPat -> Term -> Int -> [[Selector]] -> [Named Term]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillymakeSelEqs dt ct n (sel:sels) =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly makeSelTupleEqs dt ct n 1 sel
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly ++ makeSelEqs dt ct (n + 1) sels
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillymakeSelEqs _ _ _ _ = []
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'ReillymakeAltSelEqs dt@(DataPat _ args _ rt) (Construct mc ts p sels) =
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly case mc of
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly Nothing -> []
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly Just c -> let sc = TypeScheme (map inVarTypeArg args)
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly (getFunType rt p ts) nullRange
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly newSc = sc
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly vars = genSelVars 1 sels
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly ars = map ( \ vs -> mkTupleTerm (map QualVar vs) nullRange)
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly vars
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ct = mkApplTerm (mkOpTerm c newSc) ars
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly in map (mapNamed (mkForall (map GenTypeVarDecl args
65f3cba1cc071292846eb69c59007c5a199ee941Liam O'Reilly ++ map GenVarDecl (concat vars))))
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly $ makeSelEqs dt ct 1 sels
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | create selector equations for a data type
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillymakeDataSelEqs :: DataEntry -> Type -> [Named Sentence]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillymakeDataSelEqs (DataEntry _ i _ args rk alts) rt =
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly map (mapNamed Formula) $
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly concatMap (makeAltSelEqs $ DataPat i args rk rt) $ Set.toList alts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly-- | analyse the alternatives of a data type
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyanaAlts :: [DataPat] -> DataPat -> [Alternative] -> Env -> Result [AltDefn]
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillyanaAlts tys dt alts te =
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly do l <- mapM (anaAlt tys dt te) alts
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly Result (checkUniqueness $ catMaybes $
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly map ( \ (Construct i _ _ _) -> i) l) $ Just ()
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly return l
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyanaAlt :: [DataPat] -> DataPat -> Env -> Alternative
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Result AltDefn
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyanaAlt _ _ te (Subtype ts _) =
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly do l <- mapM ( \ t -> anaStarTypeM t te) ts
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly return $ Construct Nothing (map snd l) Partial []
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyanaAlt tys dt te (Constructor i cs p _) =
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly do newCs <- mapM (anaComps tys dt te) cs
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly let sels = map snd newCs
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly Result (checkUniqueness $ catMaybes $
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly map ( \ (Select s _ _) -> s ) $ concat sels) $ Just ()
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly return $ Construct (Just i) (map fst newCs) p sels
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyanaComps :: [DataPat] -> DataPat -> Env -> [Component]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly -> Result (Type, [Selector])
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillyanaComps tys rt te cs =
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly do newCs <- mapM (anaComp tys rt te) cs
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly return (mkProductType $ map fst newCs, map snd newCs)
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyanaComp :: [DataPat] -> DataPat -> Env -> Component
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly -> Result (Type, Selector)
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyanaComp tys rt te (Selector s _ t _ _) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do ct <- anaCompType tys rt t te
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly let (p, nct) = case getTypeAppl ct of
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly (TypeName i _ _, [lt]) | i == lazyTypeId -> (Partial, lt)
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly _ -> (Total, ct)
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly return (nct, Select (Just s) nct p)
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyanaComp tys rt te (NoSelector t) =
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly do ct <- anaCompType tys rt t te
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly return (ct, Select Nothing ct Partial)
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyanaCompType :: [DataPat] -> DataPat -> Type -> Env -> Result Type
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederanaCompType tys (DataPat _ tArgs _ _) t te = do
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly (_, ct) <- anaStarTypeM t te
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly let ds = unboundTypevars True tArgs ct
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly if null ds then return () else Result ds Nothing
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly mapM (checkMonomorphRecursion ct te) tys
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly return $ generalize tArgs ct
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycheckMonomorphRecursion :: Type -> Env -> DataPat -> Result ()
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillycheckMonomorphRecursion t te (DataPat i _ _ rt) =
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly case filter (\ ty -> not (lesserType te ty rt || lesserType te rt ty))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $ findSubTypes (typeMap te) i t of
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly [] -> return ()
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly ty : _ -> Result [Diag Error ("illegal polymorphic recursion"
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly ++ expected rt ty) $ getRange ty] Nothing
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyfindSubTypes :: TypeMap -> Id -> Type -> [Type]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyfindSubTypes tm i t = case getTypeAppl t of
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly (TypeName j _ _, args) -> if relatedTypeIds tm i j then [t]
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly else concatMap (findSubTypes tm i) args
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly (topTy, args) -> concatMap (findSubTypes tm i) $ topTy : args
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyrelatedTypeIds :: TypeMap -> Id -> Id -> Bool
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyrelatedTypeIds tm i1 i2 =
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'Reilly not $ Set.null $ Set.intersection (allRelIds tm i1) $ allRelIds tm i2
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
059e541d741fa3faa3a2e4cf81fc7627a87ce3b7Liam O'ReillyallRelIds :: TypeMap -> Id -> Set.Set Id
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillyallRelIds tm i = Set.union (superIds tm i) $ subIds tm i
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillysubIds :: TypeMap -> Id -> Set.Set Id
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'ReillysubIds tm i = foldr ( \ j s ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if Set.member i $ superIds tm j then
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly Set.insert j s else s) Set.empty $ Map.keys tm
045f46b4b5421fb16786bd5bcd612291faf7e7a9Liam O'Reilly