{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Grisette.Internal.SymPrim.Prim.Internal.IsZero
  ( IsZero,
    KnownIsZero (..),
    IsZeroCases (..),
  )
where

import qualified Data.SBV as SBV
import GHC.TypeNats (KnownNat, Nat, type (<=))

type family IsZero (a :: Nat) :: Bool where
  IsZero 0 = 'True
  IsZero _ = 'False

data IsZeroCases (a :: Nat) where
  IsZeroEvidence :: (IsZero a ~ 'True) => IsZeroCases a
  NonZeroEvidence ::
    (IsZero a ~ 'False, SBV.BVIsNonZero a, 1 <= a) =>
    IsZeroCases a

instance Show (IsZeroCases a) where
  show :: IsZeroCases a -> String
show IsZeroCases a
IsZeroEvidence = String
"IsZeroEvidence"
  show IsZeroCases a
NonZeroEvidence = String
"NonZeroEvidence"

class (KnownNat a) => KnownIsZero (a :: Nat) where
  isZero :: proxy a -> IsZeroCases a

instance KnownIsZero 0 where
  isZero :: forall (proxy :: Nat -> *). proxy 0 -> IsZeroCases 0
isZero proxy 0
_ = IsZeroCases 0
forall (a :: Nat). (IsZero a ~ 'True) => IsZeroCases a
IsZeroEvidence

instance
  {-# OVERLAPPABLE #-}
  (KnownNat a, IsZero a ~ 'False, 1 <= a, SBV.BVIsNonZero a) =>
  KnownIsZero a
  where
  isZero :: forall (proxy :: Nat -> *). proxy a -> IsZeroCases a
isZero proxy a
_ = IsZeroCases a
forall (a :: Nat).
(IsZero a ~ 'False, BVIsNonZero a, 1 <= a) =>
IsZeroCases a
NonZeroEvidence