0 | module Utils.IPAddr
  1 |
  2 | import Data.String.Parser
  3 | import Data.Vect
  4 | import Data.Fin
  5 | import Data.String.Extra
  6 | import Data.String
  7 | import Utils.Num
  8 | import Utils.Misc
  9 | import Data.List
 10 | import Data.List1
 11 | import Data.Bits
 12 | import Utils.Bytes
 13 |
 14 | public export
 15 | record IPv4Addr where
 16 |   constructor MkIPv4Addr
 17 |   body : Vect 4 Bits8
 18 |
 19 | public export
 20 | Show IPv4Addr where
 21 |   show x = join "." $ map show x.body
 22 |
 23 | public export
 24 | Eq IPv4Addr where
 25 |   x == y = x.body == y.body
 26 |
 27 | public export
 28 | record IPv6Addr where
 29 |   constructor MkIPv6Addr
 30 |   body : Vect 16 Bits8
 31 |
 32 | bits16_show : Bits16 -> String
 33 | bits16_show x = (show_hex (cast $ shiftR x 8)) <+> (show_hex $ cast x)
 34 |
 35 | to_hextets : IPv6Addr -> Vect 8 Bits16
 36 | to_hextets addr = map from_be $ group 8 2 addr.body
 37 |
 38 | public export
 39 | Show IPv6Addr where
 40 |   show x = assert_total $ join ":" $ map bits16_show (to_hextets x)
 41 |
 42 | public export
 43 | Eq IPv6Addr where
 44 |   x == y = x.body == y.body
 45 |
 46 | read_decimal_byte : Monad m => ParseT m Bits8
 47 | read_decimal_byte = do
 48 |   n <- natural
 49 |   if n < 256
 50 |     then pure $ cast n
 51 |     else fail "number out of bound"
 52 |
 53 | parse_ipv4' : Monad m => ParseT m IPv4Addr
 54 | parse_ipv4' = do
 55 |   a <- read_decimal_byte
 56 |   _ <- char '.'
 57 |   b <- read_decimal_byte
 58 |   _ <- char '.'
 59 |   c <- read_decimal_byte
 60 |   _ <- char '.'
 61 |   d <- read_decimal_byte
 62 |   pure $ MkIPv4Addr [a, b, c, d]
 63 |
 64 | export
 65 | parse_ipv4 : String -> Either String IPv4Addr
 66 | parse_ipv4 = map fst . parse parse_ipv4'
 67 |
 68 | data IPv6R : Type -> Type where
 69 |   One : a -> IPv6R a
 70 |   Two : a -> a -> IPv6R a
 71 |
 72 | splitDoubleColon : String -> Either String (IPv6R String)
 73 | splitDoubleColon str = do
 74 |   let (a ::: [b]) = split ((':', ':') ==) (f $ unpack str)
 75 |   | (a ::: []) => pure (One str)
 76 |   | _ => Left "too many double colons"
 77 |   pure $ Two (pack $ map fst a) (pack $ map snd b)
 78 |   where
 79 |     f : List Char -> List (Char, Char)
 80 |     f [] = []
 81 |     f (x :: xs) = zip (x :: xs) xs
 82 |
 83 | parse_ipv6_to_octets : String -> Either String (IPv6R (List Bits16))
 84 | parse_ipv6_to_octets string = do
 85 |   Two a b <- splitDoubleColon string
 86 |   | One a => One <$> to a
 87 |   a <- to a
 88 |   b <- to b
 89 |   pure $ Two a b
 90 |   where
 91 |     go : String -> Either String Bits16
 92 |     go x = do
 93 |       let Just hex = stringToNat' 16 x
 94 |       | Nothing => Left $ "invalid hextet: " <+> x
 95 |       if hex < 65536
 96 |         then Right $ cast hex
 97 |         else Left "number out of bound"
 98 |     to : String -> Either String (List Bits16)
 99 |     to "" = Right []
100 |     to x = traverse go $ toList $ split (':' ==) x
101 |
102 | parse_ipv6_expand_columns : IPv6R (List Bits16) -> Either String (Vect 8 Bits16)
103 | parse_ipv6_expand_columns (One a) = maybe_to_either (exactLength _ $ fromList a) "invalid length"
104 | parse_ipv6_expand_columns (Two a b) = do
105 |   let plen = minus 8 (length a + length b)
106 |   let apb = a <+> replicate plen 0 <+> b
107 |   maybe_to_either (exactLength _ $ fromList apb) "invalid length"
108 |
109 | export
110 | parse_ipv6 : String -> Either String IPv6Addr
111 | parse_ipv6 x = do
112 |   y <- (parse_ipv6_to_octets x >>= parse_ipv6_expand_columns)
113 |   pure $ MkIPv6Addr $ concat $ map (to_be {n=2}) y
114 |