logic-TPTP (empty) → 0.1
raw patch · 18 files changed
+5040/−0 lines, 18 filesdep +QuickCheckdep +ansi-wl-pprintdep +arraysetup-changed
Dependencies added: QuickCheck, ansi-wl-pprint, array, base, containers, haskell98, syb, utf8-prelude
Files
- Codec/TPTP.hs +17/−0
- Codec/TPTP/Base.hs +435/−0
- Codec/TPTP/Diff.hs +335/−0
- Codec/TPTP/Export.hs +154/−0
- Codec/TPTP/Import.hs +18/−0
- Codec/TPTP/Pretty.hs +224/−0
- Codec/TPTP/QuickCheck.hs +53/−0
- LICENSE +674/−0
- Lexer.x +95/−0
- Parser.y +423/−0
- Setup.hs +24/−0
- dist/build/Lexer.hs +395/−0
- dist/build/Parser.hs +1939/−0
- logic-TPTP.cabal +69/−0
- testing/PrettyPrintFile.hs +44/−0
- testing/TestImportExportImportFile.hs +67/−0
- testing/TestImportExportRandom.hs +62/−0
- testing/compileTests.sh +12/−0
+ Codec/TPTP.hs view
@@ -0,0 +1,17 @@+module Codec.TPTP(+ module Codec.TPTP.Base+ ,module Codec.TPTP.Import+ ,module Codec.TPTP.Pretty+ ,module Codec.TPTP.Export+ ,module Codec.TPTP.Diff+ )+ where++import Codec.TPTP.Base+import Codec.TPTP.Pretty+import Codec.TPTP.Import+import Codec.TPTP.Export+import Codec.TPTP.Diff+import Text.PrettyPrint.ANSI.Leijen(Pretty(..),renderPretty,displayS,displayIO)+ +
+ Codec/TPTP/Base.hs view
@@ -0,0 +1,435 @@+{-# OPTIONS -fwarn-missing-signatures -XRecordWildCards -XCPP -XDeriveDataTypeable -fglasgow-exts -XNoMonomorphismRestriction -XTemplateHaskell -XUndecidableInstances -XGeneralizedNewtypeDeriving -Wall #-}++module Codec.TPTP.Base where+ +import Data.Generics+import Data.Set as S hiding(fold)+import Control.Applicative+--import Data.Foldable+import Prelude --hiding(concat,foldl,foldl1,foldr,foldr1)+--import Data.Foldable +--import Test.QuickCheck.Instances+import Test.QuickCheck+import Data.Char+import Control.Monad+import Codec.TPTP.QuickCheck+import Data.String+import Data.Monoid hiding(All)+ +-- * Basic undecorated formulae and terms+ +-- | Basic (undecorated) first-order formulae +newtype Formula = FF (Formula0 Term Formula)+ deriving (Eq,Ord,Show,Read,Data,Typeable)++-- | 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 + +(.~.) :: Formula -> Formula+(.~.) x = FF $ (:~:) x+ +(.=.) :: Term -> Term -> Formula+x .=. y = FF $ InfixPred x (:=:) y +(.!=.) :: Term -> Term -> Formula+x .!=. y = FF $ InfixPred x (:!=:) y + +for_all :: [String] -> Formula -> Formula+for_all vars x = FF $ Quant All vars x+ +exists :: [String] -> Formula -> Formula+exists vars x = FF $ Quant Exists vars x+ +pApp :: AtomicWord -> [Term] -> Formula+pApp x args = FF $ PredApp x args+ +var :: String -> Term+var = TT . Var+fApp :: AtomicWord -> [Term] -> Term+fApp x args = TT $ FunApp x args+numberLitTerm :: Double -> Term+numberLitTerm = TT . NumberLitTerm+distinctObjectTerm :: String -> Term+distinctObjectTerm = TT . DistinctObjectTerm+ +infixl 2 .<=>. , .=>. , .<=. , .<~>.+infixl 3 .|. , .~|.+infixl 4 .&. , .~&.+infixl 5 .=. , .!=.++-- * 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.+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+ | (:~:) 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+ | NumberLitTerm Double -- ^ Number literal+ | DistinctObjectTerm String -- ^ Double-quoted item+ | FunApp AtomicWord [term] -- ^ Function symbol application (constants are nullary functions) + deriving (Eq,Ord,Show,Read,Data,Typeable)+ +-- | Binary formula connectives +data BinOp =+ -- Please don't change the constructor names+ (:<=>:) -- ^ Equivalence+ | (:=>:) -- ^ Implication+ | (:<=:) -- ^ Implication (reverse)+ | (:&:) -- ^ AND+ | (:|:) -- ^ OR+ | (:~&:) -- ^ NAND+ | (:~|:) -- ^ NOR+ | (:<~>:) -- ^ XOR+ deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded)++-- | /Term -> Term -> Formula/ infix connectives+data InfixPred =+ -- Please don't change the constructor names+ (:=:) | (:!=:) + deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded)+ +-- | Quantifier specification+data Quant = All | Exists+ deriving (Eq,Ord,Show,Read,Data,Typeable,Enum,Bounded)+ +-- * Formula Metadata+ +-- | A line of a TPTP file: Annotated formula, comment or include statement.+data TPTP_Input = + -- | Annotated formulae+ AFormula {+ name :: AtomicWord + , role :: Role + , formula :: Formula + , sourceInfo :: SourceInfo + , usefulInfo :: UsefulInfo+ } + | Comment String+ | Include FilePath [AtomicWord]++ deriving (Eq,Ord,Show,Read,Data,Typeable)+ + + ++-- | Annotations about the formulas origin +data SourceInfo = NoSourceInfo | SourceInfo GTerm+ deriving (Eq,Ord,Show,Read,Data,Typeable)+ +-- | Misc annotations+data UsefulInfo = NoUsefulInfo | UsefulInfo [GTerm]+ deriving (Eq,Ord,Show,Read,Data,Typeable)+ +-- | Formula roles+data Role = Role { unrole :: String }+ deriving (Eq,Ord,Show,Read,Data,Typeable)+++-- | Metadata (the /general_data/ rule in TPTP's grammar)+data GData = GWord AtomicWord+ | GApp AtomicWord [GTerm]+ | GVar String+ | GNumber Double+ | GDistinctObject String+ | GFormulaData String Formula + deriving (Eq,Ord,Show,Read,Data,Typeable)+ +-- | Metadata (the /general_term/ rule in TPTP's grammar)+data GTerm = ColonSep GData GTerm + | GTerm GData+ | GList [GTerm]+ deriving (Eq,Ord,Show,Read,Data,Typeable)+ ++ ++-- * Gathering free Variables++class FormulaOrTerm a where+ elimFormulaOrTerm :: (Formula -> r) -> (Term -> r) -> a -> r++instance FormulaOrTerm Formula where+ elimFormulaOrTerm k _ x = k x+ +instance FormulaOrTerm Term where+ elimFormulaOrTerm _ k x = k x++-- | 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+ [] -> 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+ + ++++--- modified derive-generated code+--- have this in this module to avoid orphan instances++instance Arbitrary TPTP_Input+ where arbitrary = frequency [(10, + do + x1 <- AtomicWord <$> arbLowerWord+ x2 <- arbitrary+ x3 <- arbitrary+ x4 <- arbitrary+ x5 <- arbitrary+ return (AFormula x1 x2 x3 x4 x5))+ + , (1,+ do + x1 <- arbPrintable+ return (Comment ("% "++x1))+ )++ , (1, Include `fmap` arbLowerWord `ap` + listOf arbitrary)+ ]++instance Arbitrary Formula+ where arbitrary = fmap FF arbitrary++instance Arbitrary Term+ where arbitrary = fmap TT arbitrary++instance Arbitrary SourceInfo+ where arbitrary = oneof [+ return NoSourceInfo+ , do + x1 <- arbitrary+ return (SourceInfo x1)+ ]+ +instance Arbitrary UsefulInfo+ where arbitrary = oneof [+ return NoUsefulInfo+ , do + x1 <- arbitrary+ return (UsefulInfo x1)+ ]+ +instance Arbitrary Role+ where arbitrary = Role `fmap` arbLowerWord+ +#define TRACE(X) id+ +instance (Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b)++ + where arbitrary = sized (\n -> TRACE("arbitrary/Formula0") go n)++ where+ go 0 = flip PredApp [] `fmap` arbitrary+ + go i = + oneof [ do+ ileft <- choose (0,i-1)+ x1 <- resize ileft arbitrary+ x2 <- arbitrary+ x3 <- resize (i - 1 - ileft) arbitrary + return (BinOp x1 x2 x3)+ + , do + x1 <- arbitrary+ x2 <- arbitrary+ x3 <- arbitrary+ return (InfixPred x1 x2 x3)+ + , do+ x1 <- arbitrary+ x2 <- argsFreq vector+ return (PredApp x1 x2)+ + , do+ x1 <- arbitrary+ x2 <- liftM2 (:) arbVar (argsFreq (\nargs -> vectorOf nargs arbVar))+ x3 <- resize (i-1) arbitrary+ return (Quant x1 x2 x3)+ + , do+ x1 <- resize (i-1) arbitrary+ return ((:~:) x1)+ ]+ +instance Arbitrary BinOp+ where arbitrary = elements+ + [ (:<=>:)+ , (:=>:)+ , (:<=:)+ , (:&:)+ , (:|:)+ , (:~&:)+ , (:~|:)+ , (:<~>:)+ ]++instance Arbitrary InfixPred+ where arbitrary = elements [ (:=:),(:!=:) ]++instance Arbitrary Quant+ where arbitrary = elements [All,Exists]+ +instance Arbitrary a => Arbitrary (Term0 a)+ where arbitrary = sized (\n -> TRACE("arbitrary/Term0") go n)+ where+++ go 0 = frequency [ (2,Var <$> arbVar), (1,FunApp `fmap` arbitrary `ap` return[] ) ]++ go i = oneof [+ do + x1 <- arbVar+ return (Var x1)+ + , arbNum NumberLitTerm + + + , do + x1 <- arbPrintable+ return (DistinctObjectTerm x1)+ + , do + x1 <- arbitrary+ args <- argsFreq + (\nargs -> do+ parti <- arbPartition nargs (i-1)+ mapM (flip resize arbitrary) parti+ )+ + return (FunApp x1 args)+ ]++instance Arbitrary GData+ where arbitrary = sized go++ where+ go 0 = oneof [ fmap GWord arbitrary+ , fmap GVar arbVar+ ]+ + go i = + oneof + [+ GWord <$> arbitrary+ + ,do+ x1 <- arbLowerWord+ args <- argsFreq + (\nargs -> do+ parti <- arbPartition nargs (i-1)+ mapM (flip resize arbitrary) parti+ ) `suchThat` ((/=) [])+ + return (GApp (AtomicWord x1) args)+ + ,GVar <$> arbVar+ ,arbNum GNumber + + ,GDistinctObject <$> arbPrintable+ ,GFormulaData `fmap` ((:) '$' `fmap` arbLowerWord) `ap` (sized (\n -> resize (n `div` 2) arbitrary))+ ]++ + +instance Arbitrary GTerm+ where arbitrary = sized go++ where+ go 0 = fmap GTerm arbitrary++ go i =+ oneof [+ do + ileft <- choose(0,i-1)+ x1 <- resize ileft arbitrary+ x2 <- resize (i-1-ileft) arbitrary+ return (ColonSep x1 x2)+ + , do+ x1 <- arbitrary+ return (GTerm x1)+ + , do+ args <- argsFreq + (\nargs -> do+ parti <- arbPartition nargs (i-1)+ mapM (flip resize arbitrary) parti+ ) `suchThat` (/= [])+ + return (GList args)+ ]+ +-- | Tip: Use the @-XOverloadedStrings@ compiler flag if you don't want to type /AtomicWord/ to construct an 'AtomicWord' +newtype AtomicWord = AtomicWord String+ deriving (Eq,Ord,Show,Data,Typeable,Read,Monoid,IsString)+ +instance Arbitrary AtomicWord where+ arbitrary = frequency [ (5, AtomicWord <$> arbLowerWord)+ ,(1, AtomicWord <$> arbPrintable)+ ]++ +-- * Fixed-point style decorated formulae and terms++-- | For a given type constructor @f@, make the fixed point type @Y@ satisfying: +--+-- > Y = f (Term0 Y)+--+-- (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: +--+-- > X = f (Formula0 Y X) +-- > Y = f (Term0 Y)+--+-- (modulo newtype wrapping). See for example 'diffTerm'.+newtype FormulaFix f = FormulaFix { runFormulaFix :: f (Formula0 (TermFix f) (FormulaFix f)) }+ +
+ Codec/TPTP/Diff.hs view
@@ -0,0 +1,335 @@+{-# OPTIONS -fwarn-missing-signatures -XRecordWildCards -XCPP -XDeriveDataTypeable -fglasgow-exts -XNoMonomorphismRestriction -XTemplateHaskell -XUndecidableInstances -Wall -XOverloadedStrings #-}++module Codec.TPTP.Diff(Diffable(..),DiffResult(..),T0Diff,F0Diff,isSame,diffGenF,diffGenT,printSampleDiffs) where+ + +-- Warning: This module is a MESS (but it seems to work :)).+ +import Data.Generics+import Control.Applicative()+--import Data.Foldable+import Prelude hiding (putStrLn)+--import Data.Foldable +--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+ + + ++data DiffResult d = + Same -- ^ Both arguments are the same. + | SameHead d -- ^ The arguments are recursive expressions of the same form, but their subterms differ. Return a \"decorated\" term that shows where the differences are + | Differ d d -- ^ The arguments differ and are not of similar form (don't recurse)+ | DontCare+ deriving (Eq,Ord,Show,Data,Typeable,Read)+ +isSame :: forall t. DiffResult t -> Bool+isSame Same = True+isSame _ = False+ +-- | Abstraction for diff'ing [predicate symbol|function symbol|gdata] applications+-- Suggestive variable names for the case of function symbol applications+handleAppExpr :: (Eq str) => + (term -> term -> termfix DiffResult) -- ^ the diff function + + -> (DiffResult a -> termfix DiffResult) -- ^ newtype wrapper + -> (termfix DiffResult -> DiffResult a) -- ^ newtype unwrapper+ + -> (str -> [termfix DiffResult] -> b) -- ^ Application expression constructor+ + -> str -- ^ First funsym+ -> [term] -- ^ First args+ + -> str -- ^ Second funsum+ -> [term] -- ^ Second args+ + -> DiffResult b+handleAppExpr recFun newtypewrapper newtypeunwrapper constr x1 args1 x2 args2 =+ -- recurse if heads and arities agree+ case (x1==x2 && length args1 == length args2) of+ True -> + let+ rec = zipWith recFun args1 args2+ in+ case all (isSame . newtypeunwrapper) rec of+ True -> Same+ False -> SameHead (constr x1 rec) + + False -> + Differ (constr x1 (fmap (const . newtypewrapper $ DontCare) args1))+ (constr x2 (fmap (const . newtypewrapper $ DontCare) args2))+ +handleBinExpr :: + (Eq op) =>+ (term -> term -> termfix DiffResult)+ + -> (DiffResult a -> termfix DiffResult) -- ^ NT wrapper+ -> (termfix DiffResult -> DiffResult a) -- ^ NT unwrapepr+ + -> (termfix DiffResult -> op -> termfix DiffResult -> b) -- ^ constructor+ + -> term+ -> op+ -> term+ + -> term+ -> op+ -> term+ + -> DiffResult b+handleBinExpr recFun newtypewrapper newtypeunwrapper constr l1 op1 r1 l2 op2 r2 =+ case op1==op2 of+ True -> + let + recl = recFun l1 l2+ recr = recFun r1 r2+ in+ case (newtypeunwrapper recl,newtypeunwrapper recr) of+ (Same,Same) -> Same+ (_,_) -> SameHead (constr recl op1 recr)+ + False ->+ let dc = newtypewrapper DontCare + + in Differ (constr dc op1 dc)+ (constr dc op2 dc)+ +handleUnary :: + (term -> term -> termfix DiffResult)+ + -> (DiffResult a -> termfix DiffResult) -- ^ NT wrapper+ -> (termfix DiffResult -> DiffResult a) -- ^ NT unwrapepr+ + -> (termfix DiffResult -> b) -- ^ constructor+ + -> term+ + -> term+ + -> DiffResult b+ +handleUnary recFun _ newtypeunwrapper constr r1 r2 =+ let + rec = recFun r1 r2+ in+ case newtypeunwrapper rec of+ Same -> Same+ _ -> SameHead (constr rec)+ ++ +handleLeaf :: + (Eq a) =>+ (a -> d) -> a -> a -> DiffResult d+handleLeaf constr x1 x2 = + if x1==x2 + then Same + else Differ (constr x1) (constr x2)+ + + +-- runDiffTerm :: Term+-- -> Term+-- -> DiffResult (Term0 (TermFix DiffResult))+-- runDiffTerm t1 t2 = runTermFix (diffTerm t1 t2)++diffTerm :: Term -> Term -> TermFix DiffResult+diffTerm (TT t1) (TT t2) = TermFix $+ case (t1,t2) of+ (FunApp x1 args1,FunApp x2 args2) -> handleAppExpr diffTerm TermFix runTermFix 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)+ +plugSubterms :: forall a a1. a -> Term0 a1 -> Term0 a+plugSubterms p t = case t of+ FunApp x1 args -> FunApp x1 (fmap (const p) args)+ DistinctObjectTerm x1 -> DistinctObjectTerm x1+ NumberLitTerm x1 -> NumberLitTerm x1+ Var x1 -> Var x1+ +plugSubformulae :: forall a formula a1 t.+ a -> formula -> Formula0 a1 t -> Formula0 a formula+plugSubformulae pt pf f = case f of+ Quant q vars _ -> Quant q vars pf+ PredApp x1 args -> PredApp x1 (fmap (const pt) args)+ BinOp _ b _ -> BinOp pf b pf+ InfixPred _ b _ -> InfixPred pt b pt+ (:~:) _ -> (:~:) pf+ + + +diffFormula :: Formula -> Formula -> FormulaFix DiffResult+diffFormula (FF f1) (FF f2) = FormulaFix $+ 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)) + ++ ( BinOp l1 op1 r1+ ,BinOp l2 op2 r2 ) -> handleBinExpr diffFormula FormulaFix runFormulaFix 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+ + ( (:~:) g1+ ,(:~:) g2 ) -> handleUnary diffFormula FormulaFix runFormulaFix (:~:) g1 g2++ + ( PredApp x1 args1+ ,PredApp x2 args2 ) -> handleAppExpr diffTerm TermFix runTermFix PredApp x1 args1 x2 args2 + + _ -> let plug=plugSubformulae (TermFix DontCare) (FormulaFix DontCare) in Differ (plug f1) (plug f2)+++instance Show (TermFix DiffResult) where+ show (TermFix t) = show t++instance Show (FormulaFix DiffResult) where+ show (FormulaFix f) = show f+ +type T0Diff = DiffResult (Term0 (TermFix DiffResult))+type F0Diff = DiffResult (Formula0 (TermFix DiffResult) (FormulaFix DiffResult))+ ++wildcard :: AtomicWord+wildcard = "_"+ +instance Pretty (WithEnclosing T0Diff) where+ pretty = prettyHelper (plugSubterms (TT (FunApp wildcard [])))+ +instance Pretty (WithEnclosing F0Diff) where+ pretty = prettyHelper (plugSubformulae (TT (FunApp wildcard [])) (FF (PredApp wildcard [])))+ +prettyHelper :: forall t a.+ (Pretty (WithEnclosing t), Pretty (WithEnclosing a)) =>+ (t -> a) -> WithEnclosing (DiffResult t) -> Doc+prettyHelper _ (WithEnclosing _ d) = + let + pwe = pretty . WithEnclosing EnclNothing+ in+ case d of+ DontCare -> dullwhite.pretty $ wildcard+ Same -> dullgreen.text $ "Same"+ SameHead x -> blue . encloseSep (text "{ SameHead ") (text "}") semi $+ [ pwe x+ ]+ ++ + Differ x y -> red . encloseSep (text "{ Differ ") rbrace (text "; ") $++ [ pwe x + , pwe y+ ]+ +deriving instance Pretty (TermFix DiffResult)++deriving instance Pretty (FormulaFix DiffResult)+ +instance Pretty (WithEnclosing (TermFix DiffResult)) where+ pretty (WithEnclosing x (TermFix y)) = pretty (WithEnclosing x y) + +instance Pretty (WithEnclosing (FormulaFix DiffResult)) where+ pretty (WithEnclosing x (FormulaFix y)) = pretty (WithEnclosing x y) + +instance Pretty (T0Diff) where+ pretty = pretty . WithEnclosing EnclNothing+ +instance Pretty (F0Diff) where+ pretty = pretty . WithEnclosing EnclNothing++-- instance Pretty (DiffResult (TermFix DiffResult)) where+-- pretty = pretty . WithEnclosing EnclNothing . TermFix+ +-- instance Pretty (DiffResult (TermFix DiffResult) (FormulaFix DiffResult)) where+-- pretty = pretty . WithEnclosing EnclNothing . FormulaFix+ + +-- runFormulaDiff :: Formula+-- -> Formula+-- -> DiffResult+-- (Formula0 (TermFix DiffResult) (FormulaFix DiffResult))+-- runFormulaDiff a b = runFormulaFix (diffFormula a b)+ +-- | Less random generator for generating formulae suitable for testing diff+diffGenF :: Gen Formula+diffGenF = sized go+ where+ go 0 = return $ pApp "Truth" []+ go i = oneof + [+ do+ ileft <- choose (0,i-1)+ liftM2 (.&.) (resize ileft diffGenF) (resize (i-1-ileft) diffGenF)+ , let a=diffGenT in fmap (.=.) a `ap` a+ ]+ +diffGenT :: Gen Term+diffGenT = sized go+ where+ go 0 = elements[var "Z",fApp "1" []]+ + go i = oneof + [+ let a=resize (i`div`3) diffGenT in fmap (fApp "g") (sequence [a,a,a])+ , do+ ileft <- choose (0,i-1)+ fmap (fApp "f") (sequence [resize ileft diffGenT,+ resize (i-1-ileft) diffGenT])+ ]+ + +printSampleDiffs :: IO ()+printSampleDiffs = do+ xs <- sample' diffGenF+ ys <- sample' diffGenF++ let item x y = text (replicate 50 '=') + <$> pretty x+ <$> text (replicate 40 '-')+ <$> pretty y+ <$> text (replicate 40 '-')+ <$> pretty (diffFormula x y)+ + mapM_ (putStrLn . prettySimple . uncurry item) (zip xs ys)++-- prop0 :: Formula -> Formula -> Property+-- prop0 f1 f2 = f1 /= f2 ==>++-- let res=diffFormula (pApp "foo" [] .&. f1)+-- (pApp "foo" [] .&. f2)++-- in collect res $ True+ +-- -- case res of+-- -- SameHead ((FormulaFix Same) :&: +-- -- (FormulaFix (Differ f1 ++instance Functor DiffResult where+ fmap f d = case d of+ Same -> Same+ SameHead x -> SameHead (f x)+ Differ x y -> Differ (f x) (f y)+ DontCare -> DontCare+++++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
+ Codec/TPTP/Export.hs view
@@ -0,0 +1,154 @@+{-# OPTIONS -fglasgow-exts -XStandaloneDeriving -XRecordWildCards -XNoMonomorphismRestriction -fwarn-missing-signatures -Wall #-}++module Codec.TPTP.Export(toTPTP',ToTPTP(..),isLowerWord) where+ +import Codec.TPTP.Base+ +-- | Convenient wrapper for 'toTPTP'+toTPTP' :: forall a. (ToTPTP a) => a -> String+toTPTP' = ($"") . toTPTP+ +s :: String -> String -> String+s = showString+ +comma :: String -> String+comma = s ","+ +commaSepMap :: forall a.+ (a -> String -> String) -> [a] -> String -> String+commaSepMap _ [] = s ""+commaSepMap f (y:ys) = f y . foldr (\x xs -> comma . f x . xs) id ys + ++ + +class ToTPTP a where+ -- | Convert to TPTP+ toTPTP :: a -> ShowS+ +instance ToTPTP [TPTP_Input] where+ toTPTP = foldr (\x xs -> toTPTP x . s "\n" . xs) id++instance ToTPTP TPTP_Input where+ toTPTP AFormula{..} =+ s "fof(" . toTPTP name . comma . toTPTP role . comma .+ toTPTP formula . toTPTP sourceInfo . toTPTP usefulInfo . s ")."+ + toTPTP (Comment x) =+ s x -- % included in x + + toTPTP (Include x sel) = s "include" . s "(" . showString (tptpSQuote x) . ++ case sel of { [] -> id; _ -> s ",[" . commaSepMap toTPTP sel . s "]" } . +++ s ")." + ++instance ToTPTP Role where+ toTPTP (Role x) = s x+ +instance ToTPTP Quant where+ toTPTP All = s "!"+ toTPTP Exists = s "?"+ +instance ToTPTP InfixPred where+ toTPTP = s . reverse . drop 1 . reverse . drop 1 . show -- {-# EVIL #-} + +instance ToTPTP BinOp where+ toTPTP = s . reverse . drop 1 . reverse . drop 1 . show -- {-# EVIL #-}++instance (ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f) where+ toTPTP formu = + let+ result =+ case formu of+ Quant q vars f -> + let par = True in++ toTPTP q + . s " [" + . commaSepMap s vars + . s "] : " + . showParen par (toTPTP f)+ + PredApp p [] -> toTPTP p+ PredApp p args -> toTPTP p . s "(" . commaSepMap toTPTP args . s ")" + (:~:) f -> s "~ " . showParen True (toTPTP f)+ + BinOp x op y -> showParen True $ + (toTPTP x) . s " " . toTPTP op . s " " . (toTPTP y)+ + InfixPred x op y -> showParen True $ + (toTPTP x) . s " " . toTPTP op . s " " . (toTPTP y)+ in+ result+ +instance ToTPTP t => ToTPTP (Term0 t) where+ toTPTP term =+ + case term of + Var x -> s 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 Formula+deriving instance ToTPTP Term+++instance ToTPTP SourceInfo where+ toTPTP NoSourceInfo = s ""+ toTPTP (SourceInfo x) = s "," . toTPTP x++instance ToTPTP UsefulInfo where+ toTPTP NoUsefulInfo = s ""+ toTPTP (UsefulInfo xs) = s "," . s "[" . commaSepMap toTPTP xs . s "]"++instance ToTPTP GTerm where+ toTPTP gt = case gt of+ GTerm x -> toTPTP x+ ColonSep x y -> toTPTP x . s ":" . toTPTP y+ GList xs -> s "[" . commaSepMap toTPTP xs . s "]"+ +instance ToTPTP AtomicWord where+ toTPTP (AtomicWord x) = s $ if isLowerWord x then x else tptpSQuote x + +instance ToTPTP GData where+ toTPTP gd = case gd of+ GWord x -> toTPTP x+ GApp x args -> toTPTP x . s "(" . commaSepMap toTPTP args . s ")"+ GVar x -> s x+ GNumber x -> shows x+ GDistinctObject x -> showString (tptpQuote x)+ GFormulaData str formu -> s str . s "(" . toTPTP formu . s ")" + +tptpQuote :: [Char] -> [Char]+tptpQuote x = "\"" ++ concatMap go x ++ "\""+ where+ go '\\' = "\\\\"+ go '"' = "\\\""+ go c = [c]++tptpSQuote :: [Char] -> [Char]+tptpSQuote x = "'" ++ concatMap go x ++ "'"+ where+ go '\\' = "\\\\"+ go '\'' = "\\'"+ go c = [c]+++ +isBetween :: forall a. (Ord a) => a -> a -> a -> Bool+isBetween a x b = a <= x && x <= b+ +isReallyAlnum :: Char -> Bool+isReallyAlnum x = isBetween 'a' x 'z' || isBetween 'A' x 'Z' || isBetween '0' x '9' || x=='_' + +isLowerWord :: [Char] -> Bool+isLowerWord str = case str of+ (x:xs) | isBetween 'a' x 'z' && all isReallyAlnum xs -> True+ _ -> False
+ Codec/TPTP/Import.hs view
@@ -0,0 +1,18 @@+{-# OPTIONS -fwarn-missing-signatures #-}++module Codec.TPTP.Import(parse,parseFile+ ,Token(..)) where+ ++import Lexer+import Parser+import Codec.TPTP.Base+ ++ +parse :: String -> [TPTP_Input]+parse = parseTPTP . map snd . alexScanTokens+ + +parseFile :: FilePath -> IO [TPTP_Input]+parseFile x = parse `fmap` readFile x
+ Codec/TPTP/Pretty.hs view
@@ -0,0 +1,224 @@+{-# OPTIONS -XRecordWildCards -XCPP -XDeriveDataTypeable -XNoMonomorphismRestriction -XStandaloneDeriving -XFlexibleInstances -XGeneralizedNewtypeDeriving -fglasgow-exts #-}++{-# OPTIONS -Wall -fno-warn-orphans #-}++-- | Mainly just 'Pretty' instances+module Codec.TPTP.Pretty(prettySimple,WithEnclosing(..),Enclosing(..)) where++import Codec.TPTP.Base+import Codec.TPTP.Export+import Text.PrettyPrint.ANSI.Leijen+import Data.Data++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+fsym = yellow . pretty++--wtext :: String -> Doc+--wtext = white.text+ +prettyargs :: forall a. (Pretty a) => [a] -> Doc+--prettyargs = encloseSep (wtext "(") (wtext ")") (wtext ",") . fmap pretty+prettyargs = tupled . fmap pretty+-- prettyargs [] = white $ text "()"+-- prettyargs (x:xs) =+-- let pxs = fmap ((white (text ",") <+>) . pretty) xs in ++-- align (fillSep $ [ white (text "(") <+> pretty x ] +-- ++ pxs +-- ++ [ white (text ")") ] ) + + +-- | Carries information about the enclosing operation (for the purpose of printing stuff without parentheses if possible).+data WithEnclosing a = WithEnclosing Enclosing a+ +data Enclosing = EnclBinOp BinOp | EnclQuant | EnclNeg | EnclInfixPred InfixPred | EnclNothing+ deriving (Eq,Ord,Show,Data,Typeable,Read)+ +unaryEncl :: Enclosing -> Bool+unaryEncl EnclNeg = True+unaryEncl EnclQuant = True+unaryEncl _ = False++needsParens :: Enclosing -> Enclosing -> Bool+needsParens inner outer =+ case (inner,outer) of+ -- special handling for associative ops+ ((EnclBinOp (:&:)),(EnclBinOp (:&:))) -> False+ ((EnclBinOp (:|:)),(EnclBinOp (:|:))) -> False+ ((EnclBinOp (:<~>:)),(EnclBinOp (:<~>:))) -> False+ + -- chains of quantifiers/negation don't need parentheses+ _ + | unaryEncl inner, unaryEncl outer + -> False+ + _ -> prec inner <= prec outer+ where+ prec :: Enclosing -> Int+ prec x = case x of + (EnclInfixPred _) -> 60+ (EnclNeg) -> 50+ (EnclQuant) -> 50+ (EnclBinOp (:&:)) -> 40+ (EnclBinOp (:~&:)) -> 40+ (EnclBinOp (:|:)) -> 30+ (EnclBinOp (:~|:)) -> 30+ (EnclBinOp (:=>:)) -> 20+ (EnclBinOp (:<=:)) -> 20+ (EnclBinOp (:<=>:)) -> 20+ (EnclBinOp (:<~>:)) -> 20+ EnclNothing -> (-1000) -- if there's no enclosing operation, we don't need parentheses+++maybeParens :: Enclosing -> Enclosing -> Doc -> Doc+maybeParens inner outer | needsParens inner outer = parens+maybeParens _ _ = id + +instance Pretty TPTP_Input where+ pretty AFormula{..} + = (text) "Formula " <+> (dullwhite.text) "name:"+ </>+ vsep+ [+ (red.pretty) name <+> dullwhite (text "role:") <+> (magenta.text.unrole) role+ , pretty formula+ , pretty sourceInfo+ , pretty usefulInfo+ ,empty+ ]+ + pretty (Comment str)+ = magenta . string $ str+ + pretty (Include f sel) = text "include" <> parens (squotes (text f) <> (case sel of { [] -> empty; _ -> comma <+> sep (punctuate comma (fmap pretty sel)) } )) + + + prettyList = foldr (\x xs -> pretty x <$> xs) empty + +instance Pretty Quant where+ pretty All = oper "∀"+ pretty Exists = oper "∃"+ +instance (Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty ((WithEnclosing (Formula0 t f))) where+ pretty (WithEnclosing enclosing formu) = + let + newEnclosing =+ case formu of+ Quant _ _ _ -> EnclQuant + PredApp _ _ -> EnclNothing -- arguments are comma-seperated, so they don't need any parens+ (:~:) _ -> EnclNeg+ BinOp _ op _ -> EnclBinOp op+ InfixPred _ op _ -> EnclInfixPred op+ + wne = WithEnclosing newEnclosing+ + in+ maybeParens newEnclosing enclosing $+ + case formu of++ Quant q vars f ->+ pretty q + <+> brackets (hsep (punctuate comma (fmap prettyvar vars))) + <> dot + </> pretty (wne f)++ (:~:) f -> oper "¬" <+> pretty (wne f)+ + PredApp p [] -> psym p+ PredApp p args -> psym p <> prettyargs (fmap wne args)++ + BinOp f1 op f2 ->+ align $ sep [indent 0 $ pretty (wne f1), pretty op, indent 0 $ pretty (wne f2)]+ + InfixPred f1 op f2 ->+ align $ sep [indent 0 $ pretty (wne f1), pretty op, indent 0 $ pretty (wne f2)]+ +instance Pretty BinOp where+ pretty x = case x of+ (:<=>:) -> oper "⇔"+ (:=>:) -> oper "⇒"+ (:<=:) -> oper "⇐"+ (:&:) -> oper "∧"+ (:|:) -> oper "∨"+ (:~&:) -> oper "NAND"+ (:~|:) -> oper "NOR"+ (:<~>:) -> oper "XOR"+ +instance Pretty InfixPred where+ pretty x = case x of+ (:=:) -> oper "="+ (:!=:) -> oper "≠"+ +instance (Pretty (WithEnclosing t)) => Pretty (WithEnclosing (Term0 t)) where+ pretty (WithEnclosing _ x) = + case x of + Var s -> prettyvar s+ NumberLitTerm d -> text (show d)+ DistinctObjectTerm s -> cyan (dquotes (text s))+ FunApp f [] -> fsym f+ FunApp f args -> fsym f <> prettyargs (fmap (WithEnclosing EnclNothing) args)+ + ++instance Pretty (Formula0 Term Formula) where+ pretty = pretty . WithEnclosing EnclNothing . FF+ +instance Pretty (Term0 Term) where+ pretty = pretty . WithEnclosing EnclNothing . TT+ +instance Pretty (WithEnclosing Formula) where+ pretty (WithEnclosing x (FF y)) = pretty (WithEnclosing x y) + +instance Pretty (WithEnclosing Term) where+ pretty (WithEnclosing x (TT y)) = pretty (WithEnclosing x y) + +deriving instance Pretty Formula+deriving instance Pretty Term+ +-- instance (Pretty f, Pretty t) => Pretty (Formula0 t f) where+-- pretty = pretty . WithEnclosing ""+ +-- instance (Pretty t) => Pretty (Term0 t) where+-- pretty = pretty . WithEnclosing ""+ +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 UsefulInfo where+ pretty NoUsefulInfo = dullwhite . text $ "NoUsefulInfo"+ pretty (UsefulInfo x) = dullwhite (text "UsefulInfo: ") <+> pretty x++++instance Pretty GData where+ pretty (GWord x) = pretty x+ pretty (GNumber x) = pretty x+ pretty (GDistinctObject x) = cyan (dquotes (text x))+ 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++instance Pretty AtomicWord where+ pretty (AtomicWord x) = (if isLowerWord x then text else squotes.text) x ++instance Pretty GTerm where+ pretty (GTerm x) = pretty x+ pretty (ColonSep x y) = pretty x <+> oper ":" <+> pretty y+ pretty (GList xs) = let f = oper+ in+ f "[" <+> (fillSep . punctuate comma . fmap pretty) xs <+> f "]"+ +
+ Codec/TPTP/QuickCheck.hs view
@@ -0,0 +1,53 @@+{-# OPTIONS -fglasgow-exts #-}+module Codec.TPTP.QuickCheck where+ +import Test.QuickCheck+import Control.Monad+import Control.Applicative+import Data.Char+import Data.Array.ST+import Data.Array.IArray+ +argsFreq :: (Int -> Gen a) -> Gen a+argsFreq f = frequency [ (10,f 0)+ , (10,f 1)+ , (10,f 2)+ , (2 ,f 3)+ , (2 ,f 4)+ , (1, f 15)+ ]+ +arbVar :: Gen [Char]+arbVar = liftM2 (:) (elements "WXZY") (show <$> choose(1::Int,3)) + +-- sorry I don't feel like calculating this distribution deductively at the moment ;)+-- | Return random partition of n items into the given number of buckets if buckets>0+--+-- Return [] if buckets=0+arbPartition :: Int -> Int -> Gen [Int]+arbPartition 0 _ = return []+arbPartition 1 n = return [n]+arbPartition buckets n = do+ choices <- replicateM n (choose (1,buckets))++ return . Data.Array.IArray.elems . runSTUArray $+ do+ arrr <- newArray (1,buckets) 0+ forM_ choices (\bucket -> writeArray arrr bucket . succ =<< readArray arrr bucket)+ return arrr+ +arbPrintable :: Gen [Char]+arbPrintable = listOf (arbitrary `suchThat` printable)+ +printable :: Char -> Bool+printable x = isAscii x && isPrint x --isDigit x || isLetter x || x `elem` " _+!@#$%^&*()[]{}-=?.,;'\":/\\"+ +arbLowerWord :: Gen String+arbLowerWord = (:) `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)+ ,(8, fmap (f . fromIntegral) (arbitrary::Gen Int))+ ]
+ LICENSE view
@@ -0,0 +1,674 @@+ GNU GENERAL PUBLIC LICENSE+ Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.++ Preamble++ The GNU General Public License is a free, copyleft license for+software and other kinds of works.++ The licenses for most software and other practical works are designed+to take away your freedom to share and change the works. By contrast,+the GNU General Public License is intended to guarantee your freedom to+share and change all versions of a program--to make sure it remains free+software for all its users. We, the Free Software Foundation, use the+GNU General Public License for most of our software; it applies also to+any other work released this way by its authors. You can apply it to+your programs, too.++ When we speak of free software, we are referring to freedom, not+price. Our General Public Licenses are designed to make sure that you+have the freedom to distribute copies of free software (and charge for+them if you wish), that you receive source code or can get it if you+want it, that you can change the software or use pieces of it in new+free programs, and that you know you can do these things.++ To protect your rights, we need to prevent others from denying you+these rights or asking you to surrender the rights. Therefore, you have+certain responsibilities if you distribute copies of the software, or if+you modify it: responsibilities to respect the freedom of others.++ For example, if you distribute copies of such a program, whether+gratis or for a fee, you must pass on to the recipients the same+freedoms that you received. You must make sure that they, too, receive+or can get the source code. And you must show them these terms so they+know their rights.++ Developers that use the GNU GPL protect your rights with two steps:+(1) assert copyright on the software, and (2) offer you this License+giving you legal permission to copy, distribute and/or modify it.++ For the developers' and authors' protection, the GPL clearly explains+that there is no warranty for this free software. For both users' and+authors' sake, the GPL requires that modified versions be marked as+changed, so that their problems will not be attributed erroneously to+authors of previous versions.++ Some devices are designed to deny users access to install or run+modified versions of the software inside them, although the manufacturer+can do so. This is fundamentally incompatible with the aim of+protecting users' freedom to change the software. The systematic+pattern of such abuse occurs in the area of products for individuals to+use, which is precisely where it is most unacceptable. Therefore, we+have designed this version of the GPL to prohibit the practice for those+products. If such problems arise substantially in other domains, we+stand ready to extend this provision to those domains in future versions+of the GPL, as needed to protect the freedom of users.++ Finally, every program is threatened constantly by software patents.+States should not allow patents to restrict development and use of+software on general-purpose computers, but in those that do, we wish to+avoid the special danger that patents applied to a free program could+make it effectively proprietary. To prevent this, the GPL assures that+patents cannot be used to render the program non-free.++ The precise terms and conditions for copying, distribution and+modification follow.++ TERMS AND CONDITIONS++ 0. Definitions.++ "This License" refers to version 3 of the GNU General Public License.++ "Copyright" also means copyright-like laws that apply to other kinds of+works, such as semiconductor masks.++ "The Program" refers to any copyrightable work licensed under this+License. Each licensee is addressed as "you". "Licensees" and+"recipients" may be individuals or organizations.++ To "modify" a work means to copy from or adapt all or part of the work+in a fashion requiring copyright permission, other than the making of an+exact copy. The resulting work is called a "modified version" of the+earlier work or a work "based on" the earlier work.++ A "covered work" means either the unmodified Program or a work based+on the Program.++ To "propagate" a work means to do anything with it that, without+permission, would make you directly or secondarily liable for+infringement under applicable copyright law, except executing it on a+computer or modifying a private copy. Propagation includes copying,+distribution (with or without modification), making available to the+public, and in some countries other activities as well.++ To "convey" a work means any kind of propagation that enables other+parties to make or receive copies. Mere interaction with a user through+a computer network, with no transfer of a copy, is not conveying.++ An interactive user interface displays "Appropriate Legal Notices"+to the extent that it includes a convenient and prominently visible+feature that (1) displays an appropriate copyright notice, and (2)+tells the user that there is no warranty for the work (except to the+extent that warranties are provided), that licensees may convey the+work under this License, and how to view a copy of this License. If+the interface presents a list of user commands or options, such as a+menu, a prominent item in the list meets this criterion.++ 1. Source Code.++ The "source code" for a work means the preferred form of the work+for making modifications to it. "Object code" means any non-source+form of a work.++ A "Standard Interface" means an interface that either is an official+standard defined by a recognized standards body, or, in the case of+interfaces specified for a particular programming language, one that+is widely used among developers working in that language.++ The "System Libraries" of an executable work include anything, other+than the work as a whole, that (a) is included in the normal form of+packaging a Major Component, but which is not part of that Major+Component, and (b) serves only to enable use of the work with that+Major Component, or to implement a Standard Interface for which an+implementation is available to the public in source code form. A+"Major Component", in this context, means a major essential component+(kernel, window system, and so on) of the specific operating system+(if any) on which the executable work runs, or a compiler used to+produce the work, or an object code interpreter used to run it.++ The "Corresponding Source" for a work in object code form means all+the source code needed to generate, install, and (for an executable+work) run the object code and to modify the work, including scripts to+control those activities. However, it does not include the work's+System Libraries, or general-purpose tools or generally available free+programs which are used unmodified in performing those activities but+which are not part of the work. For example, Corresponding Source+includes interface definition files associated with source files for+the work, and the source code for shared libraries and dynamically+linked subprograms that the work is specifically designed to require,+such as by intimate data communication or control flow between those+subprograms and other parts of the work.++ The Corresponding Source need not include anything that users+can regenerate automatically from other parts of the Corresponding+Source.++ The Corresponding Source for a work in source code form is that+same work.++ 2. Basic Permissions.++ All rights granted under this License are granted for the term of+copyright on the Program, and are irrevocable provided the stated+conditions are met. This License explicitly affirms your unlimited+permission to run the unmodified Program. The output from running a+covered work is covered by this License only if the output, given its+content, constitutes a covered work. This License acknowledges your+rights of fair use or other equivalent, as provided by copyright law.++ You may make, run and propagate covered works that you do not+convey, without conditions so long as your license otherwise remains+in force. You may convey covered works to others for the sole purpose+of having them make modifications exclusively for you, or provide you+with facilities for running those works, provided that you comply with+the terms of this License in conveying all material for which you do+not control copyright. Those thus making or running the covered works+for you must do so exclusively on your behalf, under your direction+and control, on terms that prohibit them from making any copies of+your copyrighted material outside their relationship with you.++ Conveying under any other circumstances is permitted solely under+the conditions stated below. Sublicensing is not allowed; section 10+makes it unnecessary.++ 3. Protecting Users' Legal Rights From Anti-Circumvention Law.++ No covered work shall be deemed part of an effective technological+measure under any applicable law fulfilling obligations under article+11 of the WIPO copyright treaty adopted on 20 December 1996, or+similar laws prohibiting or restricting circumvention of such+measures.++ When you convey a covered work, you waive any legal power to forbid+circumvention of technological measures to the extent such circumvention+is effected by exercising rights under this License with respect to+the covered work, and you disclaim any intention to limit operation or+modification of the work as a means of enforcing, against the work's+users, your or third parties' legal rights to forbid circumvention of+technological measures.++ 4. Conveying Verbatim Copies.++ You may convey verbatim copies of the Program's source code as you+receive it, in any medium, provided that you conspicuously and+appropriately publish on each copy an appropriate copyright notice;+keep intact all notices stating that this License and any+non-permissive terms added in accord with section 7 apply to the code;+keep intact all notices of the absence of any warranty; and give all+recipients a copy of this License along with the Program.++ You may charge any price or no price for each copy that you convey,+and you may offer support or warranty protection for a fee.++ 5. Conveying Modified Source Versions.++ You may convey a work based on the Program, or the modifications to+produce it from the Program, in the form of source code under the+terms of section 4, provided that you also meet all of these conditions:++ a) The work must carry prominent notices stating that you modified+ it, and giving a relevant date.++ b) The work must carry prominent notices stating that it is+ released under this License and any conditions added under section+ 7. This requirement modifies the requirement in section 4 to+ "keep intact all notices".++ c) You must license the entire work, as a whole, under this+ License to anyone who comes into possession of a copy. This+ License will therefore apply, along with any applicable section 7+ additional terms, to the whole of the work, and all its parts,+ regardless of how they are packaged. This License gives no+ permission to license the work in any other way, but it does not+ invalidate such permission if you have separately received it.++ d) If the work has interactive user interfaces, each must display+ Appropriate Legal Notices; however, if the Program has interactive+ interfaces that do not display Appropriate Legal Notices, your+ work need not make them do so.++ A compilation of a covered work with other separate and independent+works, which are not by their nature extensions of the covered work,+and which are not combined with it such as to form a larger program,+in or on a volume of a storage or distribution medium, is called an+"aggregate" if the compilation and its resulting copyright are not+used to limit the access or legal rights of the compilation's users+beyond what the individual works permit. Inclusion of a covered work+in an aggregate does not cause this License to apply to the other+parts of the aggregate.++ 6. Conveying Non-Source Forms.++ You may convey a covered work in object code form under the terms+of sections 4 and 5, provided that you also convey the+machine-readable Corresponding Source under the terms of this License,+in one of these ways:++ a) Convey the object code in, or embodied in, a physical product+ (including a physical distribution medium), accompanied by the+ Corresponding Source fixed on a durable physical medium+ customarily used for software interchange.++ b) Convey the object code in, or embodied in, a physical product+ (including a physical distribution medium), accompanied by a+ written offer, valid for at least three years and valid for as+ long as you offer spare parts or customer support for that product+ model, to give anyone who possesses the object code either (1) a+ copy of the Corresponding Source for all the software in the+ product that is covered by this License, on a durable physical+ medium customarily used for software interchange, for a price no+ more than your reasonable cost of physically performing this+ conveying of source, or (2) access to copy the+ Corresponding Source from a network server at no charge.++ c) Convey individual copies of the object code with a copy of the+ written offer to provide the Corresponding Source. This+ alternative is allowed only occasionally and noncommercially, and+ only if you received the object code with such an offer, in accord+ with subsection 6b.++ d) Convey the object code by offering access from a designated+ place (gratis or for a charge), and offer equivalent access to the+ Corresponding Source in the same way through the same place at no+ further charge. You need not require recipients to copy the+ Corresponding Source along with the object code. If the place to+ copy the object code is a network server, the Corresponding Source+ may be on a different server (operated by you or a third party)+ that supports equivalent copying facilities, provided you maintain+ clear directions next to the object code saying where to find the+ Corresponding Source. Regardless of what server hosts the+ Corresponding Source, you remain obligated to ensure that it is+ available for as long as needed to satisfy these requirements.++ e) Convey the object code using peer-to-peer transmission, provided+ you inform other peers where the object code and Corresponding+ Source of the work are being offered to the general public at no+ charge under subsection 6d.++ A separable portion of the object code, whose source code is excluded+from the Corresponding Source as a System Library, need not be+included in conveying the object code work.++ A "User Product" is either (1) a "consumer product", which means any+tangible personal property which is normally used for personal, family,+or household purposes, or (2) anything designed or sold for incorporation+into a dwelling. In determining whether a product is a consumer product,+doubtful cases shall be resolved in favor of coverage. For a particular+product received by a particular user, "normally used" refers to a+typical or common use of that class of product, regardless of the status+of the particular user or of the way in which the particular user+actually uses, or expects or is expected to use, the product. A product+is a consumer product regardless of whether the product has substantial+commercial, industrial or non-consumer uses, unless such uses represent+the only significant mode of use of the product.++ "Installation Information" for a User Product means any methods,+procedures, authorization keys, or other information required to install+and execute modified versions of a covered work in that User Product from+a modified version of its Corresponding Source. The information must+suffice to ensure that the continued functioning of the modified object+code is in no case prevented or interfered with solely because+modification has been made.++ If you convey an object code work under this section in, or with, or+specifically for use in, a User Product, and the conveying occurs as+part of a transaction in which the right of possession and use of the+User Product is transferred to the recipient in perpetuity or for a+fixed term (regardless of how the transaction is characterized), the+Corresponding Source conveyed under this section must be accompanied+by the Installation Information. But this requirement does not apply+if neither you nor any third party retains the ability to install+modified object code on the User Product (for example, the work has+been installed in ROM).++ The requirement to provide Installation Information does not include a+requirement to continue to provide support service, warranty, or updates+for a work that has been modified or installed by the recipient, or for+the User Product in which it has been modified or installed. Access to a+network may be denied when the modification itself materially and+adversely affects the operation of the network or violates the rules and+protocols for communication across the network.++ Corresponding Source conveyed, and Installation Information provided,+in accord with this section must be in a format that is publicly+documented (and with an implementation available to the public in+source code form), and must require no special password or key for+unpacking, reading or copying.++ 7. Additional Terms.++ "Additional permissions" are terms that supplement the terms of this+License by making exceptions from one or more of its conditions.+Additional permissions that are applicable to the entire Program shall+be treated as though they were included in this License, to the extent+that they are valid under applicable law. If additional permissions+apply only to part of the Program, that part may be used separately+under those permissions, but the entire Program remains governed by+this License without regard to the additional permissions.++ When you convey a copy of a covered work, you may at your option+remove any additional permissions from that copy, or from any part of+it. (Additional permissions may be written to require their own+removal in certain cases when you modify the work.) You may place+additional permissions on material, added by you to a covered work,+for which you have or can give appropriate copyright permission.++ Notwithstanding any other provision of this License, for material you+add to a covered work, you may (if authorized by the copyright holders of+that material) supplement the terms of this License with terms:++ a) Disclaiming warranty or limiting liability differently from the+ terms of sections 15 and 16 of this License; or++ b) Requiring preservation of specified reasonable legal notices or+ author attributions in that material or in the Appropriate Legal+ Notices displayed by works containing it; or++ c) Prohibiting misrepresentation of the origin of that material, or+ requiring that modified versions of such material be marked in+ reasonable ways as different from the original version; or++ d) Limiting the use for publicity purposes of names of licensors or+ authors of the material; or++ e) Declining to grant rights under trademark law for use of some+ trade names, trademarks, or service marks; or++ f) Requiring indemnification of licensors and authors of that+ material by anyone who conveys the material (or modified versions of+ it) with contractual assumptions of liability to the recipient, for+ any liability that these contractual assumptions directly impose on+ those licensors and authors.++ All other non-permissive additional terms are considered "further+restrictions" within the meaning of section 10. If the Program as you+received it, or any part of it, contains a notice stating that it is+governed by this License along with a term that is a further+restriction, you may remove that term. If a license document contains+a further restriction but permits relicensing or conveying under this+License, you may add to a covered work material governed by the terms+of that license document, provided that the further restriction does+not survive such relicensing or conveying.++ If you add terms to a covered work in accord with this section, you+must place, in the relevant source files, a statement of the+additional terms that apply to those files, or a notice indicating+where to find the applicable terms.++ Additional terms, permissive or non-permissive, may be stated in the+form of a separately written license, or stated as exceptions;+the above requirements apply either way.++ 8. Termination.++ You may not propagate or modify a covered work except as expressly+provided under this License. Any attempt otherwise to propagate or+modify it is void, and will automatically terminate your rights under+this License (including any patent licenses granted under the third+paragraph of section 11).++ However, if you cease all violation of this License, then your+license from a particular copyright holder is reinstated (a)+provisionally, unless and until the copyright holder explicitly and+finally terminates your license, and (b) permanently, if the copyright+holder fails to notify you of the violation by some reasonable means+prior to 60 days after the cessation.++ Moreover, your license from a particular copyright holder is+reinstated permanently if the copyright holder notifies you of the+violation by some reasonable means, this is the first time you have+received notice of violation of this License (for any work) from that+copyright holder, and you cure the violation prior to 30 days after+your receipt of the notice.++ Termination of your rights under this section does not terminate the+licenses of parties who have received copies or rights from you under+this License. If your rights have been terminated and not permanently+reinstated, you do not qualify to receive new licenses for the same+material under section 10.++ 9. Acceptance Not Required for Having Copies.++ You are not required to accept this License in order to receive or+run a copy of the Program. Ancillary propagation of a covered work+occurring solely as a consequence of using peer-to-peer transmission+to receive a copy likewise does not require acceptance. However,+nothing other than this License grants you permission to propagate or+modify any covered work. These actions infringe copyright if you do+not accept this License. Therefore, by modifying or propagating a+covered work, you indicate your acceptance of this License to do so.++ 10. Automatic Licensing of Downstream Recipients.++ Each time you convey a covered work, the recipient automatically+receives a license from the original licensors, to run, modify and+propagate that work, subject to this License. You are not responsible+for enforcing compliance by third parties with this License.++ An "entity transaction" is a transaction transferring control of an+organization, or substantially all assets of one, or subdividing an+organization, or merging organizations. If propagation of a covered+work results from an entity transaction, each party to that+transaction who receives a copy of the work also receives whatever+licenses to the work the party's predecessor in interest had or could+give under the previous paragraph, plus a right to possession of the+Corresponding Source of the work from the predecessor in interest, if+the predecessor has it or can get it with reasonable efforts.++ You may not impose any further restrictions on the exercise of the+rights granted or affirmed under this License. For example, you may+not impose a license fee, royalty, or other charge for exercise of+rights granted under this License, and you may not initiate litigation+(including a cross-claim or counterclaim in a lawsuit) alleging that+any patent claim is infringed by making, using, selling, offering for+sale, or importing the Program or any portion of it.++ 11. Patents.++ A "contributor" is a copyright holder who authorizes use under this+License of the Program or a work on which the Program is based. The+work thus licensed is called the contributor's "contributor version".++ A contributor's "essential patent claims" are all patent claims+owned or controlled by the contributor, whether already acquired or+hereafter acquired, that would be infringed by some manner, permitted+by this License, of making, using, or selling its contributor version,+but do not include claims that would be infringed only as a+consequence of further modification of the contributor version. For+purposes of this definition, "control" includes the right to grant+patent sublicenses in a manner consistent with the requirements of+this License.++ Each contributor grants you a non-exclusive, worldwide, royalty-free+patent license under the contributor's essential patent claims, to+make, use, sell, offer for sale, import and otherwise run, modify and+propagate the contents of its contributor version.++ In the following three paragraphs, a "patent license" is any express+agreement or commitment, however denominated, not to enforce a patent+(such as an express permission to practice a patent or covenant not to+sue for patent infringement). To "grant" such a patent license to a+party means to make such an agreement or commitment not to enforce a+patent against the party.++ If you convey a covered work, knowingly relying on a patent license,+and the Corresponding Source of the work is not available for anyone+to copy, free of charge and under the terms of this License, through a+publicly available network server or other readily accessible means,+then you must either (1) cause the Corresponding Source to be so+available, or (2) arrange to deprive yourself of the benefit of the+patent license for this particular work, or (3) arrange, in a manner+consistent with the requirements of this License, to extend the patent+license to downstream recipients. "Knowingly relying" means you have+actual knowledge that, but for the patent license, your conveying the+covered work in a country, or your recipient's use of the covered work+in a country, would infringe one or more identifiable patents in that+country that you have reason to believe are valid.++ If, pursuant to or in connection with a single transaction or+arrangement, you convey, or propagate by procuring conveyance of, a+covered work, and grant a patent license to some of the parties+receiving the covered work authorizing them to use, propagate, modify+or convey a specific copy of the covered work, then the patent license+you grant is automatically extended to all recipients of the covered+work and works based on it.++ A patent license is "discriminatory" if it does not include within+the scope of its coverage, prohibits the exercise of, or is+conditioned on the non-exercise of one or more of the rights that are+specifically granted under this License. You may not convey a covered+work if you are a party to an arrangement with a third party that is+in the business of distributing software, under which you make payment+to the third party based on the extent of your activity of conveying+the work, and under which the third party grants, to any of the+parties who would receive the covered work from you, a discriminatory+patent license (a) in connection with copies of the covered work+conveyed by you (or copies made from those copies), or (b) primarily+for and in connection with specific products or compilations that+contain the covered work, unless you entered into that arrangement,+or that patent license was granted, prior to 28 March 2007.++ Nothing in this License shall be construed as excluding or limiting+any implied license or other defenses to infringement that may+otherwise be available to you under applicable patent law.++ 12. No Surrender of Others' Freedom.++ If conditions are imposed on you (whether by court order, agreement or+otherwise) that contradict the conditions of this License, they do not+excuse you from the conditions of this License. If you cannot convey a+covered work so as to satisfy simultaneously your obligations under this+License and any other pertinent obligations, then as a consequence you may+not convey it at all. For example, if you agree to terms that obligate you+to collect a royalty for further conveying from those to whom you convey+the Program, the only way you could satisfy both those terms and this+License would be to refrain entirely from conveying the Program.++ 13. Use with the GNU Affero General Public License.++ Notwithstanding any other provision of this License, you have+permission to link or combine any covered work with a work licensed+under version 3 of the GNU Affero General Public License into a single+combined work, and to convey the resulting work. The terms of this+License will continue to apply to the part which is the covered work,+but the special requirements of the GNU Affero General Public License,+section 13, concerning interaction through a network will apply to the+combination as such.++ 14. Revised Versions of this License.++ The Free Software Foundation may publish revised and/or new versions of+the GNU General Public License from time to time. Such new versions will+be similar in spirit to the present version, but may differ in detail to+address new problems or concerns.++ Each version is given a distinguishing version number. If the+Program specifies that a certain numbered version of the GNU General+Public License "or any later version" applies to it, you have the+option of following the terms and conditions either of that numbered+version or of any later version published by the Free Software+Foundation. If the Program does not specify a version number of the+GNU General Public License, you may choose any version ever published+by the Free Software Foundation.++ If the Program specifies that a proxy can decide which future+versions of the GNU General Public License can be used, that proxy's+public statement of acceptance of a version permanently authorizes you+to choose that version for the Program.++ Later license versions may give you additional or different+permissions. However, no additional obligations are imposed on any+author or copyright holder as a result of your choosing to follow a+later version.++ 15. Disclaimer of Warranty.++ THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY+APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR+PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM+IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.++ 16. Limitation of Liability.++ IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF+SUCH DAMAGES.++ 17. Interpretation of Sections 15 and 16.++ If the disclaimer of warranty and limitation of liability provided+above cannot be given local legal effect according to their terms,+reviewing courts shall apply local law that most closely approximates+an absolute waiver of all civil liability in connection with the+Program, unless a warranty or assumption of liability accompanies a+copy of the Program in return for a fee.++ END OF TERMS AND CONDITIONS++ How to Apply These Terms to Your New Programs++ If you develop a new program, and you want it to be of the greatest+possible use to the public, the best way to achieve this is to make it+free software which everyone can redistribute and change under these terms.++ To do so, attach the following notices to the program. It is safest+to attach them to the start of each source file to most effectively+state the exclusion of warranty; and each file should have at least+the "copyright" line and a pointer to where the full notice is found.++ <one line to give the program's name and a brief idea of what it does.>+ Copyright (C) <year> <name of author>++ This program is free software: you can redistribute it and/or modify+ it under the terms of the GNU General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ This program is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU General Public License for more details.++ You should have received a copy of the GNU General Public License+ along with this program. If not, see <http://www.gnu.org/licenses/>.++Also add information on how to contact you by electronic and paper mail.++ If the program does terminal interaction, make it output a short+notice like this when it starts in an interactive mode:++ <program> Copyright (C) <year> <name of author>+ This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+ This is free software, and you are welcome to redistribute it+ under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License. Of course, your program's commands+might be different; for a GUI interface, you would use an "about box".++ You should also get your employer (if you work as a programmer) or school,+if any, to sign a "copyright disclaimer" for the program, if necessary.+For more information on this, and how to apply and follow the GNU GPL, see+<http://www.gnu.org/licenses/>.++ The GNU General Public License does not permit incorporating your program+into proprietary programs. If your program is a subroutine library, you+may consider it more useful to permit linking proprietary applications with+the library. If this is what you want to do, use the GNU Lesser General+Public License instead of this License. But first, please read+<http://www.gnu.org/philosophy/why-not-lgpl.html>.
+ Lexer.x view
@@ -0,0 +1,95 @@+{+module Lexer where+}++%wrapper "posn"++$sign = [\+\-]+$exponent = [Ee]+$numeric = 0-9+$non_zero_numeric = 1-9+$lower_alpha = a-z+$upper_alpha = A-Z+$alpha_numeric = [$lower_alpha$upper_alpha$numeric\_] +$dollar = \$+$printable_char = .+$viewable_char = [$printable_char\n]+ + +@not_star_slash = ( ([\n] | [^\*]) * ("*"+) ([\n] | [^\/\*]) )* ([\n] | [^\*])*+@sq_char = [^\\\'] | [\\][\\\'] +@do_char = [^\\\"] | [\\][\\\"] ++@decimal_natural = [0]| $non_zero_numeric $numeric* +@signed_decimal = $sign @decimal_natural+@decimal = @signed_decimal | @decimal_natural +@dot_decimal = "." $numeric $numeric*+@decimal_fraction = @decimal @dot_decimal+@decimal_exponent = ( @decimal | @decimal_fraction ) $exponent @decimal+ ++tokens :-++ $white+ ;+ "(" { withPos $ const LP }+ "[" { withPos $ const Lbrack }+ "]" { withPos $ const Rbrack }+ ")" { withPos $ const RP }+ "," { withPos $ const Comma }+ "!="|"="|"<=>"|"<="|"=>"|"<~>"|"&"|"|"+ |"~|"|"~&"|"!"|"?"|":"|"~" { withPos $ Oper }+ "." { withPos $ const Dot }+ ("%"|"#")$printable_char* { withPos $ CommentToken } -- comment line+ "/*" @not_star_slash "*"("*"*)"/" { withPos $ CommentToken } -- comment block + [\'] @sq_char* [\'] { withPos SingleQuoted }+ [\"] @do_char* [\"] { withPos DoubleQuoted }+ $dollar $dollar $lower_alpha $alpha_numeric* { withPos DollarDollarWord }+ $dollar $lower_alpha $alpha_numeric* { withPos DollarWord }+ $upper_alpha $alpha_numeric* { withPos UpperWord }+ $lower_alpha $alpha_numeric* { withPos LowerWord }+ "*" { withPos $ const Star }+ "+" { withPos $ const Plus }+ ">" { withPos $ const Rangle }+ @decimal_fraction | @decimal_exponent { withPos (Real . read . stripPlus) }+ $sign @decimal_natural { withPos (SignedInt . read . stripPlus) }+ @decimal_natural { withPos (UnsignedInt . read . stripPlus) }+++ + +++{+-- Each action has type :: String -> Token++withPos f pos s = (pos, f s)++-- The token type:+data Token = + LP + | RP + | Comma + | Dot + | Lbrack + | Rbrack+ | Oper String+ | SingleQuoted String+ | DoubleQuoted String+ | DollarWord String + | DollarDollarWord String+ | UpperWord String+ | LowerWord String+ | Star+ | Plus+ | Rangle+ | SignedInt Int+ | UnsignedInt Int+ | Real Double+ | CommentToken String+ deriving (Eq,Ord,Show)++-- alex defines: alexScanTokens++stripPlus ('+':xs) = xs+stripPlus xs = xs+}
+ Parser.y view
@@ -0,0 +1,423 @@+{+{-# OPTIONS -XDeriveDataTypeable -XCPP #-}+module Parser where+ +import Data.Char+import Data.Data+import Control.Monad+import Data.List as L+import Lexer+import Data.Set as S+import Codec.TPTP.Base+import System.IO+import System.IO.Unsafe+}++%name parseTPTP+%tokentype { Token }+%error { + + ((\xs -> case xs of+ xs -> error ("Parse error, pos: "++show (take 25 xs))))+ }+++%token+ lp { LP }+ rp { RP }+ lbra { Lbrack }+ rbra { Rbrack }+ comma { Comma }+ dot { Dot }+ star { Star }+ plus { Plus }+ rangle { Rangle }+ colon { Oper ":" }++ iff { Oper "<=>"}+ implies { Oper "=>"}+ xor { Oper "<~>"}+ nor { Oper "~|"}+ nand { Oper "~&"}+ impliedby { Oper "<=" }+ equals { Oper "=" }+ nequals { Oper "!=" }+ + exclam { Oper "!" }+ question { Oper "?" }+ ampersand { Oper "&" }+ vline { Oper "|" }+ tilde { Oper "~" }+ + fof { LowerWord "fof" }+ cnf { LowerWord "cnf" }+ include_ { LowerWord "include" }+ + single_quoted { SingleQuoted $$ }+ distinct_object { DoubleQuoted $$ }+ dollar_word { DollarWord $$ }+ dollar_dollar_word { DollarDollarWord $$ }+ upper_word { UpperWord $$ }+ lower_word { LowerWord $$ }+ signed_integer { SignedInt $$ }+ unsigned_integer { UnsignedInt $$ }+ real { Real $$ }+ + comment { CommentToken $$ }++ +%% ++TPTP_file :: {[TPTP_Input]}+TPTP_file : {[]} | TPTP_input TPTP_file {$1 : $2}+ +TPTP_input :: {TPTP_Input}+TPTP_input : annotated_formula {$1} + | include { $1 }+ | comment { Comment $1 }++annotated_formula :: {TPTP_Input}+annotated_formula : fof_annotated {$1} + | cnf_annotated {$1}++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) }+ +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) }+ + +annotations :: { (SourceInfo,UsefulInfo) }+annotations : comma source optional_info { ($2,$3) } + | { (NoSourceInfo, NoUsefulInfo) }++formula_role :: {Role}+formula_role : lower_word_ { Role $1 }+++fof_formula :: {Formula}+fof_formula : binary_formula { $1 }+ | unitary_formula { $1 }+ +binary_formula :: {Formula}+binary_formula : nonassoc_binary {$1}+ | assoc_binary {$1}+ +nonassoc_binary :: {Formula}+nonassoc_binary : unitary_formula binary_connective unitary_formula + { $2 $1 $3 }++ +assoc_binary :: {Formula}+assoc_binary : or_formula { $1 }+ | and_formula { $1 }+ + +or_formula :: {Formula}+or_formula : unitary_formula vline unitary_formula more_or_formula+ { foldl (.|.) ($1 .|. $3) $4 }+ +more_or_formula :: {[Formula]}+more_or_formula : {[]} | vline unitary_formula more_or_formula + { $2 : $3 }+ +and_formula :: {Formula}+and_formula : unitary_formula ampersand unitary_formula more_and_formula+ { foldl (.&.) ($1 .&. $3) $4 }+++more_and_formula :: {[Formula]}+more_and_formula : {[]} | ampersand unitary_formula more_and_formula + { $2 : $3 }+ +unitary_formula :: {Formula}+unitary_formula : quantified_formula {$1}+ | unary_formula {$1}+ | atomic_formula {$1}+ | lp fof_formula rp {$2}+ +quantified_formula :: {Formula}+quantified_formula : quantifier lbra variable_list rbra colon unitary_formula + { $1 $3 $6 }++variable_list :: {[String]}+variable_list : variable { [$1] }+ | variable comma variable_list { $1 : $3 }++unary_formula :: {Formula}+unary_formula : unary_connective unitary_formula { $1 $2 }+ | fol_infix_unary { $1 }+ ++++-- cnf_formula :: {Formula}+-- cnf_formula : assoc_binary {$1}+-- | lp assoc_binary rp {$2}++cnf_formula :: {Formula}+cnf_formula : lp disjunction rp { $2 }+ | disjunction { $1 }++ +disjunction :: {Formula}+disjunction : literal more_disjunction + { foldl (.|.) $1 $2 }+ +more_disjunction :: {[Formula]}+more_disjunction : {[]} | vline literal more_disjunction + { $2 : $3 }++literal :: {Formula}+literal : atomic_formula {$1} + | tilde atomic_formula { (.~.) $2} + | fol_infix_unary {$1}+ +fol_infix_unary :: {Formula}+fol_infix_unary : term infix_inequality term { $2 $1 $3 }++quantifier :: {[String] -> Formula -> Formula}+quantifier : exclam { for_all } | question { exists }++binary_connective :: {Formula -> Formula -> Formula}+binary_connective : iff { (.<=>.) }+ | implies { (.=>.) }+ | impliedby { (.<=.) }+ | xor { (.<~>.) }+ | nor { (.~|.) }+ | nand { (.~&.) }++--- assoc_connective : vline +--- | ampersand+ +unary_connective :: {Formula -> Formula}+unary_connective : tilde { (.~.) }++-- defined_type :== atomic_defined_word ++-- defined_type :== $oType | $o | $iType | $i | $tType | $real | $int+-- system_type :== atomic_system_word ++atomic_formula :: {Formula} +atomic_formula : plain_atomic_formula {$1}+ | defined_atomic_formula {$1}+ | system_atomic_formula {$1}+ ++plain_atomic_formula :: {Formula}+plain_atomic_formula : plain_term {let TT (FunApp x args) = $1 in pApp x args}++-- plain_atomic_formula :== proposition | predicate lp arguments rp +-- proposition :== predicate +-- predicate :== atomic_word ++defined_atomic_formula :: {Formula}+defined_atomic_formula : defined_plain_formula {$1} + | 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_prop | defined_pred lp arguments rp +--defined_prop :== atomic_defined_word +--defined_prop :== $true | $false+--defined_pred :== atomic_defined_word +--defined_pred :== $equal+++defined_infix_formula :: {Formula}+defined_infix_formula : term defined_infix_pred term { $2 $1 $3 }+ +defined_infix_pred :: { Term -> Term -> Formula } +defined_infix_pred : infix_equality { $1 }++infix_equality :: { Term -> Term -> Formula }+infix_equality : equals { (.=.) }+ +infix_inequality :: { Term -> Term -> Formula }+infix_inequality : nequals { (.!=.) }++system_atomic_formula :: {Formula} +system_atomic_formula : system_term {let TT (FunApp x args) = $1 in pApp x args}++term :: {Term} +term : function_term {$1}+ | variable {var $1}+ +function_term :: {Term} +function_term : plain_term {$1} + | defined_term {$1}+ | system_term {$1}++plain_term :: {Term} +plain_term : constant {fApp $1 []}+ | functor lp arguments rp {fApp $1 $3}+ +constant :: {AtomicWord}+constant : functor {$1}++functor :: {AtomicWord}+functor : atomic_word {$1}++defined_term :: {Term} +defined_term : defined_atom {$1} + | defined_atomic_term {$1}+ ++defined_atom :: {Term} +defined_atom : number {numberLitTerm $1} + | distinct_object {distinctObjectTerm (stripQuotes '"' $1)}+ +defined_atomic_term :: {Term} +defined_atomic_term : defined_plain_term {$1}+ +defined_plain_term :: {Term} +defined_plain_term : defined_constant {fApp (AtomicWord $1) []} + | defined_functor lp arguments rp {fApp (AtomicWord $1) $3} ++defined_constant :: {String}+defined_constant : defined_functor {$1}+-- defined_constant :==++defined_functor :: {String}+defined_functor : atomic_defined_word {$1}+-- defined_functor :==++system_term :: {Term} +system_term : system_constant {fApp (AtomicWord $1) []}+ | system_functor lp arguments rp {fApp (AtomicWord $1) $3} ++system_constant :: {String} +system_constant : system_functor {$1}++system_functor :: {String} +system_functor : atomic_system_word {$1}+ +variable :: {String}+variable : upper_word {$1}++arguments :: {[Term]}+arguments : term {[$1]}+ | term comma arguments { $1 : $3 }++source :: {SourceInfo} +source : general_term {SourceInfo $1}++-- source :== dag_source | internal_source | external_source | unknown++-- dag_source :== name | inference_record ++-- inference_record :== inference lp inference_rule comma useful_info comma [parent_list ] rp +-- inference_rule :== atomic_word +-- parent_list :== parent_info | parent_info comma parent_list +-- parent_info :== source parent_details +-- parent_details :== :general_list | null +-- internal_source :== introduced lp intro_type optional_info rp +-- intro_type :== definition | axiom_of_choice | tautology | assumption+-- external_source :== file_source | theory | creator_source +-- file_source :== file lp file_name file_info rp +-- file_info :== comma name | null +-- theory :== theory lp theory_name optional_info rp +-- theory_name :== equality | ac+-- creator_source :== creator lp creator_name optional_info rp +-- creator_name :== atomic_word ++optional_info :: {UsefulInfo} +optional_info : comma useful_info {$2} | {NoUsefulInfo}+ +useful_info :: { UsefulInfo }+useful_info : general_list {UsefulInfo $1}++-- useful_info :== [] | [info_items ]+-- info_items :== info_item | info_item comma info_items +-- info_item :== formula_item | inference_item | general_function +-- formula_item :== description_item | iquote_item +-- description_item :== description lp atomic_word rp +-- iquote_item :== iquote lp atomic_word rp +-- inference_item :== inference_status | assumptions_record | refutation +-- inference_status :== status lp status_value rp | inference_info +-- status_value :== suc | unp | sap | esa | sat | fsa | thm | eqv | tac | wec | eth | tau | wtc | wth | cax | sca | tca | wca |cup | csp | ecs | csa | cth | ceq | unc | wcc | ect | fun | uns | wuc | wct | scc | uca | noc++-- inference_info :== inference_rule lp atomic_word comma general_list rp +-- assumptions_record :== assumptions lp [name_list ] rp +-- refutation :== refutation lp file_source rp ++include :: {TPTP_Input}+include : include_ lp file_name formula_selection rp dot { Include $3 $4 } ++formula_selection :: {[AtomicWord]}+formula_selection : comma lbra name_list rbra { $3 } + | { [] }++name_list :: {[AtomicWord]}+name_list : name {[$1]}+ | name comma name_list { $1 : $3 }++ +general_term :: {GTerm}+general_term : general_data {GTerm $1} + | general_data colon general_term {ColonSep $1 $3} + | general_list {GList $1} ++general_data :: {GData}+general_data : atomic_word { GWord $1 } + | atomic_word lp general_terms rp { GApp $1 $3 } + | variable { GVar $1 }+ | number { GNumber $1 }+ | distinct_object { GDistinctObject (stripQuotes '"' $1) }+ | formula_data { $1 }+ +formula_data :: {GData}+formula_data : dollar_word lp fof_formula rp { GFormulaData $1 $3 }+ -- too ambiguous | dollar_word lp cnf_formula rp { GFormulaData $1 $3 }+ +general_list :: {[GTerm]}+general_list : lbra rbra {[]}+ | lbra general_terms rbra {$2}+ +general_terms :: {[GTerm]}+general_terms : general_term {[$1]} + | general_term comma general_terms {$1 : $3}++name :: {AtomicWord}+name : atomic_word {$1}+ | unsigned_integer {AtomicWord(show $1)}+ +atomic_word :: {AtomicWord} +atomic_word : lower_word_ {AtomicWord $1}+ | single_quoted{AtomicWord (stripQuotes '\'' $1)}+ +atomic_defined_word :: {String} +atomic_defined_word : dollar_word{$1}+ +atomic_system_word :: {String} +atomic_system_word : dollar_dollar_word{$1}++number :: {Double} -- maybe keep track of the number type that was actually parsed+number : real {$1} | signed_integer {fromIntegral $1} | unsigned_integer {fromIntegral $1}+ +file_name :: {String} +file_name : single_quoted {stripQuotes '\'' $1}+ +lower_word_ :: {String}+lower_word_ : lower_word {$1} | fof {"fof"} | cnf {"cnf"} | include_ {"include"} -- "fof" is a perfectly cromulent lower_word, but it is interpreted as a "fof" token+ +++++ +{++stripQuotes which (x:xs) = go xs+ where+ go [x] = []+ go ('\\':'\\':xs) = '\\':go xs+ go ('\\':which:xs) = which:go xs+ go (x:xs) = x:go xs+ + +}+
+ Setup.hs view
@@ -0,0 +1,24 @@+module Main where++import Distribution.Simple+import Distribution.Simple.Program+import Distribution.Simple.LocalBuildInfo+import System.Environment++main = defaultMain+ +--happyArgs = ["--info", "--glr", "--decode"]+-- happyArgs = ["--info","--array","--ghc"]++-- main :: IO ()+-- main = defaultMainWithHooks (simpleUserHooks { confHook = theConfHook })++-- theConfHook a b = do+-- defaultBuildInfo <- confHook simpleUserHooks a b+-- let+-- defaultWithPrograms = withPrograms defaultBuildInfo+-- theWithPrograms = userSpecifyArgs "happy" happyArgs defaultWithPrograms+ +-- return $ defaultBuildInfo { withPrograms = theWithPrograms }+ +
+ dist/build/Lexer.hs view
@@ -0,0 +1,395 @@+{-# OPTIONS -fglasgow-exts -cpp #-}+{-# LINE 1 "Lexer.x" #-}++module Lexer where++#if __GLASGOW_HASKELL__ >= 603+#include "ghcconfig.h"+#elif defined(__GLASGOW_HASKELL__)+#include "config.h"+#endif+#if __GLASGOW_HASKELL__ >= 503+import Data.Array+import Data.Char (ord)+import Data.Array.Base (unsafeAt)+#else+import Array+import Char (ord)+#endif+#if __GLASGOW_HASKELL__ >= 503+import GHC.Exts+#else+import GlaExts+#endif+{-# LINE 1 "templates/wrappers.hs" #-}+{-# LINE 1 "templates/wrappers.hs" #-}+{-# LINE 1 "<built-in>" #-}+{-# LINE 1 "<command-line>" #-}+{-# LINE 1 "templates/wrappers.hs" #-}+-- -----------------------------------------------------------------------------+-- Alex wrapper code.+--+-- This code is in the PUBLIC DOMAIN; you may copy it freely and use+-- it for any purpose whatsoever.++{-# LINE 18 "templates/wrappers.hs" #-}++-- -----------------------------------------------------------------------------+-- The input type+++type AlexInput = (AlexPosn, -- current position,+ Char, -- previous char+ String) -- current input string++alexInputPrevChar :: AlexInput -> Char+alexInputPrevChar (p,c,s) = c++alexGetChar :: AlexInput -> Maybe (Char,AlexInput)+alexGetChar (p,c,[]) = Nothing+alexGetChar (p,_,(c:s)) = let p' = alexMove p c in p' `seq`+ Just (c, (p', c, s))+++{-# LINE 51 "templates/wrappers.hs" #-}++-- -----------------------------------------------------------------------------+-- Token positions++-- `Posn' records the location of a token in the input text. It has three+-- fields: the address (number of chacaters preceding the token), line number+-- and column of a token within the file. `start_pos' gives the position of the+-- start of the file and `eof_pos' a standard encoding for the end of file.+-- `move_pos' calculates the new position after traversing a given character,+-- assuming the usual eight character tab stops.+++data AlexPosn = AlexPn !Int !Int !Int+ deriving (Eq,Show)++alexStartPos :: AlexPosn+alexStartPos = AlexPn 0 1 1++alexMove :: AlexPosn -> Char -> AlexPosn+alexMove (AlexPn a l c) '\t' = AlexPn (a+1) l (((c+7) `div` 8)*8+1)+alexMove (AlexPn a l c) '\n' = AlexPn (a+1) (l+1) 1+alexMove (AlexPn a l c) _ = AlexPn (a+1) l (c+1)+++-- -----------------------------------------------------------------------------+-- Default monad++{-# LINE 162 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- Monad (with ByteString input)++{-# LINE 251 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- Basic wrapper++{-# LINE 273 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- Basic wrapper, ByteString version++{-# LINE 297 "templates/wrappers.hs" #-}++{-# LINE 322 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- Posn wrapper++-- Adds text positions to the basic model.+++--alexScanTokens :: String -> [token]+alexScanTokens str = go (alexStartPos,'\n',str)+ where go inp@(pos,_,str) =+ case alexScan inp 0 of+ AlexEOF -> []+ AlexError _ -> error "lexical error"+ AlexSkip inp' len -> go inp'+ AlexToken inp' len act -> act pos (take len str) : go inp'++++-- -----------------------------------------------------------------------------+-- Posn wrapper, ByteString version++{-# LINE 354 "templates/wrappers.hs" #-}+++-- -----------------------------------------------------------------------------+-- GScan wrapper++-- For compatibility with previous versions of Alex, and because we can.++alex_base :: AlexAddr+alex_base = AlexA# "\xf8\xff\xff\xff\x6e\x00\x00\x00\x73\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc9\xff\xff\xff\x00\x00\x00\x00\xca\xff\xff\xff\xcb\xff\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xd6\xff\xff\xff\xcc\xff\xff\xff\x00\x00\x00\x00\xfd\xff\xff\xff\x01\x00\x00\x00\x02\x00\x00\x00\x00\x00\x00\x00\xe3\xff\xff\xff\xe5\xff\xff\xff\xe4\xff\xff\xff\xe6\xff\xff\xff\xe7\xff\xff\xff\xeb\xff\xff\xff\x00\x00\x00\x00\x4c\x00\x00\x00\x4e\x00\x00\x00\x30\x00\x00\x00\x00\x00\x00\x00\x77\x00\x00\x00\x78\x00\x00\x00\x61\x00\x00\x00\x94\x00\x00\x00\xdf\x00\x00\x00\xf9\x00\x00\x00\x16\x01\x00\x00\x61\x01\x00\x00\xac\x01\x00\x00\xf7\x01\x00\x00\x42\x02\x00\x00\x8d\x02\x00\x00\xd8\x02\x00\x00\x00\x00\x00\x00\x6b\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x23\x03\x00\x00\x2d\x03\x00\x00\x7b\x00\x00\x00\x43\x03\x00\x00\x4d\x03\x00\x00\x63\x03\x00\x00\x6f\x03\x00\x00\x85\x03\x00\x00\xa7\x03\x00\x00\xbd\x03\x00\x00\x8a\x00\x00\x00\x8b\x00\x00\x00\x79\x03\x00\x00\x8f\x03\x00\x00\xdd\x03\x00\x00\xc7\x03\x00\x00"#++alex_table :: AlexAddr+alex_table = AlexA# "\x00\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x09\x00\xff\xff\x0d\x00\x0c\x00\x0e\x00\xff\xff\xff\xff\x1e\x00\x1d\x00\x1e\x00\x1d\x00\x1d\x00\x1c\x00\x0b\x00\x1c\x00\x1f\x00\x00\x00\x00\x00\x02\x00\x08\x00\x28\x00\x1a\x00\x2e\x00\x19\x00\x0f\x00\x24\x00\x03\x00\x06\x00\x35\x00\x36\x00\x07\x00\x45\x00\x18\x00\x22\x00\x44\x00\x41\x00\x41\x00\x41\x00\x41\x00\x41\x00\x41\x00\x41\x00\x41\x00\x41\x00\x15\x00\x13\x00\x16\x00\x0a\x00\x37\x00\x14\x00\x00\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x31\x00\x04\x00\x17\x00\x05\x00\xff\xff\x25\x00\xff\xff\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x33\x00\x23\x00\x10\x00\x23\x00\x11\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\x02\x00\xff\xff\xff\xff\x29\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x12\x00\x00\x00\x00\x00\x25\x00\x00\x00\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x27\x00\x27\x00\x43\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x00\x00\x00\x00\x00\x00\x26\x00\x00\x00\x26\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x00\x00\x00\x00\x00\x00\x46\x00\x46\x00\x00\x00\x00\x00\x00\x00\x29\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x00\x00\x47\x00\x47\x00\x00\x00\x00\x00\x2a\x00\x2a\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x47\x00\x47\x00\x00\x00\x00\x00\x2c\x00\x00\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2d\x00\x00\x00\x00\x00\x00\x00\x2c\x00\x00\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2c\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x2b\x00\x00\x00\x00\x00\x00\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x2f\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x00\x00\x00\x00\x00\x00\x00\x00\x30\x00\x00\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x00\x00\x00\x00\x00\x00\x00\x00\x30\x00\x00\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x30\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x00\x00\x00\x00\x00\x00\x00\x00\x32\x00\x00\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x00\x00\x00\x00\x00\x00\x00\x00\x32\x00\x00\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x32\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x00\x00\x00\x00\x00\x00\x00\x00\x34\x00\x00\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x00\x00\x00\x00\x00\x00\x00\x00\x34\x00\x00\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x34\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x3a\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x47\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3c\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x47\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x3e\x00\x46\x00\x00\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x43\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x3f\x00\x46\x00\x47\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x40\x00\x39\x00\x39\x00\x39\x00\x39\x00\x39\x00\x39\x00\x39\x00\x39\x00\x39\x00\x39\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x47\x00\x46\x00\x00\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x47\x00\x46\x00\x47\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x42\x00\x38\x00\x3b\x00\x3b\x00\x3b\x00\x3b\x00\x3b\x00\x3b\x00\x3b\x00\x3b\x00\x3b\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x48\x00\x00\x00\x48\x00\x00\x00\x47\x00\x38\x00\x3d\x00\x3d\x00\x3d\x00\x3d\x00\x3d\x00\x3d\x00\x3d\x00\x3d\x00\x3d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#++alex_check :: AlexAddr+alex_check = AlexA# "\xff\xff\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x3d\x00\x0a\x00\x3e\x00\x3e\x00\x3e\x00\x0a\x00\x0a\x00\x2a\x00\x2a\x00\x2a\x00\x2a\x00\x2a\x00\x2f\x00\x3d\x00\x2f\x00\x2a\x00\xff\xff\xff\xff\x20\x00\x21\x00\x22\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x26\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x5b\x00\x7e\x00\x5d\x00\x0a\x00\x27\x00\x0a\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x27\x00\x7c\x00\x27\x00\x7e\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x0a\x00\x0a\x00\x22\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7c\x00\xff\xff\xff\xff\x5c\x00\xff\xff\x20\x00\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x22\x00\x22\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\x5c\x00\xff\xff\x5c\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\x2e\x00\x2e\x00\xff\xff\xff\xff\xff\xff\x5c\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\x45\x00\x45\x00\xff\xff\xff\xff\x5c\x00\x5c\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x65\x00\x65\x00\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\x24\x00\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\x45\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x45\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\x65\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x65\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x2e\x00\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x2e\x00\x45\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\x45\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x65\x00\x2e\x00\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x65\x00\x2e\x00\x45\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\x45\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x2b\x00\xff\xff\x2d\x00\xff\xff\x65\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x65\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#++alex_deflt :: AlexAddr+alex_deflt = AlexA# "\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x1b\x00\x1b\x00\x1b\x00\xff\xff\x20\x00\x20\x00\x21\x00\x21\x00\x21\x00\xff\xff\xff\xff\x25\x00\x25\x00\xff\xff\xff\xff\x29\x00\x29\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#++alex_accept = listArray (0::Int,72) [[],[],[(AlexAccSkip)],[(AlexAcc (alex_action_1))],[(AlexAcc (alex_action_2))],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_4))],[(AlexAcc (alex_action_5))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[(AlexAcc (alex_action_6))],[],[],[(AlexAcc (alex_action_7))],[(AlexAcc (alex_action_8))],[(AlexAcc (alex_action_8))],[(AlexAcc (alex_action_8))],[(AlexAcc (alex_action_9))],[],[],[],[],[],[],[(AlexAcc (alex_action_10))],[],[],[],[(AlexAcc (alex_action_11))],[],[],[],[(AlexAcc (alex_action_12))],[(AlexAcc (alex_action_12))],[],[],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_13))],[(AlexAcc (alex_action_14))],[(AlexAcc (alex_action_14))],[(AlexAcc (alex_action_15))],[(AlexAcc (alex_action_15))],[(AlexAcc (alex_action_16))],[(AlexAcc (alex_action_17))],[(AlexAcc (alex_action_18))],[(AlexAcc (alex_action_19))],[(AlexAcc (alex_action_19))],[(AlexAcc (alex_action_19))],[(AlexAcc (alex_action_19))],[(AlexAcc (alex_action_19))],[(AlexAcc (alex_action_19))],[(AlexAcc (alex_action_19))],[(AlexAcc (alex_action_20))],[(AlexAcc (alex_action_20))],[(AlexAcc (alex_action_21))],[(AlexAcc (alex_action_21))],[(AlexAcc (alex_action_20))],[(AlexAcc (alex_action_21))],[],[],[],[]]+{-# LINE 62 "Lexer.x" #-}++-- Each action has type :: String -> Token++withPos f pos s = (pos, f s)++-- The token type:+data Token = + LP + | RP + | Comma + | Dot + | Lbrack + | Rbrack+ | Oper String+ | SingleQuoted String+ | DoubleQuoted String+ | DollarWord String + | DollarDollarWord String+ | UpperWord String+ | LowerWord String+ | Star+ | Plus+ | Rangle+ | SignedInt Int+ | UnsignedInt Int+ | Real Double+ | CommentToken String+ deriving (Eq,Ord,Show)++-- alex defines: alexScanTokens++stripPlus ('+':xs) = xs+stripPlus xs = xs++alex_action_1 = withPos $ const LP +alex_action_2 = withPos $ const Lbrack +alex_action_3 = withPos $ const Rbrack +alex_action_4 = withPos $ const RP +alex_action_5 = withPos $ const Comma +alex_action_6 = withPos $ Oper +alex_action_7 = withPos $ const Dot +alex_action_8 = withPos $ CommentToken +alex_action_9 = withPos $ CommentToken +alex_action_10 = withPos SingleQuoted +alex_action_11 = withPos DoubleQuoted +alex_action_12 = withPos DollarDollarWord +alex_action_13 = withPos DollarWord +alex_action_14 = withPos UpperWord +alex_action_15 = withPos LowerWord +alex_action_16 = withPos $ const Star +alex_action_17 = withPos $ const Plus +alex_action_18 = withPos $ const Rangle +alex_action_19 = withPos (Real . read . stripPlus) +alex_action_20 = withPos (SignedInt . read . stripPlus) +alex_action_21 = withPos (UnsignedInt . read . stripPlus) +{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "<built-in>" #-}+{-# LINE 1 "<command-line>" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+-- -----------------------------------------------------------------------------+-- ALEX TEMPLATE+--+-- This code is in the PUBLIC DOMAIN; you may copy it freely and use+-- it for any purpose whatsoever.++-- -----------------------------------------------------------------------------+-- INTERNALS and main scanner engine++{-# LINE 35 "templates/GenericTemplate.hs" #-}++{-# LINE 45 "templates/GenericTemplate.hs" #-}+++data AlexAddr = AlexA# Addr#++#if __GLASGOW_HASKELL__ < 503+uncheckedShiftL# = shiftL#+#endif++{-# INLINE alexIndexInt16OffAddr #-}+alexIndexInt16OffAddr (AlexA# arr) off =+#ifdef WORDS_BIGENDIAN+ narrow16Int# i+ where+ i = word2Int# ((high `uncheckedShiftL#` 8#) `or#` low)+ high = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ low = int2Word# (ord# (indexCharOffAddr# arr off'))+ off' = off *# 2#+#else+ indexInt16OffAddr# arr off+#endif++++++{-# INLINE alexIndexInt32OffAddr #-}+alexIndexInt32OffAddr (AlexA# arr) off = +#ifdef WORDS_BIGENDIAN+ narrow32Int# i+ where+ i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#`+ (b2 `uncheckedShiftL#` 16#) `or#`+ (b1 `uncheckedShiftL#` 8#) `or#` b0)+ b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#)))+ b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#)))+ b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ b0 = int2Word# (ord# (indexCharOffAddr# arr off'))+ off' = off *# 4#+#else+ indexInt32OffAddr# arr off+#endif++++++#if __GLASGOW_HASKELL__ < 503+quickIndex arr i = arr ! i+#else+-- GHC >= 503, unsafeAt is available from Data.Array.Base.+quickIndex = unsafeAt+#endif+++++-- -----------------------------------------------------------------------------+-- Main lexing routines++data AlexReturn a+ = AlexEOF+ | AlexError !AlexInput+ | AlexSkip !AlexInput !Int+ | AlexToken !AlexInput !Int a++-- alexScan :: AlexInput -> StartCode -> AlexReturn a+alexScan input (I# (sc))+ = alexScanUser undefined input (I# (sc))++alexScanUser user input (I# (sc))+ = case alex_scan_tkn user input 0# input sc AlexNone of+ (AlexNone, input') ->+ case alexGetChar input of+ Nothing -> ++++ AlexEOF+ Just _ ->++++ AlexError input'++ (AlexLastSkip input len, _) ->++++ AlexSkip input len++ (AlexLastAcc k input len, _) ->++++ AlexToken input len k+++-- Push the input through the DFA, remembering the most recent accepting+-- state it encountered.++alex_scan_tkn user orig_input len input s last_acc =+ input `seq` -- strict in the input+ let + new_acc = check_accs (alex_accept `quickIndex` (I# (s)))+ in+ new_acc `seq`+ case alexGetChar input of+ Nothing -> (new_acc, input)+ Just (c, new_input) -> ++++ let+ base = alexIndexInt32OffAddr alex_base s+ (I# (ord_c)) = ord c+ offset = (base +# ord_c)+ check = alexIndexInt16OffAddr alex_check offset+ + new_s = if (offset >=# 0#) && (check ==# ord_c)+ then alexIndexInt16OffAddr alex_table offset+ else alexIndexInt16OffAddr alex_deflt s+ in+ case new_s of + -1# -> (new_acc, input)+ -- on an error, we want to keep the input *before* the+ -- character that failed, not after.+ _ -> alex_scan_tkn user orig_input (len +# 1#) + new_input new_s new_acc++ where+ check_accs [] = last_acc+ check_accs (AlexAcc a : _) = AlexLastAcc a input (I# (len))+ check_accs (AlexAccSkip : _) = AlexLastSkip input (I# (len))+ check_accs (AlexAccPred a pred : rest)+ | pred user orig_input (I# (len)) input+ = AlexLastAcc a input (I# (len))+ check_accs (AlexAccSkipPred pred : rest)+ | pred user orig_input (I# (len)) input+ = AlexLastSkip input (I# (len))+ check_accs (_ : rest) = check_accs rest++data AlexLastAcc a+ = AlexNone+ | AlexLastAcc a !AlexInput !Int+ | AlexLastSkip !AlexInput !Int++data AlexAcc a user+ = AlexAcc a+ | AlexAccSkip+ | AlexAccPred a (AlexAccPred user)+ | AlexAccSkipPred (AlexAccPred user)++type AlexAccPred user = user -> AlexInput -> Int -> AlexInput -> Bool++-- -----------------------------------------------------------------------------+-- Predicates on a rule++alexAndPred p1 p2 user in1 len in2+ = p1 user in1 len in2 && p2 user in1 len in2++--alexPrevCharIsPred :: Char -> AlexAccPred _ +alexPrevCharIs c _ input _ _ = c == alexInputPrevChar input++--alexPrevCharIsOneOfPred :: Array Char Bool -> AlexAccPred _ +alexPrevCharIsOneOf arr _ input _ _ = arr ! alexInputPrevChar input++--alexRightContext :: Int -> AlexAccPred _+alexRightContext (I# (sc)) user _ _ input = + case alex_scan_tkn user input 0# input sc AlexNone of+ (AlexNone, _) -> False+ _ -> True+ -- TODO: there's no need to find the longest+ -- match when checking the right context, just+ -- the first match will do.++-- used by wrappers+iUnbox (I# (i)) = i
+ dist/build/Parser.hs view
@@ -0,0 +1,1939 @@+{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}+{-# OPTIONS -fglasgow-exts -cpp #-}+{-# OPTIONS -XDeriveDataTypeable -XCPP #-}+module Parser where+ +import Data.Char+import Data.Data+import Control.Monad+import Data.List as L+import Lexer+import Data.Set as S+import Codec.TPTP.Base+import System.IO+import System.IO.Unsafe+#if __GLASGOW_HASKELL__ >= 503+import qualified Data.Array as Happy_Data_Array+#else+import qualified Array as Happy_Data_Array+#endif+#if __GLASGOW_HASKELL__ >= 503+import qualified GHC.Exts as Happy_GHC_Exts+#else+import qualified GlaExts as Happy_GHC_Exts+#endif++-- parser produced by Happy Version 1.18.5++newtype HappyAbsSyn = HappyAbsSyn HappyAny+#if __GLASGOW_HASKELL__ >= 607+type HappyAny = Happy_GHC_Exts.Any+#else+type HappyAny = forall a . a+#endif+happyIn4 :: ([TPTP_Input]) -> (HappyAbsSyn )+happyIn4 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn4 #-}+happyOut4 :: (HappyAbsSyn ) -> ([TPTP_Input])+happyOut4 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut4 #-}+happyIn5 :: (TPTP_Input) -> (HappyAbsSyn )+happyIn5 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn5 #-}+happyOut5 :: (HappyAbsSyn ) -> (TPTP_Input)+happyOut5 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut5 #-}+happyIn6 :: (TPTP_Input) -> (HappyAbsSyn )+happyIn6 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn6 #-}+happyOut6 :: (HappyAbsSyn ) -> (TPTP_Input)+happyOut6 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut6 #-}+happyIn7 :: (TPTP_Input) -> (HappyAbsSyn )+happyIn7 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn7 #-}+happyOut7 :: (HappyAbsSyn ) -> (TPTP_Input)+happyOut7 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut7 #-}+happyIn8 :: (TPTP_Input) -> (HappyAbsSyn )+happyIn8 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn8 #-}+happyOut8 :: (HappyAbsSyn ) -> (TPTP_Input)+happyOut8 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut8 #-}+happyIn9 :: ((SourceInfo,UsefulInfo)) -> (HappyAbsSyn )+happyIn9 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn9 #-}+happyOut9 :: (HappyAbsSyn ) -> ((SourceInfo,UsefulInfo))+happyOut9 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut9 #-}+happyIn10 :: (Role) -> (HappyAbsSyn )+happyIn10 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn10 #-}+happyOut10 :: (HappyAbsSyn ) -> (Role)+happyOut10 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut10 #-}+happyIn11 :: (Formula) -> (HappyAbsSyn )+happyIn11 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn11 #-}+happyOut11 :: (HappyAbsSyn ) -> (Formula)+happyOut11 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut11 #-}+happyIn12 :: (Formula) -> (HappyAbsSyn )+happyIn12 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn12 #-}+happyOut12 :: (HappyAbsSyn ) -> (Formula)+happyOut12 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut12 #-}+happyIn13 :: (Formula) -> (HappyAbsSyn )+happyIn13 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn13 #-}+happyOut13 :: (HappyAbsSyn ) -> (Formula)+happyOut13 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut13 #-}+happyIn14 :: (Formula) -> (HappyAbsSyn )+happyIn14 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn14 #-}+happyOut14 :: (HappyAbsSyn ) -> (Formula)+happyOut14 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut14 #-}+happyIn15 :: (Formula) -> (HappyAbsSyn )+happyIn15 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn15 #-}+happyOut15 :: (HappyAbsSyn ) -> (Formula)+happyOut15 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut15 #-}+happyIn16 :: ([Formula]) -> (HappyAbsSyn )+happyIn16 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn16 #-}+happyOut16 :: (HappyAbsSyn ) -> ([Formula])+happyOut16 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut16 #-}+happyIn17 :: (Formula) -> (HappyAbsSyn )+happyIn17 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn17 #-}+happyOut17 :: (HappyAbsSyn ) -> (Formula)+happyOut17 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut17 #-}+happyIn18 :: ([Formula]) -> (HappyAbsSyn )+happyIn18 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn18 #-}+happyOut18 :: (HappyAbsSyn ) -> ([Formula])+happyOut18 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut18 #-}+happyIn19 :: (Formula) -> (HappyAbsSyn )+happyIn19 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn19 #-}+happyOut19 :: (HappyAbsSyn ) -> (Formula)+happyOut19 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut19 #-}+happyIn20 :: (Formula) -> (HappyAbsSyn )+happyIn20 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn20 #-}+happyOut20 :: (HappyAbsSyn ) -> (Formula)+happyOut20 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut20 #-}+happyIn21 :: ([String]) -> (HappyAbsSyn )+happyIn21 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn21 #-}+happyOut21 :: (HappyAbsSyn ) -> ([String])+happyOut21 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut21 #-}+happyIn22 :: (Formula) -> (HappyAbsSyn )+happyIn22 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn22 #-}+happyOut22 :: (HappyAbsSyn ) -> (Formula)+happyOut22 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut22 #-}+happyIn23 :: (Formula) -> (HappyAbsSyn )+happyIn23 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn23 #-}+happyOut23 :: (HappyAbsSyn ) -> (Formula)+happyOut23 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut23 #-}+happyIn24 :: (Formula) -> (HappyAbsSyn )+happyIn24 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn24 #-}+happyOut24 :: (HappyAbsSyn ) -> (Formula)+happyOut24 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut24 #-}+happyIn25 :: ([Formula]) -> (HappyAbsSyn )+happyIn25 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn25 #-}+happyOut25 :: (HappyAbsSyn ) -> ([Formula])+happyOut25 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut25 #-}+happyIn26 :: (Formula) -> (HappyAbsSyn )+happyIn26 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn26 #-}+happyOut26 :: (HappyAbsSyn ) -> (Formula)+happyOut26 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut26 #-}+happyIn27 :: (Formula) -> (HappyAbsSyn )+happyIn27 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn27 #-}+happyOut27 :: (HappyAbsSyn ) -> (Formula)+happyOut27 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut27 #-}+happyIn28 :: ([String] -> Formula -> Formula) -> (HappyAbsSyn )+happyIn28 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn28 #-}+happyOut28 :: (HappyAbsSyn ) -> ([String] -> Formula -> Formula)+happyOut28 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut28 #-}+happyIn29 :: (Formula -> Formula -> Formula) -> (HappyAbsSyn )+happyIn29 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn29 #-}+happyOut29 :: (HappyAbsSyn ) -> (Formula -> Formula -> Formula)+happyOut29 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut29 #-}+happyIn30 :: (Formula -> Formula) -> (HappyAbsSyn )+happyIn30 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn30 #-}+happyOut30 :: (HappyAbsSyn ) -> (Formula -> Formula)+happyOut30 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut30 #-}+happyIn31 :: (Formula) -> (HappyAbsSyn )+happyIn31 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn31 #-}+happyOut31 :: (HappyAbsSyn ) -> (Formula)+happyOut31 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut31 #-}+happyIn32 :: (Formula) -> (HappyAbsSyn )+happyIn32 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn32 #-}+happyOut32 :: (HappyAbsSyn ) -> (Formula)+happyOut32 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut32 #-}+happyIn33 :: (Formula) -> (HappyAbsSyn )+happyIn33 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn33 #-}+happyOut33 :: (HappyAbsSyn ) -> (Formula)+happyOut33 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut33 #-}+happyIn34 :: (Formula) -> (HappyAbsSyn )+happyIn34 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn34 #-}+happyOut34 :: (HappyAbsSyn ) -> (Formula)+happyOut34 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut34 #-}+happyIn35 :: (Formula) -> (HappyAbsSyn )+happyIn35 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn35 #-}+happyOut35 :: (HappyAbsSyn ) -> (Formula)+happyOut35 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut35 #-}+happyIn36 :: (Term -> Term -> Formula) -> (HappyAbsSyn )+happyIn36 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn36 #-}+happyOut36 :: (HappyAbsSyn ) -> (Term -> Term -> Formula)+happyOut36 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut36 #-}+happyIn37 :: (Term -> Term -> Formula) -> (HappyAbsSyn )+happyIn37 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn37 #-}+happyOut37 :: (HappyAbsSyn ) -> (Term -> Term -> Formula)+happyOut37 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut37 #-}+happyIn38 :: (Term -> Term -> Formula) -> (HappyAbsSyn )+happyIn38 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn38 #-}+happyOut38 :: (HappyAbsSyn ) -> (Term -> Term -> Formula)+happyOut38 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut38 #-}+happyIn39 :: (Formula) -> (HappyAbsSyn )+happyIn39 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn39 #-}+happyOut39 :: (HappyAbsSyn ) -> (Formula)+happyOut39 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut39 #-}+happyIn40 :: (Term) -> (HappyAbsSyn )+happyIn40 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn40 #-}+happyOut40 :: (HappyAbsSyn ) -> (Term)+happyOut40 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut40 #-}+happyIn41 :: (Term) -> (HappyAbsSyn )+happyIn41 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn41 #-}+happyOut41 :: (HappyAbsSyn ) -> (Term)+happyOut41 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut41 #-}+happyIn42 :: (Term) -> (HappyAbsSyn )+happyIn42 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn42 #-}+happyOut42 :: (HappyAbsSyn ) -> (Term)+happyOut42 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut42 #-}+happyIn43 :: (AtomicWord) -> (HappyAbsSyn )+happyIn43 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn43 #-}+happyOut43 :: (HappyAbsSyn ) -> (AtomicWord)+happyOut43 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut43 #-}+happyIn44 :: (AtomicWord) -> (HappyAbsSyn )+happyIn44 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn44 #-}+happyOut44 :: (HappyAbsSyn ) -> (AtomicWord)+happyOut44 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut44 #-}+happyIn45 :: (Term) -> (HappyAbsSyn )+happyIn45 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn45 #-}+happyOut45 :: (HappyAbsSyn ) -> (Term)+happyOut45 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut45 #-}+happyIn46 :: (Term) -> (HappyAbsSyn )+happyIn46 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn46 #-}+happyOut46 :: (HappyAbsSyn ) -> (Term)+happyOut46 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut46 #-}+happyIn47 :: (Term) -> (HappyAbsSyn )+happyIn47 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn47 #-}+happyOut47 :: (HappyAbsSyn ) -> (Term)+happyOut47 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut47 #-}+happyIn48 :: (Term) -> (HappyAbsSyn )+happyIn48 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn48 #-}+happyOut48 :: (HappyAbsSyn ) -> (Term)+happyOut48 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut48 #-}+happyIn49 :: (String) -> (HappyAbsSyn )+happyIn49 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn49 #-}+happyOut49 :: (HappyAbsSyn ) -> (String)+happyOut49 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut49 #-}+happyIn50 :: (String) -> (HappyAbsSyn )+happyIn50 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn50 #-}+happyOut50 :: (HappyAbsSyn ) -> (String)+happyOut50 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut50 #-}+happyIn51 :: (Term) -> (HappyAbsSyn )+happyIn51 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn51 #-}+happyOut51 :: (HappyAbsSyn ) -> (Term)+happyOut51 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut51 #-}+happyIn52 :: (String) -> (HappyAbsSyn )+happyIn52 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn52 #-}+happyOut52 :: (HappyAbsSyn ) -> (String)+happyOut52 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut52 #-}+happyIn53 :: (String) -> (HappyAbsSyn )+happyIn53 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn53 #-}+happyOut53 :: (HappyAbsSyn ) -> (String)+happyOut53 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut53 #-}+happyIn54 :: (String) -> (HappyAbsSyn )+happyIn54 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn54 #-}+happyOut54 :: (HappyAbsSyn ) -> (String)+happyOut54 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut54 #-}+happyIn55 :: ([Term]) -> (HappyAbsSyn )+happyIn55 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn55 #-}+happyOut55 :: (HappyAbsSyn ) -> ([Term])+happyOut55 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut55 #-}+happyIn56 :: (SourceInfo) -> (HappyAbsSyn )+happyIn56 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn56 #-}+happyOut56 :: (HappyAbsSyn ) -> (SourceInfo)+happyOut56 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut56 #-}+happyIn57 :: (UsefulInfo) -> (HappyAbsSyn )+happyIn57 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn57 #-}+happyOut57 :: (HappyAbsSyn ) -> (UsefulInfo)+happyOut57 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut57 #-}+happyIn58 :: (UsefulInfo) -> (HappyAbsSyn )+happyIn58 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn58 #-}+happyOut58 :: (HappyAbsSyn ) -> (UsefulInfo)+happyOut58 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut58 #-}+happyIn59 :: (TPTP_Input) -> (HappyAbsSyn )+happyIn59 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn59 #-}+happyOut59 :: (HappyAbsSyn ) -> (TPTP_Input)+happyOut59 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut59 #-}+happyIn60 :: ([AtomicWord]) -> (HappyAbsSyn )+happyIn60 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn60 #-}+happyOut60 :: (HappyAbsSyn ) -> ([AtomicWord])+happyOut60 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut60 #-}+happyIn61 :: ([AtomicWord]) -> (HappyAbsSyn )+happyIn61 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn61 #-}+happyOut61 :: (HappyAbsSyn ) -> ([AtomicWord])+happyOut61 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut61 #-}+happyIn62 :: (GTerm) -> (HappyAbsSyn )+happyIn62 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn62 #-}+happyOut62 :: (HappyAbsSyn ) -> (GTerm)+happyOut62 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut62 #-}+happyIn63 :: (GData) -> (HappyAbsSyn )+happyIn63 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn63 #-}+happyOut63 :: (HappyAbsSyn ) -> (GData)+happyOut63 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut63 #-}+happyIn64 :: (GData) -> (HappyAbsSyn )+happyIn64 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn64 #-}+happyOut64 :: (HappyAbsSyn ) -> (GData)+happyOut64 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut64 #-}+happyIn65 :: ([GTerm]) -> (HappyAbsSyn )+happyIn65 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn65 #-}+happyOut65 :: (HappyAbsSyn ) -> ([GTerm])+happyOut65 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut65 #-}+happyIn66 :: ([GTerm]) -> (HappyAbsSyn )+happyIn66 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn66 #-}+happyOut66 :: (HappyAbsSyn ) -> ([GTerm])+happyOut66 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut66 #-}+happyIn67 :: (AtomicWord) -> (HappyAbsSyn )+happyIn67 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn67 #-}+happyOut67 :: (HappyAbsSyn ) -> (AtomicWord)+happyOut67 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut67 #-}+happyIn68 :: (AtomicWord) -> (HappyAbsSyn )+happyIn68 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn68 #-}+happyOut68 :: (HappyAbsSyn ) -> (AtomicWord)+happyOut68 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut68 #-}+happyIn69 :: (String) -> (HappyAbsSyn )+happyIn69 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn69 #-}+happyOut69 :: (HappyAbsSyn ) -> (String)+happyOut69 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut69 #-}+happyIn70 :: (String) -> (HappyAbsSyn )+happyIn70 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn70 #-}+happyOut70 :: (HappyAbsSyn ) -> (String)+happyOut70 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut70 #-}+happyIn71 :: (Double) -> (HappyAbsSyn )+happyIn71 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn71 #-}+happyOut71 :: (HappyAbsSyn ) -> (Double)+happyOut71 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut71 #-}+happyIn72 :: (String) -> (HappyAbsSyn )+happyIn72 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn72 #-}+happyOut72 :: (HappyAbsSyn ) -> (String)+happyOut72 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut72 #-}+happyIn73 :: (String) -> (HappyAbsSyn )+happyIn73 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyIn73 #-}+happyOut73 :: (HappyAbsSyn ) -> (String)+happyOut73 x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOut73 #-}+happyInTok :: (Token) -> (HappyAbsSyn )+happyInTok x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyInTok #-}+happyOutTok :: (HappyAbsSyn ) -> (Token)+happyOutTok x = Happy_GHC_Exts.unsafeCoerce# x+{-# INLINE happyOutTok #-}+++happyActOffsets :: HappyAddr+happyActOffsets = HappyA# "\x3d\x00\x00\x00\x4a\x01\x3d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x6c\x01\x68\x01\x63\x01\x00\x00\x46\x01\x77\x01\x77\x01\x00\x00\x5b\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x5a\x01\x59\x01\x00\x00\x45\x01\x43\x01\x9c\x00\x9c\x00\x40\x01\x00\x00\x39\x01\x77\x01\x32\x01\x00\x00\x37\x01\x35\x01\x02\x03\xf2\x02\x34\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4d\x01\x00\x00\x00\x00\x00\x00\x33\x01\xf2\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x82\x00\x00\x00\x67\x00\x00\x00\x31\x01\x00\x00\x00\x00\x00\x00\x65\x00\x00\x00\x2c\x01\x11\x00\x00\x00\x0f\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0a\x01\x00\x00\xf8\x00\x00\x00\x00\x00\xd3\x00\x09\x01\x77\x01\x00\x00\x00\x00\x00\x00\xf3\x00\x01\x01\x00\x00\xd3\x00\xd6\x00\xe9\x03\xd5\x00\x09\x01\x09\x01\x09\x01\x09\x01\x00\x00\x09\x01\x00\x00\x00\x00\x00\x00\xe0\x00\xf2\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf2\x02\xf2\x02\xcb\x00\xca\x00\xb6\x00\xc4\x00\x00\x00\xc7\x00\xc5\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc3\x00\xbb\x00\xb9\x00\xb8\x00\x00\x00\x00\x00\xb4\x00\x00\x00\xad\x00\x00\x00\x00\x00\xa1\x00\x00\x00\xdd\x03\x00\x00\xa0\x00\x90\x00\x8a\x00\x00\x00\x00\x00\x00\x00\xf2\x02\x94\x00\x91\x00\x00\x00\xe9\x03\xe9\x03\x00\x00\x8e\x00\x00\x00\x00\x00\x00\x00\x09\x01\x6d\x00\x84\x00\x00\x00\xf2\x02\x00\x00\xf2\x02\x00\x00\x6f\x00\x66\x00\xf2\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x58\x00\x00\x00\xe9\x03\x52\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#++happyGotoOffsets :: HappyAddr+happyGotoOffsets = HappyA# "\x7c\x00\x00\x00\x00\x00\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0e\x00\x35\x00\xf9\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00\xfc\xff\xfb\xff\x00\x00\x00\x00\x00\x00\xc2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x34\x02\x80\x00\x48\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x2d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x02\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x1b\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x41\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x3a\x00\x00\x00\x20\x00\x00\x00\x00\x00\x64\x02\xbf\x02\x7f\x00\x00\x00\x00\x00\x00\x00\x42\x00\x00\x00\x00\x00\x94\x02\x00\x00\xfc\x03\x00\x00\x69\x03\x47\x03\x25\x03\xad\x03\x00\x00\x8b\x03\x00\x00\x00\x00\x00\x00\x05\x00\xca\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x93\x01\x5c\x01\x00\x00\x00\x00\x18\x00\x0a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xd9\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xef\x03\x00\x00\x00\x00\x00\x00\x06\x00\x00\x00\x00\x00\x00\x00\x02\x00\x00\x00\x00\x00\x00\x00\xe2\x03\x08\x04\x00\x00\xda\xff\x00\x00\x00\x00\x00\x00\x03\x03\x04\x00\x00\x00\x00\x00\x25\x01\x00\x00\xee\x00\x00\x00\x07\x00\xfa\xff\xb7\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xd5\x03\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#++happyDefActions :: HappyAddr+happyDefActions = HappyA# "\xfe\xff\x00\x00\x00\x00\xfe\xff\xfc\xff\xf9\xff\xf8\xff\xfb\xff\x00\x00\x00\x00\x00\x00\xfa\xff\x00\x00\x00\x00\x00\x00\xfd\xff\x00\x00\x8e\xff\x8c\xff\x83\xff\x82\xff\x81\xff\x8b\xff\x84\xff\x8d\xff\x00\x00\x9f\xff\x85\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf3\xff\x00\x00\x00\x00\x00\x00\xa1\xff\x00\x00\x9e\xff\x00\x00\x00\x00\xf4\xff\xf2\xff\xf0\xff\xef\xff\xed\xff\xec\xff\xf1\xff\xe5\xff\xe4\xff\xdd\xff\x00\x00\x00\x00\xe3\xff\xca\xff\xc9\xff\xc6\xff\xc5\xff\xc8\xff\x00\x00\xbe\xff\xc7\xff\xb9\xff\xb7\xff\xbb\xff\xb5\xff\xb4\xff\xc4\xff\xb0\xff\xae\xff\xbf\xff\xac\xff\xaa\xff\xbd\xff\xb6\xff\xad\xff\xa9\xff\xb3\xff\x00\x00\xd3\xff\xd2\xff\xcb\xff\xb2\xff\x8a\xff\x89\xff\xa8\xff\x87\xff\x86\xff\x88\xff\xf4\xff\xdb\xff\xd9\xff\xd5\xff\xd7\xff\x00\x00\x00\x00\x00\x00\xa0\xff\x9d\xff\xd6\xff\x00\x00\x00\x00\xda\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc2\xff\x00\x00\xc1\xff\xc0\xff\xde\xff\x00\x00\x00\x00\xd1\xff\xd0\xff\xce\xff\xcd\xff\xcc\xff\xcf\xff\x00\x00\x00\x00\x00\x00\x00\x00\xea\xff\xe7\xff\xee\xff\x00\x00\xe0\xff\xd4\xff\xbc\xff\xb1\xff\xba\xff\xc3\xff\xa7\xff\x00\x00\x00\x00\x00\x00\xe2\xff\x97\xff\xa3\xff\xa5\xff\x9c\xff\x94\xff\x9a\xff\x99\xff\x96\xff\x00\x00\x95\xff\x00\x00\x00\x00\xd9\xff\xdc\xff\xd8\xff\xf6\xff\x00\x00\x90\xff\x00\x00\x92\xff\x00\x00\x00\x00\xf5\xff\x00\x00\xab\xff\xaf\xff\xb8\xff\x00\x00\x00\x00\x00\x00\xe8\xff\x00\x00\xeb\xff\x00\x00\xf7\xff\xea\xff\xe7\xff\x00\x00\xdf\xff\xa6\xff\xa4\xff\xa2\xff\x9b\xff\x00\x00\x91\xff\x00\x00\x00\x00\x93\xff\x8f\xff\x98\xff\xe1\xff\xe6\xff\xe9\xff"#++happyCheck :: HappyAddr+happyCheck = HappyA# "\xff\xff\x06\x00\x06\x00\x00\x00\x01\x00\x02\x00\x03\x00\x04\x00\x0e\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x0b\x00\x35\x00\x0d\x00\x36\x00\x0f\x00\x10\x00\x0c\x00\x12\x00\x11\x00\x11\x00\x3d\x00\x0e\x00\x17\x00\x18\x00\x15\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x11\x00\x12\x00\x0c\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x15\x00\x32\x00\x32\x00\x3f\x00\x40\x00\x37\x00\x20\x00\x21\x00\x22\x00\x45\x00\x05\x00\x45\x00\x45\x00\x40\x00\x41\x00\x42\x00\x43\x00\x19\x00\x45\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x0b\x00\x05\x00\x0d\x00\x38\x00\x0f\x00\x10\x00\x44\x00\x12\x00\x02\x00\x18\x00\x19\x00\x1a\x00\x17\x00\x18\x00\x02\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x24\x00\x20\x00\x21\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x3f\x00\x40\x00\x11\x00\x12\x00\x11\x00\x12\x00\x45\x00\x15\x00\x00\x00\x01\x00\x02\x00\x03\x00\x04\x00\x40\x00\x41\x00\x42\x00\x43\x00\x16\x00\x45\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x0b\x00\x1f\x00\x0d\x00\x0a\x00\x0f\x00\x10\x00\x03\x00\x12\x00\x11\x00\x12\x00\x04\x00\x06\x00\x17\x00\x18\x00\x05\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x16\x00\x01\x00\x01\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x37\x00\x18\x00\x19\x00\x1a\x00\x0a\x00\x39\x00\x05\x00\x02\x00\x02\x00\x20\x00\x02\x00\x3f\x00\x40\x00\x40\x00\x41\x00\x42\x00\x43\x00\x45\x00\x45\x00\x0f\x00\x10\x00\x05\x00\x12\x00\x05\x00\x04\x00\x16\x00\x02\x00\x17\x00\x18\x00\x06\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x02\x00\x02\x00\x15\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x17\x00\x18\x00\x19\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x20\x00\x21\x00\x22\x00\x23\x00\x40\x00\x41\x00\x42\x00\x43\x00\x39\x00\x45\x00\x0f\x00\x10\x00\x1f\x00\x12\x00\x3f\x00\x40\x00\x02\x00\x11\x00\x17\x00\x18\x00\x45\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x16\x00\x05\x00\x01\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x18\x00\x19\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x20\x00\x21\x00\x22\x00\x23\x00\x01\x00\x40\x00\x41\x00\x42\x00\x43\x00\x01\x00\x45\x00\x0f\x00\x10\x00\x03\x00\x12\x00\x06\x00\x05\x00\x05\x00\x04\x00\x17\x00\x18\x00\x05\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x05\x00\x03\x00\x02\x00\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x0b\x00\x0c\x00\x0d\x00\x0e\x00\x0f\x00\x10\x00\x05\x00\x05\x00\x05\x00\x1b\x00\x15\x00\x16\x00\x01\x00\x40\x00\x41\x00\x42\x00\x43\x00\x01\x00\x45\x00\x0f\x00\x10\x00\x01\x00\x12\x00\x25\x00\xff\xff\xff\xff\xff\xff\x17\x00\x18\x00\xff\xff\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\xff\xff\xff\xff\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x18\x00\x19\x00\x1a\x00\x1b\x00\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\xff\xff\x22\x00\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x0f\x00\x10\x00\xff\xff\x12\x00\xff\xff\xff\xff\xff\xff\xff\xff\x17\x00\x18\x00\xff\xff\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\xff\xff\xff\xff\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x0f\x00\x10\x00\xff\xff\x12\x00\xff\xff\xff\xff\xff\xff\xff\xff\x17\x00\x18\x00\xff\xff\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\xff\xff\xff\xff\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x0f\x00\x10\x00\xff\xff\x12\x00\xff\xff\xff\xff\xff\xff\xff\xff\x17\x00\x18\x00\xff\xff\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\xff\xff\xff\xff\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x13\x00\x14\x00\xff\xff\x16\x00\x17\x00\xff\xff\xff\xff\xff\xff\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\xff\xff\xff\xff\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\x14\x00\x45\x00\x16\x00\x17\x00\xff\xff\xff\xff\xff\xff\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\xff\xff\xff\xff\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x16\x00\x17\x00\xff\xff\xff\xff\xff\xff\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\xff\xff\xff\xff\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\xff\xff\xff\xff\x23\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\xff\xff\x01\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\x01\x00\x45\x00\x13\x00\x14\x00\xff\xff\xff\xff\x17\x00\x18\x00\x19\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x20\x00\x21\x00\x22\x00\x23\x00\xff\xff\xff\xff\xff\xff\x17\x00\x18\x00\x19\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x20\x00\x21\x00\x22\x00\x23\x00\xff\xff\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x33\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\x24\x00\x25\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x2f\x00\x30\x00\x31\x00\x32\x00\x03\x00\x04\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x03\x00\x40\x00\x41\x00\x42\x00\x43\x00\xff\xff\x45\x00\xff\xff\xff\xff\x18\x00\x19\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\xff\xff\x1f\x00\x20\x00\x21\x00\x22\x00\x23\x00\x18\x00\x19\x00\x1a\x00\x1b\x00\x1c\x00\x1d\x00\x32\x00\x1f\x00\x20\x00\x21\x00\x22\x00\x23\x00\xff\xff\xff\xff\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x32\x00\x40\x00\xff\xff\xff\xff\x43\x00\xff\xff\x45\x00\xff\xff\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x32\x00\x40\x00\xff\xff\xff\xff\x43\x00\xff\xff\x45\x00\xff\xff\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x32\x00\x40\x00\x34\x00\xff\xff\x43\x00\xff\xff\x45\x00\xff\xff\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x32\x00\xff\xff\x40\x00\xff\xff\xff\xff\x43\x00\xff\xff\x45\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\xff\xff\xff\xff\x40\x00\xff\xff\xff\xff\x43\x00\xff\xff\x45\x00\xff\xff"#++happyTable :: HappyAddr+happyTable = HappyA# "\x00\x00\x20\x00\x22\x00\x0f\x00\x03\x00\x04\x00\x05\x00\x06\x00\xc3\x00\xbe\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\xa6\x00\x2f\x00\xb8\x00\x30\x00\x31\x00\xc4\x00\x32\x00\xb6\x00\x84\x00\xb9\x00\xae\x00\x33\x00\x34\x00\x9e\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\xba\xff\xba\xff\xb0\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x67\x00\x85\x00\x85\x00\x10\x00\x11\x00\x07\x00\x6f\x00\x70\x00\x71\x00\x12\x00\x69\x00\x21\x00\x21\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x76\x00\x12\x00\x6b\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x7f\x00\x2f\x00\x1c\x00\x30\x00\x31\x00\x1a\x00\x32\x00\xc0\x00\x09\x00\x0a\x00\x0b\x00\x33\x00\x34\x00\xc2\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x0c\x00\x6f\x00\x70\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x19\x00\x11\x00\xb1\xff\xb1\xff\xbc\xff\xbc\xff\x12\x00\xb0\x00\x02\x00\x03\x00\x04\x00\x05\x00\x06\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\xb2\x00\x12\x00\x2a\x00\x2b\x00\x2c\x00\x2d\x00\x2e\x00\x57\x00\x2f\x00\xb6\x00\x30\x00\x31\x00\x99\x00\x32\x00\x73\x00\x74\x00\xbd\x00\xa0\x00\x33\x00\x34\x00\xbe\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x69\x00\xa1\x00\xa5\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x07\x00\x14\x00\x15\x00\x16\x00\xa6\x00\x63\x00\xa8\x00\xa9\x00\xaa\x00\x18\x00\xab\x00\x27\x00\x11\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x12\x00\x12\x00\xc2\x00\x31\x00\xac\x00\x32\x00\xad\x00\xae\x00\xb2\x00\x81\x00\x33\x00\x34\x00\xb3\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x90\x00\x9c\x00\xb0\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x61\x00\x14\x00\x15\x00\x16\x00\x17\x00\x54\x00\x55\x00\x56\x00\x57\x00\x18\x00\x58\x00\x59\x00\x5a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x26\x00\x12\x00\xb3\x00\x31\x00\x57\x00\x32\x00\x27\x00\x11\x00\x9e\x00\x73\x00\x33\x00\x34\x00\x12\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x69\x00\x6b\x00\x6d\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x14\x00\x15\x00\x16\x00\x17\x00\x54\x00\x55\x00\x56\x00\x57\x00\x18\x00\x58\x00\x59\x00\x5a\x00\x6e\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x6f\x00\x12\x00\xb4\x00\x31\x00\x76\x00\x32\x00\x26\x00\x6b\x00\x62\x00\x63\x00\x33\x00\x34\x00\x29\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x2a\x00\x24\x00\x25\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x78\x00\x79\x00\x7a\x00\x7b\x00\x7c\x00\x7d\x00\x1e\x00\x1f\x00\x20\x00\x1c\x00\x7e\x00\x7f\x00\x0d\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x0e\x00\x12\x00\x81\x00\x31\x00\x0f\x00\x32\x00\xff\xff\x00\x00\x00\x00\x00\x00\x33\x00\x34\x00\x00\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x00\x00\x00\x00\x00\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x14\x00\x15\x00\x16\x00\x17\x00\x00\x00\x00\x00\x00\x00\x00\x00\x18\x00\x00\x00\x19\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x82\x00\x31\x00\x00\x00\x32\x00\x00\x00\x00\x00\x00\x00\x00\x00\x33\x00\x34\x00\x00\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x00\x00\x00\x00\x00\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x83\x00\x31\x00\x00\x00\x32\x00\x00\x00\x00\x00\x00\x00\x00\x00\x33\x00\x34\x00\x00\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x00\x00\x00\x00\x00\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x74\x00\x31\x00\x00\x00\x32\x00\x00\x00\x00\x00\x00\x00\x00\x00\x33\x00\x34\x00\x00\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x00\x00\x00\x00\x00\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x5a\x00\x5b\x00\x00\x00\x5c\x00\x5d\x00\x00\x00\x00\x00\x00\x00\x5e\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x00\x00\x00\x00\x00\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x66\x00\x12\x00\x5c\x00\x5d\x00\x00\x00\x00\x00\x00\x00\x5e\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x00\x00\x00\x00\x00\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x9c\x00\x5d\x00\x00\x00\x00\x00\x00\x00\x5e\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x00\x00\x00\x00\x00\x00\x3b\x00\x3c\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x64\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x00\x00\x00\x00\x00\x00\x3b\x00\x65\x00\x3d\x00\x3e\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x00\x00\x50\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x60\x00\x12\x00\x51\x00\x52\x00\x00\x00\x00\x00\x53\x00\x14\x00\x15\x00\x16\x00\x17\x00\x54\x00\x55\x00\x56\x00\x57\x00\x18\x00\x58\x00\x59\x00\x5a\x00\x00\x00\x00\x00\x00\x00\x61\x00\x14\x00\x15\x00\x16\x00\x17\x00\x54\x00\x55\x00\x56\x00\x57\x00\x18\x00\x58\x00\x59\x00\x5a\x00\x00\x00\x8b\x00\x3d\x00\x87\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x88\x00\x45\x00\x46\x00\x89\x00\x48\x00\x49\x00\x4a\x00\xb7\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x8b\x00\x3d\x00\x87\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x88\x00\x45\x00\x46\x00\x89\x00\x48\x00\x49\x00\x4a\x00\x8c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x8b\x00\x3d\x00\x87\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x88\x00\x45\x00\x46\x00\x89\x00\x48\x00\x49\x00\x4a\x00\x8d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x8b\x00\x3d\x00\x87\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x88\x00\x45\x00\x46\x00\x89\x00\x48\x00\x49\x00\x4a\x00\x8e\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x86\x00\x3d\x00\x87\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x88\x00\x45\x00\x46\x00\x89\x00\x48\x00\x49\x00\x4a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x8a\x00\x3d\x00\x87\x00\x3f\x00\x40\x00\x41\x00\x42\x00\x43\x00\x88\x00\x45\x00\x46\x00\x89\x00\x48\x00\x49\x00\x4a\x00\x99\x00\xa4\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x99\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x00\x00\x12\x00\x00\x00\x00\x00\x14\x00\x15\x00\x16\x00\x17\x00\x9a\x00\x9b\x00\x00\x00\x57\x00\x18\x00\x58\x00\x59\x00\x5a\x00\x14\x00\x15\x00\x16\x00\x17\x00\x9a\x00\x9b\x00\x90\x00\x57\x00\x18\x00\x58\x00\x59\x00\x5a\x00\x00\x00\x00\x00\xa1\x00\x93\x00\x94\x00\x95\x00\xc0\x00\x90\x00\x96\x00\x00\x00\x00\x00\x97\x00\x00\x00\x12\x00\x00\x00\xa1\x00\x93\x00\x94\x00\x95\x00\xbb\x00\x90\x00\x96\x00\x00\x00\x00\x00\x97\x00\x00\x00\x12\x00\x00\x00\xa1\x00\x93\x00\x94\x00\x95\x00\xa2\x00\x90\x00\x96\x00\x91\x00\x00\x00\x97\x00\x00\x00\x12\x00\x00\x00\x92\x00\x93\x00\x94\x00\x95\x00\x90\x00\x00\x00\x96\x00\x00\x00\x00\x00\x97\x00\x00\x00\x12\x00\xba\x00\x93\x00\x94\x00\x95\x00\x00\x00\x00\x00\x96\x00\x00\x00\x00\x00\x97\x00\x00\x00\x12\x00\x00\x00"#++happyReduceArr = Happy_Data_Array.array (1, 126) [+ (1 , happyReduce_1),+ (2 , happyReduce_2),+ (3 , happyReduce_3),+ (4 , happyReduce_4),+ (5 , happyReduce_5),+ (6 , happyReduce_6),+ (7 , happyReduce_7),+ (8 , happyReduce_8),+ (9 , happyReduce_9),+ (10 , happyReduce_10),+ (11 , happyReduce_11),+ (12 , happyReduce_12),+ (13 , happyReduce_13),+ (14 , happyReduce_14),+ (15 , happyReduce_15),+ (16 , happyReduce_16),+ (17 , happyReduce_17),+ (18 , happyReduce_18),+ (19 , happyReduce_19),+ (20 , happyReduce_20),+ (21 , happyReduce_21),+ (22 , happyReduce_22),+ (23 , happyReduce_23),+ (24 , happyReduce_24),+ (25 , happyReduce_25),+ (26 , happyReduce_26),+ (27 , happyReduce_27),+ (28 , happyReduce_28),+ (29 , happyReduce_29),+ (30 , happyReduce_30),+ (31 , happyReduce_31),+ (32 , happyReduce_32),+ (33 , happyReduce_33),+ (34 , happyReduce_34),+ (35 , happyReduce_35),+ (36 , happyReduce_36),+ (37 , happyReduce_37),+ (38 , happyReduce_38),+ (39 , happyReduce_39),+ (40 , happyReduce_40),+ (41 , happyReduce_41),+ (42 , happyReduce_42),+ (43 , happyReduce_43),+ (44 , happyReduce_44),+ (45 , happyReduce_45),+ (46 , happyReduce_46),+ (47 , happyReduce_47),+ (48 , happyReduce_48),+ (49 , happyReduce_49),+ (50 , happyReduce_50),+ (51 , happyReduce_51),+ (52 , happyReduce_52),+ (53 , happyReduce_53),+ (54 , happyReduce_54),+ (55 , happyReduce_55),+ (56 , happyReduce_56),+ (57 , happyReduce_57),+ (58 , happyReduce_58),+ (59 , happyReduce_59),+ (60 , happyReduce_60),+ (61 , happyReduce_61),+ (62 , happyReduce_62),+ (63 , happyReduce_63),+ (64 , happyReduce_64),+ (65 , happyReduce_65),+ (66 , happyReduce_66),+ (67 , happyReduce_67),+ (68 , happyReduce_68),+ (69 , happyReduce_69),+ (70 , happyReduce_70),+ (71 , happyReduce_71),+ (72 , happyReduce_72),+ (73 , happyReduce_73),+ (74 , happyReduce_74),+ (75 , happyReduce_75),+ (76 , happyReduce_76),+ (77 , happyReduce_77),+ (78 , happyReduce_78),+ (79 , happyReduce_79),+ (80 , happyReduce_80),+ (81 , happyReduce_81),+ (82 , happyReduce_82),+ (83 , happyReduce_83),+ (84 , happyReduce_84),+ (85 , happyReduce_85),+ (86 , happyReduce_86),+ (87 , happyReduce_87),+ (88 , happyReduce_88),+ (89 , happyReduce_89),+ (90 , happyReduce_90),+ (91 , happyReduce_91),+ (92 , happyReduce_92),+ (93 , happyReduce_93),+ (94 , happyReduce_94),+ (95 , happyReduce_95),+ (96 , happyReduce_96),+ (97 , happyReduce_97),+ (98 , happyReduce_98),+ (99 , happyReduce_99),+ (100 , happyReduce_100),+ (101 , happyReduce_101),+ (102 , happyReduce_102),+ (103 , happyReduce_103),+ (104 , happyReduce_104),+ (105 , happyReduce_105),+ (106 , happyReduce_106),+ (107 , happyReduce_107),+ (108 , happyReduce_108),+ (109 , happyReduce_109),+ (110 , happyReduce_110),+ (111 , happyReduce_111),+ (112 , happyReduce_112),+ (113 , happyReduce_113),+ (114 , happyReduce_114),+ (115 , happyReduce_115),+ (116 , happyReduce_116),+ (117 , happyReduce_117),+ (118 , happyReduce_118),+ (119 , happyReduce_119),+ (120 , happyReduce_120),+ (121 , happyReduce_121),+ (122 , happyReduce_122),+ (123 , happyReduce_123),+ (124 , happyReduce_124),+ (125 , happyReduce_125),+ (126 , happyReduce_126)+ ]++happy_n_terms = 38 :: Int+happy_n_nonterms = 70 :: Int++happyReduce_1 = happySpecReduce_0 0# happyReduction_1+happyReduction_1 = happyIn4+ ([]+ )++happyReduce_2 = happySpecReduce_2 0# happyReduction_2+happyReduction_2 happy_x_2+ happy_x_1+ = case happyOut5 happy_x_1 of { happy_var_1 -> + case happyOut4 happy_x_2 of { happy_var_2 -> + happyIn4+ (happy_var_1 : happy_var_2+ )}}++happyReduce_3 = happySpecReduce_1 1# happyReduction_3+happyReduction_3 happy_x_1+ = case happyOut6 happy_x_1 of { happy_var_1 -> + happyIn5+ (happy_var_1+ )}++happyReduce_4 = happySpecReduce_1 1# happyReduction_4+happyReduction_4 happy_x_1+ = case happyOut59 happy_x_1 of { happy_var_1 -> + happyIn5+ (happy_var_1+ )}++happyReduce_5 = happySpecReduce_1 1# happyReduction_5+happyReduction_5 happy_x_1+ = case happyOutTok happy_x_1 of { (CommentToken happy_var_1) -> + happyIn5+ (Comment happy_var_1+ )}++happyReduce_6 = happySpecReduce_1 2# happyReduction_6+happyReduction_6 happy_x_1+ = case happyOut7 happy_x_1 of { happy_var_1 -> + happyIn6+ (happy_var_1+ )}++happyReduce_7 = happySpecReduce_1 2# happyReduction_7+happyReduction_7 happy_x_1+ = case happyOut8 happy_x_1 of { happy_var_1 -> + happyIn6+ (happy_var_1+ )}++happyReduce_8 = happyReduce 10# 3# happyReduction_8+happyReduction_8 (happy_x_10 `HappyStk`+ happy_x_9 `HappyStk`+ happy_x_8 `HappyStk`+ happy_x_7 `HappyStk`+ happy_x_6 `HappyStk`+ happy_x_5 `HappyStk`+ happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut67 happy_x_3 of { happy_var_3 -> + case happyOut10 happy_x_5 of { happy_var_5 -> + 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)+ ) `HappyStk` happyRest}}}}++happyReduce_9 = happyReduce 10# 4# happyReduction_9+happyReduction_9 (happy_x_10 `HappyStk`+ happy_x_9 `HappyStk`+ happy_x_8 `HappyStk`+ happy_x_7 `HappyStk`+ happy_x_6 `HappyStk`+ happy_x_5 `HappyStk`+ happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut67 happy_x_3 of { happy_var_3 -> + case happyOut10 happy_x_5 of { happy_var_5 -> + 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)+ ) `HappyStk` happyRest}}}}++happyReduce_10 = happySpecReduce_3 5# happyReduction_10+happyReduction_10 happy_x_3+ happy_x_2+ happy_x_1+ = 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)+ )}}++happyReduce_11 = happySpecReduce_0 5# happyReduction_11+happyReduction_11 = happyIn9+ ((NoSourceInfo, NoUsefulInfo)+ )++happyReduce_12 = happySpecReduce_1 6# happyReduction_12+happyReduction_12 happy_x_1+ = case happyOut73 happy_x_1 of { happy_var_1 -> + happyIn10+ (Role happy_var_1+ )}++happyReduce_13 = happySpecReduce_1 7# happyReduction_13+happyReduction_13 happy_x_1+ = case happyOut12 happy_x_1 of { happy_var_1 -> + happyIn11+ (happy_var_1+ )}++happyReduce_14 = happySpecReduce_1 7# happyReduction_14+happyReduction_14 happy_x_1+ = case happyOut19 happy_x_1 of { happy_var_1 -> + happyIn11+ (happy_var_1+ )}++happyReduce_15 = happySpecReduce_1 8# happyReduction_15+happyReduction_15 happy_x_1+ = case happyOut13 happy_x_1 of { happy_var_1 -> + happyIn12+ (happy_var_1+ )}++happyReduce_16 = happySpecReduce_1 8# happyReduction_16+happyReduction_16 happy_x_1+ = case happyOut14 happy_x_1 of { happy_var_1 -> + happyIn12+ (happy_var_1+ )}++happyReduce_17 = happySpecReduce_3 9# happyReduction_17+happyReduction_17 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut19 happy_x_1 of { happy_var_1 -> + case happyOut29 happy_x_2 of { happy_var_2 -> + case happyOut19 happy_x_3 of { happy_var_3 -> + happyIn13+ (happy_var_2 happy_var_1 happy_var_3+ )}}}++happyReduce_18 = happySpecReduce_1 10# happyReduction_18+happyReduction_18 happy_x_1+ = case happyOut15 happy_x_1 of { happy_var_1 -> + happyIn14+ (happy_var_1+ )}++happyReduce_19 = happySpecReduce_1 10# happyReduction_19+happyReduction_19 happy_x_1+ = case happyOut17 happy_x_1 of { happy_var_1 -> + happyIn14+ (happy_var_1+ )}++happyReduce_20 = happyReduce 4# 11# happyReduction_20+happyReduction_20 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut19 happy_x_1 of { happy_var_1 -> + case happyOut19 happy_x_3 of { happy_var_3 -> + case happyOut16 happy_x_4 of { happy_var_4 -> + happyIn15+ (foldl (.|.) (happy_var_1 .|. happy_var_3) happy_var_4+ ) `HappyStk` happyRest}}}++happyReduce_21 = happySpecReduce_0 12# happyReduction_21+happyReduction_21 = happyIn16+ ([]+ )++happyReduce_22 = happySpecReduce_3 12# happyReduction_22+happyReduction_22 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut19 happy_x_2 of { happy_var_2 -> + case happyOut16 happy_x_3 of { happy_var_3 -> + happyIn16+ (happy_var_2 : happy_var_3+ )}}++happyReduce_23 = happyReduce 4# 13# happyReduction_23+happyReduction_23 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut19 happy_x_1 of { happy_var_1 -> + case happyOut19 happy_x_3 of { happy_var_3 -> + case happyOut18 happy_x_4 of { happy_var_4 -> + happyIn17+ (foldl (.&.) (happy_var_1 .&. happy_var_3) happy_var_4+ ) `HappyStk` happyRest}}}++happyReduce_24 = happySpecReduce_0 14# happyReduction_24+happyReduction_24 = happyIn18+ ([]+ )++happyReduce_25 = happySpecReduce_3 14# happyReduction_25+happyReduction_25 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut19 happy_x_2 of { happy_var_2 -> + case happyOut18 happy_x_3 of { happy_var_3 -> + happyIn18+ (happy_var_2 : happy_var_3+ )}}++happyReduce_26 = happySpecReduce_1 15# happyReduction_26+happyReduction_26 happy_x_1+ = case happyOut20 happy_x_1 of { happy_var_1 -> + happyIn19+ (happy_var_1+ )}++happyReduce_27 = happySpecReduce_1 15# happyReduction_27+happyReduction_27 happy_x_1+ = case happyOut22 happy_x_1 of { happy_var_1 -> + happyIn19+ (happy_var_1+ )}++happyReduce_28 = happySpecReduce_1 15# happyReduction_28+happyReduction_28 happy_x_1+ = case happyOut31 happy_x_1 of { happy_var_1 -> + happyIn19+ (happy_var_1+ )}++happyReduce_29 = happySpecReduce_3 15# happyReduction_29+happyReduction_29 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut11 happy_x_2 of { happy_var_2 -> + happyIn19+ (happy_var_2+ )}++happyReduce_30 = happyReduce 6# 16# happyReduction_30+happyReduction_30 (happy_x_6 `HappyStk`+ happy_x_5 `HappyStk`+ happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut28 happy_x_1 of { happy_var_1 -> + case happyOut21 happy_x_3 of { happy_var_3 -> + case happyOut19 happy_x_6 of { happy_var_6 -> + happyIn20+ (happy_var_1 happy_var_3 happy_var_6+ ) `HappyStk` happyRest}}}++happyReduce_31 = happySpecReduce_1 17# happyReduction_31+happyReduction_31 happy_x_1+ = case happyOut54 happy_x_1 of { happy_var_1 -> + happyIn21+ ([happy_var_1]+ )}++happyReduce_32 = happySpecReduce_3 17# happyReduction_32+happyReduction_32 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut54 happy_x_1 of { happy_var_1 -> + case happyOut21 happy_x_3 of { happy_var_3 -> + happyIn21+ (happy_var_1 : happy_var_3+ )}}++happyReduce_33 = happySpecReduce_2 18# happyReduction_33+happyReduction_33 happy_x_2+ happy_x_1+ = case happyOut30 happy_x_1 of { happy_var_1 -> + case happyOut19 happy_x_2 of { happy_var_2 -> + happyIn22+ (happy_var_1 happy_var_2+ )}}++happyReduce_34 = happySpecReduce_1 18# happyReduction_34+happyReduction_34 happy_x_1+ = case happyOut27 happy_x_1 of { happy_var_1 -> + happyIn22+ (happy_var_1+ )}++happyReduce_35 = happySpecReduce_3 19# happyReduction_35+happyReduction_35 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut24 happy_x_2 of { happy_var_2 -> + happyIn23+ (happy_var_2+ )}++happyReduce_36 = happySpecReduce_1 19# happyReduction_36+happyReduction_36 happy_x_1+ = case happyOut24 happy_x_1 of { happy_var_1 -> + happyIn23+ (happy_var_1+ )}++happyReduce_37 = happySpecReduce_2 20# happyReduction_37+happyReduction_37 happy_x_2+ happy_x_1+ = case happyOut26 happy_x_1 of { happy_var_1 -> + case happyOut25 happy_x_2 of { happy_var_2 -> + happyIn24+ (foldl (.|.) happy_var_1 happy_var_2+ )}}++happyReduce_38 = happySpecReduce_0 21# happyReduction_38+happyReduction_38 = happyIn25+ ([]+ )++happyReduce_39 = happySpecReduce_3 21# happyReduction_39+happyReduction_39 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut26 happy_x_2 of { happy_var_2 -> + case happyOut25 happy_x_3 of { happy_var_3 -> + happyIn25+ (happy_var_2 : happy_var_3+ )}}++happyReduce_40 = happySpecReduce_1 22# happyReduction_40+happyReduction_40 happy_x_1+ = case happyOut31 happy_x_1 of { happy_var_1 -> + happyIn26+ (happy_var_1+ )}++happyReduce_41 = happySpecReduce_2 22# happyReduction_41+happyReduction_41 happy_x_2+ happy_x_1+ = case happyOut31 happy_x_2 of { happy_var_2 -> + happyIn26+ ((.~.) happy_var_2+ )}++happyReduce_42 = happySpecReduce_1 22# happyReduction_42+happyReduction_42 happy_x_1+ = case happyOut27 happy_x_1 of { happy_var_1 -> + happyIn26+ (happy_var_1+ )}++happyReduce_43 = happySpecReduce_3 23# happyReduction_43+happyReduction_43 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut40 happy_x_1 of { happy_var_1 -> + case happyOut38 happy_x_2 of { happy_var_2 -> + case happyOut40 happy_x_3 of { happy_var_3 -> + happyIn27+ (happy_var_2 happy_var_1 happy_var_3+ )}}}++happyReduce_44 = happySpecReduce_1 24# happyReduction_44+happyReduction_44 happy_x_1+ = happyIn28+ (for_all+ )++happyReduce_45 = happySpecReduce_1 24# happyReduction_45+happyReduction_45 happy_x_1+ = happyIn28+ (exists+ )++happyReduce_46 = happySpecReduce_1 25# happyReduction_46+happyReduction_46 happy_x_1+ = happyIn29+ ((.<=>.)+ )++happyReduce_47 = happySpecReduce_1 25# happyReduction_47+happyReduction_47 happy_x_1+ = happyIn29+ ((.=>.)+ )++happyReduce_48 = happySpecReduce_1 25# happyReduction_48+happyReduction_48 happy_x_1+ = happyIn29+ ((.<=.)+ )++happyReduce_49 = happySpecReduce_1 25# happyReduction_49+happyReduction_49 happy_x_1+ = happyIn29+ ((.<~>.)+ )++happyReduce_50 = happySpecReduce_1 25# happyReduction_50+happyReduction_50 happy_x_1+ = happyIn29+ ((.~|.)+ )++happyReduce_51 = happySpecReduce_1 25# happyReduction_51+happyReduction_51 happy_x_1+ = happyIn29+ ((.~&.)+ )++happyReduce_52 = happySpecReduce_1 26# happyReduction_52+happyReduction_52 happy_x_1+ = happyIn30+ ((.~.)+ )++happyReduce_53 = happySpecReduce_1 27# happyReduction_53+happyReduction_53 happy_x_1+ = case happyOut32 happy_x_1 of { happy_var_1 -> + happyIn31+ (happy_var_1+ )}++happyReduce_54 = happySpecReduce_1 27# happyReduction_54+happyReduction_54 happy_x_1+ = case happyOut33 happy_x_1 of { happy_var_1 -> + happyIn31+ (happy_var_1+ )}++happyReduce_55 = happySpecReduce_1 27# happyReduction_55+happyReduction_55 happy_x_1+ = case happyOut39 happy_x_1 of { happy_var_1 -> + happyIn31+ (happy_var_1+ )}++happyReduce_56 = happySpecReduce_1 28# happyReduction_56+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+ )}++happyReduce_57 = happySpecReduce_1 29# happyReduction_57+happyReduction_57 happy_x_1+ = case happyOut34 happy_x_1 of { happy_var_1 -> + happyIn33+ (happy_var_1+ )}++happyReduce_58 = happySpecReduce_1 29# happyReduction_58+happyReduction_58 happy_x_1+ = case happyOut35 happy_x_1 of { happy_var_1 -> + happyIn33+ (happy_var_1+ )}++happyReduce_59 = happySpecReduce_1 30# happyReduction_59+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+ )}++happyReduce_60 = happySpecReduce_3 31# happyReduction_60+happyReduction_60 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut40 happy_x_1 of { happy_var_1 -> + case happyOut36 happy_x_2 of { happy_var_2 -> + case happyOut40 happy_x_3 of { happy_var_3 -> + happyIn35+ (happy_var_2 happy_var_1 happy_var_3+ )}}}++happyReduce_61 = happySpecReduce_1 32# happyReduction_61+happyReduction_61 happy_x_1+ = case happyOut37 happy_x_1 of { happy_var_1 -> + happyIn36+ (happy_var_1+ )}++happyReduce_62 = happySpecReduce_1 33# happyReduction_62+happyReduction_62 happy_x_1+ = happyIn37+ ((.=.)+ )++happyReduce_63 = happySpecReduce_1 34# happyReduction_63+happyReduction_63 happy_x_1+ = happyIn38+ ((.!=.)+ )++happyReduce_64 = happySpecReduce_1 35# happyReduction_64+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+ )}++happyReduce_65 = happySpecReduce_1 36# happyReduction_65+happyReduction_65 happy_x_1+ = case happyOut41 happy_x_1 of { happy_var_1 -> + happyIn40+ (happy_var_1+ )}++happyReduce_66 = happySpecReduce_1 36# happyReduction_66+happyReduction_66 happy_x_1+ = case happyOut54 happy_x_1 of { happy_var_1 -> + happyIn40+ (var happy_var_1+ )}++happyReduce_67 = happySpecReduce_1 37# happyReduction_67+happyReduction_67 happy_x_1+ = case happyOut42 happy_x_1 of { happy_var_1 -> + happyIn41+ (happy_var_1+ )}++happyReduce_68 = happySpecReduce_1 37# happyReduction_68+happyReduction_68 happy_x_1+ = case happyOut45 happy_x_1 of { happy_var_1 -> + happyIn41+ (happy_var_1+ )}++happyReduce_69 = happySpecReduce_1 37# happyReduction_69+happyReduction_69 happy_x_1+ = case happyOut51 happy_x_1 of { happy_var_1 -> + happyIn41+ (happy_var_1+ )}++happyReduce_70 = happySpecReduce_1 38# happyReduction_70+happyReduction_70 happy_x_1+ = case happyOut43 happy_x_1 of { happy_var_1 -> + happyIn42+ (fApp happy_var_1 []+ )}++happyReduce_71 = happyReduce 4# 38# happyReduction_71+happyReduction_71 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut44 happy_x_1 of { happy_var_1 -> + case happyOut55 happy_x_3 of { happy_var_3 -> + happyIn42+ (fApp happy_var_1 happy_var_3+ ) `HappyStk` happyRest}}++happyReduce_72 = happySpecReduce_1 39# happyReduction_72+happyReduction_72 happy_x_1+ = case happyOut44 happy_x_1 of { happy_var_1 -> + happyIn43+ (happy_var_1+ )}++happyReduce_73 = happySpecReduce_1 40# happyReduction_73+happyReduction_73 happy_x_1+ = case happyOut68 happy_x_1 of { happy_var_1 -> + happyIn44+ (happy_var_1+ )}++happyReduce_74 = happySpecReduce_1 41# happyReduction_74+happyReduction_74 happy_x_1+ = case happyOut46 happy_x_1 of { happy_var_1 -> + happyIn45+ (happy_var_1+ )}++happyReduce_75 = happySpecReduce_1 41# happyReduction_75+happyReduction_75 happy_x_1+ = case happyOut47 happy_x_1 of { happy_var_1 -> + happyIn45+ (happy_var_1+ )}++happyReduce_76 = happySpecReduce_1 42# happyReduction_76+happyReduction_76 happy_x_1+ = case happyOut71 happy_x_1 of { happy_var_1 -> + happyIn46+ (numberLitTerm happy_var_1+ )}++happyReduce_77 = happySpecReduce_1 42# happyReduction_77+happyReduction_77 happy_x_1+ = case happyOutTok happy_x_1 of { (DoubleQuoted happy_var_1) -> + happyIn46+ (distinctObjectTerm (stripQuotes '"' happy_var_1)+ )}++happyReduce_78 = happySpecReduce_1 43# happyReduction_78+happyReduction_78 happy_x_1+ = case happyOut48 happy_x_1 of { happy_var_1 -> + happyIn47+ (happy_var_1+ )}++happyReduce_79 = happySpecReduce_1 44# happyReduction_79+happyReduction_79 happy_x_1+ = case happyOut49 happy_x_1 of { happy_var_1 -> + happyIn48+ (fApp (AtomicWord happy_var_1) []+ )}++happyReduce_80 = happyReduce 4# 44# happyReduction_80+happyReduction_80 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut50 happy_x_1 of { happy_var_1 -> + case happyOut55 happy_x_3 of { happy_var_3 -> + happyIn48+ (fApp (AtomicWord happy_var_1) happy_var_3+ ) `HappyStk` happyRest}}++happyReduce_81 = happySpecReduce_1 45# happyReduction_81+happyReduction_81 happy_x_1+ = case happyOut50 happy_x_1 of { happy_var_1 -> + happyIn49+ (happy_var_1+ )}++happyReduce_82 = happySpecReduce_1 46# happyReduction_82+happyReduction_82 happy_x_1+ = case happyOut69 happy_x_1 of { happy_var_1 -> + happyIn50+ (happy_var_1+ )}++happyReduce_83 = happySpecReduce_1 47# happyReduction_83+happyReduction_83 happy_x_1+ = case happyOut52 happy_x_1 of { happy_var_1 -> + happyIn51+ (fApp (AtomicWord happy_var_1) []+ )}++happyReduce_84 = happyReduce 4# 47# happyReduction_84+happyReduction_84 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut53 happy_x_1 of { happy_var_1 -> + case happyOut55 happy_x_3 of { happy_var_3 -> + happyIn51+ (fApp (AtomicWord happy_var_1) happy_var_3+ ) `HappyStk` happyRest}}++happyReduce_85 = happySpecReduce_1 48# happyReduction_85+happyReduction_85 happy_x_1+ = case happyOut53 happy_x_1 of { happy_var_1 -> + happyIn52+ (happy_var_1+ )}++happyReduce_86 = happySpecReduce_1 49# happyReduction_86+happyReduction_86 happy_x_1+ = case happyOut70 happy_x_1 of { happy_var_1 -> + happyIn53+ (happy_var_1+ )}++happyReduce_87 = happySpecReduce_1 50# happyReduction_87+happyReduction_87 happy_x_1+ = case happyOutTok happy_x_1 of { (UpperWord happy_var_1) -> + happyIn54+ (happy_var_1+ )}++happyReduce_88 = happySpecReduce_1 51# happyReduction_88+happyReduction_88 happy_x_1+ = case happyOut40 happy_x_1 of { happy_var_1 -> + happyIn55+ ([happy_var_1]+ )}++happyReduce_89 = happySpecReduce_3 51# happyReduction_89+happyReduction_89 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut40 happy_x_1 of { happy_var_1 -> + case happyOut55 happy_x_3 of { happy_var_3 -> + happyIn55+ (happy_var_1 : happy_var_3+ )}}++happyReduce_90 = happySpecReduce_1 52# happyReduction_90+happyReduction_90 happy_x_1+ = case happyOut62 happy_x_1 of { happy_var_1 -> + happyIn56+ (SourceInfo happy_var_1+ )}++happyReduce_91 = happySpecReduce_2 53# happyReduction_91+happyReduction_91 happy_x_2+ happy_x_1+ = case happyOut58 happy_x_2 of { happy_var_2 -> + happyIn57+ (happy_var_2+ )}++happyReduce_92 = happySpecReduce_0 53# happyReduction_92+happyReduction_92 = happyIn57+ (NoUsefulInfo+ )++happyReduce_93 = happySpecReduce_1 54# happyReduction_93+happyReduction_93 happy_x_1+ = case happyOut65 happy_x_1 of { happy_var_1 -> + happyIn58+ (UsefulInfo happy_var_1+ )}++happyReduce_94 = happyReduce 6# 55# happyReduction_94+happyReduction_94 (happy_x_6 `HappyStk`+ happy_x_5 `HappyStk`+ happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut72 happy_x_3 of { happy_var_3 -> + case happyOut60 happy_x_4 of { happy_var_4 -> + happyIn59+ (Include happy_var_3 happy_var_4+ ) `HappyStk` happyRest}}++happyReduce_95 = happyReduce 4# 56# happyReduction_95+happyReduction_95 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut61 happy_x_3 of { happy_var_3 -> + happyIn60+ (happy_var_3+ ) `HappyStk` happyRest}++happyReduce_96 = happySpecReduce_0 56# happyReduction_96+happyReduction_96 = happyIn60+ ([]+ )++happyReduce_97 = happySpecReduce_1 57# happyReduction_97+happyReduction_97 happy_x_1+ = case happyOut67 happy_x_1 of { happy_var_1 -> + happyIn61+ ([happy_var_1]+ )}++happyReduce_98 = happySpecReduce_3 57# happyReduction_98+happyReduction_98 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut67 happy_x_1 of { happy_var_1 -> + case happyOut61 happy_x_3 of { happy_var_3 -> + happyIn61+ (happy_var_1 : happy_var_3+ )}}++happyReduce_99 = happySpecReduce_1 58# happyReduction_99+happyReduction_99 happy_x_1+ = case happyOut63 happy_x_1 of { happy_var_1 -> + happyIn62+ (GTerm happy_var_1+ )}++happyReduce_100 = happySpecReduce_3 58# happyReduction_100+happyReduction_100 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut63 happy_x_1 of { happy_var_1 -> + case happyOut62 happy_x_3 of { happy_var_3 -> + happyIn62+ (ColonSep happy_var_1 happy_var_3+ )}}++happyReduce_101 = happySpecReduce_1 58# happyReduction_101+happyReduction_101 happy_x_1+ = case happyOut65 happy_x_1 of { happy_var_1 -> + happyIn62+ (GList happy_var_1+ )}++happyReduce_102 = happySpecReduce_1 59# happyReduction_102+happyReduction_102 happy_x_1+ = case happyOut68 happy_x_1 of { happy_var_1 -> + happyIn63+ (GWord happy_var_1+ )}++happyReduce_103 = happyReduce 4# 59# happyReduction_103+happyReduction_103 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut68 happy_x_1 of { happy_var_1 -> + case happyOut66 happy_x_3 of { happy_var_3 -> + happyIn63+ (GApp happy_var_1 happy_var_3+ ) `HappyStk` happyRest}}++happyReduce_104 = happySpecReduce_1 59# happyReduction_104+happyReduction_104 happy_x_1+ = case happyOut54 happy_x_1 of { happy_var_1 -> + happyIn63+ (GVar happy_var_1+ )}++happyReduce_105 = happySpecReduce_1 59# happyReduction_105+happyReduction_105 happy_x_1+ = case happyOut71 happy_x_1 of { happy_var_1 -> + happyIn63+ (GNumber happy_var_1+ )}++happyReduce_106 = happySpecReduce_1 59# happyReduction_106+happyReduction_106 happy_x_1+ = case happyOutTok happy_x_1 of { (DoubleQuoted happy_var_1) -> + happyIn63+ (GDistinctObject (stripQuotes '"' happy_var_1)+ )}++happyReduce_107 = happySpecReduce_1 59# happyReduction_107+happyReduction_107 happy_x_1+ = case happyOut64 happy_x_1 of { happy_var_1 -> + happyIn63+ (happy_var_1+ )}++happyReduce_108 = happyReduce 4# 60# happyReduction_108+happyReduction_108 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOutTok happy_x_1 of { (DollarWord happy_var_1) -> + case happyOut11 happy_x_3 of { happy_var_3 -> + happyIn64+ (GFormulaData happy_var_1 happy_var_3+ ) `HappyStk` happyRest}}++happyReduce_109 = happySpecReduce_2 61# happyReduction_109+happyReduction_109 happy_x_2+ happy_x_1+ = happyIn65+ ([]+ )++happyReduce_110 = happySpecReduce_3 61# happyReduction_110+happyReduction_110 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut66 happy_x_2 of { happy_var_2 -> + happyIn65+ (happy_var_2+ )}++happyReduce_111 = happySpecReduce_1 62# happyReduction_111+happyReduction_111 happy_x_1+ = case happyOut62 happy_x_1 of { happy_var_1 -> + happyIn66+ ([happy_var_1]+ )}++happyReduce_112 = happySpecReduce_3 62# happyReduction_112+happyReduction_112 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut62 happy_x_1 of { happy_var_1 -> + case happyOut66 happy_x_3 of { happy_var_3 -> + happyIn66+ (happy_var_1 : happy_var_3+ )}}++happyReduce_113 = happySpecReduce_1 63# happyReduction_113+happyReduction_113 happy_x_1+ = case happyOut68 happy_x_1 of { happy_var_1 -> + happyIn67+ (happy_var_1+ )}++happyReduce_114 = happySpecReduce_1 63# happyReduction_114+happyReduction_114 happy_x_1+ = case happyOutTok happy_x_1 of { (UnsignedInt happy_var_1) -> + happyIn67+ (AtomicWord(show happy_var_1)+ )}++happyReduce_115 = happySpecReduce_1 64# happyReduction_115+happyReduction_115 happy_x_1+ = case happyOut73 happy_x_1 of { happy_var_1 -> + happyIn68+ (AtomicWord happy_var_1+ )}++happyReduce_116 = happySpecReduce_1 64# happyReduction_116+happyReduction_116 happy_x_1+ = case happyOutTok happy_x_1 of { (SingleQuoted happy_var_1) -> + happyIn68+ (AtomicWord (stripQuotes '\'' happy_var_1)+ )}++happyReduce_117 = happySpecReduce_1 65# happyReduction_117+happyReduction_117 happy_x_1+ = case happyOutTok happy_x_1 of { (DollarWord happy_var_1) -> + happyIn69+ (happy_var_1+ )}++happyReduce_118 = happySpecReduce_1 66# happyReduction_118+happyReduction_118 happy_x_1+ = case happyOutTok happy_x_1 of { (DollarDollarWord happy_var_1) -> + happyIn70+ (happy_var_1+ )}++happyReduce_119 = happySpecReduce_1 67# happyReduction_119+happyReduction_119 happy_x_1+ = case happyOutTok happy_x_1 of { (Real happy_var_1) -> + happyIn71+ (happy_var_1+ )}++happyReduce_120 = happySpecReduce_1 67# happyReduction_120+happyReduction_120 happy_x_1+ = case happyOutTok happy_x_1 of { (SignedInt happy_var_1) -> + happyIn71+ (fromIntegral happy_var_1+ )}++happyReduce_121 = happySpecReduce_1 67# happyReduction_121+happyReduction_121 happy_x_1+ = case happyOutTok happy_x_1 of { (UnsignedInt happy_var_1) -> + happyIn71+ (fromIntegral happy_var_1+ )}++happyReduce_122 = happySpecReduce_1 68# happyReduction_122+happyReduction_122 happy_x_1+ = case happyOutTok happy_x_1 of { (SingleQuoted happy_var_1) -> + happyIn72+ (stripQuotes '\'' happy_var_1+ )}++happyReduce_123 = happySpecReduce_1 69# happyReduction_123+happyReduction_123 happy_x_1+ = case happyOutTok happy_x_1 of { (LowerWord happy_var_1) -> + happyIn73+ (happy_var_1+ )}++happyReduce_124 = happySpecReduce_1 69# happyReduction_124+happyReduction_124 happy_x_1+ = happyIn73+ ("fof"+ )++happyReduce_125 = happySpecReduce_1 69# happyReduction_125+happyReduction_125 happy_x_1+ = happyIn73+ ("cnf"+ )++happyReduce_126 = happySpecReduce_1 69# happyReduction_126+happyReduction_126 happy_x_1+ = happyIn73+ ("include"+ )++happyNewToken action sts stk [] =+ happyDoAction 37# notHappyAtAll action sts stk []++happyNewToken action sts stk (tk:tks) =+ let cont i = happyDoAction i tk action sts stk tks in+ case tk of {+ LP -> cont 1#;+ RP -> cont 2#;+ Lbrack -> cont 3#;+ Rbrack -> cont 4#;+ Comma -> cont 5#;+ Dot -> cont 6#;+ Star -> cont 7#;+ Plus -> cont 8#;+ Rangle -> cont 9#;+ Oper ":" -> cont 10#;+ Oper "<=>" -> cont 11#;+ Oper "=>" -> cont 12#;+ Oper "<~>" -> cont 13#;+ Oper "~|" -> cont 14#;+ Oper "~&" -> cont 15#;+ Oper "<=" -> cont 16#;+ Oper "=" -> cont 17#;+ Oper "!=" -> cont 18#;+ Oper "!" -> cont 19#;+ Oper "?" -> cont 20#;+ Oper "&" -> cont 21#;+ Oper "|" -> cont 22#;+ Oper "~" -> cont 23#;+ LowerWord "fof" -> cont 24#;+ LowerWord "cnf" -> cont 25#;+ LowerWord "include" -> cont 26#;+ SingleQuoted happy_dollar_dollar -> cont 27#;+ DoubleQuoted happy_dollar_dollar -> cont 28#;+ DollarWord happy_dollar_dollar -> cont 29#;+ DollarDollarWord happy_dollar_dollar -> cont 30#;+ UpperWord happy_dollar_dollar -> cont 31#;+ LowerWord happy_dollar_dollar -> cont 32#;+ SignedInt happy_dollar_dollar -> cont 33#;+ UnsignedInt happy_dollar_dollar -> cont 34#;+ Real happy_dollar_dollar -> cont 35#;+ CommentToken happy_dollar_dollar -> cont 36#;+ _ -> happyError' (tk:tks)+ }++happyError_ tk tks = happyError' (tk:tks)++newtype HappyIdentity a = HappyIdentity a+happyIdentity = HappyIdentity+happyRunIdentity (HappyIdentity a) = a++instance Monad HappyIdentity where+ return = HappyIdentity+ (HappyIdentity p) >>= q = q p++happyThen :: () => HappyIdentity a -> (a -> HappyIdentity b) -> HappyIdentity b+happyThen = (>>=)+happyReturn :: () => a -> HappyIdentity a+happyReturn = (return)+happyThen1 m k tks = (>>=) m (\a -> k a tks)+happyReturn1 :: () => a -> b -> HappyIdentity a+happyReturn1 = \a tks -> (return) a+happyError' :: () => [(Token)] -> HappyIdentity a+happyError' = HappyIdentity . ((\xs -> case xs of+ xs -> error ("Parse error, pos: "++show (take 25 xs))))++parseTPTP tks = happyRunIdentity happySomeParser where+ happySomeParser = happyThen (happyParse 0# tks) (\x -> happyReturn (happyOut4 x))++happySeq = happyDontSeq+++stripQuotes which (x:xs) = go xs+ where+ go [x] = []+ go ('\\':'\\':xs) = '\\':go xs+ go ('\\':which:xs) = which:go xs+ go (x:xs) = x:go xs+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "<built-in>" #-}+{-# LINE 1 "<command-line>" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+-- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp ++{-# LINE 28 "templates/GenericTemplate.hs" #-}+++data Happy_IntList = HappyCons Happy_GHC_Exts.Int# Happy_IntList++++++{-# LINE 49 "templates/GenericTemplate.hs" #-}++{-# LINE 59 "templates/GenericTemplate.hs" #-}++{-# LINE 68 "templates/GenericTemplate.hs" #-}++infixr 9 `HappyStk`+data HappyStk a = HappyStk a (HappyStk a)++-----------------------------------------------------------------------------+-- starting the parse++happyParse start_state = happyNewToken start_state notHappyAtAll notHappyAtAll++-----------------------------------------------------------------------------+-- Accepting the parse++-- If the current token is 0#, it means we've just accepted a partial+-- parse (a %partial parser). We must ignore the saved token on the top of+-- the stack in this case.+happyAccept 0# tk st sts (_ `HappyStk` ans `HappyStk` _) =+ happyReturn1 ans+happyAccept j tk st sts (HappyStk ans _) = + (happyTcHack j (happyTcHack st)) (happyReturn1 ans)++-----------------------------------------------------------------------------+-- Arrays only: do the next action++++happyDoAction i tk st+ = {- nothing -}+++ case action of+ 0# -> {- nothing -}+ happyFail i tk st+ -1# -> {- nothing -}+ happyAccept i tk st+ n | (n Happy_GHC_Exts.<# (0# :: Happy_GHC_Exts.Int#)) -> {- nothing -}++ (happyReduceArr Happy_Data_Array.! rule) i tk st+ where rule = (Happy_GHC_Exts.I# ((Happy_GHC_Exts.negateInt# ((n Happy_GHC_Exts.+# (1# :: Happy_GHC_Exts.Int#))))))+ n -> {- nothing -}+++ happyShift new_state i tk st+ where new_state = (n Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#))+ where off = indexShortOffAddr happyActOffsets st+ off_i = (off Happy_GHC_Exts.+# i)+ check = if (off_i Happy_GHC_Exts.>=# (0# :: Happy_GHC_Exts.Int#))+ then (indexShortOffAddr happyCheck off_i Happy_GHC_Exts.==# i)+ else False+ action | check = indexShortOffAddr happyTable off_i+ | otherwise = indexShortOffAddr happyDefActions st++{-# LINE 127 "templates/GenericTemplate.hs" #-}+++indexShortOffAddr (HappyA# arr) off =+#if __GLASGOW_HASKELL__ > 500+ Happy_GHC_Exts.narrow16Int# i+#elif __GLASGOW_HASKELL__ == 500+ Happy_GHC_Exts.intToInt16# i+#else+ Happy_GHC_Exts.iShiftRA# (Happy_GHC_Exts.iShiftL# i 16#) 16#+#endif+ where+#if __GLASGOW_HASKELL__ >= 503+ i = Happy_GHC_Exts.word2Int# (Happy_GHC_Exts.or# (Happy_GHC_Exts.uncheckedShiftL# high 8#) low)+#else+ i = Happy_GHC_Exts.word2Int# (Happy_GHC_Exts.or# (Happy_GHC_Exts.shiftL# high 8#) low)+#endif+ high = Happy_GHC_Exts.int2Word# (Happy_GHC_Exts.ord# (Happy_GHC_Exts.indexCharOffAddr# arr (off' Happy_GHC_Exts.+# 1#)))+ low = Happy_GHC_Exts.int2Word# (Happy_GHC_Exts.ord# (Happy_GHC_Exts.indexCharOffAddr# arr off'))+ off' = off Happy_GHC_Exts.*# 2#++++++data HappyAddr = HappyA# Happy_GHC_Exts.Addr#+++++-----------------------------------------------------------------------------+-- HappyState data type (not arrays)++{-# LINE 170 "templates/GenericTemplate.hs" #-}++-----------------------------------------------------------------------------+-- Shifting a token++happyShift new_state 0# tk st sts stk@(x `HappyStk` _) =+ let i = (case Happy_GHC_Exts.unsafeCoerce# x of { (Happy_GHC_Exts.I# (i)) -> i }) in+-- trace "shifting the error token" $+ happyDoAction i tk new_state (HappyCons (st) (sts)) (stk)++happyShift new_state i tk st sts stk =+ happyNewToken new_state (HappyCons (st) (sts)) ((happyInTok (tk))`HappyStk`stk)++-- happyReduce is specialised for the common cases.++happySpecReduce_0 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_0 nt fn j tk st@((action)) sts stk+ = happyGoto nt j tk st (HappyCons (st) (sts)) (fn `HappyStk` stk)++happySpecReduce_1 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_1 nt fn j tk _ sts@((HappyCons (st@(action)) (_))) (v1`HappyStk`stk')+ = let r = fn v1 in+ happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk'))++happySpecReduce_2 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_2 nt fn j tk _ (HappyCons (_) (sts@((HappyCons (st@(action)) (_))))) (v1`HappyStk`v2`HappyStk`stk')+ = let r = fn v1 v2 in+ happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk'))++happySpecReduce_3 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_3 nt fn j tk _ (HappyCons (_) ((HappyCons (_) (sts@((HappyCons (st@(action)) (_))))))) (v1`HappyStk`v2`HappyStk`v3`HappyStk`stk')+ = let r = fn v1 v2 v3 in+ happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk'))++happyReduce k i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happyReduce k nt fn j tk st sts stk+ = case happyDrop (k Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#)) sts of+ sts1@((HappyCons (st1@(action)) (_))) ->+ let r = fn stk in -- it doesn't hurt to always seq here...+ happyDoSeq r (happyGoto nt j tk st1 sts1 r)++happyMonadReduce k nt fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happyMonadReduce k nt fn j tk st sts stk =+ happyThen1 (fn stk tk) (\r -> happyGoto nt j tk st1 sts1 (r `HappyStk` drop_stk))+ where sts1@((HappyCons (st1@(action)) (_))) = happyDrop k (HappyCons (st) (sts))+ drop_stk = happyDropStk k stk++happyMonad2Reduce k nt fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happyMonad2Reduce k nt fn j tk st sts stk =+ happyThen1 (fn stk tk) (\r -> happyNewToken new_state sts1 (r `HappyStk` drop_stk))+ where sts1@((HappyCons (st1@(action)) (_))) = happyDrop k (HappyCons (st) (sts))+ drop_stk = happyDropStk k stk++ off = indexShortOffAddr happyGotoOffsets st1+ off_i = (off Happy_GHC_Exts.+# nt)+ new_state = indexShortOffAddr happyTable off_i+++++happyDrop 0# l = l+happyDrop n (HappyCons (_) (t)) = happyDrop (n Happy_GHC_Exts.-# (1# :: Happy_GHC_Exts.Int#)) t++happyDropStk 0# l = l+happyDropStk n (x `HappyStk` xs) = happyDropStk (n Happy_GHC_Exts.-# (1#::Happy_GHC_Exts.Int#)) xs++-----------------------------------------------------------------------------+-- Moving to a new state after a reduction+++happyGoto nt j tk st = + {- nothing -}+ happyDoAction j tk new_state+ where off = indexShortOffAddr happyGotoOffsets st+ off_i = (off Happy_GHC_Exts.+# nt)+ new_state = indexShortOffAddr happyTable off_i+++++-----------------------------------------------------------------------------+-- Error recovery (0# is the error token)++-- parse error if we are in recovery and we fail again+happyFail 0# tk old_st _ stk =+-- trace "failing" $ + happyError_ tk++{- We don't need state discarding for our restricted implementation of+ "error". In fact, it can cause some bogus parses, so I've disabled it+ for now --SDM++-- discard a state+happyFail 0# tk old_st (HappyCons ((action)) (sts)) + (saved_tok `HappyStk` _ `HappyStk` stk) =+-- trace ("discarding state, depth " ++ show (length stk)) $+ happyDoAction 0# tk action sts ((saved_tok`HappyStk`stk))+-}++-- Enter error recovery: generate an error token,+-- save the old token and carry on.+happyFail i tk (action) sts stk =+-- trace "entering error recovery" $+ happyDoAction 0# tk action sts ( (Happy_GHC_Exts.unsafeCoerce# (Happy_GHC_Exts.I# (i))) `HappyStk` stk)++-- Internal happy errors:++notHappyAtAll = error "Internal Happy error\n"++-----------------------------------------------------------------------------+-- Hack to get the typechecker to accept our action functions+++happyTcHack :: Happy_GHC_Exts.Int# -> a -> a+happyTcHack x y = y+{-# INLINE happyTcHack #-}+++-----------------------------------------------------------------------------+-- Seq-ing. If the --strict flag is given, then Happy emits +-- happySeq = happyDoSeq+-- otherwise it emits+-- happySeq = happyDontSeq++happyDoSeq, happyDontSeq :: a -> b -> b+happyDoSeq a b = a `seq` b+happyDontSeq a b = b++-----------------------------------------------------------------------------+-- Don't inline any functions from the template. GHC has a nasty habit+-- of deciding to inline happyGoto everywhere, which increases the size of+-- the generated parser quite a bit.+++{-# NOINLINE happyDoAction #-}+{-# NOINLINE happyTable #-}+{-# NOINLINE happyCheck #-}+{-# NOINLINE happyActOffsets #-}+{-# NOINLINE happyGotoOffsets #-}+{-# NOINLINE happyDefActions #-}++{-# NOINLINE happyShift #-}+{-# NOINLINE happySpecReduce_0 #-}+{-# NOINLINE happySpecReduce_1 #-}+{-# NOINLINE happySpecReduce_2 #-}+{-# NOINLINE happySpecReduce_3 #-}+{-# NOINLINE happyReduce #-}+{-# NOINLINE happyMonadReduce #-}+{-# NOINLINE happyGoto #-}+{-# NOINLINE happyFail #-}++-- end of Happy Template.
+ logic-TPTP.cabal view
@@ -0,0 +1,69 @@+name: logic-TPTP +version: 0.1+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+description: + For information about the TPTP format, see <http://www.cs.miami.edu/~tptp/>.+ .+ Components:+ .+ - Parser ('parse')+ .+ - Exporter ('toTPTP')+ .+ - Pretty-printer ('pretty')+ .+ - 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)+ .+ 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@ + .+ Not yet implemented: The new /thf/ formula type.+ .+ + +category: Codec,Math,Theorem Provers+author: Daniel Schüssler+cabal-version: >= 1.6+extra-source-files: testing/compileTests.sh+ testing/TestImportExportRandom.hs+ testing/TestImportExportImportFile.hs+ testing/PrettyPrintFile.hs+ testing/PrettyPrintFile.hs+ +tested-with: GHC==6.10.2++source-repository head+ type: darcs+ location: http://code.haskell.org/~daniels/logic-TPTP+ + ++Library+ ghc-options: -O2+ + build-depends: base >=4 ,array, syb, containers, haskell98+ , ansi-wl-pprint, QuickCheck>=2 + , utf8-prelude+ + exposed-modules: Codec.TPTP.Import+ ,Codec.TPTP.Base+ ,Codec.TPTP+ ,Codec.TPTP.Pretty+ ,Codec.TPTP.Export+ ,Codec.TPTP.Diff+ + other-modules:+ Lexer + , Parser+ ,Codec.TPTP.QuickCheck
+ testing/PrettyPrintFile.hs view
@@ -0,0 +1,44 @@+{-# OPTIONS + -fglasgow-exts + -XCPP + -XTemplateHaskell + -XNamedFieldPuns + -XRecordWildCards + -XDeriveDataTypeable + -XOverlappingInstances+ -XPackageImports+ -fwarn-incomplete-patterns+ #-}++module PrettyPrintFile 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+++main = putStrLn . prettySimple . parse =<< readFile =<< getArgs+
+ testing/TestImportExportImportFile.hs view
@@ -0,0 +1,67 @@+{-# OPTIONS + -fglasgow-exts + -XCPP + -XTemplateHaskell + -XNamedFieldPuns + -XRecordWildCards + -XDeriveDataTypeable + -XOverlappingInstances+ -XPackageImports+ -fwarn-incomplete-patterns+ #-}++module TestImportExportImportFile 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+++main = diff_once_twice+ +diff_once_twice = 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)+ + +
+ testing/TestImportExportRandom.hs view
@@ -0,0 +1,62 @@+{-# OPTIONS + -fglasgow-exts + -XCPP + -XTemplateHaskell + -XNamedFieldPuns + -XRecordWildCards + -XDeriveDataTypeable + -XOverlappingInstances+ -XPackageImports+ -fwarn-incomplete-patterns+ #-}++module TestImportExportRandom 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++main = quickCheck prop_test_ie++prop_test_ie f =+ let tptp = toTPTP' [f] in++ (let+ [g] = parse $ trace tptp tptp+ + dif = diffAFormula f g+ in+ whenFail+ (putStrLn . prettySimple $ dif) + + (case dif of + OtherSame -> True+ FormulaDiff (FormulaFix Same) -> True+ _ -> False+ ))+ +
+ testing/compileTests.sh view
@@ -0,0 +1,12 @@+#!/bin/bash++set -e++mkdir -p bin+mkdir -p obj++for x in TestImportExportImportFile TestImportExportRandom PrettyPrintFile ParseRandom; do+ + ghc -outputdir obj -o bin/$x --make -O2 -main-is $x $x+ +done