DataAna.hs revision 961fc5d08256957f68f245f2723085ced14a0a1f
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiDescription : analysis of data type declarations
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiMaintainer : Christian.Maeder@dfki.de
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiStability : provisional
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiPortability : portable
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskianalyse alternatives of data types
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski-}
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskimodule HasCASL.DataAna
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski ( DataPat(..)
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski , anaAlts
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski , makeDataSelEqs
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski ) where
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport Data.Maybe
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowskiimport qualified Data.Map as Map
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport qualified Data.Set as Set
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport Common.Id
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport Common.Result
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport Common.AS_Annotation
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport HasCASL.As
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescuimport HasCASL.Le
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport HasCASL.TypeAna
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport HasCASL.AsUtils
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport HasCASL.Builtin
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiimport HasCASL.Unify
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski-- | description of polymorphic data types
04f798a5a79477754ad20e255444d99757911be0mcodescudata DataPat = DataPat Id [TypeArg] RawKind Type
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski
27de5bf664bde811f402d8e43db0721d3c58362cTill MossakowskimkSelId :: Range -> String -> Int -> Int -> Id
27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescumkSelId p str n m = mkId
27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescu [Token (str ++ "_" ++ show n ++ "_" ++ show m) p]
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescumkSelVar :: Int -> Int -> Type -> VarDecl
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescumkSelVar n m ty = VarDecl (mkSelId (getRange ty) "x" n m) ty Other nullRange
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu
b0dc688d623e51d3848b4b56d090669f18fc8f17mcodescugenTuple :: Int -> Int -> [Selector] -> [VarDecl]
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescugenTuple _ _ [] = []
27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescugenTuple n m (Select _ ty _ : sels) =
04f798a5a79477754ad20e255444d99757911be0mcodescu mkSelVar n m ty : genTuple n (m + 1) sels
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski
c0ca1d8524a3ca7f687adf192468541ae68802c9mcodescugenSelVars :: Int -> [[Selector]] -> [[VarDecl]]
82a602f211abdebc623f4823b913c8ffea10af06mcodescugenSelVars _ [] = []
82a602f211abdebc623f4823b913c8ffea10af06mcodescugenSelVars n (ts:sels) =
82a602f211abdebc623f4823b913c8ffea10af06mcodescu genTuple n 1 ts : genSelVars (n + 1) sels
82a602f211abdebc623f4823b913c8ffea10af06mcodescu
82a602f211abdebc623f4823b913c8ffea10af06mcodescumakeSelTupleEqs :: DataPat -> Term -> Int -> Int -> [Selector] -> [Named Term]
27de5bf664bde811f402d8e43db0721d3c58362cTill MossakowskimakeSelTupleEqs dt@(DataPat _ tArgs _ rt) ct n m (Select mi ty p : sels) =
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski let sc = TypeScheme (map inVarTypeArg tArgs) (getSelType rt p ty) nullRange
156ff56fb6d907911e63df36d12df9220877981amcodescu in (case mi of
156ff56fb6d907911e63df36d12df9220877981amcodescu Just i -> let
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski vt = QualVar $ mkSelVar n m ty
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski eq = mkEqTerm eqId nullRange
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski (mkApplTerm (mkOpTerm i sc) [ct]) vt
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski in [makeNamed ("ga_select_" ++ show i) eq]
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski _ -> [])
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski ++ makeSelTupleEqs dt ct n (m + 1) sels
27de5bf664bde811f402d8e43db0721d3c58362cTill MossakowskimakeSelTupleEqs _ _ _ _ [] = []
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski
27de5bf664bde811f402d8e43db0721d3c58362cTill MossakowskimakeSelEqs :: DataPat -> Term -> Int -> [[Selector]] -> [Named Term]
27de5bf664bde811f402d8e43db0721d3c58362cTill MossakowskimakeSelEqs dt ct n (sel:sels) =
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski makeSelTupleEqs dt ct n 1 sel
04f798a5a79477754ad20e255444d99757911be0mcodescu ++ makeSelEqs dt ct (n + 1) sels
04f798a5a79477754ad20e255444d99757911be0mcodescumakeSelEqs _ _ _ _ = []
04f798a5a79477754ad20e255444d99757911be0mcodescu
27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescumakeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskimakeAltSelEqs dt@(DataPat _ args _ rt) (Construct mc ts p sels) =
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski case mc of
c0ca1d8524a3ca7f687adf192468541ae68802c9mcodescu Nothing -> []
76212ada4c518a69f3125b3531b716c7f5151177mcodescu Just c -> let
04f798a5a79477754ad20e255444d99757911be0mcodescu iargs = map inVarTypeArg args
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski sc = TypeScheme iargs (getFunType rt p ts) nullRange
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski vars = genSelVars 1 sels
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu ars = map ( \ vs -> mkTupleTerm (map QualVar vs) nullRange) vars
04f798a5a79477754ad20e255444d99757911be0mcodescu ct = mkApplTerm (mkOpTerm c sc) ars
04f798a5a79477754ad20e255444d99757911be0mcodescu in map (mapNamed (mkForall (map GenTypeVarDecl iargs
04f798a5a79477754ad20e255444d99757911be0mcodescu ++ map GenVarDecl (concat vars)))) $ makeSelEqs dt ct 1 sels
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu-- | create selector equations for a data type
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescumakeDataSelEqs :: DataEntry -> Type -> [Named Sentence]
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescumakeDataSelEqs (DataEntry _ i _ args rk alts) rt = map (mapNamed Formula)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski $ concatMap (makeAltSelEqs $ DataPat i args rk rt)
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu $ Set.toList alts
04f798a5a79477754ad20e255444d99757911be0mcodescu
04f798a5a79477754ad20e255444d99757911be0mcodescu-- | analyse the alternatives of a data type
04f798a5a79477754ad20e255444d99757911be0mcodescuanaAlts :: [DataPat] -> DataPat -> [Alternative] -> Env -> Result [AltDefn]
04f798a5a79477754ad20e255444d99757911be0mcodescuanaAlts tys dt alts te =
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski do l <- mapM (anaAlt tys dt te) alts
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski Result (checkUniqueness $ catMaybes $
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu map ( \ (Construct i _ _ _) -> i) l) $ Just ()
c0ca1d8524a3ca7f687adf192468541ae68802c9mcodescu return l
82a602f211abdebc623f4823b913c8ffea10af06mcodescu
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescuanaAlt :: [DataPat] -> DataPat -> Env -> Alternative
27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescu -> Result AltDefn
27ae03fc2f67c39292e72f0a69837f34b2521c29mcodescuanaAlt _ _ te (Subtype ts _) =
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu do l <- mapM ( \ t -> anaStarTypeM t te) ts
04f798a5a79477754ad20e255444d99757911be0mcodescu return $ Construct Nothing (Set.toList $ Set.fromList $ map snd l)
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescu Partial []
09e732ce6115cf6aaedc2622e8e78696bb875b60mcodescuanaAlt tys dt te (Constructor i cs p _) =
04f798a5a79477754ad20e255444d99757911be0mcodescu do newCs <- mapM (anaComps tys dt te) cs
04f798a5a79477754ad20e255444d99757911be0mcodescu let sels = map snd newCs
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski Result (checkUniqueness $ catMaybes $
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu map ( \ (Select s _ _) -> s ) $ concat sels) $ Just ()
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu return $ Construct (Just i) (map fst newCs) p sels
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu
04f798a5a79477754ad20e255444d99757911be0mcodescuanaComps :: [DataPat] -> DataPat -> Env -> [Component]
35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu -> Result (Type, [Selector])
35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescuanaComps tys rt te cs =
04f798a5a79477754ad20e255444d99757911be0mcodescu do newCs <- mapM (anaComp tys rt te) cs
04f798a5a79477754ad20e255444d99757911be0mcodescu return (mkProductType $ map fst newCs, map snd newCs)
35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu
35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescuanaComp :: [DataPat] -> DataPat -> Env -> Component
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski -> Result (Type, Selector)
35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescuanaComp tys rt te (Selector s _ t _ _) =
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu do ct <- anaCompType tys rt t te
35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu let (p, nct) = case getTypeAppl ct of
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu (TypeName i _ _, [lt]) | i == lazyTypeId -> (Partial, lt)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski _ -> (Total, ct)
80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski return (nct, Select (Just s) nct p)
35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescuanaComp tys rt te (NoSelector t) =
35f4256bb7c21011ecd0656f32cd8e3275253ff7mcodescu do ct <- anaCompType tys rt t te
04f798a5a79477754ad20e255444d99757911be0mcodescu return (ct, Select Nothing ct Partial)
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescu
b6f5631ceb98f1be235d3b53e145f83fd7565bfamcodescuanaCompType :: [DataPat] -> DataPat -> Type -> Env -> Result Type
80875f917d741946a39d0ec0b5721e46ba609823Till MossakowskianaCompType tys (DataPat _ tArgs _ _) t te = do
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski (_, ct) <- anaStarTypeM t te
27de5bf664bde811f402d8e43db0721d3c58362cTill Mossakowski let ds = unboundTypevars True tArgs ct
if null ds then return () else Result ds Nothing
mapM (checkMonomorphRecursion ct te) tys
return $ generalize tArgs ct
checkMonomorphRecursion :: Type -> Env -> DataPat -> Result ()
checkMonomorphRecursion t te (DataPat i _ _ rt) =
case filter (\ ty -> not (lesserType te ty rt || lesserType te rt ty))
$ findSubTypes (typeMap te) i t of
[] -> return ()
ty : _ -> Result [Diag Error ("illegal polymorphic recursion"
++ expected rt ty) $ getRange ty] Nothing
findSubTypes :: TypeMap -> Id -> Type -> [Type]
findSubTypes tm i t = case getTypeAppl t of
(TypeName j _ _, args) -> if relatedTypeIds tm i j then [t]
else concatMap (findSubTypes tm i) args
(topTy, args) -> concatMap (findSubTypes tm i) $ topTy : args
relatedTypeIds :: TypeMap -> Id -> Id -> Bool
relatedTypeIds tm i1 i2 =
not $ Set.null $ Set.intersection (allRelIds tm i1) $ allRelIds tm i2
allRelIds :: TypeMap -> Id -> Set.Set Id
allRelIds tm i = Set.union (superIds tm i) $ subIds tm i
subIds :: TypeMap -> Id -> Set.Set Id
subIds tm i = foldr ( \ j s ->
if Set.member i $ superIds tm j then
Set.insert j s else s) Set.empty $ Map.keys tm