{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeInType             #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# OPTIONS_GHC -Wall                       #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}

{-|
Module      : Fcf.Alg.Nat
Description : Nat helpers
Copyright   : (c) gspia 2020-
License     : BSD
Maintainer  : gspia

= Fcf.Data.Nat


-}


--------------------------------------------------------------------------------

module Fcf.Alg.Nat where

import qualified GHC.TypeNats as TN
import           Fcf.Core (Eval, Exp)
import           Fcf.Data.Bool
import           Fcf.Data.Nat (Nat)
import qualified Fcf.Data.Nat as FN

--------------------------------------------------------------------------------

-- | Nat equality.
--
-- >>> :kind! Eval (2 == 2)
-- Eval (2 == 2) :: Bool
-- = 'True
--
-- >>> :kind! Eval (2 == 3)
-- Eval (2 == 3) :: Bool
-- = 'False
data (==) :: Nat -> Nat -> Exp Bool
type instance Eval ((==) a b) = Eval ((a TN.<=? b) && (b TN.<=? a))


-- | Nat in-equality.
--
-- >>> :kind! Eval (2 /= 2)
-- Eval (2 /= 2) :: Bool
-- = 'False
--
-- >>> :kind! Eval (2 /= 3)
-- Eval (2 /= 3) :: Bool
-- = 'True
data (/=) :: Nat -> Nat -> Exp Bool
type instance Eval ((/=) a b) = Eval (Eval (a FN.< b) || Eval (b FN.< a))