module Data.Logic.Types.FirstOrder
( Formula(..)
, PTerm(..)
, Predicate(..)
) where
import Data.Data (Data)
import qualified Data.Logic.Classes.Apply as C
import qualified Data.Logic.Classes.Atom as C
import Data.Logic.Classes.Combine (Combinable(..), Combination(..), BinOp(..))
import Data.Logic.Classes.Constants (Constants(..), asBool)
import Data.Logic.Classes.Equals (AtomEq(..), (.=.), pApp, substAtomEq, varAtomEq, prettyAtomEq)
import Data.Logic.Classes.FirstOrder (FirstOrderFormula(..), Quant(..), prettyFirstOrder, fixityFirstOrder, foldAtomsFirstOrder, mapAtomsFirstOrder)
import qualified Data.Logic.Classes.Formula as C
import Data.Logic.Classes.Literal (Literal(..))
import Data.Logic.Classes.Negate (Negatable(..))
import Data.Logic.Classes.Pretty (Pretty(pretty), HasFixity(..), botFixity)
import Data.Logic.Classes.Term (Term(..), Function)
import Data.Logic.Classes.Variable (Variable(..))
import Data.Logic.Classes.Propositional (PropositionalFormula(..))
import Data.Logic.Harrison.Resolution (matchAtomsEq)
import Data.Logic.Harrison.Tableaux (unifyAtomsEq)
import Data.Logic.Resolution (isRenameOfAtomEq, getSubstAtomEq)
import Data.SafeCopy (SafeCopy, base, deriveSafeCopy, extension, MigrateFrom(..))
import Data.Typeable (Typeable)
data Formula v p f
= Predicate (Predicate p (PTerm v f))
| Combine (Combination (Formula v p f))
| Quant Quant v (Formula v p f)
deriving (Eq, Ord, Data, Typeable, Show, Read)
data Predicate p term
= Equal term term
| Apply p [term]
deriving (Eq, Ord, Data, Typeable, Show, Read)
data PTerm v f
= Var v
| FunApp f [PTerm v f]
deriving (Eq, Ord, Data, Typeable, Show, Read)
instance Negatable (Formula v p f) where
negatePrivate x = Combine ((:~:) x)
foldNegation normal inverted (Combine ((:~:) x)) = foldNegation inverted normal x
foldNegation normal _ x = normal x
instance Constants p => Constants (Formula v p f) where
fromBool = Predicate . fromBool
asBool (Predicate x) = asBool x
asBool _ = Nothing
instance Constants p => Constants (Predicate p (PTerm v f)) where
fromBool x = Apply (fromBool x) []
asBool (Apply p _) = asBool p
asBool _ = Nothing
instance (Constants (Formula v p f) ) => Combinable (Formula v p f) where
x .<=>. y = Combine (BinOp x (:<=>:) y)
x .=>. y = Combine (BinOp x (:=>:) y)
x .|. y = Combine (BinOp x (:|:) y)
x .&. y = Combine (BinOp x (:&:) y)
instance (C.Predicate p, Function f v) => C.Formula (Formula v p f) (Predicate p (PTerm v f)) where
atomic = Predicate
foldAtoms = foldAtomsFirstOrder
mapAtoms = mapAtomsFirstOrder
instance (C.Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, C.Predicate p, Function f v, Constants (Formula v p f), Combinable (Formula v p f)
) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f)) where
foldPropositional co tf at formula =
maybe testFm tf (asBool formula)
where
testFm =
case formula of
Quant _ _ _ -> error "foldF0: quantifiers should not be present"
Combine x -> co x
Predicate x -> at x
instance (Variable v, Function f v) => Term (PTerm v f) v f where
foldTerm vf fn t =
case t of
Var v -> vf v
FunApp f ts -> fn f ts
zipTerms v f t1 t2 =
case (t1, t2) of
(Var v1, Var v2) -> v v1 v2
(FunApp f1 ts1, FunApp f2 ts2) -> f f1 ts1 f2 ts2
_ -> Nothing
vt = Var
fApp x args = FunApp x args
instance C.Predicate p => AtomEq (Predicate p (PTerm v f)) p (PTerm v f) where
foldAtomEq ap tf _ (Apply p ts) = maybe (ap p ts) tf (asBool p)
foldAtomEq _ _ eq (Equal t1 t2) = eq t1 t2
equals = Equal
applyEq' = Apply
instance (C.Formula (Formula v p f) (Predicate p (PTerm v f)),
AtomEq (Predicate p (PTerm v f)) p (PTerm v f),
Constants (Formula v p f),
Variable v, C.Predicate p, Function f v
) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v where
for_all v x = Quant Forall v x
exists v x = Quant Exists v x
foldFirstOrder qu co tf at f =
maybe testFm tf (asBool f)
where testFm = case f of
Quant op v f' -> qu op v f'
Combine x -> co x
Predicate x -> at x
instance (Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), C.Formula (Formula v p f) (Predicate p (PTerm v f))
) => Literal (Formula v p f) (Predicate p (PTerm v f)) where
foldLiteral neg tf at f =
case f of
Quant _ _ _ -> error "Invalid literal"
Combine ((:~:) p) -> neg p
Combine _ -> error "Invalid literal"
Predicate p -> if p == fromBool True
then tf True
else if p == fromBool False
then tf False
else at p
instance (C.Predicate p, Variable v, Function f v) => C.Atom (Predicate p (PTerm v f)) (PTerm v f) v where
substitute = substAtomEq
freeVariables = varAtomEq
allVariables = varAtomEq
unify = unifyAtomsEq
match = matchAtomsEq
foldTerms f r (Apply _ ts) = foldr f r ts
foldTerms f r (Equal t1 t2) = f t2 (f t1 r)
isRename = isRenameOfAtomEq
getSubst = getSubstAtomEq
instance (Variable v, Pretty v,
C.Predicate p, Pretty p,
Function f v, Pretty f) => Pretty (Predicate p (PTerm v f)) where
pretty atom = prettyAtomEq pretty pretty pretty 0 atom
instance (C.Formula (Formula v p f) (Predicate p (PTerm v f)),
C.Predicate p, Variable v, Function f v, HasFixity (Predicate p (PTerm v f))) => HasFixity (Formula v p f) where
fixity = fixityFirstOrder
instance (C.Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, C.Predicate p, Function f v) => Pretty (Formula v p f) where
pretty f = prettyFirstOrder (\ _ -> pretty) pretty 0 $ f
instance HasFixity (Predicate p term) where
fixity = const botFixity
$(deriveSafeCopy 1 'base ''PTerm)
$(deriveSafeCopy 1 'base ''Formula)
$(deriveSafeCopy 2 'extension ''Predicate)
data Predicate_v1 p term
= Equal_v1 term term
| NotEqual_v1 term term
| Constant_v1 Bool
| Apply_v1 p [term]
deriving (Eq, Ord, Data, Typeable, Show, Read)
$(deriveSafeCopy 1 'base ''Predicate_v1)
instance (SafeCopy p, SafeCopy term) => Migrate (Predicate p term) where
type MigrateFrom (Predicate p term) = (Predicate_v1 p term)
migrate (Equal_v1 t1 t2) = Equal t1 t2
migrate (Apply_v1 p ts) = Apply p ts
migrate (NotEqual_v1 _ _) = error "Failure migrating Predicate NotEqual"
migrate (Constant_v1 _) = error "Failure migrating Predicate Constant"