{- |
Module : ./Propositional/Tools.hs
Description : Some additional helper functions
Copyright : (c) Dominik Luecke, Uni Bremen 2007
License : GPLv2 or higher, see LICENSE.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : experimental
Portability : non-portable (imports Logic.Logic)
Some helper functions for Propositional Logic
-}
{-
Ref.
Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
What is a Logic?.
In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
2005.
-}
module Propositional.Tools
( flatten -- "flattening" of specs
, flattenDis -- "flattening" of disjunctions
) where
{- | the flatten functions use associtivity to "flatten" the syntax
tree of the formulae.
flatten \"flattens\" formulae under the assumption of the
semantics of basic specs, this means that we put each
\"clause\" into a single formula for CNF we really will obtain
clauses. -}
flatten :: FORMULA -> [FORMULA]
flatten f = case f of
Conjunction fs _ -> concatMap flatten fs
_ -> [f]
-- | "flattening" for disjunctions
flattenDis :: FORMULA -> [FORMULA]
flattenDis f = case f of
Disjunction fs _ -> concatMap flattenDis fs
_ -> [f]