Sign.hs revision b3bacd257ffcdd346b70ab690f03b28ad5f33fdc
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Definition of signatures for the Edinburgh
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski Logical Framework
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : k.sojakova@jacobs-university.de
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederStability : experimental
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , Symbol (..)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , getDeclaredSyms
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , getDefinedSyms
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder , getLocalSyms
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , getLocalDefs
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder , isDeclaredSym
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder , isDefinedSym
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich , getSymValue
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , getSymsOfType
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , getFreeVars
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , getConstants
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder , sigIntersection
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederimport qualified Data.List as List
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederimport qualified Data.Set as Set
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederimport qualified Data.Map as Map
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maedertype VAR = String
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maedertype NAME = String
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maedertype MODULE = String
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maedertype BASE = String
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maedergen_base :: String
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maedergen_module :: String
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maedergen_module = "GEN_SIG"
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maederdata Symbol = Symbol
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder { symBase :: BASE
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , symModule :: MODULE
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder , symName :: NAME
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder } deriving (Ord, Eq, Show)
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maedertype RAW_SYM = String
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaedertoSym :: RAW_SYM -> Symbol
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaedertoSym s = Symbol gen_base gen_module s
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maederinstance GetRange Symbol
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maederdata EXP = Type
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder | Const Symbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | Appl EXP [EXP]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder | Func [EXP] EXP
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder | Pi CONTEXT EXP
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder | Lamb CONTEXT EXP
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder deriving (Ord,Show)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance GetRange EXP
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maedertype Sentence = EXP
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maedertype CONTEXT = [(VAR,EXP)]
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederdata DEF = Def
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { getSym :: Symbol
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder , getType :: EXP
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , getValue :: Maybe EXP
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder } deriving (Eq,Ord,Show)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederdata Sign = Sign
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder { sigBase :: BASE
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , sigModule :: MODULE
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , getDefs :: [DEF]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski } deriving (Eq, Ord, Show)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiemptySig :: Sign
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiemptySig = Sign gen_base gen_module []
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederaddDef :: DEF -> Sign -> Sign
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederaddDef d (Sign b m ds) = Sign b m $ ds ++ [d]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- get the set of all symbols
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedergetSymbols :: Sign -> Set.Set Symbol
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedergetSymbols (Sign _ _ ds) = Set.fromList $ map getSym ds
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder-- checks if the symbol is defined or declared in the signature
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederisConstant :: Symbol -> Sign -> Bool
26d11a256b1433604a3dbc69913b520fff7586acChristian MaederisConstant s sig = Set.member s $ getSymbols sig
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- get the set of declared symbols
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedergetDeclaredSyms :: Sign -> Set.Set Symbol
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedergetDeclaredSyms (Sign _ _ ds) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Set.fromList $ map getSym $ filter (\ d -> isNothing $ getValue d) ds
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- checks if the symbol is declared in the signature
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaederisDeclaredSym :: Symbol -> Sign -> Bool
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederisDeclaredSym s sig = Set.member s $ getDeclaredSyms sig
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- get the set of declared symbols
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedergetDefinedSyms :: Sign -> Set.Set Symbol
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian MaedergetDefinedSyms (Sign _ _ ds) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Set.fromList $ map getSym $ filter (\ d -> isJust $ getValue d) ds
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- checks if the symbol is defined in the signature
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederisDefinedSym :: Symbol -> Sign -> Bool
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederisDefinedSym s sig = Set.member s $ getDefinedSyms sig
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- get the set of symbols not included from other signatures
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedergetLocalSyms :: Sign -> Set.Set Symbol
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedergetLocalSyms sig = Set.filter (\ s -> isLocalSym s sig) $ getSymbols sig
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder-- checks if the symbol is local to the signature
5e46b572ed576c0494768998b043d9d340594122Till MossakowskiisLocalSym :: Symbol -> Sign -> Bool
74d9a385499bf903b24848dff450a153f525bda7Christian MaederisLocalSym s sig =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder and [sigBase sig == symBase s, sigModule sig == symModule s]
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- get the list of local definitions
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedergetLocalDefs :: Sign -> [DEF]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedergetLocalDefs sig = filter (\ (Def s _ _) -> isLocalSym s sig) $ getDefs sig
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- returns the type/kind for the given symbol
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedergetSymType :: Symbol -> Sign -> Maybe EXP
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedergetSymType sym sig =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let res = List.find (\ d -> getSym d == sym) $ getDefs sig
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder in case res of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Nothing -> Nothing
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Just (Def _ t _) -> Just t
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- returns the value for the given symbol, if it exists
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedergetSymValue :: Symbol -> Sign -> Maybe EXP
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedergetSymValue sym sig =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let res = List.find (\ d -> getSym d == sym) $ getDefs sig
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in case res of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> Nothing
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Just (Def _ _ v) -> v
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- returns the set of symbols of the given type
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian MaedergetSymsOfType :: EXP -> Sign -> Set.Set Symbol
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian MaedergetSymsOfType t sig =
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder Set.fromList $ map getSym $ filter (\ (Def _ t' _) -> t' == t) $ getDefs sig
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder-- pretty printing
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maederinstance Pretty Sign where
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder pretty = printSig
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maederinstance Pretty DEF where
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder pretty = printDef
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maederinstance Pretty EXP where
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder pretty = printExp
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maederinstance Pretty Symbol where
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder pretty = printSymbol
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederprintSig :: Sign -> Doc
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaederprintSig sig = vcat $ map printDef (getDefs sig)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaederprintDef :: DEF -> Doc
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaederprintDef (Def s t v) =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Nothing -> fsep [ pretty s
ab642ff136ce716af9e609b667e3f06d766c4ad7Christian Maeder , colon <+> pretty t <> dot ]
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Just val -> fsep [ pretty s
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder , colon <+> pretty t
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder , text "=" <+> pretty val <> dot ]
99476ac2689c74251219db4782e57fe713a24a52Christian MaederprintSymbol :: Symbol -> Doc
99476ac2689c74251219db4782e57fe713a24a52Christian MaederprintSymbol s = text $ symName s
99476ac2689c74251219db4782e57fe713a24a52Christian MaederprintExp :: EXP -> Doc
99476ac2689c74251219db4782e57fe713a24a52Christian MaederprintExp Type = text "type"
99476ac2689c74251219db4782e57fe713a24a52Christian MaederprintExp (Const s) = pretty s
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian MaederprintExp (Var n) = text n
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederprintExp (Appl e es) =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let f = printExpWithPrec (precAppl + 1) e
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder as = map (printExpWithPrec precAppl) es
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder in hsep (f:as)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederprintExp (Func es e) =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let as = map (printExpWithPrec precFunc) es
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder val = printExpWithPrec (precFunc + 1) e
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder in hsep $ punctuate (text " ->") (as ++ [val])
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederprintExp (Pi ds e) = sep [braces $ printContext ds, pretty e]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederprintExp (Lamb ds e) = sep [brackets $ printContext ds, pretty e]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederprintExpWithPrec :: Int -> EXP -> Doc
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaederprintExpWithPrec i e =
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder if prec e >= i
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder then parens $ printExp e
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder else printExp e
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maederprec :: EXP -> Int
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederprec Const {} = 0
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederprec Var {} = 0
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederprec Appl {} = 1
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maederprec Func {} = 2
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maederprec Pi {} = 3
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maederprec Lamb {} = 3
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederprecFunc, precAppl :: Int
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian MaederprintContext :: CONTEXT -> Doc
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian MaederprintContext xs = sep $ punctuate comma $ map printVarDecl xs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprintVarDecl :: (VAR,EXP) -> Doc
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiprintVarDecl (n,e) = sep [text n, colon <+> pretty e]
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder{- converts the expression into a form where each construct takes
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder exactly one argument -}
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederrecForm :: EXP -> EXP
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederrecForm (Appl f []) = recForm f
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederrecForm (Appl f as) = Appl (recForm $ Appl f $ init as) $ [recForm $ last as]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederrecForm (Func [] a) = recForm a
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederrecForm (Func (t:ts) a) = Func [recForm t] $ recForm $ Func ts a
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederrecForm (Pi [] t) = recForm t
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederrecForm (Pi ((n,t):ds) a) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Pi [(n,recForm t)] $ recForm $ Pi ds a
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederrecForm (Lamb [] t) = recForm t
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederrecForm (Lamb ((n,t):ds) a) =
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Lamb [(n,recForm t)] $ recForm $ Lamb ds a
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder{- modifies the given name until it is different from each of the names
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder in the input set -}
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedergetNewName :: VAR -> Set.Set VAR -> VAR
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedergetNewName var names = getNewNameH var names var 0
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedergetNewNameH :: VAR -> Set.Set VAR -> VAR -> Int -> VAR
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedergetNewNameH var names root i =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder else let newVar = root ++ (show i)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in getNewNameH newVar names root $ i+1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- returns the set of free Variables used within an expression
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedergetFreeVars :: EXP -> Set.Set VAR
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedergetFreeVars e = getFreeVarsH $ recForm e
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedergetFreeVarsH :: EXP -> Set.Set VAR
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedergetFreeVarsH Type = Set.empty
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedergetFreeVarsH (Const _) = Set.empty
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedergetFreeVarsH (Var x) = Set.singleton x
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedergetFreeVarsH (Appl f [a]) =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Set.union (getFreeVarsH f) (getFreeVarsH a)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedergetFreeVarsH (Func [t] v) =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Set.union (getFreeVarsH t) (getFreeVarsH v)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedergetFreeVarsH (Pi [(n,t)] a) =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Set.delete n $ Set.union (getFreeVarsH t) (getFreeVarsH a)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedergetFreeVarsH (Lamb [(n,t)] a) =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Set.delete n $ Set.union (getFreeVarsH t) (getFreeVarsH a)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedergetFreeVarsH _ = Set.empty
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder-- returns the set of symbols used within an expression
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedergetConstants :: EXP -> Set.Set Symbol
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedergetConstants e = getConstantsH $ recForm e
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedergetConstantsH :: EXP -> Set.Set Symbol
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedergetConstantsH Type = Set.empty
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedergetConstantsH (Const s) = Set.singleton s
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian MaedergetConstantsH (Var _) = Set.empty
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedergetConstantsH (Appl f [a]) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Set.union (getConstantsH f) (getConstantsH a)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedergetConstantsH (Func [t] v) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Set.union (getConstantsH t) (getConstantsH v)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedergetConstantsH (Pi [(_,t)] a) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Set.union (getConstantsH t) (getConstantsH a)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedergetConstantsH (Lamb [(_,t)] a) =
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Set.union (getConstantsH t) (getConstantsH a)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedergetConstantsH _ = Set.empty
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder{- Variable renamings:
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder - the first argument specifies the desired Variable renamings
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder - the second argument specifies the set of Variables which cannot
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder be used as new Variable names -}
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederrename :: Map.Map VAR VAR -> Set.Set VAR -> EXP -> EXP
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederrename m s e = renameH m s (recForm e)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederrenameH :: Map.Map VAR VAR -> Set.Set VAR -> EXP -> EXP
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederrenameH _ _ Type = Type
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederrenameH _ _ (Const n) = Const n
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederrenameH m _ (Var n) = Var $ Map.findWithDefault n n m
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederrenameH m s (Appl f [a]) = Appl (rename m s f) [rename m s a]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederrenameH m s (Func [t] u) = Func [rename m s t] (rename m s u)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederrenameH m s (Pi [(x,t)] a) =
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let t1 = rename m s t
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder x1 = getNewName x s
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder a1 = rename (Map.insert x x1 m) (Set.insert x1 s) a
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder in Pi [(x1,t1)] a1
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederrenameH m s (Lamb [(x,t)] a) =
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let t1 = rename m s t
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder x1 = getNewName x s
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder a1 = rename (Map.insert x x1 m) (Set.insert x1 s) a
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder in Lamb [(x1,t1)] a1
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian MaederrenameH _ _ t = t
fa167e362877db231378e17ba49c66fbb84862fcChristian Maederinstance Eq EXP where
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder e1 == e2 = eqExp (recForm e1) (recForm e2)
fa167e362877db231378e17ba49c66fbb84862fcChristian MaedereqExp :: EXP -> EXP -> Bool
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedereqExp Type Type = True
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedereqExp (Const x1) (Const x2) = x1 == x2
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedereqExp (Var x1) (Var x2) = x1 == x2
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedereqExp (Appl f1 [a1]) (Appl f2 [a2]) = and [f1 == f2, a1 == a2]
aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaedereqExp (Func [t1] s1) (Func [t2] s2) = and [t1 == t2, s1 == s2]
caf021dd48c90ff6b26117f13e1d8c0ef1ca618aChristian MaedereqExp (Pi [(n1,t1)] s1) (Pi [(n2,t2)] s2) =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let vars = Set.delete n1 $ getFreeVars s1
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski vars1 = Set.delete n2 $ getFreeVars s2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in if (vars1 /= vars)
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder else let s3 = rename (Map.singleton n2 n1) (Set.insert n1 vars) s2
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder in and [t1 == t2, s1 == s3]
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaedereqExp (Lamb [(n1,t1)] s1) (Lamb [(n2,t2)] s2) =
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder let vars = Set.delete n1 $ getFreeVars s1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder vars1 = Set.delete n2 $ getFreeVars s2
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder in if (vars1 /= vars)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder else let s3 = rename (Map.singleton n2 n1) (Set.insert n1 vars) s2
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder in and [t1 == t2, s1 == s3]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedereqExp _ _ = False
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- tests for inclusion of signatures
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederisSubsig :: Sign -> Sign -> Bool
44d2a211a352759ee988ed8353026f5fa9511209Christian MaederisSubsig (Sign _ _ ds1) (Sign _ _ ds2) =
44d2a211a352759ee988ed8353026f5fa9511209Christian Maeder Set.isSubsetOf (Set.fromList ds1) (Set.fromList ds2)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- constructs the union of two signatures
4fc727afa544a757d1959ce77c02208f8bf330dcChristian MaedersigUnion :: Sign -> Sign -> Result Sign
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersigUnion sig1 sig2 = return $
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder foldl (\ sig d@(Def s t v) ->
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder if (isConstant s sig)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder then let Just t1 = getSymType s sig
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder v1 = getSymValue s sig
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder in if (t == t1 && v == v1) then sig else
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder error $ conflictDefsError s
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else addDef d sig
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder ) sig1 $ getDefs sig2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- constructs the intersection of two signatures
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersigIntersection :: Sign -> Sign -> Result Sign
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedersigIntersection sig1 sig2 = do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let defs1 = Set.fromList $ getDefs sig1
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let defs2 = Set.fromList $ getDefs sig2
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder let defs = Set.difference defs1 defs2
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder let syms = Set.map getSym defs
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder coGenSig syms sig1
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder-- constructs the signature generated by the specified symbol set
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian MaedergenSig :: Set.Set Symbol -> Sign -> Result Sign
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaedergenSig syms sig = do
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder let syms' = inclSyms syms sig
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let defs' = filter (\ d -> Set.member (getSym d) syms') $ getDefs sig
74d9a385499bf903b24848dff450a153f525bda7Christian Maeder return $ Sign gen_base gen_module defs'
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederinclSyms :: Set.Set Symbol -> Sign -> Set.Set Symbol
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederinclSyms syms sig =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski foldl (\ syms' (Def s t v) ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder if (Set.notMember s syms') then syms' else
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let syms1 = getConstants t
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder syms2 = case v of
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Just v' -> getConstants v'
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ) syms $ reverse $ getDefs sig
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- constructs the signature cogenerated by the specified symbol set
5e46b572ed576c0494768998b043d9d340594122Till MossakowskicoGenSig :: Set.Set Symbol -> Sign -> Result Sign
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian MaedercoGenSig syms sig = trace (show syms) $ do
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder let syms' = exclSyms syms sig
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder let defs' = filter (\ d -> Set.notMember (getSym d) syms') $ getDefs sig
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder return $ Sign gen_base gen_module defs'
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian MaederexclSyms :: Set.Set Symbol -> Sign -> Set.Set Symbol
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian MaederexclSyms syms sig =
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder foldl (\ syms' (Def s t v) ->
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder if (Set.member s syms') then syms' else
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder let syms1 = getConstants t
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder syms2 = case v of
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder Just v' -> getConstants v'
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder diff = Set.intersection syms' $ Set.union syms1 syms2
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder in if (Set.null diff) then syms' else Set.insert s syms'
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder ) syms $ getDefs sig
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder--------------------------------------------------------------------
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder---------------------------------------------------------------------
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- ERROR MESSAGES
d058429727dd696a0327cdc28cadd268c34c36baChristian MaederconflictDefsError :: Symbol -> String
d058429727dd696a0327cdc28cadd268c34c36baChristian MaederconflictDefsError s =
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder "Symbol " ++ (show $ pretty s) ++ " has conflicting declarations " ++
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder "in the signature union and hence the union is not defined."