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
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
'# Parser Combinators
'Basic combinator-based parser in Dex (as opposed to of Dex).
'## Utilities unrelated to parsing
def from_ordinal_exc(n|Ix, i:Nat) -> {Except} n =
if (0 <= i) && (i < size n)
then unsafe_from_ordinal i
else throw()
# TODO: allow this to happen in-place
# TODO: if it takes too long to make that possible, start with a bounded version
def push(ref:Ref h (List a), x:a) -> {State h} () given (h, a|Data) =
l = get ref
ref := l <> AsList _ [x]
def index_list(l:List a, i:Nat) -> {Except} a given (a|Data) =
AsList(n, xs) = l
xs[from_ordinal_exc _ i]
'## The Parser type
struct ParserHandle(h:Heap) =
input: String
offset: Ref h Nat
enum Parser(a:Type) =
MkParser((given(h:Heap), ParserHandle h )-> {Except, State h} a)
def parse(handle:ParserHandle h, parser:Parser a) -> {Except, State h} a given (a, h) =
MkParser f = parser
f handle
def run_parser_partial(s:String, parser:Parser a) -> Maybe a given (a) =
MkParser f = parser
with_state 0 \pos.
catch $ \.
f ParserHandle(s, pos)
'## Primitive combinators
def p_char(c:Char) -> Parser () = MkParser \h.
i = get h.offset
c' = index_list h.input i
assert (c == c')
h.offset := i + 1
def p_eof() ->> Parser () = MkParser \h.
assert $ get h.offset >= list_length h.input
def (<|>)(p1:Parser a, p2:Parser a) -> Parser a given (a) = MkParser \h.
curPos = get h.offset
case catch \. parse h p1 of
Nothing ->
assert $ curPos == get h.offset
parse h p2
Just ans -> ans
def returnP(x:a) -> Parser a given (a) = MkParser \_. x
def run_parser(s:String, parser:Parser a) -> Maybe a given (a) =
run_parser_partial s $ MkParser \h.
ans = parse h parser
_ = parse h p_eof
ans
def parse_any() ->> Parser Char = MkParser \h.
i = get h.offset
c' = index_list h.input i
h.offset := i + 1
c'
def parse_anything_but(c:Char) -> Parser Char =
MkParser \h.
i = get h.offset
c' = index_list h.input i
assert (c /= c')
h.offset := i + 1
c'
def try(parser:Parser a) -> Parser a given (a) = MkParser \h.
savedPos = get h.offset
ans = catch \. parse h parser
case ans of
Nothing ->
h.offset := savedPos
throw()
Just x -> x
'## Derived combinators
def parse_digit() ->> Parser Int = try $ MkParser \h.
c = parse h $ parse_any
i = w8_to_i c - 48
assert $ 0 <= i && i < 10
i
def optional(p:Parser a) -> Parser (Maybe a) given (a) =
(MkParser \h. Just (parse h p)) <|> returnP Nothing
def parse_many(parser:Parser a) -> Parser (List a) given (a|Data) = MkParser \h.
yield_state (AsList _ []) \results.
iter \_.
maybeVal = parse h $ optional parser
case maybeVal of
Nothing -> Done ()
Just x ->
push results x
Continue
def parse_some(parser:Parser a) -> Parser (List a) given (a|Data) =
MkParser \h.
c = parse h parser
rest = parse h $ parse_many parser
AsList(_, [c]) <> rest
def parse_unsigned_int() ->> Parser Int = MkParser \h.
AsList(_, digits) = parse h $ parse_many parse_digit
yield_state 0 \ref.
for i. ref := 10 * get ref + digits[i]
def parse_int() ->> Parser Int = MkParser \h.
negSign = parse h $ optional $ p_char '-'
x = parse h $ parse_unsigned_int
case negSign of
Nothing -> x
Just () -> (-1) * x
def bracketed(l:Parser (), r:Parser (), body:Parser a) -> Parser a given (a) =
MkParser \h.
_ = parse h l
ans = parse h body
_ = parse h r
ans
def parens(parser:Parser a) -> Parser a given (a) =
bracketed (p_char '(') (p_char ')') parser
def split(space:Char, s:String) -> List String =
def trailing_spaces(space:Parser (), body:Parser a) -> Parser a given (a) =
MkParser \h.
ans = parse h body
_ = parse h $ parse_many space
ans
split_parser = MkParser \h.
_ = parse h $ parse_many (p_char space)
parse h $ parse_many (trailing_spaces (p_char space) (parse_some (parse_anything_but space)))
case run_parser s split_parser of
Just l -> l
Nothing -> AsList _ []
|
