Analysis.hs revision 1ac1d44af1a5d0c4a800b689d2afc68826484b06
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederDescription : Abstract syntax for reduce
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) Dominik Dietrich, Ewaryst Schulz, DFKI Bremen 2010
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederMaintainer : Ewaryst.Schulz@dfki.de
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : experimental
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederPortability : portable
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder , basicCSLAnalysis
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-- basicCSLAnalysis
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- ,mkStatSymbItems
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- ,mkStatSymbMapItem
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- ,inducedFromMorphism
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- ,inducedFromToMorphism
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- , signatureColimit
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederimport Common.Utils (mapAccumLM)
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederimport qualified Data.Set as Set
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederimport qualified Data.Map as Map
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- * Diagnosis Types and Functions
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- | generates a named formula
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederwithName :: Annoted CMD -> Int -> Named CMD
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaederwithName f i = (makeNamed (if label == "" then "Ax_" ++ show i
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder else label) $ item f)
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder { isAxiom = not isTheorem }
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder label = getRLabel f
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder annos = r_annos f
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder isImplies' = foldl (\ y x -> isImplies x || y) False annos
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder isImplied' = foldl (\ y x -> isImplied x || y) False annos
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder isTheorem = isImplies' || isImplied'
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder-- | takes a signature and a formula and a number.
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- It analyzes the formula and returns a formula with diagnosis
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederanalyzeFormula :: Sign.Sign -> (Annoted CMD) -> Int -> Result (Named CMD)
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederanalyzeFormula _ f i =
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder return $ withName f{ item = staticUpdate $ item f } i
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder{- TODO: we want to proceed as follows:
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder 1. Extract the operators from the definitions and store their arity in the optype
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder 2. Check if all applications are valid w.r.t. the arity
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder 3. compute the variables as is done by staticUpdate
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder 4. split the definitions and the program and process the extended parameters
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder 5. handle conditional assignments
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder 6. build the dependency relation and store it in the signature
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder-- | Extracts the axioms and the signature of a basic spec
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedersplitSpec :: BASIC_SPEC -> Sign.Sign -> Result (Sign.Sign, [Named CMD])
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian MaedersplitSpec (Basic_spec specitems) sig =
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder ((newsig, _), mNCmds) <- mapAccumLM anaBasicItem (sig, 0) specitems
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder return (newsig, catMaybes mNCmds)
37e2067019ef1e30bc7ad98b9bc623aa41cfa980Christian MaederanaBasicItem :: (Sign.Sign, Int) -> Annoted BASIC_ITEM
37e2067019ef1e30bc7ad98b9bc623aa41cfa980Christian Maeder -> Result ((Sign.Sign, Int), Maybe (Named CMD))
37e2067019ef1e30bc7ad98b9bc623aa41cfa980Christian MaederanaBasicItem acc@(sign, i) itm =
37e2067019ef1e30bc7ad98b9bc623aa41cfa980Christian Maeder case item itm of
37e2067019ef1e30bc7ad98b9bc623aa41cfa980Christian Maeder Op_decl (Op_item tokens _) -> return ((addTokens sign tokens, i), Nothing)
37e2067019ef1e30bc7ad98b9bc623aa41cfa980Christian Maeder Var_decls _ -> return (acc, Nothing) -- TODO: implement
37e2067019ef1e30bc7ad98b9bc623aa41cfa980Christian Maeder Axiom_item annocmd ->
37e2067019ef1e30bc7ad98b9bc623aa41cfa980Christian Maeder ncmd <- analyzeFormula sign annocmd i
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder return ((sign, i+1), Just ncmd)
f0742398d4587242b1a115de113cd17f63dcb6d0Christian Maeder-- | adds the specified tokens to the signature
d0fc60b7507b34c721c032c49dede882509e8de5Christian MaederaddTokens :: Sign.Sign -> [Token] -> Sign.Sign
d0fc60b7507b34c721c032c49dede882509e8de5Christian MaederaddTokens sign tokens = let f res itm = addToSig res (simpleIdToId itm)
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder $ optypeFromArity 0
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder in foldl f sign tokens
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder{- | stepwise extends an initially empty signature by the basic spec bs.
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder The resulting spec contains analyzed axioms in it. The result contains:
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder (1) the basic spec
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder (2) the new signature + the added symbols
49a475aee8bae6c05798d65fddf13ec6da66f0beChristian Maeder (3) sentences of the spec
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederbasicCSLAnalysis :: (BASIC_SPEC, Sign, a)
51281dddda866c0cda9fca22bf6bc4eea7128112Christian Maeder -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])
51281dddda866c0cda9fca22bf6bc4eea7128112Christian MaederbasicCSLAnalysis (bs, sig, _) =
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder (newSig, ncmds) <- splitSpec bs sig
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder $ Map.difference (items newSig) $ items sig
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder return (bs, ExtSign newSig newSyms, ncmds)
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder-- | A function which regroups all updates on a CMD during the static analysis.
b49276c9f50038e0bd499ad49f7bd6444566a834Christian MaederstaticUpdate :: CMD -> CMD
d0fc60b7507b34c721c032c49dede882509e8de5Christian MaederstaticUpdate = handleFunAssignment . handleBinder
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder-- | Replaces the function-arguments in functional assignments by variables.
d0fc60b7507b34c721c032c49dede882509e8de5Christian MaederhandleFunAssignment :: CMD -> CMD
d0fc60b7507b34c721c032c49dede882509e8de5Christian MaederhandleFunAssignment (Ass (Op f epl al@(_:_) rg) e) =
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder let (env, al') = varSet al in Ass (Op f epl al' rg) $ constsToVars env e
d0fc60b7507b34c721c032c49dede882509e8de5Christian MaederhandleFunAssignment x = x
d0fc60b7507b34c721c032c49dede882509e8de5Christian Maeder-- | If element x is at position i in the first list and there is an entry (i,y)
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder-- in the second list then the resultlist has element y at position i. All non-
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder-- mentioned positions by the second list have identical values in the first
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder-- and the result list.
c71de4012d1bf91340ac64de505fee08d1a7c907Christian MaederreplacePositions :: [a] -> [(Int, a)] -> [a]
c71de4012d1bf91340ac64de505fee08d1a7c907Christian MaederreplacePositions l posl =
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder let f (x, _) (y, _) = compare x y
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder -- the actual merge function
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder g _ l' [] = l'
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder g _ [] _ = error "replacePositions: positions left for replacement"
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder g i (a:l1) l2'@((j,b):l2) =
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder if i == j then b:g (i+1) l1 l2 else a:g (i+1) l1 l2'
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder -- works only if the positions are in ascending order
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder in g 0 l $ sortBy f posl
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder-- | Replaces the binding-arguments in binders by variables.
64558a09e6f6b95d2689d02dd5251339f8ac505bChristian MaederhandleBinder :: CMD -> CMD
c71de4012d1bf91340ac64de505fee08d1a7c907Christian MaederhandleBinder cmd =
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder let substBinderArgs bvl bbl args =
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder -- compute the var set from the given positions
c71de4012d1bf91340ac64de505fee08d1a7c907Christian Maeder let (vs, vl) = varSet $ map (args!!) bvl
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder -- compute the substituted bodyexpressionlist
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder bl = map (constsToVars vs . (args!!)) bbl
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder in replacePositions args $ zip (bvl ++ bbl) $ vl ++ bl
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder { foldAss = \ _ cmd' _ def ->
varSet :: [EXPRESSION] -> (Set.Set String, [EXPRESSION])
(Set.insert (show v) s, Var Token{ tokStr = show v, tokPos = rg' })
in mapAccumL opToVar' Set.empty l
constsToVars :: Set.Set String -> EXPRESSION -> EXPRESSION
if Set.member (show s) env' then