-- | ATOM with a distinguished Equate predicate.

{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Logic.ATP.Equate
    ( HasEquate(equate, foldEquate)
    , (.=.)
    , zipEquates
    , prettyEquate
    , overtermsEq
    , ontermsEq
    , showApplyAndEquate
    , showEquate
    , convertEquate
    , precedenceEquate
    , associativityEquate
    , FOL(R, Equals)
    , EqAtom
    ) where

import Data.Data (Data)
import Data.Logic.ATP.Apply (HasApply(PredOf, TermOf, applyPredicate, foldApply', overterms, onterms),
                             IsPredicate, Predicate, prettyApply, showApply)
import Data.Logic.ATP.Formulas (IsAtom, IsFormula(..))
import Data.Logic.ATP.Pretty as Pretty ((<>), Associativity(InfixN), atomPrec, Doc, eqPrec, HasFixity(associativity, precedence), pAppPrec, Precedence, text)
import Data.Logic.ATP.Term (FTerm, IsTerm)
import Data.Typeable (Typeable)
import Prelude hiding (pred)
import Text.PrettyPrint.HughesPJClass (maybeParens, Pretty(pPrintPrec), PrettyLevel)

-- | Atoms that support equality must be an instance of HasEquate
class HasApply atom => HasEquate atom where
    equate :: TermOf atom -> TermOf atom -> atom
    -- ^ Create an equate predicate
    foldEquate :: (TermOf atom -> TermOf atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
    -- ^ Analyze whether a predicate is an equate or a regular apply.

-- | Combine 'equate' and 'atomic' to build a formula from two terms.
(.=.) :: (IsFormula formula, HasEquate atom, atom ~ AtomOf formula) => TermOf atom -> TermOf atom -> formula
TermOf atom
a .=. :: forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. TermOf atom
b = AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (TermOf atom -> TermOf atom -> atom
forall atom. HasEquate atom => TermOf atom -> TermOf atom -> atom
equate TermOf atom
a TermOf atom
b)
infix 6 .=.

-- | Zip two atoms that support equality
zipEquates :: (HasEquate atom1, HasEquate atom2, PredOf atom1 ~ PredOf atom2) =>
              (TermOf atom1 -> TermOf atom1 ->
               TermOf atom2 -> TermOf atom2 -> Maybe r)
           -> (PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r)
           -> atom1 -> atom2 -> Maybe r
zipEquates :: forall atom1 atom2 r.
(HasEquate atom1, HasEquate atom2, PredOf atom1 ~ PredOf atom2) =>
(TermOf atom1
 -> TermOf atom1 -> TermOf atom2 -> TermOf atom2 -> Maybe r)
-> (PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r)
-> atom1
-> atom2
-> Maybe r
zipEquates TermOf atom1
-> TermOf atom1 -> TermOf atom2 -> TermOf atom2 -> Maybe r
eq PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r
ap atom1
atom1 atom2
atom2 =
    (TermOf atom1 -> TermOf atom1 -> Maybe r)
-> (PredOf atom1 -> [TermOf atom1] -> Maybe r) -> atom1 -> Maybe r
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom1 -> TermOf atom1 -> r)
-> (PredOf atom1 -> [TermOf atom1] -> r) -> atom1 -> r
foldEquate TermOf atom1 -> TermOf atom1 -> Maybe r
eq' PredOf atom1 -> [TermOf atom1] -> Maybe r
PredOf atom2 -> [TermOf atom1] -> Maybe r
ap' atom1
atom1
    where
      eq' :: TermOf atom1 -> TermOf atom1 -> Maybe r
eq' TermOf atom1
l1 TermOf atom1
r1 = (TermOf atom2 -> TermOf atom2 -> Maybe r)
-> (PredOf atom2 -> [TermOf atom2] -> Maybe r) -> atom2 -> Maybe r
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom2 -> TermOf atom2 -> r)
-> (PredOf atom2 -> [TermOf atom2] -> r) -> atom2 -> r
foldEquate (TermOf atom1
-> TermOf atom1 -> TermOf atom2 -> TermOf atom2 -> Maybe r
eq TermOf atom1
l1 TermOf atom1
r1) (\PredOf atom2
_ [TermOf atom2]
_ -> Maybe r
forall a. Maybe a
Nothing) atom2
atom2
      ap' :: PredOf atom2 -> [TermOf atom1] -> Maybe r
ap' PredOf atom2
p1 [TermOf atom1]
ts1 = (TermOf atom2 -> TermOf atom2 -> Maybe r)
-> (PredOf atom2 -> [TermOf atom2] -> Maybe r) -> atom2 -> Maybe r
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom2 -> TermOf atom2 -> r)
-> (PredOf atom2 -> [TermOf atom2] -> r) -> atom2 -> r
foldEquate (\TermOf atom2
_ TermOf atom2
_ -> Maybe r
forall a. Maybe a
Nothing) (PredOf atom2
-> [TermOf atom1] -> PredOf atom2 -> [TermOf atom2] -> Maybe r
ap'' PredOf atom2
p1 [TermOf atom1]
ts1) atom2
atom2
      ap'' :: PredOf atom2
-> [TermOf atom1] -> PredOf atom2 -> [TermOf atom2] -> Maybe r
ap'' PredOf atom2
p1 [TermOf atom1]
ts1 PredOf atom2
p2 [TermOf atom2]
ts2 | PredOf atom2
p1 PredOf atom2 -> PredOf atom2 -> Bool
forall a. Eq a => a -> a -> Bool
== PredOf atom2
p2 Bool -> Bool -> Bool
&& [TermOf atom1] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TermOf atom1]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TermOf atom2] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TermOf atom2]
ts2 = PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r
ap PredOf atom1
PredOf atom2
p1 ([TermOf atom1] -> [TermOf atom2] -> [(TermOf atom1, TermOf atom2)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TermOf atom1]
ts1 [TermOf atom2]
ts2)
      ap'' PredOf atom2
_ [TermOf atom1]
_ PredOf atom2
_ [TermOf atom2]
_ = Maybe r
forall a. Maybe a
Nothing

-- | Convert between HasEquate atom types.
convertEquate :: (HasEquate atom1, HasEquate atom2) =>
                 (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2
convertEquate :: forall atom1 atom2.
(HasEquate atom1, HasEquate atom2) =>
(PredOf atom1 -> PredOf atom2)
-> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2
convertEquate PredOf atom1 -> PredOf atom2
cp TermOf atom1 -> TermOf atom2
ct = (TermOf atom1 -> TermOf atom1 -> atom2)
-> (PredOf atom1 -> [TermOf atom1] -> atom2) -> atom1 -> atom2
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom1 -> TermOf atom1 -> r)
-> (PredOf atom1 -> [TermOf atom1] -> r) -> atom1 -> r
foldEquate (\TermOf atom1
t1 TermOf atom1
t2 -> TermOf atom2 -> TermOf atom2 -> atom2
forall atom. HasEquate atom => TermOf atom -> TermOf atom -> atom
equate (TermOf atom1 -> TermOf atom2
ct TermOf atom1
t1) (TermOf atom1 -> TermOf atom2
ct TermOf atom1
t2)) (\PredOf atom1
p1 [TermOf atom1]
ts1 -> PredOf atom2 -> [TermOf atom2] -> atom2
forall atom. HasApply atom => PredOf atom -> [TermOf atom] -> atom
applyPredicate (PredOf atom1 -> PredOf atom2
cp PredOf atom1
p1) ((TermOf atom1 -> TermOf atom2) -> [TermOf atom1] -> [TermOf atom2]
forall a b. (a -> b) -> [a] -> [b]
map TermOf atom1 -> TermOf atom2
ct [TermOf atom1]
ts1))

-- | Implementation of 'overterms' for 'HasEquate' types.
overtermsEq :: HasEquate atom => ((TermOf atom) -> r -> r) -> r -> atom -> r
overtermsEq :: forall atom r.
HasEquate atom =>
(TermOf atom -> r -> r) -> r -> atom -> r
overtermsEq TermOf atom -> r -> r
f r
r0 = (TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldEquate (\TermOf atom
t1 TermOf atom
t2 -> TermOf atom -> r -> r
f TermOf atom
t2 (TermOf atom -> r -> r
f TermOf atom
t1 r
r0)) (\PredOf atom
_ [TermOf atom]
ts -> (TermOf atom -> r -> r) -> r -> [TermOf atom] -> r
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TermOf atom -> r -> r
f r
r0 [TermOf atom]
ts)

-- | Implementation of 'onterms' for 'HasEquate' types.
ontermsEq :: HasEquate atom => ((TermOf atom) -> (TermOf atom)) -> atom -> atom
ontermsEq :: forall atom.
HasEquate atom =>
(TermOf atom -> TermOf atom) -> atom -> atom
ontermsEq TermOf atom -> TermOf atom
f = (TermOf atom -> TermOf atom -> atom)
-> (PredOf atom -> [TermOf atom] -> atom) -> atom -> atom
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldEquate (\TermOf atom
t1 TermOf atom
t2 -> TermOf atom -> TermOf atom -> atom
forall atom. HasEquate atom => TermOf atom -> TermOf atom -> atom
equate (TermOf atom -> TermOf atom
f TermOf atom
t1) (TermOf atom -> TermOf atom
f TermOf atom
t2)) (\PredOf atom
p [TermOf atom]
ts -> PredOf atom -> [TermOf atom] -> atom
forall atom. HasApply atom => PredOf atom -> [TermOf atom] -> atom
applyPredicate PredOf atom
p ((TermOf atom -> TermOf atom) -> [TermOf atom] -> [TermOf atom]
forall a b. (a -> b) -> [a] -> [b]
map TermOf atom -> TermOf atom
f [TermOf atom]
ts))

-- | Implementation of Show for 'HasEquate' types
showApplyAndEquate :: (HasEquate atom, Show (TermOf atom)) => atom -> String
showApplyAndEquate :: forall atom. (HasEquate atom, Show (TermOf atom)) => atom -> String
showApplyAndEquate atom
atom = (TermOf atom -> TermOf atom -> String)
-> (PredOf atom -> [TermOf atom] -> String) -> atom -> String
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldEquate TermOf atom -> TermOf atom -> String
forall term. Show term => term -> term -> String
showEquate PredOf atom -> [TermOf atom] -> String
forall predicate term.
(Show predicate, Show term) =>
predicate -> [term] -> String
showApply atom
atom

showEquate :: Show term => term -> term -> String
showEquate :: forall term. Show term => term -> term -> String
showEquate term
t1 term
t2 = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ term -> String
forall a. Show a => a -> String
show term
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") .=. (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ term -> String
forall a. Show a => a -> String
show term
t2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Format the infix equality predicate applied to two terms.
prettyEquate :: IsTerm term => PrettyLevel -> Rational -> term -> term -> Doc
prettyEquate :: forall term.
IsTerm term =>
PrettyLevel -> Rational -> term -> term -> Doc
prettyEquate PrettyLevel
l Rational
p term
t1 term
t2 =
    Bool -> Doc -> Doc
maybeParens (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
forall a. Num a => a
atomPrec) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ PrettyLevel -> Rational -> term -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
forall a. Num a => a
atomPrec term
t1 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text String
"=" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> PrettyLevel -> Rational -> term -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
forall a. Num a => a
atomPrec term
t2

precedenceEquate :: HasEquate atom => atom -> Precedence
precedenceEquate :: forall atom. HasEquate atom => atom -> forall a. Num a => a
precedenceEquate = (TermOf atom -> TermOf atom -> a)
-> (PredOf atom -> [TermOf atom] -> a) -> atom -> a
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldEquate (\TermOf atom
_ TermOf atom
_ -> a
forall a. Num a => a
eqPrec) (\PredOf atom
_ [TermOf atom]
_ -> a
forall a. Num a => a
pAppPrec)

associativityEquate :: HasEquate atom => atom -> Associativity
associativityEquate :: forall atom. HasEquate atom => atom -> Associativity
associativityEquate = (TermOf atom -> TermOf atom -> Associativity)
-> (PredOf atom -> [TermOf atom] -> Associativity)
-> atom
-> Associativity
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldEquate (\TermOf atom
_ TermOf atom
_ -> Associativity
Pretty.InfixN) (\PredOf atom
_ [TermOf atom]
_ -> Associativity
Pretty.InfixN)

-- | Instance of an atom type with a distinct equality predicate.
data FOL predicate term = R predicate [term] | Equals term term deriving (FOL predicate term -> FOL predicate term -> Bool
(FOL predicate term -> FOL predicate term -> Bool)
-> (FOL predicate term -> FOL predicate term -> Bool)
-> Eq (FOL predicate term)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall predicate term.
(Eq predicate, Eq term) =>
FOL predicate term -> FOL predicate term -> Bool
$c== :: forall predicate term.
(Eq predicate, Eq term) =>
FOL predicate term -> FOL predicate term -> Bool
== :: FOL predicate term -> FOL predicate term -> Bool
$c/= :: forall predicate term.
(Eq predicate, Eq term) =>
FOL predicate term -> FOL predicate term -> Bool
/= :: FOL predicate term -> FOL predicate term -> Bool
Eq, Eq (FOL predicate term)
Eq (FOL predicate term) =>
(FOL predicate term -> FOL predicate term -> Ordering)
-> (FOL predicate term -> FOL predicate term -> Bool)
-> (FOL predicate term -> FOL predicate term -> Bool)
-> (FOL predicate term -> FOL predicate term -> Bool)
-> (FOL predicate term -> FOL predicate term -> Bool)
-> (FOL predicate term -> FOL predicate term -> FOL predicate term)
-> (FOL predicate term -> FOL predicate term -> FOL predicate term)
-> Ord (FOL predicate term)
FOL predicate term -> FOL predicate term -> Bool
FOL predicate term -> FOL predicate term -> Ordering
FOL predicate term -> FOL predicate term -> FOL predicate term
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 predicate term.
(Ord predicate, Ord term) =>
Eq (FOL predicate term)
forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> Bool
forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> Ordering
forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> FOL predicate term
$ccompare :: forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> Ordering
compare :: FOL predicate term -> FOL predicate term -> Ordering
$c< :: forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> Bool
< :: FOL predicate term -> FOL predicate term -> Bool
$c<= :: forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> Bool
<= :: FOL predicate term -> FOL predicate term -> Bool
$c> :: forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> Bool
> :: FOL predicate term -> FOL predicate term -> Bool
$c>= :: forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> Bool
>= :: FOL predicate term -> FOL predicate term -> Bool
$cmax :: forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> FOL predicate term
max :: FOL predicate term -> FOL predicate term -> FOL predicate term
$cmin :: forall predicate term.
(Ord predicate, Ord term) =>
FOL predicate term -> FOL predicate term -> FOL predicate term
min :: FOL predicate term -> FOL predicate term -> FOL predicate term
Ord, Typeable (FOL predicate term)
Typeable (FOL predicate term) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> FOL predicate term
 -> c (FOL predicate term))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (FOL predicate term))
-> (FOL predicate term -> Constr)
-> (FOL predicate term -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (FOL predicate term)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (FOL predicate term)))
-> ((forall b. Data b => b -> b)
    -> FOL predicate term -> FOL predicate term)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> FOL predicate term -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> FOL predicate term -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> FOL predicate term -> m (FOL predicate term))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> FOL predicate term -> m (FOL predicate term))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> FOL predicate term -> m (FOL predicate term))
-> Data (FOL predicate term)
FOL predicate term -> Constr
FOL predicate term -> DataType
(forall b. Data b => b -> b)
-> FOL predicate term -> FOL predicate term
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) -> FOL predicate term -> u
forall u. (forall d. Data d => d -> u) -> FOL predicate term -> [u]
forall predicate term.
(Data predicate, Data term) =>
Typeable (FOL predicate term)
forall predicate term.
(Data predicate, Data term) =>
FOL predicate term -> Constr
forall predicate term.
(Data predicate, Data term) =>
FOL predicate term -> DataType
forall predicate term.
(Data predicate, Data term) =>
(forall b. Data b => b -> b)
-> FOL predicate term -> FOL predicate term
forall predicate term u.
(Data predicate, Data term) =>
Int -> (forall d. Data d => d -> u) -> FOL predicate term -> u
forall predicate term u.
(Data predicate, Data term) =>
(forall d. Data d => d -> u) -> FOL predicate term -> [u]
forall predicate term r r'.
(Data predicate, Data term) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r
forall predicate term r r'.
(Data predicate, Data term) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r
forall predicate term (m :: * -> *).
(Data predicate, Data term, Monad m) =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
forall predicate term (m :: * -> *).
(Data predicate, Data term, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
forall predicate term (c :: * -> *).
(Data predicate, Data term) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FOL predicate term)
forall predicate term (c :: * -> *).
(Data predicate, Data term) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> FOL predicate term
-> c (FOL predicate term)
forall predicate term (t :: * -> *) (c :: * -> *).
(Data predicate, Data term, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (FOL predicate term))
forall predicate term (t :: * -> * -> *) (c :: * -> *).
(Data predicate, Data term, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (FOL predicate term))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FOL predicate term)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> FOL predicate term
-> c (FOL predicate term)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (FOL predicate term))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (FOL predicate term))
$cgfoldl :: forall predicate term (c :: * -> *).
(Data predicate, Data term) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> FOL predicate term
-> c (FOL predicate term)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> FOL predicate term
-> c (FOL predicate term)
$cgunfold :: forall predicate term (c :: * -> *).
(Data predicate, Data term) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FOL predicate term)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FOL predicate term)
$ctoConstr :: forall predicate term.
(Data predicate, Data term) =>
FOL predicate term -> Constr
toConstr :: FOL predicate term -> Constr
$cdataTypeOf :: forall predicate term.
(Data predicate, Data term) =>
FOL predicate term -> DataType
dataTypeOf :: FOL predicate term -> DataType
$cdataCast1 :: forall predicate term (t :: * -> *) (c :: * -> *).
(Data predicate, Data term, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (FOL predicate term))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (FOL predicate term))
$cdataCast2 :: forall predicate term (t :: * -> * -> *) (c :: * -> *).
(Data predicate, Data term, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (FOL predicate term))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (FOL predicate term))
$cgmapT :: forall predicate term.
(Data predicate, Data term) =>
(forall b. Data b => b -> b)
-> FOL predicate term -> FOL predicate term
gmapT :: (forall b. Data b => b -> b)
-> FOL predicate term -> FOL predicate term
$cgmapQl :: forall predicate term r r'.
(Data predicate, Data term) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r
$cgmapQr :: forall predicate term r r'.
(Data predicate, Data term) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FOL predicate term -> r
$cgmapQ :: forall predicate term u.
(Data predicate, Data term) =>
(forall d. Data d => d -> u) -> FOL predicate term -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> FOL predicate term -> [u]
$cgmapQi :: forall predicate term u.
(Data predicate, Data term) =>
Int -> (forall d. Data d => d -> u) -> FOL predicate term -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> FOL predicate term -> u
$cgmapM :: forall predicate term (m :: * -> *).
(Data predicate, Data term, Monad m) =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
$cgmapMp :: forall predicate term (m :: * -> *).
(Data predicate, Data term, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
$cgmapMo :: forall predicate term (m :: * -> *).
(Data predicate, Data term, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> FOL predicate term -> m (FOL predicate term)
Data, Typeable, ReadPrec [FOL predicate term]
ReadPrec (FOL predicate term)
Int -> ReadS (FOL predicate term)
ReadS [FOL predicate term]
(Int -> ReadS (FOL predicate term))
-> ReadS [FOL predicate term]
-> ReadPrec (FOL predicate term)
-> ReadPrec [FOL predicate term]
-> Read (FOL predicate term)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall predicate term.
(Read predicate, Read term) =>
ReadPrec [FOL predicate term]
forall predicate term.
(Read predicate, Read term) =>
ReadPrec (FOL predicate term)
forall predicate term.
(Read predicate, Read term) =>
Int -> ReadS (FOL predicate term)
forall predicate term.
(Read predicate, Read term) =>
ReadS [FOL predicate term]
$creadsPrec :: forall predicate term.
(Read predicate, Read term) =>
Int -> ReadS (FOL predicate term)
readsPrec :: Int -> ReadS (FOL predicate term)
$creadList :: forall predicate term.
(Read predicate, Read term) =>
ReadS [FOL predicate term]
readList :: ReadS [FOL predicate term]
$creadPrec :: forall predicate term.
(Read predicate, Read term) =>
ReadPrec (FOL predicate term)
readPrec :: ReadPrec (FOL predicate term)
$creadListPrec :: forall predicate term.
(Read predicate, Read term) =>
ReadPrec [FOL predicate term]
readListPrec :: ReadPrec [FOL predicate term]
Read)

instance (IsPredicate predicate, IsTerm term) => HasEquate (FOL predicate term) where
    equate :: TermOf (FOL predicate term)
-> TermOf (FOL predicate term) -> FOL predicate term
equate TermOf (FOL predicate term)
lhs TermOf (FOL predicate term)
rhs = term -> term -> FOL predicate term
forall predicate term. term -> term -> FOL predicate term
Equals term
TermOf (FOL predicate term)
lhs term
TermOf (FOL predicate term)
rhs
    foldEquate :: forall r.
(TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> r)
-> (PredOf (FOL predicate term)
    -> [TermOf (FOL predicate term)] -> r)
-> FOL predicate term
-> r
foldEquate TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> r
eq PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r
_ (Equals term
lhs term
rhs) = TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> r
eq term
TermOf (FOL predicate term)
lhs term
TermOf (FOL predicate term)
rhs
    foldEquate TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> r
_ PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r
ap (R predicate
p [term]
ts) = PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r
ap predicate
PredOf (FOL predicate term)
p [term]
[TermOf (FOL predicate term)]
ts

instance (IsPredicate predicate, IsTerm term) => IsAtom (FOL predicate term)

instance (HasApply (FOL predicate term),
          HasEquate (FOL predicate term), IsTerm term) => Pretty (FOL predicate term) where
    pPrintPrec :: PrettyLevel -> Rational -> FOL predicate term -> Doc
pPrintPrec PrettyLevel
d Rational
r = (TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> Doc)
-> (PredOf (FOL predicate term)
    -> [TermOf (FOL predicate term)] -> Doc)
-> FOL predicate term
-> Doc
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> r)
-> (PredOf (FOL predicate term)
    -> [TermOf (FOL predicate term)] -> r)
-> FOL predicate term
-> r
foldEquate (PrettyLevel -> Rational -> term -> term -> Doc
forall term.
IsTerm term =>
PrettyLevel -> Rational -> term -> term -> Doc
prettyEquate PrettyLevel
d Rational
r) predicate -> [term] -> Doc
PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> Doc
forall v term predicate.
(v ~ TVarOf term, IsPredicate predicate, IsTerm term) =>
predicate -> [term] -> Doc
prettyApply

instance (IsPredicate predicate, IsTerm term) => HasApply (FOL predicate term) where
    type PredOf (FOL predicate term) = predicate
    type TermOf (FOL predicate term) = term
    applyPredicate :: PredOf (FOL predicate term)
-> [TermOf (FOL predicate term)] -> FOL predicate term
applyPredicate = predicate -> [term] -> FOL predicate term
PredOf (FOL predicate term)
-> [TermOf (FOL predicate term)] -> FOL predicate term
forall predicate term. predicate -> [term] -> FOL predicate term
R
    foldApply' :: forall r.
(FOL predicate term -> r)
-> (PredOf (FOL predicate term)
    -> [TermOf (FOL predicate term)] -> r)
-> FOL predicate term
-> r
foldApply' FOL predicate term -> r
_ PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r
f (R predicate
p [term]
ts) = PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r
f predicate
PredOf (FOL predicate term)
p [term]
[TermOf (FOL predicate term)]
ts
    foldApply' FOL predicate term -> r
d PredOf (FOL predicate term) -> [TermOf (FOL predicate term)] -> r
_ FOL predicate term
x = FOL predicate term -> r
d FOL predicate term
x
    overterms :: forall r.
(TermOf (FOL predicate term) -> r -> r)
-> r -> FOL predicate term -> r
overterms = (TermOf (FOL predicate term) -> r -> r)
-> r -> FOL predicate term -> r
forall atom r.
HasEquate atom =>
(TermOf atom -> r -> r) -> r -> atom -> r
overtermsEq
    onterms :: (TermOf (FOL predicate term) -> TermOf (FOL predicate term))
-> FOL predicate term -> FOL predicate term
onterms = (TermOf (FOL predicate term) -> TermOf (FOL predicate term))
-> FOL predicate term -> FOL predicate term
forall atom.
HasEquate atom =>
(TermOf atom -> TermOf atom) -> atom -> atom
ontermsEq

instance (IsPredicate predicate, IsTerm term, Show predicate, Show term) => Show (FOL predicate term) where
    show :: FOL predicate term -> String
show = (TermOf (FOL predicate term)
 -> TermOf (FOL predicate term) -> String)
-> (PredOf (FOL predicate term)
    -> [TermOf (FOL predicate term)] -> String)
-> FOL predicate term
-> String
forall atom r.
HasEquate atom =>
(TermOf atom -> TermOf atom -> r)
-> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(TermOf (FOL predicate term) -> TermOf (FOL predicate term) -> r)
-> (PredOf (FOL predicate term)
    -> [TermOf (FOL predicate term)] -> r)
-> FOL predicate term
-> r
foldEquate (\TermOf (FOL predicate term)
t1 TermOf (FOL predicate term)
t2 -> term -> term -> String
forall term. Show term => term -> term -> String
showEquate (term
TermOf (FOL predicate term)
t1 :: term) (term
TermOf (FOL predicate term)
t2 :: term))
                      (\PredOf (FOL predicate term)
p [TermOf (FOL predicate term)]
ts -> predicate -> [term] -> String
forall predicate term.
(Show predicate, Show term) =>
predicate -> [term] -> String
showApply (predicate
PredOf (FOL predicate term)
p :: predicate) ([term]
[TermOf (FOL predicate term)]
ts :: [term]))

instance  (IsPredicate predicate, IsTerm term) => HasFixity (FOL predicate term) where
    precedence :: FOL predicate term -> forall a. Num a => a
precedence = FOL predicate term -> a
FOL predicate term -> forall a. Num a => a
forall atom. HasEquate atom => atom -> forall a. Num a => a
precedenceEquate
    associativity :: FOL predicate term -> Associativity
associativity = FOL predicate term -> Associativity
forall atom. HasEquate atom => atom -> Associativity
associativityEquate

-- | An atom type with equality predicate
type EqAtom = FOL Predicate FTerm