0 | module HTTP.Parser.URI

  2 | import Data.ByteVect as BV

  3 | import Derive.Prelude

  4 | import HTTP.Parser.Util

  5 | import Text.ILex.Derive

  7 | %default total

  8 | %language ElabReflection

 15 | isUnreserved : Bits8 -> Bool

 16 | isUnreserved 45  = True -- '-'

 17 | isUnreserved 46  = True -- '.'

 18 | isUnreserved 95  = True -- '_'

 19 | isUnreserved 126 = True -- '~'

 20 | isUnreserved b   = isAlphaNum b

 23 | isSubDelims : Bits8 -> Bool

 24 | isSubDelims 33 = True -- '!'

 25 | isSubDelims 36 = True -- '$'

 26 | isSubDelims 38 = True -- '&'

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

 28 | isSubDelims 40 = True -- '('

 29 | isSubDelims 41 = True -- ')'

 30 | isSubDelims 42 = True -- '*'

 31 | isSubDelims 43 = True -- '+'

 32 | isSubDelims 44 = True -- ','

 33 | isSubDelims 59 = True -- ';'

 34 | isSubDelims 61 = True -- '='

 35 | isSubDelims _  = False

 38 | ispchar : Bits8 -> Bool

 39 | ispchar 58 = True -- ':'

 40 | ispchar 64 = True -- '@'

 41 | ispchar c  = isUnreserved c || isSubDelims c

 44 | isAuthByte : Bits8 -> Bool

 45 | isAuthByte = ispchar

 48 | isQueryByte : Bits8 -> Bool

 49 | isQueryByte 47 = True -- '/'

 50 | isQueryByte 63 = True -- '?'

 51 | isQueryByte 38 = False -- '&'

 52 | isQueryByte c  = ispchar c

 55 | isQueryNameByte : Bits8 -> Bool

 56 | isQueryNameByte 61 = False -- '='

 57 | isQueryNameByte c  = isQueryByte c

 59 | export %inline

 60 | isFragmentByte : Bits8 -> Bool

 61 | isFragmentByte 47 = True -- '/'

 62 | isFragmentByte 63 = True -- '?'

 63 | isFragmentByte c  = ispchar c

 69 | scheme : RExp True

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

 72 | subDelims : RExp True

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

 75 | genDelims : RExp True

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

 78 | unreserved : RExp True

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

 81 | reserved : RExp True

 82 | reserved = genDelims <|> subDelims

 84 | pchar : RExp True

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

 87 | fragment : RExp True

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

 90 | query : RExp True

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

 93 | segment : RExp False

 94 | segment = star pchar

 96 | segmentNz : RExp True

 97 | segmentNz   = plus pchar

 99 | segmentNzNc : RExp True

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

102 | regName : RExp False

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

105 | decOctet : RExp True

106 | decOctet =

107 |       digit

108 |   <|> (posdigit >> digit)

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

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

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

113 | ip4address : RExp True

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

116 | h16 : RExp True

117 | h16 = repeatRange 1 4 hexdigit

119 | ls32 : RExp True

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

122 | ip6address : RExp True

123 | ip6address =

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

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

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

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

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

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

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

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

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

134 | ipFuture : RExp True

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

137 | ipLiteral : RExp True

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

140 | host : RExp False

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

143 | userinfo : RExp False

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

146 | authority : RExp True

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

153 | %runElab deriveParserState "USz" "UST"

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

156 | public export

157 | record Part where

158 |   constructor P

159 |   sch  : Maybe ByteString

160 |   auth : Maybe ByteString

161 |   abs  : Bool

162 |   segs : SnocList ByteString

163 |   ques : Maybe ByteString

164 |   frag : Maybe ByteString

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

168 | pinit : Part

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

171 | setScheme : ByteString -> Part -> Part

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

174 | setQuery : ByteString -> Part -> Part

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

177 | setAuth : ByteString -> Part -> Part

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

180 | absoluteSegment : ByteString -> Part -> Part

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

183 | rootSegment : ByteString -> Part -> Part

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

186 | addSegment : ByteString -> Part -> Part

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

189 | setFragment : ByteString -> Part -> Part

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

192 | public export

193 | 0 SK : Type -> Type

194 | SK = Stack Void Part USz

197 | upd : SK q => UST -> (Part -> Part) -> F1 q UST

198 | upd u f = modStackAs SK f u

204 | init : DFA q USz SK

205 | init =

206 |   dfa

207 |     [ conv (scheme >> ':') $ upd Hier . setScheme

208 |     , conv authority $ upd Segments . setAuth

209 |     , conv ('/' >> opt segmentNz) $ upd Segments . absoluteSegment

210 |     , conv segmentNzNc $ upd Segments . rootSegment

211 |     , conv query $ upd Fragment . setQuery

212 |     , conv fragment $ upd End . setFragment

213 |     ]

215 | hier : DFA q USz SK

216 | hier =

217 |   dfa

218 |     [ conv authority $ upd Segments . setAuth

219 |     , conv ('/' >> opt segmentNz) $ upd Segments . absoluteSegment

220 |     , conv segmentNz $ upd Segments . rootSegment

221 |     , conv query $ upd Fragment . setQuery

222 |     , conv fragment $ upd End . setFragment

223 |     ]

225 | segments : DFA q USz SK

226 | segments =

227 |   dfa

228 |     [ conv ('/' >> segment) $ upd Segments . addSegment

229 |     , conv query $ upd Fragment . setQuery

230 |     , conv fragment $ upd End . setFragment

231 |     ]

233 | uriTrans : Lex1 q USz SK

234 | uriTrans =

235 |   lex1

236 |     [ E Init init

237 |     , E Hier hier

238 |     , E Segments segments

239 |     , E Fragment $ dfa [conv fragment $ upd End . setFragment]

240 |     ]

242 | uriErr : Arr32 USz (SK q -> F1 q (BoundedErr Void))

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

245 | uriEOI : UST -> SK q -> F1 q (Either (BoundedErr Void) Part)

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

248 | public export

249 | uri : P1 q (BoundedErr Void) Part

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