module Theory.Text.Parser.Token (
symbol
, symbol_
, dot
, comma
, colon
, natural
, naturalSubscript
, formalComment
, identifier
, indexedIdentifier
, freshName
, pubName
, sortedLVar
, lvar
, msgvar
, nodevar
, opExp
, opMult
, opEqual
, opLess
, opAt
, opForall
, opExists
, opImplies
, opLEquiv
, opLAnd
, opLOr
, opLNot
, opLFalse
, opLTrue
, opRequires
, opChain
, equalSign
, opSharp
, opBang
, opSlash
, opMinus
, opPlus
, opLeftarrow
, opRightarrow
, opLongleftarrow
, opLongrightarrow
, braced
, parens
, angled
, brackets
, singleQuoted
, doubleQuoted
, commaSep
, commaSep1
, list
, Parser
, parseFile
, parseString
) where
import Prelude hiding (id, (.))
import Data.Foldable (asum)
import Data.List (foldl')
import Control.Applicative hiding (empty, many, optional)
import Control.Category
import Control.Monad
import Text.Parsec hiding ((<|>))
import qualified Text.Parsec.Token as T
import Theory
type Parser a = Parsec String MaudeSig a
spthy :: T.TokenParser MaudeSig
spthy =
T.makeTokenParser spthyStyle
where
spthyStyle = T.LanguageDef
{ T.commentStart = "/*"
, T.commentEnd = "*/"
, T.commentLine = "//"
, T.nestedComments = True
, T.identStart = alphaNum
, T.identLetter = alphaNum <|> oneOf "_"
, T.reservedNames = ["in","let","rule"]
, T.opStart = oneOf ":!$%&*+./<=>?@\\^|-"
, T.opLetter = oneOf ":!$%&*+./<=>?@\\^|-"
, T.reservedOpNames= []
, T.caseSensitive = True
}
parseFile :: Parser a -> FilePath -> IO a
parseFile parser inFile = do
inp <- readFile inFile
case parseString inFile parser inp of
Right x -> return x
Left err -> error $ show err
parseString :: FilePath
-> Parser a
-> String
-> Either ParseError a
parseString srcDesc parser =
runParser (T.whiteSpace spthy *> parser) minimalMaudeSig srcDesc
symbol :: String -> Parser String
symbol sym = try (T.symbol spthy sym) <?> ("\"" ++ sym ++ "\"")
symbol_ :: String -> Parser ()
symbol_ = void . symbol
braced :: Parser a -> Parser a
braced = T.braces spthy
brackets :: Parser a -> Parser a
brackets = T.brackets spthy
parens :: Parser a -> Parser a
parens = T.parens spthy
angled :: Parser a -> Parser a
angled = T.angles spthy
singleQuoted :: Parser a -> Parser a
singleQuoted = between (symbol "'") (symbol "'")
doubleQuoted :: Parser a -> Parser a
doubleQuoted = between (symbol "\"") (symbol "\"")
dot :: Parser ()
dot = void $ T.dot spthy
comma :: Parser ()
comma = void $ T.comma spthy
colon :: Parser ()
colon = void $ T.colon spthy
natural :: Parser Integer
natural = T.natural spthy
naturalSubscript :: Parser Integer
naturalSubscript = T.lexeme spthy $ do
digits <- many1 (oneOf "₀₁₂₃₄₅₆₇₈₉")
let n = foldl' (\x d -> 10*x + subscriptDigitToInteger d) 0 digits
seq n (return n)
where
subscriptDigitToInteger d = toInteger $ fromEnum d fromEnum '₀'
commaSep :: Parser a -> Parser [a]
commaSep = T.commaSep spthy
commaSep1 :: Parser a -> Parser [a]
commaSep1 = T.commaSep1 spthy
list :: Parser a -> Parser [a]
list = brackets . commaSep
formalComment :: Parser (String, String)
formalComment = T.lexeme spthy $ do
header <- try (many1 letter <* string "{*")
body <- many bodyChar <* string "*}"
return (header, body)
where
bodyChar = try $ do
c <- anyChar
case c of
'\\' -> char '\\' <|> char '*'
'*' -> mzero
_ -> return c
identifier :: Parser String
identifier = T.identifier spthy
indexedIdentifier :: Parser (String, Integer)
indexedIdentifier = do
(,) <$> identifier
<*> option 0 (try (dot *> (fromIntegral <$> natural)))
sortedLVar :: [LSort] -> Parser LVar
sortedLVar ss =
asum $ map (try . mkSuffixParser) ss ++ map mkPrefixParser ss
where
mkSuffixParser s = do
(n, i) <- indexedIdentifier <* colon
symbol_ (sortSuffix s)
return (LVar n s i)
mkPrefixParser s = do
case s of
LSortMsg -> pure ()
LSortPub -> void $ char '$'
LSortFresh -> void $ char '~'
LSortNode -> void $ char '#'
(n, i) <- indexedIdentifier
return (LVar n s i)
lvar :: Parser LVar
lvar = sortedLVar [minBound..]
msgvar :: Parser LVar
msgvar = sortedLVar [LSortFresh, LSortPub, LSortMsg]
nodevar :: Parser NodeId
nodevar = asum
[ sortedLVar [LSortNode]
, (\(n, i) -> LVar n LSortNode i) <$> indexedIdentifier ]
<?> "timepoint variable"
freshName :: Parser String
freshName = try (symbol "~" *> singleQuoted identifier)
pubName :: Parser String
pubName = singleQuoted identifier
opExp :: Parser ()
opExp = symbol_ "^"
opMult :: Parser ()
opMult = symbol_ "*"
opPlus :: Parser ()
opPlus = symbol_ "+"
opLess :: Parser ()
opLess = symbol_ "<"
opAt :: Parser ()
opAt = symbol_ "@"
opEqual :: Parser ()
opEqual = symbol_ "="
opForall :: Parser ()
opForall = symbol_ "All" <|> symbol_ "∀"
opExists :: Parser ()
opExists = symbol_ "Ex" <|> symbol_ "∃"
opImplies :: Parser ()
opImplies = symbol_ "==>" <|> symbol_ "⇒"
opLEquiv :: Parser ()
opLEquiv = symbol_ "<=>" <|> symbol_ "⇔"
opLAnd :: Parser ()
opLAnd = symbol_ "&" <|> symbol_ "∧"
opLOr :: Parser ()
opLOr = symbol_ "|" <|> symbol_ "∨"
opLNot :: Parser ()
opLNot = symbol_ "¬" <|> symbol_ "not"
opLFalse :: Parser ()
opLFalse = symbol_ "⊥" <|> T.reserved spthy "F"
opLTrue :: Parser ()
opLTrue = symbol_ "⊤" <|> T.reserved spthy "T"
opRequires :: Parser PremIdx
opRequires = (PremIdx . fromIntegral) <$> (symbol "▶" *> naturalSubscript)
opChain :: Parser ()
opChain = symbol_ "~~>"
equalSign :: Parser ()
equalSign = symbol_ "="
opSlash :: Parser ()
opSlash = symbol_ "/"
opBang :: Parser ()
opBang = symbol_ "!"
opSharp :: Parser ()
opSharp = symbol_ "#"
opMinus :: Parser ()
opMinus = symbol_ "-"
opLeftarrow :: Parser ()
opLeftarrow = symbol_ "<-"
opRightarrow :: Parser ()
opRightarrow = symbol_ "->"
opLongleftarrow :: Parser ()
opLongleftarrow = symbol_ "<--"
opLongrightarrow :: Parser ()
opLongrightarrow = symbol_ "-->"