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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
module XFD.SMTLib.RDParser where
import XFD.Parser
import XFD.SMTLib.Scanner
import XFD.SMTLib.Types
import XFD.SMTLib.Build
parse :: String -> Either ParseError CmdResponse
parse s = case parseCmdResult $ scan s of
Left e -> Left e
Right ([], x) -> Right x
Right _ -> Left "incomplete parse"
parseCmdResult :: Parser Token CmdResponse
parseCmdResult = parseCmdCheckSatResponse
<|> parseCmdGetValueResponse
<|> parseCmdGenResponse
<* terminal EOF
parseCmdCheckSatResponse :: Parser Token CmdResponse
parseCmdCheckSatResponse [] = eof []
parseCmdCheckSatResponse (t:ts) = case t of
KW_sat -> yield (CmdCheckSatResponse Sat) ts
KW_unsat -> yield (CmdCheckSatResponse Unsat) ts
KW_unknown -> yield (CmdCheckSatResponse Unknown) ts
_ -> unexpected t ts
parseCmdGetValueResponse :: Parser Token CmdResponse
parseCmdGetValueResponse [] = eof []
parseCmdGetValueResponse (t:ts) = case t of
LParen -> CmdGetValueResponse <$> parseGetValueResponse <* terminal RParen $ ts
_ -> unexpected t ts
parseGetValueResponse :: Parser Token GetValueResponse
parseGetValueResponse = some parseValuePair
parseValuePair :: Parser Token ValuationPair
parseValuePair = terminal LParen *> liftP2 ValuationPair parseTerm parseTerm <* terminal RParen
parseTerm :: Parser Token Term
parseTerm [] = eof []
parseTerm (t:ts) = case t of
Number i -> yield (termSpecConstNum i) ts
Id name -> yield (termQIdent name) ts
LParen -> terminal OP_Minus *> (termQIdentT "-" <$> (some parseTerm)) <* terminal RParen $ ts
_ -> unexpected t ts
parseCmdGenResponse :: Parser Token CmdResponse
parseCmdGenResponse [] = eof []
parseCmdGenResponse (t:ts) = case t of
LParen -> CmdGenResponse <$> parseErrorResponse <* terminal RParen $ ts
_ -> unexpected t ts
parseErrorResponse :: Parser Token GenResponse
parseErrorResponse [] = eof []
parseErrorResponse (t:ts) = case t of
KW_error -> Error <$> parseString $ ts
_ -> unexpected t ts
parseString :: Parser Token String
parseString [] = eof []
parseString (t:ts) = case t of
Str string -> yield string ts
_ -> unexpected t ts
|