
   0 | module HTTP.Parser.Util
   1 | 
   2 | import Data.Bits
   3 | import public Text.ILex
   4 | 
   5 | %default total
   6 | 
   7 | public export %inline
   8 | byte_percent : Bits8
   9 | byte_percent = 37
  10 | 
  11 | public export %inline
  12 | byte_equals : Bits8
  13 | byte_equals = 61
  14 | 
  15 | public export %inline
  16 | byte_questionmark : Bits8
  17 | byte_questionmark = 63
  18 | 
  19 | public export %inline
  20 | byte_ampersand : Bits8
  21 | byte_ampersand = 38
  22 | 
  23 | export
  24 | hex : Bits8 -> Bits8
  25 | hex b = if b < 10 then byte_0 + b else byte_A + b - 10
  26 | 
  27 | export
  28 | escape : Bits8 -> ByteString
  29 | escape b = pack [byte_percent, hex (shiftR b 4 .&. 0xf), hex (b .&. 0xf)]
  30 | 
  31 | ||| URI-escapes all bytes for which the given predicate does
  32 | ||| not return `True`.
  33 | |||
  34 | ||| An escaped byte is represented as two hexadecimal digits prefixed by
  35 | ||| a "percent" character ('%').
  36 | export
  37 | uriEscape : (Bits8 -> Bool) -> ByteString -> ByteString
  38 | uriEscape p = go [<]
  39 |   where
  40 |     go : SnocList ByteString -> ByteString -> ByteString
  41 |     go sx bs =
  42 |       case break p bs of
  43 |         (pre, BS 0 _)      => fastConcat $ sx <>> [pre]
  44 |         (pre, BS (S k) bv) =>
  45 |           let b := head bv
  46 |            in go (sx :< pre :< escape b) (assert_smaller bs $ BS k $ tail bv)
  47 | 
  48 | ||| Converts all escape sequences (see `uriEscape`) in a byte string
  49 | ||| to the corresponding bytes.
  50 | |||
  51 | ||| Note: This is an internal function and should only be invoked
  52 | |||       with correctly escaped byte strings.
  53 | export
  54 | uriUnescape : ByteString -> ByteString
  55 | uriUnescape = go [<]
  56 |   where
  57 |     go : SnocList ByteString -> ByteString -> ByteString
  58 |     go sx bs =
  59 |       case break (byte_percent ==) bs of
  60 |         (pre, bs2@(BS (S (S (S k))) bv)) =>
  61 |           let b := cast $ 16 * hexdigit (at bv 1) + hexdigit (at bv 2)
  62 |            in go (sx :< pre :< singleton b) (assert_smaller bs $ drop 3 bs2)
  63 |         (pre, _) => fastConcat $ sx <>> [pre]
  64 | 
  65 | --------------------------------------------------------------------------------
  66 | -- Charsets
  67 | -- (see Appendix B from [RFC 5234](https://www.rfc-editor.org/rfc/rfc5234.txt)
  68 | --------------------------------------------------------------------------------
  69 | 
  70 | export %inline
  71 | OCTETT : Set8
  72 | OCTETT = range (range 0x00 0xff)
  73 | 
  74 | export %inline
  75 | ALPHA : Set32
  76 | ALPHA = alpha
  77 | 
  78 | export %inline
  79 | BIT : Set32
  80 | BIT = range $ range 48 49
  81 | 
  82 | export %inline
  83 | DIGIT : Set32
  84 | DIGIT = range $ range 0x30 0x39
  85 | 
  86 | export %inline
  87 | HEXDIG : Set32
  88 | HEXDIG = DIGIT `union` (range (range 65 70) `union` range (range 97 102))
  89 | 
  90 | export %inline
  91 | CHAR : Set32
  92 | CHAR = range $ range 0x01 0x7f
  93 | 
  94 | export %inline
  95 | CTL : Set32
  96 | CTL = range (range 0x00 0x1f) `union` singleton 0x7f
  97 | 
  98 | export %inline
  99 | VCHAR : Set32
 100 | VCHAR = range $ range 0x21 0x7e
 101 | 
 102 | export
 103 | tokenChar : Set32
 104 | tokenChar = chars "!#$%&'*+-.^_`|~"
 105 | 
 106 | --------------------------------------------------------------------------------
 107 | -- Regular Expressions
 108 | -- (see Appendix B from [RFC 5234](https://www.rfc-editor.org/rfc/rfc5234.txt)
 109 | --------------------------------------------------------------------------------
 110 | 
 111 | public export %inline
 112 | CR : RExp True
 113 | CR = Ch $ singleton 0x0d
 114 | 
 115 | public export %inline
 116 | LF : RExp True
 117 | LF = Ch $ singleton 0xa
 118 | 
 119 | public export
 120 | CRLF : RExp True
 121 | CRLF = CR >> LF
 122 | 
 123 | public export %inline
 124 | DQUOTE : RExp True
 125 | DQUOTE = Ch $ singleton 0x22
 126 | 
 127 | public export %inline
 128 | HTAB : RExp True
 129 | HTAB = Ch $ singleton 0x09
 130 | 
 131 | public export %inline
 132 | SP : RExp True
 133 | SP = Ch $ singleton 0x20
 134 | 
 135 | public export
 136 | WSP : RExp True
 137 | WSP = SP <|> HTAB
 138 | 
 139 | ||| Optional whitespace
 140 | export
 141 | OWS : RExp False
 142 | OWS = star $ SP <|> HTAB
 143 | 
 144 | export %inline
 145 | BWS : RExp False
 146 | BWS = OWS
 147 | 
 148 | public export
 149 | pctEncoded : RExp True
 150 | pctEncoded = '%' >> Ch HEXDIG >> Ch HEXDIG
 151 |