
  0 | module TyTTP.URL.Definition
  1 | 
  2 | public export
  3 | data Scheme
  4 |   = HTTP
  5 |   | HTTPS
  6 |   | OtherScheme String
  7 | 
  8 | namespace Scheme
  9 |   export
 10 |   parse : String -> Scheme
 11 |   parse "http" = HTTP
 12 |   parse "https" = HTTPS
 13 |   parse str = OtherScheme str
 14 | 
 15 |   export
 16 |   Show Scheme where
 17 |     show s = case s of
 18 |       HTTP => "http"
 19 |       HTTPS => "https"
 20 |       OtherScheme str => str
 21 | 
 22 | public export
 23 | record URL a p s where
 24 |   constructor MkURL
 25 |   scheme : Maybe Scheme
 26 |   authority : Maybe a
 27 |   path : p
 28 |   search : s
 29 | 
 30 |