-- |
-- Module      : Math.VectorSpace.DimensionAware.Theorems.MaybeNat
-- Copyright   : (c) Justus Sagemüller 2022
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE AllowAmbiguousTypes        #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE UnicodeSyntax              #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE NoStarIsType               #-}
{-# LANGUAGE CPP                        #-}

module Math.VectorSpace.DimensionAware.Theorems.MaybeNat where

#if MIN_VERSION_singletons(3,0,0)
import Prelude.Singletons (SNum(..))
import Data.Maybe.Singletons
import GHC.TypeLits.Singletons (SNat(..), withKnownNat, sDiv)
#else
import Data.Singletons.Prelude.Num (SNum(..))
import Data.Singletons.Prelude.Maybe (SMaybe(..))
import Data.Singletons.TypeLits (SNat(..), withKnownNat, sDiv)
#endif
import Data.Singletons
import qualified Data.Type.Natural as DTN
import GHC.TypeLits
import Unsafe.Coerce

type family ZipWith (f :: k -> l -> m) (a :: Maybe k) (b :: Maybe l) :: Maybe m where
  ZipWith f 'Nothing y = 'Nothing
  ZipWith f x 'Nothing = 'Nothing
  ZipWith f ('Just x) ('Just y) = 'Just (f x y)

type family ZipWithPlus (a :: Maybe Nat) (b :: Maybe Nat) :: Maybe Nat where
  ZipWithPlus 'Nothing y = 'Nothing
  ZipWithPlus x 'Nothing = 'Nothing
  ZipWithPlus ('Just x) ('Just y) = 'Just (x+y)

type family ZipWithTimes (a :: Maybe Nat) (b :: Maybe Nat) :: Maybe Nat where
  ZipWithTimes 'Nothing y = 'Nothing
  ZipWithTimes x 'Nothing = 'Nothing
  ZipWithTimes ('Just x) ('Just y) = 'Just (x*y)

type family MaybePred (a :: Nat) :: Maybe Nat where
  MaybePred 0 = 'Nothing
  MaybePred n = 'Just (n-1)

type family BindMaybePred (a :: Maybe Nat) :: Maybe Nat where
  BindMaybePred 'Nothing = 'Nothing
  BindMaybePred ('Just n) = MaybePred n

type TriangularNum (a :: Nat) = (a * (a+1))`Div`2

type family FmapTriangularNum (a :: Maybe Nat) where
  FmapTriangularNum 'Nothing = 'Nothing
  FmapTriangularNum ('Just n) = ('Just (TriangularNum n))

justNatSing :: ∀ (n :: Nat) . Sing n -> Sing ('Just n)
justNatSing :: forall (n :: Nat). Sing n -> Sing ('Just n)
justNatSing SNat n
Sing n
SNat = Sing ('Just n)
forall {k} (a :: k). SingI a => Sing a
sing

succMaybePredSing :: ∀ n . DTN.SNat n -> Sing (MaybePred (n+1))
succMaybePredSing :: forall (n :: Nat). SNat n -> Sing (MaybePred (n + 1))
succMaybePredSing SNat n
s = SMaybe ('Just n) -> SMaybe (MaybePred (n + 1))
forall a b. a -> b
unsafeCoerce (SNat n -> (KnownNat n => SMaybe ('Just n)) -> SMaybe ('Just n)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
DTN.withKnownNat SNat n
s (Sing n -> Sing ('Just n)
forall (n :: Nat). Sing n -> Sing ('Just n)
justNatSing (forall (n :: Nat). KnownNat n => SNat n
SNat @n)))

maybePredSing :: ∀ a . Sing a -> Sing (MaybePred a)
maybePredSing :: forall (a :: Nat). Sing a -> Sing (MaybePred a)
maybePredSing Sing a
α = SNat a
-> (KnownNat a => SMaybe (MaybePred a)) -> SMaybe (MaybePred a)
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat a
Sing a
α
   (case SNat a -> ZeroOrSucc a
forall (n :: Nat). SNat n -> ZeroOrSucc n
DTN.viewNat (forall (n :: Nat). KnownNat n => SNat n
DTN.sNat @a) of
      ZeroOrSucc a
DTN.IsZero -> Sing 'Nothing
SMaybe (MaybePred a)
forall {k} (a :: k). SingI a => Sing a
sing
      DTN.IsSucc SNat n1
β -> SNat n1 -> Sing (MaybePred (n1 + 1))
forall (n :: Nat). SNat n -> Sing (MaybePred (n + 1))
succMaybePredSing SNat n1
β
    )

binMaybePredSing :: ∀ a . Sing a -> Sing (BindMaybePred a)
binMaybePredSing :: forall (a :: Maybe Nat). Sing a -> Sing (BindMaybePred a)
binMaybePredSing Sing a
SMaybe a
SNothing = Sing 'Nothing
Sing (BindMaybePred a)
forall {k} (a :: k). SingI a => Sing a
sing
binMaybePredSing (SJust Sing n
ν) = Sing n -> Sing (MaybePred n)
forall (a :: Nat). Sing a -> Sing (MaybePred a)
maybePredSing Sing n
ν

triangularNumSing :: ∀ a . Sing a -> Sing (TriangularNum a)
triangularNumSing :: forall (a :: Nat). Sing a -> Sing (TriangularNum a)
triangularNumSing Sing a
α = (Sing a
α Sing a -> Sing (a + 1) -> Sing (Apply (Apply (*@#@$) a) (a + 1))
forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
%* (Sing a
αSing a -> Sing 1 -> Sing (Apply (Apply (+@#@$) a) 1)
forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+(forall (a :: Nat). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @1)))Sing (a * (a + 1)) -> Sing 2 -> Sing (Div (a * (a + 1)) 2)
forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Div x y)
`sDiv`(forall (a :: Nat). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @2)

fmapTriangularNumSing :: ∀ a . Sing a -> Sing (FmapTriangularNum a)
fmapTriangularNumSing :: forall (a :: Maybe Nat). Sing a -> Sing (FmapTriangularNum a)
fmapTriangularNumSing Sing a
SMaybe a
SNothing = Sing (FmapTriangularNum a)
SMaybe 'Nothing
forall a. SMaybe 'Nothing
SNothing
fmapTriangularNumSing (SJust Sing n
α) = Sing (Div (n * (n + 1)) 2) -> SMaybe ('Just (Div (n * (n + 1)) 2))
forall a (n :: a). Sing n -> SMaybe ('Just n)
SJust (Sing n -> Sing (Div (n * (n + 1)) 2)
forall (a :: Nat). Sing a -> Sing (TriangularNum a)
triangularNumSing Sing n
α)

zipWithPlusSing :: ∀ a b r . Sing a -> Sing b -> Sing (ZipWithPlus a b)
zipWithPlusSing :: forall {k} (a :: Maybe Nat) (b :: Maybe Nat) (r :: k).
Sing a -> Sing b -> Sing (ZipWithPlus a b)
zipWithPlusSing Sing a
SMaybe a
SNothing Sing b
_ = Sing 'Nothing
Sing (ZipWithPlus a b)
forall {k} (a :: k). SingI a => Sing a
sing
zipWithPlusSing Sing a
_ Sing b
SMaybe b
SNothing = Sing 'Nothing
Sing (ZipWithPlus a b)
forall {k} (a :: k). SingI a => Sing a
sing
zipWithPlusSing (SJust Sing n
α) (SJust Sing n
β) = SNat (n + n)
-> (KnownNat (n + n) => SMaybe ('Just (n + n)))
-> SMaybe ('Just (n + n))
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (Sing n
αSing n -> Sing n -> Sing (Apply (Apply (+@#@$) n) n)
forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+Sing n
β) Sing ('Just (n + n))
SMaybe ('Just (n + n))
KnownNat (n + n) => SMaybe ('Just (n + n))
forall {k} (a :: k). SingI a => Sing a
sing

zipWithTimesSing :: ∀ a b r . Sing a -> Sing b -> Sing (ZipWithTimes a b)
zipWithTimesSing :: forall {k} (a :: Maybe Nat) (b :: Maybe Nat) (r :: k).
Sing a -> Sing b -> Sing (ZipWithTimes a b)
zipWithTimesSing Sing a
SMaybe a
SNothing Sing b
_ = Sing 'Nothing
Sing (ZipWithTimes a b)
forall {k} (a :: k). SingI a => Sing a
sing
zipWithTimesSing Sing a
_ Sing b
SMaybe b
SNothing = Sing 'Nothing
Sing (ZipWithTimes a b)
forall {k} (a :: k). SingI a => Sing a
sing
zipWithTimesSing (SJust Sing n
α) (SJust Sing n
β) = SNat (n * n)
-> (KnownNat (n * n) => SMaybe ('Just (n * n)))
-> SMaybe ('Just (n * n))
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (Sing n
αSing n -> Sing n -> Sing (Apply (Apply (*@#@$) n) n)
forall (t1 :: Nat) (t2 :: Nat).
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
%*Sing n
β) Sing ('Just (n * n))
SMaybe ('Just (n * n))
KnownNat (n * n) => SMaybe ('Just (n * n))
forall {k} (a :: k). SingI a => Sing a
sing

zipWithTimesAssoc :: ∀ a b c r . Sing a -> Sing b -> Sing c
    -> ((ZipWithTimes a (ZipWithTimes b c) ~ ZipWithTimes (ZipWithTimes a b) c) => r)
           -> r
zipWithTimesAssoc :: forall (a :: Maybe Nat) (b :: Maybe Nat) (c :: Maybe Nat) r.
Sing a
-> Sing b
-> Sing c
-> ((ZipWithTimes a (ZipWithTimes b c)
     ~ ZipWithTimes (ZipWithTimes a b) c) =>
    r)
-> r
zipWithTimesAssoc Sing a
SMaybe a
SNothing Sing b
_ Sing c
_ (ZipWithTimes a (ZipWithTimes b c)
 ~ ZipWithTimes (ZipWithTimes a b) c) =>
r
φ = r
(ZipWithTimes a (ZipWithTimes b c)
 ~ ZipWithTimes (ZipWithTimes a b) c) =>
r
φ
zipWithTimesAssoc Sing a
_ Sing b
SMaybe b
SNothing Sing c
_ (ZipWithTimes a (ZipWithTimes b c)
 ~ ZipWithTimes (ZipWithTimes a b) c) =>
r
φ = r
(ZipWithTimes a (ZipWithTimes b c)
 ~ ZipWithTimes (ZipWithTimes a b) c) =>
r
φ
zipWithTimesAssoc Sing a
_ Sing b
_ Sing c
SMaybe c
SNothing (ZipWithTimes a (ZipWithTimes b c)
 ~ ZipWithTimes (ZipWithTimes a b) c) =>
r
φ = r
(ZipWithTimes a (ZipWithTimes b c)
 ~ ZipWithTimes (ZipWithTimes a b) c) =>
r
φ
zipWithTimesAssoc (SJust Sing n
_) (SJust Sing n
_) (SJust Sing n
_) (ZipWithTimes a (ZipWithTimes b c)
 ~ ZipWithTimes (ZipWithTimes a b) c) =>
r
φ = r
(ZipWithTimes a (ZipWithTimes b c)
 ~ ZipWithTimes (ZipWithTimes a b) c) =>
r
φ

zipWithTimesCommu :: ∀ a b r . Sing a -> Sing b
    -> ((ZipWithTimes a b ~ ZipWithTimes b a) => r) -> r
zipWithTimesCommu :: forall (a :: Maybe Nat) (b :: Maybe Nat) r.
Sing a
-> Sing b -> ((ZipWithTimes a b ~ ZipWithTimes b a) => r) -> r
zipWithTimesCommu Sing a
SMaybe a
SNothing Sing b
_ (ZipWithTimes a b ~ ZipWithTimes b a) => r
φ = r
(ZipWithTimes a b ~ ZipWithTimes b a) => r
φ
zipWithTimesCommu Sing a
_ Sing b
SMaybe b
SNothing (ZipWithTimes a b ~ ZipWithTimes b a) => r
φ = r
(ZipWithTimes a b ~ ZipWithTimes b a) => r
φ
zipWithTimesCommu (SJust Sing n
_) (SJust Sing n
_) (ZipWithTimes a b ~ ZipWithTimes b a) => r
φ = r
(ZipWithTimes a b ~ ZipWithTimes b a) => r
φ