-- |
-- Module      : Net.DNSBase.Internal.Nat16
-- Description : TBD
-- Copyright   : (c) Viktor Dukhovni, 2026
-- License     : BSD-3-Clause
-- Maintainer  : ietf-dane@dukhovni.org
-- Stability   : unstable
{-# LANGUAGE
    DataKinds
  , MagicHash
  #-}

module Net.DNSBase.Internal.Nat16
    ( type Nat16
    , Nat
    , Typeable
    , natToWord16
    , withNat16
    )
    where

import Data.Kind (Constraint)
import Data.Typeable ((:~:)(Refl), Typeable)
import Data.Word (Word16)
import GHC.TypeNats ( Nat, CmpNat, KnownNat, SNat
                    , natVal', withSomeSNat, withKnownNat )
import GHC.Exts ( proxy# )
import Unsafe.Coerce (unsafeCoerce)

type Nat16 :: Nat -> Constraint
type Nat16 n = (KnownNat n, CmpNat n 65536 ~ LT)

-- | Convert 16-bit type-level natural to corresponding RRTYPE.
natToWord16 :: forall (n :: Nat) -> KnownNat n => Word16
natToWord16 :: forall (n :: Nat) -> KnownNat n => Word16
natToWord16 n = Nat -> Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Word16) -> Nat -> Word16
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Proxy# n -> Nat
natVal' @n Proxy# n
forall {k} (a :: k). Proxy# a
proxy#
{-# INLINE natToWord16 #-}

-- | Convert RRTYPE to 16-bit natural @SomeNat@ singleton.
withNat16 :: forall r. Word16 -> (forall n -> Nat16 n => r) -> r
withNat16 :: forall r. Word16 -> (forall (n :: Nat) -> Nat16 n => r) -> r
withNat16 Word16
w forall (n :: Nat) -> Nat16 n => r
f = Nat -> (forall (n :: Nat). SNat n -> r) -> r
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat (Word16 -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word16
w) SNat n -> r
forall (n :: Nat). SNat n -> r
go
  where
    go :: forall n. SNat n -> r
    go :: forall (n :: Nat). SNat n -> r
go SNat n
s = case magic n of { CmpNat n 65536 :~: 'LT
Refl -> SNat n -> (KnownNat n => r) -> r
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
s (f n) }
    magic :: forall n -> CmpNat n 65536 :~: LT
    magic :: forall (n :: Nat) -> CmpNat n 65536 :~: 'LT
magic _ = ('LT :~: 'LT) -> CmpNat n 65536 :~: 'LT
forall a b. a -> b
unsafeCoerce (forall (a :: Ordering). a :~: a
forall {k} (a :: k). a :~: a
Refl @LT)
{-# INLINE withNat16 #-}