module Codec.TPTP.Base where
import Data.Generics
import Data.Set as S hiding(fold)
import Control.Applicative
import Prelude --hiding(concat,foldl,foldl1,foldr,foldr1)
import Test.QuickCheck hiding ((.&.))
import Data.Char
import Codec.TPTP.QuickCheck
import Data.String
import Data.Monoid hiding(All)
import Control.Monad.Identity
import Control.Monad.State
import Data.Function
deriving instance Eq a => Eq (Identity a)
deriving instance Ord a => Ord (Identity a)
deriving instance Show a => Show (Identity a)
deriving instance Read a => Read (Identity a)
deriving instance Data a => Data (Identity a)
deriving instance Typeable1 Identity
type Formula = F Identity
type Term = T Identity
type FormulaST s = F (State s)
type TermST s = T (State s)
type FormulaC = FormulaST [String]
type TermC = TermST [String]
forgetFC :: FormulaC -> Formula
forgetFC (F f) = F . return $
case evalState f [] of
BinOp f1 op f2 -> BinOp (forgetFC f1) op (forgetFC f2)
InfixPred t1 pred t2 -> InfixPred (forgetTC t1) pred (forgetTC t1)
PredApp aw ts -> PredApp aw (fmap forgetTC ts)
Quant quant vs f -> Quant quant vs (forgetFC f)
(:~:) f -> (:~:) (forgetFC f)
forgetTC :: TermC -> Term
forgetTC (T t) = T . return $
case evalState t [] of
Var v -> Var v
NumberLitTerm d -> NumberLitTerm d
DistinctObjectTerm s -> DistinctObjectTerm s
FunApp aw ts -> FunApp aw (fmap forgetTC ts)
(.<=>.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(F c) -> (F c) -> F c
x .<=>. y = (F . point) $ BinOp x (:<=>:) y
(.=>.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(F c) -> (F c) -> F c
x .=>. y = (F . point) $ BinOp x (:=>:) y
(.<=.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(F c) -> (F c) -> F c
x .<=. y = (F . point) $ BinOp x (:<=:) y
(.|.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(F c) -> (F c) -> F c
x .|. y = (F . point) $ BinOp x (:|:) y
(.&.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(F c) -> (F c) -> F c
x .&. y = (F . point) $ BinOp x (:&:) y
(.<~>.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(F c) -> (F c) -> F c
x .<~>. y = (F . point) $ BinOp x (:<~>:) y
(.~|.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(F c) -> (F c) -> F c
x .~|. y = (F . point) $ BinOp x (:~|:) y
(.~&.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(F c) -> (F c) -> F c
x .~&. y = (F . point) $ BinOp x (:~&:) y
(.~.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(F c) -> F c
(.~.) x = (F . point) $ (:~:) x
(.=.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(T c) -> (T c) -> F c
x .=. y = (F . point) $ InfixPred x (:=:) y
(.!=.) ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
(T c) -> (T c) -> F c
x .!=. y = (F . point) $ InfixPred x (:!=:) y
for_all ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
[V] -> (F c) -> F c
for_all vars x = (F . point) $ Quant All vars x
exists ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
[V] -> (F c) -> F c
exists vars x = (F . point) $ Quant Exists vars x
pApp ::
(Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) =>
AtomicWord -> [T c] -> F c
pApp x args = (F . point) $ PredApp x args
var ::
(Pointed (Term0 (T c)) (c (Term0 (T c)))) =>
V -> T c
var = (T . point) . Var
fApp ::
(Pointed (Term0 (T c)) (c (Term0 (T c)))) =>
AtomicWord -> [T c] -> T c
fApp x args = (T . point) $ FunApp x args
numberLitTerm ::
(Pointed (Term0 (T c)) (c (Term0 (T c)))) =>
Double -> T c
numberLitTerm = (T . point) . NumberLitTerm
distinctObjectTerm ::
(Pointed (Term0 (T c)) (c (Term0 (T c)))) =>
String -> T c
distinctObjectTerm = (T . point) . DistinctObjectTerm
infixl 2 .<=>. , .=>. , .<=. , .<~>.
infixl 3 .|. , .~|.
infixl 4 .&. , .~&.
infixl 5 .=. , .!=.
data Formula0 term formula =
BinOp formula BinOp formula
| InfixPred term InfixPred term
| PredApp AtomicWord [term]
| Quant Quant [V] formula
| (:~:) formula
deriving (Eq,Ord,Show,Read,Data,Typeable)
data Term0 term =
Var V
| NumberLitTerm Double
| DistinctObjectTerm String
| FunApp AtomicWord [term]
deriving (Eq,Ord,Show,Read,Data,Typeable)
newtype F c = F { runF :: c (Formula0 (T c) (F c)) }
newtype T c = T { runT :: c (Term0 (T c)) }
data BinOp =
(:<=>:)
| (:=>:)
| (:<=:)
| (:&:)
| (:|:)
| (:~&:)
| (:~|:)
| (:<~>:)
deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded)
data InfixPred =
(:=:) | (:!=:)
deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded)
data Quant = All | Exists
deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded)
type TPTP_Input = TPTP_Input_ Identity
type TPTP_Input_C = TPTP_Input_ (State [String])
forgetTIC :: TPTP_Input_C -> TPTP_Input
forgetTIC tic@(AFormula {}) = tic { formula = forgetFC (formula tic) }
forgetTIC (Comment s) = Comment s
forgetTIC (Include p aws) = Include p aws
data TPTP_Input_ c =
AFormula {
name :: AtomicWord
, role :: Role
, formula :: F c
, annotations :: Annotations
}
| Comment String
| Include FilePath [AtomicWord]
deriving instance Eq (c (Formula0 (T c) (F c))) => Eq (TPTP_Input_ c)
deriving instance Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c)
deriving instance Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c)
deriving instance Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c)
deriving instance (Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c)
instance Typeable1 c => Typeable (TPTP_Input_ c) where
typeOf ti = mkTyCon "TPTP_Input_" `mkTyConApp` [typeOf1 (runF $ formula ti)]
data Annotations = NoAnnotations | Annotations GTerm UsefulInfo
deriving (Eq,Ord,Show,Read,Data,Typeable)
data UsefulInfo = NoUsefulInfo | UsefulInfo [GTerm]
deriving (Eq,Ord,Show,Read,Data,Typeable)
data Role = Role { unrole :: String }
deriving (Eq,Ord,Show,Read,Data,Typeable)
data GData = GWord AtomicWord
| GApp AtomicWord [GTerm]
| GVar V
| GNumber Double
| GDistinctObject String
| GFormulaData String Formula
deriving (Eq,Ord,Show,Read,Data,Typeable)
data GTerm = ColonSep GData GTerm
| GTerm GData
| GList [GTerm]
deriving (Eq,Ord,Show,Read,Data,Typeable)
class FreeVars a where
freeVars :: a -> Set V
univquant_free_vars :: Formula -> Formula
univquant_free_vars cnf =
case S.toList (freeVars cnf) of
[] -> cnf
vars -> for_all vars cnf
instance FreeVars Formula where
freeVars = foldF
freeVars
(\_ vars x -> S.difference (freeVars x) (S.fromList vars))
(\x _ y -> (mappend `on` freeVars) x y)
(\x _ y -> (mappend `on` freeVars) x y)
(\_ args -> S.unions (fmap freeVars args))
instance FreeVars Term where
freeVars = foldT
(const mempty)
(const mempty)
S.singleton
(\_ args -> S.unions (fmap freeVars args))
instance Arbitrary TPTP_Input
where arbitrary = frequency [(10,
do
x1 <- AtomicWord <$> arbLowerWord
x2 <- arbitrary
x3 <- arbitrary
x4 <- arbitrary
return (AFormula x1 x2 x3 x4))
, (1,
do
x1 <- arbPrintable
return (Comment ("% "++x1))
)
, (1, Include `fmap` arbLowerWord `ap`
listOf arbitrary)
]
instance Arbitrary Formula
where arbitrary = fmap (F . point) arbitrary
instance Arbitrary Term
where arbitrary = fmap (T . point) arbitrary
instance Arbitrary Annotations
where arbitrary = oneof [
return NoAnnotations
, Annotations `fmap` arbitrary `ap` arbitrary
]
instance Arbitrary UsefulInfo
where arbitrary = oneof [
return NoUsefulInfo
, do
x1 <- arbitrary
return (UsefulInfo x1)
]
instance Arbitrary Role
where arbitrary = Role `fmap` arbLowerWord
#define TRACE(X) id
instance (Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b)
where arbitrary = sized (\n -> TRACE("arbitrary/Formula0") go n)
where
go 0 = flip PredApp [] `fmap` arbitrary
go i =
oneof [ do
ileft <- choose (0,i1)
x1 <- resize ileft arbitrary
x2 <- arbitrary
x3 <- resize (i 1 ileft) arbitrary
return (BinOp x1 x2 x3)
, do
x1 <- arbitrary
x2 <- arbitrary
x3 <- arbitrary
return (InfixPred x1 x2 x3)
, do
x1 <- arbitrary
x2 <- argsFreq vector
return (PredApp x1 x2)
, do
x1 <- arbitrary
x2 <- liftM2 (:) arbitrary (argsFreq (\nargs -> vectorOf nargs arbitrary))
x3 <- resize (i1) arbitrary
return (Quant x1 x2 x3)
, do
x1 <- resize (i1) arbitrary
return ((:~:) x1)
]
instance Arbitrary BinOp
where arbitrary = elements
[ (:<=>:)
, (:=>:)
, (:<=:)
, (:&:)
, (:|:)
, (:~&:)
, (:~|:)
, (:<~>:)
]
instance Arbitrary InfixPred
where arbitrary = elements [ (:=:),(:!=:) ]
instance Arbitrary Quant
where arbitrary = elements [All,Exists]
instance Arbitrary a => Arbitrary (Term0 a)
where arbitrary = sized (\n -> TRACE("arbitrary/Term0") go n)
where
go 0 = frequency [ (2,Var <$> arbitrary), (1,FunApp `fmap` arbitrary `ap` return[] ) ]
go i = oneof [
do
x1 <- arbitrary
return (Var x1)
, arbNum NumberLitTerm
, do
x1 <- arbPrintable
return (DistinctObjectTerm x1)
, do
x1 <- arbitrary
args <- argsFreq
(\nargs -> do
parti <- arbPartition nargs (i1)
mapM (flip resize arbitrary) parti
)
return (FunApp x1 args)
]
instance Arbitrary GData
where arbitrary = sized go
where
go 0 = oneof [ fmap GWord arbitrary
, fmap GVar arbitrary
]
go i =
oneof
[
GWord <$> arbitrary
,do
x1 <- arbLowerWord
args <- argsFreq
(\nargs -> do
parti <- arbPartition nargs (i1)
mapM (flip resize arbitrary) parti
) `suchThat` ((/=) [])
return (GApp (AtomicWord x1) args)
,GVar <$> arbitrary
,arbNum GNumber
,GDistinctObject <$> arbPrintable
,GFormulaData `fmap` ((:) '$' `fmap` arbLowerWord) `ap` (sized (\n -> resize (n `div` 2) arbitrary))
]
instance Arbitrary GTerm
where arbitrary = sized go
where
go 0 = fmap GTerm arbitrary
go i =
oneof [
do
ileft <- choose(0,i1)
x1 <- resize ileft arbitrary
x2 <- resize (i1ileft) arbitrary
return (ColonSep x1 x2)
, do
x1 <- arbitrary
return (GTerm x1)
, do
args <- argsFreq
(\nargs -> do
parti <- arbPartition nargs (i1)
mapM (flip resize arbitrary) parti
) `suchThat` (/= [])
return (GList args)
]
newtype AtomicWord = AtomicWord String
deriving (Eq,Ord,Show,Data,Typeable,Read,Monoid,IsString)
instance Arbitrary AtomicWord where
arbitrary = frequency [ (5, AtomicWord <$> arbLowerWord)
,(1, AtomicWord <$> arbPrintable)
]
newtype V = V String
deriving (Eq,Ord,Show,Data,Typeable,Read,Monoid,IsString)
instance Arbitrary V where
arbitrary = V <$> arbVar
#define DI(X) deriving instance (X (c (Term0 (T c)))) => X (T c); deriving instance (X (c (Formula0 (T c) (F c)))) => X (F c)
DI(Eq)
DI(Ord)
DI(Show)
DI(Read)
instance Typeable1 c => Typeable (F c) where
typeOf =
let tc = mkTyCon "F"
in (\(F x) -> mkTyConApp tc [typeOf1 x])
instance Typeable1 c => Typeable (T c) where
typeOf =
let tc = mkTyCon "T"
in (\(T x) -> mkTyConApp tc [typeOf1 x])
deriving instance (Typeable1 c, Data (c (Term0 (T c)))) => Data (T c)
deriving instance (Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (F c)
class Pointed a b | b -> a where
point :: a -> b
instance (Monad m) => Pointed a (m a) where
point = return
instance Ord a => Pointed a (Set a) where
point = S.singleton
class Copointed a b | b -> a where
copoint :: b -> a
instance Copointed a (Identity a) where
copoint (Identity x) = x
unwrapF ::
(Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t)))) =>
F t -> Formula0 (T t) (F t)
unwrapF (F x) = copoint x
unwrapT ::
(Copointed (Term0 (T t)) (t (Term0 (T t)))) =>
T t -> Term0 (T t)
unwrapT (T x) = copoint x
foldFormula0 ::
(f -> r)
-> (Quant -> [V] -> f -> r)
-> (f -> BinOp -> f -> r)
-> (t -> InfixPred -> t -> r)
-> (AtomicWord -> [t] -> r)
-> Formula0 t f
-> r
foldFormula0 kneg kquant kbinop kinfix kpredapp f =
case f of
(:~:) x -> kneg x
Quant x y z -> kquant x y z
BinOp x y z -> kbinop x y z
InfixPred x y z -> kinfix x y z
PredApp x y -> kpredapp x y
foldTerm0 ::
(String -> r)
-> (Double -> r)
-> (V -> r)
-> (AtomicWord -> [t] -> r)
-> Term0 t
-> r
foldTerm0 kdistinct knum kvar kfunapp t =
case t of
DistinctObjectTerm x -> kdistinct x
NumberLitTerm x -> knum x
Var x -> kvar x
FunApp x y -> kfunapp x y
foldF ::
(Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t)))) =>
(F t -> r)
-> (Quant -> [V] -> F t -> r)
-> (F t -> BinOp -> F t -> r)
-> (T t -> InfixPred -> T t -> r)
-> (AtomicWord -> [T t] -> r)
-> (F t -> r)
foldF kneg kquant kbinop kinfix kpredapp f = foldFormula0 kneg kquant kbinop kinfix kpredapp (unwrapF f)
foldT ::
(Copointed (Term0 (T t)) (t (Term0 (T t)))) =>
(String -> r)
-> (Double -> r)
-> (V -> r)
-> (AtomicWord -> [T t] -> r)
-> (T t -> r)
foldT kdistinct knum kvar kfunapp t = foldTerm0 kdistinct knum kvar kfunapp (unwrapT t)