-- | The 'IsFormula' class contains definitions for the boolean true
-- and false values, and methods for traversing the atoms of a formula.

{-# 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)

-- | Basic properties of an atomic formula
class (Ord atom, Show atom, HasFixity atom, Pretty atom) => IsAtom atom

-- | Class associating a formula type with its atom (atomic formula) type.
class (Pretty formula, HasFixity formula, IsAtom (AtomOf formula)) => IsFormula formula where
    type AtomOf formula
    -- ^ AtomOf is a function that maps the formula type to the
    -- associated atomic formula type
    true :: formula
    -- ^ The true element
    false :: formula
    -- ^ The false element
    asBool :: formula -> Maybe Bool
    -- ^ If the arugment is true or false return the corresponding
    -- 'Bool', otherwise return 'Nothing'.
    atomic :: AtomOf formula -> formula
    -- ^ Build a formula from an atom.
    overatoms :: (AtomOf formula -> r -> r) -> formula -> r -> r
    -- ^ Formula analog of iterator 'foldr'.
    onatoms :: (AtomOf formula -> AtomOf formula) -> formula -> formula
    -- ^ Apply a function to the atoms, otherwise keeping structure (new sig)

(⊤) :: 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
"⊥"

-- | Special case of a union of the results of a function over the atoms.
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