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
import Data.Char
import Control.Monad
import Codec.TPTP.QuickCheck
import Data.String
import Data.Monoid hiding(All)
newtype Formula = FF (Formula0 Term Formula)
deriving (Eq,Ord,Show,Read,Data,Typeable)
newtype Term = TT (Term0 Term)
deriving (Eq,Ord,Show,Read,Data,Typeable)
(.<=>.) :: Formula -> Formula -> Formula
x .<=>. y = FF $ BinOp x (:<=>:) y
(.<~>.) :: Formula -> Formula -> Formula
x .<~>. y = FF $ BinOp x (:<~>:) y
(.=>.) :: Formula -> Formula -> Formula
x .=>. y = FF $ BinOp x (:=>:) y
(.<=.) :: Formula -> Formula -> Formula
x .<=. y = FF $ BinOp x (:<=:) y
(.~|.) :: Formula -> Formula -> Formula
x .~|. y = FF $ BinOp x (:~|:) y
(.|.) :: Formula -> Formula -> Formula
x .|. y = FF $ BinOp x (:|:) y
(.~&.) :: Formula -> Formula -> Formula
x .~&. y = FF $ BinOp x (:~&:) y
(.&.) :: Formula -> Formula -> Formula
x .&. y = FF $ BinOp x (:&:) y
(.~.) :: Formula -> Formula
(.~.) x = FF $ (:~:) x
(.=.) :: Term -> Term -> Formula
x .=. y = FF $ InfixPred x (:=:) y
(.!=.) :: Term -> Term -> Formula
x .!=. y = FF $ InfixPred x (:!=:) y
for_all :: [String] -> Formula -> Formula
for_all vars x = FF $ Quant All vars x
exists :: [String] -> Formula -> Formula
exists vars x = FF $ Quant Exists vars x
pApp :: AtomicWord -> [Term] -> Formula
pApp x args = FF $ PredApp x args
var :: String -> Term
var = TT . Var
fApp :: AtomicWord -> [Term] -> Term
fApp x args = TT $ FunApp x args
numberLitTerm :: Double -> Term
numberLitTerm = TT . NumberLitTerm
distinctObjectTerm :: String -> Term
distinctObjectTerm = TT . 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 [String] formula
| (:~:) formula
deriving (Eq,Ord,Show,Read,Data,Typeable)
data Term0 term =
Var String
| NumberLitTerm Double
| DistinctObjectTerm String
| FunApp AtomicWord [term]
deriving (Eq,Ord,Show,Read,Data,Typeable)
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)
data TPTP_Input =
AFormula {
name :: AtomicWord
, role :: Role
, formula :: Formula
, sourceInfo :: SourceInfo
, usefulInfo :: UsefulInfo
}
| Comment String
| Include FilePath [AtomicWord]
deriving (Eq,Ord,Show,Read,Data,Typeable)
data SourceInfo = NoSourceInfo | SourceInfo GTerm
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 String
| 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 FormulaOrTerm a where
elimFormulaOrTerm :: (Formula -> r) -> (Term -> r) -> a -> r
instance FormulaOrTerm Formula where
elimFormulaOrTerm k _ x = k x
instance FormulaOrTerm Term where
elimFormulaOrTerm _ k x = k x
free_vars :: forall a. (FormulaOrTerm a) => a -> Set String
free_vars = elimFormulaOrTerm free_vars0 free_vars0
univquant_free_vars :: Formula -> Formula
univquant_free_vars cnf =
case S.toList (free_vars cnf) of
[] -> cnf
vars -> for_all vars cnf
free_vars0 :: Data d => d -> Set String
free_vars0 x = case cast x :: Maybe Formula of
Just (FF (Quant All vars f0)) -> free_vars0 f0 `S.difference` S.fromList vars
Just (FF (Quant Exists vars f0)) -> free_vars0 f0 `S.difference` S.fromList vars
Just (FF f) -> unions (gmapQ free_vars0 f)
_ ->
case cast x :: Maybe Term of
Just (TT (Var s)) -> S.singleton s
Just (TT t) -> unions (gmapQ free_vars0 t)
_ -> S.empty
instance Arbitrary TPTP_Input
where arbitrary = frequency [(10,
do
x1 <- AtomicWord <$> arbLowerWord
x2 <- arbitrary
x3 <- arbitrary
x4 <- arbitrary
x5 <- arbitrary
return (AFormula x1 x2 x3 x4 x5))
, (1,
do
x1 <- arbPrintable
return (Comment ("% "++x1))
)
, (1, Include `fmap` arbLowerWord `ap`
listOf arbitrary)
]
instance Arbitrary Formula
where arbitrary = fmap FF arbitrary
instance Arbitrary Term
where arbitrary = fmap TT arbitrary
instance Arbitrary SourceInfo
where arbitrary = oneof [
return NoSourceInfo
, do
x1 <- arbitrary
return (SourceInfo x1)
]
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 (:) arbVar (argsFreq (\nargs -> vectorOf nargs arbVar))
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 <$> arbVar), (1,FunApp `fmap` arbitrary `ap` return[] ) ]
go i = oneof [
do
x1 <- arbVar
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 arbVar
]
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 <$> arbVar
,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 TermFix f = TermFix { runTermFix :: f (Term0 (TermFix f)) }
newtype FormulaFix f = FormulaFix { runFormulaFix :: f (Formula0 (TermFix f) (FormulaFix f)) }