{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}

-----------------------------------------------------------------------------
{-|
Module      : Math.Tensor.Basic.Area
Description : Definitions of area-symmetric tensors.
Copyright   : (c) Nils Alex, 2020
License     : MIT
Maintainer  : nils.alex@fau.de

Definitions of area-symmetric tensors.
-}
-----------------------------------------------------------------------------
module Math.Tensor.Basic.Area
  ( -- * Area metric tensor induced from flat Lorentzian metric
    flatAreaCon
  , someFlatAreaCon
  ,  -- * Injections from \(AS(V)\) into \(V\times V\times V\times V\)
    injAreaCon'
  , injAreaCov'
  , someInjAreaCon
  , someInjAreaCov
  , -- * Surjections from \(V\times V\times V\times V\) onto \(AS(V)\)
    surjAreaCon'
  , surjAreaCov'
  , someSurjAreaCon
  , someSurjAreaCov
  , -- * Vertical coefficients for functions on \(AS(V)\)
    someInterAreaCon
  , someInterAreaCov
  , -- * Kronecker delta on \(AS(V)\)
    someDeltaArea
  , -- * Internals
    trianMapArea
  , facMapArea
  , areaSign
  , sortArea
  ) where

import Math.Tensor
import Math.Tensor.Safe
import Math.Tensor.Safe.TH
import Math.Tensor.Basic.TH
import Math.Tensor.Basic.Delta

import Data.Singletons
  ( Sing
  , SingI (sing)
  , Demote
  , withSomeSing
  , withSingI
  )
import Data.Singletons.Prelude
import Data.Singletons.Decide
  ( (:~:) (Refl)
  , Decision (Proved)
  , (%~)
  )
import Data.Singletons.TypeLits
  ( Symbol
  , withKnownSymbol
  )

import Data.Maybe (catMaybes)
import Data.Ratio (Ratio, numerator, denominator)
import qualified Data.Map.Strict as Map
  ( Map
  , lookup
  , fromList
  )
import Data.List.NonEmpty (NonEmpty((:|)))
import Control.Monad.Except
  ( MonadError
  , runExcept
  )

trianMapArea :: Map.Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
trianMapArea :: Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
trianMapArea = [(Vec ('S ('S ('S ('S 'Z)))) Int, Int)]
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Vec ('S ('S ('S ('S 'Z)))) Int, Int)]
 -> Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int)
-> [(Vec ('S ('S ('S ('S 'Z)))) Int, Int)]
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
forall a b. (a -> b) -> a -> b
$ [Vec ('S ('S ('S ('S 'Z)))) Int]
-> [Int] -> [(Vec ('S ('S ('S ('S 'Z)))) Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Vec ('S ('S ('S ('S 'Z)))) Int]
indices4 [Int]
indices1
  where
    indices1 :: [Int]
    indices1 :: [Int]
indices1 = [Int
0..]
    indices4 :: [Vec ('S ('S ('S ('S 'Z)))) Int]
    indices4 :: [Vec ('S ('S ('S ('S 'Z)))) Int]
indices4 = [Int
a Int -> Vec ('S ('S ('S 'Z))) Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
b Int -> Vec ('S ('S 'Z)) Int -> Vec ('S ('S ('S 'Z))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
c Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
d Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil))) |
                  Int
a <- [Int
0..Int
2],
                  Int
b <- [Int
aInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..Int
3],
                  Int
c <- [Int
a..Int
2],
                  Int
d <- [Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..Int
3],
                  Bool -> Bool
not (Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c Bool -> Bool -> Bool
&& Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
d) ]

facMapArea :: forall b.Num b => Map.Map (Vec ('S ('S ('S ('S 'Z)))) Int) b
facMapArea :: Map (Vec ('S ('S ('S ('S 'Z)))) Int) b
facMapArea = [(Vec ('S ('S ('S ('S 'Z)))) Int, b)]
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) b
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Vec ('S ('S ('S ('S 'Z)))) Int, b)]
 -> Map (Vec ('S ('S ('S ('S 'Z)))) Int) b)
-> [(Vec ('S ('S ('S ('S 'Z)))) Int, b)]
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) b
forall a b. (a -> b) -> a -> b
$ [(Int
a Int -> Vec ('S ('S ('S 'Z))) Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
b Int -> Vec ('S ('S 'Z)) Int -> Vec ('S ('S ('S 'Z))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
c Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
d Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil))), Int -> Int -> Int -> Int -> b
fac Int
a Int
b Int
c Int
d) |
                                Int
a <- [Int
0..Int
2],
                                Int
b <- [Int
aInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..Int
3],
                                Int
c <- [Int
a..Int
2],
                                Int
d <- [Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1..Int
3],
                                Bool -> Bool
not (Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c Bool -> Bool -> Bool
&& Int
b Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
d)]
  where
    fac :: Int -> Int -> Int -> Int -> b
    fac :: Int -> Int -> Int -> Int -> b
fac Int
a Int
b Int
c Int
d
      | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
c Bool -> Bool -> Bool
&& Int
b Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
d = b
4
      | Bool
otherwise        = b
8

areaSign :: (Ord a, Num v) => a -> a -> a -> a -> Maybe v
areaSign :: a -> a -> a -> a -> Maybe v
areaSign a
a a
b a
c a
d
  | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b = Maybe v
forall a. Maybe a
Nothing
  | a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
d = Maybe v
forall a. Maybe a
Nothing
  | a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
b  = ((-v
1) v -> v -> v
forall a. Num a => a -> a -> a
*) (v -> v) -> Maybe v -> Maybe v
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> a -> a -> Maybe v
forall a v. (Ord a, Num v) => a -> a -> a -> a -> Maybe v
areaSign a
b a
a a
c a
d
  | a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
d  = ((-v
1) v -> v -> v
forall a. Num a => a -> a -> a
*) (v -> v) -> Maybe v -> Maybe v
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> a -> a -> Maybe v
forall a v. (Ord a, Num v) => a -> a -> a -> a -> Maybe v
areaSign a
a a
b a
d a
c
  | Bool
otherwise = v -> Maybe v
forall a. a -> Maybe a
Just v
1

sortArea :: Ord a => a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
sortArea :: a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
sortArea a
a a
b a
c a
d
  | a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
b = a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
forall a. Ord a => a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
sortArea a
b a
a a
c a
d
  | a
c a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
d = a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
forall a. Ord a => a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
sortArea a
a a
b a
d a
c
  | (a
a,a
b) (a, a) -> (a, a) -> Bool
forall a. Ord a => a -> a -> Bool
> (a
c,a
d) = a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
forall a. Ord a => a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
sortArea a
c a
d a
a a
b
  | Bool
otherwise = a
a a -> Vec ('S ('S ('S 'Z))) a -> Vec ('S ('S ('S ('S 'Z)))) a
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (a
b a -> Vec ('S ('S 'Z)) a -> Vec ('S ('S ('S 'Z))) a
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (a
c a -> Vec ('S 'Z) a -> Vec ('S ('S 'Z)) a
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (a
d a -> Vec 'Z a -> Vec ('S 'Z) a
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z a
forall a. Vec 'Z a
VNil)))


injAreaCon' :: forall (id :: Symbol) (a :: Symbol) (b :: Symbol) ( c :: Symbol) (d :: Symbol)
                     (i :: Symbol) (r :: Rank) v.
               (
                InjAreaConRank id a b c d i ~ 'Just r,
                SingI r,
                Num v
               ) => Sing id -> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
injAreaCon' :: Sing id
-> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
injAreaCon' Sing id
_ Sing a
_ Sing b
_ Sing c
_ Sing d
_ Sing i
_ =
    case Sing r -> Sing (Apply LengthRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
Sing t -> Sing (Apply LengthRSym0 t)
sLengthR Sing r
sr of
      SS (SS (SS (SS (SS SZ)))) ->
        case Sing r -> Sing (Apply SaneSym0 r)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing r
sr Sing (Sane r) -> Sing 'True -> Decision (Sane r :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
          Proved Sane r :~: 'True
Refl -> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)] -> Tensor r v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
assocs
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
    tm :: Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
tm = Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
trianMapArea
    assocs :: [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
assocs = [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
 -> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)])
-> [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall a b. (a -> b) -> a -> b
$
             (\Int
a Int
b Int
c Int
d ->
                  do
                     v
s <- Int -> Int -> Int -> Int -> Maybe v
forall a v. (Ord a, Num v) => a -> a -> a -> a -> Maybe v
areaSign Int
a Int
b Int
c Int
d
                     let v :: Vec ('S ('S ('S ('S 'Z)))) Int
v = Int -> Int -> Int -> Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a. Ord a => a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
sortArea Int
a Int
b Int
c Int
d
                     Int
i <- Vec ('S ('S ('S ('S 'Z)))) Int
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Vec ('S ('S ('S ('S 'Z)))) Int
v Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
tm
                     (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)
-> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int
a Int
-> Vec ('S ('S ('S ('S 'Z)))) Int
-> Vec ('S ('S ('S ('S ('S 'Z))))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
b Int -> Vec ('S ('S ('S 'Z))) Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
c Int -> Vec ('S ('S 'Z)) Int -> Vec ('S ('S ('S 'Z))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
d Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
i Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil)))), v
s :: v))
             (Int
 -> Int
 -> Int
 -> Int
 -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v))
-> [Int]
-> [Int
    -> Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..Int
3] [Int
 -> Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int]
-> [Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3] [Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int] -> [Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3] [Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int] -> [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3]

injAreaCov' :: forall (id :: Symbol) (a :: Symbol) (b :: Symbol) ( c :: Symbol) (d :: Symbol)
                     (i :: Symbol) (r :: Rank) v.
               (
                InjAreaCovRank id a b c d i ~ 'Just r,
                SingI r,
                Num v
               ) => Sing id -> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
injAreaCov' :: Sing id
-> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
injAreaCov' Sing id
_ Sing a
_ Sing b
_ Sing c
_ Sing d
_ Sing i
_ =
    case Sing r -> Sing (Apply LengthRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
Sing t -> Sing (Apply LengthRSym0 t)
sLengthR Sing r
sr of
      SS (SS (SS (SS (SS SZ)))) ->
        case Sing r -> Sing (Apply SaneSym0 r)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing r
sr Sing (Sane r) -> Sing 'True -> Decision (Sane r :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
          Proved Sane r :~: 'True
Refl -> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)] -> Tensor r v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
assocs
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
    tm :: Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
tm = Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
trianMapArea
    assocs :: [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
assocs = [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
 -> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)])
-> [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall a b. (a -> b) -> a -> b
$
             (\Int
a Int
b Int
c Int
d ->
                  do
                     v
s <- Int -> Int -> Int -> Int -> Maybe v
forall a v. (Ord a, Num v) => a -> a -> a -> a -> Maybe v
areaSign Int
a Int
b Int
c Int
d
                     let v :: Vec ('S ('S ('S ('S 'Z)))) Int
v = Int -> Int -> Int -> Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a. Ord a => a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
sortArea Int
a Int
b Int
c Int
d
                     Int
i <- Vec ('S ('S ('S ('S 'Z)))) Int
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Vec ('S ('S ('S ('S 'Z)))) Int
v Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
tm
                     (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)
-> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int
a Int
-> Vec ('S ('S ('S ('S 'Z)))) Int
-> Vec ('S ('S ('S ('S ('S 'Z))))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
b Int -> Vec ('S ('S ('S 'Z))) Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
c Int -> Vec ('S ('S 'Z)) Int -> Vec ('S ('S ('S 'Z))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
d Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
i Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil)))), v
s :: v))
             (Int
 -> Int
 -> Int
 -> Int
 -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v))
-> [Int]
-> [Int
    -> Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..Int
3] [Int
 -> Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int]
-> [Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3] [Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int] -> [Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3] [Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int] -> [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3]

surjAreaCon' :: forall (id :: Symbol) (a :: Symbol) (b :: Symbol) ( c :: Symbol) (d :: Symbol)
                     (i :: Symbol) (r :: Rank) v.
               (
                SurjAreaConRank id a b c d i ~ 'Just r,
                SingI r,
                Fractional v
               ) => Sing id -> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
surjAreaCon' :: Sing id
-> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
surjAreaCon' Sing id
_ Sing a
_ Sing b
_ Sing c
_ Sing d
_ Sing i
_ =
    case Sing r -> Sing (Apply LengthRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
Sing t -> Sing (Apply LengthRSym0 t)
sLengthR Sing r
sr of
      SS (SS (SS (SS (SS SZ)))) ->
        case Sing r -> Sing (Apply SaneSym0 r)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing r
sr Sing (Sane r) -> Sing 'True -> Decision (Sane r :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
          Proved Sane r :~: 'True
Refl -> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)] -> Tensor r v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
assocs
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
    tm :: Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
tm = Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
trianMapArea
    fm :: Map (Vec ('S ('S ('S ('S 'Z)))) Int) v
fm = Num v => Map (Vec ('S ('S ('S ('S 'Z)))) Int) v
forall b. Num b => Map (Vec ('S ('S ('S ('S 'Z)))) Int) b
facMapArea @v
    assocs :: [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
assocs = [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
 -> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)])
-> [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall a b. (a -> b) -> a -> b
$
             (\Int
a Int
b Int
c Int
d ->
                  do
                     v
s <- Int -> Int -> Int -> Int -> Maybe v
forall a v. (Ord a, Num v) => a -> a -> a -> a -> Maybe v
areaSign Int
a Int
b Int
c Int
d
                     let v :: Vec ('S ('S ('S ('S 'Z)))) Int
v = Int -> Int -> Int -> Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a. Ord a => a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
sortArea Int
a Int
b Int
c Int
d
                     Int
i <- Vec ('S ('S ('S ('S 'Z)))) Int
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Vec ('S ('S ('S ('S 'Z)))) Int
v Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
tm
                     v
f <- Vec ('S ('S ('S ('S 'Z)))) Int
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Vec ('S ('S ('S ('S 'Z)))) Int
v Map (Vec ('S ('S ('S ('S 'Z)))) Int) v
fm
                     (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)
-> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int
a Int
-> Vec ('S ('S ('S ('S 'Z)))) Int
-> Vec ('S ('S ('S ('S ('S 'Z))))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
b Int -> Vec ('S ('S ('S 'Z))) Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
c Int -> Vec ('S ('S 'Z)) Int -> Vec ('S ('S ('S 'Z))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
d Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
i Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil)))), v
sv -> v -> v
forall a. Fractional a => a -> a -> a
/v
f :: v))
             (Int
 -> Int
 -> Int
 -> Int
 -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v))
-> [Int]
-> [Int
    -> Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..Int
3] [Int
 -> Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int]
-> [Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3] [Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int] -> [Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3] [Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int] -> [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3]

surjAreaCov' :: forall (id :: Symbol) (a :: Symbol) (b :: Symbol) ( c :: Symbol) (d :: Symbol)
                     (i :: Symbol) (r :: Rank) v.
               (
                SurjAreaCovRank id a b c d i ~ 'Just r,
                SingI r,
                Fractional v
               ) => Sing id -> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
surjAreaCov' :: Sing id
-> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
surjAreaCov' Sing id
_ Sing a
_ Sing b
_ Sing c
_ Sing d
_ Sing i
_ =
    case Sing r -> Sing (Apply LengthRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
Sing t -> Sing (Apply LengthRSym0 t)
sLengthR Sing r
sr of
      SS (SS (SS (SS (SS SZ)))) ->
        case Sing r -> Sing (Apply SaneSym0 r)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing r
sr Sing (Sane r) -> Sing 'True -> Decision (Sane r :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
          Proved Sane r :~: 'True
Refl -> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)] -> Tensor r v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
assocs
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
    tm :: Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
tm = Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
trianMapArea
    fm :: Map (Vec ('S ('S ('S ('S 'Z)))) Int) v
fm = Num v => Map (Vec ('S ('S ('S ('S 'Z)))) Int) v
forall b. Num b => Map (Vec ('S ('S ('S ('S 'Z)))) Int) b
facMapArea @v
    assocs :: [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
assocs = [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
 -> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)])
-> [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [(Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall a b. (a -> b) -> a -> b
$
             (\Int
a Int
b Int
c Int
d ->
                  do
                     v
s <- Int -> Int -> Int -> Int -> Maybe v
forall a v. (Ord a, Num v) => a -> a -> a -> a -> Maybe v
areaSign Int
a Int
b Int
c Int
d
                     let v :: Vec ('S ('S ('S ('S 'Z)))) Int
v = Int -> Int -> Int -> Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a. Ord a => a -> a -> a -> a -> Vec ('S ('S ('S ('S 'Z)))) a
sortArea Int
a Int
b Int
c Int
d
                     Int
i <- Vec ('S ('S ('S ('S 'Z)))) Int
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Vec ('S ('S ('S ('S 'Z)))) Int
v Map (Vec ('S ('S ('S ('S 'Z)))) Int) Int
tm
                     v
f <- Vec ('S ('S ('S ('S 'Z)))) Int
-> Map (Vec ('S ('S ('S ('S 'Z)))) Int) v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Vec ('S ('S ('S ('S 'Z)))) Int
v Map (Vec ('S ('S ('S ('S 'Z)))) Int) v
fm
                     (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)
-> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int
a Int
-> Vec ('S ('S ('S ('S 'Z)))) Int
-> Vec ('S ('S ('S ('S ('S 'Z))))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
b Int -> Vec ('S ('S ('S 'Z))) Int -> Vec ('S ('S ('S ('S 'Z)))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
c Int -> Vec ('S ('S 'Z)) Int -> Vec ('S ('S ('S 'Z))) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
d Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
i Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil)))), v
sv -> v -> v
forall a. Fractional a => a -> a -> a
/v
f :: v))
             (Int
 -> Int
 -> Int
 -> Int
 -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v))
-> [Int]
-> [Int
    -> Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..Int
3] [Int
 -> Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int]
-> [Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3] [Int -> Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int] -> [Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3] [Int -> Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
-> [Int] -> [Maybe (Vec ('S ('S ('S ('S ('S 'Z))))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
3]

_injAreaCon :: Num v => Demote Symbol -> Demote Symbol -> T v
_injAreaCon :: Demote Symbol -> Demote Symbol -> T v
_injAreaCon Demote Symbol
vid Demote Symbol
i =
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
vid   ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
sid ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
i     ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
si  ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 01" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s01 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 02" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s02 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 03" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s03 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 04" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s04 ->
    case Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing
     (Apply
        (Apply
           (Apply (Apply (Apply (Apply InjAreaConRankSym0 a) a) a) a) a)
        a)
forall (t1 :: Symbol) (t2 :: Symbol) (t3 :: Symbol) (t4 :: Symbol)
       (t5 :: Symbol) (t6 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing t6
-> Sing
     (Apply
        (Apply
           (Apply (Apply (Apply (Apply InjAreaConRankSym0 t1) t2) t3) t4) t5)
        t6)
sInjAreaConRank Sing a
sid Sing a
s01 Sing a
s02 Sing a
s03 Sing a
s04 Sing a
si of
      SJust sr -> Sing n -> (SingI n => T v) -> T v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => T v) -> T v) -> (SingI n => T v) -> T v
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
SingI r =>
Tensor r v -> T v
T (Tensor n v -> T v) -> Tensor n v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a -> Sing a -> Sing a -> Sing a -> Sing a -> Tensor n v
forall (id :: Symbol) (a :: Symbol) (b :: Symbol) (c :: Symbol)
       (d :: Symbol) (i :: Symbol)
       (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
(InjAreaConRank id a b c d i ~ 'Just r, SingI r, Num v) =>
Sing id
-> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
injAreaCon' Sing a
sid Sing a
s01 Sing a
s02 Sing a
s03 Sing a
s04 Sing a
si

_injAreaCov :: Num v => Demote Symbol -> Demote Symbol -> T v
_injAreaCov :: Demote Symbol -> Demote Symbol -> T v
_injAreaCov Demote Symbol
vid Demote Symbol
i =
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
vid   ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
sid ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
i     ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
si  ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 01" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s01 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 02" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s02 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 03" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s03 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 04" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s04 ->
    case Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing
     (Apply
        (Apply
           (Apply (Apply (Apply (Apply InjAreaCovRankSym0 a) a) a) a) a)
        a)
forall (t1 :: Symbol) (t2 :: Symbol) (t3 :: Symbol) (t4 :: Symbol)
       (t5 :: Symbol) (t6 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing t6
-> Sing
     (Apply
        (Apply
           (Apply (Apply (Apply (Apply InjAreaCovRankSym0 t1) t2) t3) t4) t5)
        t6)
sInjAreaCovRank Sing a
sid Sing a
s01 Sing a
s02 Sing a
s03 Sing a
s04 Sing a
si of
      SJust sr -> Sing n -> (SingI n => T v) -> T v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => T v) -> T v) -> (SingI n => T v) -> T v
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
SingI r =>
Tensor r v -> T v
T (Tensor n v -> T v) -> Tensor n v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a -> Sing a -> Sing a -> Sing a -> Sing a -> Tensor n v
forall (id :: Symbol) (a :: Symbol) (b :: Symbol) (c :: Symbol)
       (d :: Symbol) (i :: Symbol)
       (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
(InjAreaCovRank id a b c d i ~ 'Just r, SingI r, Num v) =>
Sing id
-> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
injAreaCov' Sing a
sid Sing a
s01 Sing a
s02 Sing a
s03 Sing a
s04 Sing a
si

_surjAreaCon :: Fractional v => Demote Symbol -> Demote Symbol -> T v
_surjAreaCon :: Demote Symbol -> Demote Symbol -> T v
_surjAreaCon Demote Symbol
vid Demote Symbol
i =
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
vid   ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
sid ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
i     ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
si  ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 01" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s01 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 02" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s02 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 03" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s03 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 04" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s04 ->
    case Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing
     (Apply
        (Apply
           (Apply (Apply (Apply (Apply SurjAreaConRankSym0 a) a) a) a) a)
        a)
forall (t1 :: Symbol) (t2 :: Symbol) (t3 :: Symbol) (t4 :: Symbol)
       (t5 :: Symbol) (t6 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing t6
-> Sing
     (Apply
        (Apply
           (Apply (Apply (Apply (Apply SurjAreaConRankSym0 t1) t2) t3) t4) t5)
        t6)
sSurjAreaConRank Sing a
sid Sing a
s01 Sing a
s02 Sing a
s03 Sing a
s04 Sing a
si of
      SJust sr -> Sing n -> (SingI n => T v) -> T v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => T v) -> T v) -> (SingI n => T v) -> T v
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
SingI r =>
Tensor r v -> T v
T (Tensor n v -> T v) -> Tensor n v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a -> Sing a -> Sing a -> Sing a -> Sing a -> Tensor n v
forall (id :: Symbol) (a :: Symbol) (b :: Symbol) (c :: Symbol)
       (d :: Symbol) (i :: Symbol)
       (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
(SurjAreaConRank id a b c d i ~ 'Just r, SingI r, Fractional v) =>
Sing id
-> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
surjAreaCon' Sing a
sid Sing a
s01 Sing a
s02 Sing a
s03 Sing a
s04 Sing a
si

_surjAreaCov :: Fractional v => Demote Symbol -> Demote Symbol -> T v
_surjAreaCov :: Demote Symbol -> Demote Symbol -> T v
_surjAreaCov Demote Symbol
vid Demote Symbol
i =
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
vid   ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
sid ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
i     ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
si  ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 01" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s01 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 02" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s02 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 03" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s03 ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
" 04" ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
s04 ->
    case Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing
     (Apply
        (Apply
           (Apply (Apply (Apply (Apply SurjAreaCovRankSym0 a) a) a) a) a)
        a)
forall (t1 :: Symbol) (t2 :: Symbol) (t3 :: Symbol) (t4 :: Symbol)
       (t5 :: Symbol) (t6 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing t6
-> Sing
     (Apply
        (Apply
           (Apply (Apply (Apply (Apply SurjAreaCovRankSym0 t1) t2) t3) t4) t5)
        t6)
sSurjAreaCovRank Sing a
sid Sing a
s01 Sing a
s02 Sing a
s03 Sing a
s04 Sing a
si of
      SJust sr -> Sing n -> (SingI n => T v) -> T v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => T v) -> T v) -> (SingI n => T v) -> T v
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
SingI r =>
Tensor r v -> T v
T (Tensor n v -> T v) -> Tensor n v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a -> Sing a -> Sing a -> Sing a -> Sing a -> Tensor n v
forall (id :: Symbol) (a :: Symbol) (b :: Symbol) (c :: Symbol)
       (d :: Symbol) (i :: Symbol)
       (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
(SurjAreaCovRank id a b c d i ~ 'Just r, SingI r, Fractional v) =>
Sing id
-> Sing a -> Sing b -> Sing c -> Sing d -> Sing i -> Tensor r v
surjAreaCov' Sing a
sid Sing a
s01 Sing a
s02 Sing a
s03 Sing a
s04 Sing a
si

someInjAreaCon :: forall v m.(Num v, MonadError String m) =>
                  Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                  m (T v)
someInjAreaCon :: Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjAreaCon Demote Symbol
vid Demote Symbol
a Demote Symbol
b Demote Symbol
c Demote Symbol
d Demote Symbol
i = VSpace (Demote Symbol) Dimension
-> [(Demote Symbol, Demote Symbol)] -> T v -> m (T v)
forall (m :: Type -> Type) v.
MonadError String m =>
VSpace (Demote Symbol) Dimension
-> [(Demote Symbol, Demote Symbol)] -> T v -> m (T v)
relabelT (Text -> Natural -> VSpace Text Natural
forall a b. a -> b -> VSpace a b
VSpace Text
Demote Symbol
vid Natural
4) [(Demote Symbol
" 01",Demote Symbol
a), (Demote Symbol
" 02",Demote Symbol
b), (Demote Symbol
" 03",Demote Symbol
c), (Demote Symbol
" 04",Demote Symbol
d)] T v
t
  where
    t :: T v
t = Demote Symbol -> Demote Symbol -> T v
forall v. Num v => Demote Symbol -> Demote Symbol -> T v
_injAreaCon Demote Symbol
vid Demote Symbol
i :: T v

someInjAreaCov :: forall v m.(Num v, MonadError String m) =>
                  Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                  m (T v)
someInjAreaCov :: Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjAreaCov Demote Symbol
vid Demote Symbol
a Demote Symbol
b Demote Symbol
c Demote Symbol
d Demote Symbol
i = VSpace (Demote Symbol) Dimension
-> [(Demote Symbol, Demote Symbol)] -> T v -> m (T v)
forall (m :: Type -> Type) v.
MonadError String m =>
VSpace (Demote Symbol) Dimension
-> [(Demote Symbol, Demote Symbol)] -> T v -> m (T v)
relabelT (Text -> Natural -> VSpace Text Natural
forall a b. a -> b -> VSpace a b
VSpace Text
Demote Symbol
vid Natural
4) [(Demote Symbol
" 01",Demote Symbol
a), (Demote Symbol
" 02",Demote Symbol
b), (Demote Symbol
" 03",Demote Symbol
c), (Demote Symbol
" 04",Demote Symbol
d)] T v
t
  where
    t :: T v
t = Demote Symbol -> Demote Symbol -> T v
forall v. Num v => Demote Symbol -> Demote Symbol -> T v
_injAreaCov Demote Symbol
vid Demote Symbol
i :: T v

someSurjAreaCon :: forall v m.(Fractional v, MonadError String m) =>
                  Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                  m (T v)
someSurjAreaCon :: Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjAreaCon Demote Symbol
vid Demote Symbol
a Demote Symbol
b Demote Symbol
c Demote Symbol
d Demote Symbol
i = VSpace (Demote Symbol) Dimension
-> [(Demote Symbol, Demote Symbol)] -> T v -> m (T v)
forall (m :: Type -> Type) v.
MonadError String m =>
VSpace (Demote Symbol) Dimension
-> [(Demote Symbol, Demote Symbol)] -> T v -> m (T v)
relabelT (Text -> Natural -> VSpace Text Natural
forall a b. a -> b -> VSpace a b
VSpace Text
Demote Symbol
vid Natural
4) [(Demote Symbol
" 01",Demote Symbol
a), (Demote Symbol
" 02",Demote Symbol
b), (Demote Symbol
" 03",Demote Symbol
c), (Demote Symbol
" 04",Demote Symbol
d)] T v
t
  where
    t :: T v
t = Demote Symbol -> Demote Symbol -> T v
forall v. Fractional v => Demote Symbol -> Demote Symbol -> T v
_surjAreaCon Demote Symbol
vid Demote Symbol
i :: T v

someSurjAreaCov :: forall v m.(Fractional v, MonadError String m) =>
                  Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                  m (T v)
someSurjAreaCov :: Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjAreaCov Demote Symbol
vid Demote Symbol
a Demote Symbol
b Demote Symbol
c Demote Symbol
d Demote Symbol
i = VSpace (Demote Symbol) Dimension
-> [(Demote Symbol, Demote Symbol)] -> T v -> m (T v)
forall (m :: Type -> Type) v.
MonadError String m =>
VSpace (Demote Symbol) Dimension
-> [(Demote Symbol, Demote Symbol)] -> T v -> m (T v)
relabelT (Text -> Natural -> VSpace Text Natural
forall a b. a -> b -> VSpace a b
VSpace Text
Demote Symbol
vid Natural
4) [(Demote Symbol
" 01",Demote Symbol
a), (Demote Symbol
" 02",Demote Symbol
b), (Demote Symbol
" 03",Demote Symbol
c), (Demote Symbol
" 04",Demote Symbol
d)] T v
t
  where
    t :: T v
t = Demote Symbol -> Demote Symbol -> T v
forall v. Fractional v => Demote Symbol -> Demote Symbol -> T v
_surjAreaCov Demote Symbol
vid Demote Symbol
i :: T v

someInterAreaCon :: Num v =>
                    Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                    T v
someInterAreaCon :: Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> T v
someInterAreaCon Demote Symbol
vid Demote Symbol
m Demote Symbol
n Demote Symbol
a Demote Symbol
b = T v
t
  where
    Right T v
t = Except String (T v) -> Either String (T v)
forall e a. Except e a -> Either e a
runExcept (Except String (T v) -> Either String (T v))
-> Except String (T v) -> Either String (T v)
forall a b. (a -> b) -> a -> b
$
      do
        T (Ratio Int)
j :: T (Ratio Int) <- Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> ExceptT String Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Fractional v, MonadError String m) =>
Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjAreaCon Demote Symbol
vid Demote Symbol
" 1" Demote Symbol
" 2" Demote Symbol
" 3" Demote Symbol
n Demote Symbol
a
        T (Ratio Int)
i :: T (Ratio Int) <- Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> ExceptT String Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Num v, MonadError String m) =>
Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjAreaCon Demote Symbol
vid Demote Symbol
" 1" Demote Symbol
" 2" Demote Symbol
" 3" Demote Symbol
m Demote Symbol
b
        T (Ratio Int)
prod <- T (Ratio Int)
i T (Ratio Int)
-> T (Ratio Int) -> ExceptT String Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Num v, MonadError String m) =>
T v -> T v -> m (T v)
.* T (Ratio Int)
j
        let res :: T (Ratio Int)
res = T (Ratio Int) -> T (Ratio Int)
forall v. (Num v, Eq v) => T v -> T v
contractT (T (Ratio Int) -> T (Ratio Int)) -> T (Ratio Int) -> T (Ratio Int)
forall a b. (a -> b) -> a -> b
$ (Ratio Int -> Ratio Int) -> T (Ratio Int) -> T (Ratio Int)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ratio Int -> Ratio Int -> Ratio Int
forall a. Num a => a -> a -> a
*(-Ratio Int
4)) T (Ratio Int)
prod
        T v -> Except String (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> Except String (T v)) -> T v -> Except String (T v)
forall a b. (a -> b) -> a -> b
$ (Ratio Int -> v) -> T (Ratio Int) -> T v
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Ratio Int
v -> if Ratio Int -> Int
forall a. Ratio a -> a
denominator Ratio Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
                             then Int -> v
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Ratio Int -> Int
forall a. Ratio a -> a
numerator Ratio Int
v)
                             else String -> v
forall a. HasCallStack => String -> a
error String
"someInterAreaCon is not fraction-free, as it should be!") T (Ratio Int)
res

someInterAreaCov :: Num v =>
                    Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                    T v
someInterAreaCov :: Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> T v
someInterAreaCov Demote Symbol
vid Demote Symbol
m Demote Symbol
n Demote Symbol
a Demote Symbol
b = T v
t
  where
    Right T v
t = Except String (T v) -> Either String (T v)
forall e a. Except e a -> Either e a
runExcept (Except String (T v) -> Either String (T v))
-> Except String (T v) -> Either String (T v)
forall a b. (a -> b) -> a -> b
$
      do
        T (Ratio Int)
j :: T (Ratio Int) <- Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> ExceptT String Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Fractional v, MonadError String m) =>
Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjAreaCov Demote Symbol
vid Demote Symbol
" 1" Demote Symbol
" 2" Demote Symbol
" 3" Demote Symbol
m Demote Symbol
a
        T (Ratio Int)
i :: T (Ratio Int) <- Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> ExceptT String Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Num v, MonadError String m) =>
Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjAreaCov Demote Symbol
vid Demote Symbol
" 1" Demote Symbol
" 2" Demote Symbol
" 3" Demote Symbol
n Demote Symbol
b
        T (Ratio Int)
prod <- T (Ratio Int)
i T (Ratio Int)
-> T (Ratio Int) -> ExceptT String Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Num v, MonadError String m) =>
T v -> T v -> m (T v)
.* T (Ratio Int)
j
        let res :: T (Ratio Int)
res = T (Ratio Int) -> T (Ratio Int)
forall v. (Num v, Eq v) => T v -> T v
contractT (T (Ratio Int) -> T (Ratio Int)) -> T (Ratio Int) -> T (Ratio Int)
forall a b. (a -> b) -> a -> b
$ (Ratio Int -> Ratio Int) -> T (Ratio Int) -> T (Ratio Int)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ratio Int -> Ratio Int -> Ratio Int
forall a. Num a => a -> a -> a
*Ratio Int
4) T (Ratio Int)
prod
        T v -> Except String (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> Except String (T v)) -> T v -> Except String (T v)
forall a b. (a -> b) -> a -> b
$ (Ratio Int -> v) -> T (Ratio Int) -> T v
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Ratio Int
v -> if Ratio Int -> Int
forall a. Ratio a -> a
denominator Ratio Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
                             then Int -> v
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Ratio Int -> Int
forall a. Ratio a -> a
numerator Ratio Int
v)
                             else String -> v
forall a. HasCallStack => String -> a
error String
"someInterAreaCov is not fraction-free, as it should be!") T (Ratio Int)
res

someDeltaArea :: Num v => Demote Symbol -> Demote Symbol -> Demote Symbol -> T v
someDeltaArea :: Demote Symbol -> Demote Symbol -> Demote Symbol -> T v
someDeltaArea Demote Symbol
vid = Demote Symbol -> Dimension -> Demote Symbol -> Demote Symbol -> T v
forall v.
Num v =>
Demote Symbol -> Dimension -> Demote Symbol -> Demote Symbol -> T v
someDelta (Text
Demote Symbol
vid Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"Area") Dimension
21

flatAreaCon :: forall (id :: Symbol) (a :: Symbol) (r :: Rank) v.
               (
                '[ '( 'VSpace (id <> "Area") 21, 'Con (a ':| '[]))] ~ r,
                Num v
               ) => Sing id -> Sing a -> Tensor r v
flatAreaCon :: Sing id -> Sing a -> Tensor r v
flatAreaCon Sing id
sid Sing a
sa =
  Sing (AppendSymbol id "Area")
-> (KnownSymbol (AppendSymbol id "Area") => Tensor r v)
-> Tensor r v
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol (Sing id
sid Sing id -> Sing "Area" -> Sing (Apply (Apply (<>@#@$) id) "Area")
forall a (t1 :: a) (t2 :: a).
SSemigroup a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (<>@#@$) t1) t2)
%<> (Sing "Area"
forall k (a :: k). SingI a => Sing a
sing :: Sing "Area")) ((KnownSymbol (AppendSymbol id "Area") => Tensor r v)
 -> Tensor r v)
-> (KnownSymbol (AppendSymbol id "Area") => Tensor r v)
-> Tensor r v
forall a b. (a -> b) -> a -> b
$
  Sing a -> (KnownSymbol a => Tensor r v) -> Tensor r v
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sa ((KnownSymbol a => Tensor r v) -> Tensor r v)
-> (KnownSymbol a => Tensor r v) -> Tensor r v
forall a b. (a -> b) -> a -> b
$
  [(Vec ('S 'Z) Int, v)]
-> Tensor
     '[ '( 'VSpace (AppendSymbol id "Area") 21, 'Con (a ':| '[]))] v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList [(Int
0 Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil, -v
1), (Int
5 Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil, v
1),   --  0  1  2  3  4  5
            (Int
6 Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil, -v
1), (Int
9 Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil, -v
1),  --     6  7  8  9 10
            (Int
11 Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil, -v
1), (Int
12 Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil, v
1), --       11 12 13 14
            (Int
15 Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil, v
1),                        --          15 16 17
            (Int
18 Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil, v
1),                        --             18 19
            (Int
20 Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec 'Z Int
forall a. Vec 'Z a
VNil, v
1)]                        --                20



someFlatAreaCon :: Num v => Demote Symbol -> Demote Symbol -> T v
someFlatAreaCon :: Demote Symbol -> Demote Symbol -> T v
someFlatAreaCon Demote Symbol
vid Demote Symbol
a =
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
vid ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
sid ->
  Demote Symbol -> (forall (a :: Symbol). Sing a -> T v) -> T v
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
a   ((forall (a :: Symbol). Sing a -> T v) -> T v)
-> (forall (a :: Symbol). Sing a -> T v) -> T v
forall a b. (a -> b) -> a -> b
$ \Sing a
sa  ->
  Sing (AppendSymbol a "Area")
-> (KnownSymbol (AppendSymbol a "Area") => T v) -> T v
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol (Sing a
sid Sing a -> Sing "Area" -> Sing (Apply (Apply (<>@#@$) a) "Area")
forall a (t1 :: a) (t2 :: a).
SSemigroup a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (<>@#@$) t1) t2)
%<> (Sing "Area"
forall k (a :: k). SingI a => Sing a
sing :: Sing "Area")) ((KnownSymbol (AppendSymbol a "Area") => T v) -> T v)
-> (KnownSymbol (AppendSymbol a "Area") => T v) -> T v
forall a b. (a -> b) -> a -> b
$
  Sing a -> (KnownSymbol a => T v) -> T v
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sa ((KnownSymbol a => T v) -> T v) -> (KnownSymbol a => T v) -> T v
forall a b. (a -> b) -> a -> b
$
  Tensor
  '[ '( 'VSpace (AppendSymbol a "Area") 21, 'Con (a ':| '[]))] v
-> T v
forall (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
SingI r =>
Tensor r v -> T v
T (Tensor
   '[ '( 'VSpace (AppendSymbol a "Area") 21, 'Con (a ':| '[]))] v
 -> T v)
-> Tensor
     '[ '( 'VSpace (AppendSymbol a "Area") 21, 'Con (a ':| '[]))] v
-> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a
-> Tensor
     '[ '( 'VSpace (AppendSymbol a "Area") 21, 'Con (a ':| '[]))] v
forall (id :: Symbol) (a :: Symbol)
       (r :: [(VSpace Symbol Nat, IList Symbol)]) v.
('[ '( 'VSpace (id <> "Area") 21, 'Con (a ':| '[]))] ~ r, Num v) =>
Sing id -> Sing a -> Tensor r v
flatAreaCon Sing a
sid Sing a
sa