{-|
Copyright  :  (C) 2024-2025, Felix Klein
License    :  MIT (see the file LICENSE)
Maintainer :  Felix Klein <felix@qbaylogic.com>
-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

{-# OPTIONS_HADDOCK hide #-}

module Clash.Class.Finite.Internal.Evidence where

import Data.Constraint (Dict(..))
import GHC.TypeNats
  ( Nat, type (^), type (<=), type (*), type (+)
#if !MIN_VERSION_base(4,16,0)
  , type (-)
#endif
  )
#if !MIN_VERSION_base(4,16,0)
import GHC.TypeLits.Extra (CLog)
#endif
import Unsafe.Coerce (unsafeCoerce)

-- | Evidence that exponentiation can never return a zero result,
-- except the base is zero.
powPositiveIfPositiveBase ::
  forall (n :: Nat) (m :: Nat).
  1 <= n => Dict (1 <= n^m)
powPositiveIfPositiveBase :: forall (n :: Nat) (m :: Nat). (1 <= n) => Dict (1 <= (n ^ m))
powPositiveIfPositiveBase = Dict (() :: Constraint)
-> Dict
     (Assert
        (OrdCond (CmpNat 1 (n ^ m)) 'True 'True 'False) (TypeError ...))
forall a b. a -> b
unsafeCoerce (Dict (() :: Constraint)
Dict
  (Assert (OrdCond (Compare 0 0) 'True 'True 'False) (TypeError ...))
forall (a :: Constraint). a => Dict a
Dict :: Dict (0 <= 0))

-- | Evidence that exponentiation not returning a zero result is
-- a proof of the base being greater than zero.
powPositiveImpliesPositiveBase ::
  forall (n :: Nat) (m :: Nat).
  1 <= n^m => Dict (1 <= n)
powPositiveImpliesPositiveBase :: forall (n :: Nat) (m :: Nat). (1 <= (n ^ m)) => Dict (1 <= n)
powPositiveImpliesPositiveBase = Dict (() :: Constraint)
-> Dict
     (Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...))
forall a b. a -> b
unsafeCoerce (Dict (() :: Constraint)
Dict
  (Assert (OrdCond (Compare 0 0) 'True 'True 'False) (TypeError ...))
forall (a :: Constraint). a => Dict a
Dict :: Dict (0 <= 0))

-- | Evidence that any multiplicaton resulting in a positive number
-- must have two positive operands.
mulPositiveImpliesPositiveOperands ::
  forall (n :: Nat) (m :: Nat).
  1 <= n * m => Dict (1 <= n, 1 <= m)
mulPositiveImpliesPositiveOperands :: forall (n :: Nat) (m :: Nat).
(1 <= (n * m)) =>
Dict (1 <= n, 1 <= m)
mulPositiveImpliesPositiveOperands =
  Dict (() :: Constraint, () :: Constraint)
-> Dict
     (Assert (OrdCond (CmpNat 1 n) 'True 'True 'False) (TypeError ...),
      Assert (OrdCond (CmpNat 1 m) 'True 'True 'False) (TypeError ...))
forall a b. a -> b
unsafeCoerce (Dict (() :: Constraint, () :: Constraint)
Dict
  (Assert (OrdCond (Compare 0 0) 'True 'True 'False) (TypeError ...),
   Assert (OrdCond (Compare 0 0) 'True 'True 'False) (TypeError ...))
forall (a :: Constraint). a => Dict a
Dict :: Dict (0 <= 0, 0 <= 0))

-- | Evidence that zero is the only natural number that is less or
-- equal than zero, also in the scope of addition.
zeroLeAdd ::
  forall (n :: Nat) (m :: Nat).
  n + m <= m => Dict (n ~ 0)
zeroLeAdd :: forall (n :: Nat) (m :: Nat). ((n + m) <= m) => Dict (n ~ 0)
zeroLeAdd = Dict (0 ~ 0) -> Dict (n ~ 0)
forall a b. a -> b
unsafeCoerce (Dict (0 ~ 0)
forall (a :: Constraint). a => Dict a
Dict :: Dict (0 ~ 0))

-- | Evidence that exponentiation with a fixed exponent perserves
-- monotonicity.
powMonotone1 ::
  forall (a :: Nat) (b :: Nat) (n :: Nat).
  a <= b => Dict (a^n <= b^n)
powMonotone1 :: forall (a :: Nat) (b :: Nat) (n :: Nat).
(a <= b) =>
Dict ((a ^ n) <= (b ^ n))
powMonotone1 = Dict (() :: Constraint)
-> Dict
     (Assert
        (OrdCond (CmpNat (a ^ n) (b ^ n)) 'True 'True 'False)
        (TypeError ...))
forall a b. a -> b
unsafeCoerce (Dict (() :: Constraint)
Dict
  (Assert (OrdCond (Compare 0 0) 'True 'True 'False) (TypeError ...))
forall (a :: Constraint). a => Dict a
Dict :: Dict (0 <= 0))

-- | Evidence that we can use the exponentiation laws to rewrite the
-- term as stated below.
powLawsRewrite ::
  forall (a :: Nat) (n :: Nat).
  Dict ((a^(2^(n + 1))) ~ ((a^(2^n)) * (a^(2^n))))
powLawsRewrite :: forall (a :: Nat) (n :: Nat).
Dict ((a ^ (2 ^ (n + 1))) ~ ((a ^ (2 ^ n)) * (a ^ (2 ^ n))))
powLawsRewrite = Dict (0 ~ 0)
-> Dict ((a ^ (2 ^ (n + 1))) ~ ((a ^ (2 ^ n)) * (a ^ (2 ^ n))))
forall a b. a -> b
unsafeCoerce (Dict (0 ~ 0)
forall (a :: Constraint). a => Dict a
Dict :: Dict (0 ~ 0))

#if !MIN_VERSION_base(4,16,0)
-- | Evidence that exponentiation and clog are dual to each other.
pow2CLogDual ::
  forall (n :: Nat).
  Dict (CLog 2 (2^n) ~ n)
pow2CLogDual = unsafeCoerce (Dict :: Dict (0 ~ 0))

-- | Evidence that substraction and addition of the same nat cancels
-- each other in a greater or equal than one equation.
leqOnePlusMinus ::
  forall (a :: Nat) (b :: Nat).
  (a <= b, 1 <= b) => Dict (1 <= a + (b - a))
leqOnePlusMinus = unsafeCoerce (Dict :: Dict (0 <= 0))
#endif