edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-26 06:11:50 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #256 from gallais/faster-lexer

Browse Source 
[ performance ] rewrite-free concatMap
This commit is contained in:
Edwin Brady 2020-04-02 16:11:02 +01:00 committed by GitHub
commit 8029241458
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 9 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Text/Lexer.idr
View File

@ -44,7 +44,7 @@ choice = choiceMap id
||| Sequence a list of recognisers. Guaranteed to consume input if the list is ||| Sequence a list of recognisers. Guaranteed to consume input if the list is
||| non-empty and the recognisers consume. ||| non-empty and the recognisers consume.
concat : (xs : List (Recognise c)) -> Recognise (c && isCons xs) concat : (xs : List (Recognise c)) -> Recognise (isCons xs && c)
concat = concatMap id concat = concatMap id
||| Recognise a specific character. ||| Recognise a specific character.

14
src/Text/Lexer/Core.idr
View File

@ -17,6 +17,7 @@ data Recognise : (consumes : Bool) -> Type where
Pred : (Char -> Bool) -> Recognise True Pred : (Char -> Bool) -> Recognise True
SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2) SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
SeqSame : Recognise e -> Recognise e -> Recognise e
Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2) Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)
||| A token recogniser. Guaranteed to consume at least one character. ||| A token recogniser. Guaranteed to consume at least one character.
@ -67,12 +68,10 @@ reject = Lookahead False
||| of a list. The resulting recogniser will consume input if the produced ||| of a list. The resulting recogniser will consume input if the produced
||| recognisers consume and the list is non-empty. ||| recognisers consume and the list is non-empty.
export export
concatMap : {c : Bool} -> concatMap : (a -> Recognise c) -> (xs : List a) -> Recognise (isCons xs && c)
(a -> Recognise c) -> (xs : List a) -> Recognise (c && isCons xs) concatMap _ [] = Empty
concatMap {c} _ [] = rewrite andFalseFalse c in Empty concatMap f (x :: []) = f x
concatMap {c} f (x :: xs) = rewrite andTrueNeutral c in concatMap f (x :: xs@(_ :: _)) = SeqSame (f x) (concatMap f xs)
rewrite sym (orSameAndRightNeutral c (isCons xs)) in
SeqEmpty (f x) (concatMap f xs)
data StrLen : Type where data StrLen : Type where
MkStrLen : String -> Nat -> StrLen MkStrLen : String -> Nat -> StrLen
@ -114,6 +113,9 @@ scan (SeqEat r1 r2) idx str
scan (SeqEmpty r1 r2) idx str scan (SeqEmpty r1 r2) idx str
= do idx' <- scan r1 idx str = do idx' <- scan r1 idx str
scan r2 idx' str scan r2 idx' str
scan (SeqSame r1 r2) idx str
= do idx' <- scan r1 idx str
scan r2 idx' str
scan (Alt r1 r2) idx str scan (Alt r1 r2) idx str
= maybe (scan r2 idx str) Just (scan r1 idx str) = maybe (scan r2 idx str) Just (scan r1 idx str)