Analysis.hs revision 44eca622a16639b4a1a3d4fd088c7c3bfff89b8e
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederDescription : Static Analysis for EnCL
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Dominik Dietrich, Ewaryst Schulz, DFKI Bremen 2010
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Ewaryst.Schulz@dfki.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : experimental
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPortability : portable
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederStatic Analysis for EnCL including elimination procedure for extended parameters
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder{- ( splitSpec
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , basicCSLAnalysis
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , Guarded(..)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , dependencySortAS
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , getDependencyRelation
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , epElimination
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , topsortDirect
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- basicCSLAnalysis
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- ,mkStatSymbItems
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- ,mkStatSymbMapItem
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- ,inducedFromMorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- ,inducedFromToMorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- , signatureColimit
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport Common.Utils (mapAccumLM)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Data.Tree as Tr
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Data.Set as Set
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maederimport qualified Data.Map as Map
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- * Diagnosis Types and Functions
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder-- | generates a named formula
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederwithName :: Annoted CMD -> Int -> Named CMD
351391e0e3226210e7ffb183b334da9f96de36eaChristian MaederwithName f i = (makeNamed (if label == "" then "Ax_" ++ show i
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder else label) $ item f)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder { isAxiom = not isTheorem }
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder label = getRLabel f
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder annos = r_annos f
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder isImplies' = foldl (\ y x -> isImplies x || y) False annos
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder isImplied' = foldl (\ y x -> isImplied x || y) False annos
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder isTheorem = isImplies' || isImplied'
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder-- | takes a signature and a formula and a number.
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder-- It analyzes the formula and returns a formula with diagnosis
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederanalyzeFormula :: Sign.Sign -> (Annoted CMD) -> Int -> Result (Named CMD)
5e46b572ed576c0494768998b043d9d340594122Till MossakowskianalyzeFormula _ f i =
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang return $ withName f{ item = staticUpdate $ item f } i
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-- | Extracts the axioms and the signature of a basic spec
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian MaedersplitSpec :: BASIC_SPEC -> Sign.Sign -> Result (Sign.Sign, [Named CMD])
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangsplitSpec (Basic_spec specitems) sig =
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder ((newsig, _), mNCmds) <- mapAccumLM anaBasicItem (sig, 0) specitems
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return (newsig, catMaybes mNCmds)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskianaBasicItem :: (Sign.Sign, Int) -> Annoted BASIC_ITEM
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder -> Result ((Sign.Sign, Int), Maybe (Named CMD))
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederanaBasicItem (sign, i) itm =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case item itm of
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder Op_decl (Op_item tokens _) -> return ((addTokens sign tokens, i), Nothing)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder Var_decls l -> return ((addVarDecls sign l, i), Nothing)
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Axiom_item annocmd ->
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich ncmd <- analyzeFormula sign annocmd i
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return ((sign, i+1), Just ncmd)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | adds the specified tokens to the signature
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederaddTokens sign tokens = let f res itm = addToSig res (simpleIdToId itm)
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder $ optypeFromArity 0
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in foldl f sign tokens
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | adds the specified var items to the signature
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederaddVarDecls :: Sign.Sign -> [VAR_ITEM] -> Sign.Sign
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederaddVarDecls sign vitems = foldl f sign vitems where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder f res (Var_item toks dom _) = addVarItem res toks dom
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder{- | stepwise extends an initially empty signature by the basic spec bs.
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder The resulting spec contains analyzed axioms in it. The result contains:
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder (1) the basic spec
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder (2) the new signature + the added symbols
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder (3) sentences of the spec
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederbasicCSLAnalysis :: (BASIC_SPEC, Sign, a)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaederbasicCSLAnalysis (bs, sig, _) =
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder (newSig, ncmds) <- splitSpec bs sig
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder $ Map.difference (items newSig) $ items sig
e6dccba746efe07338d3107fed512e713fd50b28Christian Maeder return (bs, ExtSign newSig newSyms, ncmds)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder-- | A function which regroups all updates on a CMD during the static analysis.
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederstaticUpdate :: CMD -> CMD
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederstaticUpdate = handleFunAssignment . handleBinder
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder-- | Replaces the function-arguments in functional assignments by variables.
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaederhandleFunAssignment :: CMD -> CMD
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaederhandleFunAssignment (Ass (Op f epl al@(_:_) rg) e) =
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder let (env, al') = varSet al in Ass (Op f epl al' rg) $ constsToVars env e
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederhandleFunAssignment x = x
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder{- | If element x is at position i in the first list and there is an entry (i,y)
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder in the second list then the resultlist has element y at position i. All
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder positions not mentioned by the second list have identical values in the first
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder and the result list.
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaederreplacePositions :: [a] -> [(Int, a)] -> [a]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederreplacePositions l posl =
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder let f (x, _) (y, _) = compare x y
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -- the actual merge function
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder g _ l' [] = l'
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder g _ [] _ = error "replacePositions: positions left for replacement"
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder g i (a:l1) l2'@((j,b):l2) =
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder if i == j then b:g (i+1) l1 l2 else a:g (i+1) l1 l2'
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder -- works only if the positions are in ascending order
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder in g 0 l $ sortBy f posl
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | Replaces the binding-arguments in binders by variables.
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederhandleBinder :: CMD -> CMD
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederhandleBinder cmd =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder let substBinderArgs bvl bbl args =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -- compute the var set from the given positions
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let (vs, vl) = varSet $ map (args!!) bvl
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- compute the substituted bodyexpressionlist
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder bl = map (constsToVars vs . (args!!)) bbl
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder in replacePositions args $ zip (bvl ++ bbl) $ vl ++ bl
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder { foldAss = \ cmd' _ def ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder -- we do not want to recurse into the left hand side hence
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -- we take the original value
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Ass c _ -> Ass c def
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder _ -> error "handleBinder: impossible case"
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder , foldOp = \ _ s epl' args rg' ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case lookupBindInfo s $ length args of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Just (BindInfo bvl bbl) ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Op s epl' (substBinderArgs bvl bbl args) rg'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> Op s epl' args rg'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , foldList = \ _ l rg' -> List l rg'
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder in foldCMD substRec cmd
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- | Transforms Op-Expressions to a set of op-names and a Var-list
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedervarSet :: [EXPRESSION] -> (Set.Set String, [EXPRESSION])
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder let opToVar' s (Op v _ _ rg') =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Set.insert (show v) s, Var Token{ tokStr = show v, tokPos = rg' })
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder opToVar' _ x =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder error $ "varSet: not supported varexpression " ++ show x
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in mapAccumL opToVar' Set.empty l
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- | Replaces Op occurrences to Var if the op is in the given set
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederconstsToVars :: Set.Set String -> EXPRESSION -> EXPRESSION
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederconstsToVars env e =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let substRec =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder \ _ s epl' args rg' ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if Set.member (show s) env then
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder then Var (Token { tokStr = show s, tokPos = rg' })
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder else error $ "constsToVars: variable must not have"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ++ " arguments:" ++ show args
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else Op s epl' args rg'
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder , foldList = \ _ l rg' -> List l rg'
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder in foldTerm substRec e
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- * Utils for 'CMD' and 'EXPRESSION'
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaedersubAssignments :: CMD -> [(EXPRESSION, EXPRESSION)]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaedersubAssignments = foldCMD listCMDRecord{ foldAss = \ _ c def -> [(c, def)] }
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- * Further analysis in order to run this specification
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz-- ** Datatypes and guarded definitions
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder{- TODO: we want to proceed here as follows:
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz 1. split the definitions and the program and process the extended parameters
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder 2. build the dependency relation ( and store it in the signature ?)
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder Not checked is:
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder 1. if all defined symbols have the same arity
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- | A guard consists of the guard range and the corresponding expression
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- together with a name, a set of not propagated parameters and a set of
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder-- constrained parameters (in the extended parameter specification)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulzdata Guard a = Guard { range :: a
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz , definition :: EXPRESSION
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz , assName :: String
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz , filtered :: Set.Set String
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz , constrained :: Set.Set String }
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederprettyGuard :: (a -> Doc) -> Guard a -> Doc
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederprettyGuard f g = f (range g) <+> text "-->" <+> pretty (definition g)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maederinstance Functor Guard where
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder fmap f (Guard x e an fs ct) = Guard (f x) e an fs ct
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederinstance Pretty a => Pretty (Guard a) where
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder pretty = prettyGuard pretty
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederinstance Pretty a => Show (Guard a) where
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder show = show . pretty
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder-- | A guarded constant consists of the argument list (for function definitions)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder-- and a list of guard-expressions
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederdata Guarded a = Guarded { argvars :: [String]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder , guards :: [Guard a] }
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder{- Comment it in if needed later
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaederundefinedGuard :: String -> a -> Guard a
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederundefinedGuard s x = Guard { range = x
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder , definition = err
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder , assName = err
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder , filtered = err
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder , constrained = err }
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder where err = error $ "undefinedGuard: " ++ s
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaederundefinedGuarded :: String -> a -> Guarded a
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaederundefinedGuarded s x = Guarded { argvars = []
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder , guards = [undefinedGuard s x] }
568da6120906d5283c4322114eee10f24ea8dd6dChristian MaederprettyGuarded :: (a -> Doc) -> Guarded a -> Doc
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian MaederprettyGuarded f grdd = vcat $ map (prettyGuard f) $ guards grdd
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederinstance Functor Guarded where
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder fmap f grdd = grdd { guards = map (fmap f) $ guards grdd }
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maederinstance Pretty a => Pretty (Guarded a) where
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder pretty = prettyGuarded pretty
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maederinstance Pretty a => Show (Guarded a) where
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder show = show . pretty
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maederinstance Pretty EPRange where
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder pretty = prettyEPRange
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maedertype GuardedMap a = Map.Map String (Guarded a)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederaddAssignment :: String -> EXPRESSION -> EXPRESSION -> GuardedMap [EXTPARAM]
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -> GuardedMap [EXTPARAM]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiaddAssignment n (Op (OpUser s) epl al _) def m =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let f (Var tok) = tokStr tok
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder f x = error $ "addAssignment: not a variable " ++ show x
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder combf x y | argvars x == argvars y = y { guards = guards y ++ guards x }
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder | otherwise =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder error "addAssignment: the argument vars does not match."
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder grd = Guarded (map f al) [uncurry (Guard epl def n)
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder $ filteredConstrainedParams epl]
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder in Map.insertWith combf (show s) grd m
99476ac2689c74251219db4782e57fe713a24a52Christian MaederaddAssignment _ x _ _ = error $ "unexpected assignment " ++ show x
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder 1. analysis for missing definitions and undeclared extparams
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder 2. Integrating extparam domain definitions
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder 3. check for each constant if the Guards exhaust the extparam domain (in splitAS)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- | Splits the Commands into the AssignmentStore and a program sequence
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaedersplitAS :: [Named CMD] -> (GuardedMap [EXTPARAM], [Named CMD])
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let f nc (m,l) = case sentence nc of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Ass c def -> (addAssignment (senAttr nc) c def m, l)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ -> (m, nc:l)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder in foldr f (Map.empty, []) cl
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder-- | Transforms the old guards where inclusion overlapping was allowed into
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder-- disjoint new guards.
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaederanalyzeGuarded :: Guarded [EXTPARAM] -> Guarded EPRange
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian MaederanalyzeGuarded x =
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder let f grd = (grd, toEPExps $ range grd)
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder -- builds a forest mirroring the inclusion relation of the guard ranges
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder frst = forestFromEPs f $ guards x
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- compute the new range information with the disjointness property
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let nodeRg = Atom $ eplabel rl
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder newRg = case map (Atom . eplabel . Tr.rootLabel) sf of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- we make nodeRg disjoint with its children
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- by removing the union of the children from it
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder rgl -> if isStarEP (eplabel rl)
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder then Complement $ mkUnion rgl
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder else Intersection
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder [nodeRg, Complement $ mkUnion rgl]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in (nodelabel rl) { range = newRg } : l
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder newguards = foldForest g [] frst
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder in x { guards = newguards }
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder-- | Folds the forest in top-down direction constructing the accumulator
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- from the labels and children of each node.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskifoldForest :: (b -> a -> Tr.Forest a -> b) -> b -> Tr.Forest a -> b
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederfoldForest f = foldl g where
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder g x tr = let sf = Tr.subForest tr
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in foldl g (f x (Tr.rootLabel tr) sf) sf
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- ** Dependency Sorting
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-- | Returns a dependency sorted list of constants with their guarded
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- definitions. Requires as input an analyzed Assignment store:
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- @(fmap analyzeGuarded . fst . splitAS)@ produces an adequate input.
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederdependencySortAS :: GuardedMap EPRange -> [(String, Guarded EPRange)]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederdependencySortAS grdm = mapMaybe f $ topsortDirect $ getDependencyRelation grdm
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder where f x = fmap ((,) x) $ Map.lookup x grdm
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedertype BackRef a = Map.Map a [a]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | @r dependsOn r'@ if @r'@ occurs in the definition term of @r@. In this case
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- the set which corresponds to the 'Map.Map' entry of @r@ contains @r'@.
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetDependencyRelation :: GuardedMap a -> Rel2 String
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetDependencyRelation gm = Map.fold f dr dr where
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder $ map (flip (,) Set.empty) $ Set.toAscList s
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder g grdd = Set.unions $ map (setOfUserDefined . definition) $ guards grdd
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetBackRef :: Ord a => Rel2 a -> BackRef a
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedergetBackRef d =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let uf k n m = Map.insertWith (++) n [k] m
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- for each entry in the set insert k into the list
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder f k s m = Set.fold (uf k) m s
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- from each entry in d add entries in the map
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedertopsortDirect :: (Show a, Ord a) => Rel2 a -> [a]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedertopsortDirect d = topsort d $ getBackRef d
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | This function is based on the Kahn-algorithm. It requires a representation
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder-- of a relation which has for each entry of the domain an entry in the map.
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder-- E.g., 1 |-> {2}, 2 |-> {3, 4} is not allowed because the entries
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- 3 |-> {}, 4 |-> {} are missing
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedertopsort :: (Show a, Ord a) => Rel2 a -> BackRef a -> [a]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maedertopsort d br =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let f d' acc []
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder | otherwise =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let (s, v) = Map.findMin d'
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in error $ concat [ "topsort: Dependency relation contains cycles "
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder , show s, " -> ", show v ]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder f d' acc (n:l) =
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (nl, d'') = foldl (remEdge n) ([], d') cl
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in f d'' (acc ++ [n]) $ l ++ nl
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder uf n a = let b = Set.delete n a in if Set.null b then Nothing else Just b
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -- returns a new list of empty-nodes and a new def-map
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder remEdge n (nl, m) s = let c = Map.size m
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder m' = Map.update (uf n) s m
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in (if Map.size m' < c then s:nl else nl, m')
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder in f mne [] $ Map.keys me
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- ** Extended Parameter Elimination
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Given a dependency ordered list of constant definitions we compute all
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder definitions not depending on extended parameter propagation, therefore
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder eliminating them. For each constant we produce probably many new constants
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder that we call elim-constants. The definition of elim-constant N can be
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder looked up in @(guards x)!!N@.
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederepElimination :: CompareIO m => [(String, Guarded EPRange)]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> m [(String, Guarded EPRange)]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederepElimination = f Map.empty
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -- for efficient lookup, we build a map in addition to the list containing
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -- the same information
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder f _ [] = return []
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder f m ((s, g):l) = do
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder newguards <- liftM concat $ mapM (eliminateGuard m) $ guards g
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let g' = g{ guards = newguards }
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder liftM ((s, g') :) $ f (Map.insert s g' m) l
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder The given map already contains only elim-constants. We extract the
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (partly instantiated) constants from the definition in the guard and
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder create a partition from their guarded entry in the map. We use
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder 'refineDefPartitions' to create the refinement and from this we produce
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder the new guards.
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedereliminateGuard :: CompareIO m => GuardedMap EPRange -> Guard EPRange
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -> m [Guard EPRange]
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedereliminateGuard m grd = do
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder let f s epl _ = restrictPartition (range grd)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just grdd -> partitionFromGuarded epl grdd
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Nothing -> AllPartition 0
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder h pim = foldTerm passRecord{ foldOp = const $ mappedElimConst pim }
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder $ definition grd
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder g (er, pim) = grd{ range = er, definition = h pim }
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder logMessage $ "eliminating Guard " ++ assName grd
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder partMap <- mapUserDefined f $ definition grd
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder rePart <- refineDefPartitions partMap
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder case rePart of
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder AllPartition x -> return [g (range grd, x)]
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder Partition l ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- for each entry in the refined partition create a new guard
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski return $ map g l
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder-- | Helper function of 'eliminateGuard' for substitution of operatornames
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder-- by mapped entries given in the @'Map.Map' 'PIConst' 'Int'@.
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaedermappedElimConst :: (Map.Map PIConst Int)
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder -> OPID -- ^ the original operator id
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -> [EXTPARAM] -- ^ the extended parameter instantiation
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder -> [EXPRESSION] -- ^ the new arguments
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder -> Range -- ^ the original range
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -> EXPRESSION
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedermappedElimConst m oi e al rg = Op newOi [] al rg
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder where err = error $ "mappedElimConst: No entry for " ++ show oi
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder f c = Map.findWithDefault err (mkPIConst (show c) e) m
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder newOi = case oi of
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder OpUser c -> OpUser $ toElimConst c $ f c
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder-- | Returns the simplified partition representation of the 'Guarded' object
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder-- probably instantiated by the provided extended parameter list.
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaederpartitionFromGuarded :: [EXTPARAM] -> Guarded EPRange -> Partition Int
4072adb8c5d2c86123e8e1c1918263968f187829Christian MaederpartitionFromGuarded epl grdd =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder -- it is crucial here that the zipping takes place with the original guard
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder -- list, otherwise the indexes doesn't match their definitions
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder Partition $ mapMaybe f $ zip (guards grdd) [0..] where
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ep = toEPExps epl
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder f (a, b) | null epl = Just (range a, b)
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder | otherwise = case projectRange ep $ range a of
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Empty -> Nothing
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder x -> Just (x, b)
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder-- | A partially instantiated constant
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maedertype PIConst = (String, Maybe EPExps)
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaedermkPIConst :: String -> [EXTPARAM] -> PIConst
5e46b572ed576c0494768998b043d9d340594122Till MossakowskimkPIConst s epl = (s, if null epl then Nothing else Just $ toEPExps epl)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- | Returns a map of user defined (partially instantiated) constants
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- to the result of this constant under the given function.
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedermapUserDefined :: Monad m => (String -> [EXTPARAM] -> [EXPRESSION] -> m a)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> EXPRESSION -> m (Map.Map PIConst a)
5e46b572ed576c0494768998b043d9d340594122Till MossakowskimapUserDefined f e = g Map.empty e
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Op (OpUser s) epl al _ -> do
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder v <- f (show s) epl al
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder let pic = mkPIConst (show s) epl
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder foldM g m' al
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder -- handle also non-userdefined ops.
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder Op _ _ al _ -> foldM g m al
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder -- ignoring lists (TODO: they should be removed soon anyway)
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder _ -> return m
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder-- | Returns a set of user defined constants ignoring instantiation.
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaedersetOfUserDefined :: EXPRESSION -> Set.Set String
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaedersetOfUserDefined e = g Set.empty e
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder Op (OpUser n) _ al _ -> foldl g (Set.insert (show n) s) al
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder -- handle also non-userdefined ops.
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder Op _ _ al _ -> foldl g s al
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder -- ignoring lists (TODO: they should be removed soon anyway)
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder Given a map holding for each constant, probably partly instantiated,
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder a partition labeled by the corresponding elim-constants we build a
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder partition which refines each of the given partitions labeled by a mapping
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder of partly instantiated constants to the corresponding elim-constant
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrefineDefPartitions :: CompareIO m => Map.Map PIConst (Partition Int)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder -> m (Partition (Map.Map PIConst Int))
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrefineDefPartitions =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder foldM refineDefPartition (AllPartition Map.empty) . Map.toList
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederrefineDefPartition :: CompareIO m => Partition (Map.Map PIConst Int)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder -> (PIConst, Partition Int)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder -> m (Partition (Map.Map PIConst Int))
d058429727dd696a0327cdc28cadd268c34c36baChristian MaederrefineDefPartition pm (c, ps) = do
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder logMessage $ "refining partition for " ++ show c
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski liftM (fmap $ uncurry $ Map.insert c) $ refinePartition ps pm
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder-- * Various Outputs of Guarded Assignments
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | All in the given AssignmentStore undefined constants
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian MaederundefinedConstants :: GuardedMap a -> Set.Set String
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian MaederundefinedConstants gm =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder $ Map.difference (Map.filter Set.null $ getDependencyRelation gm) gm
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- | Turn the output of the elimination procedure into single (unguarded)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- (probably functional) definitions. Respects the input order of the list.
2feea92963a4b1b7482a4b72ee85148d842d9ad6Christian MaedergetElimAS :: [(String, Guarded EPRange)] ->
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder [(ConstantName, AssDefinition)]
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedergetElimAS = concatMap f where
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder f (s, grdd) = zipWith (g s $ argvars grdd) [0..] $ guards grdd
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder g s args i grd = (ElimConstant s i, mkDefinition args $ definition grd)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-- | The elim-constant to 'EPRange' mapping.
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederelimConstants :: [(String, Guarded EPRange)] ->
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder [(String, Map.Map ConstantName EPRange)]
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaederelimConstants = map f where
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder f (s, grdd) = (s, Map.fromList $ zipWith (g s) [0..] $ guards grdd)
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder g s i grd = (ElimConstant s i, range grd)