@@ -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
@@ -191,10 +185,10 @@ strTail start (MkStrLen str len)
191185scan : Recognise c -> Nat -> StrLen -> Maybe Nat
192186scan Empty idx str = pure idx
193187scan Fail idx str = Nothing
194−scan (Expect r) idx str
195− = case scan r idx str of
196− Just _ => pure idx
197− Nothing => Nothing
188+scan (Lookahead positive r) idx str
189+ = if isJust (scan r idx str) == positive
190+ then Just idx
191+ else Nothing
198192scan (Pred f) idx str
199193 = do c <- strIndex str idx
200194 if f c