0 | module HTTP.Parser.Header

  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

 11 | %default total

 12 | %hide Data.Linear.(.)

 13 | %language ElabReflection

 15 | mtype : ByteString -> (String,String)

 16 | mtype bs = let (x,y) := break (47 ==) bs in (toString x, toString $ drop 1 y)

 18 | md : ByteString -> MediaDesc

 19 | md bs = let (x,y) := mtype bs in MD x y

 21 | mt : ByteString -> MediaType

 22 | mt bs = let (x,y) := mtype bs in MT x y

 24 | mdstar : ByteString -> MediaDesc

 25 | mdstar = MDStar . toString . dropEnd 2

 32 | qdtext : RExp True

 33 | qdtext =

 34 |   plus $ HTAB <|> SP <|> '!' <|> range32 0x23 0x5b <|> range32 0x5d 0x7e

 36 | quotedPair : RExp True

 37 | quotedPair = '\\' >> (HTAB <|> SP <|> Ch VCHAR)

 39 | field : RExp True

 40 | field = plus (HTAB <|> SP <|> Ch VCHAR) >> CRLF

 42 | public export

 43 | dayname : RExp True

 44 | dayname = "Mon" <|> "Tue" <|> "Wed" <|> "Thu" <|> "Fri" <|> "Sat" <|> "Sun"

 47 | daynameL : RExp True

 48 | daynameL =

 49 |      "Monday"

 50 |  <|> "Tuesday"

 51 |  <|> "Wednesday"

 52 |  <|> "Thursday"

 53 |  <|> "Friday"

 54 |  <|> "Saturday"

 55 |  <|> "Sunday"

 57 | public export

 58 | second : RExp True

 59 | second = digit >> digit

 61 | public export

 62 | minute : RExp True

 63 | minute = digit >> digit

 65 | public export

 66 | hour : RExp True

 67 | hour = digit >> digit

 69 | public export

 70 | timeOfDay : RExp True

 71 | timeOfDay = hour >> ':' >> minute >> ':' >> second

 73 | public export

 74 | month : RExp True

 75 | month =

 76 |       "Jan" <|> "Feb" <|> "Mar" <|> "Apr" <|> "May" <|> "Jun"

 77 |   <|> "Jul" <|> "Aug" <|> "Sep" <|> "Oct" <|> "Nov" <|> "Dec"

 79 | public export

 80 | year : RExp True

 81 | year = repeat 4 digit

 84 | qvalue : RExp True

 85 | qvalue =

 86 |       ('0' >> opt ('.' >> atmost 3 digit))

 87 |   <|> ('1' >> opt ('.' >> atmost 3 '0'))

 89 | token : RExp True

 90 | token = plus (alphaNum <|> Ch tokenChar)

 96 | public export

 97 | data HState : List Type -> Type where

 98 |   HMap    : HState [HeaderMap]

 99 |   HNam    : HState [String]

100 |   HPar    : HState [SnocList Parameter]

101 |   HParS   : HState [Void]

102 |   HParN   : HState [String,SnocList Parameter]

103 |   HParQ   : HState [Void]

104 |   HVal1   : HState []

105 |   HVal    : HState [String]

106 |   HAcc    : HState [SnocList MediaRange]

107 |   HAccD   : HState [MediaDesc,SnocList MediaRange]

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 []

118 | %runElab deriveIndexed "HState" [Show,ConIndex]

120 | public export

121 | data HRes : HState ts -> Stack False HState ts -> 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

129 | HSz : Bits32

130 | HSz = 1 + cast (conIndexHState HErr)

132 | inBoundsHState : (s : HState ts) -> (cast (conIndexHState s) < HSz) === True

134 | export %inline

135 | Cast (HState ts) (Index HSz) where

136 |   cast v = I (cast $ conIndexHState v) @{mkLT $ inBoundsHState v}

138 | public export

139 | 0 SK : Type -> Type

140 | SK = DStack HState Void

142 | parameters {auto sk : SK q}

143 |   hfield : ByteString -> StateAct q HState HSz

144 |   hfield b HNam (n::HMap:>[m]) = dput HMap [insert n b m]

145 |   hfield _ st   x              = derr HErr st x

147 |   meddesc : MediaDesc -> StateAct q HState HSz

148 |   meddesc md HAcc x t = dput HPar ([<]::HAccD:>md::x) t

149 |   meddesc md st   x t = derr HErr st x t

151 |   medtype : MediaType -> StateAct q HState HSz

152 |   medtype m HMT x t = dput HPar ([<]::HMT1:>[m]) t

153 |   medtype m st  x t = derr HErr st x t

155 |   condisp : ByteString -> StateAct q HState HSz

156 |   condisp bs HCD x t = dput HPar ([<]::HCD1:>[toString bs]) t

157 |   condisp _  st  x t = derr HErr st x t

159 |   hendpar : StateAct q HState HSz

160 |   hendpar HPar (sp::HAccD:>md::sd::x) = dput HAcc $ (sd:<MR md (sp<>>[]))::x

161 |   hendpar st   x                      = derr HErr st x

163 |   pname : String -> StateAct q HState HSz

164 |   pname s HPar x = dput HParN (s::x)

165 |   pname s st   x = derr HErr st x

167 |   pvalue : String -> StateAct q HState HSz

168 |   pvalue v HParN (n::sp::x) = dput HPar $ (sp:<P n v)::x

169 |   pvalue v HVal1 x          = dput HVal [v]

170 |   pvalue v st    x          = derr HErr st x

172 |   qval : Double -> StateAct q HState HSz

173 |   qval v HPar (sp::x) = dput HPar $ (sp:<Q v)::x

174 |   qval v st   x       = derr HErr st x

176 |   hstr : String -> StateAct q HState HSz

177 |   hstr s st x = pvalue s st x

179 | spaced : HState ts -> Steps q HSz SK -> DFA q HSz SK

180 | spaced r ss = dfa $ [conv' (plus WSP) r] ++ ss

182 | headerTrans : Lex1 q HSz SK

183 | headerTrans =

184 |   lex1

185 |     [ entry HMap $ dfa [read token $ dpush HNam . toUpper, newline' CRLF HEnd]

186 |     , entry HNam $ dfa [cexpr' ':' HField]

187 |     , entry HAcc $ spaced HAcc

188 |         [ cexpr' ',' HAcc

189 |         , cexpr "*/*" $ dact (meddesc MDAny)

190 |         , conv (token >> "/*") $ dact . meddesc . mdstar

191 |         , conv (token >> "/" >> token) $ dact . meddesc . md

192 |         ]

193 |     , entry HPar $ spaced HPar [cexpr' ';' HParS, cexpr ',' $ dact hendpar]

194 |     , entry HParS $ spaced HParS

195 |         [ cexpr' ';' HParS

196 |         , cexpr ',' $ dact hendpar

197 |         , cexpr' (like "q=") HParQ

198 |         , read token $ dact . pname

199 |         ]

200 |     , entry HParN $ dfa [cexpr' '=' HVal1]

201 |     , entry HParQ $ dfa

202 |         [ cexpr "1." $ dact $ qval 1.0

203 |         , cexpr "0." $ dact $ qval 0.0

204 |         , conv qvalue $ dact . qval . cast . toString

205 |         ]

206 |     , entry HVal1 $ dfa [read token $ dact . pvalue, copen' '"' HStr]

207 |     , entry HNat $ dfa [conv (plus digit) $ \bs => dput HNat [cast $ integer bs]]

208 |     , entry HMT $ dfa [conv (token >> "/" >> token) $ dact . medtype . mt]

209 |     , entry HCD $ dfa [conv token $ dact . condisp]

210 |     , entry HStr $ dfa

211 |         [ ccloseStr '"' $ dact . hstr

212 |         , read qdtext $ pushStr HStr

213 |         , conv quotedPair $ pushStr HStr . toString . drop 1

214 |         ]

215 |     , entry HField $ spaced HField [convline field $ dact . hfield . trim]

216 |     ]

218 | headerErr : Arr32 HSz (SK q -> F1 q (BoundedErr Void))

219 | headerErr = errs []

221 | end : HRes st x t -> HState ts -> Stack b HState ts -> Maybe t

222 | end RMap  HMap   [m]                 = Just m

223 | end RAcc  HAcc   [sm]                = Just $ sm<>>[]

224 | end RAcc  HAccD  [d,sm]              = Just $ sm<>>[MR d []]

225 | end RVal  HVal   [s]                 = Just s

226 | end RConL HNat   [n]                 = Just n

227 | end RConT HMT1   [m]                 = Just $ CT m []

228 | end RConD HCD1   [v]                 = Just $ CD v []

229 | end RAcc  HPar   (sp::HAccD:>[d,sm]) = Just $ sm<>>[MR d $ sp<>>[]]

230 | end RConT HPar   (sp::HMT1:>[m])     = Just $ CT m (sp <>>[])

231 | end RConD HPar   (sp::HCD1:>[s])     = Just $ CD s (sp <>>[])

232 | end _     _      _                   = Nothing

234 | headerEOI : HRes st x v -> Index HSz -> SK q -> F1 q (Either (BoundedErr Void) v)

235 | headerEOI res sk s t =

236 |   let (st:>x) # t := read1 s.stack_ t

237 |       Nothing     := end res st x | Just v => Right v # t

238 |    in arrFail SK headerErr sk s t

240 | public export

241 | header : {st : _} -> {x : _} -> HRes st x t -> P1 q (BoundedErr Void) t

242 | header res =

243 |   P (cast st) (init $ st:>x) headerTrans (\x => (Nothing #))

244 |     headerErr (headerEOI res)

247 | headerMay : {st : _} -> {x : _} -> HRes st x t -> ByteString -> Maybe t

248 | headerMay res bs = eitherToMaybe $ parseBytes (header res) Virtual bs

251 | testHeader : {st : _} -> {x : _} -> HRes st x v -> Show v => String -> IO ()

252 | testHeader res s =

253 |   case parseString (header res) Virtual s of

254 |     Left x => putStrLn "\{x}"

255 |     Right res => printLn res

261 | inBoundsHState HMap    = Refl

262 | inBoundsHState HNam    = Refl

263 | inBoundsHState HPar    = Refl

264 | inBoundsHState HParQ   = Refl

265 | inBoundsHState HParS   = Refl

266 | inBoundsHState HParN   = Refl

267 | inBoundsHState HVal    = Refl

268 | inBoundsHState HVal1   = Refl

269 | inBoundsHState HAcc    = Refl

270 | inBoundsHState HAccD   = Refl

271 | inBoundsHState HField  = Refl

272 | inBoundsHState HStr    = Refl

273 | inBoundsHState HEnd    = Refl

274 | inBoundsHState HNat    = Refl

275 | inBoundsHState HMT     = Refl

276 | inBoundsHState HMT1    = Refl

277 | inBoundsHState HCD     = Refl

278 | inBoundsHState HCD1    = Refl

279 | inBoundsHState HErr    = Refl