blob: 2525ec0af68d9fb462b0ce9c48f0ad869344099c (
plain)
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
|
'Utilities unrelated to parsing
def from_ordinal_exc (n:Type) [Ix n] (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 {h a} (ref:Ref h (List a)) (x:a) : {State h} Unit =
l = get ref
ref := l <> AsList _ [x]
def index_list {a} (l:List a) (i:Nat) : {Except} a =
(AsList n xs) = l
xs.(from_ordinal_exc _ i)
'The Parser type
def ParserHandle (h:Type) : Type = (String & Ref h Nat)
data Parser a:Type =
MkParser ((h:Type) ?-> ParserHandle h -> {Except, State h} a)
def parse {a h} (handle:ParserHandle h) (parser:Parser a) : {Except, State h} a =
(MkParser f) = parser
f handle
def run_parser_partial {a} (s:String) (parser:Parser a) : Maybe a =
(MkParser f) = parser
with_state 0 \pos.
catch $ do
f (s, pos)
'Primitive combinators
def p_char (c:Char) : Parser Unit = MkParser \(s, posRef).
i = get posRef
c' = index_list s i
assert (c == c')
posRef := i + 1
def p_eof : Parser Unit = MkParser \(s, posRef).
assert $ get posRef >= list_length s
def (<|>) {a} (p1:Parser a) (p2:Parser a) : Parser a = MkParser \h.
(s, posRef) = h
curPos = get posRef
case catch do parse h p1 of
Nothing ->
assert $ curPos == get posRef
parse h p2
Just ans -> ans
def returnP {a} (x:a) : Parser a = MkParser \_. x
def run_parser {a} (s:String) (parser:Parser a) : Maybe a =
run_parser_partial s $ MkParser \h.
ans = parse h parser
_ = parse h p_eof
ans
def parse_any : Parser Char = MkParser \h.
(s, posRef) = h
i = get posRef
c' = index_list s i
posRef := i + 1
c'
def try {a} (parser:Parser a) : Parser a = MkParser \h.
(s, posRef) = h
savedPos = get posRef
ans = catch do parse h parser
case ans of
Nothing ->
posRef := 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 {a} (p:Parser a) : Parser (Maybe a) =
(MkParser \h. Just (parse h p)) <|> returnP Nothing
def parse_many {a} (parser:Parser a) : Parser (List a) = 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_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 {a} (l:Parser Unit) (r:Parser Unit) (body:Parser a) : Parser a =
MkParser \h.
_ = parse h l
ans = parse h body
_ = parse h r
ans
def parens {a} (parser:Parser a) : Parser a =
bracketed (p_char '(') (p_char ')') parser
|
