diff --git a/Codec/TPTP/Base.hs b/Codec/TPTP/Base.hs --- a/Codec/TPTP/Base.hs +++ b/Codec/TPTP/Base.hs @@ -1,4 +1,8 @@ -{-# OPTIONS -fwarn-missing-signatures -XRecordWildCards -XCPP -XDeriveDataTypeable -fglasgow-exts -XNoMonomorphismRestriction -XTemplateHaskell -XUndecidableInstances -XGeneralizedNewtypeDeriving -Wall #-} +{-# OPTIONS -XRecordWildCards -XCPP + -XDeriveDataTypeable -fglasgow-exts -XNoMonomorphismRestriction + -XTemplateHaskell -XGeneralizedNewtypeDeriving -Wall + -fno-warn-orphans -XOverlappingInstances -XUndecidableInstances + #-} module Codec.TPTP.Base where @@ -9,65 +13,147 @@ import Prelude --hiding(concat,foldl,foldl1,foldr,foldr1) --import Data.Foldable --import Test.QuickCheck.Instances -import Test.QuickCheck +import Test.QuickCheck hiding ((.&.)) import Data.Char -import Control.Monad import Codec.TPTP.QuickCheck import Data.String import Data.Monoid hiding(All) +import Control.Monad.Identity +import Data.Function +-- Should be in the standard library +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 + + + -- * Basic undecorated formulae and terms -- | Basic (undecorated) first-order formulae -newtype Formula = FF (Formula0 Term Formula) - deriving (Eq,Ord,Show,Read,Data,Typeable) - +type Formula = F Identity + -- | Basic (undecorated) terms -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 +type Term = T Identity + +-- | Equivalence +-- +-- Don't let the type context of these wrapper function confuse you :) -- the important special case is just: +-- +-- @\(\.\<\=\>\.\) :: 'Formula' -> 'Formula' -> 'Formula'@ +(.<=>.) :: + (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 + -(.~.) :: Formula -> Formula -(.~.) x = FF $ (:~:) x +-- | Implication +(.=>.) :: + (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 + +-- | Reverse implication +(.<=.) :: + (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 + +-- | Disjunction/OR +(.|.) :: + (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 + +-- | Conjunction/AND +(.&.) :: + (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 + +-- | XOR +(.<~>.) :: + (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 + +-- | NOR +(.~|.) :: + (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 + + + +-- | NAND +(.~&.) :: + (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 + + +-- | Negation +(.~.) :: + (Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c)))) => + (F c) -> F c +(.~.) x = (F . point) $ (:~:) x -(.=.) :: Term -> Term -> Formula -x .=. y = FF $ InfixPred x (:=:) y -(.!=.) :: Term -> Term -> Formula -x .!=. y = FF $ InfixPred x (:!=:) y +-- | Equality +(.=.) :: + (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 :: [String] -> Formula -> Formula -for_all vars x = FF $ Quant All vars x +-- | Inequality +(.!=.) :: + (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 + +-- | Universal quantification +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 :: [String] -> Formula -> Formula -exists vars x = FF $ Quant Exists vars x +-- | Existential quantification +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 :: AtomicWord -> [Term] -> Formula -pApp x args = FF $ PredApp x args +-- | Predicate symbol application +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 :: 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 +-- | Variable +var :: + (Pointed (Term0 (T c)) (c (Term0 (T c)))) => + V -> T c +var = (T . point) . Var + +-- | Function symbol application (constants are encoded as nullary functions) +fApp :: + (Pointed (Term0 (T c)) (c (Term0 (T c)))) => + AtomicWord -> [T c] -> T c +fApp x args = (T . point) $ FunApp x args + +-- | Number literal +numberLitTerm :: + (Pointed (Term0 (T c)) (c (Term0 (T c)))) => + Double -> T c +numberLitTerm = (T . point) . NumberLitTerm + +-- | Double-quoted string literal, called /Distinct Object/ in TPTP's grammar +distinctObjectTerm :: + (Pointed (Term0 (T c)) (c (Term0 (T c)))) => + String -> T c +distinctObjectTerm = (T . point) . DistinctObjectTerm infixl 2 .<=>. , .=>. , .<=. , .<~>. infixl 3 .|. , .~|. @@ -76,30 +162,48 @@ -- * General decorated formulae and terms --- | See for the point of the type parameters (they allow for future decorations). If you don't need decorations, you can just use 'Formula' and the wrapped constructors above. +-- | See for the point of the type parameters (they allow for future decorations, e.g. monadic subformulae). If you don't need decorations, you can just use 'Formula' and the wrapped constructors above. data Formula0 term formula = BinOp formula BinOp formula -- ^ Binary connective application | InfixPred term InfixPred term -- ^ Infix predicate application (equalities, inequalities) | PredApp AtomicWord [term] -- ^ Predicate application - | Quant Quant [String] formula -- ^ Quantified formula + | Quant Quant [V] formula -- ^ Quantified formula | (:~:) formula -- ^ Negation deriving (Eq,Ord,Show,Read,Data,Typeable) -- | See for the point of the type parameters (they allow for future decorations). If you don't need decorations, you can just use 'Term' and the wrapped constructors above. data Term0 term = - Var String -- ^ Variable + Var V -- ^ Variable | NumberLitTerm Double -- ^ Number literal | DistinctObjectTerm String -- ^ Double-quoted item - | FunApp AtomicWord [term] -- ^ Function symbol application (constants are nullary functions) + | FunApp AtomicWord [term] -- ^ Function symbol application (constants are encoded as nullary functions) deriving (Eq,Ord,Show,Read,Data,Typeable) + + +-- | Formulae whose subexpressions are wrapped in the given type constructor @c@. +-- +-- For example: +-- +-- - @c = 'Identity'@: Plain formulae +-- +-- - @c = 'Maybe'@: Formulae that may contain \"holes\" +-- +-- - @c = 'IORef'@: (Mutable) formulae with mutable subexpressions +newtype F c = F { runF :: c (Formula0 (T c) (F c)) } + +-- | Terms whose subterms are wrapped in the given type constructor @c@ +newtype T c = T { runT :: c (Term0 (T c)) } + + + -- | Binary formula connectives data BinOp = - -- Please don't change the constructor names + -- Please don't change the constructor names (the Show instance is significant) (:<=>:) -- ^ Equivalence | (:=>:) -- ^ Implication - | (:<=:) -- ^ Implication (reverse) + | (:<=:) -- ^ Reverse Implication | (:&:) -- ^ AND | (:|:) -- ^ OR | (:~&:) -- ^ NAND @@ -109,7 +213,7 @@ -- | /Term -> Term -> Formula/ infix connectives data InfixPred = - -- Please don't change the constructor names + -- Please don't change the constructor names (the Show instance is significant) (:=:) | (:!=:) deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded) @@ -126,8 +230,7 @@ name :: AtomicWord , role :: Role , formula :: Formula - , sourceInfo :: SourceInfo - , usefulInfo :: UsefulInfo + , annotations :: Annotations } | Comment String | Include FilePath [AtomicWord] @@ -138,7 +241,7 @@ -- | Annotations about the formulas origin -data SourceInfo = NoSourceInfo | SourceInfo GTerm +data Annotations = NoAnnotations | Annotations GTerm UsefulInfo deriving (Eq,Ord,Show,Read,Data,Typeable) -- | Misc annotations @@ -153,7 +256,7 @@ -- | Metadata (the /general_data/ rule in TPTP's grammar) data GData = GWord AtomicWord | GApp AtomicWord [GTerm] - | GVar String + | GVar V | GNumber Double | GDistinctObject String | GFormulaData String Formula @@ -170,46 +273,43 @@ -- * Gathering free Variables -class FormulaOrTerm a where - elimFormulaOrTerm :: (Formula -> r) -> (Term -> r) -> a -> r +-- class FormulaOrTerm c a where +-- elimFormulaOrTerm :: (F c -> r) -> (T c -> r) -> a -> r -instance FormulaOrTerm Formula where - elimFormulaOrTerm k _ x = k x +-- instance FormulaOrTerm Identity Formula where +-- elimFormulaOrTerm k _ x = k x -instance FormulaOrTerm Term where - elimFormulaOrTerm _ k x = k x +-- instance FormulaOrTerm Identity Term where +-- elimFormulaOrTerm _ k x = k x + +class FreeVars a where + -- | Obtain the free variables from a formula or term + freeVars :: a -> Set V --- | Get the free variables -free_vars :: forall a. (FormulaOrTerm a) => a -> Set String -free_vars = elimFormulaOrTerm free_vars0 free_vars0 - -- | Universally quantify all free variables in the formula univquant_free_vars :: Formula -> Formula univquant_free_vars cnf = - case S.toList (free_vars cnf) of + case S.toList (freeVars cnf) of [] -> cnf vars -> for_all vars cnf --- ** Internal - -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 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)) ---- modified derive-generated code ---- have this in this module to avoid orphan instances +--- Have the Arbitrary instances in this module to avoid orphan instances instance Arbitrary TPTP_Input where arbitrary = frequency [(10, @@ -218,8 +318,7 @@ x2 <- arbitrary x3 <- arbitrary x4 <- arbitrary - x5 <- arbitrary - return (AFormula x1 x2 x3 x4 x5)) + return (AFormula x1 x2 x3 x4)) , (1, do @@ -232,17 +331,15 @@ ] instance Arbitrary Formula - where arbitrary = fmap FF arbitrary + where arbitrary = fmap (F . point) arbitrary instance Arbitrary Term - where arbitrary = fmap TT arbitrary + where arbitrary = fmap (T . point) arbitrary -instance Arbitrary SourceInfo +instance Arbitrary Annotations where arbitrary = oneof [ - return NoSourceInfo - , do - x1 <- arbitrary - return (SourceInfo x1) + return NoAnnotations + , Annotations `fmap` arbitrary `ap` arbitrary ] instance Arbitrary UsefulInfo @@ -287,7 +384,7 @@ , do x1 <- arbitrary - x2 <- liftM2 (:) arbVar (argsFreq (\nargs -> vectorOf nargs arbVar)) + x2 <- liftM2 (:) arbitrary (argsFreq (\nargs -> vectorOf nargs arbitrary)) x3 <- resize (i-1) arbitrary return (Quant x1 x2 x3) @@ -320,11 +417,11 @@ where - go 0 = frequency [ (2,Var <$> arbVar), (1,FunApp `fmap` arbitrary `ap` return[] ) ] + go 0 = frequency [ (2,Var <$> arbitrary), (1,FunApp `fmap` arbitrary `ap` return[] ) ] go i = oneof [ do - x1 <- arbVar + x1 <- arbitrary return (Var x1) , arbNum NumberLitTerm @@ -350,7 +447,7 @@ where go 0 = oneof [ fmap GWord arbitrary - , fmap GVar arbVar + , fmap GVar arbitrary ] go i = @@ -368,7 +465,7 @@ return (GApp (AtomicWord x1) args) - ,GVar <$> arbVar + ,GVar <$> arbitrary ,arbNum GNumber ,GDistinctObject <$> arbPrintable @@ -405,7 +502,9 @@ return (GList args) ] --- | Tip: Use the @-XOverloadedStrings@ compiler flag if you don't want to type /AtomicWord/ to construct an 'AtomicWord' +-- | TPTP constant symbol\/predicate symbol\/function symbol identifiers (they are output in single quotes unless they are /lower_word/s). +-- +-- Tip: Use the @-XOverloadedStrings@ compiler flag if you don't want to have to type /AtomicWord/ to construct an 'AtomicWord' newtype AtomicWord = AtomicWord String deriving (Eq,Ord,Show,Data,Typeable,Read,Monoid,IsString) @@ -413,23 +512,121 @@ arbitrary = frequency [ (5, AtomicWord <$> arbLowerWord) ,(1, AtomicWord <$> arbPrintable) ] - - + +-- | Variable names +newtype V = V String + deriving (Eq,Ord,Show,Data,Typeable,Read,Monoid,IsString) + +instance Arbitrary V where + arbitrary = V <$> arbVar + -- * Fixed-point style decorated formulae and terms + + +#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]) --- | For a given type constructor @f@, make the fixed point type @Y@ satisfying: --- --- > Y = f (Term0 Y) +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) + + +-- | This class is used in several utility functions involving 'F' and 'T'. -- --- (modulo newtype wrapping). See for example 'diffFormula'. -newtype TermFix f = TermFix { runTermFix :: f (Term0 (TermFix f)) } - --- | For a given type constructor @f@, make the fixed point type @X@ satisfying: +-- Conceptually 'point' should be of type @a -> m a@, but we need the extra flexibility to make restricted monads like 'Set' instances. -- --- > X = f (Formula0 Y X) --- > Y = f (Term0 Y) +-- Note: We have @instance (Monad m) => Pointed a (m a)@, but Haddock currently doesn't display this. +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 + +-- | This class is used in several utility functions involving 'F' and 'T'. -- --- (modulo newtype wrapping). See for example 'diffTerm'. -newtype FormulaFix f = FormulaFix { runFormulaFix :: f (Formula0 (TermFix f) (FormulaFix f)) } - - +-- Conceptually 'copoint' should be of type @w a -> a@, but let's keep the extra flexibility. +class Copointed a b | b -> a where + copoint :: b -> a + +instance Copointed a (Identity a) where + copoint (Identity x) = x + +-- * Utility functions + +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 + + +-- | Eliminate formulae +foldF :: + (Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t)))) => + (F t -> r) -- ^ Handle negation + -> (Quant -> [V] -> F t -> r) -- ^ Handle quantification + -> (F t -> BinOp -> F t -> r) -- ^ Handle binary op + -> (T t -> InfixPred -> T t -> r) -- ^ Handle equality/inequality + -> (AtomicWord -> [T t] -> r) -- ^ Handle predicate symbol application + -> (F t -> r) -- ^ Handle formula + +foldF kneg kquant kbinop kinfix kpredapp f = foldFormula0 kneg kquant kbinop kinfix kpredapp (unwrapF f) + +-- | Eliminate terms +foldT :: + (Copointed (Term0 (T t)) (t (Term0 (T t)))) => + (String -> r) -- ^ Handle string literal + -> (Double -> r) -- ^ Handle number literal + -> (V -> r) -- ^ Handle variable + -> (AtomicWord -> [T t] -> r) -- ^ Handle function symbol application + -> (T t -> r) -- ^ Handle term +foldT kdistinct knum kvar kfunapp t = foldTerm0 kdistinct knum kvar kfunapp (unwrapT t) diff --git a/Codec/TPTP/Diff.hs b/Codec/TPTP/Diff.hs --- a/Codec/TPTP/Diff.hs +++ b/Codec/TPTP/Diff.hs @@ -13,12 +13,12 @@ --import Test.QuickCheck.Instances import Test.QuickCheck hiding((.&.)) import Data.Char() -import Control.Monad import Debug.Trace() import Codec.TPTP.Base import Codec.TPTP.Pretty import Text.PrettyPrint.ANSI.Leijen import System.UTF8IO +import Control.Monad.Identity @@ -137,17 +137,17 @@ -- runDiffTerm :: Term -- -> Term --- -> DiffResult (Term0 (TermFix DiffResult)) --- runDiffTerm t1 t2 = runTermFix (diffTerm t1 t2) +-- -> DiffResult (Term0 (T DiffResult)) +-- runDiffTerm t1 t2 = runT (diffTerm t1 t2) -diffTerm :: Term -> Term -> TermFix DiffResult -diffTerm (TT t1) (TT t2) = TermFix $ +diffTerm :: Term -> Term -> T DiffResult +diffTerm (T (Identity t1)) (T (Identity t2)) = T $ case (t1,t2) of - (FunApp x1 args1,FunApp x2 args2) -> handleAppExpr diffTerm TermFix runTermFix FunApp x1 args1 x2 args2 + (FunApp x1 args1,FunApp x2 args2) -> handleAppExpr diffTerm T runT FunApp x1 args1 x2 args2 (Var x1,Var x2) -> handleLeaf Var x1 x2 (DistinctObjectTerm x1, DistinctObjectTerm x2) -> handleLeaf DistinctObjectTerm x1 x2 (NumberLitTerm x1, NumberLitTerm x2) -> handleLeaf NumberLitTerm x1 x2 - _ -> let plug=plugSubterms (TermFix DontCare) in Differ (plug t1) (plug t2) + _ -> let plug=plugSubterms (T DontCare) in Differ (plug t1) (plug t2) plugSubterms :: forall a a1. a -> Term0 a1 -> Term0 a plugSubterms p t = case t of @@ -167,56 +167,56 @@ -diffFormula :: Formula -> Formula -> FormulaFix DiffResult -diffFormula (FF f1) (FF f2) = FormulaFix $ +diffFormula :: Formula -> Formula -> F DiffResult +diffFormula (F (Identity f1)) (F (Identity f2)) = F $ case (f1,f2) of ( Quant q1 vars1 g1 ,Quant q2 vars2 g2) -> case (q1==q2, vars1==vars2) of - (True,True) -> handleUnary diffFormula FormulaFix runFormulaFix (Quant q1 vars1) g1 g2 - _ -> Differ (Quant q1 vars1 (FormulaFix DontCare)) - (Quant q2 vars2 (FormulaFix DontCare)) + (True,True) -> handleUnary diffFormula F runF (Quant q1 vars1) g1 g2 + _ -> Differ (Quant q1 vars1 (F DontCare)) + (Quant q2 vars2 (F DontCare)) ( BinOp l1 op1 r1 - ,BinOp l2 op2 r2 ) -> handleBinExpr diffFormula FormulaFix runFormulaFix BinOp l1 op1 r1 l2 op2 r2 + ,BinOp l2 op2 r2 ) -> handleBinExpr diffFormula F runF BinOp l1 op1 r1 l2 op2 r2 ( InfixPred l1 op1 r1 - ,InfixPred l2 op2 r2 ) -> handleBinExpr diffTerm TermFix runTermFix InfixPred l1 op1 r1 l2 op2 r2 + ,InfixPred l2 op2 r2 ) -> handleBinExpr diffTerm T runT InfixPred l1 op1 r1 l2 op2 r2 ( (:~:) g1 - ,(:~:) g2 ) -> handleUnary diffFormula FormulaFix runFormulaFix (:~:) g1 g2 + ,(:~:) g2 ) -> handleUnary diffFormula F runF (:~:) g1 g2 ( PredApp x1 args1 - ,PredApp x2 args2 ) -> handleAppExpr diffTerm TermFix runTermFix PredApp x1 args1 x2 args2 + ,PredApp x2 args2 ) -> handleAppExpr diffTerm T runT PredApp x1 args1 x2 args2 - _ -> let plug=plugSubformulae (TermFix DontCare) (FormulaFix DontCare) in Differ (plug f1) (plug f2) + _ -> let plug=plugSubformulae (T DontCare) (F DontCare) in Differ (plug f1) (plug f2) -instance Show (TermFix DiffResult) where - show (TermFix t) = show t +instance Show (T DiffResult) where + show (T t) = show t -instance Show (FormulaFix DiffResult) where - show (FormulaFix f) = show f +instance Show (F DiffResult) where + show (F f) = show f -type T0Diff = DiffResult (Term0 (TermFix DiffResult)) -type F0Diff = DiffResult (Formula0 (TermFix DiffResult) (FormulaFix DiffResult)) +type T0Diff = DiffResult (Term0 (T DiffResult)) +type F0Diff = DiffResult (Formula0 (T DiffResult) (F DiffResult)) wildcard :: AtomicWord wildcard = "_" instance Pretty (WithEnclosing T0Diff) where - pretty = prettyHelper (plugSubterms (TT (FunApp wildcard []))) + pretty = prettyHelper --(plugSubterms (fApp wildcard [])) instance Pretty (WithEnclosing F0Diff) where - pretty = prettyHelper (plugSubformulae (TT (FunApp wildcard [])) (FF (PredApp wildcard []))) + pretty = prettyHelper --(plugSubformulae (fApp wildcard []) (pApp wildcard [])) -prettyHelper :: forall t a. - (Pretty (WithEnclosing t), Pretty (WithEnclosing a)) => - (t -> a) -> WithEnclosing (DiffResult t) -> Doc -prettyHelper _ (WithEnclosing _ d) = +prettyHelper :: forall t. + (Pretty (WithEnclosing t)) => + WithEnclosing (DiffResult t) -> Doc +prettyHelper (WithEnclosing _ d) = let pwe = pretty . WithEnclosing EnclNothing in @@ -235,15 +235,15 @@ , pwe y ] -deriving instance Pretty (TermFix DiffResult) +deriving instance Pretty (T DiffResult) -deriving instance Pretty (FormulaFix DiffResult) +deriving instance Pretty (F DiffResult) -instance Pretty (WithEnclosing (TermFix DiffResult)) where - pretty (WithEnclosing x (TermFix y)) = pretty (WithEnclosing x y) +instance Pretty (WithEnclosing (T DiffResult)) where + pretty (WithEnclosing x (T y)) = pretty (WithEnclosing x y) -instance Pretty (WithEnclosing (FormulaFix DiffResult)) where - pretty (WithEnclosing x (FormulaFix y)) = pretty (WithEnclosing x y) +instance Pretty (WithEnclosing (F DiffResult)) where + pretty (WithEnclosing x (F y)) = pretty (WithEnclosing x y) instance Pretty (T0Diff) where pretty = pretty . WithEnclosing EnclNothing @@ -251,18 +251,18 @@ instance Pretty (F0Diff) where pretty = pretty . WithEnclosing EnclNothing --- instance Pretty (DiffResult (TermFix DiffResult)) where --- pretty = pretty . WithEnclosing EnclNothing . TermFix +-- instance Pretty (DiffResult (T DiffResult)) where +-- pretty = pretty . WithEnclosing EnclNothing . T --- instance Pretty (DiffResult (TermFix DiffResult) (FormulaFix DiffResult)) where --- pretty = pretty . WithEnclosing EnclNothing . FormulaFix +-- instance Pretty (DiffResult (T DiffResult) (F DiffResult)) where +-- pretty = pretty . WithEnclosing EnclNothing . F -- runFormulaDiff :: Formula -- -> Formula -- -> DiffResult --- (Formula0 (TermFix DiffResult) (FormulaFix DiffResult)) --- runFormulaDiff a b = runFormulaFix (diffFormula a b) +-- (Formula0 (T DiffResult) (F DiffResult)) +-- runFormulaDiff a b = runF (diffFormula a b) -- | Less random generator for generating formulae suitable for testing diff diffGenF :: Gen Formula @@ -315,8 +315,8 @@ -- in collect res $ True -- -- case res of --- -- SameHead ((FormulaFix Same) :&: --- -- (FormulaFix (Differ f1 +-- -- SameHead ((F Same) :&: +-- -- (F (Differ f1 instance Functor DiffResult where fmap f d = case d of @@ -331,5 +331,5 @@ class Diffable a b where diff :: a -> a -> b -instance Diffable Formula (FormulaFix DiffResult) where diff = diffFormula -instance Diffable Term (TermFix DiffResult) where diff = diffTerm +instance Diffable Formula (F DiffResult) where diff = diffFormula +instance Diffable Term (T DiffResult) where diff = diffTerm diff --git a/Codec/TPTP/Export.hs b/Codec/TPTP/Export.hs --- a/Codec/TPTP/Export.hs +++ b/Codec/TPTP/Export.hs @@ -3,6 +3,7 @@ module Codec.TPTP.Export(toTPTP',ToTPTP(..),isLowerWord) where import Codec.TPTP.Base +import Control.Monad.Identity -- | Convenient wrapper for 'toTPTP' toTPTP' :: forall a. (ToTPTP a) => a -> String @@ -32,7 +33,7 @@ instance ToTPTP TPTP_Input where toTPTP AFormula{..} = s "fof(" . toTPTP name . comma . toTPTP role . comma . - toTPTP formula . toTPTP sourceInfo . toTPTP usefulInfo . s ")." + toTPTP formula . toTPTP annotations . s ")." toTPTP (Comment x) = s x -- % included in x @@ -68,7 +69,7 @@ toTPTP q . s " [" - . commaSepMap s vars + . commaSepMap toTPTP vars . s "] : " . showParen par (toTPTP f) @@ -88,21 +89,21 @@ toTPTP term = case term of - Var x -> s x + Var x -> toTPTP x NumberLitTerm d -> shows d DistinctObjectTerm x -> showString (tptpQuote x) FunApp f [] -> toTPTP f FunApp f args -> toTPTP f . s "(" . commaSepMap toTPTP args . s ")" - +deriving instance (ToTPTP a) => (ToTPTP (Identity a)) deriving instance ToTPTP Formula deriving instance ToTPTP Term -instance ToTPTP SourceInfo where - toTPTP NoSourceInfo = s "" - toTPTP (SourceInfo x) = s "," . toTPTP x +instance ToTPTP Annotations where + toTPTP NoAnnotations = s "" + toTPTP (Annotations a b) = s "," . toTPTP a . toTPTP b instance ToTPTP UsefulInfo where toTPTP NoUsefulInfo = s "" @@ -121,7 +122,7 @@ toTPTP gd = case gd of GWord x -> toTPTP x GApp x args -> toTPTP x . s "(" . commaSepMap toTPTP args . s ")" - GVar x -> s x + GVar x -> toTPTP x GNumber x -> shows x GDistinctObject x -> showString (tptpQuote x) GFormulaData str formu -> s str . s "(" . toTPTP formu . s ")" @@ -152,3 +153,6 @@ isLowerWord str = case str of (x:xs) | isBetween 'a' x 'z' && all isReallyAlnum xs -> True _ -> False + +instance ToTPTP V where + toTPTP (V x) = s x diff --git a/Codec/TPTP/Pretty.hs b/Codec/TPTP/Pretty.hs --- a/Codec/TPTP/Pretty.hs +++ b/Codec/TPTP/Pretty.hs @@ -9,11 +9,10 @@ import Codec.TPTP.Export import Text.PrettyPrint.ANSI.Leijen import Data.Data +import Control.Monad.Identity oper :: String -> Doc oper = dullyellow . text -prettyvar :: String -> Doc -prettyvar = blue . text psym :: forall a. (Pretty a) => a -> Doc psym = green . pretty fsym :: forall a. (Pretty a) => a -> Doc @@ -88,8 +87,7 @@ [ (red.pretty) name <+> dullwhite (text "role:") <+> (magenta.text.unrole) role , pretty formula - , pretty sourceInfo - , pretty usefulInfo + , pretty annotations ,empty ] @@ -125,7 +123,7 @@ Quant q vars f -> pretty q - <+> brackets (hsep (punctuate comma (fmap prettyvar vars))) + <+> brackets (hsep (punctuate comma (fmap pretty vars))) <> dot pretty (wne f) @@ -160,7 +158,7 @@ instance (Pretty (WithEnclosing t)) => Pretty (WithEnclosing (Term0 t)) where pretty (WithEnclosing _ x) = case x of - Var s -> prettyvar s + Var s -> pretty s NumberLitTerm d -> text (show d) DistinctObjectTerm s -> cyan (dquotes (text s)) FunApp f [] -> fsym f @@ -169,19 +167,20 @@ instance Pretty (Formula0 Term Formula) where - pretty = pretty . WithEnclosing EnclNothing . FF + pretty = pretty . WithEnclosing EnclNothing . F . Identity instance Pretty (Term0 Term) where - pretty = pretty . WithEnclosing EnclNothing . TT + pretty = pretty . WithEnclosing EnclNothing . T . Identity instance Pretty (WithEnclosing Formula) where - pretty (WithEnclosing x (FF y)) = pretty (WithEnclosing x y) + pretty (WithEnclosing x (F (Identity y))) = pretty (WithEnclosing x y) instance Pretty (WithEnclosing Term) where - pretty (WithEnclosing x (TT y)) = pretty (WithEnclosing x y) + pretty (WithEnclosing x (T (Identity y))) = pretty (WithEnclosing x y) deriving instance Pretty Formula deriving instance Pretty Term +deriving instance Pretty a => Pretty (Identity a) -- instance (Pretty f, Pretty t) => Pretty (Formula0 t f) where -- pretty = pretty . WithEnclosing "" @@ -192,12 +191,12 @@ prettySimple :: Pretty a => a -> String prettySimple x = displayS (renderPretty 0.9 80 (pretty x)) "" -instance Pretty SourceInfo where - pretty NoSourceInfo = dullwhite . text $ "NoSourceInfo" - pretty (SourceInfo x) = dullwhite (text "SourceInfo: ") <+> pretty x +instance Pretty Annotations where + pretty NoAnnotations = dullwhite . text $ "NoAnnotations" + pretty (Annotations a b) = dullwhite (text "SourceInfo: ") <+> pretty a <+> pretty b instance Pretty UsefulInfo where - pretty NoUsefulInfo = dullwhite . text $ "NoUsefulInfo" + pretty NoUsefulInfo = empty pretty (UsefulInfo x) = dullwhite (text "UsefulInfo: ") <+> pretty x @@ -209,7 +208,7 @@ pretty (GApp x []) = fsym x pretty (GApp x args) = fsym x <+> prettyargs args pretty (GFormulaData s f) = text s <> align (parens (pretty f)) - pretty (GVar x) = prettyvar x + pretty (GVar x) = pretty x instance Pretty AtomicWord where pretty (AtomicWord x) = (if isLowerWord x then text else squotes.text) x @@ -222,3 +221,6 @@ f "[" <+> (fillSep . punctuate comma . fmap pretty) xs <+> f "]" + +instance Pretty V where + pretty (V x) = blue . text $ x diff --git a/Codec/TPTP/QuickCheck.hs b/Codec/TPTP/QuickCheck.hs --- a/Codec/TPTP/QuickCheck.hs +++ b/Codec/TPTP/QuickCheck.hs @@ -46,6 +46,10 @@ arbLowerWord = (:) `fmap` elements ['a'..'z'] `ap` listOf (elements (['a'..'z']++['A'..'Z']++"_")) +arbUpperWord :: Gen String +arbUpperWord = (:) `fmap` elements ['A'..'Z'] `ap` listOf (elements (['a'..'z']++['A'..'Z']++"_")) + + arbNum :: forall a a1. (Arbitrary a, Num a) => (a -> a1) -> Gen a1 arbNum f = frequency [(1,fmap f arbitrary) diff --git a/Parser.y b/Parser.y --- a/Parser.y +++ b/Parser.y @@ -11,6 +11,7 @@ import Codec.TPTP.Base import System.IO import System.IO.Unsafe +import Control.Monad.Identity } %name parseTPTP @@ -82,16 +83,16 @@ fof_annotated :: {TPTP_Input} fof_annotated : fof lp name comma formula_role comma fof_formula annotations rp dot - { AFormula $3 $5 $7 (fst $8) (snd $8) } + { AFormula $3 $5 $7 $8 } cnf_annotated :: {TPTP_Input} cnf_annotated : cnf lp name comma formula_role comma cnf_formula annotations rp dot - { AFormula $3 $5 (univquant_free_vars $7) (fst $8)(snd $8) } + { AFormula $3 $5 (univquant_free_vars $7) $8 } -annotations :: { (SourceInfo,UsefulInfo) } -annotations : comma source optional_info { ($2,$3) } - | { (NoSourceInfo, NoUsefulInfo) } +annotations :: { Annotations } +annotations : comma source optional_info { Annotations $2 $3 } + | { NoAnnotations } formula_role :: {Role} formula_role : lower_word_ { Role $1 } @@ -142,7 +143,7 @@ quantified_formula : quantifier lbra variable_list rbra colon unitary_formula { $1 $3 $6 } -variable_list :: {[String]} +variable_list :: {[V]} variable_list : variable { [$1] } | variable comma variable_list { $1 : $3 } @@ -178,7 +179,7 @@ fol_infix_unary :: {Formula} fol_infix_unary : term infix_inequality term { $2 $1 $3 } -quantifier :: {[String] -> Formula -> Formula} +quantifier :: {[V] -> Formula -> Formula} quantifier : exclam { for_all } | question { exists } binary_connective :: {Formula -> Formula -> Formula} @@ -207,7 +208,7 @@ plain_atomic_formula :: {Formula} -plain_atomic_formula : plain_term {let TT (FunApp x args) = $1 in pApp x args} +plain_atomic_formula : plain_term { fApp2pApp $1 } -- plain_atomic_formula :== proposition | predicate lp arguments rp -- proposition :== predicate @@ -218,7 +219,7 @@ | defined_infix_formula {$1} defined_plain_formula :: {Formula} -defined_plain_formula : defined_plain_term {let TT (FunApp x args) = $1 in pApp x args} +defined_plain_formula : defined_plain_term {fApp2pApp $1} --defined_plain_formula :== defined_prop | defined_pred lp arguments rp --defined_prop :== atomic_defined_word @@ -240,7 +241,7 @@ infix_inequality : nequals { (.!=.) } system_atomic_formula :: {Formula} -system_atomic_formula : system_term {let TT (FunApp x args) = $1 in pApp x args} +system_atomic_formula : system_term {fApp2pApp $1} term :: {Term} term : function_term {$1} @@ -295,15 +296,15 @@ system_functor :: {String} system_functor : atomic_system_word {$1} -variable :: {String} -variable : upper_word {$1} +variable :: {V} +variable : upper_word {V $1} arguments :: {[Term]} arguments : term {[$1]} | term comma arguments { $1 : $3 } -source :: {SourceInfo} -source : general_term {SourceInfo $1} +source :: {GTerm} +source : general_term {$1} -- source :== dag_source | internal_source | external_source | unknown @@ -418,6 +419,6 @@ go ('\\':which:xs) = which:go xs go (x:xs) = x:go xs - +fApp2pApp (T (Identity (FunApp x args))) = (F (Identity (PredApp x args))) } diff --git a/dist/build/Parser.hs b/dist/build/Parser.hs --- a/dist/build/Parser.hs +++ b/dist/build/Parser.hs @@ -12,6 +12,7 @@ import Codec.TPTP.Base import System.IO import System.IO.Unsafe +import Control.Monad.Identity #if __GLASGOW_HASKELL__ >= 503 import qualified Data.Array as Happy_Data_Array #else @@ -61,10 +62,10 @@ happyOut8 :: (HappyAbsSyn ) -> (TPTP_Input) happyOut8 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut8 #-} -happyIn9 :: ((SourceInfo,UsefulInfo)) -> (HappyAbsSyn ) +happyIn9 :: (Annotations) -> (HappyAbsSyn ) happyIn9 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyIn9 #-} -happyOut9 :: (HappyAbsSyn ) -> ((SourceInfo,UsefulInfo)) +happyOut9 :: (HappyAbsSyn ) -> (Annotations) happyOut9 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut9 #-} happyIn10 :: (Role) -> (HappyAbsSyn ) @@ -133,10 +134,10 @@ happyOut20 :: (HappyAbsSyn ) -> (Formula) happyOut20 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut20 #-} -happyIn21 :: ([String]) -> (HappyAbsSyn ) +happyIn21 :: ([V]) -> (HappyAbsSyn ) happyIn21 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyIn21 #-} -happyOut21 :: (HappyAbsSyn ) -> ([String]) +happyOut21 :: (HappyAbsSyn ) -> ([V]) happyOut21 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut21 #-} happyIn22 :: (Formula) -> (HappyAbsSyn ) @@ -175,10 +176,10 @@ happyOut27 :: (HappyAbsSyn ) -> (Formula) happyOut27 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut27 #-} -happyIn28 :: ([String] -> Formula -> Formula) -> (HappyAbsSyn ) +happyIn28 :: ([V] -> Formula -> Formula) -> (HappyAbsSyn ) happyIn28 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyIn28 #-} -happyOut28 :: (HappyAbsSyn ) -> ([String] -> Formula -> Formula) +happyOut28 :: (HappyAbsSyn ) -> ([V] -> Formula -> Formula) happyOut28 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut28 #-} happyIn29 :: (Formula -> Formula -> Formula) -> (HappyAbsSyn ) @@ -331,10 +332,10 @@ happyOut53 :: (HappyAbsSyn ) -> (String) happyOut53 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut53 #-} -happyIn54 :: (String) -> (HappyAbsSyn ) +happyIn54 :: (V) -> (HappyAbsSyn ) happyIn54 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyIn54 #-} -happyOut54 :: (HappyAbsSyn ) -> (String) +happyOut54 :: (HappyAbsSyn ) -> (V) happyOut54 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut54 #-} happyIn55 :: ([Term]) -> (HappyAbsSyn ) @@ -343,10 +344,10 @@ happyOut55 :: (HappyAbsSyn ) -> ([Term]) happyOut55 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut55 #-} -happyIn56 :: (SourceInfo) -> (HappyAbsSyn ) +happyIn56 :: (GTerm) -> (HappyAbsSyn ) happyIn56 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyIn56 #-} -happyOut56 :: (HappyAbsSyn ) -> (SourceInfo) +happyOut56 :: (HappyAbsSyn ) -> (GTerm) happyOut56 x = Happy_GHC_Exts.unsafeCoerce# x {-# INLINE happyOut56 #-} happyIn57 :: (UsefulInfo) -> (HappyAbsSyn ) @@ -672,7 +673,7 @@ case happyOut11 happy_x_7 of { happy_var_7 -> case happyOut9 happy_x_8 of { happy_var_8 -> happyIn7 - (AFormula happy_var_3 happy_var_5 happy_var_7 (fst happy_var_8) (snd happy_var_8) + (AFormula happy_var_3 happy_var_5 happy_var_7 happy_var_8 ) `HappyStk` happyRest}}}} happyReduce_9 = happyReduce 10# 4# happyReduction_9 @@ -692,7 +693,7 @@ case happyOut23 happy_x_7 of { happy_var_7 -> case happyOut9 happy_x_8 of { happy_var_8 -> happyIn8 - (AFormula happy_var_3 happy_var_5 (univquant_free_vars happy_var_7) (fst happy_var_8)(snd happy_var_8) + (AFormula happy_var_3 happy_var_5 (univquant_free_vars happy_var_7) happy_var_8 ) `HappyStk` happyRest}}}} happyReduce_10 = happySpecReduce_3 5# happyReduction_10 @@ -702,12 +703,12 @@ = case happyOut56 happy_x_2 of { happy_var_2 -> case happyOut57 happy_x_3 of { happy_var_3 -> happyIn9 - ((happy_var_2,happy_var_3) + (Annotations happy_var_2 happy_var_3 )}} happyReduce_11 = happySpecReduce_0 5# happyReduction_11 happyReduction_11 = happyIn9 - ((NoSourceInfo, NoUsefulInfo) + (NoAnnotations ) happyReduce_12 = happySpecReduce_1 6# happyReduction_12 @@ -1056,7 +1057,7 @@ happyReduction_56 happy_x_1 = case happyOut42 happy_x_1 of { happy_var_1 -> happyIn32 - (let TT (FunApp x args) = happy_var_1 in pApp x args + (fApp2pApp happy_var_1 )} happyReduce_57 = happySpecReduce_1 29# happyReduction_57 @@ -1077,7 +1078,7 @@ happyReduction_59 happy_x_1 = case happyOut48 happy_x_1 of { happy_var_1 -> happyIn34 - (let TT (FunApp x args) = happy_var_1 in pApp x args + (fApp2pApp happy_var_1 )} happyReduce_60 = happySpecReduce_3 31# happyReduction_60 @@ -1114,7 +1115,7 @@ happyReduction_64 happy_x_1 = case happyOut51 happy_x_1 of { happy_var_1 -> happyIn39 - (let TT (FunApp x args) = happy_var_1 in pApp x args + (fApp2pApp happy_var_1 )} happyReduce_65 = happySpecReduce_1 36# happyReduction_65 @@ -1290,7 +1291,7 @@ happyReduction_87 happy_x_1 = case happyOutTok happy_x_1 of { (UpperWord happy_var_1) -> happyIn54 - (happy_var_1 + (V happy_var_1 )} happyReduce_88 = happySpecReduce_1 51# happyReduction_88 @@ -1314,7 +1315,7 @@ happyReduction_90 happy_x_1 = case happyOut62 happy_x_1 of { happy_var_1 -> happyIn56 - (SourceInfo happy_var_1 + (happy_var_1 )} happyReduce_91 = happySpecReduce_2 53# happyReduction_91 @@ -1673,6 +1674,8 @@ go ('\\':'\\':xs) = '\\':go xs go ('\\':which:xs) = which:go xs go (x:xs) = x:go xs + +fApp2pApp (T (Identity (FunApp x args))) = (F (Identity (PredApp x args))) {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "templates/GenericTemplate.hs" #-} {-# LINE 1 "" #-} diff --git a/logic-TPTP.cabal b/logic-TPTP.cabal --- a/logic-TPTP.cabal +++ b/logic-TPTP.cabal @@ -1,12 +1,12 @@ name: logic-TPTP -version: 0.1 +version: 0.2.0 cabal-version: >= 1.6 build-type: Simple license: GPL license-file: LICENSE maintainer: Daniel Schüssler bug-reports: mailto:daniels@community.haskell.org -synopsis: Import, export and other utilities for TPTP, a syntax for first-order logic +synopsis: Import, export etc. for TPTP, a syntax for first-order logic description: For information about the TPTP format, see . . @@ -20,13 +20,13 @@ . - QuickCheck instances (generation of random formulae) . - - 'diff' : Get a \"formula\" which concisely represents the differences between two given formulae (equal subexpressions are truncated; so are the subexpressions of subexpressions whose heads already differ) + - 'diff' : Get a \"formula\" which represents the differences between two given formulae (equal subexpressions are truncated; so are the subexpressions of subexpressions whose heads already differ) . Tests passed: . - For randomly generated formulae, @parse . toTPTP == id@ . - - For each problem in the TPTP library (v 3.7.0.0) which doesn't contain the string \"thf(\", @parse . toTPTP . parse == parse@ + - For the @.p@ files in the TPTP (v 3.7.0.0) distribution's @PROBLEMS@ subtree which don't contain the string \"thf(\", @parse . toTPTP . parse == parse@ . Not yet implemented: The new /thf/ formula type. . @@ -39,7 +39,11 @@ testing/TestImportExportRandom.hs testing/TestImportExportImportFile.hs testing/PrettyPrintFile.hs - testing/PrettyPrintFile.hs + testing/ParseRandom.hs + testing/Common.hs + testing/profiling.sh + testing/Prof.hs + profiling-build.sh tested-with: GHC==6.10.2 @@ -52,9 +56,15 @@ Library ghc-options: -O2 - build-depends: base >=4 ,array, syb, containers, haskell98 - , ansi-wl-pprint, QuickCheck>=2 + build-depends: base >=4 + , array + , syb + , containers + , haskell98 + , ansi-wl-pprint + , QuickCheck >= 2 , utf8-prelude + , mtl exposed-modules: Codec.TPTP.Import ,Codec.TPTP.Base diff --git a/profiling-build.sh b/profiling-build.sh new file mode 100644 --- /dev/null +++ b/profiling-build.sh @@ -0,0 +1,4 @@ +set -e + +cabal clean +cabal install --enable-library-profiling --ghc-option=-auto-all --disable-documentation diff --git a/testing/Common.hs b/testing/Common.hs new file mode 100644 --- /dev/null +++ b/testing/Common.hs @@ -0,0 +1,75 @@ +{-# OPTIONS + -fglasgow-exts + -XCPP + -XTemplateHaskell + -XNamedFieldPuns + -XRecordWildCards + -XDeriveDataTypeable + -XOverlappingInstances + -XPackageImports + -fwarn-incomplete-patterns + #-} + +module Common where + +import Control.Monad +import Control.Monad.State +import Control.Applicative((<$>),(<*>)) +import Control.Arrow +import Text.Printf.TH +import Data.Maybe +import Data.List as L +import Data.Map as M +import Data.Set as S +import qualified Data.ByteString as B +import Data.Function +import System.Process +import System.UTF8IO +import Control.Arrow +import Debug.Trace +import Prelude() +import UTF8Prelude hiding(catch) +import System.SimpleArgs +import Data.Generics +import Test.QuickCheck +import Data.Monoid +import Text.PrettyPrint.ANSI.Leijen +import System.Exit +import Text.Regex.PCRE.Light.Char8 + +import "logic-TPTP" Codec.TPTP + + +data AFormulaComparison = OtherSame | OtherDiff String String | FormulaDiff (F DiffResult) + +instance Monoid AFormulaComparison where + mempty = OtherSame + + -- keep the most interesting comparison result + mappend OtherSame y = y + mappend x OtherSame = x + mappend x@(OtherDiff _ _) y@(FormulaDiff (F y0)) = if isSame y0 then y else x + mappend x@(FormulaDiff (F x0)) y@(OtherDiff _ _) = if isSame x0 then x else y + mappend x@(OtherDiff _ _) y@(OtherDiff _ _) = x + mappend x@(FormulaDiff _ ) y@(FormulaDiff _ ) = x + +instance Pretty AFormulaComparison where + pretty (OtherSame) = dullgreen.text$"OtherSame" + pretty (OtherDiff x y) = sep + [dullred.text$"OtherDiff" + ,pretty x + ,pretty y + ] + pretty (FormulaDiff fd) = pretty fd + +compareOther x y = if x==y then OtherSame else OtherDiff (show x) (show y) + +diffAFormula (AFormula a b c d) (AFormula a1 b1 c1 d1) = + mconcat [ compareOther a a1 + , compareOther b b1 + , FormulaDiff (diff c c1) + , compareOther d d1 + ] +diffAFormula x y = compareOther x y + +isThf = let re = compile "thf\\(" [] in (\x -> match re x [] /= Nothing) diff --git a/testing/ParseRandom.hs b/testing/ParseRandom.hs new file mode 100644 --- /dev/null +++ b/testing/ParseRandom.hs @@ -0,0 +1,58 @@ +{-# OPTIONS + -fglasgow-exts + -XCPP + -XTemplateHaskell + -XNamedFieldPuns + -XRecordWildCards + -XDeriveDataTypeable + -XOverlappingInstances + -XPackageImports + -fwarn-incomplete-patterns + #-} + +module ParseRandom where + +import Control.Monad +import Control.Monad.State +import Control.Applicative((<$>),(<*>)) +import Control.Arrow +import Text.Printf.TH +import Data.Maybe +import Data.List as L +import Data.Map as M +import Data.Set as S +import qualified Data.ByteString as B +import Data.Function +import System.Process +import System.UTF8IO +import Control.Arrow +import Debug.Trace +import Prelude() +import UTF8Prelude hiding(catch) +import System.SimpleArgs +import Data.Generics +import Test.QuickCheck +import Data.Monoid +import Text.PrettyPrint.ANSI.Leijen +import System.Exit +import Text.Regex.PCRE.Light.Char8 +import Common + +import "logic-TPTP" Codec.TPTP + +infilename = getArgs +parseRes = return . parse =<< readFile =<< infilename + +--main = forever $ quickCheck prop_test_ie --iei_i + +--main = stressTestParser + +main = stressTestParser + +stressTestParser = replicateM 100 $ + do + n <- getArgs + x <- head `fmap` sample' (resize n arbitrary) :: IO TPTP_Input + let tptp = toTPTP' [x] + putStrLn tptp + putStrLn (prettySimple (parse tptp)) diff --git a/testing/Prof.hs b/testing/Prof.hs new file mode 100644 --- /dev/null +++ b/testing/Prof.hs @@ -0,0 +1,45 @@ +{-# OPTIONS + -fglasgow-exts + -XCPP + -XTemplateHaskell + -XNamedFieldPuns + -XRecordWildCards + -XDeriveDataTypeable + -XOverlappingInstances + -XPackageImports + -fwarn-incomplete-patterns + -XNoImplicitPrelude + #-} + +module Prof where + +import Control.Monad.State(Monad(..), Functor(..), (=<<), + replicateM, unless) +import Codec.TPTP(TPTP_Input, parse, toTPTP') +import Test.QuickCheck(Arbitrary(arbitrary)) +import Test.QuickCheck.Gen(Gen(unGen)) +import System.SimpleArgs(Args(..)) +import UTF8Prelude(Eq((==)), GHC.Num.Num, Show(show), Bool, IO, + (.), and, unlines, words, print, writeFile, fromInteger) +import System.Random(newStdGen) + + +size = 100 + +randomF :: IO TPTP_Input +randomF = (\seed -> unGen arbitrary seed size) `fmap` newStdGen + +main = do + reps <- getArgs + print . and =<< replicateM reps (do + f <- randomF + let res = checkit f + -- unless res (print f >> replicateM 20 (putChar '-') >> print (parse(toTPTP' [f]))) + unless res (writeFile "tmp1" (format [f]) >> writeFile "tmp2" (format (parse (toTPTP' [f])))) + return res + ) + +checkit :: TPTP_Input -> Bool +checkit f = [f] == parse (toTPTP' [f]) + +format = unlines . words . show diff --git a/testing/TestImportExportImportFile.hs b/testing/TestImportExportImportFile.hs --- a/testing/TestImportExportImportFile.hs +++ b/testing/TestImportExportImportFile.hs @@ -41,27 +41,40 @@ import "logic-TPTP" Codec.TPTP -main = diff_once_twice +main = do + files <- lines `fmap` getContents + --print (length files) + print_export <- getArgs + forM_ files (diff_once_twice print_export) + exitWith ExitSuccess -diff_once_twice = do +diff_once_twice print_export infilename' = do --let tmp = "/tmp/tmp.tptp" - (infilename',print_export) <- getArgs putStrLn infilename' input <- readFile infilename' - when (isThf input) $ (putStrLn . prettySimple . yellow . text $ "Skipping Thf") >> exitWith ExitSuccess - let once = parse input - let tptp = toTPTP' once - when print_export (putStrLn $ "new tptp = " ++tptp) - let twice = parse tptp - let dif = mconcat (zipWith diffAFormula once twice) - let success = (putStrLn . prettySimple . dullgreen . text $ "Ok") >> exitWith ExitSuccess - - case dif of - OtherSame -> success - FormulaDiff (FormulaFix Same) -> success - _ -> do - putStrLn . prettySimple $ dif - exitWith (ExitFailure 1) - - - + if (isThf input) + then putStrLn . prettySimple . yellow . text $ "Skipping Thf" + else do + + let once = parse input + let tptp = toTPTP' once + when print_export (putStrLn $ "new tptp = " ++tptp) + let twice = parse tptp + let dif = mconcat (zipWith diffAFormula once twice) + let success = (putStrLn . prettySimple . dullgreen . text $ "Ok") + + -- case dif of + -- OtherSame -> success + -- FormulaDiff (F Same) -> success + -- _ -> do + -- putStrLn . prettySimple $ dif + -- exitWith (ExitFailure 1) + + if once==twice + then success + else do + putStrLn . prettySimple $ dif + exitWith (ExitFailure 1) + + + diff --git a/testing/TestImportExportRandom.hs b/testing/TestImportExportRandom.hs --- a/testing/TestImportExportRandom.hs +++ b/testing/TestImportExportRandom.hs @@ -40,23 +40,25 @@ import "logic-TPTP" Codec.TPTP -main = quickCheck prop_test_ie +main = quickCheckWith (stdArgs { maxSuccess = 5000 }) prop_test_ie prop_test_ie f = let tptp = toTPTP' [f] in (let - [g] = parse $ trace tptp tptp + [g] = parse tptp -- $ trace tptp tptp dif = diffAFormula f g in whenFail (putStrLn . prettySimple $ dif) - (case dif of - OtherSame -> True - FormulaDiff (FormulaFix Same) -> True - _ -> False - )) + (f==g) + + -- (case dif of + -- OtherSame -> True + -- FormulaDiff (F Same) -> True + -- _ -> False + -- )) - + ) diff --git a/testing/compileTests.sh b/testing/compileTests.sh --- a/testing/compileTests.sh +++ b/testing/compileTests.sh @@ -7,6 +7,6 @@ for x in TestImportExportImportFile TestImportExportRandom PrettyPrintFile ParseRandom; do - ghc -outputdir obj -o bin/$x --make -O2 -main-is $x $x + ghc -prof -auto-all -outputdir obj -o bin/$x --make -O2 -main-is $x $x done diff --git a/testing/profiling.sh b/testing/profiling.sh new file mode 100644 --- /dev/null +++ b/testing/profiling.sh @@ -0,0 +1,14 @@ +#!/bin/bash + +set -e + +mkdir -p bin +mkdir -p obj + +x=Prof +ghc -fforce-recomp -prof -auto-all -outputdir obj -o bin/$x --make -O2 -main-is $x $x + +echo "Running..." +bin/$x +RTS -P -RTS 1000 +x-www-browser "$x.prof" +