edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-28 07:15:33 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #221 from ziman/parser-lazy

Browse Source 
Make the applicative combinators in `Text.Parser.Core` lazier
This commit is contained in:
Edwin Brady 2020-03-18 20:35:01 +00:00 committed by GitHub
commit 6f933ba230
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
libs/contrib/Text/Parser/Core.idr
View File

@ -86,16 +86,17 @@ export
export
(<*>) : {c1, c2 : _} ->
Grammar tok c1 (a -> b) ->
Grammar tok c2 a ->
Inf (Grammar tok c2 a) ->
Grammar tok (c1 || c2) b
(<*>) x y = SeqEmpty x (\f => map f y)
(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
(<*>) {c1 = True } x y = SeqEmpty x (\f => map f (Force y))
||| Sequence two grammars. If both succeed, use the value of the first one.
||| Guaranteed to consume if either grammar consumes.
export
(<*) : {c1, c2 : _} ->
Grammar tok c1 a ->
Grammar tok c2 b ->
Inf (Grammar tok c2 b) ->
Grammar tok (c1 || c2) a
(<*) x y = map const x <*> y
@ -104,7 +105,7 @@ export
export
(*>) : {c1, c2 : _} ->
Grammar tok c1 a ->
Grammar tok c2 b ->
Inf (Grammar tok c2 b) ->
Grammar tok (c1 || c2) b
(*>) x y = map (const id) x <*> y