content: {- |
  Module      :  ./CSL/BoolBasic.hs
  Description :  Some basic types for simple boolean representations
  Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  ewaryst.schulz@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  This module defines some basic types for a simple boolean representation and
  a printer which outputs this representation into an s-expression like format.
  This is mainly for communication with the smt-solver yices.
   -}
  
  module CSL.BoolBasic where
  
  import Data.List
  {- ----------------------------------------------------------------------
  General Datatypes for Extended Parameters
  ---------------------------------------------------------------------- -}
  
  data BoolRep = Not BoolRep | Impl BoolRep BoolRep | And [BoolRep]
               | Or [BoolRep] | Pred String [String]
  
  
  trueBool :: BoolRep
  trueBool = Pred "true" []
  
  falseBool :: BoolRep
  falseBool = Pred "false" []
  
  mapPred :: (String -> [String] -> BoolRep) -> BoolRep -> BoolRep
  mapPred f br =
      case br of
        Not x -> Not $ mapPred f x
        Impl x y -> Impl (mapPred f x) $ mapPred f y
        And l -> And $ map (mapPred f) l
        Or l -> Or $ map (mapPred f) l
        Pred s l -> f s l
  
  {- ----------------------------------------------------------------------
  Output for SMT
  ---------------------------------------------------------------------- -}
  
  
  smtBoolExp :: BoolRep -> String
  smtBoolExp br = let f s = g s smtBoolExp
                      g s _ [] = s
                      g s h l = concat ["(", unwords $ s : map h l, ")"]
                  in case br of
                       Not b -> f "not" [b]
                       Impl b1 b2 -> f "=>" [b1, b2]
                       And l -> f "and" l
                       Or l -> f "or" l
                       Pred s l -> g s id l
  