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

-----------------------------------------------------------------------------
{-|
Module      : Math.Tensor
Description : Existentially quantified wrapper for Math.Tensor.Safe.
Copyright   : (c) Nils Alex, 2020
License     : MIT
Maintainer  : nils.alex@fau.de

Existentially quantified wrapper around the safe interface from "Math.Tensor.Safe".
In contrast to the safe interface, all tensor operations are fair game, but potentially
illegal operations take place in the Error monad "Control.Monad.Except" and may fail
with an error message.

For usage examples, see <https://github.com/nilsalex/safe-tensor/#readme>.

For the documentation on generalized tensor ranks, see "Math.Tensor.Safe".
-}
-----------------------------------------------------------------------------
module Math.Tensor
  ( -- * Existentially quantified tensor
    -- |Wrapping a @'Tensor' r v@ in a @'T' v@ allows to define tensor operations like
    -- additions or multiplications without any constraints on the generalized ranks
    -- of the operands.
    T(..)
  , -- * Unrefined rank types
    -- |These unrefined versions of the types used to parameterise generalized tensor
    -- ranks are used in functions producing or manipulating existentially quantified
    -- tensors.
    Label
  , Dimension
  , RankT
    -- * Tensor operations
    -- |The existentially quantified versions of tensor operations from "Math.Tensor.Safe".
    -- Some operations are always safe and therefore pure. The unsafe operations take place
    -- in the Error monad "Control.Monad.Except".
  , rankT
    -- ** Special tensors
  , scalarT
  , zeroT
    -- ** Conversion from and to lists
  , toListT
  , fromListT
  , removeZerosT
    -- ** Tensor algebra
  , (.*)
  , (.+)
  , (.-)
  , (.°)
    -- ** Other operations
  , contractT
  , transposeT
  , transposeMultT
  , relabelT
  , -- * Rank construction
    conRank
  , covRank
  , conCovRank
  ) where

import Math.Tensor.Safe
import Math.Tensor.Safe.TH

import Data.Kind (Type)

import Data.Singletons
  ( Sing, SingI (sing), Demote
  , withSomeSing, withSingI
  , fromSing
  )
import Data.Singletons.Prelude
import Data.Singletons.Prelude.Maybe
  ( sIsJust
  )
import Data.Singletons.Decide
  ( Decision(Proved, Disproved)
  , (:~:) (Refl), (%~)
  )
import Data.Singletons.TypeLits
  ( Nat
  , Symbol
  )

import Data.Bifunctor (first)

import Data.List.NonEmpty (NonEmpty((:|)),sort)

import Control.DeepSeq (NFData(rnf))

import Control.Monad.Except (MonadError, throwError)

-- |@'T'@ wraps around @'Tensor'@ and exposes only the value type @v@.
data T :: Type -> Type where
  T :: forall (r :: Rank) v. SingI r => Tensor r v -> T v

deriving instance Show v => Show (T v)

instance NFData v => NFData (T v) where
  rnf :: T v -> ()
rnf (T Tensor r v
t) = Tensor r v -> ()
forall a. NFData a => a -> ()
rnf Tensor r v
t

instance Functor T where
  fmap :: (a -> b) -> T a -> T b
fmap a -> b
f (T Tensor r a
t) = Tensor r b -> T b
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor r b -> T b) -> Tensor r b -> T b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> Tensor r a -> Tensor r b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Tensor r a
t

-- |The unrefined type of labels.
--
-- @ Demote Symbol ~ 'Data.Text.Text' @
type Label     = Demote Symbol

-- |The unrefined type of dimensions.
--
-- @ Demote Nat ~ 'GHC.Natural.Natural' @
type Dimension = Demote Nat

-- |The unrefined type of generalized tensor ranks.
--
-- @ 'Demote' 'Rank' ~ 'GRank' 'Label' 'Dimension' ~ [('VSpace' 'Label' 'Dimension', 'IList' 'Dimension')] @
type RankT     = Demote Rank

-- |@'Scalar'@ of given value. Result is pure
-- because there is only one possible rank: @'[]@
scalarT :: v -> T v
scalarT :: v -> T v
scalarT v
v = Tensor '[] v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor '[] v -> T v) -> Tensor '[] v -> T v
forall a b. (a -> b) -> a -> b
$ v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar v
v

-- |@'ZeroTensor'@ of given rank @r@. Throws an
-- error if @'Sane' r ~ ''False'@.
zeroT :: MonadError String m => RankT -> m (T v)
zeroT :: RankT -> m (T v)
zeroT RankT
dr =
  RankT -> (forall (a :: Rank). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing RankT
dr ((forall (a :: Rank). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Rank). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sr ->
  case Sing a -> Sing (Apply SaneSym0 a)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing a
sr Sing (Sane a) -> Sing 'True -> Decision (Sane a :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
    Proved Sane a :~: 'True
Refl ->
      case Sing a
sr of
        (_ :: Sing r) -> Sing a -> (SingI a => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
sr ((SingI a => m (T v)) -> m (T v))
-> (SingI a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ 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 a v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
forall v. Tensor a v
ZeroTensor :: Tensor r v)
    Disproved Refuted (Sane a :~: 'True)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m (T v)) -> String -> m (T v)
forall a b. (a -> b) -> a -> b
$ String
"Illegal index list for zero : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(VSpace Text Natural, IList Text)] -> String
forall a. Show a => a -> String
show [(VSpace Text Natural, IList Text)]
RankT
dr

vecToList :: Vec n a -> [a]
vecToList :: Vec n a -> [a]
vecToList Vec n a
VNil = []
vecToList (a
x `VCons` Vec n a
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Vec n a -> [a]
forall (n :: N) a. Vec n a -> [a]
vecToList Vec n a
xs

vecFromList :: forall (n :: N) a m.
               MonadError String m => Sing n -> [a] -> m (Vec n a)
vecFromList :: Sing n -> [a] -> m (Vec n a)
vecFromList Sing n
SZ [] = Vec 'Z a -> m (Vec 'Z a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Vec 'Z a
forall a. Vec 'Z a
VNil
vecFromList (SS _) [] = String -> m (Vec n a)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"List provided for vector reconstruction is too short."
vecFromList Sing n
SZ (a
_:[a]
_)   = String -> m (Vec n a)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"List provided for vector reconstruction is too long."
vecFromList (SS sn) (a
x:[a]
xs) = do
  Vec n a
xs' <- Sing n -> [a] -> m (Vec n a)
forall (n :: N) a (m :: Type -> Type).
MonadError String m =>
Sing n -> [a] -> m (Vec n a)
vecFromList Sing n
sn [a]
xs
  Vec ('S n) a -> m (Vec ('S n) a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vec ('S n) a -> m (Vec ('S n) a))
-> Vec ('S n) a -> m (Vec ('S n) a)
forall a b. (a -> b) -> a -> b
$ a
x a -> Vec n a -> Vec ('S n) a
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
`VCons` Vec n a
xs'

-- |Pure function removing all zeros from a tensor. Wraps around @'removeZeros'@.
removeZerosT :: (Eq v, Num v) => T v -> T v
removeZerosT :: T v -> T v
removeZerosT T v
o =
  case T v
o of
    T Tensor r v
t -> Tensor r v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor r v -> T v) -> Tensor r v -> T v
forall a b. (a -> b) -> a -> b
$ Tensor r v -> Tensor r v
forall v (r :: Rank). (Num v, Eq v) => Tensor r v -> Tensor r v
removeZeros Tensor r v
t

-- |Tensor product. Throws an error if ranks overlap, i.e.
-- @'MergeR' r1 r2 ~ ''Nothing'@. Wraps around @'(&*)'@.
(.*) :: (Num v, MonadError String m) => T v -> T v -> m (T v)
.* :: T v -> T v -> m (T v)
(.*) T v
o1 T v
o2 =
  case T v
o1 of
    T (Tensor r v
t1 :: Tensor r1 v) ->
      case T v
o2 of
        T (Tensor r v
t2 :: Tensor r2 v) ->
          let sr1 :: Sing r
sr1 = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r1
              sr2 :: Sing r
sr2 = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r2
          in case Sing r -> Sing r -> Sing (Apply (Apply MergeRSym0 r) r)
forall s n (t1 :: [(VSpace s n, IList s)])
       (t2 :: [(VSpace s n, IList s)]).
(SOrd s, SOrd n) =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply MergeRSym0 t1) t2)
sMergeR Sing r
sr1 Sing r
sr2 of
               Sing (Apply (Apply MergeRSym0 r) r)
SNothing  -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Tensors have overlapping indices. Cannot multiply."
               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
$ 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 r v
t1 Tensor r v -> Tensor r v -> Tensor n v
forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v.
(Num v, 'Just r'' ~ MergeR r r', SingI r, SingI r') =>
Tensor r v -> Tensor r' v -> Tensor r'' v
&* Tensor r v
t2)
infixl 7 .*

-- |Scalar multiplication of a tensor.
(.°) :: Num v => v -> T v -> T v
.° :: v -> T v -> T v
(.°) v
s = (v -> v) -> T v -> T v
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> v -> v
forall a. Num a => a -> a -> a
*v
s)

infixl 7 .°

-- |Tensor addition. Throws an error if summand ranks do not coincide. Wraps around @'(&+)'@.
(.+) :: (Eq v, Num v, MonadError String m) => T v -> T v -> m (T v)
.+ :: T v -> T v -> m (T v)
(.+) T v
o1 T v
o2 =
  case T v
o1 of
    T (Tensor r v
t1 :: Tensor r1 v) ->
      case T v
o2 of
        T (Tensor r v
t2 :: Tensor r2 v) ->
          let sr1 :: Sing r
sr1 = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r1
              sr2 :: Sing r
sr2 = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r2
          in case Sing r
sr1 Sing r -> Sing r -> Decision (r :~: r)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing r
sr2 of
               Proved r :~: r
Refl -> 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
sr1 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 -> 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 r v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor r v
t1 Tensor r v -> Tensor r v -> Tensor r v
forall (r :: Rank) (r' :: Rank) v.
(r ~ r', Num v, Eq v) =>
Tensor r v -> Tensor r' v -> Tensor r v
&+ Tensor r v
t2)
                                Disproved Refuted (Sane r :~: 'True)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Rank of summands is not sane."
               Disproved Refuted (r :~: r)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Generalized tensor ranks do not match. Cannot add."
infixl 6 .+

-- |Tensor subtraction. Throws an error if summand ranks do not coincide. Wraps around @'(&-)'@.
(.-) :: (Eq v, Num v, MonadError String m) => T v -> T v -> m (T v)
.- :: T v -> T v -> m (T v)
(.-) T v
o1 T v
o2 =
  case T v
o1 of
    T (Tensor r v
t1 :: Tensor r1 v) ->
      case T v
o2 of
        T (Tensor r v
t2 :: Tensor r2 v) ->
          let sr1 :: Sing r
sr1 = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r1
              sr2 :: Sing r
sr2 = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r2
          in case Sing r
sr1 Sing r -> Sing r -> Decision (r :~: r)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing r
sr2 of
               Proved r :~: r
Refl -> 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
sr1 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 -> 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 r v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor r v
t1 Tensor r v -> Tensor r v -> Tensor r v
forall (r :: Rank) (r' :: Rank) v.
(r ~ r', Num v, Eq v) =>
Tensor r v -> Tensor r' v -> Tensor r v
&- Tensor r v
t2)
                                Disproved Refuted (Sane r :~: 'True)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Rank of operands is not sane."
               Disproved Refuted (r :~: r)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Generalized tensor ranks do not match. Cannot add."

-- |Tensor contraction. Pure function, because a tensor of any rank can be contracted.
-- Wraps around @'contract'@.
contractT :: (Num v, Eq v) => T v -> T v
contractT :: T v -> T v
contractT T v
o =
  case T v
o of
    T (Tensor r v
t :: Tensor r v) ->
      let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
          sr' :: Sing (Apply ContractRSym0 r)
sr' = Sing r -> Sing (Apply ContractRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply ContractRSym0 t)
sContractR Sing r
sr
      in Sing (ContractR r) -> (SingI (ContractR r) => T v) -> T v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing (Apply ContractRSym0 r)
Sing (ContractR r)
sr' ((SingI (ContractR r) => T v) -> T v)
-> (SingI (ContractR r) => T v) -> T v
forall a b. (a -> b) -> a -> b
$ Tensor (ContractR r) v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor (ContractR r) v -> T v) -> Tensor (ContractR r) v -> T v
forall a b. (a -> b) -> a -> b
$ Tensor r v -> Tensor (ContractR r) v
forall (r :: Rank) (r' :: Rank) v.
(r' ~ ContractR r, SingI r, Num v, Eq v) =>
Tensor r v -> Tensor r' v
contract Tensor r v
t

-- |Tensor transposition. Throws an error if given indices cannot be transposed.
-- Wraps around @'transpose'@.
transposeT :: MonadError String m =>
              VSpace Label Dimension -> Ix Label -> Ix Label ->
              T v -> m (T v)
transposeT :: VSpace Label Dimension -> Ix Label -> Ix Label -> T v -> m (T v)
transposeT VSpace Label Dimension
v Ix Label
ia Ix Label
ib T v
o = 
  case T v
o of
    T (Tensor r v
t :: Tensor r v) ->
      let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
      in Sing r -> (SingI r => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r
sr ((SingI r => m (T v)) -> m (T v))
-> (SingI r => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
         Demote (VSpace Symbol Nat)
-> (forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing VSpace Label Dimension
Demote (VSpace Symbol Nat)
v ((forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sv ->
         Demote (Ix Symbol)
-> (forall (a :: Ix Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Ix Label
Demote (Ix Symbol)
ia ((forall (a :: Ix Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Ix Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sia ->
         Demote (Ix Symbol)
-> (forall (a :: Ix Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing Ix Label
Demote (Ix Symbol)
ib ((forall (a :: Ix Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Ix Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sib ->
         case Sing a
-> Sing a
-> Sing a
-> Sing r
-> Sing (Apply (Apply (Apply (Apply CanTransposeSym0 a) a) a) r)
forall s n (t1 :: VSpace s n) (t2 :: Ix s) (t3 :: Ix s)
       (t4 :: [(VSpace s n, IList s)]).
(SOrd s, SOrd n) =>
Sing t1
-> Sing t2
-> Sing t3
-> Sing t4
-> Sing
     (Apply (Apply (Apply (Apply CanTransposeSym0 t1) t2) t3) t4)
sCanTranspose Sing a
sv Sing a
sia Sing a
sib Sing r
sr of
           Sing (Apply (Apply (Apply (Apply CanTransposeSym0 a) a) a) r)
STrue  -> 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 r v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor r v -> T v) -> Tensor r v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> Sing a -> Tensor r v -> Tensor r v
forall (vs :: VSpace Symbol Nat) (a :: Ix Symbol) (b :: Ix Symbol)
       (r :: Rank) v.
(CanTranspose vs a b r ~ 'True, SingI r) =>
Sing vs -> Sing a -> Sing b -> Tensor r v -> Tensor r v
transpose Sing a
sv Sing a
sia Sing a
sib Tensor r v
t
           Sing (Apply (Apply (Apply (Apply CanTransposeSym0 a) a) a) r)
SFalse -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m (T v)) -> String -> m (T v)
forall a b. (a -> b) -> a -> b
$ String
"Cannot transpose indices " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VSpace Text Natural -> String
forall a. Show a => a -> String
show VSpace Text Natural
VSpace Label Dimension
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Ix Text -> String
forall a. Show a => a -> String
show Ix Text
Ix Label
ia String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Ix Text -> String
forall a. Show a => a -> String
show Ix Text
Ix Label
ib String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!"

-- |Transposition of multiple indices. Throws an error if given indices cannot be transposed.
-- Wraps around @'transposeMult'@.
transposeMultT :: MonadError String m =>
                  VSpace Label Dimension -> [(Label,Label)] -> [(Label,Label)] -> T v -> m (T v)
transposeMultT :: VSpace Label Dimension
-> [(Label, Label)] -> [(Label, Label)] -> T v -> m (T v)
transposeMultT VSpace Label Dimension
_ [] [] T v
_ = String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Empty lists for transpositions!"
transposeMultT VSpace Label Dimension
v ((Label, Label)
con:[(Label, Label)]
cons) [] T v
o =
  case T v
o of
    T (Tensor r v
t :: Tensor r v) ->
      let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
          cons' :: NonEmpty (Text, Text)
cons' = NonEmpty (Text, Text) -> NonEmpty (Text, Text)
forall a. Ord a => NonEmpty a -> NonEmpty a
sort (NonEmpty (Text, Text) -> NonEmpty (Text, Text))
-> NonEmpty (Text, Text) -> NonEmpty (Text, Text)
forall a b. (a -> b) -> a -> b
$ (Text, Text)
(Label, Label)
con (Text, Text) -> [(Text, Text)] -> NonEmpty (Text, Text)
forall a. a -> [a] -> NonEmpty a
:| [(Text, Text)]
[(Label, Label)]
cons
          tr :: TransRule Text
tr = NonEmpty Text -> NonEmpty Text -> TransRule Text
forall a. NonEmpty a -> NonEmpty a -> TransRule a
TransCon (((Text, Text) -> Text) -> NonEmpty (Text, Text) -> NonEmpty Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Text) -> Text
forall a b. (a, b) -> a
fst NonEmpty (Text, Text)
cons') (((Text, Text) -> Text) -> NonEmpty (Text, Text) -> NonEmpty Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Text) -> Text
forall a b. (a, b) -> b
snd NonEmpty (Text, Text)
cons')
      in Sing r -> (SingI r => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r
sr ((SingI r => m (T v)) -> m (T v))
-> (SingI r => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
         Demote (VSpace Symbol Nat)
-> (forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing VSpace Label Dimension
Demote (VSpace Symbol Nat)
v ((forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sv ->
         Demote (TransRule Symbol)
-> (forall (a :: TransRule Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing TransRule Text
Demote (TransRule Symbol)
tr ((forall (a :: TransRule Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: TransRule Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
str ->
         case Sing (Transpositions a a r)
-> Sing (Apply IsJustSym0 (Transpositions a a r))
forall a (t :: Maybe a). Sing t -> Sing (Apply IsJustSym0 t)
sIsJust (Sing a
-> Sing a
-> Sing r
-> Sing (Apply (Apply (Apply TranspositionsSym0 a) a) r)
forall s n (t1 :: VSpace s n) (t2 :: TransRule s)
       (t3 :: [(VSpace s n, IList s)]).
(SOrd s, SOrd n) =>
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply TranspositionsSym0 t1) t2) t3)
sTranspositions Sing a
sv Sing a
str Sing r
sr) Sing (IsJust (Transpositions a a r))
-> Sing 'True -> Decision (IsJust (Transpositions a a r) :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
           Proved IsJust (Transpositions a a r) :~: '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 r v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor r v -> T v) -> Tensor r v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> Tensor r v -> Tensor r v
forall (vs :: VSpace Symbol Nat) (tl :: TransRule Symbol)
       (r :: Rank) v.
(IsJust (Transpositions vs tl r) ~ 'True, SingI r) =>
Sing vs -> Sing tl -> Tensor r v -> Tensor r v
transposeMult Sing a
sv Sing a
str Tensor r v
t
           Disproved Refuted (IsJust (Transpositions a a r) :~: 'True)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m (T v)) -> String -> m (T v)
forall a b. (a -> b) -> a -> b
$ String
"Cannot transpose indices " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VSpace Text Natural -> String
forall a. Show a => a -> String
show VSpace Text Natural
VSpace Label Dimension
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TransRule Text -> String
forall a. Show a => a -> String
show TransRule Text
tr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!"
transposeMultT VSpace Label Dimension
v [] ((Label, Label)
cov:[(Label, Label)]
covs) T v
o =
  case T v
o of
    T (Tensor r v
t :: Tensor r v) ->
      let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
          covs' :: NonEmpty (Text, Text)
covs' = NonEmpty (Text, Text) -> NonEmpty (Text, Text)
forall a. Ord a => NonEmpty a -> NonEmpty a
sort (NonEmpty (Text, Text) -> NonEmpty (Text, Text))
-> NonEmpty (Text, Text) -> NonEmpty (Text, Text)
forall a b. (a -> b) -> a -> b
$ (Text, Text)
(Label, Label)
cov (Text, Text) -> [(Text, Text)] -> NonEmpty (Text, Text)
forall a. a -> [a] -> NonEmpty a
:| [(Text, Text)]
[(Label, Label)]
covs
          tr :: TransRule Text
tr = NonEmpty Text -> NonEmpty Text -> TransRule Text
forall a. NonEmpty a -> NonEmpty a -> TransRule a
TransCov (((Text, Text) -> Text) -> NonEmpty (Text, Text) -> NonEmpty Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Text) -> Text
forall a b. (a, b) -> a
fst NonEmpty (Text, Text)
covs') (((Text, Text) -> Text) -> NonEmpty (Text, Text) -> NonEmpty Text
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text, Text) -> Text
forall a b. (a, b) -> b
snd NonEmpty (Text, Text)
covs')
      in Sing r -> (SingI r => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r
sr ((SingI r => m (T v)) -> m (T v))
-> (SingI r => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
         Demote (VSpace Symbol Nat)
-> (forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing VSpace Label Dimension
Demote (VSpace Symbol Nat)
v ((forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sv ->
         Demote (TransRule Symbol)
-> (forall (a :: TransRule Symbol). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing TransRule Text
Demote (TransRule Symbol)
tr ((forall (a :: TransRule Symbol). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: TransRule Symbol). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
str ->
         case Sing (Transpositions a a r)
-> Sing (Apply IsJustSym0 (Transpositions a a r))
forall a (t :: Maybe a). Sing t -> Sing (Apply IsJustSym0 t)
sIsJust (Sing a
-> Sing a
-> Sing r
-> Sing (Apply (Apply (Apply TranspositionsSym0 a) a) r)
forall s n (t1 :: VSpace s n) (t2 :: TransRule s)
       (t3 :: [(VSpace s n, IList s)]).
(SOrd s, SOrd n) =>
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply TranspositionsSym0 t1) t2) t3)
sTranspositions Sing a
sv Sing a
str Sing r
sr) Sing (IsJust (Transpositions a a r))
-> Sing 'True -> Decision (IsJust (Transpositions a a r) :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
           Proved IsJust (Transpositions a a r) :~: '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 r v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor r v -> T v) -> Tensor r v -> T v
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> Tensor r v -> Tensor r v
forall (vs :: VSpace Symbol Nat) (tl :: TransRule Symbol)
       (r :: Rank) v.
(IsJust (Transpositions vs tl r) ~ 'True, SingI r) =>
Sing vs -> Sing tl -> Tensor r v -> Tensor r v
transposeMult Sing a
sv Sing a
str Tensor r v
t
           Disproved Refuted (IsJust (Transpositions a a r) :~: 'True)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m (T v)) -> String -> m (T v)
forall a b. (a -> b) -> a -> b
$ String
"Cannot transpose indices " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VSpace Text Natural -> String
forall a. Show a => a -> String
show VSpace Text Natural
VSpace Label Dimension
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TransRule Text -> String
forall a. Show a => a -> String
show TransRule Text
tr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!"
transposeMultT VSpace Label Dimension
_ [(Label, Label)]
_ [(Label, Label)]
_ T v
_ = String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Simultaneous transposition of contravariant and covariant indices not yet supported!"

-- |Relabelling of tensor indices. Throws an error if given relabellings are not allowed.
-- Wraps around @'relabel'@.
relabelT :: MonadError String m =>
            VSpace Label Dimension -> [(Label,Label)] -> T v -> m (T v)
relabelT :: VSpace Label Dimension -> [(Label, Label)] -> T v -> m (T v)
relabelT VSpace Label Dimension
_ [] T v
_ = String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Empty list for relabelling!"
relabelT VSpace Label Dimension
v ((Label, Label)
r:[(Label, Label)]
rs) T v
o =
  case T v
o of
    T (Tensor r v
t :: Tensor r v) ->
      let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
          rr :: NonEmpty (Text, Text)
rr = NonEmpty (Text, Text) -> NonEmpty (Text, Text)
forall a. Ord a => NonEmpty a -> NonEmpty a
sort (NonEmpty (Text, Text) -> NonEmpty (Text, Text))
-> NonEmpty (Text, Text) -> NonEmpty (Text, Text)
forall a b. (a -> b) -> a -> b
$ (Text, Text)
(Label, Label)
r (Text, Text) -> [(Text, Text)] -> NonEmpty (Text, Text)
forall a. a -> [a] -> NonEmpty a
:| [(Text, Text)]
[(Label, Label)]
rs
      in Sing r -> (SingI r => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r
sr ((SingI r => m (T v)) -> m (T v))
-> (SingI r => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
         Demote (VSpace Symbol Nat)
-> (forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing VSpace Label Dimension
Demote (VSpace Symbol Nat)
v ((forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: VSpace Symbol Nat). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sv ->
         Demote (NonEmpty (Symbol, Symbol))
-> (forall (a :: NonEmpty (Symbol, Symbol)). Sing a -> m (T v))
-> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing NonEmpty (Text, Text)
Demote (NonEmpty (Symbol, Symbol))
rr ((forall (a :: NonEmpty (Symbol, Symbol)). Sing a -> m (T v))
 -> m (T v))
-> (forall (a :: NonEmpty (Symbol, Symbol)). Sing a -> m (T v))
-> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
srr ->
         case Sing a
-> Sing a
-> Sing r
-> Sing (Apply (Apply (Apply RelabelRSym0 a) a) r)
forall s n (t1 :: VSpace s n) (t2 :: NonEmpty (s, s))
       (t3 :: [(VSpace s n, IList s)]).
(SOrd s, SOrd n) =>
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply RelabelRSym0 t1) t2) t3)
sRelabelR Sing a
sv Sing a
srr Sing r
sr 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 -> Tensor r v -> Tensor n v
forall (vs :: VSpace Symbol Nat) (rl :: NonEmpty (Symbol, Symbol))
       (r1 :: Rank) (r2 :: Rank) v.
(RelabelR vs rl r1 ~ 'Just r2, Sane r2 ~ 'True, SingI r1,
 SingI r2) =>
Sing vs -> Sing rl -> Tensor r1 v -> Tensor r2 v
relabel Sing a
sv Sing a
srr Tensor r v
t
               Disproved Refuted (Sane n :~: 'True)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m (T v)) -> String -> m (T v)
forall a b. (a -> b) -> a -> b
$ String
"Cannot relabel indices " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VSpace Text Natural -> String
forall a. Show a => a -> String
show VSpace Text Natural
VSpace Label Dimension
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NonEmpty (Text, Text) -> String
forall a. Show a => a -> String
show NonEmpty (Text, Text)
rr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!"
           Sing (Apply (Apply (Apply RelabelRSym0 a) a) r)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m (T v)) -> String -> m (T v)
forall a b. (a -> b) -> a -> b
$ String
"Cannot relabel indices " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VSpace Text Natural -> String
forall a. Show a => a -> String
show VSpace Text Natural
VSpace Label Dimension
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NonEmpty (Text, Text) -> String
forall a. Show a => a -> String
show NonEmpty (Text, Text)
rr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!"

-- |Hidden rank over which @'T'@ quantifies. Possible because of the @'SingI' r@ constraint.
rankT :: T v -> RankT
rankT :: T v -> RankT
rankT T v
o =
  case T v
o of
    T (Tensor r v
_ :: Tensor r v) ->
      let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
      in Sing r -> RankT
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing r
sr

-- |Assocs list of the tensor.
toListT :: T v -> [([Int], v)]
toListT :: T v -> [([Int], v)]
toListT T v
o =
  case T v
o of
    T (Tensor r v
t :: Tensor r v) -> let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r 
                               sn :: Sing (Apply LengthRSym0 r)
sn = 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
                           in Sing (LengthR r)
-> (SingI (LengthR r) => [([Int], v)]) -> [([Int], v)]
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing (Apply LengthRSym0 r)
Sing (LengthR r)
sn ((SingI (LengthR r) => [([Int], v)]) -> [([Int], v)])
-> (SingI (LengthR r) => [([Int], v)]) -> [([Int], v)]
forall a b. (a -> b) -> a -> b
$
                              (Vec (LengthR r) Int -> [Int])
-> (Vec (LengthR r) Int, v) -> ([Int], v)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Vec (LengthR r) Int -> [Int]
forall (n :: N) a. Vec n a -> [a]
vecToList ((Vec (LengthR r) Int, v) -> ([Int], v))
-> [(Vec (LengthR r) Int, v)] -> [([Int], v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Tensor r v -> [(Vec (LengthR r) Int, v)]
forall (r :: Rank) v (n :: N).
(SingI r, SingI n, LengthR r ~ n) =>
Tensor r v -> [(Vec n Int, v)]
toList Tensor r v
t

-- |Constructs a tensor from a rank and an assocs list. Throws an error for illegal ranks
-- or incompatible assocs lists.
fromListT :: MonadError String m => RankT -> [([Int], v)] -> m (T v)
fromListT :: RankT -> [([Int], v)] -> m (T v)
fromListT RankT
r [([Int], v)]
xs =
  RankT -> (forall (a :: Rank). Sing a -> m (T v)) -> m (T v)
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing RankT
r ((forall (a :: Rank). Sing a -> m (T v)) -> m (T v))
-> (forall (a :: Rank). Sing a -> m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$ \Sing a
sr ->
  Sing a -> (SingI a => m (T v)) -> m (T v)
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
sr ((SingI a => m (T v)) -> m (T v))
-> (SingI a => m (T v)) -> m (T v)
forall a b. (a -> b) -> a -> b
$
  let sn :: Sing (Apply LengthRSym0 a)
sn = Sing a -> Sing (Apply LengthRSym0 a)
forall s n (t :: [(VSpace s n, IList s)]).
Sing t -> Sing (Apply LengthRSym0 t)
sLengthR Sing a
sr
  in case Sing a -> Sing (Apply SaneSym0 a)
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing a
sr Sing (Sane a) -> Sing 'True -> Decision (Sane a :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
    Proved Sane a :~: 'True
Refl -> Tensor a v -> T v
forall (r :: Rank) v. SingI r => Tensor r v -> T v
T (Tensor a v -> T v)
-> ([(Vec (LengthR a) Int, v)] -> Tensor a v)
-> [(Vec (LengthR a) Int, v)]
-> T v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing a -> [(Vec (LengthR a) Int, v)] -> Tensor a v
forall (r :: Rank) v (n :: N).
(Sane r ~ 'True, LengthR r ~ n) =>
Sing r -> [(Vec n Int, v)] -> Tensor r v
fromList' Sing a
sr ([(Vec (LengthR a) Int, v)] -> T v)
-> m [(Vec (LengthR a) Int, v)] -> m (T v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 
                   (([Int], v) -> m (Vec (LengthR a) Int, v))
-> [([Int], v)] -> m [(Vec (LengthR a) Int, v)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\([Int]
vec, v
val) -> do
                                         Vec (LengthR a) Int
vec' <- Sing (LengthR a) -> [Int] -> m (Vec (LengthR a) Int)
forall (n :: N) a (m :: Type -> Type).
MonadError String m =>
Sing n -> [a] -> m (Vec n a)
vecFromList Sing (Apply LengthRSym0 a)
Sing (LengthR a)
sn [Int]
vec
                                         (Vec (LengthR a) Int, v) -> m (Vec (LengthR a) Int, v)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Vec (LengthR a) Int
vec', v
val)) [([Int], v)]
xs
    Disproved Refuted (Sane a :~: 'True)
_ -> String -> m (T v)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError (String -> m (T v)) -> String -> m (T v)
forall a b. (a -> b) -> a -> b
$ String
"Insane tensor rank : " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [(VSpace Text Natural, IList Text)] -> String
forall a. Show a => a -> String
show [(VSpace Text Natural, IList Text)]
RankT
r

-- |Lifts sanity check of ranks into the error monad.
saneRank :: (Ord s, Ord n, MonadError String m) => GRank s n -> m (GRank s n)
saneRank :: GRank s n -> m (GRank s n)
saneRank GRank s n
r
    | GRank s n -> Bool
forall a b. (Ord a, Ord b) => [(VSpace a b, IList a)] -> Bool
sane GRank s n
r = GRank s n -> m (GRank s n)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure GRank s n
r
    | Bool
otherwise = String -> m (GRank s n)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Index lists must be strictly ascending."

-- |Contravariant rank from vector space label, vector space dimension,
-- and list of index labels. Throws an error for illegal ranks.
conRank :: (MonadError String m, Integral a, Ord s, Ord n, Num n) =>
           s -> a -> [s] -> m (GRank s n)
conRank :: s -> a -> [s] -> m (GRank s n)
conRank s
_ a
_ [] = String -> m (GRank s n)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Generalized rank must have non-vanishing index list!"
conRank s
v a
d (s
i:[s]
is) = GRank s n -> m (GRank s n)
forall s n (m :: Type -> Type).
(Ord s, Ord n, MonadError String m) =>
GRank s n -> m (GRank s n)
saneRank [(s -> n -> VSpace s n
forall a b. a -> b -> VSpace a b
VSpace s
v (a -> n
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d), NonEmpty s -> IList s
forall a. NonEmpty a -> IList a
Con (s
i s -> [s] -> NonEmpty s
forall a. a -> [a] -> NonEmpty a
:| [s]
is))]

-- |Covariant rank from vector space label, vector space dimension,
-- and list of index labels. Throws an error for illegal ranks.
covRank :: (MonadError String m, Integral a, Ord s, Ord n, Num n) =>
           s -> a -> [s] -> m (GRank s n)
covRank :: s -> a -> [s] -> m (GRank s n)
covRank s
_ a
_ [] = String -> m (GRank s n)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Generalized rank must have non-vanishing index list!"
covRank s
v a
d (s
i:[s]
is) = GRank s n -> m (GRank s n)
forall s n (m :: Type -> Type).
(Ord s, Ord n, MonadError String m) =>
GRank s n -> m (GRank s n)
saneRank [(s -> n -> VSpace s n
forall a b. a -> b -> VSpace a b
VSpace s
v (a -> n
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d), NonEmpty s -> IList s
forall a. NonEmpty a -> IList a
Cov (s
i s -> [s] -> NonEmpty s
forall a. a -> [a] -> NonEmpty a
:| [s]
is))]

-- |Mixed rank from vector space label, vector space dimension,
-- and lists of index labels. Throws an error for illegal ranks.
conCovRank :: (MonadError String m, Integral a, Ord s, Ord n, Num n) =>
              s -> a -> [s] -> [s] -> m (GRank s n)
conCovRank :: s -> a -> [s] -> [s] -> m (GRank s n)
conCovRank s
_ a
_ [s]
_ [] = String -> m (GRank s n)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Generalized rank must have non-vanishing index list!"
conCovRank s
_ a
_ [] [s]
_ = String -> m (GRank s n)
forall e (m :: Type -> Type) a. MonadError e m => e -> m a
throwError String
"Generalized rank must have non-vanishing index list!"
conCovRank s
v a
d (s
i:[s]
is) (s
j:[s]
js) = GRank s n -> m (GRank s n)
forall s n (m :: Type -> Type).
(Ord s, Ord n, MonadError String m) =>
GRank s n -> m (GRank s n)
saneRank [(s -> n -> VSpace s n
forall a b. a -> b -> VSpace a b
VSpace s
v (a -> n
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
d), NonEmpty s -> NonEmpty s -> IList s
forall a. NonEmpty a -> NonEmpty a -> IList a
ConCov (s
i s -> [s] -> NonEmpty s
forall a. a -> [a] -> NonEmpty a
:| [s]
is) (s
j s -> [s] -> NonEmpty s
forall a. a -> [a] -> NonEmpty a
:| [s]
js))]