module Text.Lexer.Core import Data.Bool.Extra import public Control.Delayed %default total ||| A language of token recognisers.||| @ consumes If `True`, this recogniser is guaranteed to consume at|||            least one character of input when it succeeds.exportdata Recognise : (consumes : Bool) -> Type where     Empty : Recognise False     Fail : Recognise c     Lookahead : (positive : Bool) -> Recognise c -> Recognise False     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.public exportLexer : TypeLexer = Recognise True ||| Sequence two recognisers. If either consumes a character, the sequence||| is guaranteed to consume a character.export %inline(<+>) : {c1 : Bool} ->        Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)(<+>) {c1 = False} = SeqEmpty(<+>) {c1 = True} = SeqEat ||| Alternative recognisers. If both consume, the combination is guaranteed||| to consume a character.export(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)(<|>) = Alt ||| A recogniser that always fails.exportfail : Recognise cfail = Fail ||| Recognise no input (doesn't consume any input)exportempty : Recognise Falseempty = Empty ||| Recognise a character that matches a predicateexportpred : (Char -> Bool) -> Lexerpred = Pred ||| Positive lookahead. Never consumes input.exportexpect : Recognise c -> Recognise Falseexpect = Lookahead True ||| Negative lookahead. Never consumes input.exportreject : Recognise c -> Recognise Falsereject = Lookahead False ||| Sequence the recognisers resulting from applying a function to each element||| of a list. The resulting recogniser will consume input if the produced||| recognisers consume and the list is non-empty.exportconcatMap : (a -> Recognise c) -> (xs : List a) -> Recognise (isCons xs && c)concatMap _ []                 = EmptyconcatMap f (x :: [])          = f xconcatMap f (x :: xs@(_ :: _)) = SeqSame (f x) (concatMap f xs) data StrLen : Type where     MkStrLen : String -> Nat -> StrLen getString : StrLen -> StringgetString (MkStrLen str n) = str strIndex : StrLen -> Nat -> Maybe CharstrIndex (MkStrLen str len) i    = if cast {to = Integer} i >= cast len then Nothing      else Just (assert_total (prim__strIndex str (cast i))) mkStr : String -> StrLenmkStr str = MkStrLen str (length str) strTail : Nat -> StrLen -> StrLenstrTail start (MkStrLen str len)    = MkStrLen (substr start len str) (minus len start) ||| If the string is recognised, returns the index at which the token endsscan : Recognise c -> Nat -> StrLen -> Maybe Natscan Empty idx str = pure idxscan Fail idx str = Nothingscan (Lookahead positive r) idx str = do  guard (isJust (scan r idx str) == positive)  pure idxscan (Pred f) idx str = do  c <- strIndex str idx  guard (f c)  pure (1 + idx)scan (SeqEat r1 r2) idx str    = do idx' <- scan r1 idx str         -- TODO: Can we prove totality instead by showing idx has increased?         assert_total (scan r2 idx' str)scan (SeqEmpty r1 r2) idx str    = do idx' <- scan r1 idx str         scan r2 idx' strscan (SeqSame r1 r2) idx str    = do idx' <- scan r1 idx str         scan r2 idx' strscan (Alt r1 r2) idx str    = maybe (scan r2 idx str) Just (scan r1 idx str) takeToken : Lexer -> StrLen -> Maybe (String, StrLen)takeToken lex str    = do i <- scan lex 0 str -- i must be > 0 if successful         pure (substr 0 i (getString str), strTail i str) ||| A mapping from lexers to the tokens they produce.||| This is a list of pairs `(Lexer, String -> tokenType)`||| For each Lexer in the list, if a substring in the input matches, run||| the associated function to produce a token of type `tokenType`public exportTokenMap : (tokenType : Type) -> TypeTokenMap tokenType = List (Lexer, String -> tokenType) ||| A token, and the line and column where it was in the inputpublic exportrecord TokenData a where  constructor MkToken  line : Int  col : Int  tok : a ||| `fspanEnd 0` returns the index at which the span stopped together||| with the leftover string.||| BEWARE: It is NOT a `span` starting from the string's end!fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)fspanEnd k p "" = (k, "")fspanEnd k p xxs    = assert_total $      let x = prim__strHead xxs          xs = prim__strTail xxs in          if p x then fspanEnd (S k) p xs                 else (k, xxs) ||| Faster version of 'span' from the prelude (avoids unpacking)exportfspan : (Char -> Bool) -> String -> (String, String)fspan p xs    = let (end, rest) = fspanEnd 0 p xs in          (substr 0 end xs, rest) tokenise : (TokenData a -> Bool) ->           (line : Int) -> (col : Int) ->           List (TokenData a) -> TokenMap a ->           StrLen -> (List (TokenData a), (Int, Int, StrLen))tokenise pred line col acc tmap str    = case getFirstToken tmap str of           Just (tok, line', col', rest) =>           -- assert total because getFirstToken must consume something               if pred tok                  then (reverse acc, (line, col, MkStrLen "" 0))                  else assert_total (tokenise pred line' col' (tok :: acc) tmap rest)           Nothing => (reverse acc, (line, col, str))  where    countNLs : List Char -> Nat    countNLs str = List.length (filter (== '\n') str)     getCols : String -> Int -> Int    getCols x c         = case fspan (/= '\n') (reverse x) of                (incol, "") => c + cast (length incol)                (incol, _) => cast (length incol)     getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)    getFirstToken [] str = Nothing    getFirstToken ((lex, fn) :: ts) str        = case takeToken lex str of               Just (tok, rest) => Just (MkToken line col (fn tok),                                         line + cast (countNLs (unpack tok)),                                         getCols tok col, rest)               Nothing => getFirstToken ts str ||| Given a mapping from lexers to token generating functions (the||| TokenMap a) and an input string, return a list of recognised tokens,||| and the line, column, and remainder of the input at the first point in the||| string where there are no recognised tokens.exportlex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))lex tmap str   = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (mkStr str) in         (ts, (l, c, getString str')) exportlexTo : (TokenData a -> Bool) ->        TokenMap a -> String -> (List (TokenData a), (Int, Int, String))lexTo pred tmap str   = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (mkStr str) in         (ts, (l, c, getString str'))