0 | module HTTP.Parser.URI

  2 | import Data.ByteVect as BV

  3 | import Derive.Prelude

  4 | import HTTP.Parser.Util

  5 | import Text.ILex

  6 | import Text.ILex.State.Regular

  7 | import Text.ILex.State.Derive

  9 | %default total

 10 | %language ElabReflection

 17 | isUnreserved : Bits8 -> Bool

 18 | isUnreserved 45  = True -- '-'

 19 | isUnreserved 46  = True -- '.'

 20 | isUnreserved 95  = True -- '_'

 21 | isUnreserved 126 = True -- '~'

 22 | isUnreserved b   = isAlphaNum b

 25 | isSubDelims : Bits8 -> Bool

 26 | isSubDelims 33 = True -- '!'

 27 | isSubDelims 36 = True -- '$'

 28 | isSubDelims 38 = True -- '&'

 29 | isSubDelims 39 = True -- '\''

 30 | isSubDelims 40 = True -- '('

 31 | isSubDelims 41 = True -- ')'

 32 | isSubDelims 42 = True -- '*'

 33 | isSubDelims 43 = True -- '+'

 34 | isSubDelims 44 = True -- ','

 35 | isSubDelims 59 = True -- ';'

 36 | isSubDelims 61 = True -- '='

 37 | isSubDelims _  = False

 40 | ispchar : Bits8 -> Bool

 41 | ispchar 58 = True -- ':'

 42 | ispchar 64 = True -- '@'

 43 | ispchar c  = isUnreserved c || isSubDelims c

 46 | isAuthByte : Bits8 -> Bool

 47 | isAuthByte = ispchar

 50 | isQueryByte : Bits8 -> Bool

 51 | isQueryByte 47 = True -- '/'

 52 | isQueryByte 63 = True -- '?'

 53 | isQueryByte 38 = False -- '&'

 54 | isQueryByte c  = ispchar c

 57 | isQueryNameByte : Bits8 -> Bool

 58 | isQueryNameByte 61 = False -- '='

 59 | isQueryNameByte c  = isQueryByte c

 61 | export %inline

 62 | isFragmentByte : Bits8 -> Bool

 63 | isFragmentByte 47 = True -- '/'

 64 | isFragmentByte 63 = True -- '?'

 65 | isFragmentByte c  = ispchar c

 71 | scheme : RExp True

 72 | scheme = alpha >> star (alphaNum <|> oneof ['+','-','.'])

 74 | subDelims : RExp True

 75 | subDelims = oneof ['!','$','&','\'','(',')','*','+',',',';','=']

 77 | genDelims : RExp True

 78 | genDelims = oneof [':','/','?','#','[',']','@']

 80 | unreserved : RExp True

 81 | unreserved = alphaNum <|> oneof ['-','.','_','~']

 83 | reserved : RExp True

 84 | reserved = genDelims <|> subDelims

 86 | pchar : RExp True

 87 | pchar = unreserved <|> pctEncoded <|> subDelims <|> oneof [':','@']

 89 | fragment : RExp True

 90 | fragment = '#' >> star (pchar <|> oneof ['/','?'])

 92 | query : RExp True

 93 | query = '?' >> star (pchar <|> oneof ['/','?'])

 95 | segment : RExp False

 96 | segment = star pchar

 98 | segmentNz : RExp True

 99 | segmentNz   = plus pchar

101 | segmentNzNc : RExp True

102 | segmentNzNc = plus $ unreserved <|> pctEncoded <|> subDelims <|> '@'

104 | regName : RExp False

105 | regName = star $ unreserved <|> pctEncoded <|> subDelims

107 | decOctet : RExp True

108 | decOctet =

109 |       digit

110 |   <|> (posdigit >> digit)

111 |   <|> ('1' >> digit >> digit)

112 |   <|> ('2' >> range '0' '4' >> digit)

113 |   <|> ("25" >> range '0' '5')

115 | ip4address : RExp True

116 | ip4address = decOctet >> repeat 3 ("." >> decOctet)

118 | h16 : RExp True

119 | h16 = repeatRange 1 4 hexdigit

121 | ls32 : RExp True

122 | ls32 = (h16 >> ":" >> h16) <|> ip4address

124 | ip6address : RExp True

125 | ip6address =

126 |       (                                                     repeat 6 (h16 >> ':') >> ls32)

127 |   <|> (                                             "::" >> repeat 5 (h16 >> ':') >> ls32)

128 |   <|> (opt                                  h16  >> "::" >> repeat 4 (h16 >> ':') >> ls32)

129 |   <|> (opt (repeatRange 0 1 (h16 >> ':') >> h16) >> "::" >> repeat 3 (h16 >> ':') >> ls32)

130 |   <|> (opt (repeatRange 0 2 (h16 >> ':') >> h16) >> "::" >> repeat 2 (h16 >> ':') >> ls32)

131 |   <|> (opt (repeatRange 0 3 (h16 >> ':') >> h16) >> "::" >>           h16 >> ':'  >> ls32)

132 |   <|> (opt (repeatRange 0 4 (h16 >> ':') >> h16) >> "::"                          >> ls32)

133 |   <|> (opt (repeatRange 0 5 (h16 >> ':') >> h16) >> "::"                          >> h16)

134 |   <|> (opt (repeatRange 0 6 (h16 >> ':') >> h16) >> "::")

136 | ipFuture : RExp True

137 | ipFuture = 'v' >> plus hexdigit >> '.' >> plus (unreserved <|> subDelims <|> ':')

139 | ipLiteral : RExp True

140 | ipLiteral = '[' >> (ip6address <|> ipFuture) >> ']'

142 | host : RExp False

143 | host = ipLiteral <|> ip4address <|> regName

145 | userinfo : RExp False

146 | userinfo = star (unreserved <|> pctEncoded <|> subDelims <|> ':')

148 | authority : RExp True

149 | authority = "//" >> opt (userinfo >> '@') >> host >> opt (':' >> star digit)

155 | %runElab deriveParserState "USz" "UST"

156 |   ["Init", "Hier", "Segments", "Fragment", "End"]

158 | public export

159 | record Part where

160 |   constructor P

161 |   sch  : Maybe ByteString

162 |   auth : Maybe ByteString

163 |   abs  : Bool

164 |   segs : SnocList ByteString

165 |   ques : Maybe ByteString

166 |   frag : Maybe ByteString

168 | %runElab derive "Part" [Show,Eq]

170 | pinit : Part

171 | pinit = P Nothing Nothing False [<] Nothing Nothing

173 | setScheme : ByteString -> Part -> Part

174 | setScheme bs = {sch := Just $ dropEnd 1 bs}

176 | setQuery : ByteString -> Part -> Part

177 | setQuery bs = {ques := Just $ uriUnescape (drop 1 bs)}

179 | setAuth : ByteString -> Part -> Part

180 | setAuth bs = {auth := Just $ uriUnescape $ drop 2 bs}

182 | absoluteSegment : ByteString -> Part -> Part

183 | absoluteSegment bs = {abs := True, segs := [<uriUnescape $ drop 1 bs]}

185 | rootSegment : ByteString -> Part -> Part

186 | rootSegment bs = {segs := [<uriUnescape bs]}

188 | addSegment : ByteString -> Part -> Part

189 | addSegment bs = {segs $= (:< uriUnescape (drop 1 bs))}

191 | setFragment : ByteString -> Part -> Part

192 | setFragment bs = {frag := Just $ uriUnescape (drop 1 bs)}

194 | public export

195 | 0 ST : Type -> Type

196 | ST = State Void Part USz

199 | upd : ST q => UST -> (Part -> Part) -> F1 q UST

200 | upd u f = modStackAs ST f u

206 | init : DFA q USz ST

207 | init =

208 |   dfa

209 |     [ bytes (scheme >> ':') $ upd Hier . setScheme

210 |     , bytes authority $ upd Segments . setAuth

211 |     , bytes ('/' >> opt segmentNz) $ upd Segments . absoluteSegment

212 |     , bytes segmentNzNc $ upd Segments . rootSegment

213 |     , bytes query $ upd Fragment . setQuery

214 |     , bytes fragment $ upd End . setFragment

215 |     ]

217 | hier : DFA q USz ST

218 | hier =

219 |   dfa

220 |     [ bytes authority $ upd Segments . setAuth

221 |     , bytes ('/' >> opt segmentNz) $ upd Segments . absoluteSegment

222 |     , bytes segmentNz $ upd Segments . rootSegment

223 |     , bytes query $ upd Fragment . setQuery

224 |     , bytes fragment $ upd End . setFragment

225 |     ]

227 | segments : DFA q USz ST

228 | segments =

229 |   dfa

230 |     [ bytes ('/' >> segment) $ upd Segments . addSegment

231 |     , bytes query $ upd Fragment . setQuery

232 |     , bytes fragment $ upd End . setFragment

233 |     ]

235 | uriTrans : Lex1 q USz ST

236 | uriTrans =

237 |   lex1

238 |     [ E Init init

239 |     , E Hier hier

240 |     , E Segments segments

241 |     , E Fragment $ dfa [bytes fragment $ upd End . setFragment]

242 |     ]

244 | uriErr : Arr32 USz (ST q -> F1 q (BBErr Void))

245 | uriErr = arr32 USz (unexpected []) []

247 | uriEOI : UST -> ST q -> F1 q (Either (BBErr Void) Part)

248 | uriEOI sk s t = let v # t := getStack t in Right v # t

250 | public export

251 | uri : P1 q (BBErr Void) Part

252 | uri = P Init (init pinit) uriTrans (\x => (Nothing #)) uriErr uriEOI