0 | module Network.HTTP.URL
  1 |
  2 | import Data.String.Parser
  3 | import Derive.Prelude
  4 | import Network.HTTP.Protocol
  5 | import Data.String
  6 | import Network.HTTP.Path
  7 | import Data.So
  8 |
  9 | %language ElabReflection
 10 |
 11 | public export
 12 | record Hostname where
 13 |   constructor MkHostname
 14 |   domain : String
 15 |   port : Maybe Bits16
 16 |
 17 | public export
 18 | record URLCredential where
 19 |   constructor MkURLCredential
 20 |   username : String
 21 |   password : Maybe String
 22 |
 23 | public export
 24 | record URL where
 25 |   constructor MkURL
 26 |   protocol : String
 27 |   credential : Maybe URLCredential
 28 |   host : Hostname
 29 |   path : Path
 30 |   extensions : String
 31 |
 32 | %runElab derive "URLCredential" [Eq, Show]
 33 | %runElab derive "Hostname" [Eq, Show]
 34 | %runElab derive "URL" [Show]
 35 |
 36 | parse_port_number : Parser Bits16
 37 | parse_port_number = do
 38 |   n <- natural
 39 |   _ <- eos
 40 |   if n < 65536 then pure (cast n) else fail "port number bigger than 65535"
 41 |
 42 | parse_host : Parser Hostname
 43 | parse_host = do
 44 |   domain <- takeWhile (/= ':')
 45 |   port <- optional (char ':' *> (parse_port_number <|> pure 0))
 46 |   pure (MkHostname domain port)
 47 |
 48 | parse_credential : Parser URLCredential
 49 | parse_credential = parse_username_password <|> parse_username where
 50 |   parse_username : Parser URLCredential
 51 |   parse_username = do
 52 |     username <- takeWhile (const True)
 53 |     pure (MkURLCredential username Nothing)
 54 |   parse_username_password : Parser URLCredential
 55 |   parse_username_password = do
 56 |     username <- takeUntil ":"
 57 |     password <- takeWhile (const True)
 58 |     pure (MkURLCredential username $ Just password)
 59 |
 60 | export
 61 | parse_url : Parser URL
 62 | parse_url = do
 63 |   protocol <- takeUntil "://"
 64 |   credential <- optional (takeUntil "@")
 65 |   domain <- takeUntil "/" <|> takeWhile (const True)
 66 |   
 67 |   credential <- case parse parse_credential <$> credential of
 68 |     Just (Right (credential, _)) => pure $ Just credential
 69 |     Just (Left err) => fail err
 70 |     Nothing => pure Nothing
 71 |
 72 |   case parse parse_host domain of
 73 |     Right (domain_and_port, _) => do
 74 |       path <- takeWhile (\c => (c /= '#') && (c /= '?'))
 75 |       extensions <- takeWhile (const True)
 76 |       let path = fromString ("/" <+> path)
 77 |       pure $ MkURL protocol credential domain_and_port path extensions
 78 |     Left err => fail err
 79 |
 80 | export
 81 | url_from_string : String -> Either String URL
 82 | url_from_string = map fst . parse parse_url . ltrim
 83 |
 84 | public export
 85 | data URLProof : AsList m -> Type where
 86 |   IsHTTPURL : URLProof ('h' :: 't' :: 't' :: 'p' :: ':' :: '/' :: '/' :: xs)
 87 |   IsHTTPSURL : URLProof ('h' :: 't' :: 't' :: 'p' :: 's' :: ':' :: '/' :: '/' :: xs)
 88 |
 89 | export
 90 | url' : (str : String) -> {auto 0 ok : URLProof (asList str)} -> URL
 91 | url' string =
 92 |   case url_from_string string of
 93 |     Right x => x
 94 |     Left err => assert_total $ idris_crash err
 95 |
 96 | export
 97 | add : URL -> String -> URL
 98 | add url' string =
 99 |   case url_from_string string of
100 |     Right url'' => url''
101 |     Left _ =>
102 |       case break (\c => c == '#' || c == '?') string of
103 |         (path, "") => { path := (url'.path <+> fromString path), extensions := "" } url'
104 |         (path, extension) => { path := (url'.path <+> fromString path), extensions := extension } url'
105 |
106 | export
107 | parse_hostname : String -> Either String Hostname
108 | parse_hostname = map fst . parse parse_host . trim
109 |
110 | export
111 | hostname_string : Hostname -> String
112 | hostname_string host =
113 |   host.domain <+> case host.port of Just x => ":\{show x}"; Nothing => ""
114 |
115 | export
116 | url_port_number : URL -> Maybe Bits16
117 | url_port_number url = url.host.port <|> (protocol_port_number <$> protocol_from_str url.protocol)
118 |