a1ac9a2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Text.Lexer: fix `reject` behavior at end-of-input

Previously, `reject` was implemented using `expect`, and inverting the predicate used with `Pred`. This means that `reject` would fail if it's the final lexer in the input, instead of succeeding like it should. To fix this, the constructor `Expect` was renamed to `Lookahead`, with a new boolean argument indicating positive or negative lookahead. This boolean is processed in `scan`. Now, `reject` succeeds if the sub-lexer fails for any reason, including end of input.

commita1ac9a20562bf0fde4d07e76c489811de8b8bfdf authorMichael Morgan <morgan.michael@me.com> dateMon 4 Sep 2017, 14:09 (9 years ago) parentf925538

1 file changed+7−13

compare with master

unifiedsplit

libs/contrib/Text/Lexer.idr+7−13

libs/contrib/Text/Lexer.idr+7−13

@@ -9,7 +9,7 @@ export

99data Recognise : (consumes : Bool) -> Type where

1010 Empty : Recognise False

1111 Fail : Recognise c

12− Expect : Recognise c -> Recognise False

12+ Lookahead : (positive : Bool) -> Recognise c -> Recognise False

1313 Pred : (Char -> Bool) -> Recognise True

1414 SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True

1515 SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)

@@ -47,18 +47,12 @@ fail = Fail

4747||| Positive lookahead. Never consumes input.

4848export

4949expect : Recognise c -> Recognise False

50−expect = Expect

50+expect = Lookahead True

5151

5252||| Negative lookahead. Never consumes input.

5353export

5454reject : Recognise c -> Recognise False

55−reject Empty = Fail

56−reject Fail = Empty

57−reject (Expect x) = reject x

58−reject (Pred f) = Expect (Pred (not . f))

59−reject (SeqEat r1 r2) = reject r1 <|> Expect (SeqEat r1 (reject r2))

60−reject (SeqEmpty r1 r2) = reject r1 <|> Expect (SeqEmpty r1 (reject r2))

61−reject (Alt r1 r2) = reject r1 <+> reject r2

55+reject = Lookahead False

6256

6357||| Recognise a specific character

6458export

@@ -175,10 +169,10 @@ strTail start (MkStrLen str len)

175169scan : Recognise c -> Nat -> StrLen -> Maybe Nat

176170scan Empty idx str = pure idx

177171scan Fail idx str = Nothing

178−scan (Expect r) idx str

179− = case scan r idx str of

180− Just _ => pure idx

181− Nothing => Nothing

172+scan (Lookahead positive r) idx str

173+ = if isJust (scan r idx str) == positive

174+ then Just idx

175+ else Nothing

182176scan (Pred f) idx str

183177 = do c <- strIndex str idx

184178 if f c