
   0 | module Text.Lex.Shift
   1 | 
   2 | import Data.List
   3 | import Data.String
   4 | import Data.Nat
   5 | import public Text.Lex.Manual
   6 | import public Data.List.Shift
   7 | 
   8 | %default total
   9 | 
  10 | ||| Shift the position by a number of columns represented by
  11 | ||| a `Shift` value. This assumes, that no line break was "shifted".
  12 | public export %inline
  13 | shift : Position -> Shift b t sx xs sy ys -> Position
  14 | shift p s = addCol (toNat s) p
  15 | 
  16 | --------------------------------------------------------------------------------
  17 | --          ShiftRes
  18 | --------------------------------------------------------------------------------
  19 | 
  20 | ||| Result of running a lexer once: The lexer either stops, when
  21 | ||| it can no longer consume any characters, or it shifts some characters
  22 | ||| from the head of the list of remaining characters to the tail of the
  23 | ||| snoclist of already recognised characters.
  24 | |||
  25 | ||| @ st     : the initial snoclist of already recognised characters
  26 | ||| @ ts     : the initial list of remaining characters
  27 | public export
  28 | data ShiftRes :
  29 |      (b  : Bool)
  30 |   -> (sc : SnocList Char)
  31 |   -> (cs : List Char)
  32 |   -> Type where
  33 |   Succ :
  34 |        {0 b     : Bool}
  35 |     -> {0 st    : SnocList Char}
  36 |     -> {0 ts    : List Char}
  37 |     -> {pre     : SnocList Char}
  38 |     -> (post    : List Char)
  39 |     -> {auto sh : Shift b Char pre post st ts}
  40 |     -> ShiftRes b st ts
  41 | 
  42 |   Stop :
  43 |        {0 b         : Bool}
  44 |     -> {0 st,se,ee  : SnocList Char}
  45 |     -> {ts,errStart : List Char}
  46 |     -> (start       : Shift False Char se errStart st ts)
  47 |     -> (0 errEnd    : List Char)
  48 |     -> {auto end    : Shift False Char ee errEnd se errStart}
  49 |     -> InnerError Void
  50 |     -> ShiftRes b st ts
  51 | 
  52 | public export %inline
  53 | suffix : (SnocList Char -> a) -> ShiftRes True [<] cs -> LexRes True cs e a
  54 | suffix f (Succ {pre} post @{sh}) = Succ (f pre) post @{suffix sh} 
  55 | suffix f (Stop s e x @{sh})      = Fail (suffix s) e (fromVoid x) @{suffix sh}
  56 | 
  57 | --------------------------------------------------------------------------------
  58 | --         Conversions
  59 | --------------------------------------------------------------------------------
  60 | 
  61 | public export
  62 | swapOr : {0 x,y : _} -> ShiftRes (x || y) st ts -> ShiftRes (y || x) st ts
  63 | swapOr = swapOr (\k => ShiftRes k st ts)
  64 | 
  65 | public export %inline
  66 | orSame : {0 x : _} -> ShiftRes (x || x) st ts -> ShiftRes x st ts
  67 | orSame = orSame (\k => ShiftRes k st ts)
  68 | 
  69 | public export %inline
  70 | orTrue : {0 x : _} -> ShiftRes (x || True) st ts -> ShiftRes True st ts
  71 | orTrue = orTrue (\k => ShiftRes k st ts)
  72 | 
  73 | public export %inline
  74 | orFalse : {0 x : _} -> ShiftRes (x || False) st ts -> ShiftRes x st ts
  75 | orFalse = orFalse (\k => ShiftRes k st ts)
  76 | 
  77 | public export %inline
  78 | swapAnd : {0 x,y : _} -> ShiftRes (x && y) st ts -> ShiftRes (y && x) st ts
  79 | swapAnd = swapAnd (\k => ShiftRes k st ts)
  80 | 
  81 | public export %inline
  82 | andSame : {0 x : _} -> ShiftRes (x && x) st ts -> ShiftRes x st ts
  83 | andSame = andSame (\k => ShiftRes k st ts)
  84 | 
  85 | public export %inline
  86 | andTrue : {0 x : _} -> ShiftRes (x && True) st ts -> ShiftRes x st ts
  87 | andTrue = andTrue (\k => ShiftRes k st ts)
  88 | 
  89 | public export %inline
  90 | andFalse : {0 x : _} -> ShiftRes (x && False) st ts -> ShiftRes False st ts
  91 | andFalse = andFalse (\k => ShiftRes k st ts)
  92 | 
  93 | public export
  94 | weaken : {0 x : _} -> ShiftRes x st ts -> ShiftRes False st ts
  95 | weaken (Succ xs @{p}) = Succ xs @{weaken p}
  96 | weaken (Stop s e r) = Stop s e r
  97 | 
  98 | public export
  99 | weakens : {0 x : _} -> ShiftRes True st ts -> ShiftRes x st ts
 100 | weakens (Succ xs @{p}) = Succ xs @{weakens p}
 101 | weakens (Stop s e r) = Stop s e r
 102 | 
 103 | public export
 104 | and1 : {0 x : _} -> ShiftRes x st ts -> ShiftRes (x && y) st ts
 105 | and1 (Succ xs @{p})= Succ xs @{and1 p}
 106 | and1 (Stop s e r)  = Stop s e r
 107 | 
 108 | public export %inline
 109 | and2 : {0 x : _} -> ShiftRes x st ts -> ShiftRes (y && x) st ts
 110 | and2 r = swapAnd $ and1 r
 111 | 
 112 | public export %inline
 113 | trans :
 114 |      {ys : _}
 115 |   -> ShiftRes b1 sx xs
 116 |   -> Shift b2 Char sx xs sy ys
 117 |   -> ShiftRes (b1 || b2) sy ys
 118 | trans (Succ ts @{p})    q = Succ ts @{Shift.trans p q}
 119 | trans (Stop x y z @{p}) q = Stop (weaken $ trans x q) y z
 120 | 
 121 | --------------------------------------------------------------------------------
 122 | --          Combinators
 123 | --------------------------------------------------------------------------------
 124 | 
 125 | public export
 126 | (<|>) :
 127 |      ShiftRes b1 sx xs
 128 |   -> Lazy (ShiftRes b2 sx xs)
 129 |   -> ShiftRes (b1 && b2) sx xs
 130 | s@(Succ {}) <|> _ = and1 s
 131 | _           <|> r = and2 r
 132 | 
 133 | --------------------------------------------------------------------------------
 134 | --          Shifters
 135 | --------------------------------------------------------------------------------
 136 | 
 137 | ||| A `Shifter` is a function that moves items from the head of a list
 138 | ||| to the tail of a snoclist.
 139 | |||
 140 | ||| A lexer is just a fancy wrapper around a `Shifter`, and *running* a
 141 | ||| lexer (via function `run`) leads to the underlying `Shifter`
 142 | ||| (see `Text.Lex.Core`).
 143 | public export
 144 | 0 Shifter : (b : Bool) -> Type
 145 | Shifter b = (st : SnocList Char) -> (ts : List Char) -> ShiftRes b st ts
 146 | 
 147 | public export
 148 | 0 AutoShift : Bool -> Type
 149 | AutoShift s =
 150 |      {0 b     : Bool}
 151 |   -> {0 giro  : SnocList Char}
 152 |   -> {orig    : List Char}
 153 |   -> {pre     : SnocList Char}
 154 |   -> (post    : List Char)
 155 |   -> {auto sh : Shift b Char pre post giro orig}
 156 |   -> ShiftRes (s || b) giro orig
 157 | 
 158 | public export
 159 | range :
 160 |      {0 b1,b2 : Bool}
 161 |   -> {0 giro,ruc,tser : SnocList Char}
 162 |   -> {orig,cur   : List Char}
 163 |   -> (err        : InnerError Void)
 164 |   -> (shiftCur   : Shift b1 Char ruc cur giro orig)
 165 |   -> (0 rest     : List Char)
 166 |   -> {auto sr    : Shift False Char tser rest ruc cur}
 167 |   -> ShiftRes b2 giro orig
 168 | range r sc rest = Stop (weaken sc) rest r
 169 | 
 170 | public export %inline
 171 | invalidEscape :
 172 |      {0 b1,b2 : Bool}
 173 |   -> {0 giro,ruc,tser : SnocList Char}
 174 |   -> {orig,cur   : List Char}
 175 |   -> (shiftCur   : Shift b1 Char ruc cur giro orig)
 176 |   -> (0 rest     : List Char)
 177 |   -> {auto sr    : Shift False Char tser rest ruc cur}
 178 |   -> ShiftRes b2 giro orig
 179 | invalidEscape = range InvalidEscape
 180 | 
 181 | public export %inline
 182 | unknownRange :
 183 |      {0 b1,b2 : Bool}
 184 |   -> {0 giro,ruc,tser : SnocList Char}
 185 |   -> {orig,cur   : List Char}
 186 |   -> (shiftCur   : Shift b1 Char ruc cur giro orig)
 187 |   -> (0 rest     : List Char)
 188 |   -> {auto sr    : Shift False Char tser rest ruc cur}
 189 |   -> ShiftRes b2 giro orig
 190 | unknownRange sc ee = range (Unknown . packPrefix $ suffix sr) sc ee
 191 | 
 192 | public export %inline
 193 | single :
 194 |      {0 b,bres      : Bool}
 195 |   -> {0 giro,ruc    : SnocList Char}
 196 |   -> {c             : Char}
 197 |   -> {orig,errEnd   : List Char}
 198 |   -> (err           : InnerError Void)
 199 |   -> (shiftCur      : Shift b Char ruc (c::errEnd) giro orig)
 200 |   -> ShiftRes bres giro orig
 201 | single r p = range r p errEnd
 202 | 
 203 | public export %inline
 204 | unknown :
 205 |      {0 b,bres      : Bool}
 206 |   -> {0 giro,ruc    : SnocList Char}
 207 |   -> {c             : Char}
 208 |   -> {orig,errEnd   : List Char}
 209 |   -> (shiftCur      : Shift b Char ruc (c::errEnd) giro orig)
 210 |   -> ShiftRes bres giro orig
 211 | unknown p = unknownRange p errEnd
 212 | 
 213 | public export %inline
 214 | failCharClass :
 215 |      {0 b,bres      : Bool}
 216 |   -> {0 giro,ruc    : SnocList Char}
 217 |   -> {c             : Char}
 218 |   -> {orig,errEnd   : List Char}
 219 |   -> (class         : CharClass)
 220 |   -> (shiftCur      : Shift b Char ruc (c::errEnd) giro orig)
 221 |   -> ShiftRes bres giro orig
 222 | failCharClass cc = single (ExpectedChar cc)
 223 | 
 224 | public export %inline
 225 | failDigit :
 226 |      {0 b,bres      : Bool}
 227 |   -> {0 giro,ruc    : SnocList Char}
 228 |   -> {c             : Char}
 229 |   -> {orig,errEnd   : List Char}
 230 |   -> (tpe           : DigitType)
 231 |   -> (shiftCur      : Shift b Char ruc (c::errEnd) giro orig)
 232 |   -> ShiftRes bres giro orig
 233 | failDigit = failCharClass . Digit
 234 | 
 235 | public export
 236 | eoiAt :
 237 |      {0 b1,b2 : Bool}
 238 |   -> {0 ruc,giro : SnocList Char}
 239 |   -> {orig       : List Char}
 240 |   -> (shiftCur   : Shift b1 Char ruc [] giro orig)
 241 |   -> ShiftRes b2 giro orig
 242 | eoiAt sc = range EOI sc []
 243 | 
 244 | --------------------------------------------------------------------------------
 245 | --          General Purpose Shifters
 246 | --------------------------------------------------------------------------------
 247 | 
 248 | ||| Shifter that recognises the empty String
 249 | public export
 250 | eoi : Shifter False
 251 | eoi _ []      = Succ []
 252 | eoi _ (x::xs) = single ExpectedEOI Same
 253 | 
 254 | ||| Shifter that always fails
 255 | public export
 256 | fail : Shifter True
 257 | fail _ []      = eoiAt Same
 258 | fail _ (x::xs) = unknown Same
 259 | 
 260 | ||| A shifter that moves exactly one value, if
 261 | ||| it fulfills the given predicate.
 262 | public export
 263 | one : (Char -> Bool) -> AutoShift True
 264 | one f (x :: xs) = if f x then Succ xs else unknown sh
 265 | one _ []        = eoiAt sh
 266 | 
 267 | ||| A shifter that moves items while the given predicate returns
 268 | ||| `True`
 269 | public export
 270 | takeWhile : (Char -> Bool) -> AutoShift False
 271 | takeWhile f (x :: xs) = if f x then takeWhile f xs else Succ (x::xs)
 272 | takeWhile f []        = Succ []
 273 | 
 274 | ||| A strict version of `takeWhile`, which moves at least one item.
 275 | public export
 276 | takeWhile1 : (Char -> Bool) -> AutoShift True
 277 | takeWhile1 f (x :: xs) = if f x then takeWhile f xs else unknown sh
 278 | takeWhile1 f []        = eoiAt sh
 279 | 
 280 | ||| A shifter that moves items while the give predicate returns
 281 | ||| `False`
 282 | public export
 283 | takeUntil : (Char -> Bool) -> AutoShift False
 284 | takeUntil f (x :: xs) = if f x then Succ (x::xs) else takeUntil f xs
 285 | takeUntil f []        = Succ []
 286 | 
 287 | ||| A strict version of `takeUntil`, which moves at least one item.
 288 | public export
 289 | takeUntil1 : (Char -> Bool) -> AutoShift True
 290 | takeUntil1 f (x :: xs) = if f x then unknown sh else takeUntil f xs
 291 | takeUntil1 f []        = eoiAt sh
 292 | 
 293 | ||| A shifter that moves digits.
 294 | public export
 295 | digits : AutoShift False
 296 | digits (x :: xs) = if isDigit x then digits xs else Succ (x::xs)
 297 | digits []        = Succ []
 298 | 
 299 | ||| A strict version of `digits`.
 300 | public export
 301 | digits1 : AutoShift True
 302 | digits1 (x :: xs) = if isDigit x then digits xs else failDigit Dec sh
 303 | digits1 []        = eoiAt sh
 304 | 
 305 | ||| A shifter that moves an integer prefix
 306 | public export
 307 | int : AutoShift True
 308 | int ('-' :: xs) = digits1 {b} xs
 309 | int xs          = digits1 {b} xs
 310 | 
 311 | ||| Like `int` but also allows an optional leading `'+'` character.
 312 | public export
 313 | intPlus : AutoShift True
 314 | intPlus ('+' :: xs) = digits1 {b} xs
 315 | intPlus xs          = int {b} xs
 316 | 
 317 | dot,rest,digs,exp : AutoShift False
 318 | exp ('e' :: xs) = weakens $ intPlus {b} xs
 319 | exp ('E' :: xs) = weakens $ intPlus {b} xs
 320 | exp (x   :: xs) =
 321 |   if isDigit x then unknownRange Same xs else Succ (x::xs)
 322 | exp []          = Succ []
 323 | 
 324 | dot (x :: xs) = if isDigit x then dot xs else exp (x::xs)
 325 | dot []        = Succ []
 326 | 
 327 | rest ('.'::x::xs) =
 328 |   if isDigit x then dot xs else failDigit Dec (shift sh)
 329 | rest ('.'::[])    = eoiAt (shift sh)
 330 | rest xs           = exp xs
 331 | 
 332 | digs (x :: xs) = if isDigit x then digs xs else rest (x::xs)
 333 | digs []        = Succ []
 334 | 
 335 | ||| A shifter for recognizing JSON numbers
 336 | public export
 337 | number : Shifter True
 338 | number sc ('-' :: '0' :: xs) = rest xs
 339 | number sc ('-' :: x   :: xs) =
 340 |   if isDigit x then digs xs else failDigit Dec (shift Same)
 341 | number sc ('0' :: xs)        = rest xs
 342 | number sc (x          :: xs) = if isDigit x then digs xs else unknown Same
 343 | number sc []                 = eoiAt Same
 344 | 
 345 | public export
 346 | double : Tok True e Double
 347 | double cs = suffix (cast . cast {to = String}) $ number [<] cs
 348 | 
 349 | public export
 350 | take : (n : Nat) -> {auto 0 p : IsSucc n} -> AutoShift True
 351 | take (S Z)       (x::xs)   = Succ xs
 352 | take (S k@(S _)) (x :: xs) = take {b} k xs
 353 | take (S k) []              = eoiAt sh
 354 | 
 355 | public export
 356 | tail : AutoShift True
 357 | tail (x::xs)   = Succ xs
 358 | tail []        = eoiAt sh
 359 | 
 360 | public export
 361 | exact : (ts : List Char) -> {auto 0 p : NonEmpty ts} -> AutoShift True
 362 | exact (v :: vs) (x :: xs) = case v == x of
 363 |   True => case vs of
 364 |     []        => Succ xs
 365 |     ws@(_::_) => exact {b} ws xs
 366 |   False => single (Expected [String.singleton v] (String.singleton x)) sh
 367 | exact (v :: vs) []        = eoiAt sh
 368 | 
 369 | str : AutoShift True
 370 | str ('"'       :: xs) = Succ xs
 371 | str ('\\' :: x :: xs) = str {b} xs
 372 | str (x         :: xs) = str {b} xs
 373 | str []                = eoiAt sh
 374 | 
 375 | public export
 376 | string : Shifter True
 377 | string sc ('"' :: xs) = str {b = True} xs
 378 | string sc (h   :: t)  = single (Expected ["\""] (String.singleton h)) Same
 379 | string sc []          = eoiAt Same
 380 |