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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
module XFD.SMTLib.Scanner (
scan, Token(..)
) where
import ReadNumeric
import Char
import List (split)
data Token
= Id String
| Number Int
| Str String
| LParen
| RParen
| OP_Minus
| KW_sat
| KW_unsat
| KW_unknown
| KW_model
| KW_defineFun
| KW_error
| EOF
keywords :: [(String, Token)]
keywords =
[ ("sat" , KW_sat)
, ("unsat" , KW_unsat)
, ("unknown" , KW_unknown)
, ("model" , KW_model)
, ("define-fun" , KW_defineFun)
, ("error" , KW_error)
]
specialOrIdent :: String -> Token
specialOrIdent s = maybe (Id s) id (lookup s keywords)
scan :: String -> [Token]
scan str = case str of
"" -> [EOF]
('(':s) -> LParen : scan s
(')':s) -> RParen : scan s
('-':s) -> OP_Minus : scan s
('"':s) -> scanString s
cs -> scan' cs
where
scan' :: String -> [Token]
scan' "" = []
scan' x@(c:cs) | isDigit c = scanNum x
| isSymbol c = scanSpecialOrIdent x
| otherwise = scan cs
isNumber :: Char -> Bool
isNumber c = isDigit c || c == '-'
isSymbol :: Char -> Bool
isSymbol c = isAlpha c || c `elem` symbols
symbols :: [Char]
symbols = ['-', '_', '!']
scanSpecialOrIdent :: String -> [Token]
scanSpecialOrIdent xs =
let (ident, rest) = span (\c -> (isAlphaNum c) || (c `elem` symbols)) xs
in specialOrIdent ident : scan rest
scanNum :: String -> [Token]
scanNum xs =
let v = readInt xs
in case v of
Just (num, rest) -> Number num : scan rest
Nothing -> error "SMTLib.Scanner, scanNum: should not be possible"
scanString :: String -> [Token]
scanString xs =
let [string, rest] = split (=='"') xs
in Str string : scan rest
|