
   0 | ||| A simple library of lexers and their combinators. A `Lexer` is
   1 | ||| just a (dependent) function, which is guaranteed to consume a non-empty
   2 | ||| prefix of the input list of characters.
   3 | |||
   4 | ||| As such, high-performance lexers can be written manually, while
   5 | ||| many convenient combinators exist for less performance-critical
   6 | ||| applications.
   7 | module Text.Lex.Core
   8 | 
   9 | import Data.Bool.Rewrite
  10 | import public Data.List
  11 | import public Data.SnocList
  12 | import public Data.Vect
  13 | import public Text.Bounds
  14 | import public Text.ParseError
  15 | import public Text.Lex.Shift
  16 | 
  17 | %default total
  18 | 
  19 | --------------------------------------------------------------------------------
  20 | --          Recognise
  21 | --------------------------------------------------------------------------------
  22 | 
  23 | export infixl 8 <++>
  24 | 
  25 | public export
  26 | data Recognise : (strict : Bool) -> Type where
  27 |   Lift      : Shifter b -> Recognise b
  28 |   (<+>)     : Recognise b1 -> Recognise b2 -> Recognise (b1 || b2)
  29 |   (<++>)    : Recognise True -> Inf (Recognise b) -> Recognise True
  30 |   (<|>)     : Recognise b1 -> Lazy (Recognise b2) -> Recognise (b1 && b2)
  31 | 
  32 | --------------------------------------------------------------------------------
  33 | --          Conversions
  34 | --------------------------------------------------------------------------------
  35 | 
  36 | public export %inline
  37 | swapOr : {0 x,y : _} -> Recognise (x || y) -> Recognise (y || x)
  38 | swapOr = swapOr (\k => Recognise k)
  39 | 
  40 | public export %inline
  41 | orSame : {0 x : _} -> Recognise (x || x) -> Recognise x
  42 | orSame = orSame (\k => Recognise k)
  43 | 
  44 | public export %inline
  45 | orTrue : {0 x : _} -> Recognise (x || True) -> Recognise True
  46 | orTrue = orTrue (\k => Recognise k)
  47 | 
  48 | public export %inline
  49 | orFalse : {0 x : _} -> Recognise (x || False) -> Recognise x
  50 | orFalse = orFalse (\k => Recognise k)
  51 | 
  52 | public export %inline
  53 | swapAnd : {0 x,y : _} -> Recognise (x && y) -> Recognise (y && x)
  54 | swapAnd = swapAnd (\k => Recognise k)
  55 | 
  56 | public export %inline
  57 | andSame : {0 x : _} -> Recognise (x && x) -> Recognise x
  58 | andSame = andSame (\k => Recognise k)
  59 | 
  60 | public export %inline
  61 | andTrue : {0 x : _} -> Recognise (x && True) -> Recognise x
  62 | andTrue = andTrue (\k => Recognise k)
  63 | 
  64 | public export %inline
  65 | andFalse : {0 x : _} -> Recognise (x && False) -> Recognise False
  66 | andFalse = andFalse (\k => Recognise k)
  67 | 
  68 | --------------------------------------------------------------------------------
  69 | --          Core Lexers
  70 | --------------------------------------------------------------------------------
  71 | 
  72 | public export %inline
  73 | autoLift : AutoShift b -> Recognise b
  74 | autoLift f = Lift $ \st,ts => orFalse $ f ts @{Same}
  75 | 
  76 | ||| Alias for `Recognise True Char`.
  77 | public export
  78 | 0 Lexer : Type
  79 | Lexer = Recognise True
  80 | 
  81 | public export
  82 | run :
  83 |      Recognise b
  84 |   -> (st : SnocList Char)
  85 |   -> (ts : List Char)
  86 |   -> (0 acc : SuffixAcc ts)
  87 |   -> ShiftRes b st ts
  88 | run (Lift f)  st ts _ = f st ts
  89 | run (x <+> y) st ts a@(SA r) = case run x st ts a of
  90 |   Succ {pre} ts2 @{p} => case p of
  91 |     Same => run y pre ts a
  92 |     SH q =>
  93 |       let su := suffix {b = True} (SH q)
  94 |        in swapOr $ run y pre ts2 r `trans` SH q
  95 |   Stop start errEnd r        => Stop start errEnd r
  96 | run (x <++> y) st ts a@(SA r) = case run x st ts a of
  97 |   Succ {pre} ts2 @{p} =>
  98 |     let su := suffix {b = True} p
  99 |      in swapOr $ run y pre ts2 r `trans` p
 100 |   Stop start errEnd r        => Stop start errEnd r
 101 | run (x <|> y) st ts a = run x st ts a <|> run y st ts a
 102 | 
 103 | ||| Lexer succeeding always without consuming input
 104 | public export %inline
 105 | empty : Recognise False
 106 | empty = Lift $ \sc,cs => Succ cs
 107 | 
 108 | ||| Renders the given lexer optional.
 109 | public export %inline
 110 | opt : Recognise True -> Recognise False
 111 | opt l = l <|> empty
 112 | 
 113 | ||| Positive look-ahead. Does not consume any input.
 114 | public export
 115 | expect : Recognise b -> Recognise False
 116 | expect r = Lift $ \sc,cs => case run r sc cs suffixAcc of
 117 |   Succ _     => Succ cs
 118 |   Stop x y z => Stop x y z
 119 | 
 120 | ||| Negative look-ahead. Does not consume any input.
 121 | public export
 122 | reject : Recognise b -> Recognise False
 123 | reject r = Lift $ \sc,cs => case run r sc cs suffixAcc of
 124 |   Stop {} => Succ cs
 125 |   Succ {} => weaken $ fail sc cs
 126 | 
 127 | public export %inline
 128 | seqSame : Recognise b -> Recognise b -> Recognise b
 129 | seqSame x y = orSame $ x <+> y
 130 | 
 131 | public export %inline
 132 | altSame : Recognise b -> Recognise b -> Recognise b
 133 | altSame x y =  andSame $ x <|> y
 134 | 
 135 | ||| The lexer which always fails.
 136 | public export
 137 | fail : Recognise True
 138 | fail = Lift fail
 139 | 
 140 | ||| Runs the given lexer zero or more times.
 141 | public export
 142 | many : Recognise True -> Recognise False
 143 | 
 144 | ||| Runs the given lexer several times, but at least once.
 145 | public export
 146 | some : Recognise True -> Recognise True
 147 | 
 148 | many r = opt (some r)
 149 | 
 150 | some r = r <++> many r
 151 | 
 152 | ||| Lexer consuming one item if it fulfills the given predicate.
 153 | public export %inline
 154 | pred : (Char -> Bool) -> Recognise True
 155 | pred f = autoLift $ one f
 156 | 
 157 | ||| Lexer consuming items while they fulfill the given predicate.
 158 | ||| This is an optimized version of `some . pred`.
 159 | public export %inline
 160 | preds : (Char -> Bool) -> Recognise True
 161 | preds f = autoLift $ takeWhile1 f
 162 | 
 163 | ||| Recogniser consuming items while they fulfill the given predicate.
 164 | ||| This is an optimized version of `many . pred`.
 165 | public export %inline
 166 | preds0 : (Char -> Bool) -> Recognise False
 167 | preds0 = opt . preds
 168 | 
 169 | public export
 170 | concatMap :
 171 |      (a -> Recognise c)
 172 |   -> (xs : List a)
 173 |   -> {auto 0 prf : NonEmpty xs}
 174 |   -> Recognise c
 175 | concatMap f (x :: [])          = f x
 176 | concatMap f (x :: xs@(_ :: _)) = seqSame (f x) (concatMap f xs)
 177 | 
 178 | public export %inline
 179 | choiceMap : Foldable t => (a -> Recognise True) -> t a -> Recognise True
 180 | choiceMap f = foldl (\v,e => altSame v $ f e) fail
 181 | 
 182 | public export %inline
 183 | choice : Foldable t => t (Recognise True) -> Recognise True
 184 | choice = choiceMap id
 185 | 
 186 | --------------------------------------------------------------------------------
 187 | --          Lex
 188 | --------------------------------------------------------------------------------
 189 | 
 190 | public export
 191 | 0 TokenMap : (tokenType : Type) -> Type
 192 | TokenMap tt = List (Recognise True, SnocList Char -> tt)
 193 | 
 194 | public export %inline
 195 | step : Recognise True -> (SnocList Char -> a) -> Tok True e a
 196 | step x f cs = suffix f $ run x [<] cs suffixAcc
 197 | 
 198 | public export
 199 | first : (ps : TokenMap a) -> {auto 0 prf : NonEmpty ps} -> Tok True e a
 200 | first ((f,g) :: [])         cs = step f g cs
 201 | first ((f,g) :: t@(_ :: _)) cs = step f g cs <|> first t cs
 202 |