{-# language DataKinds #-}
{-# language MagicHash #-}
{-# language ExplicitNamespaces #-}
{-# language PatternSynonyms #-}
{-# language ViewPatterns #-}
{-# language GADTs #-}
{-# language KindSignatures #-}
{-# language RankNTypes #-}
{-# language TypeOperators #-}
{-# language UnboxedTuples #-}
{-# language UnboxedSums #-}

module Arithmetic.Types
  ( Nat
  , Nat#
  , WithNat(..)
  , Difference(..)
  , Fin(..)
  , Fin#
  , Fin32#
    -- * Maybe Fin
  , MaybeFin#
  , pattern MaybeFinJust#
  , pattern MaybeFinNothing#
    -- * Infix Operators
  , type (<)
  , type (<=)
  , type (<#)
  , type (<=#)
  , type (:=:)
  , type (:=:#)
  ) where

import Arithmetic.Unsafe (Fin#(Fin#),Nat#,Nat(getNat), type (<=))
import Arithmetic.Unsafe (Fin32#)
import Arithmetic.Unsafe (MaybeFin#(..))
import Arithmetic.Unsafe (type (<), type (:=:))
import Arithmetic.Unsafe (type (<#), type (<=#), (:=:#))
import Data.Kind (type Type)
import GHC.TypeNats (type (+))

import qualified GHC.TypeNats as GHC

data WithNat :: (GHC.Nat -> Type) -> Type where
  WithNat ::
       {-# UNPACK #-} !(Nat n)
    -> f n
    -> WithNat f

-- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }'
data Fin :: GHC.Nat -> Type where
  Fin :: forall m n.
    { ()
index :: !(Nat m)
    , ()
proof :: !(m < n)
    } -> Fin n

-- | Proof that the first argument can be expressed as the
-- sum of the second argument and some other natural number.
data Difference :: GHC.Nat -> GHC.Nat -> Type where
  -- It is safe for users of this library to use this data constructor
  -- freely. However, note that the interesting Difference values come
  -- from Arithmetic.Nat.monus, which is a primitive.
  Difference :: forall a b c. Nat c -> (c + b :=: a) -> Difference a b

instance Show (Fin n) where
  showsPrec :: Int -> Fin n -> ShowS
showsPrec Int
p (Fin Nat m
i m < n
_) = String -> ShowS
showString String
"Fin " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Nat m -> Int
forall (n :: Nat). Nat n -> Int
getNat Nat m
i)

instance Eq (Fin n) where
  Fin Nat m
x m < n
_ == :: Fin n -> Fin n -> Bool
== Fin Nat m
y m < n
_ = Nat m -> Int
forall (n :: Nat). Nat n -> Int
getNat Nat m
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Nat m -> Int
forall (n :: Nat). Nat n -> Int
getNat Nat m
y

instance Ord (Fin n) where
  Fin Nat m
x m < n
_ compare :: Fin n -> Fin n -> Ordering
`compare` Fin Nat m
y m < n
_ = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Nat m -> Int
forall (n :: Nat). Nat n -> Int
getNat Nat m
x) (Nat m -> Int
forall (n :: Nat). Nat n -> Int
getNat Nat m
y)

pattern MaybeFinJust# :: Fin# n -> MaybeFin# n
pattern $mMaybeFinJust# :: forall {r} {n :: Nat}.
MaybeFin# n -> (Fin# n -> r) -> ((# #) -> r) -> r
$bMaybeFinJust# :: forall (n :: Nat). Fin# n -> MaybeFin# n
MaybeFinJust# f <- (maybeFinToFin# -> (# | f #)) where
  MaybeFinJust# (Fin# Int#
i) = Int# -> MaybeFin# n
forall (a :: Nat). Int# -> MaybeFin# a
MaybeFin# Int#
i

pattern MaybeFinNothing# :: MaybeFin# n
pattern $mMaybeFinNothing# :: forall {r} {n :: Nat}.
MaybeFin# n -> ((# #) -> r) -> ((# #) -> r) -> r
$bMaybeFinNothing# :: (# #) -> forall (n :: Nat). MaybeFin# n
MaybeFinNothing# = MaybeFin# (-1#)

maybeFinToFin# :: MaybeFin# n -> (# (# #) | Fin# n #)
{-# inline maybeFinToFin# #-}
maybeFinToFin# :: forall (n :: Nat). MaybeFin# n -> (# (# #) | Fin# n #)
maybeFinToFin# (MaybeFin# Int#
i) = case Int#
i of
  Int#
-1# -> (# (# #) | #)
  Int#
_ -> (# | Int# -> Fin# n
forall (a :: Nat). Int# -> Fin# a
Fin# Int#
i #)