{-# 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

-- | Term level witness of the size of a context.
--
-- >>> SZ
-- 0
--
-- >>> SS (SS SZ)
-- 2
--
type Size :: Ctx -> Type
type role Size nominal

newtype Size ctx = UnsafeSize { forall (ctx :: Ctx). Size ctx -> Int
_sizeToInt :: Int }

-------------------------------------------------------------------------------
-- Helpers
-------------------------------------------------------------------------------

-- | Unapply 'SS'. Occasionally more useful than pattern matching.
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

-- | Convert 'Size' to 'Int.
sizeToInt :: Size ctx -> Int
sizeToInt :: forall (ctx :: Ctx). Size ctx -> Int
sizeToInt = Size ctx -> Int
forall (ctx :: Ctx). Size ctx -> Int
_sizeToInt

-------------------------------------------------------------------------------
-- Instances
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Pattern synonyms
-------------------------------------------------------------------------------

-- We need a GADT to implement pattern synonyms.
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 #-}

-------------------------------------------------------------------------------
-- Sizes
-------------------------------------------------------------------------------

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