{-# 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 #-}

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

Definitions of symmetric tensors.
-}
-----------------------------------------------------------------------------
module Math.Tensor.Basic.Sym2
  ( -- * Flat positive-definite metric
    gamma
  , gamma'
  , someGamma
  , gammaInv
  , gammaInv'
  , someGammaInv
  , -- * Flat Lorentzian metric
    eta
  , eta'
  , someEta
  , etaInv
  , etaInv'
  , someEtaInv
  ,  -- * Injections from \(S^2V\) into \(V\times V\)
    injSym2Con'
  , injSym2Cov'
  , someInjSym2Con
  , someInjSym2Cov
  , -- * Surjections from \(V\times V\) onto \(S^2V\)
    surjSym2Con'
  , surjSym2Cov'
  , someSurjSym2Con
  , someSurjSym2Cov
  , -- * Vertical coefficients for functions on \(S^2V\)
    someInterSym2Con
  , someInterSym2Cov
  , -- * Kronecker delta on \(S^2V\)
    someDeltaSym2
  , -- * Internals
    trianMapSym2
  , facMapSym2
  , sym2Assocs 
  , sym2AssocsFac
  ) 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
  , Nat
  , withKnownNat
  , natVal
  , withKnownSymbol
  )

import Data.Ratio (Ratio, numerator, denominator)
import Data.List.NonEmpty (NonEmpty((:|)))
import qualified Data.Map.Strict as Map
  ( Map
  , fromList
  , lookup
  )

import Control.Monad.Except
  ( MonadError
  , throwError
  , runExcept
  )

trianMapSym2 :: forall a.Integral a => a -> Map.Map (Vec ('S ('S 'Z)) Int) Int
trianMapSym2 :: a -> Map (Vec ('S ('S 'Z)) Int) Int
trianMapSym2 a
n = [(Vec ('S ('S 'Z)) Int, Int)] -> Map (Vec ('S ('S 'Z)) Int) Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Vec ('S ('S 'Z)) Int, Int)] -> Map (Vec ('S ('S 'Z)) Int) Int)
-> [(Vec ('S ('S 'Z)) Int, Int)] -> Map (Vec ('S ('S 'Z)) Int) Int
forall a b. (a -> b) -> a -> b
$ [Vec ('S ('S 'Z)) Int] -> [Int] -> [(Vec ('S ('S 'Z)) Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Vec ('S ('S 'Z)) Int]
indices2 [Int]
indices1
  where
    maxInd :: Int
    maxInd :: Int
maxInd   = a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
    indices1 :: [Int]
    indices1 :: [Int]
indices1 = [Int
0..]
    indices2 :: [Vec ('S ('S 'Z)) Int]
indices2 = [Int
a Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
b 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
maxInd], Int
b <- [Int
a..Int
maxInd] ]

facMapSym2 :: forall a b.(Integral a, Num b) => a -> Map.Map (Vec ('S ('S 'Z)) Int) b
facMapSym2 :: a -> Map (Vec ('S ('S 'Z)) Int) b
facMapSym2 a
n = [(Vec ('S ('S 'Z)) Int, b)] -> Map (Vec ('S ('S 'Z)) Int) b
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Vec ('S ('S 'Z)) Int, b)] -> Map (Vec ('S ('S 'Z)) Int) b)
-> [(Vec ('S ('S 'Z)) Int, b)] -> Map (Vec ('S ('S 'Z)) Int) b
forall a b. (a -> b) -> a -> b
$ [(Int
a Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int
b 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 -> b
fac Int
a Int
b) |
                                  Int
a <- [Int
0..Int
maxInd], Int
b <- [Int
a..Int
maxInd] ]
  where
    maxInd :: Int
maxInd = a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
    fac :: Int -> Int -> b
    fac :: Int -> Int -> b
fac Int
a Int
b
      | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
b    = b
1
      | Bool
otherwise = b
2

sym2Assocs :: forall (n :: Nat) v.Num v => Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
sym2Assocs :: Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
sym2Assocs Sing n
sn = [(Vec ('S ('S ('S 'Z))) Int, v)]
assocs
  where
    n :: Natural
n  = Sing n -> (KnownNat n => Natural) -> Natural
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
sn (SNat n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal SNat n
Sing n
sn)
    tm :: Map (Vec ('S ('S 'Z)) Int) Int
tm = Natural -> Map (Vec ('S ('S 'Z)) Int) Int
forall a. Integral a => a -> Map (Vec ('S ('S 'Z)) Int) Int
trianMapSym2 Natural
n
    maxInd :: Int
maxInd = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
1 :: Int)
    assocs :: [(Vec ('S ('S ('S 'Z))) Int, v)]
assocs = (\Int
a Int
b -> let v :: Vec ('S ('S 'Z)) Int
v = Int -> Int -> Vec ('S ('S 'Z)) Int
vec Int
a Int
b
                      in case Vec ('S ('S 'Z)) Int -> Map (Vec ('S ('S 'Z)) Int) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Vec ('S ('S 'Z)) Int
v Map (Vec ('S ('S 'Z)) Int) Int
tm of
                           Just Int
i -> (Int
a 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
b 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
1 :: v)
                           Maybe Int
_      -> [Char] -> (Vec ('S ('S ('S 'Z))) Int, v)
forall a. HasCallStack => [Char] -> a
error ([Char] -> (Vec ('S ('S ('S 'Z))) Int, v))
-> [Char] -> (Vec ('S ('S ('S 'Z))) Int, v)
forall a b. (a -> b) -> a -> b
$ [Char]
"indices " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> [Char]
forall a. Show a => a -> [Char]
show (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
a Int
b, Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
a Int
b) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                                             [Char]
" not present in triangle map " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Map (Vec ('S ('S 'Z)) Int) Int -> [Char]
forall a. Show a => a -> [Char]
show Map (Vec ('S ('S 'Z)) Int) Int
tm)
             (Int -> Int -> (Vec ('S ('S ('S 'Z))) Int, v))
-> [Int] -> [Int -> (Vec ('S ('S ('S 'Z))) Int, v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..Int
maxInd] [Int -> (Vec ('S ('S ('S 'Z))) Int, v)]
-> [Int] -> [(Vec ('S ('S ('S 'Z))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
maxInd]

    vec :: Int -> Int -> Vec ('S ('S 'Z)) Int
    vec :: Int -> Int -> Vec ('S ('S 'Z)) Int
vec Int
a Int
b = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
a Int
b Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
a Int
b 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)

sym2AssocsFac :: forall (n :: Nat) v.Fractional v => Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
sym2AssocsFac :: Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
sym2AssocsFac Sing n
sn = [(Vec ('S ('S ('S 'Z))) Int, v)]
assocs
  where
    n :: Natural
n  = Sing n -> (KnownNat n => Natural) -> Natural
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
sn (SNat n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal SNat n
Sing n
sn)
    tm :: Map (Vec ('S ('S 'Z)) Int) Int
tm = Natural -> Map (Vec ('S ('S 'Z)) Int) Int
forall a. Integral a => a -> Map (Vec ('S ('S 'Z)) Int) Int
trianMapSym2 Natural
n
    fm :: Map (Vec ('S ('S 'Z)) Int) v
fm = Natural -> Map (Vec ('S ('S 'Z)) Int) v
forall a b.
(Integral a, Num b) =>
a -> Map (Vec ('S ('S 'Z)) Int) b
facMapSym2 Natural
n
    maxInd :: Int
maxInd = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Sing n -> (KnownNat n => Natural) -> Natural
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
sn (SNat n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal SNat n
Sing n
sn)) Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
1 :: Int)
    assocs :: [(Vec ('S ('S ('S 'Z))) Int, v)]
assocs = (\Int
a Int
b -> case
                        (do
                           let v :: Vec ('S ('S 'Z)) Int
v = Int -> Int -> Vec ('S ('S 'Z)) Int
vec Int
a Int
b
                           Int
i <- Vec ('S ('S 'Z)) Int -> Map (Vec ('S ('S 'Z)) Int) Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Vec ('S ('S 'Z)) Int
v Map (Vec ('S ('S 'Z)) Int) Int
tm
                           v
f <- Vec ('S ('S 'Z)) Int -> Map (Vec ('S ('S 'Z)) Int) v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Vec ('S ('S 'Z)) Int
v Map (Vec ('S ('S 'Z)) Int) v
fm
                           (Vec ('S ('S ('S 'Z))) Int, v)
-> Maybe (Vec ('S ('S ('S 'Z))) Int, v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Int
a 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
b 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
1 v -> v -> v
forall a. Fractional a => a -> a -> a
/ v
f :: v)) of
                        Just (Vec ('S ('S ('S 'Z))) Int, v)
x -> (Vec ('S ('S ('S 'Z))) Int, v)
x
                        Maybe (Vec ('S ('S ('S 'Z))) Int, v)
Nothing -> [Char] -> (Vec ('S ('S ('S 'Z))) Int, v)
forall a. HasCallStack => [Char] -> a
error [Char]
"sym2AssocsFac are not fraction-free, as they should be!")
             (Int -> Int -> (Vec ('S ('S ('S 'Z))) Int, v))
-> [Int] -> [Int -> (Vec ('S ('S ('S 'Z))) Int, v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..Int
maxInd] [Int -> (Vec ('S ('S ('S 'Z))) Int, v)]
-> [Int] -> [(Vec ('S ('S ('S 'Z))) Int, v)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Int
0..Int
maxInd]

    vec :: Int -> Int -> Vec ('S ('S 'Z)) Int
    vec :: Int -> Int -> Vec ('S ('S 'Z)) Int
vec Int
a Int
b = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
a Int
b Int -> Vec ('S 'Z) Int -> Vec ('S ('S 'Z)) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
a Int
b 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)

gamma' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
           (
            '[ '( 'VSpace id n, 'Cov (a ':| '[b])) ] ~ r,
            (a < b) ~ 'True,
            SingI n,
            Num v
           ) =>
           Sing id -> Sing n -> Sing a -> Sing b ->
           Tensor r v
gamma' :: Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
gamma' Sing id
_ Sing n
_ Sing a
_ Sing b
_ = Tensor r v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
('[ '( 'VSpace id n, 'Cov (a ':| '[b]))] ~ r, (a < b) ~ 'True,
 SingI n, Num v) =>
Tensor r v
gamma

gamma :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
         (
          '[ '( 'VSpace id n, 'Cov (a ':| '[b])) ] ~ r,
          (a < b) ~ 'True,
          SingI n,
          Num v
         ) => Tensor r v
gamma :: Tensor r v
gamma = case (Sing n
forall k (a :: k). SingI a => Sing a
sing :: Sing n) of
          Sing n
sn -> let x :: Int
x = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Sing n -> (KnownNat n => Natural) -> Natural
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
sn ((KnownNat n => Natural) -> Natural)
-> (KnownNat n => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal SNat n
Sing n
sn
                in [(Int,
  Tensor ('( 'VSpace id n, 'Cov (b :|@#@$$$ '[])) :@#@$$$ '[]) v)]
-> Tensor r v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor (Int -> [(Int, Tensor (TailR r) v)]
f Int
x)
  where
    f :: Int -> [(Int, Tensor (TailR r) v)]
    f :: Int -> [(Int, Tensor (TailR r) v)]
f Int
x = (Int
 -> (Int,
     Tensor ('( 'VSpace id n, 'Cov (b :|@#@$$$ '[])) :@#@$$$ '[]) v))
-> [Int]
-> [(Int,
     Tensor ('( 'VSpace id n, 'Cov (b :|@#@$$$ '[])) :@#@$$$ '[]) v)]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> (Int
i, [(Int, Tensor '[] v)]
-> Tensor ('( 'VSpace id n, 'Cov (b :|@#@$$$ '[])) :@#@$$$ '[]) v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor [(Int
i, v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar v
1)])) [Int
0..Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

eta' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
        (
         '[ '( 'VSpace id n, 'Cov (a ':| '[b])) ] ~ r,
         (a < b) ~ 'True,
         SingI n,
         Num v
        ) =>
        Sing id -> Sing n -> Sing a -> Sing b ->
        Tensor r v
eta' :: Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
eta' Sing id
_ Sing n
_ Sing a
_ Sing b
_ = Tensor r v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
('[ '( 'VSpace id n, 'Cov (a ':| '[b]))] ~ r, (a < b) ~ 'True,
 SingI n, Num v) =>
Tensor r v
eta

eta :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
       (
        '[ '( 'VSpace id n, 'Cov (a ':| '[b])) ] ~ r,
        (a < b) ~ 'True,
        SingI n,
        Num v
       ) => Tensor r v
eta :: Tensor r v
eta = case (Sing n
forall k (a :: k). SingI a => Sing a
sing :: Sing n) of
        Sing n
sn -> let x :: Int
x = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Sing n -> (KnownNat n => Natural) -> Natural
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
sn ((KnownNat n => Natural) -> Natural)
-> (KnownNat n => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal SNat n
Sing n
sn
              in [(Int,
  Tensor ('( 'VSpace id n, 'Cov (b :|@#@$$$ '[])) :@#@$$$ '[]) v)]
-> Tensor r v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor (Int -> [(Int, Tensor (TailR r) v)]
f Int
x)
  where
    f :: Int -> [(Int, Tensor (TailR r) v)]
    f :: Int -> [(Int, Tensor (TailR r) v)]
f Int
x = (Int
 -> (Int,
     Tensor ('( 'VSpace id n, 'Cov (b :|@#@$$$ '[])) :@#@$$$ '[]) v))
-> [Int]
-> [(Int,
     Tensor ('( 'VSpace id n, 'Cov (b :|@#@$$$ '[])) :@#@$$$ '[]) v)]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> (Int
i, [(Int, Tensor '[] v)]
-> Tensor ('( 'VSpace id n, 'Cov (b :|@#@$$$ '[])) :@#@$$$ '[]) v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor [(Int
i, v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar (if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then v
1 else -v
1))])) [Int
0..Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

gammaInv' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
          (
           '[ '( 'VSpace id n, 'Con (a ':| '[b])) ] ~ r,
           (a < b) ~ 'True,
           SingI n,
           Num v
          ) =>
          Sing id -> Sing n -> Sing a -> Sing b ->
          Tensor r v
gammaInv' :: Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
gammaInv' Sing id
_ Sing n
_ Sing a
_ Sing b
_ = Tensor r v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
('[ '( 'VSpace id n, 'Con (a ':| '[b]))] ~ r, (a < b) ~ 'True,
 SingI n, Num v) =>
Tensor r v
gammaInv

gammaInv :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
          (
           '[ '( 'VSpace id n, 'Con (a ':| '[b])) ] ~ r,
           (a < b) ~ 'True,
           SingI n,
           Num v
          ) => Tensor r v
gammaInv :: Tensor r v
gammaInv = case (Sing n
forall k (a :: k). SingI a => Sing a
sing :: Sing n) of
            Sing n
sn -> let x :: Int
x = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Sing n -> (KnownNat n => Natural) -> Natural
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
sn ((KnownNat n => Natural) -> Natural)
-> (KnownNat n => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal SNat n
Sing n
sn
                  in [(Int,
  Tensor ('( 'VSpace id n, 'Con (b :|@#@$$$ '[])) :@#@$$$ '[]) v)]
-> Tensor r v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor (Int -> [(Int, Tensor (TailR r) v)]
f Int
x)
  where
    f :: Int -> [(Int, Tensor (TailR r) v)]
    f :: Int -> [(Int, Tensor (TailR r) v)]
f Int
x = (Int
 -> (Int,
     Tensor ('( 'VSpace id n, 'Con (b :|@#@$$$ '[])) :@#@$$$ '[]) v))
-> [Int]
-> [(Int,
     Tensor ('( 'VSpace id n, 'Con (b :|@#@$$$ '[])) :@#@$$$ '[]) v)]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> (Int
i, [(Int, Tensor '[] v)]
-> Tensor ('( 'VSpace id n, 'Con (b :|@#@$$$ '[])) :@#@$$$ '[]) v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor [(Int
i, v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar v
1)])) [Int
0..Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

etaInv' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
        (
         '[ '( 'VSpace id n, 'Con (a ':| '[b])) ] ~ r,
         (a < b) ~ 'True,
         SingI n,
         Num v
        ) =>
        Sing id -> Sing n -> Sing a -> Sing b ->
        Tensor r v
etaInv' :: Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
etaInv' Sing id
_ Sing n
_ Sing a
_ Sing b
_ = Tensor r v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
('[ '( 'VSpace id n, 'Con (a ':| '[b]))] ~ r, (a < b) ~ 'True,
 SingI n, Num v) =>
Tensor r v
etaInv

etaInv :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol) (r :: Rank) v.
       (
        '[ '( 'VSpace id n, 'Con (a ':| '[b])) ] ~ r,
        (a < b) ~ 'True,
        SingI n,
        Num v
       ) => Tensor r v
etaInv :: Tensor r v
etaInv = case (Sing n
forall k (a :: k). SingI a => Sing a
sing :: Sing n) of
        Sing n
sn -> let x :: Int
x = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Sing n -> (KnownNat n => Natural) -> Natural
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n
sn ((KnownNat n => Natural) -> Natural)
-> (KnownNat n => Natural) -> Natural
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal SNat n
Sing n
sn
              in [(Int,
  Tensor ('( 'VSpace id n, 'Con (b :|@#@$$$ '[])) :@#@$$$ '[]) v)]
-> Tensor r v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor (Int -> [(Int, Tensor (TailR r) v)]
f Int
x)
  where
    f :: Int -> [(Int, Tensor (TailR r) v)]
    f :: Int -> [(Int, Tensor (TailR r) v)]
f Int
x = (Int
 -> (Int,
     Tensor ('( 'VSpace id n, 'Con (b :|@#@$$$ '[])) :@#@$$$ '[]) v))
-> [Int]
-> [(Int,
     Tensor ('( 'VSpace id n, 'Con (b :|@#@$$$ '[])) :@#@$$$ '[]) v)]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> (Int
i, [(Int, Tensor '[] v)]
-> Tensor ('( 'VSpace id n, 'Con (b :|@#@$$$ '[])) :@#@$$$ '[]) v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor [(Int
i, v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar (if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then v
1 else -v
1))])) [Int
0..Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]

injSym2Con' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
                      (i :: Symbol) (r :: Rank) v.
               (
                InjSym2ConRank id n a b i ~ 'Just r,
                SingI r,
                Num v
               ) => Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
injSym2Con' :: Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
injSym2Con' Sing id
_ Sing n
svdim Sing a
_ Sing b
_ Sing i
_ =
        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 ->
            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 SZ)) -> [(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v
forall (r :: Rank) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList ([(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v)
-> [(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v
forall a b. (a -> b) -> a -> b
$ Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
forall (n :: Nat) v.
Num v =>
Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
sym2Assocs Sing n
svdim
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r

injSym2Cov' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
                      (i :: Symbol) (r :: Rank) v.
               (
                InjSym2CovRank id n a b i ~ 'Just r,
                SingI r,
                Num v
               ) => Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
injSym2Cov' :: Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
injSym2Cov' Sing id
_ Sing n
svdim Sing a
_ Sing b
_ Sing i
_ =
        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 ->
            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 SZ)) -> [(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v
forall (r :: Rank) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList ([(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v)
-> [(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v
forall a b. (a -> b) -> a -> b
$ Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
forall (n :: Nat) v.
Num v =>
Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
sym2Assocs Sing n
svdim
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r

surjSym2Con' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
                      (i :: Symbol) (r :: Rank) v.
               (
                SurjSym2ConRank id n a b i ~ 'Just r,
                SingI r,
                Fractional v
               ) => Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
surjSym2Con' :: Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
surjSym2Con' Sing id
_ Sing n
svdim Sing a
_ Sing b
_ Sing i
_ =
        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 ->
            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 SZ)) -> [(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v
forall (r :: Rank) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList ([(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v)
-> [(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v
forall a b. (a -> b) -> a -> b
$ Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
forall (n :: Nat) v.
Fractional v =>
Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
sym2AssocsFac Sing n
svdim
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r

surjSym2Cov' :: forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
                      (i :: Symbol) (r :: Rank) v.
               (
                SurjSym2CovRank id n a b i ~ 'Just r,
                SingI r,
                Fractional v
               ) => Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
surjSym2Cov' :: Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
surjSym2Cov' Sing id
_ Sing n
svdim Sing a
_ Sing b
_ Sing i
_ =
        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 ->
            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 SZ)) -> [(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v
forall (r :: Rank) v (n :: N).
(SingI r, Sane r ~ 'True, LengthR r ~ n) =>
[(Vec n Int, v)] -> Tensor r v
fromList ([(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v)
-> [(Vec ('S ('S ('S 'Z))) Int, v)] -> Tensor r v
forall a b. (a -> b) -> a -> b
$ Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
forall (n :: Nat) v.
Fractional v =>
Sing n -> [(Vec ('S ('S ('S 'Z))) Int, v)]
sym2AssocsFac Sing n
svdim
  where
    sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r

someGamma :: (Num v, MonadError String m) =>
             Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol ->
             m (T v)
someGamma :: Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
someGamma Demote Symbol
vid Demote Nat
vdim Demote Symbol
a Demote Symbol
b
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
> Text
Demote Symbol
b = Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
forall v (m :: Type -> Type).
(Num v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
someGamma Demote Symbol
vid Demote Nat
vdim Demote Symbol
b Demote Symbol
a
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
Demote Symbol
b = [Char] -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m (T v)) -> [Char] -> m (T v)
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot construct gamma with indices " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
vid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
Demote Nat
vdim [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
b
    | Bool
otherwise =
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
        Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
vdim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svdim ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sa ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
b ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sb ->
        Sing a -> (KnownNat a => m (T v)) -> m (T v)
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing a
svdim ((KnownNat a => m (T v)) -> m (T v))
-> (KnownNat a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
svid ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sa ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sb ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        case Sing a -> Sing a -> Sing (Apply (Apply CompareSym0 a) a)
forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
sCompare Sing a
sa Sing a
sb of
          Sing (Apply (Apply CompareSym0 a) a)
SLT -> T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor '[ '( 'VSpace a a, 'Cov (a ':| '[a]))] v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor '[ '( 'VSpace a a, 'Cov (a ':| '[a]))] v -> T v)
-> Tensor '[ '( 'VSpace a a, 'Cov (a ':| '[a]))] v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a
-> Sing a
-> Sing a
-> Tensor '[ '( 'VSpace a a, 'Cov (a ':| '[a]))] v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
('[ '( 'VSpace id n, 'Cov (a ':| '[b]))] ~ r, (a < b) ~ 'True,
 SingI n, Num v) =>
Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
gamma' Sing a
svid Sing a
svdim Sing a
sa Sing a
sb

someGammaInv :: (Num v, MonadError String m) =>
                Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol ->
                m (T v)
someGammaInv :: Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
someGammaInv Demote Symbol
vid Demote Nat
vdim Demote Symbol
a Demote Symbol
b
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
> Text
Demote Symbol
b = Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
forall v (m :: Type -> Type).
(Num v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
someGammaInv Demote Symbol
vid Demote Nat
vdim Demote Symbol
b Demote Symbol
a
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
Demote Symbol
b = [Char] -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m (T v)) -> [Char] -> m (T v)
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot construct gamma with indices " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
vid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
Demote Nat
vdim [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
b
    | Bool
otherwise =
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
        Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
vdim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svdim ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sa ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
b ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sb ->
        Sing a -> (KnownNat a => m (T v)) -> m (T v)
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing a
svdim ((KnownNat a => m (T v)) -> m (T v))
-> (KnownNat a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
svid ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sa ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sb ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        case Sing a -> Sing a -> Sing (Apply (Apply CompareSym0 a) a)
forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
sCompare Sing a
sa Sing a
sb of
          Sing (Apply (Apply CompareSym0 a) a)
SLT -> T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor '[ '( 'VSpace a a, 'Con (a ':| '[a]))] v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor '[ '( 'VSpace a a, 'Con (a ':| '[a]))] v -> T v)
-> Tensor '[ '( 'VSpace a a, 'Con (a ':| '[a]))] v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a
-> Sing a
-> Sing a
-> Tensor '[ '( 'VSpace a a, 'Con (a ':| '[a]))] v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
('[ '( 'VSpace id n, 'Con (a ':| '[b]))] ~ r, (a < b) ~ 'True,
 SingI n, Num v) =>
Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
gammaInv' Sing a
svid Sing a
svdim Sing a
sa Sing a
sb

someEta :: (Num v, MonadError String m) =>
           Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol ->
           m (T v)
someEta :: Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
someEta Demote Symbol
vid Demote Nat
vdim Demote Symbol
a Demote Symbol
b
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
> Text
Demote Symbol
b = Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
forall v (m :: Type -> Type).
(Num v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
someEta Demote Symbol
vid Demote Nat
vdim Demote Symbol
b Demote Symbol
a
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
Demote Symbol
b = [Char] -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m (T v)) -> [Char] -> m (T v)
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot construct eta with indices " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
vid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
Demote Nat
vdim [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
b
    | Bool
otherwise =
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
        Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
vdim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svdim ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sa ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
b ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sb ->
        Sing a -> (KnownNat a => m (T v)) -> m (T v)
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing a
svdim ((KnownNat a => m (T v)) -> m (T v))
-> (KnownNat a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
svid ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sa ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sb ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        case Sing a -> Sing a -> Sing (Apply (Apply CompareSym0 a) a)
forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
sCompare Sing a
sa Sing a
sb of
          Sing (Apply (Apply CompareSym0 a) a)
SLT -> T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor '[ '( 'VSpace a a, 'Cov (a ':| '[a]))] v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor '[ '( 'VSpace a a, 'Cov (a ':| '[a]))] v -> T v)
-> Tensor '[ '( 'VSpace a a, 'Cov (a ':| '[a]))] v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a
-> Sing a
-> Sing a
-> Tensor '[ '( 'VSpace a a, 'Cov (a ':| '[a]))] v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
('[ '( 'VSpace id n, 'Cov (a ':| '[b]))] ~ r, (a < b) ~ 'True,
 SingI n, Num v) =>
Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
eta' Sing a
svid Sing a
svdim Sing a
sa Sing a
sb

someEtaInv :: (Num v, MonadError String m) =>
           Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol ->
           m (T v)
someEtaInv :: Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
someEtaInv Demote Symbol
vid Demote Nat
vdim Demote Symbol
a Demote Symbol
b
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
> Text
Demote Symbol
b = Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
forall v (m :: Type -> Type).
(Num v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> m (T v)
someEtaInv Demote Symbol
vid Demote Nat
vdim Demote Symbol
b Demote Symbol
a
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
Demote Symbol
b = [Char] -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m (T v)) -> [Char] -> m (T v)
forall a b. (a -> b) -> a -> b
$ [Char]
"cannot construct eta with indices " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
vid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. Show a => a -> [Char]
show Natural
Demote Nat
vdim [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
b
    | Bool
otherwise =
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
        Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
vdim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svdim ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sa ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
b ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sb ->
        Sing a -> (KnownNat a => m (T v)) -> m (T v)
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing a
svdim ((KnownNat a => m (T v)) -> m (T v))
-> (KnownNat a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
svid ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sa ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        Sing a -> (KnownSymbol a => m (T v)) -> m (T v)
forall (n :: Symbol) r. Sing n -> (KnownSymbol n => r) -> r
withKnownSymbol Sing a
sb ((KnownSymbol a => m (T v)) -> m (T v))
-> (KnownSymbol a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
        case Sing a -> Sing a -> Sing (Apply (Apply CompareSym0 a) a)
forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
sCompare Sing a
sa Sing a
sb of
          Sing (Apply (Apply CompareSym0 a) a)
SLT -> T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor '[ '( 'VSpace a a, 'Con (a ':| '[a]))] v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor '[ '( 'VSpace a a, 'Con (a ':| '[a]))] v -> T v)
-> Tensor '[ '( 'VSpace a a, 'Con (a ':| '[a]))] v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a
-> Sing a
-> Sing a
-> Sing a
-> Tensor '[ '( 'VSpace a a, 'Con (a ':| '[a]))] v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (r :: Rank) v.
('[ '( 'VSpace id n, 'Con (a ':| '[b]))] ~ r, (a < b) ~ 'True,
 SingI n, Num v) =>
Sing id -> Sing n -> Sing a -> Sing b -> Tensor r v
etaInv' Sing a
svid Sing a
svdim Sing a
sa Sing a
sb

someInjSym2Con :: (Num v, MonadError String m) =>
                  Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                  m (T v)
someInjSym2Con :: Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjSym2Con Demote Symbol
vid Demote Nat
dim Demote Symbol
a Demote Symbol
b Demote Symbol
i
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
> Text
Demote Symbol
b = Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
forall v (m :: Type -> Type).
(Num v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjSym2Con Demote Symbol
vid Demote Nat
dim Demote Symbol
b Demote Symbol
a Demote Symbol
i
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
Demote Symbol
b = [Char] -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m (T v)) -> [Char] -> m (T v)
forall a b. (a -> b) -> a -> b
$ [Char]
"Invalid spacetime index for sym2 intertwiner: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"!"
    | Bool
otherwise =
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
        Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
dim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sdim ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sa ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
b   ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sb ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
si ->
        case Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing
     (Apply
        (Apply (Apply (Apply (Apply InjSym2ConRankSym0 a) a) a) a) a)
forall (t1 :: Symbol) (t2 :: Nat) (t3 :: Symbol) (t4 :: Symbol)
       (t5 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing
     (Apply
        (Apply (Apply (Apply (Apply InjSym2ConRankSym0 t1) t2) t3) t4) t5)
sInjSym2ConRank Sing a
svid Sing a
sdim Sing a
sa Sing a
sb Sing a
si of
          SJust sr ->
            Sing n -> (SingI n => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => m (T v)) -> m (T v))
-> (SingI n => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
            case Sing n -> Sing (Apply SaneSym0 n)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing n
sr Sing (Sane n) -> Sing 'True -> Decision (Sane n :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
              Proved Sane n :~: 'True
Refl -> T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: Rank) 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 -> Tensor n v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (i :: Symbol) (r :: Rank) v.
(InjSym2ConRank id n a b i ~ 'Just r, SingI r, Num v) =>
Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
injSym2Con' Sing a
svid Sing a
sdim Sing a
sa Sing a
sb Sing a
si

someInjSym2Cov :: (Num v, MonadError String m) =>
                  Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                  m (T v)
someInjSym2Cov :: Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjSym2Cov Demote Symbol
vid Demote Nat
dim Demote Symbol
a Demote Symbol
b Demote Symbol
i
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
> Text
Demote Symbol
b = Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
forall v (m :: Type -> Type).
(Num v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjSym2Cov Demote Symbol
vid Demote Nat
dim Demote Symbol
b Demote Symbol
a Demote Symbol
i
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
Demote Symbol
b = [Char] -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m (T v)) -> [Char] -> m (T v)
forall a b. (a -> b) -> a -> b
$ [Char]
"Invalid spacetime index for sym2 intertwiner: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"!"
    | Bool
otherwise =
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
        Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
dim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sdim ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sa ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
b   ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sb ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
si ->
        case Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing
     (Apply
        (Apply (Apply (Apply (Apply InjSym2CovRankSym0 a) a) a) a) a)
forall (t1 :: Symbol) (t2 :: Nat) (t3 :: Symbol) (t4 :: Symbol)
       (t5 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing
     (Apply
        (Apply (Apply (Apply (Apply InjSym2CovRankSym0 t1) t2) t3) t4) t5)
sInjSym2CovRank Sing a
svid Sing a
sdim Sing a
sa Sing a
sb Sing a
si of
          SJust sr ->
            Sing n -> (SingI n => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => m (T v)) -> m (T v))
-> (SingI n => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
            case Sing n -> Sing (Apply SaneSym0 n)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing n
sr Sing (Sane n) -> Sing 'True -> Decision (Sane n :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
              Proved Sane n :~: 'True
Refl -> T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: Rank) 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 -> Tensor n v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (i :: Symbol) (r :: Rank) v.
(InjSym2CovRank id n a b i ~ 'Just r, SingI r, Num v) =>
Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
injSym2Cov' Sing a
svid Sing a
sdim Sing a
sa Sing a
sb Sing a
si

someSurjSym2Con :: (Fractional v, MonadError String m) =>
                  Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                  m (T v)
someSurjSym2Con :: Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjSym2Con Demote Symbol
vid Demote Nat
dim Demote Symbol
a Demote Symbol
b Demote Symbol
i
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
> Text
Demote Symbol
b = Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
forall v (m :: Type -> Type).
(Fractional v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjSym2Con Demote Symbol
vid Demote Nat
dim Demote Symbol
b Demote Symbol
a Demote Symbol
i
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
Demote Symbol
b = [Char] -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m (T v)) -> [Char] -> m (T v)
forall a b. (a -> b) -> a -> b
$ [Char]
"Invalid spacetime index for sym2 intertwiner: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"!"
    | Bool
otherwise =
  Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
  Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
dim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sdim ->
  Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sa ->
  Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
b   ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sb ->
  Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
si ->
  case Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing
     (Apply
        (Apply (Apply (Apply (Apply SurjSym2ConRankSym0 a) a) a) a) a)
forall (t1 :: Symbol) (t2 :: Nat) (t3 :: Symbol) (t4 :: Symbol)
       (t5 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing
     (Apply
        (Apply (Apply (Apply (Apply SurjSym2ConRankSym0 t1) t2) t3) t4) t5)
sSurjSym2ConRank Sing a
svid Sing a
sdim Sing a
sa Sing a
sb Sing a
si of
    SJust sr ->
      Sing n -> (SingI n => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => m (T v)) -> m (T v))
-> (SingI n => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
      case Sing n -> Sing (Apply SaneSym0 n)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing n
sr Sing (Sane n) -> Sing 'True -> Decision (Sane n :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
        Proved Sane n :~: 'True
Refl -> T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: Rank) 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 -> Tensor n v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (i :: Symbol) (r :: Rank) v.
(SurjSym2ConRank id n a b i ~ 'Just r, SingI r, Fractional v) =>
Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
surjSym2Con' Sing a
svid Sing a
sdim Sing a
sa Sing a
sb Sing a
si

someSurjSym2Cov :: (Fractional v, MonadError String m) =>
                  Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                  m (T v)
someSurjSym2Cov :: Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjSym2Cov Demote Symbol
vid Demote Nat
dim Demote Symbol
a Demote Symbol
b Demote Symbol
i
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Ord a => a -> a -> Bool
> Text
Demote Symbol
b = Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
forall v (m :: Type -> Type).
(Fractional v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjSym2Cov Demote Symbol
vid Demote Nat
dim Demote Symbol
b Demote Symbol
a Demote Symbol
i
    | Text
Demote Symbol
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
Demote Symbol
b = [Char] -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError ([Char] -> m (T v)) -> [Char] -> m (T v)
forall a b. (a -> b) -> a -> b
$ [Char]
"Invalid spacetime index for sym2 intertwiner: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
forall a. Show a => a -> [Char]
show Text
Demote Symbol
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"!"
    | Bool
otherwise =
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
svid ->
        Demote Nat -> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Nat
dim ((forall (a :: Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sdim ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sa ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Demote Symbol
b   ((forall (a :: Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sb ->
        Demote Symbol
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (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 -> m (T v)) -> m (T v))
-> (forall (a :: Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
si ->
        case Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing a
-> Sing
     (Apply
        (Apply (Apply (Apply (Apply SurjSym2CovRankSym0 a) a) a) a) a)
forall (t1 :: Symbol) (t2 :: Nat) (t3 :: Symbol) (t4 :: Symbol)
       (t5 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing t5
-> Sing
     (Apply
        (Apply (Apply (Apply (Apply SurjSym2CovRankSym0 t1) t2) t3) t4) t5)
sSurjSym2CovRank Sing a
svid Sing a
sdim Sing a
sa Sing a
sb Sing a
si of
          SJust sr ->
            Sing n -> (SingI n => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sr ((SingI n => m (T v)) -> m (T v))
-> (SingI n => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
            case Sing n -> Sing (Apply SaneSym0 n)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing n
sr Sing (Sane n) -> Sing 'True -> Decision (Sane n :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
              Proved Sane n :~: 'True
Refl -> T v -> m (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> m (T v)) -> T v -> m (T v)
forall a b. (a -> b) -> a -> b
$ Tensor n v -> T v
forall (r :: Rank) 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 -> Tensor n v
forall (id :: Symbol) (n :: Nat) (a :: Symbol) (b :: Symbol)
       (i :: Symbol) (r :: Rank) v.
(SurjSym2CovRank id n a b i ~ 'Just r, SingI r, Fractional v) =>
Sing id -> Sing n -> Sing a -> Sing b -> Sing i -> Tensor r v
surjSym2Cov' Sing a
svid Sing a
sdim Sing a
sa Sing a
sb Sing a
si

someInterSym2Con :: Num v =>
                    Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                    T v
someInterSym2Con :: Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> T v
someInterSym2Con Demote Symbol
vid Demote Nat
dim Demote Symbol
m Demote Symbol
n Demote Symbol
a Demote Symbol
b = T v
t
  where
    Right T v
t = Except [Char] (T v) -> Either [Char] (T v)
forall e a. Except e a -> Either e a
runExcept (Except [Char] (T v) -> Either [Char] (T v))
-> Except [Char] (T v) -> Either [Char] (T v)
forall a b. (a -> b) -> a -> b
$
     do
       (T (Ratio Int)
j :: T (Ratio Int)) <- Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> ExceptT [Char] Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Fractional v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjSym2Con Demote Symbol
vid Demote Nat
dim Demote Symbol
" " Demote Symbol
n Demote Symbol
a
       (T (Ratio Int)
i :: T (Ratio Int)) <- Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> ExceptT [Char] Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Num v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjSym2Con Demote Symbol
vid Demote Nat
dim Demote Symbol
" " Demote Symbol
m Demote Symbol
b
       T (Ratio Int)
prod <- T (Ratio Int)
i T (Ratio Int)
-> T (Ratio Int) -> ExceptT [Char] Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Num v, MonadError [Char] 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
2) Ratio Int -> Ratio Int -> Ratio Int
forall a. Num a => a -> a -> a
*) T (Ratio Int)
prod
       T v -> Except [Char] (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> Except [Char] (T v)) -> T v -> Except [Char] (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 [Char] -> v
forall a. HasCallStack => [Char] -> a
error [Char]
"someInterSym2Con is not fraction-free, as it should be!") T (Ratio Int)
res

someInterSym2Cov :: Num v =>
                    Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol -> Demote Symbol -> Demote Symbol ->
                    T v
someInterSym2Cov :: Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> T v
someInterSym2Cov Demote Symbol
vid Demote Nat
dim Demote Symbol
m Demote Symbol
n Demote Symbol
a Demote Symbol
b = T v
t
  where
    Right T v
t = Except [Char] (T v) -> Either [Char] (T v)
forall e a. Except e a -> Either e a
runExcept (Except [Char] (T v) -> Either [Char] (T v))
-> Except [Char] (T v) -> Either [Char] (T v)
forall a b. (a -> b) -> a -> b
$
      do
        (T (Ratio Int)
j :: T (Ratio Int)) <- Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> ExceptT [Char] Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Fractional v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someSurjSym2Cov Demote Symbol
vid Demote Nat
dim Demote Symbol
" " Demote Symbol
m Demote Symbol
a
        (T (Ratio Int)
i :: T (Ratio Int)) <- Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> ExceptT [Char] Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Num v, MonadError [Char] m) =>
Demote Symbol
-> Demote Nat
-> Demote Symbol
-> Demote Symbol
-> Demote Symbol
-> m (T v)
someInjSym2Cov Demote Symbol
vid Demote Nat
dim Demote Symbol
" " Demote Symbol
n Demote Symbol
b
        T (Ratio Int)
prod <- T (Ratio Int)
i T (Ratio Int)
-> T (Ratio Int) -> ExceptT [Char] Identity (T (Ratio Int))
forall v (m :: Type -> Type).
(Num v, MonadError [Char] 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
2Ratio Int -> Ratio Int -> Ratio Int
forall a. Num a => a -> a -> a
*) T (Ratio Int)
prod
        T v -> Except [Char] (T v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (T v -> Except [Char] (T v)) -> T v -> Except [Char] (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 [Char] -> v
forall a. HasCallStack => [Char] -> a
error [Char]
"someInterSym2Cov is not fraction-free, as it should be!") T (Ratio Int)
res

someDeltaSym2 :: Num v => Demote Symbol -> Demote Nat -> Demote Symbol -> Demote Symbol -> T v
someDeltaSym2 :: Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> T v
someDeltaSym2 Demote Symbol
vid Demote Nat
n = Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> T v
forall v.
Num v =>
Demote Symbol
-> Demote Nat -> Demote Symbol -> Demote Symbol -> T v
someDelta (Text
Demote Symbol
vid Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"Sym2") ((Natural
Demote Nat
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
*(Natural
Demote Nat
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
+Natural
1)) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
2)