-- |
-- Module      : Math.Manifold.Core.Types.Internal
-- Copyright   : (c) Justus Sagemüller 2018
-- License     : GPL v3
-- 
-- Maintainer  : (@) jsagemue $ uni-koeln.de
-- Stability   : experimental
-- Portability : portable
-- 
-- Several low-dimensional manifolds, represented in some simple way as Haskell
-- data types. All these are in the 'PseudoAffine' class.
-- 
{-# LANGUAGE DeriveGeneric    #-}
{-# LANGUAGE EmptyCase        #-}


module Math.Manifold.Core.Types.Internal where

import Math.Manifold.VectorSpace.ZeroDimensional

import Data.Fixed (mod')

import Proof.Propositional (Empty(..))

import GHC.Generics


-- | The empty space can be considered a manifold with any sort of tangent space.
data EmptyMfd v

instance Empty (EmptyMfd v) where
  eliminate :: EmptyMfd v -> x
eliminate EmptyMfd v
p = case EmptyMfd v
p of {}
instance Eq (EmptyMfd v) where
  EmptyMfd v
p== :: EmptyMfd v -> EmptyMfd v -> Bool
==EmptyMfd v
q = EmptyMfd v -> Bool
forall a x. Empty a => a -> x
eliminate EmptyMfd v
p Bool -> Bool -> Bool
&& EmptyMfd v -> Bool
forall a x. Empty a => a -> x
eliminate EmptyMfd v
q
instance Ord (EmptyMfd v) where
  EmptyMfd v
p< :: EmptyMfd v -> EmptyMfd v -> Bool
<EmptyMfd v
q = EmptyMfd v -> Bool
forall a x. Empty a => a -> x
eliminate EmptyMfd v
p Bool -> Bool -> Bool
&& EmptyMfd v -> Bool
forall a x. Empty a => a -> x
eliminate EmptyMfd v
q
  EmptyMfd v
p<= :: EmptyMfd v -> EmptyMfd v -> Bool
<=EmptyMfd v
q = EmptyMfd v -> Bool
forall a x. Empty a => a -> x
eliminate EmptyMfd v
p Bool -> Bool -> Bool
&& EmptyMfd v -> Bool
forall a x. Empty a => a -> x
eliminate EmptyMfd v
q

-- | The zero-dimensional sphere is actually just two points. Implementation might
--   therefore change to @ℝ⁰ 'Control.Category.Constrained.+' ℝ⁰@: the disjoint sum of two
--   single-point spaces.
type S⁰ = S⁰_ Double

data S⁰_ r = PositiveHalfSphere | NegativeHalfSphere deriving(S⁰_ r -> S⁰_ r -> Bool
(S⁰_ r -> S⁰_ r -> Bool) -> (S⁰_ r -> S⁰_ r -> Bool) -> Eq (S⁰_ r)
forall r. S⁰_ r -> S⁰_ r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: S⁰_ r -> S⁰_ r -> Bool
$c/= :: forall r. S⁰_ r -> S⁰_ r -> Bool
== :: S⁰_ r -> S⁰_ r -> Bool
$c== :: forall r. S⁰_ r -> S⁰_ r -> Bool
Eq, Int -> S⁰_ r -> ShowS
[S⁰_ r] -> ShowS
S⁰_ r -> String
(Int -> S⁰_ r -> ShowS)
-> (S⁰_ r -> String) -> ([S⁰_ r] -> ShowS) -> Show (S⁰_ r)
forall r. Int -> S⁰_ r -> ShowS
forall r. [S⁰_ r] -> ShowS
forall r. S⁰_ r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [S⁰_ r] -> ShowS
$cshowList :: forall r. [S⁰_ r] -> ShowS
show :: S⁰_ r -> String
$cshow :: forall r. S⁰_ r -> String
showsPrec :: Int -> S⁰_ r -> ShowS
$cshowsPrec :: forall r. Int -> S⁰_ r -> ShowS
Show, (forall x. S⁰_ r -> Rep (S⁰_ r) x)
-> (forall x. Rep (S⁰_ r) x -> S⁰_ r) -> Generic (S⁰_ r)
forall x. Rep (S⁰_ r) x -> S⁰_ r
forall x. S⁰_ r -> Rep (S⁰_ r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall r x. Rep (S⁰_ r) x -> S⁰_ r
forall r x. S⁰_ r -> Rep (S⁰_ r) x
$cto :: forall r x. Rep (S⁰_ r) x -> S⁰_ r
$cfrom :: forall r x. S⁰_ r -> Rep (S⁰_ r) x
Generic)

type ℝP⁰ = ℝP⁰_ Double
data ℝP⁰_ r = ℝPZero deriving (ℝP⁰_ r -> ℝP⁰_ r -> Bool
(ℝP⁰_ r -> ℝP⁰_ r -> Bool)
-> (ℝP⁰_ r -> ℝP⁰_ r -> Bool) -> Eq (ℝP⁰_ r)
forall r. ℝP⁰_ r -> ℝP⁰_ r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ℝP⁰_ r -> ℝP⁰_ r -> Bool
$c/= :: forall r. ℝP⁰_ r -> ℝP⁰_ r -> Bool
== :: ℝP⁰_ r -> ℝP⁰_ r -> Bool
$c== :: forall r. ℝP⁰_ r -> ℝP⁰_ r -> Bool
Eq, Int -> ℝP⁰_ r -> ShowS
[ℝP⁰_ r] -> ShowS
ℝP⁰_ r -> String
(Int -> ℝP⁰_ r -> ShowS)
-> (ℝP⁰_ r -> String) -> ([ℝP⁰_ r] -> ShowS) -> Show (ℝP⁰_ r)
forall r. Int -> ℝP⁰_ r -> ShowS
forall r. [ℝP⁰_ r] -> ShowS
forall r. ℝP⁰_ r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ℝP⁰_ r] -> ShowS
$cshowList :: forall r. [ℝP⁰_ r] -> ShowS
show :: ℝP⁰_ r -> String
$cshow :: forall r. ℝP⁰_ r -> String
showsPrec :: Int -> ℝP⁰_ r -> ShowS
$cshowsPrec :: forall r. Int -> ℝP⁰_ r -> ShowS
Show, (forall x. ℝP⁰_ r -> Rep (ℝP⁰_ r) x)
-> (forall x. Rep (ℝP⁰_ r) x -> ℝP⁰_ r) -> Generic (ℝP⁰_ r)
forall x. Rep (ℝP⁰_ r) x -> ℝP⁰_ r
forall x. ℝP⁰_ r -> Rep (ℝP⁰_ r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall r x. Rep (ℝP⁰_ r) x -> ℝP⁰_ r
forall r x. ℝP⁰_ r -> Rep (ℝP⁰_ r) x
$cto :: forall r x. Rep (ℝP⁰_ r) x -> ℝP⁰_ r
$cfrom :: forall r x. ℝP⁰_ r -> Rep (ℝP⁰_ r) x
Generic)

-- | The unit circle.
type S¹ = S¹_ Double

newtype S¹_ r = S¹Polar { S¹_ r -> r
φParamS¹ :: r -- ^ Must be in range @[-π, π[@.
                        } deriving (Int -> S¹_ r -> ShowS
[S¹_ r] -> ShowS
S¹_ r -> String
(Int -> S¹_ r -> ShowS)
-> (S¹_ r -> String) -> ([S¹_ r] -> ShowS) -> Show (S¹_ r)
forall r. Show r => Int -> S¹_ r -> ShowS
forall r. Show r => [S¹_ r] -> ShowS
forall r. Show r => S¹_ r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [S¹_ r] -> ShowS
$cshowList :: forall r. Show r => [S¹_ r] -> ShowS
show :: S¹_ r -> String
$cshow :: forall r. Show r => S¹_ r -> String
showsPrec :: Int -> S¹_ r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> S¹_ r -> ShowS
Show, (forall x. S¹_ r -> Rep (S¹_ r) x)
-> (forall x. Rep (S¹_ r) x -> S¹_ r) -> Generic (S¹_ r)
forall x. Rep (S¹_ r) x -> S¹_ r
forall x. S¹_ r -> Rep (S¹_ r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall r x. Rep (S¹_ r) x -> S¹_ r
forall r x. S¹_ r -> Rep (S¹_ r) x
$cto :: forall r x. Rep (S¹_ r) x -> S¹_ r
$cfrom :: forall r x. S¹_ r -> Rep (S¹_ r) x
Generic)

instance (Eq r, RealFloat r) => Eq (S¹_ r) where
  S¹Polar r
φ == :: S¹_ r -> S¹_ r -> Bool
== S¹Polar r
φ' = r
φ r -> r -> r
forall a. Real a => a -> a -> a
`mod'` (r
2r -> r -> r
forall a. Num a => a -> a -> a
*r
forall a. Floating a => a
pi) r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
φ' r -> r -> r
forall a. Real a => a -> a -> a
`mod'` (r
2r -> r -> r
forall a. Num a => a -> a -> a
*r
forall a. Floating a => a
pi)
     -- It's not clear that it's actually a good idea to fold back the range here,
     -- since values outside @[-π, π[@ should not be allowed in the first place.


type ℝP¹ = ℝP¹_ Double
newtype ℝP¹_ r = HemisphereℝP¹Polar { ℝP¹_ r -> r
φParamℝP¹ :: r -- ^ Range @[-π\/2,π\/2[@.
                                    } deriving (Int -> ℝP¹_ r -> ShowS
[ℝP¹_ r] -> ShowS
ℝP¹_ r -> String
(Int -> ℝP¹_ r -> ShowS)
-> (ℝP¹_ r -> String) -> ([ℝP¹_ r] -> ShowS) -> Show (ℝP¹_ r)
forall r. Show r => Int -> ℝP¹_ r -> ShowS
forall r. Show r => [ℝP¹_ r] -> ShowS
forall r. Show r => ℝP¹_ r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ℝP¹_ r] -> ShowS
$cshowList :: forall r. Show r => [ℝP¹_ r] -> ShowS
show :: ℝP¹_ r -> String
$cshow :: forall r. Show r => ℝP¹_ r -> String
showsPrec :: Int -> ℝP¹_ r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> ℝP¹_ r -> ShowS
Show, (forall x. ℝP¹_ r -> Rep (ℝP¹_ r) x)
-> (forall x. Rep (ℝP¹_ r) x -> ℝP¹_ r) -> Generic (ℝP¹_ r)
forall x. Rep (ℝP¹_ r) x -> ℝP¹_ r
forall x. ℝP¹_ r -> Rep (ℝP¹_ r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall r x. Rep (ℝP¹_ r) x -> ℝP¹_ r
forall r x. ℝP¹_ r -> Rep (ℝP¹_ r) x
$cto :: forall r x. Rep (ℝP¹_ r) x -> ℝP¹_ r
$cfrom :: forall r x. ℝP¹_ r -> Rep (ℝP¹_ r) x
Generic)

-- | The ordinary unit sphere.
type S² = S²_ Double
data S²_ r = S²Polar { S²_ r -> r
ϑParamS² :: !r -- ^ Range @[0, π[@.
                     , S²_ r -> r
φParamS² :: !r -- ^ Range @[-π, π[@.
                     } deriving (Int -> S²_ r -> ShowS
[S²_ r] -> ShowS
S²_ r -> String
(Int -> S²_ r -> ShowS)
-> (S²_ r -> String) -> ([S²_ r] -> ShowS) -> Show (S²_ r)
forall r. Show r => Int -> S²_ r -> ShowS
forall r. Show r => [S²_ r] -> ShowS
forall r. Show r => S²_ r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [S²_ r] -> ShowS
$cshowList :: forall r. Show r => [S²_ r] -> ShowS
show :: S²_ r -> String
$cshow :: forall r. Show r => S²_ r -> String
showsPrec :: Int -> S²_ r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> S²_ r -> ShowS
Show, (forall x. S²_ r -> Rep (S²_ r) x)
-> (forall x. Rep (S²_ r) x -> S²_ r) -> Generic (S²_ r)
forall x. Rep (S²_ r) x -> S²_ r
forall x. S²_ r -> Rep (S²_ r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall r x. Rep (S²_ r) x -> S²_ r
forall r x. S²_ r -> Rep (S²_ r) x
$cto :: forall r x. Rep (S²_ r) x -> S²_ r
$cfrom :: forall r x. S²_ r -> Rep (S²_ r) x
Generic)

instance (Eq r, RealFloat r) => Eq (S²_ r) where
  S²Polar r
θ r
φ == :: S²_ r -> S²_ r -> Bool
== S²Polar r
θ' r
φ'
   | r
θ r -> r -> Bool
forall a. Ord a => a -> a -> Bool
> r
0, r
θ r -> r -> Bool
forall a. Ord a => a -> a -> Bool
< r
forall a. Floating a => a
pi  = r
θ r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
θ' Bool -> Bool -> Bool
&& r
φ r -> r -> r
forall a. Real a => a -> a -> a
`mod'` (r
2r -> r -> r
forall a. Num a => a -> a -> a
*r
forall a. Floating a => a
pi) r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
φ' r -> r -> r
forall a. Real a => a -> a -> a
`mod'` (r
2r -> r -> r
forall a. Num a => a -> a -> a
*r
forall a. Floating a => a
pi)
   | Bool
otherwise      = r
θ r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
θ'

-- | The two-dimensional real projective space, implemented as a disk with
--   opposing points on the rim glued together. Image this disk as the northern hemisphere
--   of a unit sphere; 'ℝP²' is the space of all straight lines passing through
--   the origin of 'ℝ³', and each of these lines is represented by the point at which it
--   passes through the hemisphere.
type ℝP² = ℝP²_ Double
data ℝP²_ r = HemisphereℝP²Polar { ℝP²_ r -> r
ϑParamℝP² :: !r -- ^ Range @[0, π/2]@.
                                 , ℝP²_ r -> r
φParamℝP² :: !r -- ^ Range @[-π, π[@.
                                 } deriving (Int -> ℝP²_ r -> ShowS
[ℝP²_ r] -> ShowS
ℝP²_ r -> String
(Int -> ℝP²_ r -> ShowS)
-> (ℝP²_ r -> String) -> ([ℝP²_ r] -> ShowS) -> Show (ℝP²_ r)
forall r. Show r => Int -> ℝP²_ r -> ShowS
forall r. Show r => [ℝP²_ r] -> ShowS
forall r. Show r => ℝP²_ r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ℝP²_ r] -> ShowS
$cshowList :: forall r. Show r => [ℝP²_ r] -> ShowS
show :: ℝP²_ r -> String
$cshow :: forall r. Show r => ℝP²_ r -> String
showsPrec :: Int -> ℝP²_ r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> ℝP²_ r -> ShowS
Show, (forall x. ℝP²_ r -> Rep (ℝP²_ r) x)
-> (forall x. Rep (ℝP²_ r) x -> ℝP²_ r) -> Generic (ℝP²_ r)
forall x. Rep (ℝP²_ r) x -> ℝP²_ r
forall x. ℝP²_ r -> Rep (ℝP²_ r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall r x. Rep (ℝP²_ r) x -> ℝP²_ r
forall r x. ℝP²_ r -> Rep (ℝP²_ r) x
$cto :: forall r x. Rep (ℝP²_ r) x -> ℝP²_ r
$cfrom :: forall r x. ℝP²_ r -> Rep (ℝP²_ r) x
Generic)


-- | The standard, closed unit disk. Homeomorphic to the cone over 'S¹', but not in the
--   the obvious, “flat” way. (In is /not/ homeomorphic, despite
--   the almost identical ADT definition, to the projective space 'ℝP²'!)
type D² = D²_ Double
data D²_ r = D²Polar { D²_ r -> r
rParamD² :: !r -- ^ Range @[0, 1]@.
                     , D²_ r -> r
φParamD² :: !r -- ^ Range @[-π, π[@.
                     } deriving (Int -> D²_ r -> ShowS
[D²_ r] -> ShowS
D²_ r -> String
(Int -> D²_ r -> ShowS)
-> (D²_ r -> String) -> ([D²_ r] -> ShowS) -> Show (D²_ r)
forall r. Show r => Int -> D²_ r -> ShowS
forall r. Show r => [D²_ r] -> ShowS
forall r. Show r => D²_ r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [D²_ r] -> ShowS
$cshowList :: forall r. Show r => [D²_ r] -> ShowS
show :: D²_ r -> String
$cshow :: forall r. Show r => D²_ r -> String
showsPrec :: Int -> D²_ r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> D²_ r -> ShowS
Show, (forall x. D²_ r -> Rep (D²_ r) x)
-> (forall x. Rep (D²_ r) x -> D²_ r) -> Generic (D²_ r)
forall x. Rep (D²_ r) x -> D²_ r
forall x. D²_ r -> Rep (D²_ r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall r x. Rep (D²_ r) x -> D²_ r
forall r x. D²_ r -> Rep (D²_ r) x
$cto :: forall r x. Rep (D²_ r) x -> D²_ r
$cfrom :: forall r x. D²_ r -> Rep (D²_ r) x
Generic)


-- | The “one-dimensional disk” – really just the line segment between
--   the two points -1 and 1 of 'S⁰', i.e. this is simply a closed interval.
type D¹ = D¹_ Double
newtype D¹_ r = D¹ { D¹_ r -> r
xParamD¹ :: r -- ^ Range @[-1, 1]@.
                   } deriving (Int -> D¹_ r -> ShowS
[D¹_ r] -> ShowS
D¹_ r -> String
(Int -> D¹_ r -> ShowS)
-> (D¹_ r -> String) -> ([D¹_ r] -> ShowS) -> Show (D¹_ r)
forall r. Show r => Int -> D¹_ r -> ShowS
forall r. Show r => [D¹_ r] -> ShowS
forall r. Show r => D¹_ r -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [D¹_ r] -> ShowS
$cshowList :: forall r. Show r => [D¹_ r] -> ShowS
show :: D¹_ r -> String
$cshow :: forall r. Show r => D¹_ r -> String
showsPrec :: Int -> D¹_ r -> ShowS
$cshowsPrec :: forall r. Show r => Int -> D¹_ r -> ShowS
Show, (forall x. D¹_ r -> Rep (D¹_ r) x)
-> (forall x. Rep (D¹_ r) x -> D¹_ r) -> Generic (D¹_ r)
forall x. Rep (D¹_ r) x -> D¹_ r
forall x. D¹_ r -> Rep (D¹_ r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall r x. Rep (D¹_ r) x -> D¹_ r
forall r x. D¹_ r -> Rep (D¹_ r) x
$cto :: forall r x. Rep (D¹_ r) x -> D¹_ r
$cfrom :: forall r x. D¹_ r -> Rep (D¹_ r) x
Generic)

type ℝ = Double
type ℝ⁰ = ZeroDim ℝ