-
Notifications
You must be signed in to change notification settings - Fork 1
/
Parser.hs
47 lines (40 loc) · 1.37 KB
/
Parser.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
module ProveEverywhere.Parser (parsePrompt) where
import Control.Applicative
import Data.Text (Text)
import qualified Data.Text as T
import Text.Parser.Char
import Text.Parser.Combinators
import Text.Parser.Token
import Text.Parsec (parse, ParseError)
import Text.Parsec.Text (Parser)
import ProveEverywhere.Types
parsePrompt :: Text -> Either ParseError CoqtopState
parsePrompt = parse prompt "prompt"
-- | Prompt parser
prompt :: Parser CoqtopState
prompt = do
skipMany $ noneOf "<" -- this may ignore important error messages
between (symbol "<prompt>") (symbol "</prompt>") internal
internal :: Parser CoqtopState
internal = do
current <- token theorem
_ <- symbol "<"
wholeState <- natural
stack <- token theoremStack
theoremState <- natural
_ <- symbol "<"
return CoqtopState
{ promptCurrentTheorem = current
, promptWholeStateNumber = wholeState
, promptTheoremStack = stack
, promptTheoremStateNumber = theoremState
}
-- | Parser for theorem name
theorem :: Parser Text
theorem = T.pack <$> some (alphaNum <|> oneOf "_'")
-- | Parses |theorem1|theorem2| ... |theoremn| and return list of theorem names
theoremStack :: Parser [Text]
theoremStack = between (char '|') (char '|') $ sepBy' theorem (char '|')
where
sepBy' p sep = sepBy1' p sep <|> pure []
sepBy1' p sep = (:) <$> p <*> many (try (sep *> p))