-- |
-- 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 Sing n
SNat n
SNat = 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 = forall a b. a -> b
unsafeCoerce (forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
DTN.withKnownNat SNat n
s (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
α = forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing a
α
   (case forall (n :: Nat). SNat n -> ZeroOrSucc n
DTN.viewNat (forall (n :: Nat). KnownNat n => SNat n
DTN.sNat @a) of
      ZeroOrSucc a
DTN.IsZero -> forall {k} (a :: k). SingI a => Sing a
sing
      DTN.IsSucc SNat n1
β -> 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 = forall {k} (a :: k). SingI a => Sing a
sing
binMaybePredSing (SJust Sing 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
α forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
%* (Sing a
αforall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+(forall {k} (a :: k). SingI a => Sing a
sing @1)))forall (x :: Nat) (y :: Nat). Sing x -> Sing y -> Sing (Div x y)
`sDiv`(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 = forall a. SMaybe 'Nothing
SNothing
fmapTriangularNumSing (SJust Sing n
α) = forall a (n :: a). Sing n -> SMaybe ('Just n)
SJust (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
_ = forall {k} (a :: k). SingI a => Sing a
sing
zipWithPlusSing Sing a
_ Sing b
SMaybe b
SNothing = forall {k} (a :: k). SingI a => Sing a
sing
zipWithPlusSing (SJust Sing n
α) (SJust Sing n
β) = forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat (Sing n
αforall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+Sing 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
_ = forall {k} (a :: k). SingI a => Sing a
sing
zipWithTimesSing Sing a
_ Sing b
SMaybe b
SNothing = forall {k} (a :: k). SingI a => Sing a
sing
zipWithTimesSing (SJust Sing n
α) (SJust Sing n
β) = forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat (Sing n
αforall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
%*Sing 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
φ = (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
φ = (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
φ = (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
φ = (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
φ = (ZipWithTimes a b ~ ZipWithTimes b a) => r
φ
zipWithTimesCommu Sing a
_ Sing b
SMaybe b
SNothing (ZipWithTimes a b ~ ZipWithTimes b a) => r
φ = (ZipWithTimes a b ~ ZipWithTimes b a) => r
φ
zipWithTimesCommu (SJust Sing n
_) (SJust Sing n
_) (ZipWithTimes a b ~ ZipWithTimes b a) => r
φ = (ZipWithTimes a b ~ ZipWithTimes b a) => r
φ