{-# LANGUAGE Unsafe #-}
module DeBruijn.Internal.Idx (
Idx (IZ, IS, UnsafeIdx),
absurdIdx,
unIdx,
idxToInt,
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)
type Idx :: Ctx -> Type
type role Idx nominal
newtype Idx j = UnsafeIdx { forall (j :: Ctx). Idx j -> Int
_idxToInt :: Int }
idxToInt :: Idx ctx -> Int
idxToInt :: forall (j :: Ctx). Idx j -> Int
idxToInt = Idx ctx -> Int
forall (j :: Ctx). Idx j -> Int
_idxToInt
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"
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 #-}
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
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