0 | module HTTP.Parser.Header
  1 |
  2 | import Data.Buffer
  3 | import Data.Either
  4 | import Data.SortedMap
  5 | import Derive.Prelude
  6 | import HTTP.Header.Types
  7 | import HTTP.Parser.Util
  8 | import Syntax.T1
  9 | import Text.ILex.DStack
 10 |
 11 | %default total
 12 | %hide Data.Linear.(.)
 13 | %language ElabReflection
 14 |
 15 | mtype : ByteString -> (String,String)
 16 | mtype bs = let (x,y) := break (47 ==) bs in (toString x, toString $ drop 1 y)
 17 |
 18 | md : ByteString -> MediaDesc
 19 | md bs = let (x,y) := mtype bs in MD x y
 20 |
 21 | mt : ByteString -> MediaType
 22 | mt bs = let (x,y) := mtype bs in MT x y
 23 |
 24 | mdstar : ByteString -> MediaDesc
 25 | mdstar = MDStar . toString . dropEnd 2
 26 |
 27 | --------------------------------------------------------------------------------
 28 | -- Regular Expressions
 29 | -- (see Appendix A from [RFC 91110](https://www.rfc-editor.org/rfc/rfc9110.txt)
 30 | --------------------------------------------------------------------------------
 31 |
 32 | qdtext : RExp True
 33 | qdtext =
 34 |   plus $ HTAB <|> SP <|> '!' <|> range32 0x23 0x5b <|> range32 0x5d 0x7e
 35 |
 36 | quotedPair : RExp True
 37 | quotedPair = '\\' >> (HTAB <|> SP <|> Ch VCHAR)
 38 |
 39 | field : RExp True
 40 | field = plus (HTAB <|> SP <|> Ch VCHAR) >> CRLF
 41 |
 42 | public export
 43 | dayname : RExp True
 44 | dayname = "Mon" <|> "Tue" <|> "Wed" <|> "Thu" <|> "Fri" <|> "Sat" <|> "Sun"
 45 |
 46 | export
 47 | daynameL : RExp True
 48 | daynameL =
 49 |      "Monday"
 50 |  <|> "Tuesday"
 51 |  <|> "Wednesday"
 52 |  <|> "Thursday"
 53 |  <|> "Friday"
 54 |  <|> "Saturday"
 55 |  <|> "Sunday"
 56 |
 57 | public export
 58 | second : RExp True
 59 | second = digit >> digit
 60 |
 61 | public export
 62 | minute : RExp True
 63 | minute = digit >> digit
 64 |
 65 | public export
 66 | hour : RExp True
 67 | hour = digit >> digit
 68 |
 69 | public export
 70 | timeOfDay : RExp True
 71 | timeOfDay = hour >> ':' >> minute >> ':' >> second
 72 |
 73 | public export
 74 | month : RExp True
 75 | month =
 76 |       "Jan" <|> "Feb" <|> "Mar" <|> "Apr" <|> "May" <|> "Jun"
 77 |   <|> "Jul" <|> "Aug" <|> "Sep" <|> "Oct" <|> "Nov" <|> "Dec"
 78 |
 79 | public export
 80 | year : RExp True
 81 | year = repeat 4 digit
 82 |
 83 | export
 84 | qvalue : RExp True
 85 | qvalue =
 86 |       ('0' >> opt ('.' >> atmost 3 digit))
 87 |   <|> ('1' >> opt ('.' >> atmost 3 '0'))
 88 |
 89 | token : RExp True
 90 | token = plus (alphaNum <|> Ch tokenChar)
 91 |
 92 | --------------------------------------------------------------------------------
 93 | -- Headers Parser
 94 | --------------------------------------------------------------------------------
 95 |
 96 | public export
 97 | data HState : SnocList Type -> Type where
 98 |   HMap    : HState [<HeaderMap]
 99 |   HNam    : HState [<String]
100 |   HPar    : HState [<SnocList Parameter]
101 |   HParS   : HState [<Void]
102 |   HParN   : HState [<SnocList Parameter,String]
103 |   HParQ   : HState [<Void]
104 |   HVal1   : HState [<]
105 |   HVal    : HState [<String]
106 |   HAcc    : HState [<SnocList MediaRange]
107 |   HAccD   : HState [<SnocList MediaRange,MediaDesc]
108 |   HField  : HState [<Void]
109 |   HStr    : HState [<Void]
110 |   HNat    : HState [<Nat]
111 |   HMT     : HState [<]
112 |   HMT1    : HState [<MediaType]
113 |   HCD     : HState [<]
114 |   HCD1    : HState [<String]
115 |   HEnd    : HState [<Void]
116 |   HErr    : HState [<]
117 |
118 | %runElab deriveIndexed "HState" [Show,ConIndex]
119 |
120 | public export
121 | data HRes : HState st -> Stack False HState st -> Type -> Type where
122 |   RMap  : HRes HMap  [<SortedMap.empty] HeaderMap
123 |   RAcc  : HRes HAcc  [<[<]]  (List MediaRange)
124 |   RConL : HRes HNat  [<0]    Nat
125 |   RConT : HRes HMT   [<]     ContentType
126 |   RConD : HRes HCD   [<]     ContentDisp
127 |   RVal  : HRes HVal1 [<]     String
128 |
129 | HSz : Bits32
130 | HSz = 1 + cast (conIndexHState HErr)
131 |
132 | inBoundsHState : (s : HState ts) -> (cast (conIndexHState s) < HSz) === True
133 |
134 | export %inline
135 | Cast (HState ts) (Index HSz) where
136 |   cast v = I (cast $ conIndexHState v) @{mkLT $ inBoundsHState v}
137 |
138 | public export
139 | 0 SK : Type -> Type
140 | SK = DStack HState Void
141 |
142 | parameters {auto sk : SK q}
143 |   hfield : ByteString -> StateAct q HState HSz
144 |   hfield b HNam ([<m]:>HMap:<n) = dput HMap [<insert n b m]
145 |   hfield _ st   sx              = derr HErr sx st
146 |
147 |   meddesc : MediaDesc -> StateAct q HState HSz
148 |   meddesc md HAcc sx t = dput HPar (sx:<md:>HAccD:<[<]) t
149 |   meddesc md st   sx t = derr HErr sx st t
150 |
151 |   medtype : MediaType -> StateAct q HState HSz
152 |   medtype m HMT sx t = dput HPar ([<m]:>HMT1:<[<]) t
153 |   medtype m st  sx t = derr HErr sx st t
154 |
155 |   condisp : ByteString -> StateAct q HState HSz
156 |   condisp bs HCD sx t = dput HPar ([<toString bs]:>HCD1:<[<]) t
157 |   condisp _  st  sx t = derr HErr sx st t
158 |
159 |   hendpar : StateAct q HState HSz
160 |   hendpar HPar (sx:<sd:<md:>HAccD:<sp) = dput HAcc $ sx:<(sd:<MR md (sp<>>[]))
161 |   hendpar st   sx                      = derr HErr sx st
162 |
163 |   pname : String -> StateAct q HState HSz
164 |   pname s HPar sx = dput HParN (sx:<s)
165 |   pname s st   sx = derr HErr sx st
166 |
167 |   pvalue : String -> StateAct q HState HSz
168 |   pvalue v HParN (sx:<sp:<n) = dput HPar $ sx:<(sp:<P n v)
169 |   pvalue v HVal1 sx          = dput HVal [<v]
170 |   pvalue v st    sx          = derr HErr sx st
171 |
172 |   qval : Double -> StateAct q HState HSz
173 |   qval v HPar (sx:<sp) = dput HPar $ sx:<(sp:<Q v)
174 |   qval v st   sx       = derr HErr sx st
175 |
176 |   %inline
177 |   hstr : String -> StateAct q HState HSz
178 |   hstr = pvalue
179 |
180 | spaced : Steps q HSz SK -> DFA q HSz SK
181 | spaced ss = dfa $ [ignore' (plus WSP)] ++ ss
182 |
183 | headerTrans : Lex1 q HSz SK
184 | headerTrans =
185 |   lex1
186 |     [ entry HMap $ dfa [string token $ dpush HNam . toUpper, step' CRLF HEnd]
187 |     , entry HNam $ dfa [step' ':' HField]
188 |     , entry HAcc $ spaced
189 |         [ step' ',' HAcc
190 |         , step "*/*" $ dact (meddesc MDAny)
191 |         , bytes (token >> "/*") $ dact . meddesc . mdstar
192 |         , bytes (token >> "/" >> token) $ dact . meddesc . md
193 |         ]
194 |     , entry HPar $ spaced [step' ';' HParS, step ',' $ dact hendpar]
195 |     , entry HParS $ spaced
196 |         [ step' ';' HParS
197 |         , step ',' $ dact hendpar
198 |         , step' (like "q=") HParQ
199 |         , string token $ dact . pname
200 |         ]
201 |     , entry HParN $ dfa [step' '=' HVal1]
202 |     , entry HParQ $ dfa
203 |         [ step "1." $ dact $ qval 1.0
204 |         , step "0." $ dact $ qval 0.0
205 |         , bytes qvalue $ dact . qval . cast . toString
206 |         ]
207 |     , entry HVal1 $ dfa [string token $ dact . pvalue, opn' '"' HStr]
208 |     , entry HNat $ dfa [bytes (plus digit) $ \bs => dput HNat [<cast $ integer bs]]
209 |     , entry HMT $ dfa [bytes (token >> "/" >> token) $ dact . medtype . mt]
210 |     , entry HCD $ dfa [bytes token $ dact . condisp]
211 |     , entry HStr $ dfa
212 |         [ closeStr '"' $ dact . hstr
213 |         , string qdtext $ pushStr HStr
214 |         , bytes quotedPair $ pushStr HStr . toString . drop 1
215 |         ]
216 |     , entry HField $ spaced [bytes field $ dact . hfield . trim]
217 |     ]
218 |
219 | headerErr : Arr32 HSz (SK q -> F1 q (BBErr Void))
220 | headerErr = errs []
221 |
222 | end : HRes st x t -> HState ts -> Stack b HState ts -> Maybe t
223 | end RMap  HMap   [<m]                 = Just m
224 | end RAcc  HAcc   [<sm]                = Just $ sm<>>[]
225 | end RAcc  HAccD  [<sm,d]              = Just $ sm<>>[MR d []]
226 | end RVal  HVal   [<s]                 = Just s
227 | end RConL HNat   [<n]                 = Just n
228 | end RConT HMT1   [<m]                 = Just $ CT m []
229 | end RConD HCD1   [<v]                 = Just $ CD v []
230 | end RAcc  HPar   ([<sm,d]:>HAccD:<sp) = Just $ sm<>>[MR d $ sp<>>[]]
231 | end RConT HPar   ([<m]:>HMT1:<sp)     = Just $ CT m (sp <>>[])
232 | end RConD HPar   ([<s]:>HCD1:<sp)     = Just $ CD s (sp <>>[])
233 | end _     _      _                    = Nothing
234 |
235 | headerEOI : HRes st x v -> Index HSz -> SK q -> F1 q (Either (BBErr Void) v)
236 | headerEOI res sk s t =
237 |   let (x:>st) # t := read1 s.stack_ t
238 |       Nothing     := end res st x | Just v => Right v # t
239 |    in arrFail SK headerErr sk s t
240 |
241 | public export
242 | header : {st : _} -> {x : _} -> HRes st x t -> P1 q (BBErr Void) t
243 | header res =
244 |   P (cast st) (init $ x:>st) headerTrans (\x => (Nothing #))
245 |     headerErr (headerEOI res)
246 |
247 | export
248 | headerMay : {st : _} -> {x : _} -> HRes st x t -> ByteString -> Maybe t
249 | headerMay res bs = eitherToMaybe $ parseBytes (header res) Virtual bs
250 |
251 | export
252 | testHeader : {st : _} -> {x : _} -> HRes st x v -> Show v => String -> IO ()
253 | testHeader res s =
254 |   case parseString (header res) Virtual s of
255 |     Left x => putStrLn "\{x}"
256 |     Right res => printLn res
257 |
258 | --------------------------------------------------------------------------------
259 | -- Proofs
260 | --------------------------------------------------------------------------------
261 |
262 | inBoundsHState HMap    = Refl
263 | inBoundsHState HNam    = Refl
264 | inBoundsHState HPar    = Refl
265 | inBoundsHState HParQ   = Refl
266 | inBoundsHState HParS   = Refl
267 | inBoundsHState HParN   = Refl
268 | inBoundsHState HVal    = Refl
269 | inBoundsHState HVal1   = Refl
270 | inBoundsHState HAcc    = Refl
271 | inBoundsHState HAccD   = Refl
272 | inBoundsHState HField  = Refl
273 | inBoundsHState HStr    = Refl
274 | inBoundsHState HEnd    = Refl
275 | inBoundsHState HNat    = Refl
276 | inBoundsHState HMT     = Refl
277 | inBoundsHState HMT1    = Refl
278 | inBoundsHState HCD     = Refl
279 | inBoundsHState HCD1    = Refl
280 | inBoundsHState HErr    = Refl
281 |