DataAna.hs revision 715ffaf874309df081d1e1cd8e05073fc1227729
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian MaederModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
a480b70e29a3ed7e77b89e410fd7bbab3e5a7e67Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : hets@tzi.de
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian MaederStability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : non-portable (MonadState)
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maederanalyse alternatives of data types
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Common.Lib.Set as Set
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangmkSelId :: String -> Int -> Int -> Id
831bfb0c3598d0508b976cd36fa97c65839ed5a3Christian MaedermkSelId str n m = mkId [mkSimpleId (str ++ "_" ++ show n ++ "_" ++ show m)]
1a38107941725211e7c3f051f7a8f5e12199f03acmaedermkSelVar :: Int -> Int -> Type -> VarDecl
e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian MaedermkSelVar n m ty = VarDecl (mkSelId "x" n m) ty Other []
806a572a6b39297e26af6b94e227b70ab295adacChristian MaedergenTuple :: Int -> Int -> [Selector] -> [VarDecl]
2b4130336e941b7d01c78a6da55449a4c6eca609Till MossakowskigenTuple _ _ [] = []
bc48a75c0a968be3d6cb31768a4120cafba0d202Christian MaedergenTuple n m (Select _ ty _ : sels) =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder mkSelVar n m ty : genTuple n (m + 1) sels
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian MaedergenSelVars :: Int -> [[Selector]] -> [[VarDecl]]
4e14c1bc2b97679b84c6ad996fa11c273b74ea02Christian MaedergenSelVars _ [] = []
4e14c1bc2b97679b84c6ad996fa11c273b74ea02Christian MaedergenSelVars n (ts:sels) =
4e14c1bc2b97679b84c6ad996fa11c273b74ea02Christian Maeder genTuple n 1 ts : genSelVars (n + 1) sels
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian MaedermakeSelTupleEqs :: Type -> [TypeArg] -> Term -> Int -> Int -> [Selector]
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder -> [Named Term]
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian MaedermakeSelTupleEqs dt args ct n m (Select mi ty p : sels) =
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder Nothing -> []
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder Just i -> let sc = TypeScheme args ([] :=> getSelType dt p ty) []
7fcb2e9d349608760b0c2c16a864c6f39d455383Christian Maeder vt = toQualVar $ mkSelVar n m ty
7fcb2e9d349608760b0c2c16a864c6f39d455383Christian Maeder eq = mkEqTerm eqId [] (mkApplTerm (mkOpTerm i sc) [ct]) vt
7fcb2e9d349608760b0c2c16a864c6f39d455383Christian Maeder in [NamedSen ("ga_select_" ++ show i) eq])
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder ++ makeSelTupleEqs dt args ct n (m + 1) sels
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian MaedermakeSelTupleEqs _ _ _ _ _ [] = []
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian MaedermakeSelEqs :: Type -> [TypeArg] -> Term -> Int -> [[Selector]]
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder -> [Named Term]
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian MaedermakeSelEqs dt args ct n (sel:sels) =
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder makeSelTupleEqs dt args ct n 1 sel
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder ++ makeSelEqs dt args ct (n + 1) sels
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian MaedermakeSelEqs _ _ _ _ _ = []
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedermakeAltSelEqs :: Type -> [TypeArg] -> AltDefn -> [Named Term]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedermakeAltSelEqs dt args (Construct mc ts p sels) =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Nothing -> []
95930e7e3689b644fcccb27cc0a26a1b5ed9d0b1Christian Maeder Just c -> let sc = TypeScheme args ([] :=> getConstrType dt p ts) []
e3169ed5885bb0888d8366c0d31ce1682e0fae74Christian Maeder vars = genSelVars 1 sels
95930e7e3689b644fcccb27cc0a26a1b5ed9d0b1Christian Maeder as = map ( \ vs -> mkTupleTerm (map toQualVar vs) []) vars
e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder ct = mkApplTerm (mkOpTerm c sc) as
e00f5b4d89ac027e883461aab6248e33ad10ae8eChristian Maeder in map (mapNamed (mkForall (map GenTypeVarDecl args
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder ++ map GenVarDecl (concat vars))))
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder $ makeSelEqs dt args ct 1 sels
961978c71545e0177683279f8b63358b3e3804b8Christian MaedermakeDataSelEqs :: DataEntry -> [Named Sentence]
961978c71545e0177683279f8b63358b3e3804b8Christian MaedermakeDataSelEqs (DataEntry _ i _ args alts) =
961978c71545e0177683279f8b63358b3e3804b8Christian Maeder map (mapNamed Formula) $
961978c71545e0177683279f8b63358b3e3804b8Christian Maeder concatMap (makeAltSelEqs (typeIdToType i args star) args) alts
961978c71545e0177683279f8b63358b3e3804b8Christian MaederanaAlts :: [(Id, Type)] -> Type -> [Alternative] -> TypeMap -> Result [AltDefn]
26d11a256b1433604a3dbc69913b520fff7586acChristian MaederanaAlts tys dt alts tm =
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder do l <- mapM (anaAlt tys dt tm) alts
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder Result (checkUniqueness $ catMaybes $
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder map ( \ (Construct i _ _ _) -> i) l) $ Just ()
26d11a256b1433604a3dbc69913b520fff7586acChristian MaederanaAlt :: [(Id, Type)] -> Type -> TypeMap -> Alternative -> Result AltDefn
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaAlt _ _ tm (Subtype ts _) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder do l <- mapM ( \ t -> anaType (Just star, t) tm) ts
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ Construct Nothing (map snd l) Partial []
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederanaAlt tys dt tm (Constructor i cs p _) =
806a572a6b39297e26af6b94e227b70ab295adacChristian Maeder do newCs <- mapM (anaComps tys dt tm) cs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let sels = map snd newCs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Result (checkUniqueness $ catMaybes $
806a572a6b39297e26af6b94e227b70ab295adacChristian Maeder map ( \ (Select s _ _) -> s ) $ concat sels) $ Just ()
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ Construct (Just i) (map fst newCs) p sels
986d3f255182539098a97ac86da9eeee5b7a72e3Christian MaederanaComps :: [(Id, Type)] -> Type -> TypeMap -> [Component]
45aaa7a259465da54f71852ac0c6c39cd987730dChristian Maeder -> Result (Type, [Selector])
45aaa7a259465da54f71852ac0c6c39cd987730dChristian MaederanaComps tys rt tm cs =
45aaa7a259465da54f71852ac0c6c39cd987730dChristian Maeder do newCs <- mapM (anaComp tys rt tm) cs
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder return (mkProductType (map fst newCs) [], map snd newCs)
dece9056c18ada64bcc8f2fba285270374139ee8Christian MaederanaComp :: [(Id, Type)] -> Type -> TypeMap -> Component
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder -> Result (Type, Selector)
3e0ed56e973aeef92177e50f7272cafa7eb96fbeChristian MaederanaComp tys rt tm (Selector s p t _ _) =
3e0ed56e973aeef92177e50f7272cafa7eb96fbeChristian Maeder do ct <- anaCompType tys rt t tm
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maeder return (ct, Select (Just s) ct p)
45aaa7a259465da54f71852ac0c6c39cd987730dChristian MaederanaComp tys rt tm (NoSelector t) =
def4be60beab1d7285732ebcebad96fad7484120Christian Maeder do ct <- anaCompType tys rt t tm
45aaa7a259465da54f71852ac0c6c39cd987730dChristian Maeder return (ct, Select Nothing ct Partial)
45aaa7a259465da54f71852ac0c6c39cd987730dChristian MaedergetSelType :: Type -> Partiality -> Type -> Type
45aaa7a259465da54f71852ac0c6c39cd987730dChristian MaedergetSelType dt p rt = (case p of
45aaa7a259465da54f71852ac0c6c39cd987730dChristian Maeder Partial -> addPartiality [dt]
45aaa7a259465da54f71852ac0c6c39cd987730dChristian Maeder Total -> id) $ FunType dt FunArr rt []
45aaa7a259465da54f71852ac0c6c39cd987730dChristian MaederanaCompType :: [(Id, Type)] -> Type -> Type -> TypeMap -> Result Type
def4be60beab1d7285732ebcebad96fad7484120Christian MaederanaCompType tys dt t tm = do
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder (_, ct) <- anaType (Just star, t) tm
2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowski ct2 <- unboundTypevars (varsOf dt) ct
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder mapM (checkMonomorphRecursion ct2 tm) tys
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian MaedercheckMonomorphRecursion :: Type -> TypeMap -> (Id, Type) -> Result ()
5824312cc0cfccce61f195fbe92307a21a467049Christian MaedercheckMonomorphRecursion t tm (i, rt) =
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder if occursIn tm i $ unalias tm t then
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder if equalSubs tm t rt then return ()
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder else Result [Diag Error ("illegal polymorphic recursion"
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ++ expected rt t) $ getMyPos t] Nothing
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder else return ()
dece9056c18ada64bcc8f2fba285270374139ee8Christian MaederunboundTypevars :: Set.Set TypeArg -> Type -> Result Type
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian MaederunboundTypevars args ct =
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder let restVars = varsOf ct Set.\\ args in
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder if Set.isEmpty restVars then return ct
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder else Result [mkDiag Error ("unbound type variable(s)\n\t"
3e0ed56e973aeef92177e50f7272cafa7eb96fbeChristian Maeder ++ showSepList ("," ++) showPretty
4d4ec273e5cb1f17985c6edcf90a295a8b612cefChristian Maeder (Set.toList restVars) " in") ct] Nothing