{-# LANGUAGE Unsafe #-}
module DeBruijn.Internal.Add (
Add (AZ, AS, UnsafeAdd),
addToInt,
addToSize,
adding,
rzeroAdd,
unrzeroAdd,
lzeroAdd,
unlzeroAdd,
rsuccAdd,
unrsuccAdd,
lsuccAdd,
unlsuccAdd,
swapAdd,
unswapAdd,
) where
import Data.Coerce (coerce)
import Data.GADT.Show (GShow (..))
import Data.Kind (Type)
import Data.Some (Some (..))
import Data.Type.Equality ((:~:) (Refl))
import Unsafe.Coerce (unsafeCoerce)
import DeBruijn.Ctx
import DeBruijn.Internal.Size
type Add :: Ctx -> Ctx -> Ctx -> Type
type role Add nominal nominal nominal
newtype Add n m p = UnsafeAdd { forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int
_addToInt :: Int }
addToInt :: Add n m p -> Int
addToInt :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int
addToInt = Add n m p -> Int
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int
_addToInt
addToSize :: Add n m p -> Size n
addToSize :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Size n
addToSize (UnsafeAdd Int
n) = Int -> Size n
forall (ctx :: Ctx). Int -> Size ctx
UnsafeSize Int
n
instance Show (Add n m p) where
showsPrec :: Int -> Add n m p -> ShowS
showsPrec Int
d Add n m p
a = Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Add n m p -> Int
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int
addToInt Add n m p
a)
instance GShow (Add n m) where
gshowsPrec :: forall (a :: Ctx). Int -> Add n m a -> ShowS
gshowsPrec = Int -> Add n m a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec
type ViewAdd :: Ctx -> Ctx -> Ctx -> Type
type role ViewAdd nominal nominal nominal
data ViewAdd n m p where
AZ' :: ViewAdd EmptyCtx ctx ctx
AS' :: !(Add n ctx ctx') -> ViewAdd (S n) ctx (S ctx')
viewAdd :: Add n m p -> ViewAdd n m p
viewAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> ViewAdd n m p
viewAdd (UnsafeAdd Int
n)
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = ViewAdd EmptyCtx Any Any -> ViewAdd n m p
forall a b. a -> b
unsafeCoerce ViewAdd EmptyCtx Any Any
forall (ctx :: Ctx). ViewAdd EmptyCtx ctx ctx
AZ'
| Bool
otherwise = ViewAdd (S Any) Any (S Any) -> ViewAdd n m p
forall a b. a -> b
unsafeCoerce (Add Any Any Any -> ViewAdd (S Any) Any (S Any)
forall (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Add n ctx ctx' -> ViewAdd (S n) ctx (S ctx')
AS' (Int -> Add Any Any Any
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p
UnsafeAdd (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)))
pattern AZ :: () => (n ~ EmptyCtx, m ~ p) => Add n m p
pattern $mAZ :: forall {r} {n :: Ctx} {m :: Ctx} {p :: Ctx}.
Add n m p -> ((n ~ EmptyCtx, m ~ p) => r) -> ((# #) -> r) -> r
$bAZ :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
(n ~ EmptyCtx, m ~ p) =>
Add n m p
AZ <- (viewAdd -> AZ')
where AZ = Int -> Add n m p
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p
UnsafeAdd Int
0
pattern AS :: () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p
pattern $mAS :: forall {r} {n :: Ctx} {p :: Ctx} {m :: Ctx}.
Add n m p
-> (forall {n' :: Ctx} {p' :: Ctx}.
(n ~ S n', p ~ S p') =>
Add n' m p' -> r)
-> ((# #) -> r)
-> r
$bAS :: forall (n :: Ctx) (p :: Ctx) (m :: Ctx) (n' :: Ctx) (p' :: Ctx).
(n ~ S n', p ~ S p') =>
Add n' m p' -> Add n m p
AS a <- (viewAdd -> AS' a)
where AS Add n' m p'
a = Int -> Add n m p
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p
UnsafeAdd (Add n' m p' -> Int
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int
_addToInt Add n' m p'
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
{-# COMPLETE AZ, AS #-}
adding :: Size n -> Some (Add n ctx)
adding :: forall (n :: Ctx) (ctx :: Ctx). Size n -> Some (Add n ctx)
adding (UnsafeSize Int
n) = Add n ctx Any -> Some (Add n ctx)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (Int -> Add n ctx Any
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p
UnsafeAdd Int
n)
rzeroAdd :: Size n -> Add n EmptyCtx n
rzeroAdd :: forall (n :: Ctx). Size n -> Add n EmptyCtx n
rzeroAdd (UnsafeSize Int
n) = Int -> Add n EmptyCtx n
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p
UnsafeAdd Int
n
unrzeroAdd :: Add n EmptyCtx m -> n :~: m
unrzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add n EmptyCtx m -> n :~: m
unrzeroAdd (UnsafeAdd !Int
_) = (Any :~: Any) -> n :~: m
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl
lzeroAdd :: Size n -> Add EmptyCtx n n
lzeroAdd :: forall (n :: Ctx). Size n -> Add EmptyCtx n n
lzeroAdd Size n
_ = Add EmptyCtx n n
forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
(n ~ EmptyCtx, m ~ p) =>
Add n m p
AZ
unlzeroAdd :: Add EmptyCtx n m -> n :~: m
unlzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add EmptyCtx n m -> n :~: m
unlzeroAdd Add EmptyCtx n m
AZ = n :~: n
n :~: m
forall {k} (a :: k). a :~: a
Refl
rsuccAdd :: Add n m p -> Add n (S m) (S p)
rsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add n m p -> Add n (S m) (S p)
rsuccAdd = Add n m p -> Add n (S m) (S p)
forall a b. Coercible a b => a -> b
coerce
unrsuccAdd :: Add n (S m) (S p) -> Add n m p
unrsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add n (S m) (S p) -> Add n m p
unrsuccAdd = Add n (S m) (S p) -> Add n m p
forall a b. Coercible a b => a -> b
coerce
lsuccAdd :: Add n m p -> Add (S n) m (S p)
lsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add n m p -> Add (S n) m (S p)
lsuccAdd = Add n m p -> Add (S n) m (S p)
forall (n :: Ctx) (p :: Ctx) (m :: Ctx) (n' :: Ctx) (p' :: Ctx).
(n ~ S n', p ~ S p') =>
Add n' m p' -> Add n m p
AS
unlsuccAdd :: Add (S n) m (S p) -> Add n m p
unlsuccAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add (S n) m (S p) -> Add n m p
unlsuccAdd (AS Add n' m p'
a)= Add n m p
Add n' m p'
a
swapAdd :: Add n (S m) p -> Add (S n) m p
swapAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add n (S m) p -> Add (S n) m p
swapAdd (UnsafeAdd Int
n) = Int -> Add (S n) m p
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p
UnsafeAdd (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
unswapAdd :: Add (S n) m p -> Add n (S m) p
unswapAdd :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add (S n) m p -> Add n (S m) p
unswapAdd (UnsafeAdd Int
n) = Int -> Add n (S m) p
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p
UnsafeAdd (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)