logic-classes-0.44: Data/Logic/Instances/TPTP.hs
{-# LANGUAGE DeriveDataTypeable, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, OverloadedStrings,
RankNTypes, ScopedTypeVariables, StandaloneDeriving, TypeSynonymInstances, UndecidableInstances #-}
{-# OPTIONS -fno-warn-missing-signatures -fno-warn-orphans #-}
module Logic.Instances.TPTP where
import Codec.TPTP (F(..), Formula, BinOp(..), V(..), T(..), Term0(..), AtomicWord(..), Formula0(..), InfixPred(..))
import qualified Codec.TPTP as TPTP
import Control.Monad.Identity (Identity(..))
import Data.Char (isDigit, ord)
import Data.Generics (Data, Typeable)
import Data.String (IsString(..))
import qualified Logic.FirstOrder as Logic
import Logic.FirstOrder (FirstOrderFormula(..), Term(..), Pretty(..), Predicate(..), Variable(next), pApp)
import qualified Logic.Logic as Logic
import Logic.Logic (Negatable(..), Logic(..), Boolean(..))
import qualified Logic.Propositional as Logic
import Text.PrettyPrint (text)
-- |Generate a series of variable names.
instance Variable V where
one = V "VS1"
next (V s) =
V (case break (not . isDigit) (reverse s) of
("", "SV") -> "VS1"
(digits, "SV") -> "VS" ++ show (1 + read (reverse digits) :: Int)
_ -> "VS1")
instance Logic.Arity AtomicWord where
arity _ = Nothing
instance Logic.Pretty V where
pretty (V s) = text s
mn = 'x'
pref = 'x'
mx = 'z'
cnt = ord mx - ord mn + 1
-- |TPTP's Term type has two extra constructors that can be represented
-- using this augmented atomic function application type.
data AtomicFunction
= Atom AtomicWord
| StringLit String
| NumberLit Double
| Skolem V
deriving (Eq, Ord, Show, Data, Typeable)
instance IsString AtomicFunction where
fromString = Atom . AtomicWord
instance Logic.Skolem AtomicFunction where
toSkolem = Skolem . V . ("sK" ++) . show
fromSkolem (Skolem (V s)) = Just (read (drop 2 s) :: Int)
fromSkolem _ = Nothing
-- |This is not a safe way to implement booleans.
instance Logic.Boolean AtomicWord where
fromBool = AtomicWord . show
instance Logic.Pretty AtomicFunction where
pretty (Atom w) = Logic.pretty w
pretty (StringLit s) = text (show s)
pretty (NumberLit n) = text (show n)
pretty (Skolem (V s)) = text ("sK" ++ s)
instance Logic.Pretty AtomicWord where
pretty (AtomicWord s) = text s
instance Logic.Negatable Formula where
negated (F (Identity ((:~:) x))) = not (negated x)
negated _ = False
(.~.) (F (Identity ((:~:) x))) = x
(.~.) x = (.~.) x
-- |If this looks confusing, it is because TPTP has the same operators
-- as Logic, the .&. on the left is the Logic method name and .&. on
-- the right is the TPTP function.
instance Logic.Logic Formula where
x .<=>. y = x .<=>. y
x .=>. y = x .=>. y
x .<=. y = x .<=. y
x .|. y = x .|. y
x .&. y = x .&. y
x .<~>. y = x .<~>. y
x .~|. y = x .~|. y
x .~&. y = x .~&. y
-- |For types designed to represent first order (predicate) logic, it
-- is easiest to make the atomic type the same as the formula type,
-- and then raise an error if we see unexpected non-atomic formulas.
instance Logic.PropositionalFormula Formula Formula where
atomic (F (Identity (InfixPred t1 (:=:) t2))) = t1 .=. t2
atomic (F (Identity (InfixPred t1 (:!=:) t2))) = t1 .!=. t2
atomic (F (Identity (PredApp p ts))) = pApp p ts
atomic _ = error "atomic method of PropositionalFormula for TPTP: invalid argument"
-- Use the TPTP fold to implement the Logic fold. This means
-- building wrappers around some of the functions so that when
-- the wrappers are passed TPTP types they turn them into Logic
-- values to pass to the argument functions.
foldF0 c a form =
TPTP.foldF n' q' b' i' p' (unwrapF' form)
where q' = error "TPTP Formula with quantifier passed to foldF0"
n' f = c ((Logic.:~:) f)
b' f1 (:<=>:) f2 = c (Logic.BinOp f1 (Logic.:<=>:) f2)
b' f1 (:<=:) f2 = c (Logic.BinOp f2 (Logic.:=>:) f1)
b' f1 (:=>:) f2 = c (Logic.BinOp f1 (Logic.:=>:) f2)
b' f1 (:&:) f2 = c (Logic.BinOp f1 (Logic.:&:) f2)
-- The :~&: operator is not present in the Logic BinOp type,
-- so we need to use the equivalent ~(a&b)
b' f1 (:~&:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .&. f2))
b' f1 (:|:) f2 = c (Logic.BinOp f1 (Logic.:|:) f2)
b' f1 (:~|:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .|. f2))
b' f1 (:<~>:) f2 = TPTP.foldF n' q' b' i' p' ((((.~.) f1) .&. f2) .|. (f1 .&. ((.~.) f2)))
i' t1 (:=:) t2 = a (F (Identity (InfixPred t1 (:=:) t2)))
i' t1 (:!=:) t2 = a (F (Identity (InfixPred t1 (:!=:) t2)))
p' p ts = a (F (Identity (PredApp p ts)))
unwrapF' (F x) = F x -- copoint x
instance Logic.FirstOrderFormula Formula (T Identity) V AtomicWord AtomicFunction where
for_all vars x = for_all vars x
exists vars x = exists vars x
-- Use the TPTP fold to implement the Logic fold. This means
-- building wrappers around some of the functions so that when
-- the wrappers are passed TPTP types they turn them into Logic
-- values to pass to the argument functions.
foldF q c p form =
TPTP.foldF n' q' b' i' p' (unwrapF' form)
where q' op (v:vs) form' =
let op' = case op of
TPTP.All -> Logic.All
TPTP.Exists -> Logic.Exists in
q op' v (foldr (\ v' f -> Logic.quant op' v' f) form' vs)
q' _ [] form' = foldF q c p form'
n' f = c ((Logic.:~:) f)
b' f1 (:<=>:) f2 = c (Logic.BinOp f1 (Logic.:<=>:) f2)
b' f1 (:<=:) f2 = c (Logic.BinOp f2 (Logic.:=>:) f1)
b' f1 (:=>:) f2 = c (Logic.BinOp f1 (Logic.:=>:) f2)
b' f1 (:&:) f2 = c (Logic.BinOp f1 (Logic.:&:) f2)
-- The :~&: operator is not present in the Logic BinOp type,
-- so we need to somehow use the equivalent ~(a&b)
b' f1 (:~&:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .&. f2))
b' f1 (:|:) f2 = c (Logic.BinOp f1 (Logic.:|:) f2)
b' f1 (:~|:) f2 = TPTP.foldF n' q' b' i' p' ((.~.) (f1 .|. f2))
b' f1 (:<~>:) f2 = TPTP.foldF n' q' b' i' p' ((((.~.) f1) .&. f2) .|. (f1 .&. ((.~.) f2)))
i' t1 (:=:) t2 = p (Equal t1 t2)
i' t1 (:!=:) t2 = p (NotEqual t1 t2) -- TPTP.foldF n' q' b' i' p' ((.~.) (t1 .=. t2))
p' pr ts = p (Apply pr ts)
unwrapF' (F x) = F x -- copoint x
zipF = error "Unimplemented: Logic.Instances.TPTP.zipF"
x .=. y = x .=. y
x .!=. y = x .!=. y
pApp0 p = TPTP.pApp p []
pApp1 p a = TPTP.pApp p [a]
pApp2 p a b = TPTP.pApp p [a,b]
pApp3 p a b c = TPTP.pApp p [a,b,c]
pApp4 p a b c d = TPTP.pApp p [a,b,c,d]
pApp5 p a b c d e = TPTP.pApp p [a,b,c,d,e]
pApp6 p a b c d e f = TPTP.pApp p [a,b,c,d,e,f]
pApp7 p a b c d e f g = TPTP.pApp p [a,b,c,d,e,f,g]
instance (Eq AtomicFunction, Logic.Skolem AtomicFunction) => Logic.Term (T Identity) V AtomicFunction where
foldT v fa term =
-- We call the foldT function from the TPTP package here, which
-- has a different signature from the foldT method we are
-- implementing. The two extra term types in TPTP are represented
-- here as additional values in the AtomicFunction type.
TPTP.foldT string double v atom (unwrapT' term)
where atom w ts = fa (Atom w) ts
string s = fa (StringLit s) []
double n = fa (NumberLit n) []
unwrapT' (T x) = T x -- copoint x
zipT = error "Unimplemented: Logic.Instances.TPTP.zipT"
var = var
fApp x args =
case x of
Atom w -> TPTP.fApp w args
StringLit s -> T {runT = Identity (DistinctObjectTerm s)}
NumberLit n -> T {runT = Identity (NumberLitTerm n)}
Skolem (V s) -> TPTP.fApp (AtomicWord ("Sk(" ++ s ++ ")")) args
--deriving instance Show TPTP.Term
--deriving instance (Show t, Show f) => Show (TPTP.Formula0 t f)
--deriving instance Show t => Show (TPTP.Term0 t)