{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE ViewPatterns #-}
module Arithmetic.Types
( Nat
, Nat#
, WithNat (..)
, Difference (..)
, Fin (..)
, Fin#
, Fin32#
, MaybeFin#
, pattern MaybeFinJust#
, pattern MaybeFinNothing#
, type (<)
, type (<=)
, type (<#)
, type (<=#)
, type (:=:)
, type (:=:#)
) where
import Arithmetic.Unsafe (Fin# (Fin#), Fin32#, MaybeFin# (..), Nat (getNat), Nat#, (:=:#), type (:=:), type (<), type (<#), 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
data Fin :: GHC.Nat -> Type where
Fin ::
forall m n.
{ ()
index :: !(Nat m)
, ()
proof :: !(m < n)
} ->
Fin n
data Difference :: GHC.Nat -> GHC.Nat -> Type where
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 #)