diff --git a/Codec/TPTP.hs b/Codec/TPTP.hs new file mode 100644 --- /dev/null +++ b/Codec/TPTP.hs @@ -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) + + diff --git a/Codec/TPTP/Base.hs b/Codec/TPTP/Base.hs new file mode 100644 --- /dev/null +++ b/Codec/TPTP/Base.hs @@ -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 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 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)) } + + diff --git a/Codec/TPTP/Diff.hs b/Codec/TPTP/Diff.hs new file mode 100644 --- /dev/null +++ b/Codec/TPTP/Diff.hs @@ -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 diff --git a/Codec/TPTP/Export.hs b/Codec/TPTP/Export.hs new file mode 100644 --- /dev/null +++ b/Codec/TPTP/Export.hs @@ -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 diff --git a/Codec/TPTP/Import.hs b/Codec/TPTP/Import.hs new file mode 100644 --- /dev/null +++ b/Codec/TPTP/Import.hs @@ -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 diff --git a/Codec/TPTP/Pretty.hs b/Codec/TPTP/Pretty.hs new file mode 100644 --- /dev/null +++ b/Codec/TPTP/Pretty.hs @@ -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 "]" + + diff --git a/Codec/TPTP/QuickCheck.hs b/Codec/TPTP/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/Codec/TPTP/QuickCheck.hs @@ -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)) + ] diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + 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. + + + Copyright (C) + + 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 . + +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: + + Copyright (C) + 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 +. + + 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 +. diff --git a/Lexer.x b/Lexer.x new file mode 100644 --- /dev/null +++ b/Lexer.x @@ -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 +} diff --git a/Parser.y b/Parser.y new file mode 100644 --- /dev/null +++ b/Parser.y @@ -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 + + +} + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -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 } + + diff --git a/dist/build/Lexer.hs b/dist/build/Lexer.hs new file mode 100644 --- /dev/null +++ b/dist/build/Lexer.hs @@ -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 "" #-} +{-# LINE 1 "" #-} +{-# 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 "" #-} +{-# LINE 1 "" #-} +{-# 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 diff --git a/dist/build/Parser.hs b/dist/build/Parser.hs new file mode 100644 --- /dev/null +++ b/dist/build/Parser.hs @@ -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 "" #-} +{-# LINE 1 "" #-} +{-# 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. diff --git a/logic-TPTP.cabal b/logic-TPTP.cabal new file mode 100644 --- /dev/null +++ b/logic-TPTP.cabal @@ -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 +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 . + . + 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 diff --git a/testing/PrettyPrintFile.hs b/testing/PrettyPrintFile.hs new file mode 100644 --- /dev/null +++ b/testing/PrettyPrintFile.hs @@ -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 + diff --git a/testing/TestImportExportImportFile.hs b/testing/TestImportExportImportFile.hs new file mode 100644 --- /dev/null +++ b/testing/TestImportExportImportFile.hs @@ -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) + + + diff --git a/testing/TestImportExportRandom.hs b/testing/TestImportExportRandom.hs new file mode 100644 --- /dev/null +++ b/testing/TestImportExportRandom.hs @@ -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 + )) + + diff --git a/testing/compileTests.sh b/testing/compileTests.sh new file mode 100644 --- /dev/null +++ b/testing/compileTests.sh @@ -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