{-# LANGUAGE Safe #-}
module DeBruijn.Size (
    Size (SZ, SS),
    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 (..), defaultCompare, defaultEq)
import Data.GADT.Show     (GShow (..))
import Data.Kind          (Type)
import Data.OrdP          (OrdP (..))
import Data.Type.Equality (TestEquality (testEquality), (:~:) (Refl))

import DeBruijn.Ctx

-- | Term level witness of the size of the context.
--
-- >>> SZ
-- 0
--
-- >>> SS (SS SZ)
-- 2
--
type Size :: Ctx -> Type
data Size ctx where
    SZ :: Size EmptyCtx
    SS :: !(Size ctx) -> Size (S ctx)

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

unSS :: Size (S ctx) -> Size ctx
unSS :: forall (ctx :: Ctx). Size (S ctx) -> Size ctx
unSS (SS Size ctx
x) = Size ctx
Size ctx
x

sizeToInt :: Size ctx -> Int
sizeToInt :: forall (ctx :: Ctx). Size ctx -> Int
sizeToInt = Int -> Size ctx -> Int
forall (ctx :: Ctx). Int -> Size ctx -> Int
go Int
0 where
    go :: Int -> Size ctx -> Int
    go :: forall (ctx :: Ctx). Int -> Size ctx -> Int
go !Int
n Size ctx
SZ     = Int
n
    go  Int
n (SS Size ctx
s) = Int -> Size ctx -> Int
forall (ctx :: Ctx). Int -> Size ctx -> Int
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Size ctx
s

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

instance Show (Size ctx) where
    showsPrec :: Int -> Size ctx -> ShowS
showsPrec Int
d Size ctx
s = Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Size ctx -> Int
forall (ctx :: Ctx). Size ctx -> Int
sizeToInt Size ctx
s)

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
    Size ctx
_ <= :: Size ctx -> Size ctx -> Bool
<= Size ctx
_ = Bool
True
    Size ctx
_ >= :: Size ctx -> Size ctx -> Bool
>= Size ctx
_ = Bool
True
    Size ctx
_ < :: Size ctx -> Size ctx -> Bool
< Size ctx
_ = Bool
False
    Size ctx
_ > :: Size ctx -> Size ctx -> Bool
> Size ctx
_ = Bool
False
    min :: Size ctx -> Size ctx -> Size ctx
min Size ctx
x Size ctx
_ = Size ctx
x
    max :: Size ctx -> Size ctx -> Size ctx
max Size ctx
x Size ctx
_ = Size ctx
x

instance EqP Size where
    eqp :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Bool
eqp = Size a -> Size b -> Bool
forall {k} (f :: k -> *) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Bool
defaultEq

instance OrdP Size where
    comparep :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Ordering
comparep = Size a -> Size b -> Ordering
forall {k} (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> Ordering
defaultCompare

instance GEq Size where
    geq :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Maybe (a :~: b)
geq Size a
SZ     Size b
SZ     = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    geq (SS Size ctx
n) (SS Size ctx
m) = do
        ctx :~: ctx
Refl <- Size ctx -> Size ctx -> Maybe (ctx :~: ctx)
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 Size ctx
n Size ctx
m
        (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
    geq Size a
_      Size b
_      = 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 Size a
SZ     Size b
SZ     = GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
    gcompare Size a
SZ     (SS Size ctx
_) = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    gcompare (SS Size ctx
_) Size b
SZ     = GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
    gcompare (SS Size ctx
n) (SS Size ctx
m) = case Size ctx -> Size ctx -> GOrdering ctx ctx
forall k (f :: k -> *) (a :: k) (b :: k).
GCompare f =>
f a -> f b -> GOrdering a b
forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> GOrdering a b
gcompare Size ctx
n Size ctx
m of
        GOrdering ctx ctx
GLT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
        GOrdering ctx ctx
GEQ -> GOrdering a a
GOrdering a b
forall {k} (a :: k). GOrdering a a
GEQ
        GOrdering ctx ctx
GGT -> 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

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