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

-----------------------------------------------------------------------------
{-|
Module      : Math.Tensor.Basic.Sym2
Description : Definitions of symmetric tensors.
Copyright   : (c) Nils Alex, 2020
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
)

, 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)