{-# LANGUAGE Safe #-}
module DeBruijn.Add (
    Add (AZ, AS),
    addToInt,
    addToSize,
    adding,
    -- * Lemmas
    rzeroAdd,
    unrzeroAdd,
    lzeroAdd,
    unlzeroAdd,
    rsuccAdd,
    unrsuccAdd,
    lsuccAdd,
    unlsuccAdd,
    swapAdd,
    unswapAdd,
) where

import Data.GADT.Show     (GShow (..))
import Data.Kind          (Type)
import Data.Some          (Some (..))
import Data.Type.Equality ((:~:) (..))

import DeBruijn.Ctx
import DeBruijn.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
data Add n m p where
    AZ :: Add EmptyCtx ctx ctx
    AS :: !(Add n ctx ctx') -> Add (S n) ctx (S ctx')

addToInt :: Add n m p -> Int
addToInt :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Int
addToInt = Int -> Add n m p -> Int
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p -> Int
go Int
0 where
    go :: Int -> Add n m p -> Int
    go :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p -> Int
go !Int
n Add n m p
AZ     = Int
n
    go !Int
n (AS Add n m ctx'
a) = Int -> Add n m ctx' -> Int
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Int -> Add n m p -> Int
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Add n m ctx'
a

addToSize :: Add n m p -> Size n
addToSize :: forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Size n
addToSize Add n m p
AZ     = Size n
Size 'Z
SZ
addToSize (AS Add n m ctx'
a) = Size n -> Size ('S n)
forall (ctx1 :: Ctx). Size ctx1 -> Size ('S ctx1)
SS (Add n m ctx' -> Size n
forall (n :: Ctx) (m :: Ctx) (p :: Ctx). Add n m p -> Size n
addToSize Add n m ctx'
a)

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

-- | 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 Size n
SZ     = Add n ctx ctx -> Some (Add n ctx)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some Add n ctx ctx
Add 'Z ctx ctx
forall (ctx :: Ctx). Add 'Z ctx ctx
AZ
adding (SS Size ctx1
s) = case Size ctx1 -> Some (Add ctx1 ctx)
forall (n :: Ctx) (ctx :: Ctx). Size n -> Some (Add n ctx)
adding Size ctx1
s of Some Add ctx1 ctx a
a -> Add n ctx (S a) -> Some (Add n ctx)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (Add ctx1 ctx a -> Add ('S ctx1) ctx (S a)
forall (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Add n ctx ctx' -> Add (S n) ctx (S ctx')
AS Add ctx1 ctx a
a)

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

-- | @n + 0 ≡ 0@
rzeroAdd :: Size n -> Add n EmptyCtx n
rzeroAdd :: forall (n :: Ctx). Size n -> Add n 'Z n
rzeroAdd Size n
SZ     = Add n 'Z n
Add 'Z 'Z 'Z
forall (ctx :: Ctx). Add 'Z ctx ctx
AZ
rzeroAdd (SS Size ctx1
s) = Add ctx1 'Z ctx1 -> Add ('S ctx1) 'Z ('S ctx1)
forall (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Add n ctx ctx' -> Add (S n) ctx (S ctx')
AS (Size ctx1 -> Add ctx1 'Z ctx1
forall (n :: Ctx). Size n -> Add n 'Z n
rzeroAdd Size ctx1
s)

-- | @n + 0 ≡ m → n ≡ m@
unrzeroAdd :: Add n EmptyCtx m -> n :~: m
unrzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add n 'Z m -> n :~: m
unrzeroAdd Add n 'Z m
AZ     = n :~: n
n :~: m
forall {k} (a :: k). a :~: a
Refl
unrzeroAdd (AS Add n 'Z ctx'
a) = case Add n 'Z ctx' -> n :~: ctx'
forall (n :: Ctx) (m :: Ctx). Add n 'Z m -> n :~: m
unrzeroAdd Add n 'Z ctx'
a of n :~: ctx'
Refl -> n :~: n
n :~: m
forall {k} (a :: k). a :~: a
Refl

-- | @0 + n ≡ 0@
lzeroAdd :: Size n -> Add EmptyCtx n n
lzeroAdd :: forall (n :: Ctx). Size n -> Add 'Z n n
lzeroAdd Size n
_ = Add 'Z n n
forall (ctx :: Ctx). Add 'Z ctx ctx
AZ

-- | @0 + n ≡ m → n ≡ m@
unlzeroAdd :: Add EmptyCtx n m -> n :~: m
unlzeroAdd :: forall (n :: Ctx) (m :: Ctx). Add 'Z n m -> n :~: m
unlzeroAdd Add 'Z 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
AZ     = Add n (S m) ('S p)
Add 'Z (S m) (S m)
forall (ctx :: Ctx). Add 'Z ctx ctx
AZ
rsuccAdd (AS Add n m ctx'
a) = Add n (S m) p -> Add ('S n) (S m) ('S p)
forall (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Add n ctx ctx' -> Add (S n) ctx (S ctx')
AS (Add n (S m) p -> Add ('S n) (S m) ('S p))
-> Add n (S m) p -> Add ('S n) (S m) ('S p)
forall a b. (a -> b) -> a -> b
$ Add n m ctx' -> Add n (S m) ('S ctx')
forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add n m p -> Add n (S m) (S p)
rsuccAdd Add n m ctx'
a

-- | @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)
AZ     = Add n m p
Add 'Z m m
forall (ctx :: Ctx). Add 'Z ctx ctx
AZ
unrsuccAdd (AS Add n (S m) ctx'
a) = Add n (S m) p -> Add ('S n) m p
forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add n (S m) p -> Add (S n) m p
swapAdd Add n (S m) p
Add n (S m) ctx'
a

-- | @n + m ≡ p → S n + m ≡ S p@
lsuccAdd :: Add n m p -> Add (S n) m (S p)
lsuccAdd :: forall (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Add n ctx ctx' -> Add (S n) ctx (S ctx')
lsuccAdd = Add n m p -> Add (S n) m (S p)
forall (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Add n ctx ctx' -> Add (S n) ctx (S ctx')
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 ctx'
a)= Add n m p
Add n m ctx'
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 Add n (S m) p
AZ     = Add n m m -> Add ('S n) m (S m)
forall (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Add n ctx ctx' -> Add (S n) ctx (S ctx')
AS Add n m m
Add 'Z m m
forall (ctx :: Ctx). Add 'Z ctx ctx
AZ
swapAdd (AS Add n (S m) ctx'
a) = Add n m ctx' -> Add ('S n) m ('S ctx')
forall (n :: Ctx) (ctx :: Ctx) (ctx' :: Ctx).
Add n ctx ctx' -> Add (S n) ctx (S ctx')
AS (Add n m ctx' -> Add ('S n) m ('S ctx'))
-> Add n m ctx' -> Add ('S n) m ('S ctx')
forall a b. (a -> b) -> a -> b
$ Add n (S m) ctx' -> Add ('S n) m ctx'
forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add n (S m) p -> Add (S n) m p
swapAdd Add n (S m) ctx'
a

-- | @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 (AS Add n m ctx'
a) = Add n m ctx' -> Add n ('S m) ('S ctx')
forall (n :: Ctx) (m :: Ctx) (p :: Ctx).
Add n m p -> Add n (S m) (S p)
rsuccAdd Add n m ctx'
Add n m ctx'
a