{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
module Type.Data.Num.Unary.Proof (
    Nat(..), Pos(..),
    natFromPos,
    addNat, addPosL, addPosR,
    mulNat, mulPos,
    ) where

import Type.Data.Num.Unary
          (Natural, Positive, Succ, switchNat, switchPos, (:+:), (:*:))

data Nat x = Natural x => Nat
data Pos x = Positive x => Pos


succNat :: Nat x -> Nat (Succ x)
succNat Nat = Nat

prevNat :: (Natural x) => Nat (Succ x) -> Nat x
prevNat Nat = Nat

posSucc :: Nat x -> Pos (Succ x)
posSucc Nat = Pos

prevPos :: (Natural x) => Pos (Succ x) -> Nat x
prevPos Pos = Nat


natFromPos :: Pos x -> Nat x
natFromPos Pos = Nat


newtype
   AddNatTheorem x y =
      AddNatTheorem {
         runAddNatTheorem :: Nat x -> Nat y -> Nat (x :+: y)
      }

addNat :: Nat x -> Nat y -> Nat (x :+: y)
addNat x0 y0@Nat =
   runAddNatTheorem
      (switchNat
         (AddNatTheorem $ \Nat Nat -> Nat)
         (AddNatTheorem $ \x -> succNat . addNat x . prevNat))
      x0 y0


newtype
   AddPosRTheorem x y =
      AddPosRTheorem {
         runAddPosRTheorem :: Nat x -> Pos y -> Pos (x :+: y)
      }

addPosR :: Nat x -> Pos y -> Pos (x :+: y)
addPosR x0 y0@Pos =
   runAddPosRTheorem
      (switchPos
         (AddPosRTheorem $ \x ->
             posSucc . addNat x . prevPos))
      x0 y0


newtype
   AddPosLTheorem x y =
      AddPosLTheorem {
         runAddPosLTheorem :: Pos x -> Nat y -> Pos (x :+: y)
      }

addPosL :: Pos x -> Nat y -> Pos (x :+: y)
addPosL x0 y0@Nat =
   runAddPosLTheorem
      (switchNat
         (AddPosLTheorem $ \x _y -> x)
         (AddPosLTheorem $ \x ->
            posSucc . addNat (natFromPos x) . prevNat))
      x0 y0


newtype
   MulNatTheorem x y =
      MulNatTheorem {
         runMulNatTheorem :: Nat x -> Nat y -> Nat (x :*: y)
      }

mulNat :: Nat x -> Nat y -> Nat (x :*: y)
mulNat x0 y0@Nat =
   runMulNatTheorem
      (switchNat
         (MulNatTheorem $ \Nat Nat -> Nat)
         (MulNatTheorem $ \x -> addNat x . mulNat x . prevNat))
      x0 y0


newtype
   MulPosTheorem x y =
      MulPosTheorem {
         runMulPosTheorem :: Pos x -> Pos y -> Pos (x :*: y)
      }

mulPos :: Pos x -> Pos y -> Pos (x :*: y)
mulPos x0 y0@Pos =
   runMulPosTheorem
      (switchPos
         (MulPosTheorem $ \x ->
            addPosL x . mulNat (natFromPos x) . prevPos))
      x0 y0