Complete repo is on https://github.com/matdsoupe/analytic-tableaux
I’m trying to build an analytic tableaux parser and prover, hwoever I got stuck with thew parser (I’m usign parsec).
This is my parser:
{-# LANGUAGE OverloadedStrings #-}
module Language.Tableaux.Parser where
import Control.Applicative ((*>), (<*))
import Data.Text (Text)
import qualified Data.Text as Text
import Text.Parsec
type Parser = Parsec Text ()
data InputMetadata = InputMetadata
{ metadataLine :: Int
, metadataColumn :: Int
}
deriving (Show)
data Operator
= Not Char
| And Char
| Or Char
| Implies Char
| Equiv Char
| Prove Char
deriving (Show)
data Sign = T | F deriving (Show, Enum)
data TableauxInput
= TableauxAtom InputMetadata Text
| TableauxSign InputMetadata Sign
| TableauxOperator InputMetadata Operator
| TableauxWff InputMetadata [TableauxInput]
deriving (Show)
parseNot :: Parser Operator
parseNot = Not <$> oneOf "¬~!"
parseAnd :: Parser Operator
parseAnd = And <$> oneOf "∧&·"
parseOr :: Parser Operator
parseOr = Or <$> oneOf "∨+∥"
parseImplies :: Parser Operator
parseImplies = Implies <$> oneOf "⇒→⊃"
parseEquiv :: Parser Operator
parseEquiv = Equiv <$> oneOf "⇔≡↔"
parseProve :: Parser Operator
parseProve = Prove <$> char '⊢'
getInputMetadata :: Parser InputMetadata
getInputMetadata = do
position <- statePos <$> getParserState
return $
InputMetadata
{ metadataLine = sourceLine position
, metadataColumn = sourceColumn position
}
parseAtom :: Parser TableauxInput
parseAtom = do
meta <- getInputMetadata
first <- lower
rest <- many (lower <|> digit)
return $ TableauxAtom meta (Text.pack (first : rest))
parseSign :: Parser TableauxInput
parseSign = do
meta <- getInputMetadata
sign <- upper
case sign of
'T' -> return $ TableauxSign meta T
'F' -> return $ TableauxSign meta F
parseOperator :: Parser TableauxInput
parseOperator = do
meta <- getInputMetadata
op <- parseNot <|> parseAnd <|> parseOr <|> parseImplies <|> parseEquiv <|> parseProve
return $ TableauxOperator meta op
parseWff :: Parser TableauxInput
parseWff = do
meta <- getInputMetadata
char '('
scope <- spaces *> many parseTableaux <* spaces
char ')'
return $ TableauxWff meta scope
parseTableaux :: Parser TableauxInput
parseTableaux = parseAtom <|> parseSign <|> parseOperator <|> parseWff
However, when I try to parse any WFF ("(p → q)" for example), i get this parser error:
Left "<stdio>" (line 1, column 4):
unexpected "\8594"
expecting space or ")"
What I’m doing wrongly?