# language DataKinds #
# language DerivingStrategies #
{-# language ExplicitNamespaces #-}
# language GADTSyntax #
# language GeneralizedNewtypeDeriving #
# language KindSignatures #
# language MagicHash #
# language RoleAnnotations #
# language StandaloneDeriving #
# language TypeOperators #
{-# language UnliftedNewtypes #-}

module Arithmetic.Unsafe
  ( Nat(..)
  , Fin#(..)
  , type (<)(Lt)
  , type (<=)(Lte)
  , type (:=:)(Eq)
  ) where

import Prelude hiding ((>=),(<=))

import Control.Category (Category)
import Data.Kind (Type)
import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep))

import qualified Control.Category
import qualified GHC.TypeNats as GHC

-- Do not import this module unless you enjoy pain.
-- Using this library to implement length-indexed arrays
-- or sized builders does not require importing this
  module to get the value out of the  data constructor .
-- Use Arithmetic.Nat.demote for this purpose.

infix 4 <
infix 4 <=
infix 4 :=:

-- | A value-level representation of a natural number @n@.
newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int }
type role Nat nominal

deriving newtype instance Show (Nat n)

-- | Finite numbers without the overhead of carrying around a proof.
newtype Fin# :: GHC.Nat -> TYPE 'IntRep where
  Fin# :: Int# -> Fin# n

  | Proof that the first argument is strictly less than the
  second argument .
data (<) :: GHC.Nat -> GHC.Nat -> Type where
  Lt :: a < b

  | Proof that the first argument is less than or equal to the
  second argument .
data (<=) :: GHC.Nat -> GHC.Nat -> Type where
  Lte :: a <= b

  | Proof that the first argument is equal to the second argument .
data (:=:) :: GHC.Nat -> GHC.Nat -> Type where
  Eq :: a :=: b

instance Category (<=) where
  id = Lte
  Lte . Lte = Lte

instance Category (:=:) where
  id = Eq
  Eq . Eq = Eq

# language ExplicitNamespaces #
# language UnliftedNewtypes #
 Do not import this module unless you enjoy pain.
 Using this library to implement length-indexed arrays
 or sized builders does not require importing this
 Use Arithmetic.Nat.demote for this purpose.
 | A value-level representation of a natural number @n@.
 | Finite numbers without the overhead of carrying around a proof.
# language DataKinds #
# language DerivingStrategies #
# language GADTSyntax #
# language GeneralizedNewtypeDeriving #
# language KindSignatures #
# language MagicHash #
# language RoleAnnotations #
# language StandaloneDeriving #
# language TypeOperators #

module Arithmetic.Unsafe
  ( Nat(..)
  , Fin#(..)
  , type (<)(Lt)
  , type (<=)(Lte)
  , type (:=:)(Eq)
  ) where

import Prelude hiding ((>=),(<=))

import Control.Category (Category)
import Data.Kind (Type)
import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep))

import qualified Control.Category
import qualified GHC.TypeNats as GHC

  module to get the value out of the  data constructor .

infix 4 <
infix 4 <=
infix 4 :=:

newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int }
type role Nat nominal

deriving newtype instance Show (Nat n)

newtype Fin# :: GHC.Nat -> TYPE 'IntRep where
  Fin# :: Int# -> Fin# n

  | Proof that the first argument is strictly less than the
  second argument .
data (<) :: GHC.Nat -> GHC.Nat -> Type where
  Lt :: a < b

  | Proof that the first argument is less than or equal to the
  second argument .
data (<=) :: GHC.Nat -> GHC.Nat -> Type where
  Lte :: a <= b

  | Proof that the first argument is equal to the second argument .
data (:=:) :: GHC.Nat -> GHC.Nat -> Type where
  Eq :: a :=: b

instance Category (<=) where
  id = Lte
  Lte . Lte = Lte

instance Category (:=:) where
  id = Eq
  Eq . Eq = Eq
