{-# LANGUAGE Unsafe #-}
module DeBruijn.Internal.Add (
    Add (AZ, AS, UnsafeAdd),
    addToInt,
    addToSize,
    adding,
    -- * Lemmas
    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

-- $setup
-- >>> import DeBruijn

-- | @'Add' n m p@ is an evidence that @n + m = p@.
--
-- Useful when you have an arity @n@ thing and need to extend a context @ctx@ with: @'Add' n ctx ctx'@.
--
-- Using a type representing a graph of a type function is often more convenient than defining type-family to begin with.
--
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 #-}

-- | Add @n@ to some context @ctx@.
--
-- >>> adding (SS (SS SZ))
-- Some 2
--
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)

-------------------------------------------------------------------------------
-- Lemmas: zero
-------------------------------------------------------------------------------

-- | @n + 0 ≡ 0@
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

-- | @n + 0 ≡ m → n ≡ m@
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

-- | @0 + n ≡ 0@
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

-- | @0 + n ≡ m → n ≡ m@
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

-------------------------------------------------------------------------------
-- Lemmas: succ
-------------------------------------------------------------------------------

-- | @n + m ≡ p → n + S m ≡ S p@
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

-- | @n + S m ≡ S p → n + m ≡ p@
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

-- | @n + m ≡ p → S n + m ≡ S p@
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

-- | @S n + m ≡ S p → n + m ≡ p@
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

-------------------------------------------------------------------------------
-- Lemmas: swap
-------------------------------------------------------------------------------

-- | @n + S m ≡ p → S n + m ≡ p@
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)

-- | @S n + m ≡ p → n + S m ≡ p@
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)