Fold.hs revision ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : folding function for propositional formulas
f11f713bebd8e1e623a0a4361065df256033de47Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
967e5f3c25249c779575864692935627004d3f9eChristian MaederStability : provisional
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederPortability : portable
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederfolding and simplification of propositional formulas
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maederdata FoldRecord a = FoldRecord
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder { foldNegation :: a -> Range -> a
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder , foldConjunction :: [a] -> Range -> a
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder , foldDisjunction :: [a] -> Range -> a
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder , foldImplication :: a -> a -> Range -> a
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder , foldEquivalence :: a -> a -> Range -> a
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , foldTrue_atom :: Range -> a
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , foldFalse_atom :: Range -> a
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , foldPredication :: Token -> a }
967e5f3c25249c779575864692935627004d3f9eChristian MaederfoldFormula :: FoldRecord a -> FORMULA -> a
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian MaederfoldFormula r frm = case frm of
78eeae099616e255ccf2e5f9122387bb10c68338Christian Maeder Negation f n -> foldNegation r (foldFormula r f) n
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Conjunction xs n -> foldConjunction r (map (foldFormula r) xs) n
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Disjunction xs n -> foldDisjunction r (map (foldFormula r) xs) n
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Implication x y n -> foldImplication r (foldFormula r x) (foldFormula r y) n
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Equivalence x y n -> foldEquivalence r (foldFormula r x) (foldFormula r y) n
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder True_atom n -> foldTrue_atom r n
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder False_atom n -> foldFalse_atom r n
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder Predication x -> foldPredication r x
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian MaedermapRecord :: FoldRecord FORMULA
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedermapRecord = FoldRecord
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder { foldNegation = Negation
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , foldConjunction = Conjunction
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , foldDisjunction = Disjunction
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , foldImplication = Implication
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , foldEquivalence = Equivalence
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder , foldTrue_atom = True_atom
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , foldFalse_atom = False_atom
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , foldPredication = Predication }
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maedersimplify :: FORMULA -> FORMULA
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maedersimplify = foldFormula mapRecord
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder { foldNegation = \ f n -> case f of
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder True_atom p -> False_atom p
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder False_atom p -> True_atom p
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Negation g _ -> g
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder s -> Negation s n
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder , foldConjunction = \ xs n -> case xs of
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder [] -> True_atom n
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder ls = concatMap (\ f -> case f of
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder Conjunction ys _ -> ys
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder in if any is_False_atom ls then False_atom n else Conjunction ls n
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , foldDisjunction = \ xs n -> case xs of
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder [] -> False_atom n
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder ls = concatMap (\ f -> case f of
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder Disjunction ys _ -> ys
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder in if any is_True_atom ls then True_atom n else Disjunction ls n
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , foldImplication = \ x y n -> case x of
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder False_atom p -> True_atom p
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder _ -> if is_True_atom x then y else Implication x y n
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder , foldEquivalence = \ x y n ->
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder if x == y then True_atom n else Equivalence x y n }