module HyLo.InputFile.Parser ( parse,
initParseState,
ParseState,
QueryType(..),
RelProperty(..),
ParseOutput(..), RelInfo, ProverInfo,InferenceTask,
relations, provers, theory, tasks)
where
import Control.Monad.State
import HyLo.InputFile.Lexer ( Token(..), FilePos, line, col )
import HyLo.Signature.String ( StringSignature,
PropSymbol(..),
NomSymbol(..),
RelSymbol(..))
import HyLo.Signature ( Signature,
emptySignature,
addNomToSig,
addPropToSig,
addRelToSig,
isNomInSig,
isPropInSig,
isRelInSig)
import HyLo.Formula as Formula ( Formula(..) )
#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
newtype HappyAbsSyn = HappyAbsSyn HappyAny
#if __GLASGOW_HASKELL__ >= 607
type HappyAny = Happy_GHC_Exts.Any
#else
type HappyAny = forall a . a
#endif
happyIn4 :: (ParseOutput) -> (HappyAbsSyn )
happyIn4 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut4 :: (HappyAbsSyn ) -> (ParseOutput)
happyOut4 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn5 :: ([RelInfo]) -> (HappyAbsSyn )
happyIn5 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut5 :: (HappyAbsSyn ) -> ([RelInfo])
happyOut5 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn6 :: (String) -> (HappyAbsSyn )
happyIn6 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut6 :: (HappyAbsSyn ) -> (String)
happyOut6 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn7 :: ([Formula NomSymbol PropSymbol RelSymbol]) -> (HappyAbsSyn )
happyIn7 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut7 :: (HappyAbsSyn ) -> ([Formula NomSymbol PropSymbol RelSymbol])
happyOut7 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn8 :: ([InferenceTask]) -> (HappyAbsSyn )
happyIn8 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut8 :: (HappyAbsSyn ) -> ([InferenceTask])
happyOut8 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn9 :: (InferenceTask) -> (HappyAbsSyn )
happyIn9 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut9 :: (HappyAbsSyn ) -> (InferenceTask)
happyOut9 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn10 :: (Maybe String) -> (HappyAbsSyn )
happyIn10 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut10 :: (HappyAbsSyn ) -> (Maybe String)
happyOut10 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn11 :: ([ProverInfo]) -> (HappyAbsSyn )
happyIn11 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut11 :: (HappyAbsSyn ) -> ([ProverInfo])
happyOut11 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn12 :: ([ProverInfo]) -> (HappyAbsSyn )
happyIn12 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut12 :: (HappyAbsSyn ) -> ([ProverInfo])
happyOut12 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn13 :: ([(String,String)]) -> (HappyAbsSyn )
happyIn13 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut13 :: (HappyAbsSyn ) -> ([(String,String)])
happyOut13 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn14 :: (String) -> (HappyAbsSyn )
happyIn14 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut14 :: (HappyAbsSyn ) -> (String)
happyOut14 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn15 :: ([RelInfo]) -> (HappyAbsSyn )
happyIn15 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut15 :: (HappyAbsSyn ) -> ([RelInfo])
happyOut15 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn16 :: ([RelInfo]) -> (HappyAbsSyn )
happyIn16 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut16 :: (HappyAbsSyn ) -> ([RelInfo])
happyOut16 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn17 :: ([RelInfo]) -> (HappyAbsSyn )
happyIn17 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut17 :: (HappyAbsSyn ) -> ([RelInfo])
happyOut17 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn18 :: ([RelProperty]) -> (HappyAbsSyn )
happyIn18 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut18 :: (HappyAbsSyn ) -> ([RelProperty])
happyOut18 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn19 :: (RelProperty) -> (HappyAbsSyn )
happyIn19 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut19 :: (HappyAbsSyn ) -> (RelProperty)
happyOut19 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn20 :: (RelProperty) -> (HappyAbsSyn )
happyIn20 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut20 :: (HappyAbsSyn ) -> (RelProperty)
happyOut20 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn21 :: ([String]) -> (HappyAbsSyn )
happyIn21 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut21 :: (HappyAbsSyn ) -> ([String])
happyOut21 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn22 :: ([Formula NomSymbol PropSymbol RelSymbol]) -> (HappyAbsSyn )
happyIn22 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut22 :: (HappyAbsSyn ) -> ([Formula NomSymbol PropSymbol RelSymbol])
happyOut22 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn23 :: (Formula NomSymbol PropSymbol RelSymbol) -> (HappyAbsSyn )
happyIn23 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut23 :: (HappyAbsSyn ) -> (Formula NomSymbol PropSymbol RelSymbol)
happyOut23 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn24 :: (RelSymbol) -> (HappyAbsSyn )
happyIn24 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut24 :: (HappyAbsSyn ) -> (RelSymbol)
happyOut24 x = Happy_GHC_Exts.unsafeCoerce# x
happyIn25 :: (NomSymbol) -> (HappyAbsSyn )
happyIn25 x = Happy_GHC_Exts.unsafeCoerce# x
happyOut25 :: (HappyAbsSyn ) -> (NomSymbol)
happyOut25 x = Happy_GHC_Exts.unsafeCoerce# x
happyInTok :: ((Token, FilePos)) -> (HappyAbsSyn )
happyInTok x = Happy_GHC_Exts.unsafeCoerce# x
happyOutTok :: (HappyAbsSyn ) -> ((Token, FilePos))
happyOutTok x = Happy_GHC_Exts.unsafeCoerce# x
happyActOffsets :: HappyAddr
happyActOffsets = HappyA# "\xff\x00\xff\x00\xf6\x00\xf5\x00\x40\x00\xf4\x00\x00\x00\x00\x00\xf3\x00\xf1\x00\xf0\x00\x00\x00\x73\x00\x73\x00\x73\x00\xf2\x00\xef\x00\xee\x00\xed\x00\xec\x00\x00\x00\x00\x00\x00\x00\xea\x00\xe7\xff\xe3\x00\xab\x00\xe8\x00\x73\x00\xab\x00\xab\x00\x73\x00\xe9\x00\xeb\x00\xe7\x00\xe9\xff\x00\x00\xe4\x00\xe6\x00\xe2\x00\xe5\x00\x00\x00\x00\x00\x00\x00\x00\x00\x6c\x00\x00\x00\xe1\x00\xe0\x00\xde\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x73\x00\x05\x00\x02\x00\x73\x00\x73\x00\x73\x00\x00\x00\x95\x00\x00\x00\xdd\x00\x2f\x00\xdc\x00\x1b\x00\x09\x00\x0a\x00\xda\x00\x00\x00\x00\x00\xe9\xff\xe9\xff\xe9\xff\xe9\xff\xe9\xff\xe9\xff\xe9\xff\xe9\xff\x71\x00\x71\x00\xce\x00\x00\x00\x00\x00\x00\x00\xca\x00\x43\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe9\xff\xd2\x00\x00\x00\x00\x00\xc0\x00\x6f\x00\xe9\xff\xe9\xff\xe9\xff\xe9\xff\xe9\xff\xe9\xff\x00\x00\xcd\x00\xcd\x00\xcd\x00\xc9\x00\x00\x00\x00\x00\x00\x00\x68\x00\x00\x00\x68\x00\x00\x00\x6c\x00\x6c\x00\xcc\x00\x68\x00\x00\x00\x00\x00\xc8\x00\xc7\x00\xc3\x00\xc6\x00\xcb\x00\xc5\x00\xc4\x00\x00\x00\x49\x00\x85\x00\xc2\x00\x00\x00\x00\x00\xe9\xff\xe9\xff\xe9\xff\xe9\xff\x00\x00\x00\x00\xe9\xff\xe9\xff\x49\x00\x49\x00\x00\x00\x00\x00\x37\x00\x33\x00\xbf\x00\xbc\x00\x00\x00\xbb\x00\x68\x00\x00\x00\x00\x00\x00\x00\xb0\x00\xb8\x00\xe9\xff\xe9\xff\xe9\xff\x00\x00\x00\x00\xb7\x00\xb4\x00\xaf\x00\xd0\x00\x64\x00\x00\x00\xb3\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x68\x00\x00\x00\x00\x00"#
happyGotoOffsets :: HappyAddr
happyGotoOffsets = HappyA# "\xdf\x00\x00\x00\x00\x00\x00\x00\x3a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x27\x00\x30\x00\x29\x00\xd9\x00\xdb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xd1\x00\x00\x00\x0b\x00\xcf\x00\x8c\x00\x19\x00\xd4\x00\x2c\x00\x00\x00\x88\x00\x00\x00\x07\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x96\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xd8\x00\xd7\x00\xd6\x00\xd5\x00\xd3\x00\x9a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc1\x00\xbe\x00\xbd\x00\xba\x00\xb9\x00\xb6\x00\xb5\x00\xb2\x00\x6b\x00\x6a\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xb1\x00\x00\x00\x00\x00\x00\x00\x00\x00\x24\x00\xae\x00\xad\x00\xaa\x00\xa9\x00\xa6\x00\x84\x00\x00\x00\x69\x00\x44\x00\x1e\x00\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x14\x00\x00\x00\x93\x00\x90\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa5\x00\xa2\x00\xa1\x00\x9e\x00\x00\x00\x00\x00\x9d\x00\x75\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x61\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x4c\x00\x39\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xfc\xff\x45\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x60\x00\x00\x00\x00\x00"#
happyDefActions :: HappyAddr
happyDefActions = HappyA# "\x00\x00\x00\x00\x00\x00\x00\x00\xe4\xff\x00\x00\xfd\xff\xfc\xff\x00\x00\x00\x00\x00\x00\xe5\xff\xe0\xff\xc9\xff\xc9\xff\xf0\xff\x00\x00\x00\x00\xc8\xff\x00\x00\xfb\xff\xfa\xff\xf9\xff\x00\x00\xdf\xff\x00\x00\xe4\xff\x00\x00\xe0\xff\xe4\xff\xe4\xff\xc9\xff\xee\xff\xf7\xff\x00\x00\xc6\xff\xfe\xff\xf7\xff\x00\x00\x00\x00\x00\x00\xc7\xff\xe3\xff\xe2\xff\xde\xff\xdb\xff\xe1\xff\x00\x00\xda\xff\xd9\xff\xd4\xff\xd6\xff\xd5\xff\xd3\xff\xd2\xff\xd1\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xef\xff\x00\x00\xf6\xff\x00\x00\xc5\xff\x00\x00\xa6\xff\x00\x00\xa7\xff\xc1\xff\xc3\xff\xc2\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa8\xff\xaa\xff\xa9\xff\x00\x00\x00\x00\xbc\xff\xbd\xff\xbe\xff\xb9\xff\xba\xff\xbb\xff\xb4\xff\x00\x00\x00\x00\xa6\xff\xa7\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc6\xff\xf8\xff\xf2\xff\xf2\xff\xf2\xff\x00\x00\xca\xff\xcb\xff\xce\xff\xc9\xff\xd0\xff\xc9\xff\xcc\xff\xdb\xff\xdb\xff\xdd\xff\xe0\xff\xd8\xff\xd7\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc4\xff\xb5\xff\xb6\xff\xb2\xff\xb3\xff\xb0\xff\x00\x00\x00\x00\x00\x00\x00\x00\xb1\xff\xab\xff\x00\x00\x00\x00\xb7\xff\xb8\xff\xac\xff\xad\xff\x00\x00\x00\x00\x00\x00\x00\x00\xf1\xff\x00\x00\xec\xff\xcd\xff\xcf\xff\xdc\xff\x00\x00\x00\x00\xc6\xff\xc6\xff\xc6\xff\xae\xff\xaf\xff\x00\x00\x00\x00\x00\x00\xee\xff\x00\x00\xe9\xff\xeb\xff\xe8\xff\xe7\xff\xe6\xff\xed\xff\xf3\xff\xf4\xff\xf5\xff\xec\xff\xea\xff"#
happyCheck :: HappyAddr
happyCheck = HappyA# "\xff\xff\x18\x00\x1b\x00\x02\x00\x08\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x20\x00\x21\x00\x04\x00\x05\x00\x02\x00\x0d\x00\x26\x00\x27\x00\x28\x00\x29\x00\x2a\x00\x2b\x00\x2c\x00\x02\x00\x30\x00\x0d\x00\x02\x00\x18\x00\x02\x00\x33\x00\x18\x00\x35\x00\x1d\x00\x1e\x00\x18\x00\x1d\x00\x1e\x00\x06\x00\x11\x00\x1d\x00\x1e\x00\x11\x00\x02\x00\x11\x00\x02\x00\x22\x00\x23\x00\x24\x00\x25\x00\x04\x00\x05\x00\x02\x00\x31\x00\x0d\x00\x2c\x00\x31\x00\x2d\x00\x2e\x00\x15\x00\x11\x00\x01\x00\x32\x00\x22\x00\x23\x00\x24\x00\x25\x00\x11\x00\x02\x00\x03\x00\x04\x00\x0b\x00\x0c\x00\x02\x00\x2d\x00\x2e\x00\x06\x00\x12\x00\x13\x00\x32\x00\x15\x00\x0a\x00\x10\x00\x22\x00\x23\x00\x24\x00\x25\x00\x22\x00\x23\x00\x24\x00\x25\x00\x22\x00\x23\x00\x24\x00\x25\x00\x2e\x00\x12\x00\x13\x00\x2d\x00\x15\x00\x02\x00\x02\x00\x2d\x00\x22\x00\x23\x00\x24\x00\x25\x00\x09\x00\x09\x00\x22\x00\x23\x00\x24\x00\x25\x00\x06\x00\x2d\x00\x05\x00\x06\x00\x07\x00\x08\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x0e\x00\x0f\x00\x18\x00\x19\x00\x14\x00\x14\x00\x18\x00\x1d\x00\x1e\x00\x1f\x00\x20\x00\x1d\x00\x1e\x00\x18\x00\x13\x00\x18\x00\x15\x00\x18\x00\x1d\x00\x1e\x00\x1d\x00\x1e\x00\x1d\x00\x1e\x00\x12\x00\x13\x00\x15\x00\x15\x00\x12\x00\x13\x00\x0c\x00\x15\x00\x12\x00\x13\x00\x02\x00\x15\x00\x0e\x00\x0f\x00\x10\x00\x0e\x00\x0f\x00\x10\x00\x0e\x00\x0f\x00\x10\x00\x22\x00\x23\x00\x24\x00\x15\x00\x16\x00\x17\x00\x02\x00\x03\x00\x04\x00\x13\x00\x13\x00\x15\x00\x15\x00\x13\x00\x13\x00\x15\x00\x15\x00\x13\x00\x13\x00\x15\x00\x15\x00\x13\x00\x13\x00\x15\x00\x15\x00\x13\x00\x13\x00\x15\x00\x15\x00\x13\x00\x13\x00\x15\x00\x15\x00\x13\x00\x13\x00\x15\x00\x15\x00\x13\x00\x13\x00\x15\x00\x15\x00\x13\x00\x13\x00\x15\x00\x15\x00\x13\x00\x02\x00\x15\x00\x02\x00\x02\x00\x02\x00\x02\x00\x0c\x00\x08\x00\x0c\x00\x03\x00\x00\x00\x07\x00\x32\x00\x12\x00\x30\x00\x22\x00\x1a\x00\x32\x00\x37\x00\xff\xff\x32\x00\x32\x00\xff\xff\x31\x00\x31\x00\xff\xff\x2f\x00\x31\x00\x2d\x00\x2d\x00\x2d\x00\x31\x00\x1b\x00\x2d\x00\x1b\x00\x14\x00\x32\x00\x32\x00\x12\x00\x30\x00\x30\x00\x34\x00\x14\x00\x01\x00\x2f\x00\x13\x00\x11\x00\x36\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x30\x00\x32\x00\x30\x00\x2c\x00\x2c\x00\x32\x00\x32\x00\x32\x00\xff\xff\xff\xff\x31\x00\x31\x00\xff\xff\xff\xff\x32\x00\x30\x00\x32\x00\x31\x00\xff\xff\x31\x00\x31\x00\xff\xff\x31\x00\xff\xff\x32\x00\x31\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x38\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#
happyTable :: HappyAddr
happyTable = HappyA# "\x00\x00\x45\x00\x1c\x00\x18\x00\xb3\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x40\x00\x25\x00\x18\x00\xa1\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x12\x00\x1d\x00\x2c\x00\x12\x00\x15\x00\x12\x00\x53\x00\x15\x00\x54\x00\x16\x00\x17\x00\x64\x00\x16\x00\x17\x00\x82\x00\x7f\x00\x65\x00\x66\x00\x80\x00\x18\x00\x29\x00\x12\x00\xc0\xff\xc0\xff\xc0\xff\xc0\xff\x24\x00\x25\x00\x12\x00\x76\x00\x19\x00\x67\x00\x78\x00\xc0\xff\xc0\xff\x8c\x00\x13\x00\x05\x00\xc0\xff\xbf\xff\xbf\xff\xbf\xff\xbf\xff\x17\x00\x09\x00\x0a\x00\x0b\x00\x06\x00\x07\x00\xae\x00\xbf\xff\xbf\xff\x84\x00\xa9\x00\x42\x00\xbf\xff\x43\x00\xaf\x00\x0c\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\xaa\x00\x42\x00\xa8\x00\x43\x00\xa2\x00\xa2\x00\xa9\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\xb8\x00\xa3\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x85\x00\x92\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\x3a\x00\x3b\x00\x3c\x00\x3d\x00\x15\x00\xb1\x00\x54\x00\x58\x00\x15\x00\x16\x00\x17\x00\xb2\x00\xb3\x00\x16\x00\x17\x00\x64\x00\x94\x00\x56\x00\x43\x00\x15\x00\x65\x00\x8e\x00\x57\x00\x58\x00\x16\x00\x17\x00\xab\x00\x42\x00\x62\x00\x43\x00\x86\x00\x42\x00\x2a\x00\x43\x00\x41\x00\x42\x00\x71\x00\x43\x00\x7d\x00\x30\x00\x31\x00\x7e\x00\x30\x00\x31\x00\x2f\x00\x30\x00\x31\x00\x69\x00\x6a\x00\x6b\x00\x6f\x00\x70\x00\x71\x00\x09\x00\x0a\x00\x0b\x00\x95\x00\x96\x00\x43\x00\x43\x00\x97\x00\x98\x00\x43\x00\x43\x00\x99\x00\x87\x00\x43\x00\x43\x00\x88\x00\x89\x00\x43\x00\x43\x00\x8a\x00\x8b\x00\x43\x00\x43\x00\x90\x00\x59\x00\x43\x00\x43\x00\x5a\x00\x5b\x00\x43\x00\x43\x00\x5c\x00\x5d\x00\x43\x00\x43\x00\x5e\x00\x5f\x00\x43\x00\x43\x00\x60\x00\x72\x00\x43\x00\x73\x00\x74\x00\x76\x00\x78\x00\x2b\x00\x27\x00\x2e\x00\x21\x00\x03\x00\x10\x00\xb5\x00\x29\x00\xb8\x00\x69\x00\x9d\x00\xb6\x00\xae\x00\x00\x00\xb7\x00\xad\x00\x00\x00\xa5\x00\xa6\x00\x00\x00\x8f\x00\xa7\x00\x9b\x00\x9c\x00\x9e\x00\x9f\x00\x62\x00\x82\x00\x68\x00\x27\x00\xa0\x00\xa1\x00\x29\x00\x7d\x00\x84\x00\x93\x00\x27\x00\x03\x00\x90\x00\x23\x00\x12\x00\x94\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7a\x00\x6e\x00\x7b\x00\x3e\x00\x40\x00\x7c\x00\x3f\x00\x1b\x00\x00\x00\x00\x00\x24\x00\x2e\x00\x00\x00\x00\x00\x1e\x00\x20\x00\x1f\x00\x21\x00\x00\x00\x0d\x00\x0e\x00\x00\x00\x0f\x00\x00\x00\x10\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xff\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#
happyReduceArr = Happy_Data_Array.array (1, 89) [
(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)
]
happy_n_terms = 57 :: Int
happy_n_nonterms = 22 :: Int
happyReduce_1 = happyReduce 7# 0# happyReduction_1
happyReduction_1 (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 happyOut5 happy_x_3 of { happy_var_3 ->
case happyOut11 happy_x_5 of { happy_var_5 ->
case happyOut7 happy_x_6 of { happy_var_6 ->
case happyOut8 happy_x_7 of { happy_var_7 ->
happyIn4
(PO{relations = happy_var_3,
provers = happy_var_5,
theory = happy_var_6,
tasks = happy_var_7}
) `HappyStk` happyRest}}}}
happyReduce_2 = happySpecReduce_1 1# happyReduction_2
happyReduction_2 happy_x_1
= case happyOut15 happy_x_1 of { happy_var_1 ->
happyIn5
(happy_var_1
)}
happyReduce_3 = happySpecReduce_1 1# happyReduction_3
happyReduction_3 happy_x_1
= case happyOut16 happy_x_1 of { happy_var_1 ->
happyIn5
(happy_var_1
)}
happyReduce_4 = happySpecReduce_1 2# happyReduction_4
happyReduction_4 happy_x_1
= case happyOutTok happy_x_1 of { ((TokenVariable happy_var_1, _)) ->
happyIn6
(happy_var_1
)}
happyReduce_5 = happySpecReduce_1 2# happyReduction_5
happyReduction_5 happy_x_1
= case happyOutTok happy_x_1 of { ((TokenProp happy_var_1 , _)) ->
happyIn6
(let PropSymbol x = happy_var_1 in x
)}
happyReduce_6 = happySpecReduce_1 2# happyReduction_6
happyReduction_6 happy_x_1
= case happyOutTok happy_x_1 of { ((TokenNom happy_var_1 , _)) ->
happyIn6
(let NomSymbol x = happy_var_1 in x
)}
happyReduce_7 = happyReduce 4# 3# happyReduction_7
happyReduction_7 (happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest)
= case happyOut22 happy_x_3 of { happy_var_3 ->
happyIn7
(happy_var_3
) `HappyStk` happyRest}
happyReduce_8 = happySpecReduce_0 4# happyReduction_8
happyReduction_8 = happyIn8
([]
)
happyReduce_9 = happySpecReduce_2 4# happyReduction_9
happyReduction_9 happy_x_2
happy_x_1
= case happyOut9 happy_x_1 of { happy_var_1 ->
case happyOut8 happy_x_2 of { happy_var_2 ->
happyIn8
(happy_var_1:happy_var_2
)}}
happyReduce_10 = happyReduce 8# 5# happyReduction_10
happyReduction_10 (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 happyOut10 happy_x_4 of { happy_var_4 ->
case happyOut22 happy_x_7 of { happy_var_7 ->
happyIn9
((Valid, happy_var_4, happy_var_7)
) `HappyStk` happyRest}}
happyReduce_11 = happyReduce 8# 5# happyReduction_11
happyReduction_11 (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 happyOut10 happy_x_4 of { happy_var_4 ->
case happyOut22 happy_x_7 of { happy_var_7 ->
happyIn9
((Satisfiable, happy_var_4, happy_var_7)
) `HappyStk` happyRest}}
happyReduce_12 = happyReduce 8# 5# happyReduction_12
happyReduction_12 (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 happyOut10 happy_x_4 of { happy_var_4 ->
case happyOut22 happy_x_7 of { happy_var_7 ->
happyIn9
((Retrieve, happy_var_4, happy_var_7)
) `HappyStk` happyRest}}
happyReduce_13 = happySpecReduce_0 6# happyReduction_13
happyReduction_13 = happyIn10
(Nothing
)
happyReduce_14 = happySpecReduce_2 6# happyReduction_14
happyReduction_14 happy_x_2
happy_x_1
= case happyOutTok happy_x_2 of { ((TokenFile happy_var_2, _)) ->
happyIn10
(Just happy_var_2
)}
happyReduce_15 = happySpecReduce_0 7# happyReduction_15
happyReduction_15 = happyIn11
([]
)
happyReduce_16 = happyReduce 4# 7# happyReduction_16
happyReduction_16 (happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest)
= case happyOut12 happy_x_3 of { happy_var_3 ->
happyIn11
(happy_var_3
) `HappyStk` happyRest}
happyReduce_17 = happySpecReduce_0 8# happyReduction_17
happyReduction_17 = happyIn12
([]
)
happyReduce_18 = happyReduce 8# 8# happyReduction_18
happyReduction_18 (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 happyOut6 happy_x_3 of { happy_var_3 ->
case happyOut13 happy_x_6 of { happy_var_6 ->
case happyOut12 happy_x_8 of { happy_var_8 ->
happyIn12
((happy_var_3,happy_var_6):happy_var_8
) `HappyStk` happyRest}}}
happyReduce_19 = happySpecReduce_0 9# happyReduction_19
happyReduction_19 = happyIn13
([]
)
happyReduce_20 = happySpecReduce_3 9# happyReduction_20
happyReduction_20 happy_x_3
happy_x_2
happy_x_1
= case happyOut6 happy_x_1 of { happy_var_1 ->
case happyOut14 happy_x_3 of { happy_var_3 ->
happyIn13
([(happy_var_1,happy_var_3)]
)}}
happyReduce_21 = happyReduce 5# 9# happyReduction_21
happyReduction_21 (happy_x_5 `HappyStk`
happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest)
= case happyOut6 happy_x_1 of { happy_var_1 ->
case happyOut14 happy_x_3 of { happy_var_3 ->
case happyOut13 happy_x_5 of { happy_var_5 ->
happyIn13
((happy_var_1,happy_var_3): happy_var_5
) `HappyStk` happyRest}}}
happyReduce_22 = happySpecReduce_1 10# happyReduction_22
happyReduction_22 happy_x_1
= case happyOut6 happy_x_1 of { happy_var_1 ->
happyIn14
(happy_var_1
)}
happyReduce_23 = happySpecReduce_1 10# happyReduction_23
happyReduction_23 happy_x_1
= case happyOutTok happy_x_1 of { ((TokenLabel happy_var_1, _)) ->
happyIn14
(happy_var_1
)}
happyReduce_24 = happySpecReduce_1 10# happyReduction_24
happyReduction_24 happy_x_1
= happyIn14
("true"
)
happyReduce_25 = happySpecReduce_1 10# happyReduction_25
happyReduction_25 happy_x_1
= happyIn14
("false"
)
happyReduce_26 = happyMonadReduce 1# 11# happyReduction_26
happyReduction_26 (happy_x_1 `HappyStk`
happyRest) tk
= happyThen (( putType Automatic >>= \s -> return [])
) (\r -> happyReturn (happyIn15 r))
happyReduce_27 = happyMonadReduce 0# 12# happyReduction_27
happyReduction_27 (happyRest) tk
= happyThen (( putType NotAutomatic >>= \s -> return [])
) (\r -> happyReturn (happyIn16 r))
happyReduce_28 = happyMonadReduce 5# 12# happyReduction_28
happyReduction_28 (happy_x_5 `HappyStk`
happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOut21 happy_x_3 of { happy_var_3 ->
case happyOut16 happy_x_5 of { happy_var_5 ->
( getSig >>= \s -> putSig (foldr addPToSig s happy_var_3)
>>= \s -> putType NotAutomatic
>>= \s -> return happy_var_5)}}
) (\r -> happyReturn (happyIn16 r))
happyReduce_29 = happyMonadReduce 5# 12# happyReduction_29
happyReduction_29 (happy_x_5 `HappyStk`
happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOut21 happy_x_3 of { happy_var_3 ->
case happyOut16 happy_x_5 of { happy_var_5 ->
( getSig >>= \s -> putSig (foldr addNToSig s happy_var_3)
>>= \s -> putType NotAutomatic
>>= \s -> return happy_var_5)}}
) (\r -> happyReturn (happyIn16 r))
happyReduce_30 = happyMonadReduce 5# 12# happyReduction_30
happyReduction_30 (happy_x_5 `HappyStk`
happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOut17 happy_x_3 of { happy_var_3 ->
case happyOut16 happy_x_5 of { happy_var_5 ->
( getSig >>= \s -> putSig (foldr (addRToSig . fst) s happy_var_3)
>>= \s -> putType NotAutomatic
>>= \s -> return (happy_var_3++happy_var_5))}}
) (\r -> happyReturn (happyIn16 r))
happyReduce_31 = happySpecReduce_0 13# happyReduction_31
happyReduction_31 = happyIn17
([]
)
happyReduce_32 = happySpecReduce_1 13# happyReduction_32
happyReduction_32 happy_x_1
= case happyOut6 happy_x_1 of { happy_var_1 ->
happyIn17
([(happy_var_1, [])]
)}
happyReduce_33 = happySpecReduce_3 13# happyReduction_33
happyReduction_33 happy_x_3
happy_x_2
happy_x_1
= case happyOut6 happy_x_1 of { happy_var_1 ->
case happyOut17 happy_x_3 of { happy_var_3 ->
happyIn17
((happy_var_1, []):happy_var_3
)}}
happyReduce_34 = happyReduce 5# 13# happyReduction_34
happyReduction_34 (happy_x_5 `HappyStk`
happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest)
= case happyOut6 happy_x_1 of { happy_var_1 ->
case happyOut18 happy_x_4 of { happy_var_4 ->
happyIn17
([(happy_var_1, happy_var_4)]
) `HappyStk` happyRest}}
happyReduce_35 = happyReduce 7# 13# happyReduction_35
happyReduction_35 (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 happyOut6 happy_x_1 of { happy_var_1 ->
case happyOut18 happy_x_4 of { happy_var_4 ->
case happyOut17 happy_x_7 of { happy_var_7 ->
happyIn17
((happy_var_1 , happy_var_4):happy_var_7
) `HappyStk` happyRest}}}
happyReduce_36 = happySpecReduce_0 14# happyReduction_36
happyReduction_36 = happyIn18
([]
)
happyReduce_37 = happySpecReduce_1 14# happyReduction_37
happyReduction_37 happy_x_1
= case happyOut19 happy_x_1 of { happy_var_1 ->
happyIn18
([happy_var_1]
)}
happyReduce_38 = happySpecReduce_1 14# happyReduction_38
happyReduction_38 happy_x_1
= case happyOut20 happy_x_1 of { happy_var_1 ->
happyIn18
([happy_var_1]
)}
happyReduce_39 = happySpecReduce_3 14# happyReduction_39
happyReduction_39 happy_x_3
happy_x_2
happy_x_1
= case happyOut19 happy_x_1 of { happy_var_1 ->
case happyOut18 happy_x_3 of { happy_var_3 ->
happyIn18
(happy_var_1:happy_var_3
)}}
happyReduce_40 = happySpecReduce_3 14# happyReduction_40
happyReduction_40 happy_x_3
happy_x_2
happy_x_1
= case happyOut20 happy_x_1 of { happy_var_1 ->
case happyOut18 happy_x_3 of { happy_var_3 ->
happyIn18
(happy_var_1:happy_var_3
)}}
happyReduce_41 = happySpecReduce_1 15# happyReduction_41
happyReduction_41 happy_x_1
= happyIn19
(Universal
)
happyReduce_42 = happySpecReduce_1 15# happyReduction_42
happyReduction_42 happy_x_1
= happyIn19
(Difference
)
happyReduce_43 = happySpecReduce_1 15# happyReduction_43
happyReduction_43 happy_x_1
= happyIn19
(Reflexive
)
happyReduce_44 = happySpecReduce_1 15# happyReduction_44
happyReduction_44 happy_x_1
= happyIn19
(Transitive
)
happyReduce_45 = happySpecReduce_1 15# happyReduction_45
happyReduction_45 happy_x_1
= happyIn19
(Symmetric
)
happyReduce_46 = happySpecReduce_1 15# happyReduction_46
happyReduction_46 happy_x_1
= happyIn19
(Functional
)
happyReduce_47 = happySpecReduce_2 16# happyReduction_47
happyReduction_47 happy_x_2
happy_x_1
= case happyOut6 happy_x_2 of { happy_var_2 ->
happyIn20
(SubsetOf [happy_var_2]
)}
happyReduce_48 = happyReduce 4# 16# happyReduction_48
happyReduction_48 (happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest)
= case happyOut21 happy_x_3 of { happy_var_3 ->
happyIn20
(SubsetOf happy_var_3
) `HappyStk` happyRest}
happyReduce_49 = happySpecReduce_2 16# happyReduction_49
happyReduction_49 happy_x_2
happy_x_1
= case happyOut6 happy_x_2 of { happy_var_2 ->
happyIn20
(Equals [happy_var_2]
)}
happyReduce_50 = happyReduce 4# 16# happyReduction_50
happyReduction_50 (happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest)
= case happyOut21 happy_x_3 of { happy_var_3 ->
happyIn20
(Equals happy_var_3
) `HappyStk` happyRest}
happyReduce_51 = happySpecReduce_2 16# happyReduction_51
happyReduction_51 happy_x_2
happy_x_1
= case happyOut6 happy_x_2 of { happy_var_2 ->
happyIn20
(InverseOf happy_var_2
)}
happyReduce_52 = happySpecReduce_2 16# happyReduction_52
happyReduction_52 happy_x_2
happy_x_1
= case happyOut6 happy_x_2 of { happy_var_2 ->
happyIn20
(TClosureOf happy_var_2
)}
happyReduce_53 = happySpecReduce_2 16# happyReduction_53
happyReduction_53 happy_x_2
happy_x_1
= case happyOut6 happy_x_2 of { happy_var_2 ->
happyIn20
(TRClosureOf happy_var_2
)}
happyReduce_54 = happySpecReduce_0 17# happyReduction_54
happyReduction_54 = happyIn21
([]
)
happyReduce_55 = happySpecReduce_1 17# happyReduction_55
happyReduction_55 happy_x_1
= case happyOut6 happy_x_1 of { happy_var_1 ->
happyIn21
([happy_var_1]
)}
happyReduce_56 = happySpecReduce_3 17# happyReduction_56
happyReduction_56 happy_x_3
happy_x_2
happy_x_1
= case happyOut6 happy_x_1 of { happy_var_1 ->
case happyOut21 happy_x_3 of { happy_var_3 ->
happyIn21
(happy_var_1:happy_var_3
)}}
happyReduce_57 = happySpecReduce_0 18# happyReduction_57
happyReduction_57 = happyIn22
([]
)
happyReduce_58 = happySpecReduce_1 18# happyReduction_58
happyReduction_58 happy_x_1
= case happyOut23 happy_x_1 of { happy_var_1 ->
happyIn22
([happy_var_1]
)}
happyReduce_59 = happySpecReduce_3 18# happyReduction_59
happyReduction_59 happy_x_3
happy_x_2
happy_x_1
= case happyOut23 happy_x_1 of { happy_var_1 ->
case happyOut22 happy_x_3 of { happy_var_3 ->
happyIn22
(happy_var_1:happy_var_3
)}}
happyReduce_60 = happySpecReduce_1 19# happyReduction_60
happyReduction_60 happy_x_1
= happyIn23
(Top
)
happyReduce_61 = happySpecReduce_1 19# happyReduction_61
happyReduction_61 happy_x_1
= happyIn23
(Bot
)
happyReduce_62 = happyMonadReduce 1# 19# happyReduction_62
happyReduction_62 (happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOutTok happy_x_1 of { ((TokenNom happy_var_1 , _)) ->
( get >>= \s -> if (isAutomatic s)
then return (Nom happy_var_1)
else if (isNomInSig happy_var_1 (pSig s))
then return (Nom happy_var_1)
else (error $ (show happy_var_1) ++ " not in Sig as Nominal"))}
) (\r -> happyReturn (happyIn23 r))
happyReduce_63 = happyMonadReduce 1# 19# happyReduction_63
happyReduction_63 (happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOutTok happy_x_1 of { ((TokenProp happy_var_1 , _)) ->
( get >>= \s -> if (isAutomatic s)
then return (Prop happy_var_1)
else if (isPropInSig happy_var_1 (pSig s))
then return (Prop happy_var_1)
else (error $ (show happy_var_1) ++ " not in Sig as Prop"))}
) (\r -> happyReturn (happyIn23 r))
happyReduce_64 = happyMonadReduce 1# 19# happyReduction_64
happyReduction_64 (happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOutTok happy_x_1 of { ((TokenVariable happy_var_1, _)) ->
( getSig >>= \s -> if (isNomInSig (NomSymbol happy_var_1) s)
then return (Nom (NomSymbol happy_var_1))
else if (isPropInSig (PropSymbol happy_var_1) s)
then return (Prop (PropSymbol happy_var_1))
else if (isRelInSig (RelSymbol happy_var_1) s)
then error (happy_var_1 ++ " defined as Rel")
else (error $ "Symbol not in Sig : " ++ happy_var_1))}
) (\r -> happyReturn (happyIn23 r))
happyReduce_65 = happySpecReduce_2 19# happyReduction_65
happyReduction_65 happy_x_2
happy_x_1
= case happyOutTok happy_x_1 of { ((TokenDia happy_var_1 , _)) ->
case happyOut23 happy_x_2 of { happy_var_2 ->
happyIn23
(Diam happy_var_1 happy_var_2
)}}
happyReduce_66 = happySpecReduce_2 19# happyReduction_66
happyReduction_66 happy_x_2
happy_x_1
= case happyOut23 happy_x_2 of { happy_var_2 ->
happyIn23
(E happy_var_2
)}
happyReduce_67 = happySpecReduce_2 19# happyReduction_67
happyReduction_67 happy_x_2
happy_x_1
= case happyOut23 happy_x_2 of { happy_var_2 ->
happyIn23
(D happy_var_2
)}
happyReduce_68 = happySpecReduce_2 19# happyReduction_68
happyReduction_68 happy_x_2
happy_x_1
= case happyOutTok happy_x_1 of { ((TokenBox happy_var_1 , _)) ->
case happyOut23 happy_x_2 of { happy_var_2 ->
happyIn23
(Box happy_var_1 happy_var_2
)}}
happyReduce_69 = happySpecReduce_2 19# happyReduction_69
happyReduction_69 happy_x_2
happy_x_1
= case happyOut23 happy_x_2 of { happy_var_2 ->
happyIn23
(A happy_var_2
)}
happyReduce_70 = happySpecReduce_2 19# happyReduction_70
happyReduction_70 happy_x_2
happy_x_1
= case happyOut23 happy_x_2 of { happy_var_2 ->
happyIn23
(B happy_var_2
)}
happyReduce_71 = happyMonadReduce 4# 19# happyReduction_71
happyReduction_71 (happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOut24 happy_x_2 of { happy_var_2 ->
case happyOut23 happy_x_4 of { happy_var_4 ->
( getSig >>= \s -> if (isRelInSig happy_var_2 s)
then return (Diam happy_var_2 happy_var_4)
else (error $ (show happy_var_2) ++ " not in Sig as Relation"))}}
) (\r -> happyReturn (happyIn23 r))
happyReduce_72 = happyMonadReduce 4# 19# happyReduction_72
happyReduction_72 (happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOut24 happy_x_2 of { happy_var_2 ->
case happyOut23 happy_x_4 of { happy_var_4 ->
( getSig >>= \s -> if (isRelInSig happy_var_2 s)
then return (Box happy_var_2 happy_var_4)
else (error $ (show happy_var_2) ++ " not in Sig as Relation"))}}
) (\r -> happyReturn (happyIn23 r))
happyReduce_73 = happySpecReduce_3 19# happyReduction_73
happyReduction_73 happy_x_3
happy_x_2
happy_x_1
= case happyOut23 happy_x_1 of { happy_var_1 ->
case happyOut23 happy_x_3 of { happy_var_3 ->
happyIn23
(happy_var_1 :<-->: happy_var_3
)}}
happyReduce_74 = happySpecReduce_3 19# happyReduction_74
happyReduction_74 happy_x_3
happy_x_2
happy_x_1
= case happyOut23 happy_x_1 of { happy_var_1 ->
case happyOut23 happy_x_3 of { happy_var_3 ->
happyIn23
(happy_var_1 :-->: happy_var_3
)}}
happyReduce_75 = happySpecReduce_2 19# happyReduction_75
happyReduction_75 happy_x_2
happy_x_1
= case happyOut23 happy_x_2 of { happy_var_2 ->
happyIn23
(Neg happy_var_2
)}
happyReduce_76 = happySpecReduce_3 19# happyReduction_76
happyReduction_76 happy_x_3
happy_x_2
happy_x_1
= case happyOut23 happy_x_1 of { happy_var_1 ->
case happyOut23 happy_x_3 of { happy_var_3 ->
happyIn23
(happy_var_1 :&: happy_var_3
)}}
happyReduce_77 = happySpecReduce_3 19# happyReduction_77
happyReduction_77 happy_x_3
happy_x_2
happy_x_1
= case happyOut23 happy_x_1 of { happy_var_1 ->
case happyOut23 happy_x_3 of { happy_var_3 ->
happyIn23
(happy_var_1 :|: happy_var_3
)}}
happyReduce_78 = happyMonadReduce 3# 19# happyReduction_78
happyReduction_78 (happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOutTok happy_x_1 of { ((TokenNom happy_var_1 , _)) ->
case happyOut23 happy_x_3 of { happy_var_3 ->
( get >>= \s -> if (isAutomatic s)
then return (At happy_var_1 happy_var_3)
else if (isNomInSig happy_var_1 (pSig s))
then return (At happy_var_1 happy_var_3)
else (error $ (show happy_var_1) ++ " not defined as Nom in Sig"))}}
) (\r -> happyReturn (happyIn23 r))
happyReduce_79 = happyMonadReduce 3# 19# happyReduction_79
happyReduction_79 (happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOut25 happy_x_1 of { happy_var_1 ->
case happyOut23 happy_x_3 of { happy_var_3 ->
( getSig >>= \s -> if (isNomInSig happy_var_1 s)
then return (At happy_var_1 happy_var_3)
else (error $ (show happy_var_1) ++ " not defined as Nom in Sig"))}}
) (\r -> happyReturn (happyIn23 r))
happyReduce_80 = happyMonadReduce 5# 19# happyReduction_80
happyReduction_80 (happy_x_5 `HappyStk`
happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOutTok happy_x_3 of { ((TokenNom happy_var_3 , _)) ->
case happyOut23 happy_x_4 of { happy_var_4 ->
( get >>= \s -> if (isAutomatic s)
then return (Formula.Down happy_var_3 happy_var_4)
else if (isNomInSig happy_var_3 (pSig s))
then return (Formula.Down happy_var_3 happy_var_4)
else (error $ (show happy_var_3) ++ " not defined as Nom in Sig"))}}
) (\r -> happyReturn (happyIn23 r))
happyReduce_81 = happyMonadReduce 5# 19# happyReduction_81
happyReduction_81 (happy_x_5 `HappyStk`
happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOut25 happy_x_3 of { happy_var_3 ->
case happyOut23 happy_x_4 of { happy_var_4 ->
( getSig >>= \s -> if (isNomInSig happy_var_3 s)
then return (Formula.Down happy_var_3 happy_var_4)
else (error $ (show happy_var_3) ++ " not defined as Nom in Sig"))}}
) (\r -> happyReturn (happyIn23 r))
happyReduce_82 = happyMonadReduce 4# 19# happyReduction_82
happyReduction_82 (happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOutTok happy_x_2 of { ((TokenNom happy_var_2 , _)) ->
case happyOut23 happy_x_4 of { happy_var_4 ->
( get >>= \s -> if (isAutomatic s)
then return (Formula.Down happy_var_2 happy_var_4)
else if (isNomInSig happy_var_2 (pSig s))
then return (Formula.Down happy_var_2 happy_var_4)
else (error $ (show happy_var_2) ++ " not defined as Nom in Sig"))}}
) (\r -> happyReturn (happyIn23 r))
happyReduce_83 = happyMonadReduce 4# 19# happyReduction_83
happyReduction_83 (happy_x_4 `HappyStk`
happy_x_3 `HappyStk`
happy_x_2 `HappyStk`
happy_x_1 `HappyStk`
happyRest) tk
= happyThen (case happyOut25 happy_x_2 of { happy_var_2 ->
case happyOut23 happy_x_4 of { happy_var_4 ->
( getSig >>= \s -> if (isNomInSig happy_var_2 s)
then return (Formula.Down happy_var_2 happy_var_4)
else (error $ (show happy_var_2) ++ " not defined as Nom in Sig"))}}
) (\r -> happyReturn (happyIn23 r))
happyReduce_84 = happySpecReduce_3 19# happyReduction_84
happyReduction_84 happy_x_3
happy_x_2
happy_x_1
= case happyOut23 happy_x_2 of { happy_var_2 ->
happyIn23
(happy_var_2
)}
happyReduce_85 = happySpecReduce_1 20# happyReduction_85
happyReduction_85 happy_x_1
= case happyOutTok happy_x_1 of { ((TokenProp happy_var_1 , _)) ->
happyIn24
(let (PropSymbol l) = happy_var_1 in RelSymbol l
)}
happyReduce_86 = happySpecReduce_1 20# happyReduction_86
happyReduction_86 happy_x_1
= case happyOutTok happy_x_1 of { ((TokenNom happy_var_1 , _)) ->
happyIn24
(let (NomSymbol l) = happy_var_1 in RelSymbol l
)}
happyReduce_87 = happySpecReduce_1 20# happyReduction_87
happyReduction_87 happy_x_1
= case happyOutTok happy_x_1 of { ((TokenVariable happy_var_1, _)) ->
happyIn24
(RelSymbol happy_var_1
)}
happyReduce_88 = happySpecReduce_1 21# happyReduction_88
happyReduction_88 happy_x_1
= case happyOutTok happy_x_1 of { ((TokenProp happy_var_1 , _)) ->
happyIn25
(let (PropSymbol l) = happy_var_1 in NomSymbol l
)}
happyReduce_89 = happySpecReduce_1 21# happyReduction_89
happyReduction_89 happy_x_1
= case happyOutTok happy_x_1 of { ((TokenVariable happy_var_1, _)) ->
happyIn25
(NomSymbol happy_var_1
)}
happyNewToken action sts stk [] =
happyDoAction 56# notHappyAtAll action sts stk []
happyNewToken action sts stk (tk:tks) =
let cont i = happyDoAction i tk action sts stk tks in
case tk of {
(TokenSignature, _) -> cont 1#;
(TokenPropositions, _) -> cont 2#;
(TokenNominals , _) -> cont 3#;
(TokenRelations, _) -> cont 4#;
(TokenReflexive, _) -> cont 5#;
(TokenUniversal, _) -> cont 6#;
(TokenDifference, _) -> cont 7#;
(TokenTransitive, _) -> cont 8#;
(TokenSymmetric, _) -> cont 9#;
(TokenFunctional, _) -> cont 10#;
(TokenInverseOf, _) -> cont 11#;
(TokenSubsetOf, _) -> cont 12#;
(TokenEquals, _) -> cont 13#;
(TokenTClosureOf ,_) -> cont 14#;
(TokenTRClosureOf, _) -> cont 15#;
(TokenAutomatic, _) -> cont 16#;
(TokenProverParameters, _) -> cont 17#;
(TokenProver, _) -> cont 18#;
(TokenTheory, _) -> cont 19#;
(TokenQuery, _) -> cont 20#;
(TokenValid, _) -> cont 21#;
(TokenSatisfiable, _) -> cont 22#;
(TokenRetrieve, _) -> cont 23#;
(TokenVariable happy_dollar_dollar, _) -> cont 24#;
(TokenLabel happy_dollar_dollar, _) -> cont 25#;
(TokenFile happy_dollar_dollar, _) -> cont 26#;
(TokenColon , _) -> cont 27#;
(TokenDown , _) -> cont 28#;
(TokenProp happy_dollar_dollar , _) -> cont 29#;
(TokenNom happy_dollar_dollar , _) -> cont 30#;
(TokenTrue , _) -> cont 31#;
(TokenFalse , _) -> cont 32#;
(TokenNeg , _) -> cont 33#;
(TokenAnd , _) -> cont 34#;
(TokenOr , _) -> cont 35#;
(TokenDimp , _) -> cont 36#;
(TokenImp , _) -> cont 37#;
(TokenBox happy_dollar_dollar , _) -> cont 38#;
(TokenUBox , _) -> cont 39#;
(TokenDBox , _) -> cont 40#;
(TokenDia happy_dollar_dollar , _) -> cont 41#;
(TokenUDia , _) -> cont 42#;
(TokenDDia , _) -> cont 43#;
(TokenOB , _) -> cont 44#;
(TokenCB , _) -> cont 45#;
(TokenSC , _) -> cont 46#;
(TokenDot , _) -> cont 47#;
(TokenComma , _) -> cont 48#;
(TokenOC , _) -> cont 49#;
(TokenCC , _) -> cont 50#;
(TokenODia , _) -> cont 51#;
(TokenCDia , _) -> cont 52#;
(TokenOBox , _) -> cont 53#;
(TokenCBox , _) -> cont 54#;
(TokenEqual , _) -> cont 55#;
_ -> happyError' (tk:tks)
}
happyError_ tk tks = happyError' (tk:tks)
happyThen :: () => State ParseState a -> (a -> State ParseState b) -> State ParseState b
happyThen = (>>=)
happyReturn :: () => a -> State ParseState a
happyReturn = (return)
happyThen1 m k tks = (>>=) m (\a -> k a tks)
happyReturn1 :: () => a -> b -> State ParseState a
happyReturn1 = \a tks -> (return) a
happyError' :: () => [((Token, FilePos))] -> State ParseState a
happyError' = happyError
parse tks = happySomeParser where
happySomeParser = happyThen (happyParse 0# tks) (\x -> happyReturn (happyOut4 x))
happySeq = happyDontSeq
data ParseOutput = PO{relations :: [RelInfo],
provers :: [ProverInfo],
theory :: [Formula NomSymbol PropSymbol RelSymbol],
tasks :: [InferenceTask]
} deriving (Show)
type RelInfo = (String,[RelProperty])
type ProverInfo = (String, [(String,String)])
type InferenceTask = (QueryType,
Maybe String,
[Formula NomSymbol PropSymbol RelSymbol])
data RelProperty = Reflexive |
Symmetric |
Transitive |
Functional |
Universal |
Difference |
InverseOf String |
SubsetOf [String] |
Equals [String] |
TClosureOf String |
TRClosureOf String
deriving (Eq, Show, Ord)
data QueryType = Valid | Satisfiable | Retrieve
deriving (Eq, Show)
data SignatureType = NotAutomatic | Automatic | NotSet deriving (Eq)
type ParseState = (StringSignature,SignatureType)
initParseState = (emptySignature, NotSet)
pSig = fst
pType = snd
isAutomatic s = (pType s) == Automatic
getSig :: State ParseState (StringSignature)
getSig = do
state <- get
return (fst state)
putSig :: StringSignature -> State ParseState ()
putSig s = do
state <- get
put (s,snd state)
getType :: State ParseState (SignatureType)
getType = do
state <- get
return (snd state)
putType :: SignatureType -> State ParseState ()
putType t = do
state <- get
put (fst state, t)
addPToSig l s =
if (isNomInSig (NomSymbol l) s)
then error $ l ++ " already declared as Nom"
else if (isRelInSig (RelSymbol l) s)
then error $ l ++ " already declared as Rel"
else addPropToSig (PropSymbol l) s
addNToSig l s =
if (isPropInSig (PropSymbol l) s)
then error $ l ++ " already declared as Prop"
else if (isRelInSig (RelSymbol l) s)
then error $ l ++ " already declared as Rel"
else addNomToSig (NomSymbol l) s
addRToSig l s =
if (isPropInSig (PropSymbol l) s)
then error $ l ++ " already declared as Prop"
else if (isNomInSig (NomSymbol l) s)
then error $ l ++ " already declared as Nom"
else addRelToSig (RelSymbol l) s
happyError :: [(Token, FilePos)] -> a
happyError ((_, fp):_) = error ("Parse error near line " ++
(show $ line fp) ++
", col. " ++
(show $ col fp))
data Happy_IntList = HappyCons Happy_GHC_Exts.Int# Happy_IntList
infixr 9 `HappyStk`
data HappyStk a = HappyStk a (HappyStk a)
happyParse start_state = happyNewToken start_state notHappyAtAll notHappyAtAll
happyAccept 0# tk st sts (_ `HappyStk` ans `HappyStk` _) =
happyReturn1 ans
happyAccept j tk st sts (HappyStk ans _) =
(happyTcHack j (happyTcHack st)) (happyReturn1 ans)
happyDoAction i tk st
=
case action of
0# ->
happyFail i tk st
1# ->
happyAccept i tk st
n | (n Happy_GHC_Exts.<# (0# :: Happy_GHC_Exts.Int#)) ->
(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 ->
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
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#
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
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)
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
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
happyGoto nt j tk st =
happyDoAction j tk new_state
where off = indexShortOffAddr happyGotoOffsets st
off_i = (off Happy_GHC_Exts.+# nt)
new_state = indexShortOffAddr happyTable off_i
happyFail 0# tk old_st _ stk =
happyError_ tk
happyFail i tk (action) sts stk =
happyDoAction 0# tk action sts ( (Happy_GHC_Exts.unsafeCoerce# (Happy_GHC_Exts.I# (i))) `HappyStk` stk)
notHappyAtAll = error "Internal Happy error\n"
happyTcHack :: Happy_GHC_Exts.Int# -> a -> a
happyTcHack x y = y
happyDoSeq, happyDontSeq :: a -> b -> b
happyDoSeq a b = a `seq` b
happyDontSeq a b = b