{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
module Data.Logic.ATP.Formulas
( IsAtom
, IsFormula(AtomOf, true, false, asBool, atomic, overatoms, onatoms)
, (⊥), (⊤)
, fromBool
, prettyBool
, atom_union
) where
import Data.Logic.ATP.Pretty (Doc, HasFixity, Pretty, text)
import Data.Set as Set (Set, empty, union)
import Prelude hiding (negate)
class (Ord atom, Show atom, HasFixity atom, Pretty atom) => IsAtom atom
class (Pretty formula, HasFixity formula, IsAtom (AtomOf formula)) => IsFormula formula where
type AtomOf formula
true :: formula
false :: formula
asBool :: formula -> Maybe Bool
atomic :: AtomOf formula -> formula
overatoms :: (AtomOf formula -> r -> r) -> formula -> r -> r
onatoms :: (AtomOf formula -> AtomOf formula) -> formula -> formula
(⊤) :: IsFormula p => p
⊤ :: forall p. IsFormula p => p
(⊤) = p
forall p. IsFormula p => p
true
(⊥) :: IsFormula p => p
⊥ :: forall p. IsFormula p => p
(⊥) = p
forall p. IsFormula p => p
false
fromBool :: IsFormula formula => Bool -> formula
fromBool :: forall formula. IsFormula formula => Bool -> formula
fromBool Bool
True = formula
forall p. IsFormula p => p
true
fromBool Bool
False = formula
forall p. IsFormula p => p
false
prettyBool :: Bool -> Doc
prettyBool :: Bool -> Doc
prettyBool Bool
True = String -> Doc
text String
"⊤"
prettyBool Bool
False = String -> Doc
text String
"⊥"
atom_union :: (IsFormula formula, Ord r) => (AtomOf formula -> Set r) -> formula -> Set r
atom_union :: forall formula r.
(IsFormula formula, Ord r) =>
(AtomOf formula -> Set r) -> formula -> Set r
atom_union AtomOf formula -> Set r
f formula
fm = (AtomOf formula -> Set r -> Set r) -> formula -> Set r -> Set r
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r. (AtomOf formula -> r -> r) -> formula -> r -> r
overatoms (\AtomOf formula
h Set r
t -> Set r -> Set r -> Set r
forall a. Ord a => Set a -> Set a -> Set a
Set.union (AtomOf formula -> Set r
f AtomOf formula
h) Set r
t) formula
fm Set r
forall a. Set a
Set.empty