DataAna.hs revision 304c84f22dd78f7979efd81b8fc38c8d2197ed39
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{- |
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachModule : $Header$
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettCopyright : (c) Christian Maeder and Uni Bremen 2002-2005
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : maeder@tzi.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiPortability : portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachanalyse alternatives of data types
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule HasCASL.DataAna where
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Data.Maybe
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport qualified Common.Lib.Map as Map
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport qualified Common.Lib.Set as Set
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Common.Id
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Common.Result
842ae753ab848a8508c4832ab64296b929167a97Christian Maederimport Common.AS_Annotation
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyimport HasCASL.As
816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'Reillyimport HasCASL.Le
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport HasCASL.TypeAna
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reillyimport HasCASL.AsUtils
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyimport HasCASL.Builtin
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyimport HasCASL.Unify
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly
d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder-- | description of polymorphic data types
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillydata DataPat = DataPat Id [TypeArg] RawKind Type
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder-- * creating selector equations
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettmkSelId :: Range -> String -> Int -> Int -> Id
842ae753ab848a8508c4832ab64296b929167a97Christian MaedermkSelId p str n m = mkId
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly [Token (str ++ "_" ++ show n ++ "_" ++ show m) p]
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillymkSelVar :: Int -> Int -> Type -> VarDecl
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettmkSelVar n m ty = VarDecl (mkSelId (getRange ty) "x" n m) ty Other nullRange
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygenTuple :: Int -> Int -> [Selector] -> [VarDecl]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygenTuple _ _ [] = []
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygenTuple n m (Select _ ty _ : sels) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly mkSelVar n m ty : genTuple n (m + 1) sels
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygenSelVars :: Int -> [[Selector]] -> [[VarDecl]]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygenSelVars _ [] = []
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillygenSelVars n (ts:sels) =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly genTuple n 1 ts : genSelVars (n + 1) sels
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymakeSelTupleEqs :: DataPat -> Term -> Int -> Int -> [Selector] -> [Named Term]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymakeSelTupleEqs dt@(DataPat _ tArgs _ rt) ct n m (Select mi ty p : sels) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder let sc = TypeScheme tArgs (getSelType rt p ty) nullRange in
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (case mi of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just i -> let
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder vt = QualVar $ mkSelVar n m ty
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder eq = mkEqTerm eqId nullRange
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (mkApplTerm (mkOpTerm i sc) [ct]) vt
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly in [NamedSen ("ga_select_" ++ show i) True False eq]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly _ -> [])
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly ++ makeSelTupleEqs dt ct n (m + 1) sels
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymakeSelTupleEqs _ _ _ _ [] = []
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymakeSelEqs :: DataPat -> Term -> Int -> [[Selector]] -> [Named Term]
842ae753ab848a8508c4832ab64296b929167a97Christian MaedermakeSelEqs dt ct n (sel:sels) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder makeSelTupleEqs dt ct n 1 sel
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ++ makeSelEqs dt ct (n + 1) sels
842ae753ab848a8508c4832ab64296b929167a97Christian MaedermakeSelEqs _ _ _ _ = []
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymakeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymakeAltSelEqs dt@(DataPat _ args _ rt) (Construct mc ts p sels) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case mc of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Nothing -> []
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Just c -> let sc = TypeScheme args (getFunType rt p ts) nullRange
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly newSc = sc
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder vars = genSelVars 1 sels
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ars = map ( \ vs -> mkTupleTerm (map QualVar vs) nullRange)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly vars
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ct = mkApplTerm (mkOpTerm c newSc) ars
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder in map (mapNamed (mkForall (map GenTypeVarDecl args
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder ++ map GenVarDecl (concat vars))))
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly $ makeSelEqs dt ct 1 sels
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymakeDataSelEqs :: DataEntry -> Type -> [Named Sentence]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillymakeDataSelEqs (DataEntry _ i _ args rk alts) rt =
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett map (mapNamed Formula) $
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly concatMap (makeAltSelEqs $ DataPat i args rk rt) alts
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- * analysis of alternatives
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettanaAlts :: [DataPat] -> DataPat -> [Alternative] -> TypeEnv -> Result [AltDefn]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyanaAlts tys dt alts te =
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly do l <- mapM (anaAlt tys dt te) alts
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder Result (checkUniqueness $ catMaybes $
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly map ( \ (Construct i _ _ _) -> i) l) $ Just ()
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return l
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyanaAlt :: [DataPat] -> DataPat -> TypeEnv -> Alternative
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -> Result AltDefn
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyanaAlt _ _ te (Subtype ts _) =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly do l <- mapM ( \ t -> anaStarTypeM t te) ts
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder return $ Construct Nothing (map snd l) Partial []
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettanaAlt tys dt te (Constructor i cs p _) =
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett do newCs <- mapM (anaComps tys dt te) cs
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett let sels = map snd newCs
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett Result (checkUniqueness $ catMaybes $
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder map ( \ (Select s _ _) -> s ) $ concat sels) $ Just ()
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder return $ Construct (Just i) (map fst newCs) p sels
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettanaComps :: [DataPat] -> DataPat -> TypeEnv -> [Component]
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -> Result (Type, [Selector])
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettanaComps tys rt te cs =
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder do newCs <- mapM (anaComp tys rt te) cs
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder return (mkProductType $ map fst newCs, map snd newCs)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettanaComp :: [DataPat] -> DataPat -> TypeEnv -> Component
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -> Result (Type, Selector)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettanaComp tys rt te (Selector s p t _ _) =
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder do ct <- anaCompType tys rt t te
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder return (ct, Select (Just s) ct p)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettanaComp tys rt te (NoSelector t) =
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett do ct <- anaCompType tys rt t te
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder return (ct, Select Nothing ct Partial)
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederanaCompType :: [DataPat] -> DataPat -> Type -> TypeEnv -> Result Type
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyanaCompType tys (DataPat _ tArgs _ _) t te = do
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (_, ct) <- anaStarTypeM t te
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett let ds = unboundTypevars True tArgs ct
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett if null ds then return () else Result ds Nothing
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett mapM (checkMonomorphRecursion ct te) tys
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett return $ generalize tArgs ct
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcheckMonomorphRecursion :: Type -> TypeEnv -> DataPat -> Result ()
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettcheckMonomorphRecursion t te (DataPat i _ _ rt) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder case filter (\ ty -> not (lesserType te ty rt || lesserType te rt ty))
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder $ findSubTypes (typeMap te) i t of
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly [] -> return ()
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ty : _ -> Result [Diag Error ("illegal polymorphic recursion"
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ++ expected rt ty) $ getRange ty] Nothing
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
842ae753ab848a8508c4832ab64296b929167a97Christian MaederfindSubTypes :: TypeMap -> TypeId -> Type -> [Type]
842ae753ab848a8508c4832ab64296b929167a97Christian MaederfindSubTypes tm i t = case getTypeAppl t of
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (TypeName j _ _, args) -> if relatedTypeIds tm i j then [t]
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder else concatMap (findSubTypes tm i) args
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reilly (topTy, args) -> concatMap (findSubTypes tm i) $ topTy : args
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly
842ae753ab848a8508c4832ab64296b929167a97Christian MaederrelatedTypeIds :: TypeMap -> TypeId -> TypeId -> Bool
842ae753ab848a8508c4832ab64296b929167a97Christian MaederrelatedTypeIds tm i1 i2 =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder not $ Set.null $ Set.intersection (allRelIds tm i1) $ allRelIds tm i2
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyallRelIds :: TypeMap -> TypeId -> Set.Set TypeId
842ae753ab848a8508c4832ab64296b929167a97Christian MaederallRelIds tm i = Set.union (superIds tm i) $ subIds tm i
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettsubIds :: TypeMap -> Id -> Set.Set Id
929190acb9f2b2f5857dce841c5a389710895515Andy GimblettsubIds tm i = foldr ( \ j s ->
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly if Set.member i $ superIds tm j then
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly Set.insert j s else s) Set.empty $ Map.keys tm
cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly