
  0 | module Network.URL.HTTP.Data
  1 | 
  2 | public export
  3 | QueryParam : Type
  4 | QueryParam = (String, String)
  5 | 
  6 | public export
  7 | record HTTPURL where
  8 |     constructor MkHTTPURL
  9 |     scheme, host : String
 10 |     port : Maybe Int
 11 |     path : String
 12 |     
 13 |     query : List QueryParam
 14 |     
 15 |     fragment : Maybe String
 16 | 
 17 | public export
 18 | Show HTTPURL where
 19 |   show (MkHTTPURL scheme host port path query fragment) = "MkHTTPURL \"" ++ scheme ++ "\" \"" 
 20 |                                         ++ host ++ "\" \"" 
 21 |                                         ++ show port ++ "\" \"" 
 22 |                                         ++ path ++ "\" \"" 
 23 |                                         ++ show query ++ "\" \"" 
 24 |                                         ++ show fragment ++ "\""
 25 | 
 26 | public export
 27 | Eq HTTPURL where
 28 |   (MkHTTPURL scheme host port path query fragment) == (MkHTTPURL scheme1 host1 port1 path1 query1 fragment1) = 
 29 |     scheme == scheme1 
 30 |     && host == host1
 31 |     && port == port1
 32 |     && path == path1
 33 |     && query == query1
 34 |     && fragment == fragment1
 35 | 
 36 |