-- | 'IsLiteral' is a subclass of formulas that support negation and
-- have true and false elements.

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Logic.ATP.Lit
    ( IsLiteral(naiveNegate, foldNegation, foldLiteral')
    , (.~.), (¬), negate
    , negated
    , negative, positive
    , foldLiteral
    , JustLiteral
    , onatomsLiteral
    , overatomsLiteral
    , zipLiterals', zipLiterals
    , convertLiteral
    , convertToLiteral
    , precedenceLiteral
    , associativityLiteral
    , prettyLiteral
    , showLiteral
    -- * Instance
    , LFormula(T, F, Atom, Not)
    , Lit(L, lname)
    ) where

import Data.Data (Data)
import Data.Logic.ATP.Formulas (IsAtom, IsFormula(atomic, AtomOf, asBool, false, true), fromBool, overatoms, onatoms, prettyBool)
import Data.Logic.ATP.Pretty (Associativity(..), boolPrec, Doc, HasFixity(precedence, associativity), notPrec, Precedence, text)
import Data.Monoid ((<>))
import Data.Typeable (Typeable)
import Prelude hiding (negate, null)
import Text.PrettyPrint.HughesPJClass (maybeParens, Pretty(pPrint, pPrintPrec), PrettyLevel, prettyNormal)

-- | The class of formulas that can be negated.  Literals are the
-- building blocks of the clause and implicative normal forms.  They
-- support negation and must include true and false elements.
class IsFormula lit => IsLiteral lit where
    -- | Negate a formula in a naive fashion, the operators below
    -- prevent double negation.
    naiveNegate :: lit -> lit
    -- | Test whether a lit is negated or normal
    foldNegation :: (lit -> r) -- ^ called for normal formulas
                 -> (lit -> r) -- ^ called for negated formulas
                 -> lit -> r
    -- | This is the internal fold for literals, 'foldLiteral' below should
    -- normally be used, but its argument must be an instance of 'JustLiteral'.
    foldLiteral' :: (lit -> r) -- ^ Called for higher order formulas (non-literal)
                 -> (lit -> r) -- ^ Called for negated formulas
                 -> (Bool -> r) -- ^ Called for true and false formulas
                 -> (AtomOf lit -> r) -- ^ Called for atomic formulas
                 -> lit -> r

-- | Is this formula negated at the top level?
negated :: IsLiteral formula => formula -> Bool
negated :: forall formula. IsLiteral formula => formula -> Bool
negated = (formula -> Bool) -> (formula -> Bool) -> formula -> Bool
forall lit r. IsLiteral lit => (lit -> r) -> (lit -> r) -> lit -> r
forall r. (formula -> r) -> (formula -> r) -> formula -> r
foldNegation (Bool -> formula -> Bool
forall a b. a -> b -> a
const Bool
False) (Bool -> Bool
not (Bool -> Bool) -> (formula -> Bool) -> formula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> Bool
forall formula. IsLiteral formula => formula -> Bool
negated)

-- | Negate the formula, avoiding double negation
(.~.), (¬), negate :: IsLiteral formula => formula -> formula
.~. :: forall formula. IsLiteral formula => formula -> formula
(.~.) = (formula -> formula) -> (formula -> formula) -> formula -> formula
forall lit r. IsLiteral lit => (lit -> r) -> (lit -> r) -> lit -> r
forall r. (formula -> r) -> (formula -> r) -> formula -> r
foldNegation formula -> formula
forall formula. IsLiteral formula => formula -> formula
naiveNegate formula -> formula
forall a. a -> a
id
¬ :: forall formula. IsLiteral formula => formula -> formula
(¬) = formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)
negate :: forall formula. IsLiteral formula => formula -> formula
negate = formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)
infix 6 .~., ¬

-- | Some operations on IsLiteral formulas
negative :: IsLiteral formula => formula -> Bool
negative :: forall formula. IsLiteral formula => formula -> Bool
negative = formula -> Bool
forall formula. IsLiteral formula => formula -> Bool
negated

positive :: IsLiteral formula => formula -> Bool
positive :: forall formula. IsLiteral formula => formula -> Bool
positive = Bool -> Bool
not (Bool -> Bool) -> (formula -> Bool) -> formula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> Bool
forall formula. IsLiteral formula => formula -> Bool
negative

foldLiteral :: JustLiteral lit => (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral :: forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral = (lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral' ([Char] -> lit -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"JustLiteral failure")

-- | Class that indicates that a formula type *only* contains 'IsLiteral'
-- features - no combinations or quantifiers.
class IsLiteral formula => JustLiteral formula

-- | Combine two literals (internal version).
zipLiterals' :: (IsLiteral lit1, IsLiteral lit2) =>
                (lit1 -> lit2 -> Maybe r)
             -> (lit1 -> lit2 -> Maybe r)
             -> (Bool -> Bool -> Maybe r)
             -> (AtomOf lit1 -> AtomOf lit2 -> Maybe r)
             -> lit1 -> lit2 -> Maybe r
zipLiterals' :: forall lit1 lit2 r.
(IsLiteral lit1, IsLiteral lit2) =>
(lit1 -> lit2 -> Maybe r)
-> (lit1 -> lit2 -> Maybe r)
-> (Bool -> Bool -> Maybe r)
-> (AtomOf lit1 -> AtomOf lit2 -> Maybe r)
-> lit1
-> lit2
-> Maybe r
zipLiterals' lit1 -> lit2 -> Maybe r
ho lit1 -> lit2 -> Maybe r
neg Bool -> Bool -> Maybe r
tf AtomOf lit1 -> AtomOf lit2 -> Maybe r
at lit1
fm1 lit2
fm2 =
    (lit1 -> Maybe r)
-> (lit1 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf lit1 -> Maybe r)
-> lit1
-> Maybe r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(lit1 -> r)
-> (lit1 -> r) -> (Bool -> r) -> (AtomOf lit1 -> r) -> lit1 -> r
foldLiteral' lit1 -> Maybe r
ho' lit1 -> Maybe r
neg' Bool -> Maybe r
tf' AtomOf lit1 -> Maybe r
at' lit1
fm1
    where
      ho' :: lit1 -> Maybe r
ho' lit1
x1 = (lit2 -> Maybe r)
-> (lit2 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf lit2 -> Maybe r)
-> lit2
-> Maybe r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(lit2 -> r)
-> (lit2 -> r) -> (Bool -> r) -> (AtomOf lit2 -> r) -> lit2 -> r
foldLiteral' (lit1 -> lit2 -> Maybe r
ho lit1
x1) (\ lit2
_ -> Maybe r
forall a. Maybe a
Nothing) (\ Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (\ AtomOf lit2
_ -> Maybe r
forall a. Maybe a
Nothing) lit2
fm2
      neg' :: lit1 -> Maybe r
neg' lit1
p1 = (lit2 -> Maybe r)
-> (lit2 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf lit2 -> Maybe r)
-> lit2
-> Maybe r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(lit2 -> r)
-> (lit2 -> r) -> (Bool -> r) -> (AtomOf lit2 -> r) -> lit2 -> r
foldLiteral' (\ lit2
_ -> Maybe r
forall a. Maybe a
Nothing) (lit1 -> lit2 -> Maybe r
neg lit1
p1) (\ Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (\ AtomOf lit2
_ -> Maybe r
forall a. Maybe a
Nothing) lit2
fm2
      tf' :: Bool -> Maybe r
tf' Bool
x1 = (lit2 -> Maybe r)
-> (lit2 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf lit2 -> Maybe r)
-> lit2
-> Maybe r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(lit2 -> r)
-> (lit2 -> r) -> (Bool -> r) -> (AtomOf lit2 -> r) -> lit2 -> r
foldLiteral' (\ lit2
_ -> Maybe r
forall a. Maybe a
Nothing) (\ lit2
_ -> Maybe r
forall a. Maybe a
Nothing) (Bool -> Bool -> Maybe r
tf Bool
x1) (\ AtomOf lit2
_ -> Maybe r
forall a. Maybe a
Nothing) lit2
fm2
      at' :: AtomOf lit1 -> Maybe r
at' AtomOf lit1
a1 = (lit2 -> Maybe r)
-> (lit2 -> Maybe r)
-> (Bool -> Maybe r)
-> (AtomOf lit2 -> Maybe r)
-> lit2
-> Maybe r
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(lit2 -> r)
-> (lit2 -> r) -> (Bool -> r) -> (AtomOf lit2 -> r) -> lit2 -> r
foldLiteral' (\ lit2
_ -> Maybe r
forall a. Maybe a
Nothing) (\ lit2
_ -> Maybe r
forall a. Maybe a
Nothing) (\ Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (AtomOf lit1 -> AtomOf lit2 -> Maybe r
at AtomOf lit1
a1) lit2
fm2

-- | Combine two literals.
zipLiterals :: (JustLiteral lit1, JustLiteral lit2) =>
               (lit1 -> lit2 -> Maybe r)
            -> (Bool -> Bool -> Maybe r)
            -> (AtomOf lit1 -> AtomOf lit2 -> Maybe r)
            -> lit1 -> lit2 -> Maybe r
zipLiterals :: forall lit1 lit2 r.
(JustLiteral lit1, JustLiteral lit2) =>
(lit1 -> lit2 -> Maybe r)
-> (Bool -> Bool -> Maybe r)
-> (AtomOf lit1 -> AtomOf lit2 -> Maybe r)
-> lit1
-> lit2
-> Maybe r
zipLiterals lit1 -> lit2 -> Maybe r
neg Bool -> Bool -> Maybe r
tf AtomOf lit1 -> AtomOf lit2 -> Maybe r
at lit1
fm1 lit2
fm2 =
    (lit1 -> Maybe r)
-> (Bool -> Maybe r) -> (AtomOf lit1 -> Maybe r) -> lit1 -> Maybe r
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral lit1 -> Maybe r
neg' Bool -> Maybe r
tf' AtomOf lit1 -> Maybe r
at' lit1
fm1
    where
      neg' :: lit1 -> Maybe r
neg' lit1
p1 = (lit2 -> Maybe r)
-> (Bool -> Maybe r) -> (AtomOf lit2 -> Maybe r) -> lit2 -> Maybe r
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral (lit1 -> lit2 -> Maybe r
neg lit1
p1) (\ Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (\ AtomOf lit2
_ -> Maybe r
forall a. Maybe a
Nothing) lit2
fm2
      tf' :: Bool -> Maybe r
tf' Bool
x1 = (lit2 -> Maybe r)
-> (Bool -> Maybe r) -> (AtomOf lit2 -> Maybe r) -> lit2 -> Maybe r
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral (\ lit2
_ -> Maybe r
forall a. Maybe a
Nothing) (Bool -> Bool -> Maybe r
tf Bool
x1) (\ AtomOf lit2
_ -> Maybe r
forall a. Maybe a
Nothing) lit2
fm2
      at' :: AtomOf lit1 -> Maybe r
at' AtomOf lit1
a1 = (lit2 -> Maybe r)
-> (Bool -> Maybe r) -> (AtomOf lit2 -> Maybe r) -> lit2 -> Maybe r
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral (\ lit2
_ -> Maybe r
forall a. Maybe a
Nothing) (\ Bool
_ -> Maybe r
forall a. Maybe a
Nothing) (AtomOf lit1 -> AtomOf lit2 -> Maybe r
at AtomOf lit1
a1) lit2
fm2

-- | Convert a 'JustLiteral' instance to any 'IsLiteral' instance.
convertLiteral :: (JustLiteral lit1, IsLiteral lit2) => (AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertLiteral :: forall lit1 lit2.
(JustLiteral lit1, IsLiteral lit2) =>
(AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertLiteral AtomOf lit1 -> AtomOf lit2
ca lit1
fm = (lit1 -> lit2)
-> (Bool -> lit2) -> (AtomOf lit1 -> lit2) -> lit1 -> lit2
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral (\lit1
fm' -> lit2 -> lit2
forall formula. IsLiteral formula => formula -> formula
(.~.) ((AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
forall lit1 lit2.
(JustLiteral lit1, IsLiteral lit2) =>
(AtomOf lit1 -> AtomOf lit2) -> lit1 -> lit2
convertLiteral AtomOf lit1 -> AtomOf lit2
ca lit1
fm')) Bool -> lit2
forall formula. IsFormula formula => Bool -> formula
fromBool (AtomOf lit2 -> lit2
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf lit2 -> lit2)
-> (AtomOf lit1 -> AtomOf lit2) -> AtomOf lit1 -> lit2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomOf lit1 -> AtomOf lit2
ca) lit1
fm

-- | Convert any formula to a literal, passing non-IsLiteral
-- structures to the first argument (typically a call to error.)
convertToLiteral :: (IsLiteral formula, JustLiteral lit) =>
                    (formula -> lit) -> (AtomOf formula -> AtomOf lit) -> formula -> lit
convertToLiteral :: forall formula lit.
(IsLiteral formula, JustLiteral lit) =>
(formula -> lit)
-> (AtomOf formula -> AtomOf lit) -> formula -> lit
convertToLiteral formula -> lit
ho AtomOf formula -> AtomOf lit
ca formula
fm = (formula -> lit)
-> (formula -> lit)
-> (Bool -> lit)
-> (AtomOf formula -> lit)
-> formula
-> lit
forall lit r.
IsLiteral lit =>
(lit -> r)
-> (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall r.
(formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldLiteral' formula -> lit
ho (\formula
fm' -> lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) ((formula -> lit)
-> (AtomOf formula -> AtomOf lit) -> formula -> lit
forall formula lit.
(IsLiteral formula, JustLiteral lit) =>
(formula -> lit)
-> (AtomOf formula -> AtomOf lit) -> formula -> lit
convertToLiteral formula -> lit
ho AtomOf formula -> AtomOf lit
ca formula
fm')) Bool -> lit
forall formula. IsFormula formula => Bool -> formula
fromBool (AtomOf lit -> lit
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf lit -> lit)
-> (AtomOf formula -> AtomOf lit) -> AtomOf formula -> lit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtomOf formula -> AtomOf lit
ca) formula
fm

precedenceLiteral :: JustLiteral lit => lit -> Precedence
precedenceLiteral :: forall lit. JustLiteral lit => lit -> Precedence
precedenceLiteral = (lit -> a) -> (Bool -> a) -> (AtomOf lit -> a) -> lit -> a
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral (a -> lit -> a
forall a b. a -> b -> a
const a
Precedence
notPrec) (a -> Bool -> a
forall a b. a -> b -> a
const a
Precedence
boolPrec) AtomOf lit -> a
AtomOf lit -> Precedence
forall x. HasFixity x => x -> Precedence
precedence
associativityLiteral :: JustLiteral lit => lit -> Associativity
associativityLiteral :: forall lit. JustLiteral lit => lit -> Associativity
associativityLiteral = (lit -> Associativity)
-> (Bool -> Associativity)
-> (AtomOf lit -> Associativity)
-> lit
-> Associativity
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral (Associativity -> lit -> Associativity
forall a b. a -> b -> a
const Associativity
InfixA) (Associativity -> Bool -> Associativity
forall a b. a -> b -> a
const Associativity
InfixN) AtomOf lit -> Associativity
forall x. HasFixity x => x -> Associativity
associativity

-- | Implementation of 'pPrint' for -- 'JustLiteral' types.
prettyLiteral :: JustLiteral lit => PrettyLevel -> Rational -> lit -> Doc
prettyLiteral :: forall lit.
JustLiteral lit =>
PrettyLevel -> Rational -> lit -> Doc
prettyLiteral PrettyLevel
l Rational
r lit
lit =
    Bool -> Doc -> Doc
maybeParens (PrettyLevel
l PrettyLevel -> PrettyLevel -> Bool
forall a. Ord a => a -> a -> Bool
> PrettyLevel
prettyNormal Bool -> Bool -> Bool
|| Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> lit -> Precedence
forall x. HasFixity x => x -> Precedence
precedence lit
lit) ((lit -> Doc) -> (Bool -> Doc) -> (AtomOf lit -> Doc) -> lit -> Doc
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral lit -> Doc
ne Bool -> Doc
tf AtomOf lit -> Doc
forall {a}. Pretty a => a -> Doc
at lit
lit)
    where
      ne :: lit -> Doc
ne lit
p = [Char] -> Doc
text [Char]
"¬" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> PrettyLevel -> Rational -> lit -> Doc
forall lit.
JustLiteral lit =>
PrettyLevel -> Rational -> lit -> Doc
prettyLiteral PrettyLevel
l (lit -> Precedence
forall x. HasFixity x => x -> Precedence
precedence lit
lit) lit
p
      tf :: Bool -> Doc
tf = Bool -> Doc
prettyBool
      at :: a -> Doc
at a
a = a -> Doc
forall {a}. Pretty a => a -> Doc
pPrint a
a

showLiteral :: JustLiteral lit => lit -> String
showLiteral :: forall lit. JustLiteral lit => lit -> [Char]
showLiteral lit
lit = (lit -> [Char])
-> (Bool -> [Char]) -> (AtomOf lit -> [Char]) -> lit -> [Char]
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral lit -> [Char]
forall lit. JustLiteral lit => lit -> [Char]
ne Bool -> [Char]
tf AtomOf lit -> [Char]
at lit
lit
    where
      ne :: lit -> [Char]
ne lit
p = [Char]
"(.~.)(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ lit -> [Char]
forall lit. JustLiteral lit => lit -> [Char]
showLiteral lit
p [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      tf :: Bool -> [Char]
tf = Bool -> [Char]
forall a. Show a => a -> [Char]
show
      at :: AtomOf lit -> [Char]
at = AtomOf lit -> [Char]
forall a. Show a => a -> [Char]
show

-- | Implementation of 'onatoms' for 'JustLiteral' types.
onatomsLiteral :: JustLiteral lit => (AtomOf lit -> AtomOf lit) -> lit -> lit
onatomsLiteral :: forall lit.
JustLiteral lit =>
(AtomOf lit -> AtomOf lit) -> lit -> lit
onatomsLiteral AtomOf lit -> AtomOf lit
f lit
fm =
    (lit -> lit) -> (Bool -> lit) -> (AtomOf lit -> lit) -> lit -> lit
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral lit -> lit
ne Bool -> lit
tf AtomOf lit -> lit
at lit
fm
    where
      ne :: lit -> lit
ne lit
p = lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) ((AtomOf lit -> AtomOf lit) -> lit -> lit
forall lit.
JustLiteral lit =>
(AtomOf lit -> AtomOf lit) -> lit -> lit
onatomsLiteral AtomOf lit -> AtomOf lit
f lit
p)
      tf :: Bool -> lit
tf = Bool -> lit
forall formula. IsFormula formula => Bool -> formula
fromBool
      at :: AtomOf lit -> lit
at AtomOf lit
x = AtomOf lit -> lit
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (AtomOf lit -> AtomOf lit
f AtomOf lit
x)

-- | implementation of 'overatoms' for 'JustLiteral' types.
overatomsLiteral :: JustLiteral lit => (AtomOf lit -> r -> r) -> lit -> r -> r
overatomsLiteral :: forall lit r.
JustLiteral lit =>
(AtomOf lit -> r -> r) -> lit -> r -> r
overatomsLiteral AtomOf lit -> r -> r
f lit
fm r
r0 =
        (lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
forall lit r.
JustLiteral lit =>
(lit -> r) -> (Bool -> r) -> (AtomOf lit -> r) -> lit -> r
foldLiteral lit -> r
ne (r -> Bool -> r
forall a b. a -> b -> a
const r
r0) ((AtomOf lit -> r -> r) -> r -> AtomOf lit -> r
forall a b c. (a -> b -> c) -> b -> a -> c
flip AtomOf lit -> r -> r
f r
r0) lit
fm
        where
          ne :: lit -> r
ne lit
fm' = (AtomOf lit -> r -> r) -> lit -> r -> r
forall lit r.
JustLiteral lit =>
(AtomOf lit -> r -> r) -> lit -> r -> r
overatomsLiteral AtomOf lit -> r -> r
f lit
fm' r
r0

-- | Example of a 'JustLiteral' type.
data LFormula atom
    = F
    | T
    | Atom atom
    | Not (LFormula atom)
    deriving (LFormula atom -> LFormula atom -> Bool
(LFormula atom -> LFormula atom -> Bool)
-> (LFormula atom -> LFormula atom -> Bool) -> Eq (LFormula atom)
forall atom. Eq atom => LFormula atom -> LFormula atom -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall atom. Eq atom => LFormula atom -> LFormula atom -> Bool
== :: LFormula atom -> LFormula atom -> Bool
$c/= :: forall atom. Eq atom => LFormula atom -> LFormula atom -> Bool
/= :: LFormula atom -> LFormula atom -> Bool
Eq, Eq (LFormula atom)
Eq (LFormula atom) =>
(LFormula atom -> LFormula atom -> Ordering)
-> (LFormula atom -> LFormula atom -> Bool)
-> (LFormula atom -> LFormula atom -> Bool)
-> (LFormula atom -> LFormula atom -> Bool)
-> (LFormula atom -> LFormula atom -> Bool)
-> (LFormula atom -> LFormula atom -> LFormula atom)
-> (LFormula atom -> LFormula atom -> LFormula atom)
-> Ord (LFormula atom)
LFormula atom -> LFormula atom -> Bool
LFormula atom -> LFormula atom -> Ordering
LFormula atom -> LFormula atom -> LFormula atom
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall atom. Ord atom => Eq (LFormula atom)
forall atom. Ord atom => LFormula atom -> LFormula atom -> Bool
forall atom. Ord atom => LFormula atom -> LFormula atom -> Ordering
forall atom.
Ord atom =>
LFormula atom -> LFormula atom -> LFormula atom
$ccompare :: forall atom. Ord atom => LFormula atom -> LFormula atom -> Ordering
compare :: LFormula atom -> LFormula atom -> Ordering
$c< :: forall atom. Ord atom => LFormula atom -> LFormula atom -> Bool
< :: LFormula atom -> LFormula atom -> Bool
$c<= :: forall atom. Ord atom => LFormula atom -> LFormula atom -> Bool
<= :: LFormula atom -> LFormula atom -> Bool
$c> :: forall atom. Ord atom => LFormula atom -> LFormula atom -> Bool
> :: LFormula atom -> LFormula atom -> Bool
$c>= :: forall atom. Ord atom => LFormula atom -> LFormula atom -> Bool
>= :: LFormula atom -> LFormula atom -> Bool
$cmax :: forall atom.
Ord atom =>
LFormula atom -> LFormula atom -> LFormula atom
max :: LFormula atom -> LFormula atom -> LFormula atom
$cmin :: forall atom.
Ord atom =>
LFormula atom -> LFormula atom -> LFormula atom
min :: LFormula atom -> LFormula atom -> LFormula atom
Ord, ReadPrec [LFormula atom]
ReadPrec (LFormula atom)
Int -> ReadS (LFormula atom)
ReadS [LFormula atom]
(Int -> ReadS (LFormula atom))
-> ReadS [LFormula atom]
-> ReadPrec (LFormula atom)
-> ReadPrec [LFormula atom]
-> Read (LFormula atom)
forall atom. Read atom => ReadPrec [LFormula atom]
forall atom. Read atom => ReadPrec (LFormula atom)
forall atom. Read atom => Int -> ReadS (LFormula atom)
forall atom. Read atom => ReadS [LFormula atom]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall atom. Read atom => Int -> ReadS (LFormula atom)
readsPrec :: Int -> ReadS (LFormula atom)
$creadList :: forall atom. Read atom => ReadS [LFormula atom]
readList :: ReadS [LFormula atom]
$creadPrec :: forall atom. Read atom => ReadPrec (LFormula atom)
readPrec :: ReadPrec (LFormula atom)
$creadListPrec :: forall atom. Read atom => ReadPrec [LFormula atom]
readListPrec :: ReadPrec [LFormula atom]
Read, Int -> LFormula atom -> [Char] -> [Char]
[LFormula atom] -> [Char] -> [Char]
LFormula atom -> [Char]
(Int -> LFormula atom -> [Char] -> [Char])
-> (LFormula atom -> [Char])
-> ([LFormula atom] -> [Char] -> [Char])
-> Show (LFormula atom)
forall atom. Show atom => Int -> LFormula atom -> [Char] -> [Char]
forall atom. Show atom => [LFormula atom] -> [Char] -> [Char]
forall atom. Show atom => LFormula atom -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall atom. Show atom => Int -> LFormula atom -> [Char] -> [Char]
showsPrec :: Int -> LFormula atom -> [Char] -> [Char]
$cshow :: forall atom. Show atom => LFormula atom -> [Char]
show :: LFormula atom -> [Char]
$cshowList :: forall atom. Show atom => [LFormula atom] -> [Char] -> [Char]
showList :: [LFormula atom] -> [Char] -> [Char]
Show, Typeable (LFormula atom)
Typeable (LFormula atom) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> LFormula atom -> c (LFormula atom))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (LFormula atom))
-> (LFormula atom -> Constr)
-> (LFormula atom -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (LFormula atom)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (LFormula atom)))
-> ((forall b. Data b => b -> b) -> LFormula atom -> LFormula atom)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LFormula atom -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LFormula atom -> r)
-> (forall u. (forall d. Data d => d -> u) -> LFormula atom -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LFormula atom -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LFormula atom -> m (LFormula atom))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LFormula atom -> m (LFormula atom))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LFormula atom -> m (LFormula atom))
-> Data (LFormula atom)
LFormula atom -> Constr
LFormula atom -> DataType
(forall b. Data b => b -> b) -> LFormula atom -> LFormula atom
forall atom. Data atom => Typeable (LFormula atom)
forall atom. Data atom => LFormula atom -> Constr
forall atom. Data atom => LFormula atom -> DataType
forall atom.
Data atom =>
(forall b. Data b => b -> b) -> LFormula atom -> LFormula atom
forall atom u.
Data atom =>
Int -> (forall d. Data d => d -> u) -> LFormula atom -> u
forall atom u.
Data atom =>
(forall d. Data d => d -> u) -> LFormula atom -> [u]
forall atom r r'.
Data atom =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LFormula atom -> r
forall atom r r'.
Data atom =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LFormula atom -> r
forall atom (m :: * -> *).
(Data atom, Monad m) =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
forall atom (m :: * -> *).
(Data atom, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
forall atom (c :: * -> *).
Data atom =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (LFormula atom)
forall atom (c :: * -> *).
Data atom =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LFormula atom -> c (LFormula atom)
forall atom (t :: * -> *) (c :: * -> *).
(Data atom, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (LFormula atom))
forall atom (t :: * -> * -> *) (c :: * -> *).
(Data atom, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (LFormula atom))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LFormula atom -> u
forall u. (forall d. Data d => d -> u) -> LFormula atom -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LFormula atom -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LFormula atom -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (LFormula atom)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LFormula atom -> c (LFormula atom)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (LFormula atom))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (LFormula atom))
$cgfoldl :: forall atom (c :: * -> *).
Data atom =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LFormula atom -> c (LFormula atom)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LFormula atom -> c (LFormula atom)
$cgunfold :: forall atom (c :: * -> *).
Data atom =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (LFormula atom)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (LFormula atom)
$ctoConstr :: forall atom. Data atom => LFormula atom -> Constr
toConstr :: LFormula atom -> Constr
$cdataTypeOf :: forall atom. Data atom => LFormula atom -> DataType
dataTypeOf :: LFormula atom -> DataType
$cdataCast1 :: forall atom (t :: * -> *) (c :: * -> *).
(Data atom, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (LFormula atom))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (LFormula atom))
$cdataCast2 :: forall atom (t :: * -> * -> *) (c :: * -> *).
(Data atom, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (LFormula atom))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (LFormula atom))
$cgmapT :: forall atom.
Data atom =>
(forall b. Data b => b -> b) -> LFormula atom -> LFormula atom
gmapT :: (forall b. Data b => b -> b) -> LFormula atom -> LFormula atom
$cgmapQl :: forall atom r r'.
Data atom =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LFormula atom -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LFormula atom -> r
$cgmapQr :: forall atom r r'.
Data atom =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LFormula atom -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LFormula atom -> r
$cgmapQ :: forall atom u.
Data atom =>
(forall d. Data d => d -> u) -> LFormula atom -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> LFormula atom -> [u]
$cgmapQi :: forall atom u.
Data atom =>
Int -> (forall d. Data d => d -> u) -> LFormula atom -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LFormula atom -> u
$cgmapM :: forall atom (m :: * -> *).
(Data atom, Monad m) =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
$cgmapMp :: forall atom (m :: * -> *).
(Data atom, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
$cgmapMo :: forall atom (m :: * -> *).
(Data atom, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LFormula atom -> m (LFormula atom)
Data, Typeable)

data Lit = L {Lit -> [Char]
lname :: String} deriving (Lit -> Lit -> Bool
(Lit -> Lit -> Bool) -> (Lit -> Lit -> Bool) -> Eq Lit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Lit -> Lit -> Bool
== :: Lit -> Lit -> Bool
$c/= :: Lit -> Lit -> Bool
/= :: Lit -> Lit -> Bool
Eq, Eq Lit
Eq Lit =>
(Lit -> Lit -> Ordering)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Lit)
-> (Lit -> Lit -> Lit)
-> Ord Lit
Lit -> Lit -> Bool
Lit -> Lit -> Ordering
Lit -> Lit -> Lit
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Lit -> Lit -> Ordering
compare :: Lit -> Lit -> Ordering
$c< :: Lit -> Lit -> Bool
< :: Lit -> Lit -> Bool
$c<= :: Lit -> Lit -> Bool
<= :: Lit -> Lit -> Bool
$c> :: Lit -> Lit -> Bool
> :: Lit -> Lit -> Bool
$c>= :: Lit -> Lit -> Bool
>= :: Lit -> Lit -> Bool
$cmax :: Lit -> Lit -> Lit
max :: Lit -> Lit -> Lit
$cmin :: Lit -> Lit -> Lit
min :: Lit -> Lit -> Lit
Ord)

instance IsAtom atom => IsFormula (LFormula atom) where
    type AtomOf (LFormula atom) = atom
    asBool :: LFormula atom -> Maybe Bool
asBool LFormula atom
T = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
    asBool LFormula atom
F = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
    asBool LFormula atom
_ = Maybe Bool
forall a. Maybe a
Nothing
    true :: LFormula atom
true = LFormula atom
forall atom. LFormula atom
T
    false :: LFormula atom
false = LFormula atom
forall atom. LFormula atom
F
    atomic :: AtomOf (LFormula atom) -> LFormula atom
atomic = atom -> LFormula atom
AtomOf (LFormula atom) -> LFormula atom
forall atom. atom -> LFormula atom
Atom
    overatoms :: forall r.
(AtomOf (LFormula atom) -> r -> r) -> LFormula atom -> r -> r
overatoms = (AtomOf (LFormula atom) -> r -> r) -> LFormula atom -> r -> r
forall lit r.
JustLiteral lit =>
(AtomOf lit -> r -> r) -> lit -> r -> r
overatomsLiteral
    onatoms :: (AtomOf (LFormula atom) -> AtomOf (LFormula atom))
-> LFormula atom -> LFormula atom
onatoms = (AtomOf (LFormula atom) -> AtomOf (LFormula atom))
-> LFormula atom -> LFormula atom
forall lit.
JustLiteral lit =>
(AtomOf lit -> AtomOf lit) -> lit -> lit
onatomsLiteral

instance (IsFormula (LFormula atom), Eq atom, Ord atom) => IsLiteral (LFormula atom) where
    naiveNegate :: LFormula atom -> LFormula atom
naiveNegate = LFormula atom -> LFormula atom
forall atom. LFormula atom -> LFormula atom
Not
    foldNegation :: forall r.
(LFormula atom -> r) -> (LFormula atom -> r) -> LFormula atom -> r
foldNegation LFormula atom -> r
normal LFormula atom -> r
inverted (Not LFormula atom
x) = (LFormula atom -> r) -> (LFormula atom -> r) -> LFormula atom -> r
forall lit r. IsLiteral lit => (lit -> r) -> (lit -> r) -> lit -> r
forall r.
(LFormula atom -> r) -> (LFormula atom -> r) -> LFormula atom -> r
foldNegation LFormula atom -> r
inverted LFormula atom -> r
normal LFormula atom
x
    foldNegation LFormula atom -> r
normal LFormula atom -> r
_ LFormula atom
x = LFormula atom -> r
normal LFormula atom
x
    foldLiteral' :: forall r.
(LFormula atom -> r)
-> (LFormula atom -> r)
-> (Bool -> r)
-> (AtomOf (LFormula atom) -> r)
-> LFormula atom
-> r
foldLiteral' LFormula atom -> r
_ LFormula atom -> r
ne Bool -> r
tf AtomOf (LFormula atom) -> r
at LFormula atom
lit =
        case LFormula atom
lit of
          LFormula atom
F -> Bool -> r
tf Bool
False
          LFormula atom
T -> Bool -> r
tf Bool
True
          Atom atom
a -> AtomOf (LFormula atom) -> r
at atom
AtomOf (LFormula atom)
a
          Not LFormula atom
f -> LFormula atom -> r
ne LFormula atom
f

instance IsAtom atom => JustLiteral (LFormula atom)

instance IsAtom atom => HasFixity (LFormula atom) where
    precedence :: LFormula atom -> Precedence
precedence = LFormula atom -> a
LFormula atom -> Precedence
forall lit. JustLiteral lit => lit -> Precedence
precedenceLiteral
    associativity :: LFormula atom -> Associativity
associativity = LFormula atom -> Associativity
forall lit. JustLiteral lit => lit -> Associativity
associativityLiteral

instance IsAtom atom => Pretty (LFormula atom) where
    pPrintPrec :: PrettyLevel -> Rational -> LFormula atom -> Doc
pPrintPrec = PrettyLevel -> Rational -> LFormula atom -> Doc
forall lit.
JustLiteral lit =>
PrettyLevel -> Rational -> lit -> Doc
prettyLiteral