{- |
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.

  http://en.wikipedia.org/wiki/Propositional_logic

  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

import Propositional.AS_BASIC_Propositional

{- | 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 :: FORMULA -> [FORMULA]
flatten f :: FORMULA
f = case FORMULA
f of
      Conjunction fs :: [FORMULA]
fs _ -> (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FORMULA -> [FORMULA]
flatten [FORMULA]
fs
      _ -> [FORMULA
f]

-- | "flattening" for disjunctions
flattenDis :: FORMULA -> [FORMULA]
flattenDis :: FORMULA -> [FORMULA]
flattenDis f :: FORMULA
f = case FORMULA
f of
      Disjunction fs :: [FORMULA]
fs _ -> (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FORMULA -> [FORMULA]
flattenDis [FORMULA]
fs
      _ -> [FORMULA
f]