-- |
-- Module      : Data.Manifold.WithBoundary
-- Copyright   : (c) Justus Sagemüller 2020
-- 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 StandaloneDeriving       #-}
{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE UnicodeSyntax            #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE EmptyCase                #-}
{-# LANGUAGE LambdaCase               #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE TypeInType               #-}
{-# 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(..)
                               )
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)





#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)
ProductBoundaryNeedleT dn a b v
n
  ProductBoundaryNeedleT dn a b v
n .+^ Diff (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
-> ProductBoundaryNeedleT dn a 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))
xSpace dn (Needle (Boundary a))
-> Space dn (Needle (Boundary a)) -> Space dn (Needle (Boundary a))
forall v. AdditiveGroup v => v -> v -> v
^+^Space dn (Needle (Boundary a))
ξ) (Space dn (Needle (Interior b))
ySpace dn (Needle (Interior b))
-> Space dn (Needle (Interior b)) -> Space dn (Needle (Interior b))
forall v. AdditiveGroup v => v -> v -> v
^+^Space dn (Needle (Interior b))
υ) (v
vv -> v -> v
forall 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
-> ProductBoundaryNeedleT dn a 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))
xSpace dn (Needle (Interior a))
-> Space dn (Needle (Interior a)) -> Space dn (Needle (Interior a))
forall v. AdditiveGroup v => v -> v -> v
^+^Space dn (Needle (Interior a))
ξ) (Space dn (Needle (Boundary b))
ySpace dn (Needle (Boundary b))
-> Space dn (Needle (Boundary b)) -> Space dn (Needle (Boundary b))
forall v. AdditiveGroup v => v -> v -> v
^+^Space dn (Needle (Boundary b))
υ) (v
vv -> v -> v
forall 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 = Diff (ProductBoundaryNeedleT dn a b v)
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
β = Space dn (Needle (Boundary a))
-> Space dn (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT dn a 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))
xSpace dn (Needle (Boundary a))
-> Space dn (Needle (Boundary a)) -> Space dn (Needle (Boundary a))
forall v. AdditiveGroup v => v -> v -> v
^-^Space dn (Needle (Boundary a))
ξ) (Space dn (Needle (Interior b))
ySpace dn (Needle (Interior b))
-> Space dn (Needle (Interior b)) -> Space dn (Needle (Interior b))
forall v. AdditiveGroup v => v -> v -> v
^-^Space dn (Needle (Interior b))
υ) (v
vv -> v -> v
forall 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
β = Space dn (Needle (Interior a))
-> Space dn (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT dn a 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))
xSpace dn (Needle (Interior a))
-> Space dn (Needle (Interior a)) -> Space dn (Needle (Interior a))
forall v. AdditiveGroup v => v -> v -> v
^-^Space dn (Needle (Interior a))
ξ) (Space dn (Needle (Boundary b))
ySpace dn (Needle (Boundary b))
-> Space dn (Needle (Boundary b)) -> Space dn (Needle (Boundary b))
forall v. AdditiveGroup v => v -> v -> v
^-^Space dn (Needle (Boundary b))
υ) (v
vv -> v -> v
forall 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 = ProductBoundaryNeedleT dn a b v
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
(^+^) = 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 = ProductBoundaryNeedleT dn a b v
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) = Space dn (Needle (Boundary a))
-> Space dn (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT dn a 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)) -> Space dn (Needle (Boundary a))
forall v. AdditiveGroup v => v -> v
negateV Space dn (Needle (Boundary a))
x) (Space dn (Needle (Interior b)) -> Space dn (Needle (Interior b))
forall v. AdditiveGroup v => v -> v
negateV Space dn (Needle (Interior b))
y) (v -> v
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) = Space dn (Needle (Interior a))
-> Space dn (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT dn a 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)) -> Space dn (Needle (Interior a))
forall v. AdditiveGroup v => v -> v
negateV Space dn (Needle (Interior a))
x) (Space dn (Needle (Boundary b)) -> Space dn (Needle (Boundary b))
forall v. AdditiveGroup v => v -> v
negateV Space dn (Needle (Boundary b))
y) (v -> v
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
(*^) = ((LinearSpace (Needle (Boundary a)),
  Scalar (Needle (Boundary a)) ~ Scalar (Needle (Interior a))) =>
 Scalar v
 -> ProductBoundaryNeedleT dn a b v
 -> ProductBoundaryNeedleT dn a b v)
-> Scalar 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 (((LinearSpace (Needle (Boundary b)),
  Scalar (Needle (Boundary b)) ~ Scalar (Needle (Interior b))) =>
 Scalar v
 -> ProductBoundaryNeedleT dn a b v
 -> ProductBoundaryNeedleT dn a b v)
-> Scalar 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 @b (
            case (ValidDualness dn => DualnessSingletons dn
forall (dn :: Dualness). ValidDualness dn => DualnessSingletons dn
decideDualness @dn, SemimanifoldWithBoundary a => SmfdWBoundWitness a
forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @a, SemimanifoldWithBoundary b => SmfdWBoundWitness b
forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @b) of
     (DualnessSingletons dn
VectorWitness, SmfdWBoundWitness a
_, SmfdWBoundWitness b
_) -> \Scalar v
μ -> \case
        ProductBoundaryNeedleT 'Vector a b v
ZeroProductBoundaryNeedle -> ProductBoundaryNeedleT 'Vector a b v
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 -> Space 'Vector (Needle (Boundary a))
-> Space 'Vector (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT 'Vector a 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 (Scalar v
Scalar (Needle (Boundary a))
μScalar (Needle (Boundary a))
-> Needle (Boundary a) -> Needle (Boundary a)
forall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Vector (Needle (Boundary a))
Needle (Boundary a)
x) (Scalar v
Scalar (Needle (Interior b))
μScalar (Needle (Interior b))
-> Needle (Interior b) -> Needle (Interior b)
forall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Vector (Needle (Interior b))
Needle (Interior b)
y) (Scalar v
μScalar v -> v -> v
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 -> Space 'Vector (Needle (Interior a))
-> Space 'Vector (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT 'Vector a 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 (Scalar v
Scalar (Needle (Interior a))
μScalar (Needle (Interior a))
-> Needle (Interior a) -> Needle (Interior a)
forall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Vector (Needle (Interior a))
Needle (Interior a)
x) (Scalar v
Scalar (Needle (Boundary b))
μScalar (Needle (Boundary b))
-> Needle (Boundary b) -> Needle (Boundary b)
forall v. VectorSpace v => Scalar v -> v -> v
*^Space 'Vector (Needle (Boundary b))
Needle (Boundary b)
y) (Scalar v
μScalar v -> v -> v
forall v. VectorSpace v => Scalar v -> v -> v
*^v
v)
     (DualnessSingletons dn
FunctionalWitness, SmfdWBoundWitness a
SmfdWBoundWitness, SmfdWBoundWitness b
SmfdWBoundWitness)
                       -> case ( LinearSpace (Needle (Interior a)) =>
DualSpaceWitness (Needle (Interior a))
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(Needle (Interior a))
                               , LinearSpace (Needle (Boundary a)) =>
DualSpaceWitness (Needle (Boundary a))
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(Needle (Boundary a))
                               , LinearSpace (Needle (Interior b)) =>
DualSpaceWitness (Needle (Interior b))
forall v. LinearSpace v => DualSpaceWitness v
dualSpaceWitness @(Needle (Interior b))
                               , LinearSpace (Needle (Boundary b)) =>
DualSpaceWitness (Needle (Boundary 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 v
μ -> \case
        ProductBoundaryNeedleT 'Functional a b v
ZeroProductBoundaryNeedle -> ProductBoundaryNeedleT 'Functional a b v
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 -> Space 'Functional (Needle (Boundary a))
-> Space 'Functional (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT 'Functional a 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 (Scalar v
Scalar (Space dn (Needle (Boundary a)))
μScalar (Space dn (Needle (Boundary a)))
-> Space dn (Needle (Boundary a)) -> Space dn (Needle (Boundary a))
forall v. VectorSpace v => Scalar v -> v -> v
*^Space dn (Needle (Boundary a))
Space 'Functional (Needle (Boundary a))
x) (Scalar v
Scalar (Space dn (Needle (Interior b)))
μScalar (Space dn (Needle (Interior b)))
-> Space dn (Needle (Interior b)) -> Space dn (Needle (Interior b))
forall v. VectorSpace v => Scalar v -> v -> v
*^Space dn (Needle (Interior b))
Space 'Functional (Needle (Interior b))
y) (Scalar v
μScalar v -> v -> v
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 -> Space 'Functional (Needle (Interior a))
-> Space 'Functional (Needle (Boundary b))
-> v
-> ProductBoundaryNeedleT 'Functional a 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 (Scalar v
Scalar (Space dn (Needle (Interior a)))
μScalar (Space dn (Needle (Interior a)))
-> Space dn (Needle (Interior a)) -> Space dn (Needle (Interior a))
forall v. VectorSpace v => Scalar v -> v -> v
*^Space dn (Needle (Interior a))
Space 'Functional (Needle (Interior a))
x) (Scalar v
Scalar (Space dn (Needle (Boundary b)))
μScalar (Space dn (Needle (Boundary b)))
-> Space dn (Needle (Boundary b)) -> Space dn (Needle (Boundary b))
forall v. VectorSpace v => Scalar v -> v -> v
*^Space dn (Needle (Boundary b))
Space 'Functional (Needle (Boundary b))
y) (Scalar v
μScalar v -> v -> v
forall v. VectorSpace v => Scalar v -> 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))
         , 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 = ProductBoundaryNeedleT dn a b v
-> Maybe (ProductBoundaryNeedleT dn a b v)
forall a. a -> Maybe a
Just ProductBoundaryNeedleT dn a b v
forall (dn :: Dualness) a b v. ProductBoundaryNeedleT dn a b v
ZeroProductBoundaryNeedle
  wellDefinedTensor :: (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
ZeroProductBoundaryNeedle) = Tensor (Scalar v) (ProductBoundaryNeedleT dn a b v) w
-> Maybe (Tensor (Scalar v) (ProductBoundaryNeedleT dn a b v) w)
forall a. a -> Maybe a
Just Tensor (Scalar v) (ProductBoundaryNeedleT dn a b v) w
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
(.+~^) = 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 = SemimanifoldWitness (ProductBoundaryNeedleT dn a b v)
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 = ProductBoundaryNeedleT dn a b v
-> Maybe (ProductBoundaryNeedleT dn a b v)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ProductBoundaryNeedleT dn a b v
pProductBoundaryNeedleT dn a b v
-> ProductBoundaryNeedleT dn a b v
-> ProductBoundaryNeedleT dn a b v
forall v. AdditiveGroup v => v -> v -> v
^-^ProductBoundaryNeedleT dn a b v
q)
  .-~! :: ProductBoundaryNeedleT dn a b v
-> ProductBoundaryNeedleT dn a b v
-> Needle (ProductBoundaryNeedleT dn a b v)
(.-~!) = 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 = SmfdWBoundWitness (ProductBoundaryNeedleT dn a b v)
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 x y.+~^(δx, δy)
--     = case (separateInterior x, separateInterior y) of
-- (Left bx, Right _) -> case y .+^| δy of
--            Right iy' -> undefined
  .+~^ :: ProductBoundary a b
-> Needle (ProductBoundary a b) -> ProductBoundary a b
(.+~^) = ProductBoundary a b
-> Needle (ProductBoundary a b) -> ProductBoundary a b
forall a. HasCallStack => a
undefined
  semimanifoldWitness :: SemimanifoldWitness (ProductBoundary a b)
semimanifoldWitness = case ( Semimanifold (Interior a) => SemimanifoldWitness (Interior a)
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior a)
                             , Semimanifold (Interior b) => SemimanifoldWitness (Interior b)
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior b) ) of
    (SemimanifoldWitness (Interior a)
SemimanifoldWitness, SemimanifoldWitness (Interior b)
SemimanifoldWitness)
       -> SemimanifoldWitness (ProductBoundary a b)
forall a. HasCallStack => a
undefined -- SemimanifoldWitness

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.-~! :: ProductBoundary a b
-> ProductBoundary a b -> Needle (ProductBoundary a b)
.-~!ProductBoundary a b
q = case ProductBoundary a b
pProductBoundary a b
-> ProductBoundary a b -> Maybe (Needle (ProductBoundary a b))
forall 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 -> [Char]
-> ProductBoundaryNeedleT
     'Vector a b (Scalar (Needle (Interior a)))
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 ( PseudoAffine (Interior a) => PseudoAffineWitness (Interior a)
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness @(Interior a)
                , PseudoAffine (Interior b) => PseudoAffineWitness (Interior b)
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness @(Interior b) ) of
   (PseudoAffineWitness SemimanifoldWitness (Interior a)
SemimanifoldWitness, PseudoAffineWitness 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
bxBoundary a -> Boundary a -> Maybe (Needle (Boundary a))
forall x. PseudoAffine x => x -> x -> Maybe (Needle x)
.-~.Boundary a
bξ, Interior b -> b
forall m. SemimanifoldWithBoundary m => Interior m -> m
fromInterior @b Interior b
yb -> b -> Maybe (Needle (Interior b))
forall m.
PseudoAffineWithBoundary m =>
m -> m -> Maybe (Needle (Interior m))
.--.Interior b -> b
forall m. SemimanifoldWithBoundary m => Interior m -> m
fromInterior Interior b
υ) of
                 (Just Needle (Boundary a)
δbx, Just Needle (Interior b)
δy) -> ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a)))
-> Maybe
     (ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a))))
forall a. a -> Maybe a
Just (ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a)))
 -> Maybe
      (ProductBoundaryNeedleT
         'Vector a b (Scalar (Needle (Interior a)))))
-> ProductBoundaryNeedleT
     'Vector a b (Scalar (Needle (Interior a)))
-> Maybe
     (ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a))))
forall a b. (a -> b) -> a -> b
$ Space 'Vector (Needle (Boundary a))
-> Space 'Vector (Needle (Interior b))
-> Scalar (Needle (Interior a))
-> ProductBoundaryNeedleT
     'Vector a b (Scalar (Needle (Interior a)))
forall (dn :: Dualness) a b v.
Space dn (Needle (Boundary a))
-> Space dn (Needle (Interior b))
-> v
-> ProductBoundaryNeedleT dn a b v
NBoundOfL Space 'Vector (Needle (Boundary a))
Needle (Boundary a)
δbx Space 'Vector (Needle (Interior b))
Needle (Interior b)
δy Scalar (Needle (Interior a))
1
                 (Maybe (Needle (Boundary a))
_, Maybe (Needle (Interior b))
Nothing) -> Maybe
  (ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a))))
forall a. Maybe a
Nothing
           BoundOfL Boundary a
bx Interior b
y − BoundOfR Interior a
ξ Boundary b
bυ
             = case ( Boundary a -> a
forall m. SemimanifoldWithBoundary m => Boundary m -> m
fromBoundary @a Boundary a
bxa -> a -> Maybe (Needle (Interior a))
forall m.
PseudoAffineWithBoundary m =>
m -> m -> Maybe (Needle (Interior m))
.--.Interior a -> a
forall m. SemimanifoldWithBoundary m => Interior m -> m
fromInterior Interior a
ξ
                    , b
-> Boundary b
-> Maybe (Needle (Boundary b), Scalar (Needle (Interior b)))
forall m.
ProjectableBoundary m =>
m
-> Boundary m
-> Maybe (Needle (Boundary m), Scalar (Needle (Interior m)))
projectToBoundary (Interior b -> b
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))
                    -> ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a)))
-> Maybe
     (ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a))))
forall a. a -> Maybe a
Just (ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a)))
 -> Maybe
      (ProductBoundaryNeedleT
         'Vector a b (Scalar (Needle (Interior a)))))
-> ProductBoundaryNeedleT
     'Vector a b (Scalar (Needle (Interior a)))
-> Maybe
     (ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a))))
forall a b. (a -> b) -> a -> b
$ Space 'Vector (Needle (Interior a))
-> Space 'Vector (Needle (Boundary b))
-> Scalar (Needle (Interior a))
-> ProductBoundaryNeedleT
     'Vector a b (Scalar (Needle (Interior a)))
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)
δbxNeedle (Interior a)
-> Scalar (Needle (Interior a)) -> Needle (Interior a)
forall v s. (VectorSpace v, s ~ Scalar v) => v -> s -> v
^*(Scalar (Needle (Interior a))
1Scalar (Needle (Interior a))
-> Scalar (Needle (Interior a)) -> Scalar (Needle (Interior a))
forall a. Num a => a -> a -> a
+Scalar (Needle (Interior a))
dy)) Space 'Vector (Needle (Boundary b))
Needle (Boundary b)
δby Scalar (Needle (Interior a))
1
                 (Maybe (Needle (Interior a)),
 Maybe (Needle (Boundary b), Scalar (Needle (Interior a))))
_ -> Maybe
  (ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a))))
forall a. Maybe a
Nothing
       in ProductBoundary a b
-> ProductBoundary a b -> Maybe (Needle (ProductBoundary a b))
ProductBoundary a b
-> ProductBoundary a b
-> Maybe
     (ProductBoundaryNeedleT 'Vector a b (Scalar (Needle (Interior a))))
(−)
  pseudoAffineWitness :: PseudoAffineWitness (ProductBoundary a b)
pseudoAffineWitness = case ( PseudoAffine (Interior a) => PseudoAffineWitness (Interior a)
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness @(Interior a)
                             , PseudoAffine (Interior b) => PseudoAffineWitness (Interior b)
forall x. PseudoAffine x => PseudoAffineWitness x
pseudoAffineWitness @(Interior b) ) of
    (PseudoAffineWitness SemimanifoldWitness (Interior a)
SemimanifoldWitness
     , PseudoAffineWitness SemimanifoldWitness)
       -> PseudoAffineWitness (ProductBoundary a b)
forall a. HasCallStack => a
undefined {- PseudoAffineWitness SemimanifoldWitness -}

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 = ProductBoundary a b
-> Either
     (EmptyMfd (Needle (Boundary a), Needle (Boundary b)),
      Scalar (Scalar (Needle (Interior a))))
     (ProductBoundary a b)
forall a b. b -> Either a b
Right (ProductBoundary a b
 -> Either
      (EmptyMfd (Needle (Boundary a), Needle (Boundary b)),
       Scalar (Scalar (Needle (Interior a))))
      (ProductBoundary a b))
-> ProductBoundary a b
-> Either
     (EmptyMfd (Needle (Boundary a), Needle (Boundary b)),
      Scalar (Scalar (Needle (Interior a))))
     (ProductBoundary a b)
forall a b. (a -> b) -> a -> b
$ ProductBoundary a b
pProductBoundary a b
-> Needle (ProductBoundary a b) -> ProductBoundary a b
forall x. Semimanifold x => x -> Needle x -> x
.+~^Needle (Interior (ProductBoundary a b))
Needle (ProductBoundary a b)
q
  fromInterior :: Interior (ProductBoundary a b) -> ProductBoundary a b
fromInterior = Interior (ProductBoundary a b) -> ProductBoundary a b
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 = ((LinearSpace (Needle (Boundary a)),
  Scalar (Needle (Boundary a)) ~ Scalar (Needle (Interior a))) =>
 SmfdWBoundWitness (ProductBoundary a b))
-> SmfdWBoundWitness (ProductBoundary a b)
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @a
     (case Num' (Scalar (Needle (Interior a))) =>
ClosedScalarWitness (Scalar (Needle (Interior a)))
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar (Needle (Interior a))) of
              ClosedScalarWitness (Scalar (Needle (Interior a)))
ClosedScalarWitness -> SmfdWBoundWitness (ProductBoundary a b)
forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness)
  needleIsOpenMfd :: (OpenManifold (Needle (Interior (ProductBoundary a b))) => r) -> r
needleIsOpenMfd OpenManifold (Needle (Interior (ProductBoundary a b))) => r
r = (OpenManifold (Needle (Interior a)) => r) -> r
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @a ((OpenManifold (Needle (Interior b)) => r) -> r
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @b
                        (case Num' (Scalar (Needle (Interior a))) =>
ClosedScalarWitness (Scalar (Needle (Interior a)))
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar (Needle (Interior a))) of
                           ClosedScalarWitness (Scalar (Needle (Interior a)))
ClosedScalarWitness -> r
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 :: (OpenManifold (Scalar (Needle (Interior (ProductBoundary a b)))) =>
 r)
-> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (ProductBoundary a b)))) =>
r
r = ((LinearSpace (Needle (Boundary a)),
  Scalar (Needle (Boundary a)) ~ Scalar (Needle (Interior a))) =>
 r)
-> r
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @a
     (case Num' (Scalar (Needle (Interior a))) =>
ClosedScalarWitness (Scalar (Needle (Interior a)))
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar (Needle (Interior a))) of
              ClosedScalarWitness (Scalar (Needle (Interior a)))
ClosedScalarWitness -> r
OpenManifold (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
boundaryHasSameScalar (LinearSpace (Needle (Boundary (ProductBoundary a b))),
 Scalar (Needle (Boundary (ProductBoundary a b)))
 ~ Scalar (Needle (Interior (ProductBoundary a b)))) =>
r
r = ((LinearSpace (Needle (Boundary a)),
  Scalar (Needle (Boundary a)) ~ Scalar (Needle (Interior a))) =>
 r)
-> r
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @a (((LinearSpace (Needle (Boundary b)),
  Scalar (Needle (Boundary b)) ~ Scalar (Needle (Interior b))) =>
 r)
-> r
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @b
     (case Num' (Scalar (Needle (Interior a))) =>
ClosedScalarWitness (Scalar (Needle (Interior a)))
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @(Scalar (Needle (Interior a))) of
              ClosedScalarWitness (Scalar (Needle (Interior a)))
ClosedScalarWitness -> r
(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 :: ProductBoundary a b -> x
eliminate (BoundOfL Boundary a
ba Interior b
_) = Boundary a -> x
forall a x. Empty a => a -> x
eliminate Boundary a
ba
  eliminate (BoundOfR Interior a
_ Boundary b
bb) = Boundary b -> x
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 = Needle (Interior a) -> Needle (Interior b) -> ProductHalfNeedle a b
forall a b.
Needle (Interior a) -> Needle (Interior b) -> ProductHalfNeedle a b
ProductHalfNeedle Needle (Interior a)
forall v. AdditiveGroup v => v
zeroV Needle (Interior b)
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)
ĥ)
            = Needle (Interior a) -> Needle (Interior b) -> ProductHalfNeedle a b
forall a b.
Needle (Interior a) -> Needle (Interior b) -> ProductHalfNeedle a b
ProductHalfNeedle (Needle (Interior a)
vNeedle (Interior a) -> Needle (Interior a) -> Needle (Interior a)
forall v. AdditiveGroup v => v -> v -> v
^+^Needle (Interior a)
ϋ) (Needle (Interior b)
wNeedle (Interior b) -> Needle (Interior b) -> Needle (Interior b)
forall 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 SemimanifoldWithBoundary a => SmfdWBoundWitness a
forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @a of
     SmfdWBoundWitness a
SmfdWBoundWitness 
        -> ((LinearSpace (Needle (Boundary a)),
  Scalar (Needle (Boundary a)) ~ Scalar (Needle (Interior a))) =>
 ℝay_ (Scalar (Needle (Interior a)))
 -> ProductHalfNeedle a b -> ProductHalfNeedle a b)
-> ℝay_ (Scalar (Needle (Interior a)))
-> ProductHalfNeedle a b
-> ProductHalfNeedle a b
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)
         -> Needle (Interior a) -> Needle (Interior b) -> ProductHalfNeedle a b
forall a b.
Needle (Interior a) -> Needle (Interior b) -> ProductHalfNeedle a b
ProductHalfNeedle (Scalar (Needle (ZeroDim (Scalar (Needle (Interior a)))))
Scalar (Needle (Interior a))
μScalar (Needle (Interior a))
-> Needle (Interior a) -> Needle (Interior a)
forall v. VectorSpace v => Scalar v -> v -> v
*^Needle (Interior a)
v) (Scalar (Needle (ZeroDim (Scalar (Needle (Interior a)))))
Scalar (Needle (Interior b))
μScalar (Needle (Interior b))
-> Needle (Interior b) -> Needle (Interior b)
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)
ZeroProductBoundaryNeedle = ProductHalfNeedle a b
forall h. AdditiveMonoid h => h
zeroHV
  fullSubspaceIsVectorSpace :: ((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 = r
forall a. HasCallStack => a
undefined
  projectToFullSubspace :: ProductHalfNeedle a b -> FullSubspace (ProductHalfNeedle a b)
projectToFullSubspace = ProductHalfNeedle a b -> FullSubspace (ProductHalfNeedle a b)
forall a. HasCallStack => a
undefined
  rayIsHalfSpace :: (HalfSpace (Ray (ProductHalfNeedle a b)) => r) -> r
rayIsHalfSpace HalfSpace (Ray (ProductHalfNeedle a b)) => r
_ = r
forall a. HasCallStack => a
undefined
  fromPositiveHalf :: ProductHalfNeedle a b -> MirrorJoin (ProductHalfNeedle a b)
fromPositiveHalf = ProductHalfNeedle a b -> MirrorJoin (ProductHalfNeedle a b)
forall a. HasCallStack => a
undefined
  fromNegativeHalf :: ProductHalfNeedle a b -> MirrorJoin (ProductHalfNeedle a b)
fromNegativeHalf = ProductHalfNeedle a b -> MirrorJoin (ProductHalfNeedle a b)
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 = Interior (a, b)
-> Needle (Interior (a, b)) -> Maybe (Boundary (a, b))
forall a. HasCallStack => a
undefined
  smfdWBoundWitness :: SmfdWBoundWitness (a, b)
smfdWBoundWitness = case (SemimanifoldWithBoundary a => SmfdWBoundWitness a
forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @a, SemimanifoldWithBoundary b => SmfdWBoundWitness b
forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @b) of
    (SmfdWBoundWitness a
OpenManifoldWitness, SmfdWBoundWitness b
OpenManifoldWitness)
        -> (OpenManifold (Needle (Interior a)) => SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @a ((OpenManifold (Needle (Interior b)) => SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @b (
             ((LinearSpace (Needle (Boundary (Needle a))),
  Scalar (Needle (Boundary (Needle a)))
  ~ Scalar (Needle (Interior (Needle a)))) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @(Needle a) (((LinearSpace (Needle (Boundary (Needle b))),
  Scalar (Needle (Boundary (Needle b)))
  ~ Scalar (Needle (Interior (Needle b)))) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @(Needle b)
               (case (Semimanifold (Interior a) => SemimanifoldWitness (Interior a)
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior a), Semimanifold (Interior b) => SemimanifoldWitness (Interior b)
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior b))
                 of (SemimanifoldWitness a
SemimanifoldWitness, SemimanifoldWitness b
SemimanifoldWitness)
                        -> (ProjectableBoundary (Needle (Interior a)) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @a
                            ((ProjectableBoundary (Needle (Interior b)) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @b ProjectableBoundary (Needle (Interior b)) =>
SmfdWBoundWitness (a, b)
forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness) )
            )))
    (SmfdWBoundWitness a
SmfdWBoundWitness, SmfdWBoundWitness b
SmfdWBoundWitness)
        -> ((LinearSpace (Needle (Boundary a)),
  Scalar (Needle (Boundary a)) ~ Scalar (Needle (Interior a))) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @a
            (((LinearSpace (Needle (Boundary b)),
  Scalar (Needle (Boundary b)) ~ Scalar (Needle (Interior b))) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @b
              ((OpenManifold (Needle (Interior (Interior a))) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @(Interior a)
                ((OpenManifold (Needle (Interior (Interior b))) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @(Interior b)
                  (case ( Semimanifold (Interior a) => SemimanifoldWitness (Interior a)
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior a)
                        , Semimanifold (Interior b) => SemimanifoldWitness (Interior b)
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior b)
                        , Num' (Scalar (Needle (Interior a))) =>
ClosedScalarWitness (Scalar (Needle (Interior a)))
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)
                        -> (ProjectableBoundary (Needle (Interior a)) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @a
                            ((ProjectableBoundary (Needle (Interior b)) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @b
                              (((LinearSpace (Needle (Boundary (Needle (Interior a)))),
  Scalar (Needle (Boundary (Needle (Interior a))))
  ~ Scalar (Needle (Interior (Needle (Interior a))))) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @(Needle (Interior a))
                                (((LinearSpace (Needle (Boundary (Needle (Interior b)))),
  Scalar (Needle (Boundary (Needle (Interior b))))
  ~ Scalar (Needle (Interior (Needle (Interior b))))) =>
 SmfdWBoundWitness (a, b))
-> SmfdWBoundWitness (a, b)
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @(Needle (Interior b))
                                  (LinearSpace (Needle (Boundary (Needle (Interior b)))),
 Scalar (Needle (Boundary (Needle (Interior b))))
 ~ Scalar (Needle (Interior (Needle (Interior b))))) =>
SmfdWBoundWitness (a, b)
forall m.
(OpenManifold (Interior m), OpenManifold (Boundary m),
 FullSubspace (HalfNeedle m) ~ Needle (Boundary m)) =>
SmfdWBoundWitness m
SmfdWBoundWitness)))))))
  boundaryHasSameScalar :: ((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 = r
forall a. HasCallStack => a
undefined
  needleIsOpenMfd :: (OpenManifold (Needle (Interior (a, b))) => r) -> r
needleIsOpenMfd OpenManifold (Needle (Interior (a, b))) => r
_ = 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 :: (ProjectableBoundary (Needle (Interior (a, b))) => r) -> r
needleBoundaryIsTriviallyProjectible ProjectableBoundary (Needle (Interior (a, b))) => r
q
      = (ProjectableBoundary (Needle (Interior a)) => r) -> r
forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @a
         ((ProjectableBoundary (Needle (Interior b)) => r) -> r
forall m r.
ProjectableBoundary m =>
(ProjectableBoundary (Needle (Interior m)) => r) -> r
needleBoundaryIsTriviallyProjectible @b
           (((LinearSpace (Needle (Boundary (Needle (Interior a)))),
  Scalar (Needle (Boundary (Needle (Interior a))))
  ~ Scalar (Needle (Interior (Needle (Interior a))))) =>
 r)
-> r
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @(Needle (Interior a))
             (((LinearSpace (Needle (Boundary (Needle (Interior b)))),
  Scalar (Needle (Boundary (Needle (Interior b))))
  ~ Scalar (Needle (Interior (Needle (Interior b))))) =>
 r)
-> r
forall m r.
SemimanifoldWithBoundary m =>
((LinearSpace (Needle (Boundary m)),
  Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
 r)
-> r
boundaryHasSameScalar @(Needle (Interior b))
               ((OpenManifold (Needle (Interior a)) => r) -> r
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @a
                 ((OpenManifold (Needle (Interior b)) => r) -> r
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Needle (Interior m)) => r) -> r
needleIsOpenMfd @b
                   (case (Semimanifold (Interior a) => SemimanifoldWitness (Interior a)
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior a), Semimanifold (Interior b) => SemimanifoldWitness (Interior b)
forall x. Semimanifold x => SemimanifoldWitness x
semimanifoldWitness @(Interior b))
                     of (SemimanifoldWitness (Interior a)
SemimanifoldWitness, SemimanifoldWitness (Interior b)
SemimanifoldWitness) -> r
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 = Interior (S⁰_ s) -> S⁰_ s
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 = S⁰_ s -> Either (Boundary (S⁰_ s)) (Interior (S⁰_ s))
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))
.+^| Needle (Interior (S⁰_ s))
Origin = S⁰_ s -> Either (EmptyMfd (ZeroDim s), s) (S⁰_ s)
forall a b. b -> Either a b
Right S⁰_ s
forall r. S⁰_ r
NegativeHalfSphere
  S⁰_ s
PositiveHalfSphere .+^| Needle (Interior (S⁰_ s))
Origin = S⁰_ s -> Either (EmptyMfd (ZeroDim s), s) (S⁰_ s)
forall a b. b -> Either a b
Right S⁰_ s
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))
_ = Maybe (Boundary (S⁰_ s))
forall a. Maybe a
Nothing
  smfdWBoundWitness :: SmfdWBoundWitness (S⁰_ s)
smfdWBoundWitness = SmfdWBoundWitness (S⁰_ s)
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 = Interior (S¹_ s) -> S¹_ s
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 = S¹_ s -> Either (Boundary (S¹_ s)) (Interior (S¹_ s))
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))
_ = Maybe (Boundary (S¹_ s))
forall a. Maybe a
Nothing
  smfdWBoundWitness :: SmfdWBoundWitness (S¹_ s)
smfdWBoundWitness = case Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> SmfdWBoundWitness (S¹_ s)
forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
  scalarIsOpenMfd :: (OpenManifold (Scalar (Needle (Interior (S¹_ s)))) => r) -> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (S¹_ s)))) => r
q = case Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> r
OpenManifold (Scalar (Needle (Interior (S¹_ s)))) => r
q
  boundaryHasSameScalar :: ((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 Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> r
(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))
(.--!) = 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 :: (ProjectableBoundary (Scalar (Needle (Interior (S¹_ s)))) => r)
-> r
scalarBoundaryIsTriviallyProjectible ProjectableBoundary (Scalar (Needle (Interior (S¹_ s)))) => r
q = case Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of
     ClosedScalarWitness s
ClosedScalarWitness -> r
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 = Interior (S²_ s) -> S²_ s
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 = S²_ s -> Either (Boundary (S²_ s)) (Interior (S²_ s))
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))
_ = Maybe (Boundary (S²_ s))
forall a. Maybe a
Nothing
  smfdWBoundWitness :: SmfdWBoundWitness (S²_ s)
smfdWBoundWitness = case Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> SmfdWBoundWitness (S²_ s)
forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
  scalarIsOpenMfd :: (OpenManifold (Scalar (Needle (Interior (S²_ s)))) => r) -> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (S²_ s)))) => r
q = case Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> r
OpenManifold (Scalar (Needle (Interior (S²_ s)))) => r
q
  boundaryHasSameScalar :: ((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 Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> r
(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))
(.--!) = 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 :: (ProjectableBoundary (Scalar (Needle (Interior (S²_ s)))) => r)
-> r
scalarBoundaryIsTriviallyProjectible ProjectableBoundary (Scalar (Needle (Interior (S²_ s)))) => r
q = case Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of
     ClosedScalarWitness s
ClosedScalarWitness -> r
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 Boundary (D¹_ s)
NegativeHalfSphere = s -> D¹_ s
forall r. r -> D¹_ r
D¹ (-s
1)
  fromBoundary Boundary (D¹_ s)
PositiveHalfSphere = s -> D¹_ s
forall r. r -> D¹_ r
D¹ s
1
  fromInterior :: Interior (D¹_ s) -> D¹_ s
fromInterior = s -> D¹_ s
forall r. r -> D¹_ r
D¹ (s -> D¹_ s) -> (s -> s) -> s -> D¹_ s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> s
forall a. Floating a => a -> a
tanh
  separateInterior :: D¹_ s -> Either (Boundary (D¹_ s)) (Interior (D¹_ s))
separateInterior (D¹ (-1)) = S⁰_ s -> Either (S⁰_ s) s
forall a b. a -> Either a b
Left S⁰_ s
forall r. S⁰_ r
NegativeHalfSphere
  separateInterior (D¹ s
1) = S⁰_ s -> Either (S⁰_ s) s
forall a b. a -> Either a b
Left S⁰_ s
forall r. S⁰_ r
PositiveHalfSphere
  separateInterior (D¹ s
x) = s -> Either (S⁰_ s) s
forall a b. b -> Either a b
Right (s -> Either (S⁰_ s) s) -> s -> Either (S⁰_ s) s
forall a b. (a -> b) -> a -> b
$ s -> s
forall a. Floating a => a -> a
atanh s
x
  Boundary (D¹_ s)
NegativeHalfSphere|+^ :: Boundary (D¹_ s) -> HalfNeedle (D¹_ s) -> D¹_ s
|+^Cℝay l Origin = s -> D¹_ s
forall r. r -> D¹_ r
D¹ (s -> D¹_ s) -> s -> D¹_ s
forall a b. (a -> b) -> a -> b
$ s
1 s -> s -> s
forall a. Num a => a -> a -> a
- s
4s -> s -> s
forall a. Fractional a => a -> a -> a
/(s
Scalar (Needle (ZeroDim s))
ls -> s -> s
forall a. Num a => a -> a -> a
+s
2)
  Boundary (D¹_ s)
PositiveHalfSphere|+^Cℝay l Origin = s -> D¹_ s
forall r. r -> D¹_ r
D¹ (s -> D¹_ s) -> s -> D¹_ s
forall a b. (a -> b) -> a -> b
$ s
4s -> s -> s
forall a. Fractional a => a -> a -> a
/(s
Scalar (Needle (ZeroDim s))
ls -> s -> s
forall a. Num a => a -> a -> a
+s
2) s -> s -> s
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 (TensorSpace s => LinearManifoldWitness s
forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s, Num' s => ClosedScalarWitness 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' b -> b -> Bool
forall a. Ord a => a -> a -> Bool
>= b
1    = (S⁰_ r, b) -> Either (S⁰_ r, b) b
forall a b. a -> Either a b
Left (S⁰_ r
forall r. S⁰_ r
PositiveHalfSphere, (b
p'b -> b -> b
forall a. Num a => a -> a -> a
-b
1) b -> b -> b
forall a. Fractional a => a -> a -> a
/ b
l)
          | b
p' b -> b -> Bool
forall a. Ord a => a -> a -> Bool
<= -b
1   = (S⁰_ r, b) -> Either (S⁰_ r, b) b
forall a b. a -> Either a b
Left (S⁰_ r
forall r. S⁰_ r
NegativeHalfSphere, (b
p'b -> b -> b
forall a. Num a => a -> a -> a
+b
1) b -> b -> b
forall a. Fractional a => a -> a -> a
/ b
l)
          | Bool
otherwise  = b -> Either (S⁰_ r, b) b
forall a b. b -> Either a b
Right (b -> Either (S⁰_ r, b) b) -> b -> Either (S⁰_ r, b) b
forall a b. (a -> b) -> a -> b
$ b -> b
forall a. Floating a => a -> a
atanh b
p'
         where p' :: b
p' = b
pb -> b -> b
forall a. Num a => a -> a -> a
+b
l
    in D¹_ s
-> Needle (Interior (D¹_ s))
-> Either
     (Boundary (D¹_ s), Scalar (Needle (Interior (D¹_ s))))
     (Interior (D¹_ s))
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 (TensorSpace s => LinearManifoldWitness s
forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s, Num' s => ClosedScalarWitness 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 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0    = S⁰_ r -> Maybe (S⁰_ r)
forall a. a -> Maybe a
Just S⁰_ r
forall r. S⁰_ r
PositiveHalfSphere
         | a
dir a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0    = S⁰_ r -> Maybe (S⁰_ r)
forall a. a -> Maybe a
Just S⁰_ r
forall r. S⁰_ r
NegativeHalfSphere
         | Bool
otherwise  = Maybe (S⁰_ r)
forall a. Maybe a
Nothing
    in Interior (D¹_ s)
-> Needle (Interior (D¹_ s)) -> Maybe (Boundary (D¹_ s))
forall a p r. (Ord a, Num a) => p -> a -> Maybe (S⁰_ r)
e2b
  smfdWBoundWitness :: SmfdWBoundWitness (D¹_ s)
smfdWBoundWitness = case Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s of ClosedScalarWitness s
ClosedScalarWitness -> SmfdWBoundWitness (D¹_ s)
forall m.
(OpenManifold (Interior m), OpenManifold (Boundary m),
 FullSubspace (HalfNeedle m) ~ Needle (Boundary m)) =>
SmfdWBoundWitness m
SmfdWBoundWitness
  scalarIsOpenMfd :: (OpenManifold (Scalar (Needle (Interior (D¹_ s)))) => r) -> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (D¹_ s)))) => r
q = case (Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s, TensorSpace s => LinearManifoldWitness s
forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s) of
   (ClosedScalarWitness s
ClosedScalarWitness, LinearManifoldWitness s
LinearManifoldWitness) -> r
OpenManifold (Scalar (Needle (Interior (D¹_ s)))) => r
q
  boundaryHasSameScalar :: ((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 (Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s, TensorSpace s => LinearManifoldWitness s
forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s) of
   (ClosedScalarWitness s
ClosedScalarWitness, LinearManifoldWitness s
LinearManifoldWitness) -> r
(LinearSpace (Needle (Boundary (D¹_ s))),
 Scalar (Needle (Boundary (D¹_ s)))
 ~ Scalar (Needle (Interior (D¹_ s)))) =>
r
q
  needleIsOpenMfd :: (OpenManifold (Needle (Interior (D¹_ s))) => r) -> r
needleIsOpenMfd OpenManifold (Needle (Interior (D¹_ s))) => r
q = case (Num' s => ClosedScalarWitness s
forall s. Num' s => ClosedScalarWitness s
closedScalarWitness @s, TensorSpace s => LinearManifoldWitness s
forall v. TensorSpace v => LinearManifoldWitness v
linearManifoldWitness @s) of
   (ClosedScalarWitness s
ClosedScalarWitness, LinearManifoldWitness s
LinearManifoldWitness) -> r
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 = SmfdWBoundWitness (Point a n)
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 = Point a n -> Either (EmptyMfd (ZeroDim n), n) (Point a n)
forall a b. b -> Either a b
Right (Point a n -> Either (EmptyMfd (ZeroDim n), n) (Point a n))
-> (a n -> Point a n)
-> a n
-> Either (EmptyMfd (ZeroDim n), n) (Point a n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a n -> Point a n
forall (f :: * -> *) a. f a -> Point f a
LinAff.P (a n -> Either (EmptyMfd (ZeroDim n), n) (Point a n))
-> a n -> Either (EmptyMfd (ZeroDim n), n) (Point a n)
forall a b. (a -> b) -> a -> b
$ a n
pa n -> a n -> a n
forall v. AdditiveGroup v => v -> v -> v
^+^a n
Needle (Interior (Point a n))
v
  fromInterior :: Interior (Point a n) -> Point a n
fromInterior = Interior (Point a n) -> Point a n
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
pa n -> a n -> a n
forall 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 = SmfdWBoundWitness (Tensor s v w)
forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
  fromInterior :: Interior (Tensor s v w) -> Tensor s v w
fromInterior = Interior (Tensor s v w) -> Tensor s v w
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 = Tensor s v w
-> Either (Boundary (Tensor s v w)) (Interior (Tensor s v w))
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 = Tensor s v w -> Either (EmptyMfd (ZeroDim s), s) (Tensor s v w)
forall a b. b -> Either a b
Right (Tensor s v w -> Either (EmptyMfd (ZeroDim s), s) (Tensor s v w))
-> Tensor s v w -> Either (EmptyMfd (ZeroDim s), s) (Tensor s v w)
forall a b. (a -> b) -> a -> b
$ Tensor s v w
aTensor s v w -> Tensor s v w -> Tensor s v w
forall v. AdditiveGroup v => v -> v -> v
^+^Tensor s v w
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))
_ = Maybe (Boundary (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))
(.--!) = 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 = SmfdWBoundWitness (LinearMap s v w)
forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
  fromInterior :: Interior (LinearMap s v w) -> LinearMap s v w
fromInterior = Interior (LinearMap s v w) -> LinearMap s v w
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 = LinearMap s v w
-> Either (Boundary (LinearMap s v w)) (Interior (LinearMap s v w))
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 = LinearMap s v w
-> Either (EmptyMfd (ZeroDim s), s) (LinearMap s v w)
forall a b. b -> Either a b
Right (LinearMap s v w
 -> Either (EmptyMfd (ZeroDim s), s) (LinearMap s v w))
-> LinearMap s v w
-> Either (EmptyMfd (ZeroDim s), s) (LinearMap s v w)
forall a b. (a -> b) -> a -> b
$ LinearMap s v w
aLinearMap s v w -> LinearMap s v w -> LinearMap s v w
forall v. AdditiveGroup v => v -> v -> v
^+^LinearMap s v w
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))
_ = Maybe (Boundary (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))
(.--!) = 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 = SmfdWBoundWitness (LinearFunction s v w)
forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
  fromInterior :: Interior (LinearFunction s v w) -> LinearFunction s v w
fromInterior = Interior (LinearFunction s v w) -> LinearFunction s v w
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 = LinearFunction s v w
-> Either
     (Boundary (LinearFunction s v w)) (Interior (LinearFunction s v w))
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 = LinearFunction s v w
-> Either (EmptyMfd (ZeroDim s), s) (LinearFunction s v w)
forall a b. b -> Either a b
Right (LinearFunction s v w
 -> Either (EmptyMfd (ZeroDim s), s) (LinearFunction s v w))
-> LinearFunction s v w
-> Either (EmptyMfd (ZeroDim s), s) (LinearFunction s v w)
forall a b. (a -> b) -> a -> b
$ LinearFunction s v w
aLinearFunction s v w
-> LinearFunction s v w -> LinearFunction s v w
forall v. AdditiveGroup v => v -> v -> v
^+^LinearFunction s v w
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))
_ = Maybe (Boundary (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))
(.--!) = 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))
_ = Maybe (Boundary (GenericNeedle a))
forall a. Maybe a
Nothing
  smfdWBoundWitness :: SmfdWBoundWitness (GenericNeedle a)
smfdWBoundWitness = SmfdWBoundWitness (GenericNeedle a)
forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness
  needleIsOpenMfd :: (OpenManifold (Needle (Interior (GenericNeedle a))) => r) -> r
needleIsOpenMfd OpenManifold (Needle (Interior (GenericNeedle a))) => r
q = r
OpenManifold (Needle (Interior (GenericNeedle a))) => r
q
  scalarIsOpenMfd :: (OpenManifold (Scalar (Needle (Interior (GenericNeedle a)))) => r)
-> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (GenericNeedle a)))) => r
q = r
OpenManifold (Scalar (Needle (Interior (GenericNeedle a)))) => r
q
  boundaryHasSameScalar :: ((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 = r
(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 = GenericNeedle a
-> Either
     (EmptyMfd (ZeroDim (Scalar (Needle (VRep a)))),
      Scalar (Needle (VRep a)))
     (GenericNeedle a)
forall a b. b -> Either a b
Right (GenericNeedle a
 -> Either
      (EmptyMfd (ZeroDim (Scalar (Needle (VRep a)))),
       Scalar (Needle (VRep a)))
      (GenericNeedle a))
-> GenericNeedle a
-> Either
     (EmptyMfd (ZeroDim (Scalar (Needle (VRep a)))),
      Scalar (Needle (VRep a)))
     (GenericNeedle a)
forall a b. (a -> b) -> a -> b
$ GenericNeedle a
pGenericNeedle a -> GenericNeedle a -> GenericNeedle a
forall v. AdditiveGroup v => v -> v -> v
^+^Needle (Interior (GenericNeedle a))
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))
(.--!) = GenericNeedle a
-> GenericNeedle a -> Needle (Interior (GenericNeedle a))
forall v. AdditiveGroup v => v -> v -> v
(^-^)