module Data.Logic.Classes.Constants
( Constants(asBool, fromBool)
, ifElse
, true
, (⊨)
, false
, (⊭)
, prettyBool
) where
import Data.Logic.Classes.Pretty (Pretty(pretty))
import Text.PrettyPrint (Doc, text)
class Constants p where
asBool :: p -> Maybe Bool
fromBool :: Bool -> p
true :: Constants p => p
true = fromBool True
false :: Constants p => p
false = fromBool False
ifElse :: a -> a -> Bool -> a
ifElse t _ True = t
ifElse _ f False = f
(⊨) :: Constants formula => formula
(⊨) = true
(⊭) :: Constants formula => formula
(⊭) = false
prettyBool :: Bool -> Doc
prettyBool True = text "⊨"
prettyBool False = text "⊭"
instance Pretty Bool where
pretty = prettyBool