9 | module Data.URI

 11 | import Data.Bits

 12 | import Data.DPair

 13 | import Data.List

 14 | import Data.List1

 15 | import Data.Maybe

 16 | import Data.String

 17 | import Data.String.Extra

 18 | import Data.String.Parser

 19 | import Data.Vect

 20 | import Data.Hex

 22 | listElem : Eq a => a -> List a -> Bool

 23 | listElem = elem

 25 | foldSeq : (Applicative f, Traversable t, Monoid m) => t (f m) -> f m

 26 | foldSeq = map concat . sequence

 29 | public export

 30 | record URIAuthority where

 31 |   constructor MkURIAuthority

 32 |   userInfo : Maybe String

 33 |   regName : String

 34 |   port : Maybe Nat

 37 | Show URIAuthority where

 38 |   show authority =

 39 |     let info = maybe "" (+> '@') authority.userInfo

 40 |         port = maybe "" ((':' <+) . show) authority.port

 41 |      in "\{info}\{authority.regName}\{port}"

 44 | Eq URIAuthority where

 45 |   x == y = show x == show y

 48 | Ord URIAuthority where

 49 |   compare x y = compare (show x) (show y)

 52 | public export

 53 | record URI where

 54 |   constructor MkURI

 55 |   scheme : String

 56 |   authority : Maybe URIAuthority

 57 |   path : String

 58 |   query : String

 59 |   fragment : String

 62 | Show URI where

 63 |   show uri =

 64 |     let auth = maybe "" ((++ "//") . show) uri.authority

 65 |         query = if uri.query == "" then "" else '?' <+ uri.query

 66 |         fragment = if uri.fragment == "" then "" else '#' <+ uri.fragment

 67 |      in "\{uri.scheme}:\{auth}\{uri.path}\{query}\{fragment}"

 70 | Eq URI where

 71 |   x == y = show x == show y

 74 | Ord URI where

 75 |   compare x y = compare (show x) (show y)

 80 | isUnreserved : Char -> Bool

 81 | isUnreserved c = isAlphaNum c || (c `listElem` ['-', '.', '_', '~'])

 83 | isGenDelim : Char -> Bool

 84 | isGenDelim c = c `listElem` [':', '/', '?', '#', '[', ']', '@']

 89 | isSubDelim : Char -> Bool

 90 | isSubDelim c = c `listElem` ['!', '$', '&', '\'', '(', ')', '*', '+', ',', ';', '=']

 92 | isReserved : Char -> Bool

 93 | isReserved c = isGenDelim c || isSubDelim c

 98 | pctEncoded : Parser Char

 99 | pctEncoded = do

100 |   ignore $ char '%'

101 |   x <- satisfy isHexDigit

102 |   y <- satisfy isHexDigit

103 |   let Just d = fromHexBigEndian "\{cast {to = String} x}\{cast {to = String} y}"

104 |     | Nothing => fail "Cannot convert \{show x}\{show y} to a hex number"

105 |   pure $ chr (cast d)

110 | schemeParser : Parser String

111 | schemeParser = pack <$> [| alphaNum :: many (satisfy isValidForScheme) |]

112 |   where isValidForScheme : Char -> Bool

113 |         isValidForScheme c = isAlphaNum c || (c `listElem` ['+', '-', '.'])

118 | userInfoParser : Parser String

119 | userInfoParser = pack <$> many (satisfy isUnreserved <|> char ':' <|> pctEncoded <|> satisfy isSubDelim)

124 | ipVFutureParser : Parser String

125 | ipVFutureParser = with Prelude.(::)

126 |   foldSeq [ string "v"

127 |           , pack <$> some (satisfy isHexDigit)

128 |           , string "."

129 |           , pack <$> some (satisfy (\c => isUnreserved c || isSubDelim c || c == ':'))

130 |           ]

135 | ipV4AddressParser : Parser String

136 | ipV4AddressParser = with Prelude.(::) foldSeq [octet, string ".", octet, string ".", octet, string ".", octet]

137 |   where

138 |     octet : Parser String

139 |     octet = integer >>= (\v => guard (0 <= v && v <= 255) *> pure (show v))

144 | ipV6AddressParser : Parser String

145 | ipV6AddressParser = with Prelude.(::)

146 |     -- This implementation follows closely the definition in the RFC 3986, so is a mess and surely can be improved :(

147 |         multipleH16LS32 6

148 |     <|> foldSeq [string "::", multipleH16LS32 5]

149 |     <|> foldSeq [optionMap "" id h16, string "::", multipleH16LS32 4]

150 |     <|> foldSeq [optionMap "" id (multipleH16 1), string "::", multipleH16LS32 3]

151 |     <|> foldSeq [optionMap "" id (multipleH16 2), string "::", multipleH16LS32 2]

152 |     <|> foldSeq [optionMap "" id (multipleH16 3), string "::", [| h16 +> char ':' |], ls32]

153 |     <|> foldSeq [optionMap "" id (multipleH16 4), string "::", ls32]

154 |     <|> foldSeq [optionMap "" id (multipleH16 5), string "::", h16]

155 |     <|> foldSeq [optionMap "" id (multipleH16 6), string "::"]

156 |   where

157 |     h16 : Parser String

158 |     h16 = do

159 |       c <- satisfy isHexDigit

160 |       o1 <- optional (satisfy isHexDigit)

161 |       o2 <- optional (satisfy isHexDigit)

162 |       o3 <- optional (satisfy isHexDigit)

163 |       pure $ pack (c :: fromMaybe [] (sequence [o1, o2, o3]))

165 |     ls32 : Parser String

166 |     ls32 = [| [| h16 +> char ':' |] ++ h16 |] <|> ipV4AddressParser

168 |     multipleH16 : Nat -> Parser String

169 |     multipleH16 n = [| (concat . toList <$> ntimes n [| h16 +> char ':' |]) ++ h16 |]

171 |     multipleH16LS32 : Nat -> Parser String

172 |     multipleH16LS32 n = [| (concat . toList <$> ntimes n [| h16 +> char ':' |]) ++ ls32 |]

177 | zoneIDParser : Parser String

178 | zoneIDParser = pack <$> some (satisfy isUnreserved <|> pctEncoded)

183 | ipV6AddrzParser : Parser String

184 | ipV6AddrzParser = with Prelude.(::) concat <$> sequence [ipV6AddressParser, string "%25", zoneIDParser]

190 | ipLiteralParser : Parser String

191 | ipLiteralParser = char '[' *> (ipV6AddressParser <|> ipV6AddrzParser <|> ipVFutureParser) <* char ']'

196 | regNameParser : Parser String

197 | regNameParser = pack <$> many (satisfy isUnreserved <|> pctEncoded <|> satisfy isSubDelim)

202 | authorityParser : Parser URIAuthority

203 | authorityParser = do

204 |   ignore $ string "//"

205 |   userInfo <- optional $ userInfoParser <* char '@'

206 |   host <- ipLiteralParser <|> ipV4AddressParser <|> regNameParser

207 |   port <- optional $ char ':' *> natural

208 |   pure $ MkURIAuthority userInfo host port

213 | pchar : Parser Char

214 | pchar = satisfy (\c => isUnreserved c || isSubDelim c) <|> pctEncoded <|> char ':' <|> char '@'

219 | segment : Parser String

220 | segment = pack <$> many pchar

225 | segmentNZ : Parser String

226 | segmentNZ = pack <$> some pchar

231 | segmentNZNC : Parser String

232 | segmentNZNC = pack <$> some (satisfy (\c => isUnreserved c || isSubDelim c) <|> pctEncoded <|> char '@')

237 | abempty : Parser String

238 | abempty = concat <$> many [| char '/' <+ segment |]

243 | absolute : Parser String

244 | absolute = [| char '/' <+ optionMap "" id [| segmentNZ ++ (concat <$> many [| char '/' <+ segment |]) |] |]

249 | noscheme : Parser String

250 | noscheme = [| segmentNZNC ++ (concat <$> many [| char '/' <+ segment |]) |]

255 | rootless : Parser String

256 | rootless = [| segmentNZ ++ (concat <$> many [| char '/' <+ segment |]) |]

261 | pathParser : Parser String

262 | pathParser = absolute <|> noscheme <|> rootless <|> abempty <|> pure ""

267 | queryParser : Parser String

268 | queryParser = pack <$> many (pchar <|> char '/' <|> char '?')

273 | fragmentParser : Parser String

274 | fragmentParser = pack <$> many (pchar <|> char '/' <|> char '?')

280 | uriParser : Parser URI

281 | uriParser = do

282 |   scheme <- schemeParser

283 |   ignore $ char ':'

284 |   (authority, path) <- [| MkPair (Just <$> authorityParser) abempty |] <|> ((Nothing,) <$> (absolute <|> rootless <|> empty))

285 |   query <- optionMap "" id (char '?' *> queryParser)

286 |   fragment <- optionMap "" id (char '#' *> fragmentParser)

287 |   pure $ MkURI scheme authority path query fragment

292 | relativeReferenceParser : Parser URI

293 | relativeReferenceParser = do

294 |   (authority, path) <- [| MkPair (Just <$> authorityParser) abempty |] <|> ((Nothing,) <$> (absolute <|> noscheme <|> empty))

295 |   query <- optionMap "" id (char '?' *> queryParser)

296 |   fragment <- optionMap "" id (char '#' *> fragmentParser)

297 |   pure $ MkURI "" authority path query fragment

303 | uriReferenceParser : Parser URI

304 | uriReferenceParser = uriParser <|> relativeReferenceParser

310 | uriAbsoluteParser : Parser URI

311 | uriAbsoluteParser = do

312 |   scheme <- schemeParser

313 |   ignore $ char ':'

314 |   (authority, path) <- [| MkPair (Just <$> authorityParser) abempty |] <|> ((Nothing,) <$> (absolute <|> rootless <|> empty))

315 |   query <- optionMap "" id (char '?' *> queryParser)

316 |   pure $ MkURI scheme authority path query ""

319 | uriIsAbsolute : URI -> Bool

320 | uriIsAbsolute (MkURI {scheme, _}) = scheme /= ""

323 | uriIsRelative : URI -> Bool

324 | uriIsRelative = not . uriIsAbsolute

327 | isUnescapedInURI : Char -> Bool

328 | isUnescapedInURI c = isReserved c || isUnreserved c

331 | isUnescapedInURIComponent : Char -> Bool

332 | isUnescapedInURIComponent c = not (isReserved c || not (isUnescapedInURI c))

334 | utf8EncodeChar : Char -> List Int

335 | utf8EncodeChar = go . ord

336 |   where

337 |     go : Int -> List Int

338 |     go x = if x <= 0x7f then [x]

339 |            else if x <= 0x7ff then [ 0xc0 + (x `shiftR` 6)

340 |                                    , 0x80 + x .&. 0x3f

341 |                                    ]

342 |            else if x <= 0xffff then [ 0xe0 + (x `shiftR` 12)

343 |                                     , 0x80 + ((x `shiftR` 6) .&. 0x3f)

344 |                                     , 0x80 + x .&. 0x3f

345 |                                     ]

346 |            else [ 0xf0 + (x `shiftR` 18)

347 |                 , 0x80 + ((x `shiftR` 12) .&. 0x3f)

348 |                 , 0x80 + ((x `shiftR` 6) .&. 0x3f)

349 |                 , 0x80 + x .&. 0x3f

350 |                 ]

352 | b16ToHexString : Bits16 -> String

353 | b16ToHexString n =

354 |   case n of

355 |     0 => "0"

356 |     1 => "1"

357 |     2 => "2"

358 |     3 => "3"

359 |     4 => "4"

360 |     5 => "5"

361 |     6 => "6"

362 |     7 => "7"

363 |     8 => "8"

364 |     9 => "9"

365 |     10 => "A"

366 |     11 => "B"

367 |     12 => "C"

368 |     13 => "D"

369 |     14 => "E"

370 |     15 => "F"

371 |     other => assert_total $ b16ToHexString (n `shiftR` 4) ++ b16ToHexString (n .&. 15)

373 | pad2 : String -> String

374 | pad2 str =

375 |   case length str of

376 |     0 => "00"

377 |     1 => strCons '0' str

378 |     _ => str

381 | escapeURIChar : (Char -> Bool) -> Char -> String

382 | escapeURIChar p c =

383 |   if p c

384 |      then cast c

385 |      else concatMap (strCons '%' . pad2 . b16ToHexString . cast) (utf8EncodeChar c)

388 | escapeURIString : (Char -> Bool) -> String -> String

389 | escapeURIString p = foldl (\acc, c => acc ++ escapeURIChar p c) "" . unpack

392 | escapeAndParseURI : String -> Either String URI

393 | escapeAndParseURI = mapSnd fst . parse (uriReferenceParser <* eos) . escapeURIString isUnescapedInURI