{-# LANGUAGE Unsafe #-}
-- | de Bruijn indices for well-scoped terms.
module DeBruijn.Internal.Idx (
    -- * de Bruijn indices
    Idx (IZ, IS, UnsafeIdx),
    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

import Unsafe.Coerce (unsafeCoerce)

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

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

newtype Idx j = UnsafeIdx { forall (j :: Ctx). Idx j -> Int
_idxToInt :: Int }

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

-- | Convert index to 'Int'.
idxToInt :: Idx ctx -> Int
idxToInt :: forall (j :: Ctx). Idx j -> Int
idxToInt = Idx ctx -> Int
forall (j :: Ctx). Idx j -> Int
_idxToInt

-- | Derive anything from index into empty scope.
--
-- Note: don't use @EmptyCase@ on 'Idx' 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"

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

-- We need a GADT to implement pattern synonyms.
type ViewIdx :: Ctx -> Type
type role ViewIdx nominal
data ViewIdx n where
    IZ' :: ViewIdx (S n)
    IS' :: Idx n -> ViewIdx (S n)

viewIdx :: Idx n -> ViewIdx n
viewIdx :: forall (n :: Ctx). Idx n -> ViewIdx n
viewIdx (UnsafeIdx Int
0) = ViewIdx (S Any) -> ViewIdx n
forall a b. a -> b
unsafeCoerce ViewIdx (S Any)
forall (n :: Ctx). ViewIdx (S n)
IZ'
viewIdx (UnsafeIdx Int
n) = ViewIdx (S Any) -> ViewIdx n
forall a b. a -> b
unsafeCoerce (Idx Any -> ViewIdx (S Any)
forall (n :: Ctx). Idx n -> ViewIdx (S n)
IS' (Int -> Idx Any
forall (j :: Ctx). Int -> Idx j
UnsafeIdx (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)))

pattern IZ :: () => (m ~ S n) => Idx m
pattern $mIZ :: forall {r} {m :: Ctx}.
Idx m -> (forall {n :: Ctx}. (m ~ S n) => r) -> ((# #) -> r) -> r
$bIZ :: forall (m :: Ctx) (n :: Ctx). (m ~ S n) => Idx m
IZ <- (viewIdx -> IZ')
  where IZ = Int -> Idx m
forall (j :: Ctx). Int -> Idx j
UnsafeIdx Int
0

pattern IS :: () => (m ~ S n) => Idx n -> Idx m
pattern $mIS :: forall {r} {m :: Ctx}.
Idx m
-> (forall {n :: Ctx}. (m ~ S n) => Idx n -> r)
-> ((# #) -> r)
-> r
$bIS :: forall (m :: Ctx) (n :: Ctx). (m ~ S n) => Idx n -> Idx m
IS n <- (viewIdx -> IS' n)
  where IS Idx n
n = Int -> Idx m
forall (j :: Ctx). Int -> Idx j
UnsafeIdx (Idx n -> Int
forall (j :: Ctx). Idx j -> Int
idxToInt Idx n
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

{-# COMPLETE IZ, IS #-}

-------------------------------------------------------------------------------
-- 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 (j :: Ctx). Idx j -> 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