{-# LANGUAGE Unsafe #-}
module DeBruijn.Internal.Size (
Size (SZ, SS, UnsafeSize),
unSS,
sizeToInt,
pattern S1,
pattern S2,
pattern S3,
pattern S4,
pattern S5,
pattern S6,
pattern S7,
pattern S8,
pattern S9,
) where
import Data.EqP (EqP (..))
import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..))
import Data.GADT.Show (GShow (..))
import Data.Kind (Type)
import Data.OrdP (OrdP (..))
import Data.Type.Equality (TestEquality (testEquality), (:~:) (Refl))
import Unsafe.Coerce (unsafeCoerce)
import DeBruijn.Ctx
type Size :: Ctx -> Type
type role Size nominal
newtype Size ctx = UnsafeSize { forall (ctx :: Ctx). Size ctx -> Int
_sizeToInt :: Int }
unSS :: Size (S ctx) -> Size ctx
unSS :: forall (ctx :: Ctx). Size (S ctx) -> Size ctx
unSS (SS Size n
x) = Size ctx
Size n
x
sizeToInt :: Size ctx -> Int
sizeToInt :: forall (ctx :: Ctx). Size ctx -> Int
sizeToInt = Size ctx -> Int
forall (ctx :: Ctx). Size ctx -> Int
_sizeToInt
instance Show (Size ctx) where
showsPrec :: Int -> Size ctx -> ShowS
showsPrec Int
d (UnsafeSize Int
i) = Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d Int
i
instance GShow Size where
gshowsPrec :: forall (ctx :: Ctx). Int -> Size ctx -> ShowS
gshowsPrec = Int -> Size a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
instance Eq (Size ctx) where
Size ctx
_ == :: Size ctx -> Size ctx -> Bool
== Size ctx
_ = Bool
True
instance Ord (Size ctx) where
compare :: Size ctx -> Size ctx -> Ordering
compare Size ctx
_ Size ctx
_ = Ordering
EQ
instance EqP Size where
eqp :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Bool
eqp (UnsafeSize Int
n) (UnsafeSize Int
m) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m
instance OrdP Size where
comparep :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Ordering
comparep (UnsafeSize Int
n) (UnsafeSize Int
m) = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
m
instance GEq Size where
geq :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Maybe (a :~: b)
geq (UnsafeSize Int
n) (UnsafeSize Int
m) =
if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m then (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl) else Maybe (a :~: b)
forall a. Maybe a
Nothing
instance GCompare Size where
gcompare :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> GOrdering a b
gcompare (UnsafeSize Int
n) (UnsafeSize Int
m) = case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
m of
Ordering
LT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
Ordering
EQ -> GOrdering Any Any -> GOrdering a b
forall a b. a -> b
unsafeCoerce GOrdering Any Any
forall {k} (a :: k). GOrdering a a
GEQ
Ordering
GT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
instance TestEquality Size where
testEquality :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Maybe (a :~: b)
testEquality = Size a -> Size b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Maybe (a :~: b)
geq
type ViewSize :: Ctx -> Type
type role ViewSize nominal
data ViewSize ctx where
SZ' :: ViewSize EmptyCtx
SS' :: Size n -> ViewSize (S n)
viewSize :: Size n -> ViewSize n
viewSize :: forall (n :: Ctx). Size n -> ViewSize n
viewSize (UnsafeSize Int
0) = ViewSize EmptyCtx -> ViewSize n
forall a b. a -> b
unsafeCoerce ViewSize EmptyCtx
SZ'
viewSize (UnsafeSize Int
n) = ViewSize (S Any) -> ViewSize n
forall a b. a -> b
unsafeCoerce (Size Any -> ViewSize (S Any)
forall (n :: Ctx). Size n -> ViewSize (S n)
SS' (Int -> Size Any
forall (ctx :: Ctx). Int -> Size ctx
UnsafeSize (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)))
pattern SZ :: () => (m ~ EmptyCtx) => Size m
pattern $mSZ :: forall {r} {m :: Ctx}.
Size m -> ((m ~ EmptyCtx) => r) -> ((# #) -> r) -> r
$bSZ :: forall (m :: Ctx). (m ~ EmptyCtx) => Size m
SZ <- (viewSize -> SZ')
where SZ = Int -> Size m
forall (ctx :: Ctx). Int -> Size ctx
UnsafeSize Int
0
pattern SS :: () => (m ~ S n) => Size n -> Size m
pattern $mSS :: forall {r} {m :: Ctx}.
Size m
-> (forall {n :: Ctx}. (m ~ S n) => Size n -> r)
-> ((# #) -> r)
-> r
$bSS :: forall (m :: Ctx) (n :: Ctx). (m ~ S n) => Size n -> Size m
SS n <- (viewSize -> SS' n)
where SS Size n
n = Int -> Size m
forall (ctx :: Ctx). Int -> Size ctx
UnsafeSize (Size n -> Int
forall (ctx :: Ctx). Size ctx -> Int
_sizeToInt Size n
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
{-# COMPLETE SZ, SS #-}
pattern S1 :: () => (m ~ Ctx1) => Size m
pattern $mS1 :: forall {r} {m :: Ctx}.
Size m -> ((m ~ Ctx1) => r) -> ((# #) -> r) -> r
$bS1 :: forall (m :: Ctx). (m ~ Ctx1) => Size m
S1 = SS SZ
pattern S2 :: () => (m ~ Ctx2) => Size m
pattern $mS2 :: forall {r} {m :: Ctx}.
Size m -> ((m ~ Ctx2) => r) -> ((# #) -> r) -> r
$bS2 :: forall (m :: Ctx). (m ~ Ctx2) => Size m
S2 = SS S1
pattern S3 :: () => (m ~ Ctx3) => Size m
pattern $mS3 :: forall {r} {m :: Ctx}.
Size m -> ((m ~ Ctx3) => r) -> ((# #) -> r) -> r
$bS3 :: forall (m :: Ctx). (m ~ Ctx3) => Size m
S3 = SS S2
pattern S4 :: () => (m ~ Ctx4) => Size m
pattern $mS4 :: forall {r} {m :: Ctx}.
Size m -> ((m ~ Ctx4) => r) -> ((# #) -> r) -> r
$bS4 :: forall (m :: Ctx). (m ~ Ctx4) => Size m
S4 = SS S3
pattern S5 :: () => (m ~ Ctx5) => Size m
pattern $mS5 :: forall {r} {m :: Ctx}.
Size m -> ((m ~ Ctx5) => r) -> ((# #) -> r) -> r
$bS5 :: forall (m :: Ctx). (m ~ Ctx5) => Size m
S5 = SS S4
pattern S6 :: () => (m ~ Ctx6) => Size m
pattern $mS6 :: forall {r} {m :: Ctx}.
Size m -> ((m ~ Ctx6) => r) -> ((# #) -> r) -> r
$bS6 :: forall (m :: Ctx). (m ~ Ctx6) => Size m
S6 = SS S5
pattern S7 :: () => (m ~ Ctx7) => Size m
pattern $mS7 :: forall {r} {m :: Ctx}.
Size m -> ((m ~ Ctx7) => r) -> ((# #) -> r) -> r
$bS7 :: forall (m :: Ctx). (m ~ Ctx7) => Size m
S7 = SS S6
pattern S8 :: () => (m ~ Ctx8) => Size m
pattern $mS8 :: forall {r} {m :: Ctx}.
Size m -> ((m ~ Ctx8) => r) -> ((# #) -> r) -> r
$bS8 :: forall (m :: Ctx). (m ~ Ctx8) => Size m
S8 = SS S7
pattern S9 :: () => (m ~ Ctx9) => Size m
pattern $mS9 :: forall {r} {m :: Ctx}.
Size m -> ((m ~ Ctx9) => r) -> ((# #) -> r) -> r
$bS9 :: forall (m :: Ctx). (m ~ Ctx9) => Size m
S9 = SS S8