{-# LANGUAGE Safe #-}
-- | de Bruijn indices for well-scoped terms.
module DeBruijn.Idx (
    -- * de Bruijn indices
    Idx (IZ,IS),
    absurdIdx,
    unIdx,
    idxToInt,
    -- * Common indices
    pattern I1,
    pattern I2,
    pattern I3,
    pattern I4,
    pattern I5,
    pattern I6,
    pattern I7,
    pattern I8,
    pattern I9,
) where

import Data.Kind    (Type)
import DeBruijn.Ctx

-------------------------------------------------------------------------------
-- de Bruijn indices
-------------------------------------------------------------------------------

-- | de Bruijn indices.
--
-- >>> IS (IS (IS IZ))
-- 3
--
type Idx :: Ctx -> Type
type role Idx nominal

data Idx n where
    IZ :: Idx (S n)
    IS :: !(Idx n) -> Idx (S n)

-------------------------------------------------------------------------------
-- Combinators
-------------------------------------------------------------------------------

-- | Convert index to 'Int'.
idxToInt :: Idx n -> Int
idxToInt :: forall (n :: Ctx). Idx n -> Int
idxToInt = Int -> Idx n -> Int
forall (j :: Ctx). Int -> Idx j -> Int
go Int
0 where
    go :: Int -> Idx j -> Int
    go :: forall (j :: Ctx). Int -> Idx j -> Int
go !Int
acc Idx j
IZ = Int
acc
    go Int
acc (IS Idx n
n) = Int -> Idx n -> Int
forall (j :: Ctx). Int -> Idx j -> Int
go (Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Idx n
n

-- | Derive anything from index into empty scope.
--
-- Note: don't use @EmptyCase@ as it doesn't work for unsafe representation.
absurdIdx :: Idx EmptyCtx -> a
absurdIdx :: forall a. Idx EmptyCtx -> a
absurdIdx Idx EmptyCtx
x = Idx EmptyCtx
x Idx EmptyCtx -> a -> a
forall a b. a -> b -> b
`seq` [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"absurd: Idx Z"

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

deriving instance Eq (Idx n)
deriving instance Ord (Idx n)

instance Show (Idx j) where
    showsPrec :: Int -> Idx j -> ShowS
showsPrec Int
d = Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Int -> ShowS) -> (Idx j -> Int) -> Idx j -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Idx j -> Int
forall (n :: Ctx). Idx n -> Int
idxToInt

-------------------------------------------------------------------------------
-- Common Combinators
-------------------------------------------------------------------------------

-- | Case on 'Idx'. (compare to 'maybe').
unIdx :: a -> (Idx n -> a) -> Idx (S n) -> a
unIdx :: forall a (n :: Ctx). a -> (Idx n -> a) -> Idx (S n) -> a
unIdx a
z Idx n -> a
_ Idx (S n)
IZ     = a
z
unIdx a
_ Idx n -> a
s (IS Idx n
x) = Idx n -> a
s Idx n
Idx n
x

pattern I1 :: () => (m ~ S (S n)) => Idx m
pattern $mI1 :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}. (m ~ S (S n)) => r) -> ((# #) -> r) -> r
$bI1 :: forall (m :: Ctx) (n :: Ctx). (m ~ S (S n)) => Idx m
I1 = IS IZ

pattern I2 :: () => (m ~ S (S (S n))) => Idx m
pattern $mI2 :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}. (m ~ S (S (S n))) => r) -> ((# #) -> r) -> r
$bI2 :: forall (m :: Ctx) (n :: Ctx). (m ~ S (S (S n))) => Idx m
I2 = IS I1

pattern I3 :: () => (m ~ S (S (S (S n)))) => Idx m
pattern $mI3 :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}. (m ~ S (S (S (S n)))) => r)
-> ((# #) -> r)
-> r
$bI3 :: forall (m :: Ctx) (n :: Ctx). (m ~ S (S (S (S n)))) => Idx m
I3 = IS I2

pattern I4 :: () => (m ~ S (S (S (S (S n))))) => Idx m
pattern $mI4 :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}. (m ~ S (S (S (S (S n))))) => r)
-> ((# #) -> r)
-> r
$bI4 :: forall (m :: Ctx) (n :: Ctx). (m ~ S (S (S (S (S n))))) => Idx m
I4 = IS I3

pattern I5 :: () => (m ~ S (S (S (S (S (S n)))))) => Idx m
pattern $mI5 :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}. (m ~ S (S (S (S (S (S n)))))) => r)
-> ((# #) -> r)
-> r
$bI5 :: forall (m :: Ctx) (n :: Ctx).
(m ~ S (S (S (S (S (S n)))))) =>
Idx m
I5 = IS I4

pattern I6 :: () => (m ~ S (S (S (S (S (S (S n))))))) => Idx m
pattern $mI6 :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}. (m ~ S (S (S (S (S (S (S n))))))) => r)
-> ((# #) -> r)
-> r
$bI6 :: forall (m :: Ctx) (n :: Ctx).
(m ~ S (S (S (S (S (S (S n))))))) =>
Idx m
I6 = IS I5

pattern I7 :: () => (m ~ S (S (S (S (S (S (S (S n)))))))) => Idx m
pattern $mI7 :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}. (m ~ S (S (S (S (S (S (S (S n)))))))) => r)
-> ((# #) -> r)
-> r
$bI7 :: forall (m :: Ctx) (n :: Ctx).
(m ~ S (S (S (S (S (S (S (S n)))))))) =>
Idx m
I7 = IS I6

pattern I8 :: () => (m ~ S (S (S (S (S (S (S (S (S n))))))))) => Idx m
pattern $mI8 :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}.
    (m ~ S (S (S (S (S (S (S (S (S n))))))))) =>
    r)
-> ((# #) -> r)
-> r
$bI8 :: forall (m :: Ctx) (n :: Ctx).
(m ~ S (S (S (S (S (S (S (S (S n))))))))) =>
Idx m
I8 = IS I7

pattern I9 :: () => (m ~ S (S (S (S (S (S (S (S (S (S n)))))))))) => Idx m
pattern $mI9 :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}.
    (m ~ S (S (S (S (S (S (S (S (S (S n)))))))))) =>
    r)
-> ((# #) -> r)
-> r
$bI9 :: forall (m :: Ctx) (n :: Ctx).
(m ~ S (S (S (S (S (S (S (S (S (S n)))))))))) =>
Idx m
I9 = IS I8