logic-TPTP 0.1 → 0.2.0

raw patch · 16 files changed

+684/−252 lines, 16 filesdep +mtlPVP ok

version bump matches the API change (PVP)

Dependencies added: mtl

API changes (from Hackage documentation)

Files

• Codec/TPTP/Base.hs +311/−114
• Codec/TPTP/Diff.hs +45/−45
• Codec/TPTP/Export.hs +12/−8
• Codec/TPTP/Pretty.hs +17/−15
• Codec/TPTP/QuickCheck.hs +4/−0
• Parser.y +16/−15
• dist/build/Parser.hs +22/−19
• logic-TPTP.cabal +17/−7
• profiling-build.sh +4/−0
• testing/Common.hs +75/−0
• testing/ParseRandom.hs +58/−0
• testing/Prof.hs +45/−0
• testing/TestImportExportImportFile.hs +33/−20
• testing/TestImportExportRandom.hs +10/−8
• testing/compileTests.sh +1/−1
• testing/profiling.sh +14/−0

@@ -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 <http://haskell.org/haskellwiki/Indirect_composite> 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 <http://haskell.org/haskellwiki/Indirect_composite> 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 <http://haskell.org/haskellwiki/Indirect_composite> 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)

@@ -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

@@ -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

@@ -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

@@ -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)

@@ -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)))  } 

@@ -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 "<built-in>" #-}

@@ -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 <daniels@community.haskell.org> 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 <http://www.cs.miami.edu/~tptp/>.  .@@ -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

@@ -0,0 +1,4 @@+set -e++cabal clean +cabal install --enable-library-profiling --ghc-option=-auto-all --disable-documentation

@@ -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)

@@ -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))

@@ -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

@@ -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)+++

@@ -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+          -- ))                 -+      )

@@ -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

@@ -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"+