
  0 | module Network.HTTP.Protocol
  1 | 
  2 | import Data.String
  3 | import Generics.Derive
  4 | import Derive.Prelude
  5 | 
  6 | %hide Generics.Derive.Eq
  7 | %hide Generics.Derive.Ord
  8 | %hide Generics.Derive.Show
  9 | 
 10 | %language ElabReflection
 11 | 
 12 | public export
 13 | data Protocol : Type where
 14 |   HTTP : Protocol
 15 |   HTTPS : Protocol
 16 | 
 17 | %runElab derive "Protocol" [Generic, Meta, Eq, DecEq, Show]
 18 | 
 19 | public export
 20 | protocol_port_number : Protocol -> Bits16
 21 | protocol_port_number HTTP = 80
 22 | protocol_port_number HTTPS = 443
 23 | 
 24 | public export
 25 | protocol_from_str : String -> Maybe Protocol
 26 | protocol_from_str protocol =
 27 |   case toUpper protocol of
 28 |     "HTTP" => Just HTTP
 29 |     "HTTPS" => Just HTTPS
 30 |     _ => Nothing
 31 |