git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4154 from msmorgan/parser-refactor
26922d4Ahmad Salim Al-Sibahi
libs/contrib/Control/Delayed.idrnew file+26
compare with master
unifiedsplit
@@ -0,0 +1,26 @@
1+||| Utilities functions for contitionally delaying values.
2+module Control.Delayed
3+
4+%default total
5+
6+||| Type-level function for a conditionally delayed type (`Lazy` or `Inf`).
7+public export
8+delayed : DelayReason -> Bool -> Type -> Type
9+delayed r False a = a
10+delayed r True a = Delayed r a
11+
12+||| Type-level function for a conditionally infinite type.
13+public export
14+inf : Bool -> Type -> Type
15+inf = delayed Infinite
16+
17+||| Type-level function for a conditionally lazy type.
18+public export
19+lazy : Bool -> Type -> Type
20+lazy = delayed LazyValue
21+
22+||| Conditionally delay a value.
23+export
24+delay : (d : Bool) -> a -> delayed r d a
25+delay False x = x
26+delay True x = Delay x
libs/contrib/Data/Bool/Extra.idrnew file+32
@@ -0,0 +1,32 @@
1+module Data.Bool.Extra
2+
3+%access public export
4+%default total
5+
6+andSameNeutral : (x : Bool) -> x && x = x
7+andSameNeutral False = Refl
8+andSameNeutral True = Refl
9+
10+andFalseFalse : (x : Bool) -> x && False = False
11+andFalseFalse False = Refl
12+andFalseFalse True = Refl
13+
14+andTrueNeutral : (x : Bool) -> x && True = x
15+andTrueNeutral False = Refl
16+andTrueNeutral True = Refl
17+
18+orSameNeutral : (x : Bool) -> x || x = x
19+orSameNeutral False = Refl
20+orSameNeutral True = Refl
21+
22+orFalseNeutral : (x : Bool) -> x || False = x
23+orFalseNeutral False = Refl
24+orFalseNeutral True = Refl
25+
26+orTrueTrue : (x : Bool) -> x || True = True
27+orTrueTrue False = Refl
28+orTrueTrue True = Refl
29+
30+orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x
31+orSameAndRightNeutral False _ = Refl
32+orSameAndRightNeutral True _ = Refl
libs/contrib/Text/Lexer.idr+80−301
@@ -1,129 +1,103 @@
1module Text.Lexer
1module Text.Lexer
2
2
3+import Data.Bool.Extra
4+
5+import public Text.Lexer.Core
6+import public Text.Quantity
7+
3%default total
8%default total
9+%access export
10+
11+||| Recognise any character
12+any : Lexer
13+any = pred (const True)
14+
15+||| Recognise a lexer or recognise no input. This is not guaranteed
16+||| to consume input
17+opt : Lexer -> Recognise False
18+opt l = l <|> empty
19+
20+||| Recognise any character if the sub-lexer `l` fails.
21+non : (l : Lexer) -> Lexer
22+non l = reject l <+> any
4
23
5−||| A language of token recognisers.
24+||| Produce recognisers by applying a function to elements of a container, and
6−||| @ consumes If `True`, this recogniser is guaranteed to consume at
25+||| recognise the first match. Consumes input if the function produces consuming
7−||| least one character of input when it succeeds.
26+||| recognisers. Fails if the container is empty.
8−export
27+choiceMap : {c : Bool} ->
9−data Recognise : (consumes : Bool) -> Type where
10− Empty : Recognise False
11− Fail : Recognise c
28+ Foldable t => (a -> Recognise c) -> t a -> Recognise c
12− Lookahead : (positive : Bool) -> Recognise c -> Recognise False
29+choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
13− Pred : (Char -> Bool) -> Recognise True
30+ f x <|> acc)
14− SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
31+ fail xs
15− SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
32+
16− Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)
33+||| Recognise the first matching recogniser in a container. Consumes input if
17−
34+||| recognisers in the list consume. Fails if the container is empty.
18−||| A token recogniser. Guaranteed to consume at least one character.
35+choice : Foldable t => t (Recognise c) -> Recognise c
19−public export
36+choice = choiceMap id
20−Lexer : Type
37+
21−Lexer = Recognise True
38+||| Sequence a list of recognisers. Guaranteed to consume input if the list is
22−
39+||| non-empty and the recognisers consume.
23−public export
24−inf : Bool -> Type -> Type
25−inf True t = Inf t
26−inf False t = t
27−
28−||| Sequence two recognisers. If either consumes a character, the sequence
29−||| is guaranteed to consume a character.
30−export %inline
31−(<+>) : {c1 : Bool} ->
32− Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
33−(<+>) {c1 = False} = SeqEmpty
34−(<+>) {c1 = True} = SeqEat
35−
36−||| Alternative recognisers. If both consume, the combination is guaranteed
37−||| to consumer a character.
38−export
39−(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
40−(<|>) = Alt
41−
42−||| A recogniser that always fails.
43−export
44−fail : Recognise c
45−fail = Fail
46−
47−||| Positive lookahead. Never consumes input.
48−export
49−expect : Recognise c -> Recognise False
40+concat : (xs : List (Recognise c)) -> Recognise (c && isCons xs)
50−expect = Lookahead True
41+concat = concatMap id
51−
42+
52−||| Negative lookahead. Never consumes input.
53−export
54−reject : Recognise c -> Recognise False
55−reject = Lookahead False
56−
57−||| Recognise a specific character
43+||| Recognise a specific character.
58−export
59is : Char -> Lexer
44is : Char -> Lexer
60−is x = Pred (==x)
45+is x = pred (==x)
61
46
62−||| Recognise anything but the given character
47+||| Recognise anything but the given character.
63−export
64isNot : Char -> Lexer
48isNot : Char -> Lexer
65−isNot x = Pred (/=x)
49+isNot x = pred (/=x)
66
50
67−||| Recognise a character case-insensitively
51+||| Recognise a specific character (case-insensitive).
68−export
69like : Char -> Lexer
52like : Char -> Lexer
70−like x = Pred (\y => toUpper x == toUpper y)
53+like x = pred (\y => toUpper x == toUpper y)
71
54
72−||| Recognise anything but the given character case-insensitively
55+||| Recognise anything but the given character (case-insensitive).
73−export
74notLike : Char -> Lexer
56notLike : Char -> Lexer
75−notLike x = Pred (\y => toUpper x /= toUpper y)
57+notLike x = pred (\y => toUpper x /= toUpper y)
76
58
77−||| Recognise a specific string
59+||| Recognise a specific string.
78−export
60+||| Fails if the string is empty.
79exact : String -> Lexer
61exact : String -> Lexer
80−exact str with (unpack str)
62+exact str = case unpack str of
81− exact str | [] = Fail -- Not allowed, Lexer has to consume
63+ [] => fail
82− exact str | (x :: xs)
64+ (x :: xs) => concatMap is (x :: xs)
83− = foldl SeqEmpty (is x) (map is xs)
84
65
85−||| Recognise a specific string case-insensitively
66+||| Recognise a specific string (case-insensitive).
86−export
67+||| Fails if the string is empty.
87approx : String -> Lexer
68approx : String -> Lexer
88−approx str with (unpack str)
69+approx str = case unpack str of
89− approx str | [] = Fail -- Not allowed, Lexer has to consume
70+ [] => fail
90− approx str | (x :: xs)
71+ (x :: xs) => concatMap like (x :: xs)
91− = foldl SeqEmpty (like x) (map like xs)
92
72
93−||| Recognise a lexer or recognise no input. This is not guaranteed
73+||| Recognise any of the characters in the given string
94−||| to consume input
74+oneOf : String -> Lexer
95−export
75+oneOf cs = pred (\x => x `elem` unpack cs)
96−opt : Lexer -> Recognise False
97−opt l = l <|> Empty
98
76
99−||| Recognise a sequence of at least one sub-lexers
77+||| Recognise a character range [`a`-`b`]. Also works in reverse!
100−export
78+range : (start : Char) -> (end : Char) -> Lexer
101−some : Lexer -> Lexer
79+range start end = pred (\x => (x >= min start end)
102−some l = l <+> opt (some l)
80+ && (x <= max start end))
103
81
82+mutual
104−||| Recognise a sequence of at zero or more sub-lexers. This is not
83+ ||| Recognise a sequence of at least one sub-lexers
105−||| guaranteed to consume input
84+ some : Lexer -> Lexer
106−export
85+ some l = l <+> many l
107−many : Lexer -> Recognise False
108−many l = opt (some l)
109
86
110−||| Recognise the first matching lexer from a Foldable. Always consumes input
87+ ||| Recognise a sequence of at zero or more sub-lexers. This is not
111−||| if one of the options succeeds. Fails if the foldable is empty.
88+ ||| guaranteed to consume input
112−export
89+ many : Lexer -> Recognise False
113−choice : Foldable t => t Lexer -> Lexer
90+ many l = opt (some l)
114−choice xs = foldr Alt Fail xs
115
91
116||| Repeat the sub-lexer `l` zero or more times until the lexer
92||| Repeat the sub-lexer `l` zero or more times until the lexer
117||| `stopBefore` is encountered. `stopBefore` will not be consumed.
93||| `stopBefore` is encountered. `stopBefore` will not be consumed.
118||| Not guaranteed to consume input.
94||| Not guaranteed to consume input.
119−export
120manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
95manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
121manyUntil stopBefore l = many (reject stopBefore <+> l)
96manyUntil stopBefore l = many (reject stopBefore <+> l)
122
97
123||| Repeat the sub-lexer `l` zero or more times until the lexer
98||| Repeat the sub-lexer `l` zero or more times until the lexer
124||| `stopAfter` is encountered, and consume it. Guaranteed to
99||| `stopAfter` is encountered, and consume it. Guaranteed to
125||| consume if `stopAfter` consumes.
100||| consume if `stopAfter` consumes.
126−export
127manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
101manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
128manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
102manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
129
103
@@ -131,255 +105,130 @@ manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
131||| encountered.
105||| encountered.
132|||
106|||
133||| Useful for defining comments.
107||| Useful for defining comments.
134−export
135manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
108manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
136manyTill l end = end <|> opt (l <+> manyTill l end)
109manyTill l end = end <|> opt (l <+> manyTill l end)
137%deprecate manyTill
110%deprecate manyTill
138 "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."
111 "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."
139
112
140−||| Recognise a sub-lexer at least `min` times. Consumes input unless
113+||| Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has
141−||| min is zero.
114+||| `min` and `max` in the wrong order. Consumes input unless `min q` is zero.
142−export
115+count : (q : Quantity) -> (l : Lexer) -> Recognise (isSucc (min q))
143−atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
116+count (Qty Z Nothing) l = many l
144−atLeast Z l = many l
117+count (Qty Z (Just Z)) _ = empty
145−atLeast (S min) l = l <+> atLeast min l
118+count (Qty Z (Just (S max))) l = opt $ l <+> count (atMost max) l
146−
119+count (Qty (S min) Nothing) l = l <+> count (atLeast min) l
147−||| Recognise a sub-lexer at most `max` times. Not guaranteed to
120+count (Qty (S min) (Just Z)) _ = fail
148−||| consume input.
121+count (Qty (S min) (Just (S max))) l = l <+> count (between min max) l
149−export
150−atMost : (max : Nat) -> (l : Lexer) -> Recognise False
151−atMost Z _ = Empty
152−atMost (S k) l = atMost k l <+> opt l
153−
154−||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
155−||| if the inputs are out of order. Consumes input unless min is zero.
156−export
157−between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
158−between Z max l = atMost max l
159−between (S min) Z _ = Fail
160−between (S min) (S max) l = l <+> between min max l
161−
162−||| Recognise exactly `count` repeated occurrences of a sub-lexer.
163−||| Consumes input unless count is zero.
164−export
165−exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
166−exactly n l = between n n l
167−
168−||| Recognise any character
169−export
170−any : Lexer
171−any = Pred (const True)
172−
173−||| Recognise any character if the sub-lexer `l` fails.
174−export
175−non : (l : Lexer) -> Lexer
176−non l = reject l <+> any
177−
178−||| Recognise no input (doesn't consume any input)
179−export
180−empty : Recognise False
181−empty = Empty
182−
183−||| Recognise a character that matches a predicate
184−export
185−pred : (Char -> Bool) -> Lexer
186−pred = Pred
187−
188−||| Recognise any of the characters in the given string
189−export
190−oneOf : String -> Lexer
191−oneOf cs = pred (\x => x `elem` unpack cs)
192−
193−data StrLen : Type where
194− MkStrLen : String -> Nat -> StrLen
195−
196−getString : StrLen -> String
197−getString (MkStrLen str n) = str
198−
199−strIndex : StrLen -> Nat -> Maybe Char
200−strIndex (MkStrLen str len) i
201− = if i >= len then Nothing
202− else Just (assert_total (prim__strIndex str (cast i)))
203−
204−mkStr : String -> StrLen
205−mkStr str = MkStrLen str (length str)
206−
207−strTail : Nat -> StrLen -> StrLen
208−strTail start (MkStrLen str len)
209− = MkStrLen (substr start len str) (minus len start)
210−
211−-- If the string is recognised, returns the index at which the token
212−-- ends
213−scan : Recognise c -> Nat -> StrLen -> Maybe Nat
214−scan Empty idx str = pure idx
215−scan Fail idx str = Nothing
216−scan (Lookahead positive r) idx str
217− = if isJust (scan r idx str) == positive
218− then Just idx
219− else Nothing
220−scan (Pred f) idx str
221− = do c <- strIndex str idx
222− if f c
223− then Just (idx + 1)
224− else Nothing
225−scan (SeqEat r1 r2) idx str
226− = do idx' <- scan r1 idx str
227− -- TODO: Can we prove totality instead by showing idx has increased?
228− assert_total (scan r2 idx' str)
229−scan (SeqEmpty r1 r2) idx str
230− = do idx' <- scan r1 idx str
231− scan r2 idx' str
232−scan (Alt r1 r2) idx str
233− = case scan r1 idx str of
234− Nothing => scan r2 idx str
235− Just idx => Just idx
236−
237−takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
238−takeToken lex str
239− = do i <- scan lex 0 str -- i must be > 0 if successful
240− pure (substr 0 i (getString str), strTail i str)
241−
242−||| Recognise a character range [`a`-`b`]. Also works in reverse!
243−export
244−range : (start : Char) -> (end : Char) -> Lexer
245−range start end = pred (\x => (x >= min start end)
246− && (x <= max start end))
247
122
248||| Recognise a single digit 0-9
123||| Recognise a single digit 0-9
249−export
250digit : Lexer
124digit : Lexer
251digit = pred isDigit
125digit = pred isDigit
252
126
253||| Recognise one or more digits
127||| Recognise one or more digits
254−export
255digits : Lexer
128digits : Lexer
256digits = some digit
129digits = some digit
257
130
258||| Recognise a single hexidecimal digit
131||| Recognise a single hexidecimal digit
259−export
260hexDigit : Lexer
132hexDigit : Lexer
261hexDigit = pred isHexDigit
133hexDigit = pred isHexDigit
262
134
263||| Recognise one or more hexidecimal digits
135||| Recognise one or more hexidecimal digits
264−export
265hexDigits : Lexer
136hexDigits : Lexer
266hexDigits = some hexDigit
137hexDigits = some hexDigit
267
138
268||| Recognise a single alpha character
139||| Recognise a single alpha character
269−export
270alpha : Lexer
140alpha : Lexer
271alpha = pred isAlpha
141alpha = pred isAlpha
272
142
273||| Recognise one or more alpha characters
143||| Recognise one or more alpha characters
274−export
275alphas : Lexer
144alphas : Lexer
276alphas = some alpha
145alphas = some alpha
277
146
278||| Recognise a lowercase alpha character
147||| Recognise a lowercase alpha character
279−export
280lower : Lexer
148lower : Lexer
281lower = pred isLower
149lower = pred isLower
282
150
283||| Recognise one or more lowercase alpha characters
151||| Recognise one or more lowercase alpha characters
284−export
285lowers : Lexer
152lowers : Lexer
286lowers = some lower
153lowers = some lower
287
154
288||| Recognise an uppercase alpha character
155||| Recognise an uppercase alpha character
289−export
290upper : Lexer
156upper : Lexer
291upper = pred isUpper
157upper = pred isUpper
292
158
293||| Recognise one or more uppercase alpha characters
159||| Recognise one or more uppercase alpha characters
294−export
295uppers : Lexer
160uppers : Lexer
296uppers = some upper
161uppers = some upper
297
162
298||| Recognise an alphanumeric character
163||| Recognise an alphanumeric character
299−export
300alphaNum : Lexer
164alphaNum : Lexer
301alphaNum = pred isAlphaNum
165alphaNum = pred isAlphaNum
302
166
303||| Recognise one or more alphanumeric characters
167||| Recognise one or more alphanumeric characters
304−export
305alphaNums : Lexer
168alphaNums : Lexer
306alphaNums = some alphaNum
169alphaNums = some alphaNum
307
170
308||| Recognise a single whitespace character
171||| Recognise a single whitespace character
309−export
310space : Lexer
172space : Lexer
311space = pred isSpace
173space = pred isSpace
312
174
313||| Recognise one or more whitespace characters
175||| Recognise one or more whitespace characters
314−export
315spaces : Lexer
176spaces : Lexer
316spaces = some space
177spaces = some space
317
178
318||| Recognise a single newline sequence. Understands CRLF, CR, and LF
179||| Recognise a single newline sequence. Understands CRLF, CR, and LF
319−export
320newline : Lexer
180newline : Lexer
321newline = let crlf = "\r\n" in
181newline = let crlf = "\r\n" in
322 exact crlf <|> oneOf crlf
182 exact crlf <|> oneOf crlf
323
183
324||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
184||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
325−export
326newlines : Lexer
185newlines : Lexer
327newlines = some newline
186newlines = some newline
328
187
329||| Recognise a single non-whitespace, non-alphanumeric character
188||| Recognise a single non-whitespace, non-alphanumeric character
330−export
331symbol : Lexer
189symbol : Lexer
332symbol = pred (\x => not (isSpace x || isAlphaNum x))
190symbol = pred (\x => not (isSpace x || isAlphaNum x))
333
191
334||| Recognise one or more non-whitespace, non-alphanumeric characters
192||| Recognise one or more non-whitespace, non-alphanumeric characters
335−export
336symbols : Lexer
193symbols : Lexer
337symbols = some symbol
194symbols = some symbol
338
195
339||| Recognise zero or more occurrences of a sub-lexer between
196||| Recognise zero or more occurrences of a sub-lexer between
340||| delimiting lexers
197||| delimiting lexers
341−export
342surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
198surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
343surround start end l = start <+> manyThen end l
199surround start end l = start <+> manyThen end l
344
200
345||| Recognise zero or more occurrences of a sub-lexer surrounded
201||| Recognise zero or more occurrences of a sub-lexer surrounded
346||| by the same quote lexer on both sides (useful for strings)
202||| by the same quote lexer on both sides (useful for strings)
347−export
348quote : (q : Lexer) -> (l : Lexer) -> Lexer
203quote : (q : Lexer) -> (l : Lexer) -> Lexer
349quote q l = surround q q l
204quote q l = surround q q l
350
205
351||| Recognise an escape character (often '\\') followed by a sub-lexer
206||| Recognise an escape character (often '\\') followed by a sub-lexer
352−export
353escape : (esc : Char) -> Lexer -> Lexer
207escape : (esc : Char) -> Lexer -> Lexer
354escape esc l = is esc <+> l
208escape esc l = is esc <+> l
355
209
356||| Recognise a string literal, including escaped characters.
210||| Recognise a string literal, including escaped characters.
357||| (Note: doesn't yet handle escape sequences such as \123)
211||| (Note: doesn't yet handle escape sequences such as \123)
358−export
359stringLit : Lexer
212stringLit : Lexer
360stringLit = quote (is '"') (escape '\\' any <|> any)
213stringLit = quote (is '"') (escape '\\' any <|> any)
361
214
362||| Recognise a character literal, including escaped characters.
215||| Recognise a character literal, including escaped characters.
363||| (Note: doesn't yet handle escape sequences such as \123)
216||| (Note: doesn't yet handle escape sequences such as \123)
364−export
365charLit : Lexer
217charLit : Lexer
366charLit = let q = '\'' in
218charLit = let q = '\'' in
367 is q <+> (escape '\\' any <|> isNot q) <+> is q
219 is q <+> (escape '\\' any <|> isNot q) <+> is q
368
220
369||| Recognise an integer literal (possibly with a '-' prefix)
221||| Recognise an integer literal (possibly with a '-' prefix)
370−export
371intLit : Lexer
222intLit : Lexer
372intLit = opt (is '-') <+> digits
223intLit = opt (is '-') <+> digits
373
224
374||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
225||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
375−export
376hexLit : Lexer
226hexLit : Lexer
377hexLit = approx "0x" <+> hexDigits
227hexLit = approx "0x" <+> hexDigits
378
228
379||| Recognise `start`, then recognise all input until a newline is encountered,
229||| Recognise `start`, then recognise all input until a newline is encountered,
380||| and consume the newline. Will succeed if end-of-input is encountered before
230||| and consume the newline. Will succeed if end-of-input is encountered before
381||| a newline.
231||| a newline.
382−export
383lineComment : (start : Lexer) -> Lexer
232lineComment : (start : Lexer) -> Lexer
384lineComment start = start <+> manyUntil newline any <+> opt newline
233lineComment start = start <+> manyUntil newline any <+> opt newline
385
234
@@ -388,78 +237,8 @@ lineComment start = start <+> manyUntil newline any <+> opt newline
388|||
237|||
389||| For block comments that don't support nesting (such as C-style comments),
238||| For block comments that don't support nesting (such as C-style comments),
390||| use `surround`.
239||| use `surround`.
391−export
392blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
240blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
393blockComment start end = start <+> middle <+> end
241blockComment start end = start <+> middle <+> end
394 where
242 where
395 middle : Recognise False
243 middle : Recognise False
396 middle = manyUntil end (blockComment start end <|> any)
244 middle = manyUntil end (blockComment start end <|> any)
397−
398−||| A mapping from lexers to the tokens they produce.
399−||| This is a list of pairs `(Lexer, String -> tokenType)`
400−||| For each Lexer in the list, if a substring in the input matches, run
401−||| the associated function to produce a token of type `tokenType`
402−public export
403−TokenMap : (tokenType : Type) -> Type
404−TokenMap tokenType = List (Lexer, String -> tokenType)
405−
406−||| A token, and the line and column where it was in the input
407−public export
408−record TokenData a where
409− constructor MkToken
410− line : Int
411− col : Int
412− tok : a
413−
414−fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
415−fspanEnd k p "" = (k, "")
416−fspanEnd k p xxs
417− = assert_total $
418− let x = prim__strHead xxs
419− xs = prim__strTail xxs in
420− if p x then fspanEnd (S k) p xs
421− else (k, xxs)
422−
423−-- Faster version of 'span' from the prelude (avoids unpacking)
424−export
425−fspan : (Char -> Bool) -> String -> (String, String)
426−fspan p xs
427− = let (end, rest) = fspanEnd 0 p xs in
428− (substr 0 end xs, rest)
429−
430−tokenise : (line : Int) -> (col : Int) ->
431− List (TokenData a) -> TokenMap a ->
432− StrLen -> (List (TokenData a), (Int, Int, StrLen))
433−tokenise line col acc tmap str
434− = case getFirstToken tmap str of
435− Just (tok, line', col', rest) =>
436− -- assert total because getFirstToken must consume something
437− assert_total (tokenise line' col' (tok :: acc) tmap rest)
438− Nothing => (reverse acc, (line, col, str))
439− where
440− countNLs : List Char -> Nat
441− countNLs str = List.length (filter (== '\n') str)
442−
443− getCols : String -> Int -> Int
444− getCols x c
445− = case fspan (/= '\n') (reverse x) of
446− (incol, "") => c + cast (length incol)
447− (incol, _) => cast (length incol)
448−
449− getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)
450− getFirstToken [] str = Nothing
451− getFirstToken ((lex, fn) :: ts) str
452− = case takeToken lex str of
453− Just (tok, rest) => Just (MkToken line col (fn tok),
454− line + cast (countNLs (unpack tok)),
455− getCols tok col, rest)
456− Nothing => getFirstToken ts str
457−
458−||| Given a mapping from lexers to token generating functions (the
459−||| TokenMap a) and an input string, return a list of recognised tokens,
460−||| and the line, column, and remainder of the input at the first point in the
461−||| string where there are no recognised tokens.
462−export
463−lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
464−lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
465− (ts, (l, c, getString str'))
libs/contrib/Text/Lexer/Core.idrnew file+193
@@ -0,0 +1,193 @@
1+module Text.Lexer.Core
2+
3+import Data.Bool.Extra
4+
5+import public Control.Delayed
6+
7+%default total
8+
9+||| A language of token recognisers.
10+||| @ consumes If `True`, this recogniser is guaranteed to consume at
11+||| least one character of input when it succeeds.
12+export
13+data Recognise : (consumes : Bool) -> Type where
14+ Empty : Recognise False
15+ Fail : Recognise c
16+ Lookahead : (positive : Bool) -> Recognise c -> Recognise False
17+ Pred : (Char -> Bool) -> Recognise True
18+ SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
19+ SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
20+ Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)
21+
22+||| A token recogniser. Guaranteed to consume at least one character.
23+public export
24+Lexer : Type
25+Lexer = Recognise True
26+
27+||| Sequence two recognisers. If either consumes a character, the sequence
28+||| is guaranteed to consume a character.
29+export %inline
30+(<+>) : {c1 : Bool} ->
31+ Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
32+(<+>) {c1 = False} = SeqEmpty
33+(<+>) {c1 = True} = SeqEat
34+
35+||| Alternative recognisers. If both consume, the combination is guaranteed
36+||| to consumer a character.
37+export
38+(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
39+(<|>) = Alt
40+
41+||| A recogniser that always fails.
42+export
43+fail : Recognise c
44+fail = Fail
45+
46+||| Recognise no input (doesn't consume any input)
47+export
48+empty : Recognise False
49+empty = Empty
50+
51+||| Recognise a character that matches a predicate
52+export
53+pred : (Char -> Bool) -> Lexer
54+pred = Pred
55+
56+||| Positive lookahead. Never consumes input.
57+export
58+expect : Recognise c -> Recognise False
59+expect = Lookahead True
60+
61+||| Negative lookahead. Never consumes input.
62+export
63+reject : Recognise c -> Recognise False
64+reject = Lookahead False
65+
66+||| Sequence the recognisers resulting from applying a function to each element
67+||| of a list. The resulting recogniser will consume input if the produced
68+||| recognisers consume and the list is non-empty.
69+export
70+concatMap : {c : Bool} ->
71+ (a -> Recognise c) -> (xs : List a) -> Recognise (c && isCons xs)
72+concatMap {c} _ [] = rewrite andFalseFalse c in Empty
73+concatMap {c} f (x :: xs) = rewrite andTrueNeutral c in
74+ rewrite sym (orSameAndRightNeutral c (isCons xs)) in
75+ SeqEmpty (f x) (concatMap f xs)
76+
77+data StrLen : Type where
78+ MkStrLen : String -> Nat -> StrLen
79+
80+getString : StrLen -> String
81+getString (MkStrLen str n) = str
82+
83+strIndex : StrLen -> Nat -> Maybe Char
84+strIndex (MkStrLen str len) i
85+ = if i >= len then Nothing
86+ else Just (assert_total (prim__strIndex str (cast i)))
87+
88+mkStr : String -> StrLen
89+mkStr str = MkStrLen str (length str)
90+
91+strTail : Nat -> StrLen -> StrLen
92+strTail start (MkStrLen str len)
93+ = MkStrLen (substr start len str) (minus len start)
94+
95+-- If the string is recognised, returns the index at which the token
96+-- ends
97+scan : Recognise c -> Nat -> StrLen -> Maybe Nat
98+scan Empty idx str = pure idx
99+scan Fail idx str = Nothing
100+scan (Lookahead positive r) idx str
101+ = if isJust (scan r idx str) == positive
102+ then Just idx
103+ else Nothing
104+scan (Pred f) idx str
105+ = do c <- strIndex str idx
106+ if f c
107+ then Just (idx + 1)
108+ else Nothing
109+scan (SeqEat r1 r2) idx str
110+ = do idx' <- scan r1 idx str
111+ -- TODO: Can we prove totality instead by showing idx has increased?
112+ assert_total (scan r2 idx' str)
113+scan (SeqEmpty r1 r2) idx str
114+ = do idx' <- scan r1 idx str
115+ scan r2 idx' str
116+scan (Alt r1 r2) idx str
117+ = case scan r1 idx str of
118+ Nothing => scan r2 idx str
119+ Just idx => Just idx
120+
121+takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
122+takeToken lex str
123+ = do i <- scan lex 0 str -- i must be > 0 if successful
124+ pure (substr 0 i (getString str), strTail i str)
125+
126+||| A mapping from lexers to the tokens they produce.
127+||| This is a list of pairs `(Lexer, String -> tokenType)`
128+||| For each Lexer in the list, if a substring in the input matches, run
129+||| the associated function to produce a token of type `tokenType`
130+public export
131+TokenMap : (tokenType : Type) -> Type
132+TokenMap tokenType = List (Lexer, String -> tokenType)
133+
134+||| A token, and the line and column where it was in the input
135+public export
136+record TokenData a where
137+ constructor MkToken
138+ line : Int
139+ col : Int
140+ tok : a
141+
142+fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
143+fspanEnd k p "" = (k, "")
144+fspanEnd k p xxs
145+ = assert_total $
146+ let x = prim__strHead xxs
147+ xs = prim__strTail xxs in
148+ if p x then fspanEnd (S k) p xs
149+ else (k, xxs)
150+
151+-- Faster version of 'span' from the prelude (avoids unpacking)
152+export
153+fspan : (Char -> Bool) -> String -> (String, String)
154+fspan p xs
155+ = let (end, rest) = fspanEnd 0 p xs in
156+ (substr 0 end xs, rest)
157+
158+tokenise : (line : Int) -> (col : Int) ->
159+ List (TokenData a) -> TokenMap a ->
160+ StrLen -> (List (TokenData a), (Int, Int, StrLen))
161+tokenise line col acc tmap str
162+ = case getFirstToken tmap str of
163+ Just (tok, line', col', rest) =>
164+ -- assert total because getFirstToken must consume something
165+ assert_total (tokenise line' col' (tok :: acc) tmap rest)
166+ Nothing => (reverse acc, (line, col, str))
167+ where
168+ countNLs : List Char -> Nat
169+ countNLs str = List.length (filter (== '\n') str)
170+
171+ getCols : String -> Int -> Int
172+ getCols x c
173+ = case fspan (/= '\n') (reverse x) of
174+ (incol, "") => c + cast (length incol)
175+ (incol, _) => cast (length incol)
176+
177+ getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)
178+ getFirstToken [] str = Nothing
179+ getFirstToken ((lex, fn) :: ts) str
180+ = case takeToken lex str of
181+ Just (tok, rest) => Just (MkToken line col (fn tok),
182+ line + cast (countNLs (unpack tok)),
183+ getCols tok col, rest)
184+ Nothing => getFirstToken ts str
185+
186+||| Given a mapping from lexers to token generating functions (the
187+||| TokenMap a) and an input string, return a list of recognised tokens,
188+||| and the line, column, and remainder of the input at the first point in the
189+||| string where there are no recognised tokens.
190+export
191+lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
192+lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
193+ (ts, (l, c, getString str'))
libs/contrib/Text/Parser.idr+204−319
@@ -1,331 +1,216 @@
1module Text.Parser
1module Text.Parser
2
2
3−%default total
3+import Data.Bool.Extra
4−
5−-- TODO: Add some primitives for helping with error messages.
6−-- e.g. perhaps set a string to state what we're currently trying to
7−-- parse, or to say what the next expected token is in words
8−
9−||| Description of a language's grammar. The `tok` parameter is the type
10−||| of tokens, and the `consumes` flag is True if the language is guaranteed
11−||| to be non-empty - that is, successfully parsing the language is guaranteed
12−||| to consume some input.
13−export
14−data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
15− Empty : (val : ty) -> Grammar tok False ty
16− Terminal : (tok -> Maybe a) -> Grammar tok True a
17− NextIs : (tok -> Bool) -> Grammar tok False tok
18− EOF : Grammar tok False ()
19−
20− Fail : String -> Grammar tok c ty
21− Commit : Grammar tok False ()
22−
23− SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
24− Grammar tok True b
25− SeqEmpty : {c1, c2 : Bool} ->
26− Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
27− Grammar tok (c1 || c2) b
28− Alt : {c1, c2 : Bool} ->
29− Grammar tok c1 ty -> Grammar tok c2 ty ->
30− Grammar tok (c1 && c2) ty
31−
32−public export
33−inf : Bool -> Type -> Type
34−inf True t = Inf t
35−inf False t = t
36−
37−||| Sequence two grammars. If either consumes some input, the sequence is
38−||| guaranteed to consume some input. If the first one consumes input, the
39−||| second is allowed to be recursive (because it means some input has been
40−||| consumed and therefore the input is smaller)
41−export %inline
42−(>>=) : {c1 : Bool} ->
43− Grammar tok c1 a ->
44− inf c1 (a -> Grammar tok c2 b) ->
45− Grammar tok (c1 || c2) b
46−(>>=) {c1 = False} = SeqEmpty
47−(>>=) {c1 = True} = SeqEat
48−
49−||| Sequence a grammar followed by the grammar it returns.
50−export
51−join : {c1 : Bool} ->
52− Grammar tok c1 (Grammar tok c2 a) ->
53− Grammar tok (c1 || c2) a
54−join {c1 = False} p = SeqEmpty p id
55−join {c1 = True} p = SeqEat p id
56−
57−||| Give two alternative grammars. If both consume, the combination is
58−||| guaranteed to consume.
59−export
60−(<|>) : Grammar tok c1 ty ->
61− Grammar tok c2 ty ->
62− Grammar tok (c1 && c2) ty
63−(<|>) = Alt
64−
65−||| Allows the result of a grammar to be mapped to a different value.
66−export
67−Functor (Grammar tok c) where
68− map f (Empty val) = Empty (f val)
69− map f (Fail msg) = Fail msg
70− map f (Terminal g) = Terminal (\t => map f (g t))
71− map f (Alt x y) = Alt (map f x) (map f y)
72− map f (SeqEat act next)
73− = SeqEat act (\val => map f (next val))
74− map f (SeqEmpty act next)
75− = SeqEmpty act (\val => map f (next val))
76− -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
77− -- so a sequence must be used.
78− map {c = False} f p = SeqEmpty p (Empty . f)
79−
80−||| Sequence a grammar with value type `a -> b` and a grammar
81−||| with value type `a`. If both succeed, apply the function
82−||| from the first grammar to the value from the second grammar.
83−||| Guaranteed to consume if either grammar consumes.
84−export
85−(<*>) : {c1 : Bool} ->
86− Grammar tok c1 (a -> b) ->
87− inf c1 (Grammar tok c2 a) ->
88− Grammar tok (c1 || c2) b
89−(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
90−(<*>) {c1 = True} x y = SeqEat x (\f => map f y)
91−
92−||| Sequence two grammars. If both succeed, use the value of the first one.
93−||| Guaranteed to consume if either grammar consumes.
94−export
95−(<*) : Grammar tok c1 a ->
96− inf c1 (Grammar tok c2 b) ->
97− Grammar tok (c1 || c2) a
98−(<*) x y = map const x <*> y
99−
100−||| Sequence two grammars. If both succeed, use the value of the second one.
101−||| Guaranteed to consume if either grammar consumes.
102−export
103−(*>) : Grammar tok c1 a ->
104− inf c1 (Grammar tok c2 b) ->
105− Grammar tok (c1 || c2) b
106−(*>) x y = map (const id) x <*> y
107−
108−||| Always succeed with the given value.
109−export
110−pure : (val : ty) -> Grammar tok False ty
111−pure = Empty
112−
113−||| Check whether the next token satisfies a predicate
114−export
115−nextIs : (tok -> Bool) -> Grammar tok False tok
116−nextIs = NextIs
117−
118−||| Look at the next token in the input
119−export
120−peek : Grammar tok False tok
121−peek = nextIs (const True)
122−
123−||| Succeeds if running the predicate on the next token returns Just x,
124−||| returning x. Otherwise fails.
125−export
126−terminal : (tok -> Maybe a) -> Grammar tok True a
127−terminal = Terminal
128−
129−||| Always fail with a message
130−export
131−fail : String -> Grammar tok c ty
132−fail = Fail
133−
134−||| Succeed if the input is empty
135−export
136−eof : Grammar tok False ()
137−eof = EOF
138−
139−||| Commit to an alternative; if the current branch of an alternative
140−||| fails to parse, no more branches will be tried
141−export
142−commit : Grammar tok False ()
143−commit = Commit
144
4
145−data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
5+import public Text.Parser.Core
146− Failure : {xs : List tok} ->
6+import public Text.Quantity
147− (committed : Bool) ->
148− (err : String) -> (rest : List tok) -> ParseResult xs c ty
149− EmptyRes : (committed : Bool) ->
150− (val : ty) -> (more : List tok) -> ParseResult more False ty
151− NonEmptyRes : (committed : Bool) ->
152− (val : ty) -> (more : List tok) ->
153− ParseResult (x :: xs ++ more) c ty
154
7
155−-- Take the result of an alternative branch, reset the commit flag to
156−-- the commit flag from the outer alternative, and weaken the 'consumes'
157−-- flag to take both alternatives into account
158−weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
159− (com' : Bool) ->
160− ParseResult xs c ty -> ParseResult xs (whatever && c) ty
161−weakenRes com' (Failure com msg ts) = Failure com' msg ts
162−weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
163−weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
164−weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
165−
166−shorter : (more : List tok) -> .(ys : List tok) ->
167− LTE (S (length more)) (S (length (ys ++ more)))
168−shorter more [] = lteRefl
169−shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
170−
171−doParse : {c : Bool} ->
172− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
173− ParseResult xs c ty
174−doParse com xs act with (sizeAccessible xs)
175− doParse com xs (Empty val) | sml = EmptyRes com val xs
176− doParse com [] (Fail str) | sml = Failure com str []
177− doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)
178− doParse com xs Commit | sml = EmptyRes True () xs
179−
180− doParse com [] (Terminal f) | sml = Failure com "End of input" []
181− doParse com (x :: xs) (Terminal f) | sml
182− = maybe
183− (Failure com "Unrecognised token" (x :: xs))
184− (\a => NonEmptyRes com {xs=[]} a xs)
185− (f x)
186− doParse com [] EOF | sml = EmptyRes com () []
187− doParse com (x :: xs) EOF | sml
188− = Failure com "Expected end of input" (x :: xs)
189− doParse com [] (NextIs f) | sml = Failure com "End of input" []
190− doParse com (x :: xs) (NextIs f) | sml
191− = if f x
192− then EmptyRes com x (x :: xs)
193− else Failure com "Unrecognised token" (x :: xs)
194− doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
195− doParse com xs (Alt x y) | sml | Failure com' msg ts
196− = if com' -- If the alternative had committed, don't try the
197− -- other branch (and reset commit flag)
198− then Failure com msg ts
199− else weakenRes com (doParse False xs y | sml)
200− -- Successfully parsed the first option, so use the outer commit flag
201− doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
202− = EmptyRes com val xs
203− doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
204− = NonEmptyRes com val more
205− doParse com xs (SeqEmpty act next) | (Access morerec)
206− = case doParse com xs act | Access morerec of
207− Failure com msg ts => Failure com msg ts
208− EmptyRes com val xs =>
209− case doParse com xs (next val) | (Access morerec) of
210− Failure com' msg ts => Failure com' msg ts
211− EmptyRes com' val xs => EmptyRes com' val xs
212− NonEmptyRes com' val more => NonEmptyRes com' val more
213− NonEmptyRes {x} {xs=ys} com val more =>
214− case (doParse com more (next val) | morerec _ (shorter more ys)) of
215− Failure com' msg ts => Failure com' msg ts
216− EmptyRes com' val _ => NonEmptyRes com' val more
217− NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
218− rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
219− NonEmptyRes com' val more'
220− doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
221− doParse com xs (SeqEat act next) | sml | Failure com' msg ts
222− = Failure com' msg ts
223− doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
224− = case doParse com' more (next val) | morerec _ (shorter more ys) of
225− Failure com' msg ts => Failure com' msg ts
226− EmptyRes com' val _ => NonEmptyRes com' val more
227− NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
228− rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
229− NonEmptyRes com' val more'
230− -- This next line is not strictly necessary, but it stops the coverage
231− -- checker taking a really long time and eating lots of memory...
232− doParse _ _ _ | sml = Failure True "Help the coverage checker!" []
233−
234−public export
8+%access export
235−data ParseError tok = Error String (List tok)
9+%default total
236−
237−||| Parse a list of tokens according to the given grammar. If successful,
238−||| returns a pair of the parse result and the unparsed tokens (the remaining
239−||| input).
240−export
241−parse : (xs : List tok) -> (act : Grammar tok c ty) ->
242− Either (ParseError tok) (ty, List tok)
243−parse xs act
244− = case doParse False xs act of
245− Failure _ msg ts => Left (Error msg ts)
246− EmptyRes _ val rest => pure (val, rest)
247− NonEmptyRes _ val rest => pure (val, rest)
248−
249−||| Parse one or more things
250−export
251−some : Grammar tok True a ->
252− Grammar tok True (List a)
253−some p = do x <- p
254− (do xs <- some p
255− pure (x :: xs)) <|> pure [x]
256−
257−||| Parse zero or more things (may match the empty input)
258−export
259−many : Grammar tok True a ->
260− Grammar tok False (List a)
261−many p = some p
262− <|> pure []
263
10
11+||| Optionally parse a thing, with a default value if the grammar doesn't
12+||| match. May match the empty input.
13+option : {c : Bool} ->
14+ (def : a) -> (p : Grammar tok c a) ->
15+ Grammar tok False a
16+option {c = False} def p = p <|> pure def
17+option {c = True} def p = p <|> pure def
18+
19+||| Optionally parse a thing.
20+||| To provide a default value, use `option` instead.
21+optional : (p : Grammar tok c a) ->
22+ Grammar tok False (Maybe a)
23+optional p = option Nothing (map Just p)
24+
25+||| Try to parse one thing or the other, producing a value that indicates
26+||| which option succeeded. If both would succeed, the left option
27+||| takes priority.
28+choose : (l : Grammar tok c1 a) ->
29+ (r : Grammar tok c2 b) ->
30+ Grammar tok (c1 && c2) (Either a b)
31+choose l r = map Left l <|> map Right r
32+
33+||| Produce a grammar by applying a function to each element of a container,
34+||| then try each resulting grammar until the first one succeeds. Fails if the
35+||| container is empty.
36+choiceMap : {c : Bool} ->
37+ (a -> Grammar tok c b) ->
38+ Foldable t => t a ->
39+ Grammar tok c b
40+choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
41+ f x <|> acc)
42+ (fail "No more options") xs
43+
44+||| Try each grammar in a container until the first one succeeds.
45+||| Fails if the container is empty.
46+choice : Foldable t => t (Grammar tok c a) ->
47+ Grammar tok c a
48+choice = choiceMap id
49+
50+mutual
264−||| Parse one or more things, separated by another thing
51+ ||| Parse one or more things
265−export
266−sepBy1 : Grammar tok True () -> Grammar tok True a ->
52+ some : Grammar tok True a ->
267 Grammar tok True (List a)
53 Grammar tok True (List a)
268−sepBy1 sep p = do x <- p
54+ some p = pure (!p :: !(many p))
269− (do sep
55+
270− xs <- sepBy1 sep p
56+ ||| Parse zero or more things (may match the empty input)
57+ many : Grammar tok True a ->
58+ Grammar tok False (List a)
59+ many p = option [] (some p)
60+
61+||| Parse one or more instances of `p`, returning the parsed items and proof
62+||| that the resulting list is non-empty.
63+some' : (p : Grammar tok True a) ->
64+ Grammar tok True (xs : List a ** NonEmpty xs)
65+some' p = pure (!p :: !(many p) ** IsNonEmpty)
66+
67+mutual
68+ private
69+ count1 : (q : Quantity) ->
70+ (p : Grammar tok True a) ->
71+ Grammar tok True (List a)
72+ count1 q p = do x <- p
73+ seq (count q p)
74+ (\xs => pure (x :: xs))
75+
76+ ||| Parse `p`, repeated as specified by `q`, returning the list of values.
77+ count : (q : Quantity) ->
78+ (p : Grammar tok True a) ->
79+ Grammar tok (isSucc (min q)) (List a)
80+ count (Qty Z Nothing) p = many p
81+ count (Qty Z (Just Z)) _ = pure []
82+ count (Qty Z (Just (S max))) p = option [] $ count1 (atMost max) p
83+ count (Qty (S min) Nothing) p = count1 (atLeast min) p
84+ count (Qty (S min) (Just Z)) _ = fail "Quantity out of order"
85+ count (Qty (S min) (Just (S max))) p = count1 (between (S min) max) p
86+
87+mutual
88+ ||| Parse one or more instances of `p` until `end` succeeds, returning the
89+ ||| list of values from `p`. Guaranteed to consume input.
90+ someTill : {c : Bool} ->
91+ (end : Grammar tok c e) ->
92+ (p : Grammar tok True a) ->
93+ Grammar tok True (List a)
94+ someTill {c} end p = do x <- p
95+ seq (manyTill end p)
271− pure (x :: xs)) <|> pure [x]
96+ (\xs => pure (x :: xs))
272−
97+
98+ ||| Parse zero or more instances of `p` until `end` succeeds, returning the
99+ ||| list of values from `p`. Guaranteed to consume input if `end` consumes.
100+ manyTill : {c : Bool} ->
101+ (end : Grammar tok c e) ->
102+ (p : Grammar tok True a) ->
103+ Grammar tok c (List a)
104+ manyTill {c} end p = rewrite sym (andTrueNeutral c) in
105+ map (const []) end <|> someTill end p
106+
107+||| Parse one or more instances of `p` until `end` succeeds, returning the
108+||| list of values from `p`, along with a proof that the resulting list is
109+||| non-empty.
110+someTill' : {c : Bool} ->
111+ (end : Grammar tok c a) ->
112+ (p : Grammar tok True a) ->
113+ Grammar tok True (xs : List a ** NonEmpty xs)
114+someTill' end p
115+ = do x <- p
116+ seq (manyTill end p)
117+ (\xs => pure (x :: xs ** IsNonEmpty))
118+
119+mutual
120+ ||| Parse one or more instance of `skip` until `p` is encountered,
121+ ||| returning its value.
122+ afterSome : (skip : Grammar tok True s) ->
123+ (p : Grammar tok c a) ->
124+ Grammar tok True a
125+ afterSome skip p = do skip
126+ afterMany skip p
127+
128+ ||| Parse zero or more instance of `skip` until `p` is encountered,
129+ ||| returning its value.
130+ afterMany : {c : Bool} ->
131+ (skip : Grammar tok True s) ->
132+ (p : Grammar tok c a) ->
133+ Grammar tok c a
134+ afterMany {c} skip p = rewrite sym (andTrueNeutral c) in
135+ p <|> afterSome skip p
136+
137+||| Parse one or more things, each separated by another thing.
138+sepBy1 : {c : Bool} ->
139+ (sep : Grammar tok True s) ->
140+ (p : Grammar tok c a) ->
141+ Grammar tok c (List a)
142+sepBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
143+ [| p :: many (sep *> p) |]
144+
273−||| Parse zero or more things, separated by another thing. May
145+||| Parse zero or more things, each separated by another thing. May
274||| match the empty input.
146||| match the empty input.
275−export
147+sepBy : (sep : Grammar tok True s) ->
276−sepBy : Grammar tok True () -> Grammar tok True a ->
148+ (p : Grammar tok c a) ->
277 Grammar tok False (List a)
149 Grammar tok False (List a)
150+sepBy sep p = option [] $ sepBy1 sep p
151+
152+||| Parse one or more instances of `p` separated by `sep`, returning the
153+||| parsed items and proof that the resulting list is non-empty.
154+sepBy1' : {c : Bool} ->
155+ (sep : Grammar tok True s) ->
156+ (p : Grammar tok c a) ->
157+ Grammar tok c (xs : List a ** NonEmpty xs)
278−sepBy sep p = sepBy1 sep p <|> pure []
158+sepBy1' {c} sep p
159+ = rewrite sym (orFalseNeutral c) in
160+ seq p (\x => do xs <- many (sep *> p)
161+ pure (x :: xs ** IsNonEmpty))
162+
163+||| Parse one or more instances of `p` separated by and optionally terminated by
164+||| `sep`.
165+sepEndBy1 : {c : Bool} ->
166+ (sep : Grammar tok True s) ->
167+ (p : Grammar tok c a) ->
168+ Grammar tok c (List a)
169+sepEndBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
170+ sepBy1 sep p <* optional sep
171+
172+||| Parse zero or more instances of `p`, separated by and optionally terminated
173+||| by `sep`. Will not match a separator by itself.
174+sepEndBy : (sep : Grammar tok True s) ->
175+ (p : Grammar tok c a) ->
176+ Grammar tok False (List a)
177+sepEndBy sep p = option [] $ sepEndBy1 sep p
178+
179+||| Parse zero or more instances of `p`, separated by and optionally terminated
180+||| by `sep`, returning the parsed items and a proof that the resulting list
181+||| is non-empty.
182+sepEndBy1' : {c : Bool} ->
183+ (sep : Grammar tok True s) ->
184+ (p : Grammar tok c a) ->
185+ Grammar tok c (xs : List a ** NonEmpty xs)
186+sepEndBy1' {c} sep p = rewrite sym (orFalseNeutral c) in
187+ sepBy1' sep p <* optional sep
188+
189+||| Parse one or more instances of `p`, separated and terminated by `sep`.
190+endBy1 : {c : Bool} ->
191+ (sep : Grammar tok True s) ->
192+ (p : Grammar tok c a) ->
193+ Grammar tok True (List a)
194+endBy1 {c} sep p = some $ rewrite sym (orTrueTrue c) in
195+ p <* sep
279
196
280−||| Optionally parse a thing, with a default value if the grammar doesn't
281−||| match. May match the empty input.
282−export
283−optional : Grammar tok True a -> (ifNothing : a) ->
197+endBy : (sep : Grammar tok True s) ->
198+ (p : Grammar tok c a) ->
284− Grammar tok False a
199+ Grammar tok False (List a)
285−optional p def = p <|> pure def
200+endBy sep p = option [] $ endBy1 sep p
286
201
287−||| Fold over a list of grammars until the first one succeeds.
202+||| Parse zero or more instances of `p`, separated and terminated by `sep`,
203+||| returning the parsed items and a proof that the resulting list is non-empty.
204+endBy1' : {c : Bool} ->
288−choice : Foldable t => t (Grammar tok True a) -> Grammar tok True a
205+ (sep : Grammar tok True s) ->
289−choice xs = foldr Alt (Fail "No more options") xs
206+ (p : Grammar tok c a) ->
207+ Grammar tok True (xs : List a ** NonEmpty xs)
208+endBy1' {c} sep p = some' $ rewrite sym (orTrueTrue c) in
209+ p <* sep
290
210
291||| Parse an instance of `p` that is between `left` and `right`.
211||| Parse an instance of `p` that is between `left` and `right`.
292−export
293−between : (left : Grammar tok True ())
294− -> (right : Grammar tok True ())
212+between : (left : Grammar tok True l) ->
295− -> (p : Grammar tok True a)
296− -> Grammar tok True a
297−between left right contents = do
298− left
299− res <- contents
300− right
301− pure res
302−
303−||| Parse one or more instances of `p` separated by `s`, returning the
304−||| parsed items and proof the resulting list is non-empty.
305−export
306−sepBy1' : (sep : Grammar tok True ())
213+ (right : Grammar tok True r) ->
307− -> (p : Grammar tok True a)
308− -> Grammar tok True (xs : List a ** NonEmpty xs)
309−sepBy1' sep p
310− = do x <- p
311− (do sep
312− xs <- sepBy1 sep p
313− pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
314−
315−||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.
316−export
317−some' : (p : Grammar tok True a)
214+ (p : Grammar tok c a) ->
318− -> Grammar tok True (xs : List a ** NonEmpty xs)
319−some' p = do
320− x <- p
321− (do xs <- some p
322− pure (x::xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
323−
324−
325−||| Optionally parse a thing. If the grammar provides a default use `optional` instead.
326−export
327−maybe : Grammar tok True a
215+ Grammar tok True a
328− -> Grammar tok False (Maybe a)
216+between left right contents = left *> contents <* right
329−maybe p =
330− (do res <- p; pure $ Just res)
331− <|> pure Nothing
libs/contrib/Text/Parser/Core.idrnew file+251
@@ -0,0 +1,251 @@
1+module Text.Parser.Core
2+
3+import public Control.Delayed
4+
5+%default total
6+
7+-- TODO: Add some primitives for helping with error messages.
8+-- e.g. perhaps set a string to state what we're currently trying to
9+-- parse, or to say what the next expected token is in words
10+
11+||| Description of a language's grammar. The `tok` parameter is the type
12+||| of tokens, and the `consumes` flag is True if the language is guaranteed
13+||| to be non-empty - that is, successfully parsing the language is guaranteed
14+||| to consume some input.
15+export
16+data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
17+ Empty : (val : ty) -> Grammar tok False ty
18+ Terminal : (tok -> Maybe a) -> Grammar tok True a
19+ NextIs : (tok -> Bool) -> Grammar tok False tok
20+ EOF : Grammar tok False ()
21+
22+ Fail : String -> Grammar tok c ty
23+ Commit : Grammar tok False ()
24+
25+ SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
26+ Grammar tok True b
27+ SeqEmpty : {c1, c2 : Bool} ->
28+ Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
29+ Grammar tok (c1 || c2) b
30+ Alt : {c1, c2 : Bool} ->
31+ Grammar tok c1 ty -> Grammar tok c2 ty ->
32+ Grammar tok (c1 && c2) ty
33+
34+||| Sequence two grammars. If either consumes some input, the sequence is
35+||| guaranteed to consume some input. If the first one consumes input, the
36+||| second is allowed to be recursive (because it means some input has been
37+||| consumed and therefore the input is smaller)
38+export %inline
39+(>>=) : {c1 : Bool} ->
40+ Grammar tok c1 a ->
41+ inf c1 (a -> Grammar tok c2 b) ->
42+ Grammar tok (c1 || c2) b
43+(>>=) {c1 = False} = SeqEmpty
44+(>>=) {c1 = True} = SeqEat
45+
46+||| Sequence two grammars. If either consumes some input, the sequence is
47+||| guaranteed to consume input. This is an explicitly non-infinite version
48+||| of `>>=`.
49+export
50+seq : Grammar tok c1 a ->
51+ (a -> Grammar tok c2 b) ->
52+ Grammar tok (c1 || c2) b
53+seq = SeqEmpty
54+
55+||| Sequence a grammar followed by the grammar it returns.
56+export
57+join : {c1 : Bool} ->
58+ Grammar tok c1 (Grammar tok c2 a) ->
59+ Grammar tok (c1 || c2) a
60+join {c1 = False} p = SeqEmpty p id
61+join {c1 = True} p = SeqEat p id
62+
63+||| Give two alternative grammars. If both consume, the combination is
64+||| guaranteed to consume.
65+export
66+(<|>) : Grammar tok c1 ty ->
67+ Grammar tok c2 ty ->
68+ Grammar tok (c1 && c2) ty
69+(<|>) = Alt
70+
71+||| Allows the result of a grammar to be mapped to a different value.
72+export
73+Functor (Grammar tok c) where
74+ map f (Empty val) = Empty (f val)
75+ map f (Fail msg) = Fail msg
76+ map f (Terminal g) = Terminal (\t => map f (g t))
77+ map f (Alt x y) = Alt (map f x) (map f y)
78+ map f (SeqEat act next)
79+ = SeqEat act (\val => map f (next val))
80+ map f (SeqEmpty act next)
81+ = SeqEmpty act (\val => map f (next val))
82+ -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
83+ -- so a sequence must be used.
84+ map {c = False} f p = SeqEmpty p (Empty . f)
85+
86+||| Sequence a grammar with value type `a -> b` and a grammar
87+||| with value type `a`. If both succeed, apply the function
88+||| from the first grammar to the value from the second grammar.
89+||| Guaranteed to consume if either grammar consumes.
90+export
91+(<*>) : Grammar tok c1 (a -> b) ->
92+ Grammar tok c2 a ->
93+ Grammar tok (c1 || c2) b
94+(<*>) x y = SeqEmpty x (\f => map f y)
95+
96+||| Sequence two grammars. If both succeed, use the value of the first one.
97+||| Guaranteed to consume if either grammar consumes.
98+export
99+(<*) : Grammar tok c1 a ->
100+ Grammar tok c2 b ->
101+ Grammar tok (c1 || c2) a
102+(<*) x y = map const x <*> y
103+
104+||| Sequence two grammars. If both succeed, use the value of the second one.
105+||| Guaranteed to consume if either grammar consumes.
106+export
107+(*>) : Grammar tok c1 a ->
108+ Grammar tok c2 b ->
109+ Grammar tok (c1 || c2) b
110+(*>) x y = map (const id) x <*> y
111+
112+||| Always succeed with the given value.
113+export
114+pure : (val : ty) -> Grammar tok False ty
115+pure = Empty
116+
117+||| Check whether the next token satisfies a predicate
118+export
119+nextIs : (tok -> Bool) -> Grammar tok False tok
120+nextIs = NextIs
121+
122+||| Look at the next token in the input
123+export
124+peek : Grammar tok False tok
125+peek = nextIs (const True)
126+
127+||| Succeeds if running the predicate on the next token returns Just x,
128+||| returning x. Otherwise fails.
129+export
130+terminal : (tok -> Maybe a) -> Grammar tok True a
131+terminal = Terminal
132+
133+||| Always fail with a message
134+export
135+fail : String -> Grammar tok c ty
136+fail = Fail
137+
138+||| Succeed if the input is empty
139+export
140+eof : Grammar tok False ()
141+eof = EOF
142+
143+||| Commit to an alternative; if the current branch of an alternative
144+||| fails to parse, no more branches will be tried
145+export
146+commit : Grammar tok False ()
147+commit = Commit
148+
149+data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
150+ Failure : {xs : List tok} ->
151+ (committed : Bool) ->
152+ (err : String) -> (rest : List tok) -> ParseResult xs c ty
153+ EmptyRes : (committed : Bool) ->
154+ (val : ty) -> (more : List tok) -> ParseResult more False ty
155+ NonEmptyRes : (committed : Bool) ->
156+ (val : ty) -> (more : List tok) ->
157+ ParseResult (x :: xs ++ more) c ty
158+
159+-- Take the result of an alternative branch, reset the commit flag to
160+-- the commit flag from the outer alternative, and weaken the 'consumes'
161+-- flag to take both alternatives into account
162+weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
163+ (com' : Bool) ->
164+ ParseResult xs c ty -> ParseResult xs (whatever && c) ty
165+weakenRes com' (Failure com msg ts) = Failure com' msg ts
166+weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
167+weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
168+weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
169+
170+shorter : (more : List tok) -> .(ys : List tok) ->
171+ LTE (S (length more)) (S (length (ys ++ more)))
172+shorter more [] = lteRefl
173+shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
174+
175+doParse : {c : Bool} ->
176+ (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
177+ ParseResult xs c ty
178+doParse com xs act with (sizeAccessible xs)
179+ doParse com xs (Empty val) | sml = EmptyRes com val xs
180+ doParse com [] (Fail str) | sml = Failure com str []
181+ doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)
182+ doParse com xs Commit | sml = EmptyRes True () xs
183+
184+ doParse com [] (Terminal f) | sml = Failure com "End of input" []
185+ doParse com (x :: xs) (Terminal f) | sml
186+ = maybe
187+ (Failure com "Unrecognised token" (x :: xs))
188+ (\a => NonEmptyRes com {xs=[]} a xs)
189+ (f x)
190+ doParse com [] EOF | sml = EmptyRes com () []
191+ doParse com (x :: xs) EOF | sml
192+ = Failure com "Expected end of input" (x :: xs)
193+ doParse com [] (NextIs f) | sml = Failure com "End of input" []
194+ doParse com (x :: xs) (NextIs f) | sml
195+ = if f x
196+ then EmptyRes com x (x :: xs)
197+ else Failure com "Unrecognised token" (x :: xs)
198+ doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
199+ doParse com xs (Alt x y) | sml | Failure com' msg ts
200+ = if com' -- If the alternative had committed, don't try the
201+ -- other branch (and reset commit flag)
202+ then Failure com msg ts
203+ else weakenRes com (doParse False xs y | sml)
204+ -- Successfully parsed the first option, so use the outer commit flag
205+ doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
206+ = EmptyRes com val xs
207+ doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
208+ = NonEmptyRes com val more
209+ doParse com xs (SeqEmpty act next) | (Access morerec)
210+ = case doParse com xs act | Access morerec of
211+ Failure com msg ts => Failure com msg ts
212+ EmptyRes com val xs =>
213+ case doParse com xs (next val) | (Access morerec) of
214+ Failure com' msg ts => Failure com' msg ts
215+ EmptyRes com' val xs => EmptyRes com' val xs
216+ NonEmptyRes com' val more => NonEmptyRes com' val more
217+ NonEmptyRes {x} {xs=ys} com val more =>
218+ case (doParse com more (next val) | morerec _ (shorter more ys)) of
219+ Failure com' msg ts => Failure com' msg ts
220+ EmptyRes com' val _ => NonEmptyRes com' val more
221+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
222+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
223+ NonEmptyRes com' val more'
224+ doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
225+ doParse com xs (SeqEat act next) | sml | Failure com' msg ts
226+ = Failure com' msg ts
227+ doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
228+ = case doParse com' more (next val) | morerec _ (shorter more ys) of
229+ Failure com' msg ts => Failure com' msg ts
230+ EmptyRes com' val _ => NonEmptyRes com' val more
231+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
232+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
233+ NonEmptyRes com' val more'
234+ -- This next line is not strictly necessary, but it stops the coverage
235+ -- checker taking a really long time and eating lots of memory...
236+ doParse _ _ _ | sml = Failure True "Help the coverage checker!" []
237+
238+public export
239+data ParseError tok = Error String (List tok)
240+
241+||| Parse a list of tokens according to the given grammar. If successful,
242+||| returns a pair of the parse result and the unparsed tokens (the remaining
243+||| input).
244+export
245+parse : (act : Grammar tok c ty) -> (xs : List tok) ->
246+ Either (ParseError tok) (ty, List tok)
247+parse act xs
248+ = case doParse False xs act of
249+ Failure _ msg ts => Left (Error msg ts)
250+ EmptyRes _ val rest => pure (val, rest)
251+ NonEmptyRes _ val rest => pure (val, rest)
libs/contrib/Text/Quantity.idrnew file+38
@@ -0,0 +1,38 @@
1+module Text.Quantity
2+
3+%access public export
4+%default total
5+
6+record Quantity where
7+ constructor Qty
8+ min : Nat
9+ max : Maybe Nat
10+
11+Show Quantity where
12+ show (Qty Z Nothing) = "*"
13+ show (Qty Z (Just (S Z))) = "?"
14+ show (Qty (S Z) Nothing) = "+"
15+ show (Qty min max) = "{" ++ show min ++ showMax ++ "}"
16+ where
17+ showMax : String
18+ showMax = case max of
19+ Nothing => ","
20+ Just max' => if min == max'
21+ then ""
22+ else "," ++ show max'
23+
24+between : Nat -> Nat -> Quantity
25+between min max = Qty min (Just max)
26+
27+atLeast : Nat -> Quantity
28+atLeast min = Qty min Nothing
29+
30+atMost : Nat -> Quantity
31+atMost max = Qty 0 (Just max)
32+
33+exactly : Nat -> Quantity
34+exactly n = Qty n (Just n)
35+
36+inOrder : Quantity -> Bool
37+inOrder (Qty min Nothing) = True
38+inOrder (Qty min (Just max)) = min <= max
libs/contrib/contrib.ipkg+5
@@ -9,6 +9,7 @@ modules = CFFI
9 , Control.Algebra.Lattice
9 , Control.Algebra.Lattice
10 , Control.Algebra.NumericImplementations
10 , Control.Algebra.NumericImplementations
11 , Control.Algebra.VectorSpace
11 , Control.Algebra.VectorSpace
12+ , Control.Delayed
12 , Control.Isomorphism.Primitives
13 , Control.Isomorphism.Primitives
13 , Control.Partial
14 , Control.Partial
14 , Control.Pipeline
15 , Control.Pipeline
@@ -16,6 +17,7 @@ modules = CFFI
16 , Control.ST.Exception
17 , Control.ST.Exception
17 , Control.ST.ImplicitCall
18 , Control.ST.ImplicitCall
18 , Control.ST.Random
19 , Control.ST.Random
20+ , Data.Bool.Extra
19 , Data.BoundedList
21 , Data.BoundedList
20 , Data.CoList
22 , Data.CoList
21 , Data.Combinators
23 , Data.Combinators
@@ -51,9 +53,12 @@ modules = CFFI
51 , Network.Socket.Raw
53 , Network.Socket.Raw
52 , System.Concurrency.Process
54 , System.Concurrency.Process
53 , Text.Lexer
55 , Text.Lexer
56+ , Text.Lexer.Core
54 , Text.Literate
57 , Text.Literate
55 , Text.Parser
58 , Text.Parser
59+ , Text.Parser.Core
56 , Text.PrettyPrint.WL
60 , Text.PrettyPrint.WL
57 , Text.PrettyPrint.WL.Characters
61 , Text.PrettyPrint.WL.Characters
58 , Text.PrettyPrint.WL.Combinators
62 , Text.PrettyPrint.WL.Combinators
59 , Text.PrettyPrint.WL.Core
63 , Text.PrettyPrint.WL.Core
64+ , Text.Quantity