{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE CPP #-}
module Data.Manifold.WithBoundary
( SemimanifoldWithBoundary(..), PseudoAffineWithBoundary(..), ProjectableBoundary(..)
, SmfdWBoundWitness(..)
, AdditiveMonoid(..), HalfSpace(..)
) where
import Data.Manifold.WithBoundary.Class
import Data.VectorSpace
import Data.AffineSpace
import Data.Basis
import Math.Manifold.Core.PseudoAffine
import Data.Manifold.PseudoAffine
import Math.Manifold.Core.Types
import Data.Manifold.Types.Primitive
import Math.Manifold.VectorSpace.ZeroDimensional
import Math.LinearMap.Category ( Tensor(..), TensorSpace(..)
, LinearMap(..), LinearFunction(..), LinearSpace(..)
, Num', closedScalarWitness, ClosedScalarWitness(..)
, DualSpaceWitness(..), ScalarSpaceWitness(..)
, LinearManifoldWitness(..) )
#if MIN_VERSION_linearmap_category(0,6,0)
import Math.VectorSpace.DimensionAware
( DimensionAware(..), Dimensional(..), DimensionalityWitness(..)
, dimensionality, DimensionalityCases(..)
, dimensionalitySing )
import GHC.TypeLits
#if MIN_VERSION_singletons(3,0,0)
import Prelude.Singletons (SNum(..))
import GHC.TypeLits.Singletons (withKnownNat, SNat(..))
#else
import Data.Singletons.Prelude.Num (SNum(..), SNat(..))
import Data.Singletons.TypeLits (withKnownNat)
#endif
#endif
import Math.VectorSpace.Dual
import Math.VectorSpace.MiscUtil.MultiConstraints (SameScalar)
import Data.Monoid.Additive
import Data.Void
import Linear (V0, V1, V2, V3, V4)
import qualified Linear.Affine as LinAff
import Control.Applicative
import Control.Arrow
import qualified GHC.Generics as Gnrx
import GHC.Generics (Generic, (:*:)(..))
import Data.Kind (Type)
import Proof.Propositional (Empty(..))
import Data.CallStack (HasCallStack)
interiorSemimanifoldWitness :: ∀ a . SemimanifoldWithBoundary a
=> SemimanifoldWitness (Interior a)
interiorSemimanifoldWitness :: forall a.
SemimanifoldWithBoundary a =>
SemimanifoldWitness (Interior a)
interiorSemimanifoldWitness = case forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @a of
SmfdWBoundWitness a
OpenManifoldWitness -> forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness
SmfdWBoundWitness a
SmfdWBoundWitness -> forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness
#define VectorSpaceSansBoundary(v, s) \
instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
=> SemimanifoldWithBoundary (v) where { \
type Interior (v) = v; \
type Boundary (v) = EmptyMfd (ZeroDim s); \
type HalfNeedle (v) = ℝay; \
smfdWBoundWitness = OpenManifoldWitness; \
fromInterior = id; \
fromBoundary b = case b of {}; \
separateInterior = Right; \
p|+^_ = case p of {}; \
a.+^|b = Right $ a^+^b; \
extendToBoundary _ _ = Nothing }; \
instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
=> PseudoAffineWithBoundary (v) where {\
_!-|p = case p of {}; \
(.--!) = (-) }; \
instance (Num' (s), Eq (s), OpenManifold (s), ProjectableBoundary (s)) \
=> ProjectableBoundary (v) where { \
projectToBoundary _ p = case p of {}; \
marginFromBoundary p = case p of {} }
VectorSpaceSansBoundary(ℝ,ℝ)
VectorSpaceSansBoundary(V0 s, s)
VectorSpaceSansBoundary(V1 s, s)
VectorSpaceSansBoundary(V2 s, s)
VectorSpaceSansBoundary(V3 s, s)
VectorSpaceSansBoundary(V4 s, s)
data ProductBoundary a b
= BoundOfL !(Boundary a) !(Interior b)
| BoundOfR !(Interior a) !(Boundary b)
data ProductBoundaryNeedleT (dn :: Dualness) a b v
= ZeroProductBoundaryNeedle
| NBoundOfL !(dn`Space`Needle (Boundary a)) !(dn`Space`Needle (Interior b)) !v
| NBoundOfR !(dn`Space`Needle (Interior a)) !(dn`Space`Needle (Boundary b)) !v
type ProductBoundaryNeedle a b = ProductBoundaryNeedleT Vector a b
(Scalar (Needle (Interior a)))
instance ( AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Interior b))
, AdditiveGroup (dn`Space`Needle (Interior a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, AdditiveGroup v
, ValidDualness dn )
=> AffineSpace (ProductBoundaryNeedleT dn a b v) where
type Diff (ProductBoundaryNeedleT dn a b v) = ProductBoundaryNeedleT dn a b v
ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle .+^ :: ProductBoundaryNeedleT dn a b v
-> Diff (ProductBoundaryNeedleT dn a b v)
-> ProductBoundaryNeedleT dn a b v
.+^ Diff (ProductBoundaryNeedleT dn a b v)
n = Diff (ProductBoundaryNeedleT dn a b v)
n
ProductBoundaryNeedleT dn a b v
n .+^ Diff (ProductBoundaryNeedleT dn a b v)
ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle = ProductBoundaryNeedleT dn a b v
n
NBoundOfL Space dn (Needle (Boundary a))
x Space dn (Needle (Interior b))
y v
v .+^ NBoundOfL Space dn (Needle (Boundary a))
ξ Space dn (Needle (Interior b))
υ v
β = forall (dn :: Dualness) a b v.
Space dn (Needle (Boundary a))
-> Space dn (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfL (Space dn (Needle (Boundary a))
xforall v. AdditiveGroup v => v -> v -> v
^+^Space dn (Needle (Boundary a))
ξ) (Space dn (Needle (Interior b))
yforall v. AdditiveGroup v => v -> v -> v
^+^Space dn (Needle (Interior b))
υ) (v
vforall v. AdditiveGroup v => v -> v -> v
^+^v
β)
NBoundOfR Space dn (Needle (Interior a))
x Space dn (Needle (Boundary b))
y v
v .+^ NBoundOfR Space dn (Needle (Interior a))
ξ Space dn (Needle (Boundary b))
υ v
β = forall (dn :: Dualness) a b v.
Space dn (Needle (Interior a))
-> Space dn (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfR (Space dn (Needle (Interior a))
xforall v. AdditiveGroup v => v -> v -> v
^+^Space dn (Needle (Interior a))
ξ) (Space dn (Needle (Boundary b))
yforall v. AdditiveGroup v => v -> v -> v
^+^Space dn (Needle (Boundary b))
υ) (v
vforall v. AdditiveGroup v => v -> v -> v
^+^v
β)
ProductBoundaryNeedleT dn a b v
n .-. :: ProductBoundaryNeedleT dn a b v
-> ProductBoundaryNeedleT dn a b v
-> Diff (ProductBoundaryNeedleT dn a b v)
.-. ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle = ProductBoundaryNeedleT dn a b v
n
NBoundOfL Space dn (Needle (Boundary a))
x Space dn (Needle (Interior b))
y v
v .-. NBoundOfL Space dn (Needle (Boundary a))
ξ Space dn (Needle (Interior b))
υ v
β = forall (dn :: Dualness) a b v.
Space dn (Needle (Boundary a))
-> Space dn (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfL (Space dn (Needle (Boundary a))
xforall v. AdditiveGroup v => v -> v -> v
^-^Space dn (Needle (Boundary a))
ξ) (Space dn (Needle (Interior b))
yforall v. AdditiveGroup v => v -> v -> v
^-^Space dn (Needle (Interior b))
υ) (v
vforall v. AdditiveGroup v => v -> v -> v
^-^v
β)
NBoundOfR Space dn (Needle (Interior a))
x Space dn (Needle (Boundary b))
y v
v .-. NBoundOfR Space dn (Needle (Interior a))
ξ Space dn (Needle (Boundary b))
υ v
β = forall (dn :: Dualness) a b v.
Space dn (Needle (Interior a))
-> Space dn (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfR (Space dn (Needle (Interior a))
xforall v. AdditiveGroup v => v -> v -> v
^-^Space dn (Needle (Interior a))
ξ) (Space dn (Needle (Boundary b))
yforall v. AdditiveGroup v => v -> v -> v
^-^Space dn (Needle (Boundary b))
υ) (v
vforall v. AdditiveGroup v => v -> v -> v
^-^v
β)
instance ( AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Interior b))
, AdditiveGroup (dn`Space`Needle (Interior a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, AdditiveGroup v
, ValidDualness dn )
=> AdditiveGroup (ProductBoundaryNeedleT dn a b v) where
zeroV :: ProductBoundaryNeedleT dn a b v
zeroV = forall (dn :: Dualness) a b v. ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle
^+^ :: ProductBoundaryNeedleT dn a b v
-> ProductBoundaryNeedleT dn a b v
-> ProductBoundaryNeedleT dn a b v
(^+^) = forall p. AffineSpace p => p -> Diff p -> p
(.+^)
negateV :: ProductBoundaryNeedleT dn a b v -> ProductBoundaryNeedleT dn a b v
negateV ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle = forall (dn :: Dualness) a b v. ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle
negateV (NBoundOfL Space dn (Needle (Boundary a))
x Space dn (Needle (Interior b))
y v
v) = forall (dn :: Dualness) a b v.
Space dn (Needle (Boundary a))
-> Space dn (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfL (forall v. AdditiveGroup v => v -> v
negateV Space dn (Needle (Boundary a))
x) (forall v. AdditiveGroup v => v -> v
negateV Space dn (Needle (Interior b))
y) (forall v. AdditiveGroup v => v -> v
negateV v
v)
negateV (NBoundOfR Space dn (Needle (Interior a))
x Space dn (Needle (Boundary b))
y v
v) = forall (dn :: Dualness) a b v.
Space dn (Needle (Interior a))
-> Space dn (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfR (forall v. AdditiveGroup v => v -> v
negateV Space dn (Needle (Interior a))
x) (forall v. AdditiveGroup v => v -> v
negateV Space dn (Needle (Boundary b))
y) (forall v. AdditiveGroup v => v -> v
negateV v
v)
instance ∀ a b v dn .
( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
, SameScalar VectorSpace
'[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
, AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, ValidDualness dn )
=> VectorSpace (ProductBoundaryNeedleT dn a b v) where
type Scalar (ProductBoundaryNeedleT dn a b v) = Scalar v
*^ :: Scalar (ProductBoundaryNeedleT dn a b v)
-> ProductBoundaryNeedleT dn a b v
-> ProductBoundaryNeedleT dn a b v
(*^) = forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @a (forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @b (
case (forall (dn :: Dualness). ValidDualness dn => DualnessSingletons dn
decideDualness @dn, forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @a, forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @b) of
(DualnessSingletons dn
VectorWitness, SmfdWBoundWitness a
_, SmfdWBoundWitness b
_) -> \Scalar (Space 'Vector (Needle (Boundary a)))
μ -> \case
ProductBoundaryNeedleT 'Vector a b v
ZeroProductBoundaryNeedle -> forall (dn :: Dualness) a b v. ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle
NBoundOfL Space 'Vector (Needle (Boundary a))
x Space 'Vector (Needle (Interior b))
y v
v -> forall (dn :: Dualness) a b v.
Space dn (Needle (Boundary a))
-> Space dn (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfL (Scalar (Space 'Vector (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Vector (Needle (Boundary a))
x) (Scalar (Space 'Vector (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Vector (Needle (Interior b))
y) (Scalar (Space 'Vector (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^v
v)
NBoundOfR Space 'Vector (Needle (Interior a))
x Space 'Vector (Needle (Boundary b))
y v
v -> forall (dn :: Dualness) a b v.
Space dn (Needle (Interior a))
-> Space dn (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfR (Scalar (Space 'Vector (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Vector (Needle (Interior a))
x) (Scalar (Space 'Vector (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Vector (Needle (Boundary b))
y) (Scalar (Space 'Vector (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^v
v)
(DualnessSingletons dn
FunctionalWitness, SmfdWBoundWitness a
SmfdWBoundWitness, SmfdWBoundWitness b
SmfdWBoundWitness)
-> case ( forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(Needle (Interior a))
, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(Needle (Boundary a))
, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(Needle (Interior b))
, forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(Needle (Boundary b)) ) of
(DualSpaceWitness (Needle (Interior a))
DualSpaceWitness, DualSpaceWitness (Needle (Boundary a))
DualSpaceWitness, DualSpaceWitness (Needle (Interior b))
DualSpaceWitness, DualSpaceWitness (Needle (Boundary b))
DualSpaceWitness)
-> \Scalar (Space 'Functional (Needle (Boundary a)))
μ -> \case
ProductBoundaryNeedleT 'Functional a b v
ZeroProductBoundaryNeedle -> forall (dn :: Dualness) a b v. ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle
NBoundOfL Space 'Functional (Needle (Boundary a))
x Space 'Functional (Needle (Interior b))
y v
v -> forall (dn :: Dualness) a b v.
Space dn (Needle (Boundary a))
-> Space dn (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfL (Scalar (Space 'Functional (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Functional (Needle (Boundary a))
x) (Scalar (Space 'Functional (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Functional (Needle (Interior b))
y) (Scalar (Space 'Functional (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^v
v)
NBoundOfR Space 'Functional (Needle (Interior a))
x Space 'Functional (Needle (Boundary b))
y v
v -> forall (dn :: Dualness) a b v.
Space dn (Needle (Interior a))
-> Space dn (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfR (Scalar (Space 'Functional (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Functional (Needle (Interior a))
x) (Scalar (Space 'Functional (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Functional (Needle (Boundary b))
y) (Scalar (Space 'Functional (Needle (Boundary a)))
μforall v. VectorSpace v => Scalar v -> v -> v
*^v
v)
))
#if MIN_VERSION_linearmap_category(0,6,0)
type family ProductBoundaryNeedleTDimension dna dnb dv where
ProductBoundaryNeedleTDimension
('Just n) ('Just m) ('Just o) = 'Just (n*m*o - 1)
ProductBoundaryNeedleTDimension _ _ _ = 'Nothing
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
, SameScalar LinearSpace
'[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
, AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, ValidDualness dn )
=> DimensionAware (ProductBoundaryNeedleT dn a b v) where
type StaticDimension (ProductBoundaryNeedleT dn a b v)
= ProductBoundaryNeedleTDimension (StaticDimension (dn`Space`Needle (Interior a)))
(StaticDimension (dn`Space`Needle (Interior b)))
(StaticDimension v)
dimensionalityWitness :: DimensionalityWitness (ProductBoundaryNeedleT dn a b v)
dimensionalityWitness = case ( forall a.
SemimanifoldWithBoundary a =>
SemimanifoldWitness (Interior a)
interiorSemimanifoldWitness @a
, forall a.
SemimanifoldWithBoundary a =>
SemimanifoldWitness (Interior a)
interiorSemimanifoldWitness @b ) of
(SemimanifoldWitness (Interior a)
SemimanifoldWitness, SemimanifoldWitness (Interior b)
SemimanifoldWitness)
-> case ( forall v. DimensionAware v => DimensionalityCases v
dimensionality @(dn`Space`Needle (Interior a))
, forall v. DimensionAware v => DimensionalityCases v
dimensionality @(dn`Space`Needle (Interior b))
, forall v. DimensionAware v => DimensionalityCases v
dimensionality @v ) of
(DimensionalityCases (Space dn (Needle (Interior a)))
StaticDimensionalCase, DimensionalityCases (Space dn (Needle (Interior b)))
StaticDimensionalCase, DimensionalityCases v
StaticDimensionalCase)
-> forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat (forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @(dn`Space`Needle (Interior a))
forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
%* forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @(dn`Space`Needle (Interior b))
forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)
%* forall v (n :: Nat). Dimensional n v => Sing n
dimensionalitySing @v
forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2)
%- forall (n :: Nat). KnownNat n => SNat n
SNat @1
)
forall (n :: Nat) v. Dimensional n v => DimensionalityWitness v
IsStaticDimensional
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
, SameScalar LinearSpace
'[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
, AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, n`Dimensional`(dn`Space`Needle (Interior a))
, m`Dimensional`(dn`Space`Needle (Interior b))
, o`Dimensional`v
, KnownNat d, d ~ (n*m*o-1)
, ValidDualness dn )
=> d`Dimensional`(ProductBoundaryNeedleT dn a b v) where
#endif
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
, SameScalar LinearSpace
'[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
, AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, ValidDualness dn )
=> TensorSpace (ProductBoundaryNeedleT dn a b v) where
type TensorProduct (ProductBoundaryNeedleT dn a b v) w
= ProductBoundaryNeedleT dn a b (v⊗w)
wellDefinedVector :: ProductBoundaryNeedleT dn a b v
-> Maybe (ProductBoundaryNeedleT dn a b v)
wellDefinedVector ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle = forall a. a -> Maybe a
Just forall (dn :: Dualness) a b v. ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle
wellDefinedTensor :: forall w.
(TensorSpace w,
Scalar w ~ Scalar (ProductBoundaryNeedleT dn a b v)) =>
(ProductBoundaryNeedleT dn a b v ⊗ w)
-> Maybe (ProductBoundaryNeedleT dn a b v ⊗ w)
wellDefinedTensor t :: ProductBoundaryNeedleT dn a b v ⊗ w
t@(Tensor TensorProduct (ProductBoundaryNeedleT dn a b v) w
ProductBoundaryNeedleT dn a b (Tensor (Scalar v) v w)
ZeroProductBoundaryNeedle) = forall a. a -> Maybe a
Just ProductBoundaryNeedleT dn a b v ⊗ w
t
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
, SameScalar LinearSpace
'[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
, AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, ValidDualness dn
)
=> LinearSpace (ProductBoundaryNeedleT dn a b v) where
type DualVector (ProductBoundaryNeedleT dn a b v)
= ProductBoundaryNeedleT (Dual dn) a b (DualVector v)
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
, SameScalar LinearSpace
'[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
, AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, ValidDualness dn
)
=> Semimanifold (ProductBoundaryNeedleT dn a b v) where
type Needle (ProductBoundaryNeedleT dn a b v) = ProductBoundaryNeedleT dn a b v
.+~^ :: ProductBoundaryNeedleT dn a b v
-> Needle (ProductBoundaryNeedleT dn a b v)
-> ProductBoundaryNeedleT dn a b v
(.+~^) = forall v. AdditiveGroup v => v -> v -> v
(^+^)
semimanifoldWitness :: SemimanifoldWitness (ProductBoundaryNeedleT dn a b v)
semimanifoldWitness = forall x.
(Semimanifold (Needle x), Needle (Needle x) ~ Needle x) =>
SemimanifoldWitness x
SemimanifoldWitness
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
, SameScalar LinearSpace
'[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
, AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, ValidDualness dn
)
=> PseudoAffine (ProductBoundaryNeedleT dn a b v) where
ProductBoundaryNeedleT dn a b v
p.-~. :: ProductBoundaryNeedleT dn a b v
-> ProductBoundaryNeedleT dn a b v
-> Maybe (Needle (ProductBoundaryNeedleT dn a b v))
.-~.ProductBoundaryNeedleT dn a b v
q = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (ProductBoundaryNeedleT dn a b v
pforall v. AdditiveGroup v => v -> v -> v
^-^ProductBoundaryNeedleT dn a b v
q)
.-~! :: HasCallStack =>
ProductBoundaryNeedleT dn a b v
-> ProductBoundaryNeedleT dn a b v
-> Needle (ProductBoundaryNeedleT dn a b v)
(.-~!) = forall v. AdditiveGroup v => v -> v -> v
(^-^)
instance ( SemimanifoldWithBoundary a, SemimanifoldWithBoundary b
, SameScalar LinearSpace
'[ v, dn`Space`Needle (Interior a), dn`Space`Needle (Interior b) ]
, AdditiveGroup (dn`Space`Needle (Boundary a))
, AdditiveGroup (dn`Space`Needle (Boundary b))
, OpenManifold (Scalar v)
, ValidDualness dn
)
=> SemimanifoldWithBoundary (ProductBoundaryNeedleT dn a b v) where
type Interior (ProductBoundaryNeedleT dn a b v) = ProductBoundaryNeedleT dn a b v
type Boundary (ProductBoundaryNeedleT dn a b v) = EmptyMfd v
type HalfNeedle (ProductBoundaryNeedleT dn a b v) = ℝay
smfdWBoundWitness :: SmfdWBoundWitness (ProductBoundaryNeedleT dn a b v)
smfdWBoundWitness = forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
instance ∀ a b . ( ProjectableBoundary a, ProjectableBoundary b
, SameScalar LinearSpace
'[ Needle (Interior a), Needle (Interior b) ]
, Num' (Scalar (Needle (Interior a)))
)
=> Semimanifold (ProductBoundary a b) where
type Needle (ProductBoundary a b) = ProductBoundaryNeedle a b
.+~^ :: ProductBoundary a b
-> Needle (ProductBoundary a b) -> ProductBoundary a b
(.+~^) = forall a. HasCallStack => a
undefined
semimanifoldWitness :: SemimanifoldWitness (ProductBoundary a b)
semimanifoldWitness = case ( forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior a)
, forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior b) ) of
(SemimanifoldWitness (Interior a)
SemimanifoldWitness, SemimanifoldWitness (Interior b)
SemimanifoldWitness)
-> forall a. HasCallStack => a
undefined
instance ∀ a b . ( ProjectableBoundary a, ProjectableBoundary b
, SameScalar LinearSpace
'[ Needle (Interior a), Needle (Interior b) ]
, Num' (Scalar (Needle (Interior a)))
)
=> PseudoAffine (ProductBoundary a b) where
ProductBoundary a b
p.-~! :: HasCallStack =>
ProductBoundary a b
-> ProductBoundary a b -> Needle (ProductBoundary a b)
.-~!ProductBoundary a b
q = case ProductBoundary a b
pforall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~.ProductBoundary a b
q of
Just Needle (ProductBoundary a b)
v -> Needle (ProductBoundary a b)
v
Maybe (Needle (ProductBoundary a b))
Nothing -> forall a. HasCallStack => [Char] -> a
error [Char]
"No path found in product-space boundary."
.-~. :: ProductBoundary a b
-> ProductBoundary a b -> Maybe (Needle (ProductBoundary a b))
(.-~.) = case ( forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness @(Interior a)
, forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness @(Interior b) ) of
(PseudoAffineWitness SemimanifoldWitness (Interior a)
SemimanifoldWitness, PseudoAffineWitness SemimanifoldWitness (Interior b)
SemimanifoldWitness)
-> let BoundOfL Boundary a
bx Interior b
y − :: ProductBoundary a b
-> ProductBoundary a b
-> Maybe
(ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a))))
− BoundOfL Boundary a
bξ Interior b
υ
= case (Boundary a
bxforall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~.Boundary a
bξ, forall m. SemimanifoldWithBoundary m => Interior m -> m
fromInterior @b Interior b
yforall m.
PseudoAffineWithBoundary m =>
m -> m -> Maybe (Needle (Interior m))
.--.forall m. SemimanifoldWithBoundary m => Interior m -> m
fromInterior Interior b
υ) of
(Just Needle (Boundary a)
δbx, Just Needle (Interior b)
δy) -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (dn :: Dualness) a b v.
Space dn (Needle (Boundary a))
-> Space dn (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfL Needle (Boundary a)
δbx Needle (Interior b)
δy Scalar (Needle (Interior a))
1
(Maybe (Needle (Boundary a))
_, Maybe (Needle (Interior b))
Nothing) -> forall a. Maybe a
Nothing
BoundOfL Boundary a
bx Interior b
y − BoundOfR Interior a
ξ Boundary b
bυ
= case ( forall m. SemimanifoldWithBoundary m => Boundary m -> m
fromBoundary @a Boundary a
bxforall m.
PseudoAffineWithBoundary m =>
m -> m -> Maybe (Needle (Interior m))
.--.forall m. SemimanifoldWithBoundary m => Interior m -> m
fromInterior Interior a
ξ
, forall m.
ProjectableBoundary m =>
m
-> Boundary m
-> Maybe (Needle (Boundary m), Scalar (Needle (Interior m)))
projectToBoundary (forall m. SemimanifoldWithBoundary m => Interior m -> m
fromInterior @b Interior b
y) Boundary b
bυ ) of
(Just Needle (Interior a)
δbx, Just (Needle (Boundary b)
δby, Scalar (Needle (Interior a))
dy))
-> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (dn :: Dualness) a b v.
Space dn (Needle (Interior a))
-> Space dn (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfR (Needle (Interior a)
δbxforall v s. (VectorSpace v, s ~ Scalar v) => v -> s -> v
^*(Scalar (Needle (Interior a))
1forall a. Num a => a -> a -> a
+Scalar (Needle (Interior a))
dy)) Needle (Boundary b)
δby Scalar (Needle (Interior a))
1
(Maybe (Needle (Interior a)),
Maybe (Needle (Boundary b), Scalar (Needle (Interior a))))
_ -> forall a. Maybe a
Nothing
in ProductBoundary a b
-> ProductBoundary a b
-> Maybe
(ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a))))
(−)
pseudoAffineWitness :: PseudoAffineWitness (ProductBoundary a b)
pseudoAffineWitness = case ( forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness @(Interior a)
, forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness @(Interior b) ) of
(PseudoAffineWitness SemimanifoldWitness (Interior a)
SemimanifoldWitness
, PseudoAffineWitness SemimanifoldWitness (Interior b)
SemimanifoldWitness)
-> forall a. HasCallStack => a
undefined
instance ∀ a b . ( ProjectableBoundary a, ProjectableBoundary b
, SameScalar LinearSpace
'[ Needle (Interior a), Needle (Interior b)
, FullSubspace (HalfNeedle a)
]
, RealFrac'' (Scalar (Needle (Interior a)))
)
=> SemimanifoldWithBoundary (ProductBoundary a b) where
type Interior (ProductBoundary a b) = ProductBoundary a b
type Boundary (ProductBoundary a b) = EmptyMfd (Needle (Boundary a), Needle (Boundary b))
type HalfNeedle (ProductBoundary a b) = (HalfNeedle a, Needle (Boundary b))
Boundary (ProductBoundary a b)
q|+^ :: Boundary (ProductBoundary a b)
-> HalfNeedle (ProductBoundary a b) -> ProductBoundary a b
|+^HalfNeedle (ProductBoundary a b)
_ = case Boundary (ProductBoundary a b)
q of {}
ProductBoundary a b
p.+^| :: ProductBoundary a b
-> Needle (Interior (ProductBoundary a b))
-> Either
(Boundary (ProductBoundary a b),
Scalar (Needle (Interior (ProductBoundary a b))))
(Interior (ProductBoundary a b))
.+^|Needle (Interior (ProductBoundary a b))
q = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ ProductBoundary a b
pforall x. Semimanifold x => x -> Needle x -> x
.+~^Needle (Interior (ProductBoundary a b))
q
fromInterior :: Interior (ProductBoundary a b) -> ProductBoundary a b
fromInterior = forall a. a -> a
id
fromBoundary :: Boundary (ProductBoundary a b) -> ProductBoundary a b
fromBoundary Boundary (ProductBoundary a b)
q = case Boundary (ProductBoundary a b)
q of {}
smfdWBoundWitness :: SmfdWBoundWitness (ProductBoundary a b)
smfdWBoundWitness = forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @a
(case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar (Needle (Interior a))) of
ClosedScalarWitness (Scalar (Needle (Interior a)))
ClosedScalarWitness -> forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness)
needleIsOpenMfd :: forall r.
(OpenManifold (Needle (Interior (ProductBoundary a b))) => r) -> r
needleIsOpenMfd OpenManifold (Needle (Interior (ProductBoundary a b))) => r
r = forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @a (forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @b
(case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar (Needle (Interior a))) of
ClosedScalarWitness (Scalar (Needle (Interior a)))
ClosedScalarWitness -> OpenManifold (Needle (Interior (ProductBoundary a b))) => r
r))
extendToBoundary :: Interior (ProductBoundary a b)
-> Needle (Interior (ProductBoundary a b))
-> Maybe (Boundary (ProductBoundary a b))
extendToBoundary Interior (ProductBoundary a b)
q = case Interior (ProductBoundary a b)
q of {}
scalarIsOpenMfd :: forall r.
(OpenManifold (Scalar (Needle (Interior (ProductBoundary a b)))) =>
r)
-> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (ProductBoundary a b)))) =>
r
r = forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @a
(case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar (Needle (Interior a))) of
ClosedScalarWitness (Scalar (Needle (Interior a)))
ClosedScalarWitness -> OpenManifold (Scalar (Needle (Interior (ProductBoundary a b)))) =>
r
r)
boundaryHasSameScalar :: forall r.
((LinearSpace (Needle (Boundary (ProductBoundary a b))),
Scalar (Needle (Boundary (ProductBoundary a b)))
~ Scalar (Needle (Interior (ProductBoundary a b)))) =>
r)
-> r
boundaryHasSameScalar (LinearSpace (Needle (Boundary (ProductBoundary a b))),
Scalar (Needle (Boundary (ProductBoundary a b)))
~ Scalar (Needle (Interior (ProductBoundary a b)))) =>
r
r = forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @a (forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @b
(case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar (Needle (Interior a))) of
ClosedScalarWitness (Scalar (Needle (Interior a)))
ClosedScalarWitness -> (LinearSpace (Needle (Boundary (ProductBoundary a b))),
Scalar (Needle (Boundary (ProductBoundary a b)))
~ Scalar (Needle (Interior (ProductBoundary a b)))) =>
r
r))
instance (Empty (Boundary a), Empty (Boundary b)) => Empty (ProductBoundary a b) where
eliminate :: forall x. ProductBoundary a b -> x
eliminate (BoundOfL Boundary a
ba Interior b
_) = forall a x. Empty a => a -> x
eliminate Boundary a
ba
eliminate (BoundOfR Interior a
_ Boundary b
bb) = forall a x. Empty a => a -> x
eliminate Boundary b
bb
data ProductHalfNeedle a b
= ProductHalfNeedle !(Needle (Interior a)) !(Needle (Interior b))
instance (AdditiveGroup (Needle (Interior a)), AdditiveGroup (Needle (Interior b)))
=> AdditiveMonoid (ProductHalfNeedle a b) where
zeroHV :: ProductHalfNeedle a b
zeroHV = forall a b.
Needle (Interior a) -> Needle (Interior b) -> ProductHalfNeedle a b
ProductHalfNeedle forall v. AdditiveGroup v => v
zeroV forall v. AdditiveGroup v => v
zeroV
addHVs :: ProductHalfNeedle a b
-> ProductHalfNeedle a b -> ProductHalfNeedle a b
addHVs (ProductHalfNeedle Needle (Interior a)
v Needle (Interior b)
w) (ProductHalfNeedle Needle (Interior a)
ϋ Needle (Interior b)
ĥ)
= forall a b.
Needle (Interior a) -> Needle (Interior b) -> ProductHalfNeedle a b
ProductHalfNeedle (Needle (Interior a)
vforall v. AdditiveGroup v => v -> v -> v
^+^Needle (Interior a)
ϋ) (Needle (Interior b)
wforall v. AdditiveGroup v => v -> v -> v
^+^Needle (Interior b)
ĥ)
instance ( SemimanifoldWithBoundary a
, SameScalar VectorSpace
'[ Needle (Interior a), Needle (Interior b) ]
, RealFrac'' (Scalar (Needle (Interior a)))
) => HalfSpace (ProductHalfNeedle a b) where
type FullSubspace (ProductHalfNeedle a b) = ProductBoundaryNeedle a b
type Ray (ProductHalfNeedle a b) = ℝay_ (Scalar (Needle (Interior a)))
type MirrorJoin (ProductHalfNeedle a b) = (Needle (Interior a), Needle (Interior b))
scaleNonNeg :: Ray (ProductHalfNeedle a b)
-> ProductHalfNeedle a b -> ProductHalfNeedle a b
scaleNonNeg = case forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @a of
SmfdWBoundWitness a
SmfdWBoundWitness
-> forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @a (\(Cℝay Scalar (Needle (ZeroDim (Scalar (Needle (Interior a)))))
μ ZeroDim (Scalar (Needle (Interior a)))
Origin) (ProductHalfNeedle Needle (Interior a)
v Needle (Interior b)
w)
-> forall a b.
Needle (Interior a) -> Needle (Interior b) -> ProductHalfNeedle a b
ProductHalfNeedle (Scalar (Needle (ZeroDim (Scalar (Needle (Interior a)))))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Needle (Interior a)
v) (Scalar (Needle (ZeroDim (Scalar (Needle (Interior a)))))
μforall v. VectorSpace v => Scalar v -> v -> v
*^Needle (Interior b)
w))
fromFullSubspace :: FullSubspace (ProductHalfNeedle a b) -> ProductHalfNeedle a b
fromFullSubspace FullSubspace (ProductHalfNeedle a b)
ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a)))
ZeroProductBoundaryNeedle = forall h. AdditiveMonoid h => h
zeroHV
fullSubspaceIsVectorSpace :: forall r.
((VectorSpace (FullSubspace (ProductHalfNeedle a b)),
ScalarSpace (Scalar (FullSubspace (ProductHalfNeedle a b))),
Scalar (FullSubspace (ProductHalfNeedle a b))
~ MirrorJoin (Ray (ProductHalfNeedle a b))) =>
r)
-> r
fullSubspaceIsVectorSpace (VectorSpace (FullSubspace (ProductHalfNeedle a b)),
ScalarSpace (Scalar (FullSubspace (ProductHalfNeedle a b))),
Scalar (FullSubspace (ProductHalfNeedle a b))
~ MirrorJoin (Ray (ProductHalfNeedle a b))) =>
r
q = forall a. HasCallStack => a
undefined
projectToFullSubspace :: ProductHalfNeedle a b -> FullSubspace (ProductHalfNeedle a b)
projectToFullSubspace = forall a. HasCallStack => a
undefined
rayIsHalfSpace :: forall r. (HalfSpace (Ray (ProductHalfNeedle a b)) => r) -> r
rayIsHalfSpace HalfSpace (Ray (ProductHalfNeedle a b)) => r
_ = forall a. HasCallStack => a
undefined
fromPositiveHalf :: ProductHalfNeedle a b -> MirrorJoin (ProductHalfNeedle a b)
fromPositiveHalf = forall a. HasCallStack => a
undefined
fromNegativeHalf :: ProductHalfNeedle a b -> MirrorJoin (ProductHalfNeedle a b)
fromNegativeHalf = forall a. HasCallStack => a
undefined
instance ∀ a b .
( ProjectableBoundary a, ProjectableBoundary b
, SameScalar LinearSpace
'[ Needle (Interior a), Needle (Interior b)
]
, RealFrac'' (Scalar (Needle (Interior a)))
, ProjectableBoundary (Interior a), ProjectableBoundary (Interior b)
) => SemimanifoldWithBoundary (a,b) where
type Interior (a,b) = (Interior a, Interior b)
type Boundary (a,b) = ProductBoundary a b
type HalfNeedle (a,b) = ProductHalfNeedle a b
extendToBoundary :: Interior (a, b)
-> Needle (Interior (a, b)) -> Maybe (Boundary (a, b))
extendToBoundary = forall a. HasCallStack => a
undefined
smfdWBoundWitness :: SmfdWBoundWitness (a, b)
smfdWBoundWitness = case (forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @a, forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @b) of
(SmfdWBoundWitness a
OpenManifoldWitness, SmfdWBoundWitness b
OpenManifoldWitness)
-> forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @a (forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @b (
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @(Needle a) (forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @(Needle b)
(case (forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior a), forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior b))
of (SemimanifoldWitness a
SemimanifoldWitness, SemimanifoldWitness b
SemimanifoldWitness)
-> forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @a
(forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @b forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness) )
)))
(SmfdWBoundWitness a
SmfdWBoundWitness, SmfdWBoundWitness b
SmfdWBoundWitness)
-> forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @a
(forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @b
(forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @(Interior a)
(forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @(Interior b)
(case ( forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior a)
, forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior b)
, forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar (Needle (Interior a)))
)
of (SemimanifoldWitness (Interior a)
SemimanifoldWitness, SemimanifoldWitness (Interior b)
SemimanifoldWitness, ClosedScalarWitness (Scalar (Needle (Interior a)))
ClosedScalarWitness)
-> forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @a
(forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @b
(forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @(Needle (Interior a))
(forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @(Needle (Interior b))
forall m.
(OpenManifold (Interior m), OpenManifold (Boundary m),
FullSubspace (HalfNeedle m) ~ Needle (Boundary m)) =>
SmfdWBoundWitness m
SmfdWBoundWitness)))))))
boundaryHasSameScalar :: forall r.
((LinearSpace (Needle (Boundary (a, b))),
Scalar (Needle (Boundary (a, b)))
~ Scalar (Needle (Interior (a, b)))) =>
r)
-> r
boundaryHasSameScalar (LinearSpace (Needle (Boundary (a, b))),
Scalar (Needle (Boundary (a, b)))
~ Scalar (Needle (Interior (a, b)))) =>
r
q = forall a. HasCallStack => a
undefined
needleIsOpenMfd :: forall r. (OpenManifold (Needle (Interior (a, b))) => r) -> r
needleIsOpenMfd OpenManifold (Needle (Interior (a, b))) => r
_ = forall a. HasCallStack => a
undefined
instance ∀ a b .
( ProjectableBoundary a, ProjectableBoundary b
, SameScalar LinearSpace
'[ Needle (Interior a), Needle (Interior b)
, Needle (Boundary a), Needle (Boundary b)
]
, ProjectableBoundary (Interior a), ProjectableBoundary (Interior b)
, RealFrac'' (Scalar (Needle (Interior a)))
) => PseudoAffineWithBoundary (a,b) where
instance ∀ a b .
( ProjectableBoundary a, ProjectableBoundary b
, SameScalar LinearSpace
'[ Needle (Interior a), Needle (Interior b)
, Needle (Boundary a), Needle (Boundary b)
]
, ProjectableBoundary (Interior a), ProjectableBoundary (Interior b)
, RealFrac'' (Scalar (Needle (Interior a)))
) => ProjectableBoundary (a,b) where
needleBoundaryIsTriviallyProjectible :: forall r.
(ProjectableBoundary (Needle (Interior (a, b))) => r) -> r
needleBoundaryIsTriviallyProjectible ProjectableBoundary (Needle (Interior (a, b))) => r
q
= forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @a
(forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @b
(forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @(Needle (Interior a))
(forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r)
-> r
boundaryHasSameScalar @(Needle (Interior b))
(forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @a
(forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @b
(case (forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior a), forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior b))
of (SemimanifoldWitness (Interior a)
SemimanifoldWitness, SemimanifoldWitness (Interior b)
SemimanifoldWitness) -> ProjectableBoundary (Needle (Interior (a, b))) => r
q))))))
instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (S⁰_ s) where
type Interior (S⁰_ s) = S⁰_ s
type Boundary (S⁰_ s) = EmptyMfd (ZeroDim s)
type HalfNeedle (S⁰_ s) = ZeroDim s
fromInterior :: Interior (S⁰_ s) -> S⁰_ s
fromInterior = forall a. a -> a
id
fromBoundary :: Boundary (S⁰_ s) -> S⁰_ s
fromBoundary Boundary (S⁰_ s)
b = case Boundary (S⁰_ s)
b of {}
separateInterior :: S⁰_ s -> Either (Boundary (S⁰_ s)) (Interior (S⁰_ s))
separateInterior = forall a b. b -> Either a b
Right
Boundary (S⁰_ s)
p|+^ :: Boundary (S⁰_ s) -> HalfNeedle (S⁰_ s) -> S⁰_ s
|+^HalfNeedle (S⁰_ s)
_ = case Boundary (S⁰_ s)
p of {}
S⁰_ s
NegativeHalfSphere .+^| :: S⁰_ s
-> Needle (Interior (S⁰_ s))
-> Either
(Boundary (S⁰_ s), Scalar (Needle (Interior (S⁰_ s))))
(Interior (S⁰_ s))
.+^| ZeroDim s
Needle (Interior (S⁰_ s))
Origin = forall a b. b -> Either a b
Right forall r. S⁰_ r
NegativeHalfSphere
S⁰_ s
PositiveHalfSphere .+^| ZeroDim s
Needle (Interior (S⁰_ s))
Origin = forall a b. b -> Either a b
Right forall r. S⁰_ r
PositiveHalfSphere
extendToBoundary :: Interior (S⁰_ s)
-> Needle (Interior (S⁰_ s)) -> Maybe (Boundary (S⁰_ s))
extendToBoundary Interior (S⁰_ s)
_ Needle (Interior (S⁰_ s))
_ = forall a. Maybe a
Nothing
smfdWBoundWitness :: SmfdWBoundWitness (S⁰_ s)
smfdWBoundWitness = forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (S¹_ s) where
type Interior (S¹_ s) = (S¹_ s)
type Boundary (S¹_ s) = EmptyMfd (ZeroDim s)
type HalfNeedle (S¹_ s) = ℝay_ s
fromInterior :: Interior (S¹_ s) -> S¹_ s
fromInterior = forall a. a -> a
id
fromBoundary :: Boundary (S¹_ s) -> S¹_ s
fromBoundary Boundary (S¹_ s)
b = case Boundary (S¹_ s)
b of {}
separateInterior :: S¹_ s -> Either (Boundary (S¹_ s)) (Interior (S¹_ s))
separateInterior = forall a b. b -> Either a b
Right
Boundary (S¹_ s)
p|+^ :: Boundary (S¹_ s) -> HalfNeedle (S¹_ s) -> S¹_ s
|+^HalfNeedle (S¹_ s)
_ = case Boundary (S¹_ s)
p of {}
S¹_ s
_ .+^| :: S¹_ s
-> Needle (Interior (S¹_ s))
-> Either
(Boundary (S¹_ s), Scalar (Needle (Interior (S¹_ s))))
(Interior (S¹_ s))
.+^| Needle (Interior (S¹_ s))
p = case Needle (Interior (S¹_ s))
p of {}
extendToBoundary :: Interior (S¹_ s)
-> Needle (Interior (S¹_ s)) -> Maybe (Boundary (S¹_ s))
extendToBoundary Interior (S¹_ s)
_ Needle (Interior (S¹_ s))
_ = forall a. Maybe a
Nothing
smfdWBoundWitness :: SmfdWBoundWitness (S¹_ s)
smfdWBoundWitness = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
scalarIsOpenMfd :: forall r.
(OpenManifold (Scalar (Needle (Interior (S¹_ s)))) => r) -> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (S¹_ s)))) => r
q = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> OpenManifold (Scalar (Needle (Interior (S¹_ s)))) => r
q
boundaryHasSameScalar :: forall r.
((LinearSpace (Needle (Boundary (S¹_ s))),
Scalar (Needle (Boundary (S¹_ s)))
~ Scalar (Needle (Interior (S¹_ s)))) =>
r)
-> r
boundaryHasSameScalar (LinearSpace (Needle (Boundary (S¹_ s))),
Scalar (Needle (Boundary (S¹_ s)))
~ Scalar (Needle (Interior (S¹_ s)))) =>
r
q = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> (LinearSpace (Needle (Boundary (S¹_ s))),
Scalar (Needle (Boundary (S¹_ s)))
~ Scalar (Needle (Interior (S¹_ s)))) =>
r
q
instance ∀ s . RealFloat'' s => PseudoAffineWithBoundary (S¹_ s) where
S¹_ s
_!-| :: S¹_ s -> Boundary (S¹_ s) -> HalfNeedle (S¹_ s)
!-|Boundary (S¹_ s)
p = case Boundary (S¹_ s)
p of {}
.--! :: S¹_ s -> S¹_ s -> Needle (Interior (S¹_ s))
(.--!) = forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
(.-~!)
instance ∀ s . RealFloat'' s => ProjectableBoundary (S¹_ s) where
scalarBoundaryIsTriviallyProjectible :: forall r.
(ProjectableBoundary (Scalar (Needle (Interior (S¹_ s)))) => r)
-> r
scalarBoundaryIsTriviallyProjectible ProjectableBoundary (Scalar (Needle (Interior (S¹_ s)))) => r
q = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of
ClosedScalarWitness s
ClosedScalarWitness -> ProjectableBoundary (Scalar (Needle (Interior (S¹_ s)))) => r
q
projectToBoundary :: S¹_ s
-> Boundary (S¹_ s)
-> Maybe
(Needle (Boundary (S¹_ s)), Scalar (Needle (Interior (S¹_ s))))
projectToBoundary S¹_ s
_ Boundary (S¹_ s)
p = case Boundary (S¹_ s)
p of {}
marginFromBoundary :: Boundary (S¹_ s) -> Scalar (Needle (Interior (S¹_ s))) -> S¹_ s
marginFromBoundary Boundary (S¹_ s)
p = case Boundary (S¹_ s)
p of {}
instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (S²_ s) where
type Interior (S²_ s) = S²_ s
type Boundary (S²_ s) = EmptyMfd s
type HalfNeedle (S²_ s) = ℝay_ s
fromInterior :: Interior (S²_ s) -> S²_ s
fromInterior = forall a. a -> a
id
fromBoundary :: Boundary (S²_ s) -> S²_ s
fromBoundary Boundary (S²_ s)
b = case Boundary (S²_ s)
b of {}
separateInterior :: S²_ s -> Either (Boundary (S²_ s)) (Interior (S²_ s))
separateInterior = forall a b. b -> Either a b
Right
Boundary (S²_ s)
p|+^ :: Boundary (S²_ s) -> HalfNeedle (S²_ s) -> S²_ s
|+^HalfNeedle (S²_ s)
_ = case Boundary (S²_ s)
p of {}
S²_ s
_ .+^| :: S²_ s
-> Needle (Interior (S²_ s))
-> Either
(Boundary (S²_ s), Scalar (Needle (Interior (S²_ s))))
(Interior (S²_ s))
.+^| Needle (Interior (S²_ s))
p = case Needle (Interior (S²_ s))
p of {}
extendToBoundary :: Interior (S²_ s)
-> Needle (Interior (S²_ s)) -> Maybe (Boundary (S²_ s))
extendToBoundary Interior (S²_ s)
_ Needle (Interior (S²_ s))
_ = forall a. Maybe a
Nothing
smfdWBoundWitness :: SmfdWBoundWitness (S²_ s)
smfdWBoundWitness = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
scalarIsOpenMfd :: forall r.
(OpenManifold (Scalar (Needle (Interior (S²_ s)))) => r) -> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (S²_ s)))) => r
q = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> OpenManifold (Scalar (Needle (Interior (S²_ s)))) => r
q
boundaryHasSameScalar :: forall r.
((LinearSpace (Needle (Boundary (S²_ s))),
Scalar (Needle (Boundary (S²_ s)))
~ Scalar (Needle (Interior (S²_ s)))) =>
r)
-> r
boundaryHasSameScalar (LinearSpace (Needle (Boundary (S²_ s))),
Scalar (Needle (Boundary (S²_ s)))
~ Scalar (Needle (Interior (S²_ s)))) =>
r
q = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> (LinearSpace (Needle (Boundary (S²_ s))),
Scalar (Needle (Boundary (S²_ s)))
~ Scalar (Needle (Interior (S²_ s)))) =>
r
q
instance ∀ s . RealFloat'' s => PseudoAffineWithBoundary (S²_ s) where
S²_ s
_!-| :: S²_ s -> Boundary (S²_ s) -> HalfNeedle (S²_ s)
!-|Boundary (S²_ s)
p = case Boundary (S²_ s)
p of {}
.--! :: S²_ s -> S²_ s -> Needle (Interior (S²_ s))
(.--!) = forall x. (PseudoAffine x, HasCallStack) => x -> x -> Needle x
(.-~!)
instance ∀ s . RealFloat'' s => ProjectableBoundary (S²_ s) where
scalarBoundaryIsTriviallyProjectible :: forall r.
(ProjectableBoundary (Scalar (Needle (Interior (S²_ s)))) => r)
-> r
scalarBoundaryIsTriviallyProjectible ProjectableBoundary (Scalar (Needle (Interior (S²_ s)))) => r
q = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of
ClosedScalarWitness s
ClosedScalarWitness -> ProjectableBoundary (Scalar (Needle (Interior (S²_ s)))) => r
q
projectToBoundary :: S²_ s
-> Boundary (S²_ s)
-> Maybe
(Needle (Boundary (S²_ s)), Scalar (Needle (Interior (S²_ s))))
projectToBoundary S²_ s
_ Boundary (S²_ s)
p = case Boundary (S²_ s)
p of {}
marginFromBoundary :: Boundary (S²_ s) -> Scalar (Needle (Interior (S²_ s))) -> S²_ s
marginFromBoundary Boundary (S²_ s)
p = case Boundary (S²_ s)
p of {}
instance ∀ s . RealFloat'' s => SemimanifoldWithBoundary (D¹_ s) where
type Interior (D¹_ s) = s
type Boundary (D¹_ s) = (S⁰_ s)
type HalfNeedle (D¹_ s) = ℝay_ s
fromBoundary :: Boundary (D¹_ s) -> D¹_ s
fromBoundary S⁰_ s
Boundary (D¹_ s)
NegativeHalfSphere = forall r. r -> D¹_ r
D¹ (-s
1)
fromBoundary S⁰_ s
Boundary (D¹_ s)
PositiveHalfSphere = forall r. r -> D¹_ r
D¹ s
1
fromInterior :: Interior (D¹_ s) -> D¹_ s
fromInterior = forall r. r -> D¹_ r
D¹ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Floating a => a -> a
tanh
separateInterior :: D¹_ s -> Either (Boundary (D¹_ s)) (Interior (D¹_ s))
separateInterior (D¹ (-1)) = forall a b. a -> Either a b
Left forall r. S⁰_ r
NegativeHalfSphere
separateInterior (D¹ s
1) = forall a b. a -> Either a b
Left forall r. S⁰_ r
PositiveHalfSphere
separateInterior (D¹ s
x) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. Floating a => a -> a
atanh s
x
S⁰_ s
Boundary (D¹_ s)
NegativeHalfSphere|+^ :: Boundary (D¹_ s) -> HalfNeedle (D¹_ s) -> D¹_ s
|+^Cℝay Scalar (Needle (ZeroDim s))
l ZeroDim s
Origin = forall r. r -> D¹_ r
D¹ forall a b. (a -> b) -> a -> b
$ s
1 forall a. Num a => a -> a -> a
- s
4forall a. Fractional a => a -> a -> a
/(Scalar (Needle (ZeroDim s))
lforall a. Num a => a -> a -> a
+s
2)
S⁰_ s
Boundary (D¹_ s)
PositiveHalfSphere|+^Cℝay Scalar (Needle (ZeroDim s))
l ZeroDim s
Origin = forall r. r -> D¹_ r
D¹ forall a b. (a -> b) -> a -> b
$ s
4forall a. Fractional a => a -> a -> a
/(Scalar (Needle (ZeroDim s))
lforall a. Num a => a -> a -> a
+s
2) forall a. Num a => a -> a -> a
- s
1
.+^| :: D¹_ s
-> Needle (Interior (D¹_ s))
-> Either
(Boundary (D¹_ s), Scalar (Needle (Interior (D¹_ s))))
(Interior (D¹_ s))
(.+^|) = case (forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s, forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s) of
(LinearManifoldWitness s
LinearManifoldWitness, ClosedScalarWitness s
ClosedScalarWitness) ->
let addBD¹ :: D¹_ b -> b -> Either (S⁰_ r, b) b
addBD¹ (D¹ b
p) b
l
| b
p' forall a. Ord a => a -> a -> Bool
>= b
1 = forall a b. a -> Either a b
Left (forall r. S⁰_ r
PositiveHalfSphere, (b
p'forall a. Num a => a -> a -> a
-b
1) forall a. Fractional a => a -> a -> a
/ b
l)
| b
p' forall a. Ord a => a -> a -> Bool
<= -b
1 = forall a b. a -> Either a b
Left (forall r. S⁰_ r
NegativeHalfSphere, (b
p'forall a. Num a => a -> a -> a
+b
1) forall a. Fractional a => a -> a -> a
/ b
l)
| Bool
otherwise = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. Floating a => a -> a
atanh b
p'
where p' :: b
p' = b
pforall a. Num a => a -> a -> a
+b
l
in forall {b} {r}.
(Ord b, Floating b) =>
D¹_ b -> b -> Either (S⁰_ r, b) b
addBD¹
extendToBoundary :: Interior (D¹_ s)
-> Needle (Interior (D¹_ s)) -> Maybe (Boundary (D¹_ s))
extendToBoundary = case (forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s, forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s) of
(LinearManifoldWitness s
LinearManifoldWitness, ClosedScalarWitness s
ClosedScalarWitness) ->
let e2b :: p -> a -> Maybe (S⁰_ r)
e2b p
_ a
dir
| a
dir forall a. Ord a => a -> a -> Bool
> a
0 = forall a. a -> Maybe a
Just forall r. S⁰_ r
PositiveHalfSphere
| a
dir forall a. Ord a => a -> a -> Bool
< a
0 = forall a. a -> Maybe a
Just forall r. S⁰_ r
NegativeHalfSphere
| Bool
otherwise = forall a. Maybe a
Nothing
in forall {a} {p} {r}. (Ord a, Num a) => p -> a -> Maybe (S⁰_ r)
e2b
smfdWBoundWitness :: SmfdWBoundWitness (D¹_ s)
smfdWBoundWitness = case forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> forall m.
(OpenManifold (Interior m), OpenManifold (Boundary m),
FullSubspace (HalfNeedle m) ~ Needle (Boundary m)) =>
SmfdWBoundWitness m
SmfdWBoundWitness
scalarIsOpenMfd :: forall r.
(OpenManifold (Scalar (Needle (Interior (D¹_ s)))) => r) -> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (D¹_ s)))) => r
q = case (forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s, forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s) of
(ClosedScalarWitness s
ClosedScalarWitness, LinearManifoldWitness s
LinearManifoldWitness) -> OpenManifold (Scalar (Needle (Interior (D¹_ s)))) => r
q
boundaryHasSameScalar :: forall r.
((LinearSpace (Needle (Boundary (D¹_ s))),
Scalar (Needle (Boundary (D¹_ s)))
~ Scalar (Needle (Interior (D¹_ s)))) =>
r)
-> r
boundaryHasSameScalar (LinearSpace (Needle (Boundary (D¹_ s))),
Scalar (Needle (Boundary (D¹_ s)))
~ Scalar (Needle (Interior (D¹_ s)))) =>
r
q = case (forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s, forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s) of
(ClosedScalarWitness s
ClosedScalarWitness, LinearManifoldWitness s
LinearManifoldWitness) -> (LinearSpace (Needle (Boundary (D¹_ s))),
Scalar (Needle (Boundary (D¹_ s)))
~ Scalar (Needle (Interior (D¹_ s)))) =>
r
q
needleIsOpenMfd :: forall r. (OpenManifold (Needle (Interior (D¹_ s))) => r) -> r
needleIsOpenMfd OpenManifold (Needle (Interior (D¹_ s))) => r
q = case (forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s, forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s) of
(ClosedScalarWitness s
ClosedScalarWitness, LinearManifoldWitness s
LinearManifoldWitness) -> OpenManifold (Needle (Interior (D¹_ s))) => r
q
instance ( Num' n, OpenManifold n, LinearManifold (a n)
, Scalar (a n) ~ n, Needle (a n) ~ a n )
=> SemimanifoldWithBoundary (LinAff.Point a n) where
type Boundary (LinAff.Point a n) = EmptyMfd (ZeroDim n)
type Interior (LinAff.Point a n) = LinAff.Point a n
type HalfNeedle (LinAff.Point a n) = ℝay
smfdWBoundWitness :: SmfdWBoundWitness (Point a n)
smfdWBoundWitness = forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
LinAff.P a n
p.+^| :: Point a n
-> Needle (Interior (Point a n))
-> Either
(Boundary (Point a n), Scalar (Needle (Interior (Point a n))))
(Interior (Point a n))
.+^|Needle (Interior (Point a n))
v = forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a. f a -> Point f a
LinAff.P forall a b. (a -> b) -> a -> b
$ a n
pforall v. AdditiveGroup v => v -> v -> v
^+^Needle (Interior (Point a n))
v
fromInterior :: Interior (Point a n) -> Point a n
fromInterior = forall a. a -> a
id
fromBoundary :: Boundary (Point a n) -> Point a n
fromBoundary Boundary (Point a n)
b = case Boundary (Point a n)
b of {}
Boundary (Point a n)
b|+^ :: Boundary (Point a n) -> HalfNeedle (Point a n) -> Point a n
|+^HalfNeedle (Point a n)
_ = case Boundary (Point a n)
b of {}
instance ( Num' n, OpenManifold n, LinearManifold (a n)
, Scalar (a n) ~ n, Needle (a n) ~ a n )
=> PseudoAffineWithBoundary (LinAff.Point a n) where
LinAff.P a n
p.--! :: Point a n -> Point a n -> Needle (Interior (Point a n))
.--!LinAff.P a n
q = a n
pforall v. AdditiveGroup v => v -> v -> v
^-^a n
q
Point a n
_!-| :: Point a n -> Boundary (Point a n) -> HalfNeedle (Point a n)
!-|Boundary (Point a n)
b = case Boundary (Point a n)
b of {}
instance ∀ n a . ( Num' n, OpenManifold n, LinearManifold (a n), ProjectableBoundary n
, Scalar (a n) ~ n, Needle (a n) ~ a n )
=> ProjectableBoundary (LinAff.Point a n) where
projectToBoundary :: Point a n
-> Boundary (Point a n)
-> Maybe
(Needle (Boundary (Point a n)),
Scalar (Needle (Interior (Point a n))))
projectToBoundary Point a n
_ Boundary (Point a n)
b = case Boundary (Point a n)
b of {}
marginFromBoundary :: Boundary (Point a n)
-> Scalar (Needle (Interior (Point a n))) -> Point a n
marginFromBoundary Boundary (Point a n)
b Scalar (Needle (Interior (Point a n)))
_ = case Boundary (Point a n)
b of {}
instance ( LinearSpace v, LinearSpace w
, s ~ Scalar v, s ~ Scalar w
, Num' s, OpenManifold s
) => SemimanifoldWithBoundary (Tensor s v w) where
type Interior (Tensor s v w) = (Tensor s v w)
type Boundary (Tensor s v w) = EmptyMfd (ZeroDim s)
type HalfNeedle (Tensor s v w) = ℝay_ s
smfdWBoundWitness :: SmfdWBoundWitness (Tensor s v w)
smfdWBoundWitness = forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
fromInterior :: Interior (Tensor s v w) -> Tensor s v w
fromInterior = forall a. a -> a
id
fromBoundary :: Boundary (Tensor s v w) -> Tensor s v w
fromBoundary Boundary (Tensor s v w)
b = case Boundary (Tensor s v w)
b of {}
separateInterior :: Tensor s v w
-> Either (Boundary (Tensor s v w)) (Interior (Tensor s v w))
separateInterior = forall a b. b -> Either a b
Right
Boundary (Tensor s v w)
p|+^ :: Boundary (Tensor s v w)
-> HalfNeedle (Tensor s v w) -> Tensor s v w
|+^HalfNeedle (Tensor s v w)
_ = case Boundary (Tensor s v w)
p of {}
Tensor s v w
a.+^| :: Tensor s v w
-> Needle (Interior (Tensor s v w))
-> Either
(Boundary (Tensor s v w),
Scalar (Needle (Interior (Tensor s v w))))
(Interior (Tensor s v w))
.+^|Needle (Interior (Tensor s v w))
b = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ Tensor s v w
aforall v. AdditiveGroup v => v -> v -> v
^+^Needle (Interior (Tensor s v w))
b
extendToBoundary :: Interior (Tensor s v w)
-> Needle (Interior (Tensor s v w))
-> Maybe (Boundary (Tensor s v w))
extendToBoundary Interior (Tensor s v w)
_ Needle (Interior (Tensor s v w))
_ = forall a. Maybe a
Nothing
instance ( LinearSpace v, LinearSpace w
, s ~ Scalar v, s ~ Scalar w
, Num' s, OpenManifold s
) => PseudoAffineWithBoundary (Tensor s v w) where
Tensor s v w
_!-| :: Tensor s v w
-> Boundary (Tensor s v w) -> HalfNeedle (Tensor s v w)
!-|Boundary (Tensor s v w)
p = case Boundary (Tensor s v w)
p of {}
.--! :: Tensor s v w -> Tensor s v w -> Needle (Interior (Tensor s v w))
(.--!) = forall v. AdditiveGroup v => v -> v -> v
(^-^)
instance ( LinearSpace v, LinearSpace w
, s ~ Scalar v, s ~ Scalar w
, Num' s, OpenManifold s
) => SemimanifoldWithBoundary (LinearMap s v w) where
type Interior (LinearMap s v w) = (LinearMap s v w)
type Boundary (LinearMap s v w) = EmptyMfd (ZeroDim s)
type HalfNeedle (LinearMap s v w) = ℝay
smfdWBoundWitness :: SmfdWBoundWitness (LinearMap s v w)
smfdWBoundWitness = forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
fromInterior :: Interior (LinearMap s v w) -> LinearMap s v w
fromInterior = forall a. a -> a
id
fromBoundary :: Boundary (LinearMap s v w) -> LinearMap s v w
fromBoundary Boundary (LinearMap s v w)
b = case Boundary (LinearMap s v w)
b of {}
separateInterior :: LinearMap s v w
-> Either (Boundary (LinearMap s v w)) (Interior (LinearMap s v w))
separateInterior = forall a b. b -> Either a b
Right
Boundary (LinearMap s v w)
p|+^ :: Boundary (LinearMap s v w)
-> HalfNeedle (LinearMap s v w) -> LinearMap s v w
|+^HalfNeedle (LinearMap s v w)
_ = case Boundary (LinearMap s v w)
p of {}
LinearMap s v w
a.+^| :: LinearMap s v w
-> Needle (Interior (LinearMap s v w))
-> Either
(Boundary (LinearMap s v w),
Scalar (Needle (Interior (LinearMap s v w))))
(Interior (LinearMap s v w))
.+^|Needle (Interior (LinearMap s v w))
b = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ LinearMap s v w
aforall v. AdditiveGroup v => v -> v -> v
^+^Needle (Interior (LinearMap s v w))
b
extendToBoundary :: Interior (LinearMap s v w)
-> Needle (Interior (LinearMap s v w))
-> Maybe (Boundary (LinearMap s v w))
extendToBoundary Interior (LinearMap s v w)
_ Needle (Interior (LinearMap s v w))
_ = forall a. Maybe a
Nothing
instance ( LinearSpace v, LinearSpace w
, s ~ Scalar v, s ~ Scalar w
, Num' s, OpenManifold s, ProjectableBoundary s
) => ProjectableBoundary (LinearMap s v w) where
projectToBoundary :: LinearMap s v w
-> Boundary (LinearMap s v w)
-> Maybe
(Needle (Boundary (LinearMap s v w)),
Scalar (Needle (Interior (LinearMap s v w))))
projectToBoundary LinearMap s v w
_ Boundary (LinearMap s v w)
p = case Boundary (LinearMap s v w)
p of {}
marginFromBoundary :: Boundary (LinearMap s v w)
-> Scalar (Needle (Interior (LinearMap s v w))) -> LinearMap s v w
marginFromBoundary Boundary (LinearMap s v w)
p = case Boundary (LinearMap s v w)
p of {}
instance ( LinearSpace v, LinearSpace w
, s ~ Scalar v, s ~ Scalar w
, Num' s, OpenManifold s
) => PseudoAffineWithBoundary (LinearMap s v w) where
LinearMap s v w
_!-| :: LinearMap s v w
-> Boundary (LinearMap s v w) -> HalfNeedle (LinearMap s v w)
!-|Boundary (LinearMap s v w)
p = case Boundary (LinearMap s v w)
p of {}
.--! :: LinearMap s v w
-> LinearMap s v w -> Needle (Interior (LinearMap s v w))
(.--!) = forall v. AdditiveGroup v => v -> v -> v
(^-^)
instance ( LinearSpace v, LinearSpace w
, s ~ Scalar v, s ~ Scalar w
, Num' s, OpenManifold s
) => SemimanifoldWithBoundary (LinearFunction s v w) where
type Interior (LinearFunction s v w) = (LinearFunction s v w)
type Boundary (LinearFunction s v w) = EmptyMfd (ZeroDim s)
type HalfNeedle (LinearFunction s v w) = ℝay
smfdWBoundWitness :: SmfdWBoundWitness (LinearFunction s v w)
smfdWBoundWitness = forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
fromInterior :: Interior (LinearFunction s v w) -> LinearFunction s v w
fromInterior = forall a. a -> a
id
fromBoundary :: Boundary (LinearFunction s v w) -> LinearFunction s v w
fromBoundary Boundary (LinearFunction s v w)
b = case Boundary (LinearFunction s v w)
b of {}
separateInterior :: LinearFunction s v w
-> Either
(Boundary (LinearFunction s v w)) (Interior (LinearFunction s v w))
separateInterior = forall a b. b -> Either a b
Right
Boundary (LinearFunction s v w)
p|+^ :: Boundary (LinearFunction s v w)
-> HalfNeedle (LinearFunction s v w) -> LinearFunction s v w
|+^HalfNeedle (LinearFunction s v w)
_ = case Boundary (LinearFunction s v w)
p of {}
LinearFunction s v w
a.+^| :: LinearFunction s v w
-> Needle (Interior (LinearFunction s v w))
-> Either
(Boundary (LinearFunction s v w),
Scalar (Needle (Interior (LinearFunction s v w))))
(Interior (LinearFunction s v w))
.+^|Needle (Interior (LinearFunction s v w))
b = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ LinearFunction s v w
aforall v. AdditiveGroup v => v -> v -> v
^+^Needle (Interior (LinearFunction s v w))
b
extendToBoundary :: Interior (LinearFunction s v w)
-> Needle (Interior (LinearFunction s v w))
-> Maybe (Boundary (LinearFunction s v w))
extendToBoundary Interior (LinearFunction s v w)
_ Needle (Interior (LinearFunction s v w))
_ = forall a. Maybe a
Nothing
instance ( LinearSpace v, LinearSpace w
, s ~ Scalar v, s ~ Scalar w
, Num' s, OpenManifold s
) => PseudoAffineWithBoundary (LinearFunction s v w) where
LinearFunction s v w
_!-| :: LinearFunction s v w
-> Boundary (LinearFunction s v w)
-> HalfNeedle (LinearFunction s v w)
!-|Boundary (LinearFunction s v w)
p = case Boundary (LinearFunction s v w)
p of {}
.--! :: LinearFunction s v w
-> LinearFunction s v w -> Needle (Interior (LinearFunction s v w))
(.--!) = forall v. AdditiveGroup v => v -> v -> v
(^-^)
instance ( Semimanifold a
, Semimanifold (VRep a), Needle a ~ GenericNeedle a
, OpenManifold (Scalar (Needle (Gnrx.Rep a Void)))
, LinearSpace (Needle (Gnrx.Rep a Void))
, Num' (Scalar (Needle (Gnrx.Rep a Void))) )
=> SemimanifoldWithBoundary (GenericNeedle a) where
type Interior (GenericNeedle a) = GenericNeedle a
type Boundary (GenericNeedle a) = EmptyMfd (ZeroDim (Scalar (Needle (Gnrx.Rep a Void))))
type HalfNeedle (GenericNeedle a) = ℝay_ (Scalar (Needle (Gnrx.Rep a Void)))
extendToBoundary :: Interior (GenericNeedle a)
-> Needle (Interior (GenericNeedle a))
-> Maybe (Boundary (GenericNeedle a))
extendToBoundary Interior (GenericNeedle a)
_ Needle (Interior (GenericNeedle a))
_ = forall a. Maybe a
Nothing
smfdWBoundWitness :: SmfdWBoundWitness (GenericNeedle a)
smfdWBoundWitness = forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
needleIsOpenMfd :: forall r.
(OpenManifold (Needle (Interior (GenericNeedle a))) => r) -> r
needleIsOpenMfd OpenManifold (Needle (Interior (GenericNeedle a))) => r
q = OpenManifold (Needle (Interior (GenericNeedle a))) => r
q
scalarIsOpenMfd :: forall r.
(OpenManifold (Scalar (Needle (Interior (GenericNeedle a)))) => r)
-> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (GenericNeedle a)))) => r
q = OpenManifold (Scalar (Needle (Interior (GenericNeedle a)))) => r
q
boundaryHasSameScalar :: forall r.
((LinearSpace (Needle (Boundary (GenericNeedle a))),
Scalar (Needle (Boundary (GenericNeedle a)))
~ Scalar (Needle (Interior (GenericNeedle a)))) =>
r)
-> r
boundaryHasSameScalar (LinearSpace (Needle (Boundary (GenericNeedle a))),
Scalar (Needle (Boundary (GenericNeedle a)))
~ Scalar (Needle (Interior (GenericNeedle a)))) =>
r
q = (LinearSpace (Needle (Boundary (GenericNeedle a))),
Scalar (Needle (Boundary (GenericNeedle a)))
~ Scalar (Needle (Interior (GenericNeedle a)))) =>
r
q
Boundary (GenericNeedle a)
b|+^ :: Boundary (GenericNeedle a)
-> HalfNeedle (GenericNeedle a) -> GenericNeedle a
|+^HalfNeedle (GenericNeedle a)
_ = case Boundary (GenericNeedle a)
b of {}
GenericNeedle a
p .+^| :: GenericNeedle a
-> Needle (Interior (GenericNeedle a))
-> Either
(Boundary (GenericNeedle a),
Scalar (Needle (Interior (GenericNeedle a))))
(Interior (GenericNeedle a))
.+^| Needle (Interior (GenericNeedle a))
k = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ GenericNeedle a
pforall v. AdditiveGroup v => v -> v -> v
^+^Needle (Interior (GenericNeedle a))
k
fromBoundary :: Boundary (GenericNeedle a) -> GenericNeedle a
fromBoundary Boundary (GenericNeedle a)
b = case Boundary (GenericNeedle a)
b of {}
instance ( Semimanifold a
, Semimanifold (VRep a), Needle a ~ GenericNeedle a
, OpenManifold (Scalar (Needle (Gnrx.Rep a Void)))
, LinearSpace (Needle (Gnrx.Rep a Void))
, Num' (Scalar (Needle (Gnrx.Rep a Void))) )
=> PseudoAffineWithBoundary (GenericNeedle a) where
GenericNeedle a
_ !-| :: GenericNeedle a
-> Boundary (GenericNeedle a) -> HalfNeedle (GenericNeedle a)
!-| Boundary (GenericNeedle a)
b = case Boundary (GenericNeedle a)
b of {}
.--! :: GenericNeedle a
-> GenericNeedle a -> Needle (Interior (GenericNeedle a))
(.--!) = forall v. AdditiveGroup v => v -> v -> v
(^-^)