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

module Data.Logic.ATP.Apply
    ( IsPredicate
    , HasApply(TermOf, PredOf, applyPredicate, foldApply', overterms, onterms)
    , atomFuncs
    , functions
    , JustApply
    , foldApply
    , prettyApply
    , overtermsApply
    , ontermsApply
    , zipApplys
    , showApply
    , convertApply
    , onformula
    , pApp
    , FOLAP(AP)
    , Predicate
    , ApAtom
    ) where

import Data.Data (Data)
import Data.Logic.ATP.Formulas (IsAtom, IsFormula(..), onatoms)
import Data.Logic.ATP.Pretty as Pretty ((<>), Associativity(InfixN), Doc, HasFixity(associativity, precedence), pAppPrec, text)
import Data.Logic.ATP.Term (Arity, FTerm, IsTerm(FunOf, TVarOf), funcs)
import Data.Set as Set (Set, union)
import Data.String (IsString(fromString))
import Data.Typeable (Typeable)
import Prelude hiding (pred)
import Text.PrettyPrint (parens, brackets, punctuate, comma, fcat, space)
import Text.PrettyPrint.HughesPJClass (Pretty(pPrint))

---------------------------
-- ATOMS (Atomic Formula) AND PREDICATES --
---------------------------

-- | A predicate is the thing we apply to a list of 'IsTerm's to make
-- an 'IsAtom'.
class (Eq predicate, Ord predicate, Show predicate, IsString predicate, Pretty predicate) => IsPredicate predicate

-- | The result of applying a predicate to some terms is an atomic
-- formula whose type is an instance of 'HasApply'.
class (IsAtom atom, IsPredicate (PredOf atom), IsTerm (TermOf atom)) => HasApply atom where
    type PredOf atom
    type TermOf atom
    applyPredicate :: PredOf atom -> [(TermOf atom)] -> atom
    foldApply' :: (atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
    overterms :: (TermOf atom -> r -> r) -> r -> atom -> r
    onterms :: (TermOf atom -> TermOf atom) -> atom -> atom

-- | The set of functions in an atom.
atomFuncs :: (HasApply atom, function ~ FunOf (TermOf atom)) => atom -> Set (function, Arity)
atomFuncs :: forall atom function.
(HasApply atom, function ~ FunOf (TermOf atom)) =>
atom -> Set (function, Arity)
atomFuncs = (TermOf atom -> Set (function, Arity) -> Set (function, Arity))
-> Set (function, Arity) -> atom -> Set (function, Arity)
forall atom r.
HasApply atom =>
(TermOf atom -> r -> r) -> r -> atom -> r
forall r. (TermOf atom -> r -> r) -> r -> atom -> r
overterms (Set (function, Arity)
-> Set (function, Arity) -> Set (function, Arity)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set (function, Arity)
 -> Set (function, Arity) -> Set (function, Arity))
-> (TermOf atom -> Set (function, Arity))
-> TermOf atom
-> Set (function, Arity)
-> Set (function, Arity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermOf atom -> Set (function, Arity)
forall term function.
(IsTerm term, function ~ FunOf term) =>
term -> Set (function, Arity)
funcs) Set (function, Arity)
forall a. Monoid a => a
mempty

-- | The set of functions in a formula.
functions :: (IsFormula formula, HasApply atom, Ord function,
              atom ~ AtomOf formula,
              term ~ TermOf atom,
              function ~ FunOf term) =>
             formula -> Set (function, Arity)
functions :: forall formula atom function term.
(IsFormula formula, HasApply atom, Ord function,
 atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term) =>
formula -> Set (function, Arity)
functions formula
fm = (AtomOf formula -> Set (function, Arity) -> Set (function, Arity))
-> formula -> Set (function, Arity) -> Set (function, Arity)
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r. (AtomOf formula -> r -> r) -> formula -> r -> r
overatoms (Set (function, Arity)
-> Set (function, Arity) -> Set (function, Arity)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set (function, Arity)
 -> Set (function, Arity) -> Set (function, Arity))
-> (atom -> Set (function, Arity))
-> atom
-> Set (function, Arity)
-> Set (function, Arity)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. atom -> Set (function, Arity)
forall atom function.
(HasApply atom, function ~ FunOf (TermOf atom)) =>
atom -> Set (function, Arity)
atomFuncs) formula
fm Set (function, Arity)
forall a. Monoid a => a
mempty

-- | Atoms that have apply but do not support equate
class HasApply atom => JustApply atom

foldApply :: (JustApply atom, term ~ TermOf atom) => (PredOf atom -> [term] -> r) -> atom -> r
foldApply :: forall atom term r.
(JustApply atom, term ~ TermOf atom) =>
(PredOf atom -> [term] -> r) -> atom -> r
foldApply = (atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall atom r.
HasApply atom =>
(atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall r.
(atom -> r) -> (PredOf atom -> [TermOf atom] -> r) -> atom -> r
foldApply' ([Char] -> atom -> r
forall a. HasCallStack => [Char] -> a
error [Char]
"JustApply failure")

-- | Pretty print prefix application of a predicate
prettyApply :: (v ~ TVarOf term, IsPredicate predicate, IsTerm term) => predicate -> [term] -> Doc
prettyApply :: forall v term predicate.
(v ~ TVarOf term, IsPredicate predicate, IsTerm term) =>
predicate -> [term] -> Doc
prettyApply predicate
p [term]
ts = predicate -> Doc
forall a. Pretty a => a -> Doc
pPrint predicate
p Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
fcat (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((term -> Doc) -> [term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map term -> Doc
forall a. Pretty a => a -> Doc
pPrint [term]
ts)))

-- | Implementation of 'overterms' for 'HasApply' types.
overtermsApply :: JustApply atom => ((TermOf atom) -> r -> r) -> r -> atom -> r
overtermsApply :: forall atom r.
JustApply atom =>
(TermOf atom -> r -> r) -> r -> atom -> r
overtermsApply TermOf atom -> r -> r
f r
r0 = (PredOf atom -> [TermOf atom] -> r) -> atom -> r
forall atom term r.
(JustApply atom, term ~ TermOf atom) =>
(PredOf atom -> [term] -> r) -> atom -> r
foldApply (\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 'HasApply' types.
ontermsApply :: JustApply atom => ((TermOf atom) -> (TermOf atom)) -> atom -> atom
ontermsApply :: forall atom.
JustApply atom =>
(TermOf atom -> TermOf atom) -> atom -> atom
ontermsApply TermOf atom -> TermOf atom
f = (PredOf atom -> [TermOf atom] -> atom) -> atom -> atom
forall atom term r.
(JustApply atom, term ~ TermOf atom) =>
(PredOf atom -> [term] -> r) -> atom -> r
foldApply (\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))

-- | Zip two atoms if they are similar
zipApplys :: (JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1,
              JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) =>
             (predicate -> [(term, term)] -> Maybe r) -> atom1 -> atom2 -> Maybe r
zipApplys :: forall atom1 term predicate atom2 r.
(JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1,
 JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) =>
(predicate -> [(term, term)] -> Maybe r)
-> atom1 -> atom2 -> Maybe r
zipApplys predicate -> [(term, term)] -> Maybe r
f atom1
atom1 atom2
atom2 =
    (PredOf atom1 -> [term] -> Maybe r) -> atom1 -> Maybe r
forall atom term r.
(JustApply atom, term ~ TermOf atom) =>
(PredOf atom -> [term] -> r) -> atom -> r
foldApply predicate -> [term] -> Maybe r
PredOf atom1 -> [term] -> Maybe r
f' atom1
atom1
    where
      f' :: predicate -> [term] -> Maybe r
f' predicate
p1 [term]
ts1 = (PredOf atom2 -> [term] -> Maybe r) -> atom2 -> Maybe r
forall atom term r.
(JustApply atom, term ~ TermOf atom) =>
(PredOf atom -> [term] -> r) -> atom -> r
foldApply (\PredOf atom2
p2 [term]
ts2 ->
                                     if predicate
p1 predicate -> predicate -> Bool
forall a. Eq a => a -> a -> Bool
/= predicate
PredOf atom2
p2 Bool -> Bool -> Bool
|| [term] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [term]
ts1 Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
/= [term] -> Arity
forall a. [a] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [term]
ts2
                                     then Maybe r
forall a. Maybe a
Nothing
                                     else predicate -> [(term, term)] -> Maybe r
f predicate
p1 ([term] -> [term] -> [(term, term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [term]
ts1 [term]
ts2)) atom2
atom2

-- | Implementation of 'Show' for 'JustApply' types
showApply :: (Show predicate, Show term) => predicate -> [term] -> String
showApply :: forall predicate term.
(Show predicate, Show term) =>
predicate -> [term] -> [Char]
showApply predicate
p [term]
ts = Doc -> [Char]
forall a. Show a => a -> [Char]
show ([Char] -> Doc
text [Char]
"pApp " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Char] -> Doc
text (predicate -> [Char]
forall a. Show a => a -> [Char]
show predicate
p)) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
brackets ([Doc] -> Doc
fcat (Doc -> [Doc] -> [Doc]
punctuate (Doc
comma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space) ((term -> Doc) -> [term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Doc
text ([Char] -> Doc) -> (term -> [Char]) -> term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. term -> [Char]
forall a. Show a => a -> [Char]
show) [term]
ts))))

-- | Convert between two instances of 'HasApply'
convertApply :: (JustApply atom1, HasApply atom2) =>
                (PredOf atom1 -> PredOf atom2) -> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2
convertApply :: forall atom1 atom2.
(JustApply atom1, HasApply atom2) =>
(PredOf atom1 -> PredOf atom2)
-> (TermOf atom1 -> TermOf atom2) -> atom1 -> atom2
convertApply PredOf atom1 -> PredOf atom2
cp TermOf atom1 -> TermOf atom2
ct = (PredOf atom1 -> [TermOf atom1] -> atom2) -> atom1 -> atom2
forall atom term r.
(JustApply atom, term ~ TermOf atom) =>
(PredOf atom -> [term] -> r) -> atom -> r
foldApply (\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))

-- | Special case of applying a subfunction to the top *terms*.
onformula :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula, term ~ TermOf atom) =>
             (term -> term) -> formula -> formula
onformula :: forall formula atom term.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula,
 term ~ TermOf atom) =>
(term -> term) -> formula -> formula
onformula term -> term
f = (AtomOf formula -> AtomOf formula) -> formula -> formula
forall formula.
IsFormula formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatoms ((TermOf atom -> TermOf atom) -> atom -> atom
forall atom.
HasApply atom =>
(TermOf atom -> TermOf atom) -> atom -> atom
onterms term -> term
TermOf atom -> TermOf atom
f)

-- | Build a formula from a predicate and a list of terms.
pApp :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula) => PredOf atom -> [TermOf atom] -> formula
pApp :: forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp PredOf atom
p [TermOf atom]
args = AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (PredOf atom -> [TermOf atom] -> atom
forall atom. HasApply atom => PredOf atom -> [TermOf atom] -> atom
applyPredicate PredOf atom
p [TermOf atom]
args)

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

instance (IsPredicate predicate, IsTerm term) => JustApply (FOLAP predicate term)

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

instance (IsPredicate predicate, IsTerm term) => Pretty (FOLAP predicate term) where
    pPrint :: FOLAP predicate term -> Doc
pPrint = (PredOf (FOLAP predicate term) -> [term] -> Doc)
-> FOLAP predicate term -> Doc
forall atom term r.
(JustApply atom, term ~ TermOf atom) =>
(PredOf atom -> [term] -> r) -> atom -> r
foldApply predicate -> [term] -> Doc
PredOf (FOLAP predicate term) -> [term] -> Doc
forall v term predicate.
(v ~ TVarOf term, IsPredicate predicate, IsTerm term) =>
predicate -> [term] -> Doc
prettyApply

instance (IsPredicate predicate, IsTerm term) => HasApply (FOLAP predicate term) where
    type PredOf (FOLAP predicate term) = predicate
    type TermOf (FOLAP predicate term) = term
    applyPredicate :: PredOf (FOLAP predicate term)
-> [TermOf (FOLAP predicate term)] -> FOLAP predicate term
applyPredicate = predicate -> [term] -> FOLAP predicate term
PredOf (FOLAP predicate term)
-> [TermOf (FOLAP predicate term)] -> FOLAP predicate term
forall predicate term. predicate -> [term] -> FOLAP predicate term
AP
    foldApply' :: forall r.
(FOLAP predicate term -> r)
-> (PredOf (FOLAP predicate term)
    -> [TermOf (FOLAP predicate term)] -> r)
-> FOLAP predicate term
-> r
foldApply' FOLAP predicate term -> r
_ PredOf (FOLAP predicate term)
-> [TermOf (FOLAP predicate term)] -> r
f (AP predicate
p [term]
ts) = PredOf (FOLAP predicate term)
-> [TermOf (FOLAP predicate term)] -> r
f predicate
PredOf (FOLAP predicate term)
p [term]
[TermOf (FOLAP predicate term)]
ts
    overterms :: forall r.
(TermOf (FOLAP predicate term) -> r -> r)
-> r -> FOLAP predicate term -> r
overterms TermOf (FOLAP predicate term) -> r -> r
f r
r (AP predicate
_ [term]
ts) = (term -> r -> r) -> r -> [term] -> r
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr term -> r -> r
TermOf (FOLAP predicate term) -> r -> r
f r
r [term]
ts
    onterms :: (TermOf (FOLAP predicate term) -> TermOf (FOLAP predicate term))
-> FOLAP predicate term -> FOLAP predicate term
onterms TermOf (FOLAP predicate term) -> TermOf (FOLAP predicate term)
f (AP predicate
p [term]
ts) = predicate -> [term] -> FOLAP predicate term
forall predicate term. predicate -> [term] -> FOLAP predicate term
AP predicate
p ((term -> term) -> [term] -> [term]
forall a b. (a -> b) -> [a] -> [b]
map term -> term
TermOf (FOLAP predicate term) -> TermOf (FOLAP predicate term)
f [term]
ts)

instance (IsPredicate predicate, IsTerm term, Show predicate, Show term) => Show (FOLAP predicate term) where
    show :: FOLAP predicate term -> [Char]
show = (PredOf (FOLAP predicate term) -> [term] -> [Char])
-> FOLAP predicate term -> [Char]
forall atom term r.
(JustApply atom, term ~ TermOf atom) =>
(PredOf atom -> [term] -> r) -> atom -> r
foldApply (\PredOf (FOLAP predicate term)
p [term]
ts -> predicate -> [term] -> [Char]
forall predicate term.
(Show predicate, Show term) =>
predicate -> [term] -> [Char]
showApply (predicate
PredOf (FOLAP predicate term)
p :: predicate) ([term]
ts :: [term]))

instance HasFixity (FOLAP predicate term) where
    precedence :: FOLAP predicate term -> Precedence
precedence FOLAP predicate term
_ = a
Precedence
pAppPrec
    associativity :: FOLAP predicate term -> Associativity
associativity FOLAP predicate term
_ = Associativity
Pretty.InfixN

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

instance IsString Predicate where

    -- fromString "True" = error "bad predicate name: True"
    -- fromString "False" = error "bad predicate name: True"
    -- fromString "=" = error "bad predicate name: True"
    fromString :: [Char] -> Predicate
fromString [Char]
s = [Char] -> Predicate
NamedPred [Char]
s

instance Show Predicate where
    show :: Predicate -> [Char]
show (NamedPred [Char]
s) = [Char]
"fromString " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> [Char]
show [Char]
s

instance Pretty Predicate where
    pPrint :: Predicate -> Doc
pPrint (NamedPred [Char]
"=") = [Char] -> Doc
forall a. HasCallStack => [Char] -> a
error [Char]
"Use of = as a predicate name is prohibited"
    pPrint (NamedPred [Char]
"True") = [Char] -> Doc
forall a. HasCallStack => [Char] -> a
error [Char]
"Use of True as a predicate name is prohibited"
    pPrint (NamedPred [Char]
"False") = [Char] -> Doc
forall a. HasCallStack => [Char] -> a
error [Char]
"Use of False as a predicate name is prohibited"
    pPrint (NamedPred [Char]
s) = [Char] -> Doc
text [Char]
s

instance IsPredicate Predicate

-- | An atom type with no equality predicate
type ApAtom = FOLAP Predicate FTerm
instance JustApply ApAtom