{-# 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))
class (Eq predicate, Ord predicate, Show predicate, IsString predicate, Pretty predicate) => IsPredicate predicate
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
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
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
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")
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)))
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)
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))
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
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))))
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))
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)
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)
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
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 :: [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
type ApAtom = FOLAP Predicate FTerm
instance JustApply ApAtom