[ performance ] rewrite-free concatMap

Simply removing rewrites took me down from a user time of ~1m8s
to ~54s when running `make test`. The (small) code duplication
in `scan` is a bit annoying.

We could have a core unindexed data structure and then only export
pseudo-constructors with the right phantom arguments. Not sure it
is worth it yet though.

A more principled solution would of course be to make sure the backend
gets rid of the code corresponding to rewrites altogether!

src/Text/Lexer.idr

@@ -44,7 +44,7 @@ choice = choiceMap id
 
 ||| Sequence a list of recognisers. Guaranteed to consume input if the list is
 ||| 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
 
 ||| Recognise a specific character.

src/Text/Lexer/Core.idr

@@ -17,6 +17,7 @@ data Recognise : (consumes : Bool) -> Type where
      Pred : (Char -> Bool) -> Recognise True
      SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
      SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
+     SeqSame : Recognise e -> Recognise e -> Recognise e
      Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)
 
 ||| 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
 ||| recognisers consume and the list is non-empty.
 export
-concatMap : {c : Bool} ->
-            (a -> Recognise c) -> (xs : List a) -> Recognise (c && isCons xs)
-concatMap {c} _ [] = rewrite andFalseFalse c in Empty
-concatMap {c} f (x :: xs) = rewrite andTrueNeutral c in
-                            rewrite sym (orSameAndRightNeutral c (isCons xs)) in
-                                    SeqEmpty (f x) (concatMap f xs)
+concatMap : (a -> Recognise c) -> (xs : List a) -> Recognise (isCons xs && c)
+concatMap _ []                 = Empty
+concatMap f (x :: [])          = f x
+concatMap f (x :: xs@(_ :: _)) = SeqSame (f x) (concatMap f xs)
 
 data StrLen : Type where
      MkStrLen : String -> Nat -> StrLen
@@ -114,6 +113,9 @@ scan (SeqEat r1 r2) idx str
 scan (SeqEmpty r1 r2) idx str
     = do idx' <- scan r1 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
     = maybe (scan r2 idx str) Just (scan r1 idx str)