-- |
-- Module      : Data.Manifold.WithBoundary.Class
-- Copyright   : (c) Justus Sagemüller 2021
-- 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 RankNTypes               #-}
{-# LANGUAGE EmptyCase                #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE TypeInType               #-}
{-# LANGUAGE CPP                      #-}


module Data.Manifold.WithBoundary.Class where

import Data.VectorSpace
import Data.AffineSpace
import Data.Basis

import Math.Manifold.Core.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'
                               )
import Math.VectorSpace.Dual
import Math.VectorSpace.MiscUtil.MultiConstraints (SameScalar)
import Linear (V0, V1, V2, V3, V4)
import qualified Linear.Affine as LinAff
import Data.Monoid.Additive

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)


type OpenManifold m = ( SemimanifoldWithBoundary m
                      , SemimanifoldWithBoundary (Needle m)
                      , LinearSpace (Needle m)
                      , SemimanifoldWithBoundary (Scalar (Needle m))
                      , Interior m ~ m
                      , Empty (Boundary m)
                      )

data SmfdWBoundWitness m where
  OpenManifoldWitness :: ∀ m . OpenManifold m
              => SmfdWBoundWitness m
  SmfdWBoundWitness :: ∀ m .
         ( OpenManifold (Interior m), OpenManifold (Boundary m)
         , FullSubspace (HalfNeedle m) ~ Needle (Boundary m) )
              => SmfdWBoundWitness m

-- | The class of spaces with a displacement operation like 'Semimanifold', but there
--   may be a limited range how far it is possible to move before leaving the space.
-- 
--   Such spaces decompose into two 'Semimanifold' spaces: the 'Interior' and the 'Boundary'.
class -- ( Semimanifold (Interior m), Semimanifold (Boundary m)
      -- , HalfSpace (HalfNeedle m) ) =>
    SemimanifoldWithBoundary m where
  -- | Subspace of @m@ representing the set of points where it is possible to move at
  --   least a small distance in any direction (with '.+^|') without leaving @m@.
  type Interior m :: Type
  -- | The set of points where an infinitesimal movement is sufficient to leave @m@.
  type Boundary m :: Type
  type HalfNeedle m :: Type
  -- | Boundary-aware pendant to '.+~^'.
  (.+^|) :: m
         -- ^ Starting point @p@
         -> Needle (Interior m)
         -- ^ Displacement @v@
         -> Either (Boundary m, Scalar (Needle (Interior m)))
                   (Interior m)
         -- ^ If @v@ is enough to leave @m@, yield the point where it does and what
         --   fraction of the length is still left (i.e. how much of @v@ “pokes out
         --   of the space”). If it stays within the space, just give back the result.
  fromInterior :: Interior m -> m
  fromBoundary :: Boundary m -> m
  (|+^) :: Boundary m -> HalfNeedle m -> m
  separateInterior :: m -> Either (Boundary m) (Interior m)
  separateInterior m
p = case SemimanifoldWithBoundary m => SmfdWBoundWitness m
forall m. SemimanifoldWithBoundary m => SmfdWBoundWitness m
smfdWBoundWitness @m of
   SmfdWBoundWitness m
OpenManifoldWitness -> m -> Either (Boundary m) m
forall a b. b -> Either a b
Right m
p
   SmfdWBoundWitness m
SmfdWBoundWitness -> case m
p m
-> Needle (Interior m)
-> Either (Boundary m, Scalar (Needle (Interior m))) (Interior m)
forall m.
SemimanifoldWithBoundary m =>
m
-> Needle (Interior m)
-> Either (Boundary m, Scalar (Needle (Interior m))) (Interior m)
.+^| Needle (Interior m)
forall v. AdditiveGroup v => v
zeroV of
    Left (Boundary m
b,Scalar (Needle (Interior m))
_) -> Boundary m -> Either (Boundary m) (Interior m)
forall a b. a -> Either a b
Left Boundary m
b 
    Right Interior m
i -> Interior m -> Either (Boundary m) (Interior m)
forall a b. b -> Either a b
Right Interior m
i
  toInterior :: m -> Maybe (Interior m)
  toInterior m
p = case m -> Either (Boundary m) (Interior m)
forall m.
SemimanifoldWithBoundary m =>
m -> Either (Boundary m) (Interior m)
separateInterior m
p of
    Right Interior m
i -> Interior m -> Maybe (Interior m)
forall a. a -> Maybe a
Just Interior m
i
    Left Boundary m
_  -> Maybe (Interior m)
forall a. Maybe a
Nothing
  extendToBoundary :: Interior m -> Needle (Interior m) -> Maybe (Boundary m)
  default extendToBoundary :: ( VectorSpace (Needle (Interior m))
                              , Num (Scalar (Needle (Interior m))) )
           => Interior m -> Needle (Interior m) -> Maybe (Boundary m)
  extendToBoundary Interior m
p Needle (Interior m)
dir = case Interior m -> m
forall m. SemimanifoldWithBoundary m => Interior m -> m
fromInterior @m Interior m
p m
-> Needle (Interior m)
-> Either (Boundary m, Scalar (Needle (Interior m))) (Interior m)
forall m.
SemimanifoldWithBoundary m =>
m
-> Needle (Interior m)
-> Either (Boundary m, Scalar (Needle (Interior m))) (Interior m)
.+^| Needle (Interior m)
dir of
    Right Interior m
_ -> Interior m -> Needle (Interior m) -> Maybe (Boundary m)
forall m.
SemimanifoldWithBoundary m =>
Interior m -> Needle (Interior m) -> Maybe (Boundary m)
extendToBoundary @m Interior m
p (Needle (Interior m) -> Maybe (Boundary m))
-> Needle (Interior m) -> Maybe (Boundary m)
forall a b. (a -> b) -> a -> b
$ Needle (Interior m)
dirNeedle (Interior m)
-> Scalar (Needle (Interior m)) -> Needle (Interior m)
forall v s. (VectorSpace v, s ~ Scalar v) => v -> s -> v
^*Scalar (Needle (Interior m))
2
    Left (Boundary m
p, Scalar (Needle (Interior m))
_) -> Boundary m -> Maybe (Boundary m)
forall a. a -> Maybe a
Just Boundary m
p
  smfdWBoundWitness :: SmfdWBoundWitness m
  default smfdWBoundWitness 
              :: ( OpenManifold (Interior m)
                 , OpenManifold (Boundary m)
                 , FullSubspace (HalfNeedle m) ~ Needle (Boundary m) )
                   => SmfdWBoundWitness m
  smfdWBoundWitness = (OpenManifold (Interior m), OpenManifold (Boundary m),
 FullSubspace (HalfNeedle m) ~ Needle (Boundary m)) =>
SmfdWBoundWitness m
forall m.
(OpenManifold (Interior m), OpenManifold (Boundary m),
 FullSubspace (HalfNeedle m) ~ Needle (Boundary m)) =>
SmfdWBoundWitness m
SmfdWBoundWitness @m
  needleIsOpenMfd :: (OpenManifold (Needle (Interior m)) => r) -> r
  default needleIsOpenMfd :: OpenManifold (Needle (Interior m))
                                 => (OpenManifold (Needle (Interior m)) => r) -> r
  needleIsOpenMfd OpenManifold (Needle (Interior m)) => r
q = r
OpenManifold (Needle (Interior m)) => r
q
  scalarIsOpenMfd :: (OpenManifold (Scalar (Needle (Interior m))) => r) -> r
  default scalarIsOpenMfd :: OpenManifold (Scalar (Needle (Interior m)))
                                 => (OpenManifold (Scalar (Needle (Interior m))) => r) -> r
  scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior m))) => r
q = r
OpenManifold (Scalar (Needle (Interior m))) => r
q
  boundaryHasSameScalar
        :: ( ( LinearSpace (Needle (Boundary m))
             , Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m)) )
                                => r)-> r
  default boundaryHasSameScalar
           :: (( LinearSpace (Needle (Boundary m))
               , Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))))
     => (( LinearSpace (Needle (Boundary m))
         , Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) => r) -> r
  boundaryHasSameScalar (LinearSpace (Needle (Boundary m)),
 Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r
q = r
(LinearSpace (Needle (Boundary m)),
 Scalar (Needle (Boundary m)) ~ Scalar (Needle (Interior m))) =>
r
q
  

class (SemimanifoldWithBoundary m, PseudoAffine (Interior m), PseudoAffine (Boundary m))
          => PseudoAffineWithBoundary m where
  -- | Inverse of '.+^|', provided the space is connected. For @p :: Interior m@, @q :: m@
  --   and @v = fromInterior p.--!q@,
  -- 
  --   @
  --   q '.+^|' v ≡ Right p
  --   @
  --
  --   (up to floating-point). Similary, for @b :: Boundary m@ and @w = fromBoundary m.--!q@,
  -- 
  --   @
  --   q '.+^|' w ≡ Left (b, 0)
  --   @
  (.--!) :: m -> m -> Needle (Interior m)
  
  (.-|) :: m -> Boundary m -> Maybe (HalfNeedle m)
  m
p.-|Boundary m
b = HalfNeedle m -> Maybe (HalfNeedle m)
forall a. a -> Maybe a
Just (HalfNeedle m -> Maybe (HalfNeedle m))
-> HalfNeedle m -> Maybe (HalfNeedle m)
forall a b. (a -> b) -> a -> b
$ m
pm -> Boundary m -> HalfNeedle m
forall m.
PseudoAffineWithBoundary m =>
m -> Boundary m -> HalfNeedle m
!-|Boundary m
b
  (!-|) :: m -> Boundary m -> HalfNeedle m
  (.--.) :: m -> m -> Maybe (Needle (Interior m))
  m
p.--.m
q = Needle (Interior m) -> Maybe (Needle (Interior m))
forall a. a -> Maybe a
Just (Needle (Interior m) -> Maybe (Needle (Interior m)))
-> Needle (Interior m) -> Maybe (Needle (Interior m))
forall a b. (a -> b) -> a -> b
$ m
pm -> m -> Needle (Interior m)
forall m.
PseudoAffineWithBoundary m =>
m -> m -> Needle (Interior m)
.--!m
q


class PseudoAffineWithBoundary m => ProjectableBoundary m where
  projectToBoundary :: m
                    -- ^ Point @p@ to project
                    -> Boundary m 
                    -- ^ Intended “course region” representative @r@ on boundary – we
                    --   seek a point that is reachable from there.
                    -> Maybe ( Needle (Boundary m)
                             , Scalar (Needle (Interior m)) )
                    -- ^ Needle @δr@ connecting @r@ to projection of the @p@, and
                    --   a measure @d@ of normal-distance such that
                    --   @'marginFromBoundary' (r.+~^δr) d == p@.
  marginFromBoundary :: Boundary m -> Scalar (Needle (Interior m)) -> m
  needleBoundaryIsTriviallyProjectible :: ∀ r .
        (ProjectableBoundary (Needle (Interior m)) => r) -> r
  default needleBoundaryIsTriviallyProjectible :: ProjectableBoundary (Needle (Interior m))
           => (ProjectableBoundary (Needle (Interior m)) => r) -> r
  needleBoundaryIsTriviallyProjectible ProjectableBoundary (Needle (Interior m)) => r
q = r
ProjectableBoundary (Needle (Interior m)) => r
q
  scalarBoundaryIsTriviallyProjectible :: ∀ r .
        (ProjectableBoundary (Scalar (Needle (Interior m))) => r) -> r
  default scalarBoundaryIsTriviallyProjectible
                      :: ProjectableBoundary (Scalar (Needle (Interior m)))
           => (ProjectableBoundary (Scalar (Needle (Interior m))) => r) -> r
  scalarBoundaryIsTriviallyProjectible ProjectableBoundary (Scalar (Needle (Interior m))) => r
q = r
ProjectableBoundary (Scalar (Needle (Interior m))) => r
q

instance ∀ k . ( LinearSpace k, OpenManifold k, OpenManifold (Scalar k) )
             => SemimanifoldWithBoundary (EmptyMfd k) where
  type Interior (EmptyMfd k) = EmptyMfd k
  type Boundary (EmptyMfd k) = EmptyMfd k
  type HalfNeedle (EmptyMfd k) = ZeroDim (Scalar k)
  smfdWBoundWitness :: SmfdWBoundWitness (EmptyMfd k)
smfdWBoundWitness = OpenManifold (EmptyMfd k) => SmfdWBoundWitness (EmptyMfd k)
forall m. OpenManifold m => SmfdWBoundWitness m
OpenManifoldWitness @(EmptyMfd k)
  Boundary (EmptyMfd k)
q|+^ :: Boundary (EmptyMfd k) -> HalfNeedle (EmptyMfd k) -> EmptyMfd k
|+^HalfNeedle (EmptyMfd k)
_ = case Boundary (EmptyMfd k)
q of {}
  EmptyMfd k
q.+^| :: EmptyMfd k
-> Needle (Interior (EmptyMfd k))
-> Either
     (Boundary (EmptyMfd k), Scalar (Needle (Interior (EmptyMfd k))))
     (Interior (EmptyMfd k))
.+^|Needle (Interior (EmptyMfd k))
_ = case EmptyMfd k
q of {}
  fromInterior :: Interior (EmptyMfd k) -> EmptyMfd k
fromInterior = Interior (EmptyMfd k) -> EmptyMfd k
forall a. a -> a
id
  fromBoundary :: Boundary (EmptyMfd k) -> EmptyMfd k
fromBoundary = Boundary (EmptyMfd k) -> EmptyMfd k
forall a. a -> a
id
  scalarIsOpenMfd :: (OpenManifold (Scalar (Needle (Interior (EmptyMfd k)))) => r) -> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (EmptyMfd k)))) => r
q = (OpenManifold (Scalar (Needle (Interior k))) => r) -> r
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Scalar (Needle (Interior m))) => r) -> r
scalarIsOpenMfd @k OpenManifold (Scalar (Needle (Interior k))) => r
OpenManifold (Scalar (Needle (Interior (EmptyMfd k)))) => r
q

instance ∀ k . (Num' k, OpenManifold k)
            => SemimanifoldWithBoundary (ZeroDim k) where
  type Interior (ZeroDim k) = ZeroDim k
  type Boundary (ZeroDim k) = EmptyMfd (ZeroDim k)
  type HalfNeedle (ZeroDim k) = ZeroDim k
  fromInterior :: Interior (ZeroDim k) -> ZeroDim k
fromInterior = Interior (ZeroDim k) -> ZeroDim k
forall a. a -> a
id
  fromBoundary :: Boundary (ZeroDim k) -> ZeroDim k
fromBoundary Boundary (ZeroDim k)
b = case Boundary (ZeroDim k)
b of {}
  separateInterior :: ZeroDim k -> Either (Boundary (ZeroDim k)) (Interior (ZeroDim k))
separateInterior = ZeroDim k -> Either (Boundary (ZeroDim k)) (Interior (ZeroDim k))
forall a b. b -> Either a b
Right
  Boundary (ZeroDim k)
p|+^ :: Boundary (ZeroDim k) -> HalfNeedle (ZeroDim k) -> ZeroDim k
|+^HalfNeedle (ZeroDim k)
_ = case Boundary (ZeroDim k)
p of {}
  ZeroDim k
Origin .+^| :: ZeroDim k
-> Needle (Interior (ZeroDim k))
-> Either
     (Boundary (ZeroDim k), Scalar (Needle (Interior (ZeroDim k))))
     (Interior (ZeroDim k))
.+^| Needle (Interior (ZeroDim k))
Origin = ZeroDim k -> Either (EmptyMfd (ZeroDim k), k) (ZeroDim k)
forall a b. b -> Either a b
Right ZeroDim k
forall s. ZeroDim s
Origin
  extendToBoundary :: Interior (ZeroDim k)
-> Needle (Interior (ZeroDim k)) -> Maybe (Boundary (ZeroDim k))
extendToBoundary Interior (ZeroDim k)
_ Needle (Interior (ZeroDim k))
_ = Maybe (Boundary (ZeroDim k))
forall a. Maybe a
Nothing
  smfdWBoundWitness :: SmfdWBoundWitness (ZeroDim k)
smfdWBoundWitness = (OpenManifold (Scalar (Needle (Interior k))) =>
 SmfdWBoundWitness (ZeroDim k))
-> SmfdWBoundWitness (ZeroDim k)
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Scalar (Needle (Interior m))) => r) -> r
scalarIsOpenMfd @k OpenManifold (Scalar (Needle (Interior k))) =>
SmfdWBoundWitness (ZeroDim k)
forall m.
(OpenManifold (Interior m), OpenManifold (Boundary m),
 FullSubspace (HalfNeedle m) ~ Needle (Boundary m)) =>
SmfdWBoundWitness m
SmfdWBoundWitness
  scalarIsOpenMfd :: (OpenManifold (Scalar (Needle (Interior (ZeroDim k)))) => r) -> r
scalarIsOpenMfd OpenManifold (Scalar (Needle (Interior (ZeroDim k)))) => r
q = (OpenManifold (Scalar (Needle (Interior k))) => r) -> r
forall m r.
SemimanifoldWithBoundary m =>
(OpenManifold (Scalar (Needle (Interior m))) => r) -> r
scalarIsOpenMfd @k OpenManifold (Scalar (Needle (Interior k))) => r
OpenManifold (Scalar (Needle (Interior (ZeroDim k)))) => r
q

instance (Num' k, OpenManifold k) => PseudoAffineWithBoundary (ZeroDim k) where
  ZeroDim k
_.-| :: ZeroDim k -> Boundary (ZeroDim k) -> Maybe (HalfNeedle (ZeroDim k))
.-|Boundary (ZeroDim k)
p = case Boundary (ZeroDim k)
p of {}
  ZeroDim k
Origin .--! :: ZeroDim k -> ZeroDim k -> Needle (Interior (ZeroDim k))
.--! ZeroDim k
Origin = Needle (Interior (ZeroDim k))
forall s. ZeroDim s
Origin
  ZeroDim k
_!-| :: ZeroDim k -> Boundary (ZeroDim k) -> HalfNeedle (ZeroDim k)
!-|Boundary (ZeroDim k)
q = case Boundary (ZeroDim k)
q of {}

instance (Num' k, ProjectableBoundary k, OpenManifold k)
            => ProjectableBoundary (ZeroDim k) where
  projectToBoundary :: ZeroDim k
-> Boundary (ZeroDim k)
-> Maybe
     (Needle (Boundary (ZeroDim k)),
      Scalar (Needle (Interior (ZeroDim k))))
projectToBoundary ZeroDim k
Origin Boundary (ZeroDim k)
b = case Boundary (ZeroDim k)
b of {}
  marginFromBoundary :: Boundary (ZeroDim k)
-> Scalar (Needle (Interior (ZeroDim k))) -> ZeroDim k
marginFromBoundary Boundary (ZeroDim k)
b Scalar (Needle (Interior (ZeroDim k)))
_ = case Boundary (ZeroDim k)
b of {}