-- |
-- Module      : Data.Monoid.Additive
-- Copyright   : (c) Justus Sagemüller 2022
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsag $ hvl.no
-- Stability   : experimental
-- Portability : portable
-- 

{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE UndecidableInstances     #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE DefaultSignatures        #-}
{-# LANGUAGE DeriveGeneric            #-}
{-# LANGUAGE DeriveAnyClass           #-}
{-# LANGUAGE StandaloneDeriving       #-}
{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE UnicodeSyntax            #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE EmptyCase                #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE TypeInType               #-}
{-# LANGUAGE CPP                      #-}


module Data.Monoid.Additive (AdditiveMonoid(..), HalfSpace(..)) where

import Data.VectorSpace
import Math.Manifold.VectorSpace.Scalar
import Data.AffineSpace
import Data.Int
import Data.Word

import Math.Manifold.Core.PseudoAffine
import Math.Manifold.Core.Types
import Math.Manifold.VectorSpace.ZeroDimensional
import Control.Applicative
import Control.Arrow
import Data.Void

import qualified GHC.Generics as Gnrx
import GHC.Generics (Generic, (:*:)(..))
import Data.Kind (Type)
import Proof.Propositional (Empty(..))



type AMRep h = Gnrx.Rep h Void

class AdditiveMonoid h where
  zeroHV :: h
  default zeroHV :: (Generic h, AdditiveMonoid (AMRep h)) => h
  zeroHV = forall a x. Generic a => Rep a x -> a
Gnrx.to (forall h. AdditiveMonoid h => h
zeroHV :: AMRep h)
  addHVs :: h -> h -> h
  default addHVs :: (Generic h, AdditiveMonoid (AMRep h)) => h -> h -> h
  addHVs h
p h
q = forall a x. Generic a => Rep a x -> a
Gnrx.to (forall h. AdditiveMonoid h => h -> h -> h
addHVs (forall a x. Generic a => a -> Rep a x
Gnrx.from h
p) (forall a x. Generic a => a -> Rep a x
Gnrx.from h
q) :: AMRep h)

instance AdditiveMonoid h => AdditiveMonoid (Gnrx.Rec0 h s) where
  zeroHV :: Rec0 h s
zeroHV = forall k i c (p :: k). c -> K1 i c p
Gnrx.K1 forall h. AdditiveMonoid h => h
zeroHV
  addHVs :: Rec0 h s -> Rec0 h s -> Rec0 h s
addHVs (Gnrx.K1 h
p) (Gnrx.K1 h
q) = forall k i c (p :: k). c -> K1 i c p
Gnrx.K1 forall a b. (a -> b) -> a -> b
$ forall h. AdditiveMonoid h => h -> h -> h
addHVs h
p h
q
instance AdditiveMonoid (f p) => AdditiveMonoid (Gnrx.M1 i c f p) where
  zeroHV :: M1 i c f p
zeroHV = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
Gnrx.M1 forall h. AdditiveMonoid h => h
zeroHV
  addHVs :: M1 i c f p -> M1 i c f p -> M1 i c f p
addHVs (Gnrx.M1 f p
p) (Gnrx.M1 f p
q) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
Gnrx.M1 forall a b. (a -> b) -> a -> b
$ forall h. AdditiveMonoid h => h -> h -> h
addHVs f p
p f p
q
instance (AdditiveMonoid (f p), AdditiveMonoid (g p))
            => AdditiveMonoid ((f:*:g) p) where
  zeroHV :: (:*:) f g p
zeroHV = forall h. AdditiveMonoid h => h
zeroHV forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall h. AdditiveMonoid h => h
zeroHV
  addHVs :: (:*:) f g p -> (:*:) f g p -> (:*:) f g p
addHVs (f p
x:*:g p
y) (f p
ξ:*:g p
υ) = forall h. AdditiveMonoid h => h -> h -> h
addHVs f p
x f p
ξ forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall h. AdditiveMonoid h => h -> h -> h
addHVs g p
y g p
υ

#define AdditiveGroupMonoid(g)     \
instance AdditiveMonoid (g) where { \
  zeroHV = zeroV;                    \
  addHVs = (^+^) }

#define NumAdditiveMonoid(g)       \
instance AdditiveMonoid (g) where { \
  zeroHV = 0;                        \
  addHVs = (+) }

NumAdditiveMonoid(Int)
NumAdditiveMonoid(Integer)
NumAdditiveMonoid(Float)
NumAdditiveMonoid(Double)
NumAdditiveMonoid(Int8)
NumAdditiveMonoid(Int16)
NumAdditiveMonoid(Int32)
NumAdditiveMonoid(Int64)
NumAdditiveMonoid(Word)
NumAdditiveMonoid(Word8)
NumAdditiveMonoid(Word16)
NumAdditiveMonoid(Word32)
NumAdditiveMonoid(Word64)

instance (AdditiveMonoid h, AdditiveMonoid i) => AdditiveMonoid (h,i)
instance (AdditiveMonoid h, AdditiveMonoid i, AdditiveMonoid j) => AdditiveMonoid (h,i,j)

class AdditiveMonoid h => HalfSpace h where
  type FullSubspace h :: Type
  type FullSubspace h = GenericFullSubspace h
  type Ray h :: Type
  type Ray h = Ray (AMRep h)
  type MirrorJoin h :: Type
  type MirrorJoin h = GenericMirrorJoin h
  scaleNonNeg :: Ray h -> h -> h
  default scaleNonNeg :: ( Generic h, HalfSpace (AMRep h)
                         , FullSubspace h ~ GenericFullSubspace h
                         , Ray h ~ Ray (AMRep h) )
             => Ray h -> h -> h
  scaleNonNeg Ray h
μ h
p = forall a x. Generic a => Rep a x -> a
Gnrx.to (forall h. HalfSpace h => Ray h -> h -> h
scaleNonNeg Ray h
μ (forall a x. Generic a => a -> Rep a x
Gnrx.from h
p) :: AMRep h)
  fromFullSubspace :: FullSubspace h -> h
  default fromFullSubspace :: ( Generic h, HalfSpace (AMRep h)
                              , FullSubspace h ~ GenericFullSubspace h
                              , Ray h ~ Ray (AMRep h) )
             => FullSubspace h -> h
  fromFullSubspace (GenericFullSubspace FullSubspace (AMRep h)
x) = forall a x. Generic a => Rep a x -> a
Gnrx.to (forall h. HalfSpace h => FullSubspace h -> h
fromFullSubspace FullSubspace (AMRep h)
x :: AMRep h)
  projectToFullSubspace :: h -> FullSubspace h
  default projectToFullSubspace :: ( Generic h, HalfSpace (AMRep h)
                                   , FullSubspace h ~ GenericFullSubspace h
                                   , Ray h ~ Ray (AMRep h) )
             => h -> FullSubspace h
  projectToFullSubspace h
p
           = forall h. FullSubspace (AMRep h) -> GenericFullSubspace h
GenericFullSubspace (forall h. HalfSpace h => h -> FullSubspace h
projectToFullSubspace (forall a x. Generic a => a -> Rep a x
Gnrx.from h
p :: AMRep h))
  fullSubspaceIsVectorSpace
   :: ( (VectorSpace (FullSubspace h)
        , ScalarSpace (Scalar (FullSubspace h))
        , Scalar (FullSubspace h) ~ MirrorJoin (Ray h) ) => r) -> r
  default fullSubspaceIsVectorSpace
       :: ( VectorSpace (FullSubspace h)
          , ScalarSpace (Scalar (FullSubspace h))
          , Scalar (FullSubspace h) ~ MirrorJoin (Ray h) )
   => ( ( VectorSpace (FullSubspace h)
        , ScalarSpace (Scalar (FullSubspace h))
        , Scalar (FullSubspace h) ~ MirrorJoin (Ray h)
        ) => r) -> r
  fullSubspaceIsVectorSpace (VectorSpace (FullSubspace h),
 ScalarSpace (Scalar (FullSubspace h)),
 Scalar (FullSubspace h) ~ MirrorJoin (Ray h)) =>
r
q = (VectorSpace (FullSubspace h),
 ScalarSpace (Scalar (FullSubspace h)),
 Scalar (FullSubspace h) ~ MirrorJoin (Ray h)) =>
r
q
  rayIsHalfSpace :: (HalfSpace (Ray h) => r) -> r
  default rayIsHalfSpace :: HalfSpace (Ray h) => (HalfSpace (Ray h) => r) -> r
  rayIsHalfSpace HalfSpace (Ray h) => r
q = HalfSpace (Ray h) => r
q
  mirrorJoinIsVectorSpace
   :: ((VectorSpace (MirrorJoin h), Scalar (MirrorJoin h) ~ MirrorJoin (Ray h)) => r) -> r
  default mirrorJoinIsVectorSpace
       :: ( VectorSpace (MirrorJoin h), Scalar (MirrorJoin h) ~ MirrorJoin (Ray h) )
   => ((VectorSpace (MirrorJoin h), Scalar (MirrorJoin h) ~ MirrorJoin (Ray h)) => r) -> r
  mirrorJoinIsVectorSpace (VectorSpace (MirrorJoin h),
 Scalar (MirrorJoin h) ~ MirrorJoin (Ray h)) =>
r
q = (VectorSpace (MirrorJoin h),
 Scalar (MirrorJoin h) ~ MirrorJoin (Ray h)) =>
r
q
  fromPositiveHalf :: h -> MirrorJoin h
  default fromPositiveHalf :: ( Generic h, HalfSpace (AMRep h)
                              , MirrorJoin h ~ GenericMirrorJoin h
                              , Ray h ~ Ray (AMRep h) )
             => h -> MirrorJoin h
  fromPositiveHalf h
p = forall h. MirrorJoin (AMRep h) -> GenericMirrorJoin h
GenericMirrorJoin forall a b. (a -> b) -> a -> b
$ forall h. HalfSpace h => h -> MirrorJoin h
fromPositiveHalf (forall a x. Generic a => a -> Rep a x
Gnrx.from h
p :: AMRep h)
  fromNegativeHalf :: h -> MirrorJoin h
  default fromNegativeHalf :: ( Generic h, HalfSpace (AMRep h)
                              , MirrorJoin h ~ GenericMirrorJoin h
                              , Ray h ~ Ray (AMRep h) )
             => h -> MirrorJoin h
  fromNegativeHalf h
p = forall h. MirrorJoin (AMRep h) -> GenericMirrorJoin h
GenericMirrorJoin forall a b. (a -> b) -> a -> b
$ forall h. HalfSpace h => h -> MirrorJoin h
fromNegativeHalf (forall a x. Generic a => a -> Rep a x
Gnrx.from h
p :: AMRep h)

newtype GenericFullSubspace h = GenericFullSubspace
    { forall h. GenericFullSubspace h -> FullSubspace (AMRep h)
getGenericFullSubspace :: FullSubspace (AMRep h) }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall h x. Rep (GenericFullSubspace h) x -> GenericFullSubspace h
forall h x. GenericFullSubspace h -> Rep (GenericFullSubspace h) x
$cto :: forall h x. Rep (GenericFullSubspace h) x -> GenericFullSubspace h
$cfrom :: forall h x. GenericFullSubspace h -> Rep (GenericFullSubspace h) x
Generic)
instance AdditiveGroup (FullSubspace (AMRep h)) => AdditiveGroup (GenericFullSubspace h)
instance VectorSpace (FullSubspace (AMRep h)) => VectorSpace (GenericFullSubspace h)

newtype GenericMirrorJoin h = GenericMirrorJoin
    { forall h. GenericMirrorJoin h -> MirrorJoin (AMRep h)
getGenericMirrorJoin :: MirrorJoin (AMRep h) }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall h x. Rep (GenericMirrorJoin h) x -> GenericMirrorJoin h
forall h x. GenericMirrorJoin h -> Rep (GenericMirrorJoin h) x
$cto :: forall h x. Rep (GenericMirrorJoin h) x -> GenericMirrorJoin h
$cfrom :: forall h x. GenericMirrorJoin h -> Rep (GenericMirrorJoin h) x
Generic)
instance AdditiveGroup (MirrorJoin (AMRep h)) => AdditiveGroup (GenericMirrorJoin h)
instance VectorSpace (MirrorJoin (AMRep h)) => VectorSpace (GenericMirrorJoin h)

instance ∀ h s . HalfSpace h => HalfSpace (Gnrx.Rec0 h s) where
  type FullSubspace (Gnrx.Rec0 h s) = FullSubspace h
  type Ray (Gnrx.Rec0 h s) = Ray h
  type MirrorJoin (Gnrx.Rec0 h s) = MirrorJoin h
  scaleNonNeg :: Ray (Rec0 h s) -> Rec0 h s -> Rec0 h s
scaleNonNeg Ray (Rec0 h s)
μ (Gnrx.K1 h
p) = forall k i c (p :: k). c -> K1 i c p
Gnrx.K1 forall a b. (a -> b) -> a -> b
$ forall h. HalfSpace h => Ray h -> h -> h
scaleNonNeg Ray (Rec0 h s)
μ h
p
  fullSubspaceIsVectorSpace :: forall r.
((VectorSpace (FullSubspace (Rec0 h s)),
  ScalarSpace (Scalar (FullSubspace (Rec0 h s))),
  Scalar (FullSubspace (Rec0 h s)) ~ MirrorJoin (Ray (Rec0 h s))) =>
 r)
-> r
fullSubspaceIsVectorSpace (VectorSpace (FullSubspace (Rec0 h s)),
 ScalarSpace (Scalar (FullSubspace (Rec0 h s))),
 Scalar (FullSubspace (Rec0 h s)) ~ MirrorJoin (Ray (Rec0 h s))) =>
r
c = forall h r.
HalfSpace h =>
((VectorSpace (FullSubspace h),
  ScalarSpace (Scalar (FullSubspace h)),
  Scalar (FullSubspace h) ~ MirrorJoin (Ray h)) =>
 r)
-> r
fullSubspaceIsVectorSpace @h (VectorSpace (FullSubspace (Rec0 h s)),
 ScalarSpace (Scalar (FullSubspace (Rec0 h s))),
 Scalar (FullSubspace (Rec0 h s)) ~ MirrorJoin (Ray (Rec0 h s))) =>
r
c
  mirrorJoinIsVectorSpace :: forall r.
((VectorSpace (MirrorJoin (Rec0 h s)),
  Scalar (MirrorJoin (Rec0 h s)) ~ MirrorJoin (Ray (Rec0 h s))) =>
 r)
-> r
mirrorJoinIsVectorSpace (VectorSpace (MirrorJoin (Rec0 h s)),
 Scalar (MirrorJoin (Rec0 h s)) ~ MirrorJoin (Ray (Rec0 h s))) =>
r
c = forall h r.
HalfSpace h =>
((VectorSpace (MirrorJoin h),
  Scalar (MirrorJoin h) ~ MirrorJoin (Ray h)) =>
 r)
-> r
mirrorJoinIsVectorSpace @h (VectorSpace (MirrorJoin (Rec0 h s)),
 Scalar (MirrorJoin (Rec0 h s)) ~ MirrorJoin (Ray (Rec0 h s))) =>
r
c
  rayIsHalfSpace :: forall r. (HalfSpace (Ray (Rec0 h s)) => r) -> r
rayIsHalfSpace HalfSpace (Ray (Rec0 h s)) => r
c = forall h r. HalfSpace h => (HalfSpace (Ray h) => r) -> r
rayIsHalfSpace @h HalfSpace (Ray (Rec0 h s)) => r
c
  fromFullSubspace :: FullSubspace (Rec0 h s) -> Rec0 h s
fromFullSubspace FullSubspace (Rec0 h s)
x = forall k i c (p :: k). c -> K1 i c p
Gnrx.K1 forall a b. (a -> b) -> a -> b
$ forall h. HalfSpace h => FullSubspace h -> h
fromFullSubspace FullSubspace (Rec0 h s)
x
  projectToFullSubspace :: Rec0 h s -> FullSubspace (Rec0 h s)
projectToFullSubspace (Gnrx.K1 h
p) = forall h. HalfSpace h => h -> FullSubspace h
projectToFullSubspace h
p
  fromPositiveHalf :: Rec0 h s -> MirrorJoin (Rec0 h s)
fromPositiveHalf (Gnrx.K1 h
p) = forall h. HalfSpace h => h -> MirrorJoin h
fromPositiveHalf h
p
  fromNegativeHalf :: Rec0 h s -> MirrorJoin (Rec0 h s)
fromNegativeHalf (Gnrx.K1 h
p) = forall h. HalfSpace h => h -> MirrorJoin h
fromNegativeHalf h
p
instance HalfSpace (f p) => HalfSpace (Gnrx.M1 i c f p) where
  type FullSubspace (Gnrx.M1 i c f p) = FullSubspace (f p)
  type Ray (Gnrx.M1 i c f p) = Ray (f p)
  type MirrorJoin (Gnrx.M1 i c f p) = MirrorJoin (f p)
  scaleNonNeg :: Ray (M1 i c f p) -> M1 i c f p -> M1 i c f p
scaleNonNeg Ray (M1 i c f p)
μ (Gnrx.M1 f p
p) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
Gnrx.M1 forall a b. (a -> b) -> a -> b
$ forall h. HalfSpace h => Ray h -> h -> h
scaleNonNeg Ray (M1 i c f p)
μ f p
p
  fullSubspaceIsVectorSpace :: forall r.
((VectorSpace (FullSubspace (M1 i c f p)),
  ScalarSpace (Scalar (FullSubspace (M1 i c f p))),
  Scalar (FullSubspace (M1 i c f p))
  ~ MirrorJoin (Ray (M1 i c f p))) =>
 r)
-> r
fullSubspaceIsVectorSpace (VectorSpace (FullSubspace (M1 i c f p)),
 ScalarSpace (Scalar (FullSubspace (M1 i c f p))),
 Scalar (FullSubspace (M1 i c f p))
 ~ MirrorJoin (Ray (M1 i c f p))) =>
r
c = forall h r.
HalfSpace h =>
((VectorSpace (FullSubspace h),
  ScalarSpace (Scalar (FullSubspace h)),
  Scalar (FullSubspace h) ~ MirrorJoin (Ray h)) =>
 r)
-> r
fullSubspaceIsVectorSpace @(f p) (VectorSpace (FullSubspace (M1 i c f p)),
 ScalarSpace (Scalar (FullSubspace (M1 i c f p))),
 Scalar (FullSubspace (M1 i c f p))
 ~ MirrorJoin (Ray (M1 i c f p))) =>
r
c
  mirrorJoinIsVectorSpace :: forall r.
((VectorSpace (MirrorJoin (M1 i c f p)),
  Scalar (MirrorJoin (M1 i c f p))
  ~ MirrorJoin (Ray (M1 i c f p))) =>
 r)
-> r
mirrorJoinIsVectorSpace (VectorSpace (MirrorJoin (M1 i c f p)),
 Scalar (MirrorJoin (M1 i c f p))
 ~ MirrorJoin (Ray (M1 i c f p))) =>
r
c = forall h r.
HalfSpace h =>
((VectorSpace (MirrorJoin h),
  Scalar (MirrorJoin h) ~ MirrorJoin (Ray h)) =>
 r)
-> r
mirrorJoinIsVectorSpace @(f p) (VectorSpace (MirrorJoin (M1 i c f p)),
 Scalar (MirrorJoin (M1 i c f p))
 ~ MirrorJoin (Ray (M1 i c f p))) =>
r
c
  rayIsHalfSpace :: forall r. (HalfSpace (Ray (M1 i c f p)) => r) -> r
rayIsHalfSpace HalfSpace (Ray (M1 i c f p)) => r
c = forall h r. HalfSpace h => (HalfSpace (Ray h) => r) -> r
rayIsHalfSpace @(f p) HalfSpace (Ray (M1 i c f p)) => r
c
  fromFullSubspace :: FullSubspace (M1 i c f p) -> M1 i c f p
fromFullSubspace FullSubspace (M1 i c f p)
x = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
Gnrx.M1 forall a b. (a -> b) -> a -> b
$ forall h. HalfSpace h => FullSubspace h -> h
fromFullSubspace FullSubspace (M1 i c f p)
x
  projectToFullSubspace :: M1 i c f p -> FullSubspace (M1 i c f p)
projectToFullSubspace (Gnrx.M1 f p
p) = forall h. HalfSpace h => h -> FullSubspace h
projectToFullSubspace f p
p
  fromPositiveHalf :: M1 i c f p -> MirrorJoin (M1 i c f p)
fromPositiveHalf (Gnrx.M1 f p
p) = forall h. HalfSpace h => h -> MirrorJoin h
fromPositiveHalf f p
p
  fromNegativeHalf :: M1 i c f p -> MirrorJoin (M1 i c f p)
fromNegativeHalf (Gnrx.M1 f p
p) = forall h. HalfSpace h => h -> MirrorJoin h
fromNegativeHalf f p
p

data GenericProductFullSubspace f g p
   = GenericProductFullSubspace { forall {k} (f :: k -> *) (g :: k -> *) (p :: k).
GenericProductFullSubspace f g p -> FullSubspace (f p)
lFullSubspace :: !(FullSubspace (f p))
                                , forall {k} (f :: k -> *) (g :: k -> *) (p :: k).
GenericProductFullSubspace f g p -> g p
rFullSpace :: !(g p) }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (f :: k -> *) (g :: k -> *) (p :: k) x.
Rep (GenericProductFullSubspace f g p) x
-> GenericProductFullSubspace f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k) x.
GenericProductFullSubspace f g p
-> Rep (GenericProductFullSubspace f g p) x
$cto :: forall k (f :: k -> *) (g :: k -> *) (p :: k) x.
Rep (GenericProductFullSubspace f g p) x
-> GenericProductFullSubspace f g p
$cfrom :: forall k (f :: k -> *) (g :: k -> *) (p :: k) x.
GenericProductFullSubspace f g p
-> Rep (GenericProductFullSubspace f g p) x
Generic)
deriving instance (AdditiveGroup (FullSubspace (f p)), AdditiveGroup (g p))
           => AdditiveGroup (GenericProductFullSubspace f g p)
deriving instance ( VectorSpace (FullSubspace (f p)), VectorSpace (g p)
                  , Scalar (FullSubspace (f p)) ~ Scalar (g p) )
           => VectorSpace (GenericProductFullSubspace f g p)

data GenericProductMirrorJoin f g p
   = GenericProductMirrorJoin { forall {k} (f :: k -> *) (g :: k -> *) (p :: k).
GenericProductMirrorJoin f g p -> MirrorJoin (f p)
lPMJcomponent :: !(MirrorJoin (f p))
                              , forall {k} (f :: k -> *) (g :: k -> *) (p :: k).
GenericProductMirrorJoin f g p -> g p
rPMJcomponent :: !(g p) }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (f :: k -> *) (g :: k -> *) (p :: k) x.
Rep (GenericProductMirrorJoin f g p) x
-> GenericProductMirrorJoin f g p
forall k (f :: k -> *) (g :: k -> *) (p :: k) x.
GenericProductMirrorJoin f g p
-> Rep (GenericProductMirrorJoin f g p) x
$cto :: forall k (f :: k -> *) (g :: k -> *) (p :: k) x.
Rep (GenericProductMirrorJoin f g p) x
-> GenericProductMirrorJoin f g p
$cfrom :: forall k (f :: k -> *) (g :: k -> *) (p :: k) x.
GenericProductMirrorJoin f g p
-> Rep (GenericProductMirrorJoin f g p) x
Generic)
deriving instance (AdditiveGroup (MirrorJoin (f p)), AdditiveGroup (g p))
           => AdditiveGroup (GenericProductMirrorJoin f g p)
deriving instance ( VectorSpace (MirrorJoin (f p)), VectorSpace (g p)
                  , Scalar (MirrorJoin (f p)) ~ Scalar (g p) )
           => VectorSpace (GenericProductMirrorJoin f g p)

instance ∀ f g p . ( HalfSpace (f p), VectorSpace (g p), AdditiveMonoid (g p)
                   , Ray (f p) ~ Cℝay (ZeroDim (Scalar (g p))) )
             => HalfSpace ((f:*:g) p) where
  type FullSubspace ((f:*:g) p) = GenericProductFullSubspace f g p
  type Ray ((f:*:g) p) = Cℝay (ZeroDim (Scalar (g p)))
  type MirrorJoin ((f:*:g) p) = GenericProductMirrorJoin f g p
  scaleNonNeg :: Ray ((:*:) f g p) -> (:*:) f g p -> (:*:) f g p
scaleNonNeg (Cℝay Scalar (Needle (ZeroDim (Scalar (g p))))
μ ZeroDim (Scalar (g p))
Origin) (f p
x:*:g p
y) = forall h. HalfSpace h => Ray h -> h -> h
scaleNonNeg (forall x. Scalar (Needle x) -> x -> Cℝay x
Cℝay Scalar (Needle (ZeroDim (Scalar (g p))))
μ forall s. ZeroDim s
Origin) f p
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (Scalar (Needle (ZeroDim (Scalar (g p))))
μforall v. VectorSpace v => Scalar v -> v -> v
*^g p
y)
  fromFullSubspace :: FullSubspace ((:*:) f g p) -> (:*:) f g p
fromFullSubspace (GenericProductFullSubspace FullSubspace (f p)
xf g p
y) = forall h. HalfSpace h => FullSubspace h -> h
fromFullSubspace FullSubspace (f p)
xf forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g p
y
  fullSubspaceIsVectorSpace :: forall r.
((VectorSpace (FullSubspace ((:*:) f g p)),
  ScalarSpace (Scalar (FullSubspace ((:*:) f g p))),
  Scalar (FullSubspace ((:*:) f g p))
  ~ MirrorJoin (Ray ((:*:) f g p))) =>
 r)
-> r
fullSubspaceIsVectorSpace (VectorSpace (FullSubspace ((:*:) f g p)),
 ScalarSpace (Scalar (FullSubspace ((:*:) f g p))),
 Scalar (FullSubspace ((:*:) f g p))
 ~ MirrorJoin (Ray ((:*:) f g p))) =>
r
c = forall h r.
HalfSpace h =>
((VectorSpace (FullSubspace h),
  ScalarSpace (Scalar (FullSubspace h)),
  Scalar (FullSubspace h) ~ MirrorJoin (Ray h)) =>
 r)
-> r
fullSubspaceIsVectorSpace @(f p) (VectorSpace (FullSubspace ((:*:) f g p)),
 ScalarSpace (Scalar (FullSubspace ((:*:) f g p))),
 Scalar (FullSubspace ((:*:) f g p))
 ~ MirrorJoin (Ray ((:*:) f g p))) =>
r
c
  mirrorJoinIsVectorSpace :: forall r.
((VectorSpace (MirrorJoin ((:*:) f g p)),
  Scalar (MirrorJoin ((:*:) f g p))
  ~ MirrorJoin (Ray ((:*:) f g p))) =>
 r)
-> r
mirrorJoinIsVectorSpace (VectorSpace (MirrorJoin ((:*:) f g p)),
 Scalar (MirrorJoin ((:*:) f g p))
 ~ MirrorJoin (Ray ((:*:) f g p))) =>
r
c = forall h r.
HalfSpace h =>
((VectorSpace (MirrorJoin h),
  Scalar (MirrorJoin h) ~ MirrorJoin (Ray h)) =>
 r)
-> r
mirrorJoinIsVectorSpace @(f p) (VectorSpace (MirrorJoin ((:*:) f g p)),
 Scalar (MirrorJoin ((:*:) f g p))
 ~ MirrorJoin (Ray ((:*:) f g p))) =>
r
c
  rayIsHalfSpace :: forall r. (HalfSpace (Ray ((:*:) f g p)) => r) -> r
rayIsHalfSpace HalfSpace (Ray ((:*:) f g p)) => r
c = forall h r. HalfSpace h => (HalfSpace (Ray h) => r) -> r
rayIsHalfSpace @(f p) HalfSpace (Ray ((:*:) f g p)) => r
c
  fromPositiveHalf :: (:*:) f g p -> MirrorJoin ((:*:) f g p)
fromPositiveHalf (f p
x:*:g p
y) = forall {k} (f :: k -> *) (g :: k -> *) (p :: k).
MirrorJoin (f p) -> g p -> GenericProductMirrorJoin f g p
GenericProductMirrorJoin (forall h. HalfSpace h => h -> MirrorJoin h
fromPositiveHalf f p
x) g p
y
  fromNegativeHalf :: (:*:) f g p -> MirrorJoin ((:*:) f g p)
fromNegativeHalf (f p
x:*:g p
y) = forall {k} (f :: k -> *) (g :: k -> *) (p :: k).
MirrorJoin (f p) -> g p -> GenericProductMirrorJoin f g p
GenericProductMirrorJoin (forall h. HalfSpace h => h -> MirrorJoin h
fromNegativeHalf f p
x) g p
y
  projectToFullSubspace :: (:*:) f g p -> FullSubspace ((:*:) f g p)
projectToFullSubspace (f p
x:*:g p
y) = forall {k} (f :: k -> *) (g :: k -> *) (p :: k).
FullSubspace (f p) -> g p -> GenericProductFullSubspace f g p
GenericProductFullSubspace (forall h. HalfSpace h => h -> FullSubspace h
projectToFullSubspace f p
x) g p
y

instance AdditiveMonoid (ZeroDim k) where
  zeroHV :: ZeroDim k
zeroHV = forall s. ZeroDim s
Origin
  addHVs :: ZeroDim k -> ZeroDim k -> ZeroDim k
addHVs ZeroDim k
Origin ZeroDim k
Origin = forall s. ZeroDim s
Origin

instance ScalarSpace k => HalfSpace (ZeroDim k) where
  type FullSubspace (ZeroDim k) = ZeroDim k
  type Ray (ZeroDim k) = Cℝay (ZeroDim k)
  type MirrorJoin (ZeroDim k) = ZeroDim k
  scaleNonNeg :: Ray (ZeroDim k) -> ZeroDim k -> ZeroDim k
scaleNonNeg Ray (ZeroDim k)
_ ZeroDim k
Origin = forall s. ZeroDim s
Origin
  fromFullSubspace :: FullSubspace (ZeroDim k) -> ZeroDim k
fromFullSubspace = forall a. a -> a
id
  projectToFullSubspace :: ZeroDim k -> FullSubspace (ZeroDim k)
projectToFullSubspace = forall a. a -> a
id
  rayIsHalfSpace :: forall r. (HalfSpace (Ray (ZeroDim k)) => r) -> r
rayIsHalfSpace HalfSpace (Ray (ZeroDim k)) => r
q = HalfSpace (Ray (ZeroDim k)) => r
q
  fromPositiveHalf :: ZeroDim k -> MirrorJoin (ZeroDim k)
fromPositiveHalf = forall a. a -> a
id
  fromNegativeHalf :: ZeroDim k -> MirrorJoin (ZeroDim k)
fromNegativeHalf = forall a. a -> a
id

instance ∀ k . Num k => AdditiveMonoid (Cℝay (ZeroDim k)) where
  zeroHV :: Cℝay (ZeroDim k)
zeroHV = forall x. Scalar (Needle x) -> x -> Cℝay x
Cℝay k
0 forall s. ZeroDim s
Origin
  addHVs :: Cℝay (ZeroDim k) -> Cℝay (ZeroDim k) -> Cℝay (ZeroDim k)
addHVs (Cℝay Scalar (Needle (ZeroDim k))
a ZeroDim k
Origin) (Cℝay Scalar (Needle (ZeroDim k))
b ZeroDim k
Origin) = forall x. Scalar (Needle x) -> x -> Cℝay x
Cℝay (Scalar (Needle (ZeroDim k))
aforall a. Num a => a -> a -> a
+Scalar (Needle (ZeroDim k))
b) forall s. ZeroDim s
Origin
instance (Num k, VectorSpace k, Scalar k ~ k) => HalfSpace (Cℝay (ZeroDim k)) where
  type FullSubspace (Cℝay (ZeroDim k)) = ZeroDim k
  type Ray (Cℝay (ZeroDim k)) = Cℝay (ZeroDim k)
  type MirrorJoin (Cℝay (ZeroDim k)) = k
  scaleNonNeg :: Ray (Cℝay (ZeroDim k)) -> Cℝay (ZeroDim k) -> Cℝay (ZeroDim k)
scaleNonNeg (Cℝay Scalar (Needle (ZeroDim k))
μ ZeroDim k
Origin) (Cℝay Scalar (Needle (ZeroDim k))
l ZeroDim k
Origin) = forall x. Scalar (Needle x) -> x -> Cℝay x
Cℝay (Scalar (Needle (ZeroDim k))
μforall a. Num a => a -> a -> a
*Scalar (Needle (ZeroDim k))
l) forall s. ZeroDim s
Origin
  fromFullSubspace :: FullSubspace (Cℝay (ZeroDim k)) -> Cℝay (ZeroDim k)
fromFullSubspace ZeroDim k
FullSubspace (Cℝay (ZeroDim k))
Origin = forall x. Scalar (Needle x) -> x -> Cℝay x
Cℝay k
0 forall s. ZeroDim s
Origin
  projectToFullSubspace :: Cℝay (ZeroDim k) -> FullSubspace (Cℝay (ZeroDim k))
projectToFullSubspace (Cℝay Scalar (Needle (ZeroDim k))
_ ZeroDim k
Origin) = forall s. ZeroDim s
Origin
  fromPositiveHalf :: Cℝay (ZeroDim k) -> MirrorJoin (Cℝay (ZeroDim k))
fromPositiveHalf (Cℝay Scalar (Needle (ZeroDim k))
l ZeroDim k
Origin) = Scalar (Needle (ZeroDim k))
l
  fromNegativeHalf :: Cℝay (ZeroDim k) -> MirrorJoin (Cℝay (ZeroDim k))
fromNegativeHalf (Cℝay Scalar (Needle (ZeroDim k))
l ZeroDim k
Origin) = -Scalar (Needle (ZeroDim k))
l
  
instance ∀ x y . ( HalfSpace x, VectorSpace y, AdditiveMonoid y
                 , Ray x ~ Cℝay (ZeroDim (Scalar y)) ) => HalfSpace (x,y) where
  fullSubspaceIsVectorSpace :: forall r.
((VectorSpace (FullSubspace (x, y)),
  ScalarSpace (Scalar (FullSubspace (x, y))),
  Scalar (FullSubspace (x, y)) ~ MirrorJoin (Ray (x, y))) =>
 r)
-> r
fullSubspaceIsVectorSpace (VectorSpace (FullSubspace (x, y)),
 ScalarSpace (Scalar (FullSubspace (x, y))),
 Scalar (FullSubspace (x, y)) ~ MirrorJoin (Ray (x, y))) =>
r
c = forall h r.
HalfSpace h =>
((VectorSpace (FullSubspace h),
  ScalarSpace (Scalar (FullSubspace h)),
  Scalar (FullSubspace h) ~ MirrorJoin (Ray h)) =>
 r)
-> r
fullSubspaceIsVectorSpace @x (VectorSpace (FullSubspace (x, y)),
 ScalarSpace (Scalar (FullSubspace (x, y))),
 Scalar (FullSubspace (x, y)) ~ MirrorJoin (Ray (x, y))) =>
r
c
  rayIsHalfSpace :: forall r. (HalfSpace (Ray (x, y)) => r) -> r
rayIsHalfSpace HalfSpace (Ray (x, y)) => r
c = forall h r. HalfSpace h => (HalfSpace (Ray h) => r) -> r
rayIsHalfSpace @x HalfSpace (Ray (x, y)) => r
c
  mirrorJoinIsVectorSpace :: forall r.
((VectorSpace (MirrorJoin (x, y)),
  Scalar (MirrorJoin (x, y)) ~ MirrorJoin (Ray (x, y))) =>
 r)
-> r
mirrorJoinIsVectorSpace (VectorSpace (MirrorJoin (x, y)),
 Scalar (MirrorJoin (x, y)) ~ MirrorJoin (Ray (x, y))) =>
r
c = forall h r.
HalfSpace h =>
((VectorSpace (MirrorJoin h),
  Scalar (MirrorJoin h) ~ MirrorJoin (Ray h)) =>
 r)
-> r
mirrorJoinIsVectorSpace @x (VectorSpace (MirrorJoin (x, y)),
 Scalar (MirrorJoin (x, y)) ~ MirrorJoin (Ray (x, y))) =>
r
c


instance AdditiveGroup (Needle (Gnrx.Rep a Void))
            => AdditiveMonoid (GenericNeedle a) where
  zeroHV :: GenericNeedle a
zeroHV = forall x. Needle (VRep x) -> GenericNeedle x
GenericNeedle forall v. AdditiveGroup v => v
zeroV
  addHVs :: GenericNeedle a -> GenericNeedle a -> GenericNeedle a
addHVs (GenericNeedle Needle (Rep a Void)
v) (GenericNeedle Needle (Rep a Void)
w) = forall x. Needle (VRep x) -> GenericNeedle x
GenericNeedle forall a b. (a -> b) -> a -> b
$ Needle (Rep a Void)
vforall v. AdditiveGroup v => v -> v -> v
^+^Needle (Rep a Void)
w