
   0 | module Libraries.Text.Lexer.Core
   1 | 
   2 | import Data.List
   3 | import Data.Maybe
   4 | 
   5 | import public Libraries.Control.Delayed
   6 | import public Libraries.Text.Bounded
   7 | 
   8 | %default total
   9 | 
  10 | ||| A language of token recognisers.
  11 | ||| @ consumes If `True`, this recogniser is guaranteed to consume at
  12 | |||            least one character of input when it succeeds.
  13 | export
  14 | data Recognise : (consumes : Bool) -> Type where
  15 |      Empty : Recognise False
  16 |      Fail : Recognise c
  17 |      EOF : Recognise False
  18 |      Lookahead : (positive : Bool) -> Recognise c -> Recognise False
  19 |      Pred : (Char -> Bool) -> Recognise True
  20 |      SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
  21 |      SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
  22 |      SeqSame : Recognise e -> Recognise e -> Recognise e
  23 |      Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)
  24 | 
  25 | ||| A token recogniser. Guaranteed to consume at least one character.
  26 | public export
  27 | Lexer : Type
  28 | Lexer = Recognise True
  29 | 
  30 | ||| Sequence two recognisers. If either consumes a character, the sequence
  31 | ||| is guaranteed to consume a character.
  32 | export %inline
  33 | (<+>) : {c1 : Bool} ->
  34 |         Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
  35 | (<+>) {c1 = False} = SeqEmpty
  36 | (<+>) {c1 = True} = SeqEat
  37 | 
  38 | ||| Alternative recognisers. If both consume, the combination is guaranteed
  39 | ||| to consume a character.
  40 | export
  41 | (<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
  42 | (<|>) = Alt
  43 | 
  44 | ||| A recogniser that always fails.
  45 | export
  46 | fail : Recognise c
  47 | fail = Fail
  48 | 
  49 | ||| Recognise no input (doesn't consume any input)
  50 | export
  51 | empty : Recognise False
  52 | empty = Empty
  53 | 
  54 | ||| Recognise end of input
  55 | export
  56 | eof : Recognise False
  57 | eof = EOF
  58 | 
  59 | ||| Recognise a character that matches a predicate
  60 | export
  61 | pred : (Char -> Bool) -> Lexer
  62 | pred = Pred
  63 | 
  64 | ||| Positive lookahead. Never consumes input.
  65 | export
  66 | expect : Recognise c -> Recognise False
  67 | expect = Lookahead True
  68 | 
  69 | ||| Negative lookahead. Never consumes input.
  70 | export
  71 | reject : Recognise c -> Recognise False
  72 | reject = Lookahead False
  73 | 
  74 | ||| Sequence the recognisers resulting from applying a function to each element
  75 | ||| of a list. The resulting recogniser will consume input if the produced
  76 | ||| recognisers consume and the list is non-empty.
  77 | export
  78 | concatMap : (a -> Recognise c) -> (xs : List a) -> Recognise (isCons xs && c)
  79 | concatMap _ []                 = Empty
  80 | concatMap f (x :: [])          = f x
  81 | concatMap f (x :: xs@(_ :: _)) = SeqSame (f x) (concatMap f xs)
  82 | 
  83 | data StrLen : Type where
  84 |      MkStrLen : String -> Nat -> StrLen
  85 | 
  86 | getString : StrLen -> String
  87 | getString (MkStrLen str n) = str
  88 | 
  89 | strIndex : StrLen -> Nat -> Maybe Char
  90 | strIndex (MkStrLen str len) i
  91 |     = if cast {to = Integer} i >= cast len then Nothing
  92 |       else Just (assert_total (prim__strIndex str (cast i)))
  93 | 
  94 | mkStr : String -> StrLen
  95 | mkStr str = MkStrLen str (length str)
  96 | 
  97 | strTail : Nat -> StrLen -> StrLen
  98 | strTail start (MkStrLen str len)
  99 |     = MkStrLen (substr start len str) (minus len start)
 100 | 
 101 | -- If the string is recognised, returns the index at which the token
 102 | -- ends
 103 | export
 104 | scan : Recognise c -> List Char -> List Char -> Maybe (List Char, List Char)
 105 | scan Empty tok str = pure (tok, str)
 106 | scan Fail tok str = Nothing
 107 | scan EOF tok [] = Just (tok,[])
 108 | scan EOF tok (_::_) = Nothing
 109 | scan (Lookahead positive r) tok str
 110 |     = if isJust (scan r tok str) == positive
 111 |          then pure (tok, str)
 112 |          else Nothing
 113 | scan (Pred f) tok [] = Nothing
 114 | scan (Pred f) tok (c :: str)
 115 |     = if f c
 116 |          then Just (c :: tok, str)
 117 |          else Nothing
 118 | scan (SeqEat r1 r2) tok str
 119 |     = do (tok', rest) <- scan r1 tok str
 120 |          -- TODO: Can we prove totality instead by showing idx has increased?
 121 |          assert_total (scan r2 tok' rest)
 122 | scan (SeqEmpty r1 r2) tok str
 123 |     = do (tok', rest) <- scan r1 tok str
 124 |          scan r2 tok' rest
 125 | scan (SeqSame r1 r2) tok str
 126 |     = do (tok', rest) <- scan r1 tok str
 127 |          scan r2 tok' rest
 128 | scan (Alt r1 r2) tok str
 129 |     = maybe (scan r2 tok str) Just (scan r1 tok str)
 130 | 
 131 | ||| A mapping from lexers to the tokens they produce.
 132 | ||| This is a list of pairs `(Lexer, String -> tokenType)`
 133 | ||| For each Lexer in the list, if a substring in the input matches, run
 134 | ||| the associated function to produce a token of type `tokenType`
 135 | public export
 136 | TokenMap : (tokenType : Type) -> Type
 137 | TokenMap tokenType = List (Lexer, String -> tokenType)
 138 | 
 139 | tokenise : (a -> Bool) ->
 140 |            (line : Int) -> (col : Int) ->
 141 |            List (WithBounds a) -> TokenMap a ->
 142 |            List Char -> (List (WithBounds a), (Int, Int, List Char))
 143 | tokenise pred line col acc tmap str
 144 |     = case getFirstToken tmap str of
 145 |            Just (tok, line', col', rest) =>
 146 |            -- assert total because getFirstToken must consume something
 147 |                if pred tok.val
 148 |                   then (reverse acc, (line, col, []))
 149 |                   else assert_total (tokenise pred line' col' (tok :: acc) tmap rest)
 150 |            Nothing => (reverse acc, (line, col, str))
 151 |   where
 152 |     countNLs : List Char -> Nat
 153 |     countNLs str = List.length (filter (== '\n') str)
 154 | 
 155 |     getCols : List Char -> Int -> Int
 156 |     getCols x c
 157 |          = case span (/= '\n') x of
 158 |                 (incol, []) => c + cast (length incol)
 159 |                 (incol, _) => cast (length incol)
 160 | 
 161 |     getFirstToken : TokenMap a -> List Char ->
 162 |                     Maybe (WithBounds a, Int, Int, List Char)
 163 |     getFirstToken [] str = Nothing
 164 |     getFirstToken ((lex, fn) :: ts) str
 165 |         = case scan lex [] str of
 166 |                Just (tok, rest) =>
 167 |                  let line' = line + cast (countNLs tok)
 168 |                      col' = getCols tok col in
 169 |                      Just (MkBounded (fn (fastPack (reverse tok))) False (MkBounds line col line' col'),
 170 |                            line', col', rest)
 171 |                Nothing => getFirstToken ts str
 172 | 
 173 | export
 174 | lexTo : (a -> Bool) ->
 175 |         TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 176 | lexTo pred tmap str
 177 |     = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
 178 |           (ts, (l, c, fastPack str'))
 179 | 
 180 | ||| Given a mapping from lexers to token generating functions (the
 181 | ||| TokenMap a) and an input string, return a list of recognised tokens,
 182 | ||| and the line, column, and remainder of the input at the first point in the
 183 | ||| string where there are no recognised tokens.
 184 | export
 185 | lex : TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 186 | lex = lexTo (const False)
 187 |