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

-----------------------------------------------------------------------------
{-|
Module      : Math.Tensor.Safe
Description : Dependently typed tensor algebra.
Copyright   : (c) Nils Alex, 2020
License     : MIT
Maintainer  : nils.alex@fau.de

Dependently typed implementation of the Einstein tensor calculus, primarily used
in mathematical physics. For usage examples, see
<https://github.com/nilsalex/safe-tensor/#readme>.
-}
-----------------------------------------------------------------------------
module Math.Tensor.Safe
  ( 
    -- * Tensor calculus
    -- |Given a field \(K\) and a \(K\)-vector space \(V\) of dimension \(n\),
    -- a /tensor/ \(T\) of rank \((r,s)\) is a multilinear map from \(r\)
    -- copies of the dual vector space \(V^\ast\) and \(s\) copies of \(V\)
    -- to \(K\),
    --
    -- \[
    --    T \colon \underbrace{V^\ast \times \dots \times V^\ast}_{r\text{ times}} \times \underbrace{V \times \dots \times V}_{s\text{ times}} \rightarrow K.
    -- \]
    --
    -- The /components/ \(T^{a_1\dots a_r}_{\hphantom{a_1\dots a_r}b_1\dots b_s} \in K\)
    -- with respect to a basis \((e_i)_{i=1\dots n}\) of \(V\) and a corresponding
    -- dual basis \((\epsilon^i)_{i=1\dots n}\) of \(V^\ast\) are the \(n^{r+s}\)
    -- numbers
    --
    -- \[
    --    T^{a_1\dots a_r}_{\hphantom{a_1\dots a_r}b_1\dots b_s} = T(\epsilon^{a_1},\dots,\epsilon^{a_r},e_{b_1},\dots,e_{b_s}).
    -- \]
    --
    -- The upper indices \(a_i\) are called /contravariant/ and the lower indices \(b_i\) are
    -- called /covariant/, reflecting their behaviour under a
    -- [change of basis](https://en.wikipedia.org/wiki/Change_of_basis). From the components
    -- and the basis, the tensor can be reconstructed as
    --
    -- \[
    --    T = T^{a_1\dots a_r}_{\hphantom{a_1\dots a_3}b_1\dots b_s} \cdot e_{a_1} \otimes \dots \otimes e_{a_r} \otimes \epsilon^{b_1} \otimes \dots \otimes \epsilon^{b_s}
    -- \]
    --
    -- using the [Einstein summation convention](https://ncatlab.org/nlab/show/Einstein+summation+convention)
    -- and the [tensor product](https://en.wikipedia.org/wiki/Tensor_product).
    --
    -- The representation of tensors using their components with respect to a fixed but arbitrary
    -- basis forms the foundation of this tensor calculus. An example is the sum of a \((2,0)\) tensor
    -- \(T\) and the transposition of a \((2,0)\) tensor \(S\), which using the calculus can be
    -- written as
    --
    -- \[
    --    \lbrack T + \operatorname{transpose}(S)\rbrack^{a b} = T^{a b} + S^{b a}.
    -- \]
    --
    -- The /generalized rank/ of the tensor \(T^{a b}\) in the above example is the set of
    -- contravariant indices \(\{a, b\}\). The indices must be distinct. The generalized
    -- rank of a tensor with both contravariant and covariant indices
    -- (e.g. \(T^{ac}_{\hphantom{ac}rbl}\)) is the set of contravariant and the
    -- set of covariant indices (e.g. \((\{a,c\}, \{b,l,r\})\)). Note that
    -- both sets need not be distinct, as they label completely different entities
    -- (basis vectors vs. dual basis vectors). Overlapping indices can be removed
    -- by performing a [contraction](https://ncatlab.org/nlab/show/contraction#contraction_of_tensors),
    -- see also @'contract'@.
    --
    -- Tensors with generalized rank can be understood as a
    -- [graded algebra](https://ncatlab.org/nlab/show/graded+algebra) where only
    -- tensors of the same generalized rank can be added together and the tensor product
    -- of two tensors yields a tensor with new generalized rank. Importantly, this product
    -- is only possible if both the contravariant indices and the covariant indices of the
    -- factors do not overlap. As an example, the generalized rank of the tensor product
    -- \(T^{ap}_{\hphantom{ap}fc} S^{eg}_{\hphantom{eg}p}\) would be
    -- \((\{a,e,g,p\},\{c,f,p\})\).
    --
    -- We take this abstraction one step further and consider tensors that are multilinear
    -- maps over potentially different vector spaces and duals thereof. The generalized rank
    -- now consists of the contra- and covariant index sets for each distinct vector space.
    -- Upon multiplication of tensors, only the indices for each vector space must be distinct
    -- and contraction only removes overlapping indices among the same vector space.
    --
    -- Practical examples of configurations with multiple vector spaces are situations where
    -- both the tangent space to spacetime, \(V = T_pM\), and symmetric tensors
    -- \(S^2(V) \subset V\otimes V\), which form a proper subset of \(V\otimes V\),
    -- are considered simultaneously. See also "Math.Tensor.Basic.Sym2".

    -- * Generalized rank
    -- |The tensor calculus described above is now implemented in Haskell. Using @Template Haskell@
    -- provided by the @singletons@ library, this code is lifted to the type level and
    -- singletons are generated.
    --
    -- A vector space is parameterised by a label @a@ and a dimension @b@.
    VSpace(..)
  , -- |Each vector space must have a list of indices. This can be a contravariant index list,
    -- a covariant index list, or both. For @'sane'@ generalized ranks, the individual
    -- lists must be ascending. As already noted, both lists in the mixed case need not
    -- be disjoint.
    IList(..)
  , -- |The generalized tensor rank is a list of vector spaces and associated index lists.
    -- Sane generalized ranks have their vector spaces in ascending order.
    GRank
  , -- |The specialisation used for the parameterisation of the tensor type.
    Rank
  , -- |As explained above, the contravariant or covariant indices for each vector space must
    -- be unique. They must also be /sorted/ for more efficiency. The same applies for the
    -- vector spaces: Each distinct vector space must have a unique representation,
    -- generalized ranks are sorted by the vector spaces. This is checked by the function
    -- @'sane'@.
    sane
  , -- |The function @'headR'@ extracts the first index within a generalized rank.
    -- The first index is always referring to the
    -- first vector space within the rank. If the rank is purely covariant or purley contravariant,
    -- the first index ist the first element of the respective index list. For mixed
    -- ranks, the first index is the one which compares less. If they compare equal, it is always
    -- the contravariant index. This defines an order where contractible indices always appear
    -- next to each other, which greatly facilitates contraction.
    headR
  , -- |The remaining rank after popping the @'headR'@ is obtained by the function @'tailR'@.
    tailR
  , -- |The total number of indices. 
    lengthR
  , -- |A generalized rank is contracted by considering each vector space separately.
    -- Indices appearing in both upper and lower position are removed from the rank.
    -- If that leaves a vector space without indices, it is also discarded.
    contractR
  , -- |Merging two generalized ranks in order to obtain the generalized rank of the
    -- tensor product. Returns @'Nothing'@ for incompatible ranks.
    mergeR
  , -- |To perform transpositions of two indices, single contravariant or covariant indices
    -- have to be specified. A representation for single indices is provided by the sum type @'Ix'@.
    Ix(..)
  , -- |To perform transpositions of multiple indices at once, a list of source
    -- and a list of target indices has to be provided. Both lists must be permutations
    -- of each other. A suitable representation is provided by the sum type @'TransRule'@.
    --
    -- Note that transposing indices in a tensor does not change its generalized rank.
    TransRule (..)
  , -- |To relabel a tensor, a list of source-target pairs has to be provided. Relabelling
    -- affects each index regardless of upper or lower position, so it suffices to have
    -- the type synonym @'RelabelRule'@.
    RelabelRule
  , -- |Relabelling a tensor changes its generalized rank. If tensor indices corresponding
    -- to a given vector space can be relabelled using a given @'RelabelRule'@,
    -- @'relabelR'@ returns the new generalized rank. Otherwise, it returns @'Nothing'@.
    relabelR

  , -- * The Tensor GADT
    -- |The @'Tensor'@ type parameterised by a generalized rank @r@ and a value type @v@
    -- is a recursive container for tensor components of value @v@.
    --
    --   - The base case is a @'Scalar'@, which represents a tensor with empty rank.
    --     A scalar holds a single value of type @v@.
    --
    --   - For non-empty ranks, a tensor is represented of as a mapping from all possible
    --     index values for the first index @'headR' r@ to tensors of lower rank @'tailR' r@,
    --     implemented as sparse ascending assocs list (omitting zero values).
    --
    --   - There is a shortcut for zero tensors, which are represented as @'ZeroTensor'@
    --     regardless of the generalized rank.
    --
    -- Generalized ranks must be @'Sane'@. The empty rank @'[]@ is always sane.
    Tensor(..)
  , -- ** Conversion from and to lists
    -- |A @'Tensor' r v@ can be constructed from a list of key-value pairs,
    -- where keys are length-typed vectors @'Vec'@ of @n = 'lengthR' r@ indices
    -- and values are the corresponding components.
    --
    -- The index values must be given in the order defined by repeatedly applying
    -- @'headR'@ to the rank.
    --
    -- Given a value, such an assocs list is obtained by @'toList'@.
    fromList
  , fromList'
  , toList

  , -- * Basic operations
    -- |We have now everything at our disposal to define basic tensor operations
    -- using the rank-parameterised @'Tensor'@ type. These operations (algebra,
    -- contraction, transposition, relabelling) are /safe/ in the sense that
    -- they can only be performed between tensors of matching type and the
    -- type of the resulting tensor is predetermined. There is also an
    -- existentially quantified variant of these operations available from
    -- "Math.Tensor".

    -- ** Tensor algebra
    (&+), (&-), (&*), removeZeros
  , -- ** Contraction
    contract
  , -- ** Transpositions
    transpose
  , transposeMult
  , -- ** Relabelling
    relabel

  , -- * Length-typed vectors
    -- |Type-level naturals used for tensor construction and also internally.
    N(..)
  , -- |Length-typed vector used for tensor construction and also internally.
    Vec(..)
  , vecFromListUnsafe
  ) where

import Math.Tensor.Safe.TH
import Math.Tensor.Safe.Proofs
import Math.Tensor.Safe.Vector

import Data.Kind (Type)

import Data.Constraint (Dict(Dict), (:-)(Sub))

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

import Data.Maybe (mapMaybe)
import Data.Bifunctor (first,second)
import Data.List (foldl',groupBy,sortBy)

import Control.DeepSeq (NFData(rnf))

-- |The @'Tensor'@ type parameterized by its generalized rank @r@ and
-- arbitrary value type @v@.
data Tensor :: Rank -> Type -> Type where
    ZeroTensor :: forall (r :: Rank) v . Sane r ~ 'True => Tensor r v
    Scalar :: forall v. !v -> Tensor '[] v
    Tensor :: forall (r :: Rank) (r' :: Rank) v.
              (Sane r ~ 'True, TailR r ~ r') =>
              [(Int, Tensor r' v)] -> Tensor r v

deriving instance Eq v => Eq (Tensor r v)
deriving instance Show v => Show (Tensor r v)

instance NFData v => NFData (Tensor r v) where
    rnf :: Tensor r v -> ()
rnf Tensor r v
ZeroTensor  = ()
    rnf (Scalar v
v)  = v -> ()
forall a. NFData a => a -> ()
rnf v
v
    rnf (Tensor [(Int, Tensor r' v)]
ts) = [(Int, Tensor r' v)] -> ()
forall a. NFData a => a -> ()
rnf [(Int, Tensor r' v)]
ts

instance Functor (Tensor r) where
  fmap :: (a -> b) -> Tensor r a -> Tensor r b
fmap a -> b
_ Tensor r a
ZeroTensor = Tensor r b
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
  fmap a -> b
f (Scalar a
s) = b -> Tensor '[] b
forall v. v -> Tensor '[] v
Scalar (b -> Tensor '[] b) -> b -> Tensor '[] b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
s
  fmap a -> b
f (Tensor [(Int, Tensor r' a)]
ms) = [(Int, Tensor r' b)] -> Tensor r b
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor ([(Int, Tensor r' b)] -> Tensor r b)
-> [(Int, Tensor r' b)] -> Tensor r b
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' a) -> (Int, Tensor r' b))
-> [(Int, Tensor r' a)] -> [(Int, Tensor r' b)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' a -> Tensor r' b)
-> (Int, Tensor r' a) -> (Int, Tensor r' b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((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)) [(Int, Tensor r' a)]
ms

-- |Union of assocs lists with a merging function if a component is present in both lists
-- and two functions to treat components only present in either list.
unionWith :: (a -> b -> c) -> (a -> c) -> (b -> c) -> [(Int, a)] -> [(Int, b)] -> [(Int, c)]
unionWith :: (a -> b -> c)
-> (a -> c) -> (b -> c) -> [(Int, a)] -> [(Int, b)] -> [(Int, c)]
unionWith a -> b -> c
_ a -> c
_ b -> c
f [] [(Int, b)]
ys = ((Int, b) -> (Int, c)) -> [(Int, b)] -> [(Int, c)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> c) -> (Int, b) -> (Int, c)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> c
f) [(Int, b)]
ys
unionWith a -> b -> c
_ a -> c
f b -> c
_ [(Int, a)]
xs [] = ((Int, a) -> (Int, c)) -> [(Int, a)] -> [(Int, c)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> c) -> (Int, a) -> (Int, c)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> c
f) [(Int, a)]
xs
unionWith a -> b -> c
f a -> c
g b -> c
h xs :: [(Int, a)]
xs@((Int
ix,a
vx):[(Int, a)]
xs') ys :: [(Int, b)]
ys@((Int
iy,b
vy):[(Int, b)]
ys') =
  case Int
ix Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
iy of
    Ordering
LT -> (Int
ix, a -> c
g a
vx) (Int, c) -> [(Int, c)] -> [(Int, c)]
forall a. a -> [a] -> [a]
: (a -> b -> c)
-> (a -> c) -> (b -> c) -> [(Int, a)] -> [(Int, b)] -> [(Int, c)]
forall a b c.
(a -> b -> c)
-> (a -> c) -> (b -> c) -> [(Int, a)] -> [(Int, b)] -> [(Int, c)]
unionWith a -> b -> c
f a -> c
g b -> c
h [(Int, a)]
xs' [(Int, b)]
ys
    Ordering
EQ -> (Int
ix, a -> b -> c
f a
vx b
vy) (Int, c) -> [(Int, c)] -> [(Int, c)]
forall a. a -> [a] -> [a]
: (a -> b -> c)
-> (a -> c) -> (b -> c) -> [(Int, a)] -> [(Int, b)] -> [(Int, c)]
forall a b c.
(a -> b -> c)
-> (a -> c) -> (b -> c) -> [(Int, a)] -> [(Int, b)] -> [(Int, c)]
unionWith a -> b -> c
f a -> c
g b -> c
h [(Int, a)]
xs' [(Int, b)]
ys'
    Ordering
GT -> (Int
iy, b -> c
h b
vy) (Int, c) -> [(Int, c)] -> [(Int, c)]
forall a. a -> [a] -> [a]
: (a -> b -> c)
-> (a -> c) -> (b -> c) -> [(Int, a)] -> [(Int, b)] -> [(Int, c)]
forall a b c.
(a -> b -> c)
-> (a -> c) -> (b -> c) -> [(Int, a)] -> [(Int, b)] -> [(Int, c)]
unionWith a -> b -> c
f a -> c
g b -> c
h [(Int, a)]
xs [(Int, b)]
ys'

-- |Given a @'Num'@ and @'Eq'@ instance, remove all zero values from the tensor,
-- eventually replacing a zero @Scalar@ or an empty @Tensor@ with @ZeroTensor@.
removeZeros :: (Num v, Eq v) => Tensor r v -> Tensor r v
removeZeros :: Tensor r v -> Tensor r v
removeZeros Tensor r v
ZeroTensor = Tensor r v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
removeZeros (Scalar v
s) = if v
s v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
0 then Tensor r v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor else v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar v
s
removeZeros (Tensor [(Int, Tensor r' v)]
ms) =
    case [(Int, Tensor r' v)]
ms' of
      [] -> Tensor r v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
      [(Int, Tensor r' v)]
_  -> [(Int, Tensor r' 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, Tensor r' v)]
ms'
  where
    ms' :: [(Int, Tensor r' v)]
ms' = ((Int, Tensor r' v) -> Bool)
-> [(Int, Tensor r' v)] -> [(Int, Tensor r' v)]
forall a. (a -> Bool) -> [a] -> [a]
filter
     (\(Int
_, Tensor r' v
t) ->
        case Tensor r' v
t of
          Tensor r' v
ZeroTensor -> Bool
False
          Tensor r' v
_          -> Bool
True) ([(Int, Tensor r' v)] -> [(Int, Tensor r' v)])
-> [(Int, Tensor r' v)] -> [(Int, Tensor r' v)]
forall a b. (a -> b) -> a -> b
$
            ((Int, Tensor r' v) -> (Int, Tensor r' v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor r' v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor r' v)
-> (Int, Tensor r' v) -> (Int, Tensor r' v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Tensor r' v -> Tensor r' v
forall v (r :: Rank). (Num v, Eq v) => Tensor r v -> Tensor r v
removeZeros) [(Int, Tensor r' v)]
ms

-- |Tensor addition. Generalized ranks of summands and sum coincide.
-- Zero values are removed from the result.
(&+) :: forall (r :: Rank) (r' :: Rank) v.
        ((r ~ r'), Num v, Eq v) =>
        Tensor r v -> Tensor r' v -> Tensor r v
&+ :: Tensor r v -> Tensor r' v -> Tensor r v
(&+) Tensor r v
ZeroTensor Tensor r' v
t = Tensor r v
Tensor r' v
t
(&+) Tensor r v
t Tensor r' v
ZeroTensor = Tensor r v
t
(&+) (Scalar v
s) (Scalar v
s') = v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar (v
s v -> v -> v
forall a. Num a => a -> a -> a
+ v
s')
(&+) (Tensor [(Int, Tensor r' v)]
xs) (Tensor [(Int, Tensor r' v)]
xs') = [(Int, Tensor r' 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, Tensor r' v)]
xs''
    where
       xs'' :: [(Int, Tensor r' v)]
xs'' = (Tensor r' v -> Tensor r' v -> Tensor r' v)
-> (Tensor r' v -> Tensor r' v)
-> (Tensor r' v -> Tensor r' v)
-> [(Int, Tensor r' v)]
-> [(Int, Tensor r' v)]
-> [(Int, Tensor r' v)]
forall a b c.
(a -> b -> c)
-> (a -> c) -> (b -> c) -> [(Int, a)] -> [(Int, b)] -> [(Int, c)]
unionWith 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 -> Tensor r' v
forall a. a -> a
id Tensor r' v -> Tensor r' v
forall a. a -> a
id [(Int, Tensor r' v)]
xs [(Int, Tensor r' v)]
[(Int, Tensor r' v)]
xs' 
(&+) Tensor r v
_ Tensor r' v
_ = String -> Tensor r v
forall a. HasCallStack => String -> a
error String
"Cannot add scalar and tensor! Should have been caught by the type system!"

infixl 6 &+

-- |Tensor subtraction. Generalized ranks of operands and difference coincide.
-- Zero values are removed from the result.
(&-) :: forall (r :: Rank) (r' :: Rank) v.
        ((r ~ r'), Num v, Eq v) =>
        Tensor r v -> Tensor r' v -> Tensor r v
&- :: Tensor r v -> Tensor r' v -> Tensor r v
(&-) Tensor r v
t1 Tensor r' v
t2 = 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
&+ (v -> v) -> Tensor r' v -> Tensor r' v
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap v -> v
forall a. Num a => a -> a
negate Tensor r' v
t2

infixl 6 &-

-- |Tensor multiplication, ranks @r@, @r'@ of factors passed explicitly as singletons.
-- Rank of result is @'MergeR' r r'@.
mult :: forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v.
               (Num v, 'Just r'' ~ MergeR r r') =>
               Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
mult :: Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
mult Sing r
_ Sing r'
_ (Scalar v
s) (Scalar v
t) = v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar (v
sv -> v -> v
forall a. Num a => a -> a -> a
*v
t)
mult Sing r
sr Sing r'
sr' (Scalar v
s) (Tensor [(Int, Tensor r' v)]
ms) =
  case Sing r' -> (Sane r' ~ 'True) :- (Sane (TailR r') ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
saneTailRProof Sing r'
sr' of
    Sub (Sane r' ~ 'True) => Dict (Sane (TailR r') ~ 'True)
Dict -> [(Int, Tensor r' 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, Tensor r' v)] -> Tensor r'' v)
-> [(Int, Tensor r' v)] -> Tensor r'' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor r' v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor r' v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor r' v)
-> (Int, Tensor r' v) -> (Int, Tensor r' v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing '[] -> Sing r' -> Tensor '[] v -> Tensor r' v -> Tensor r' v
forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v.
(Num v, 'Just r'' ~ MergeR r r') =>
Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
mult Sing r
Sing '[]
sr (Sing r' -> Sing (Apply TailRSym0 r')
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r'
sr') (v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar v
s))) [(Int, Tensor r' v)]
ms
mult Sing r
sr Sing r'
sr' (Tensor [(Int, Tensor r' v)]
ms) (Scalar v
s) =
  case Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
saneTailRProof Sing r
sr of
    Sub (Sane r ~ 'True) => Dict (Sane (TailR r) ~ 'True)
Dict -> [(Int, Tensor r' 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, Tensor r' v)] -> Tensor r'' v)
-> [(Int, Tensor r' v)] -> Tensor r'' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor r' v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor r' v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor r' v)
-> (Int, Tensor r' v) -> (Int, Tensor r' v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Tensor r' v
t -> Sing r' -> Sing '[] -> Tensor r' v -> Tensor '[] v -> Tensor r' v
forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v.
(Num v, 'Just r'' ~ MergeR r r') =>
Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
mult (Sing r -> Sing (Apply TailRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r
sr) Sing r'
Sing '[]
sr' Tensor r' v
t (v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar v
s))) [(Int, Tensor r' v)]
ms
mult Sing r
sr Sing r'
sr' (Tensor [(Int, Tensor r' v)]
ms) (Tensor [(Int, Tensor r' v)]
ms') =
  let sh :: Sing (Apply HeadRSym0 r)
sh = Sing r -> Sing (Apply HeadRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply HeadRSym0 t)
sHeadR Sing r
sr
      sh' :: Sing (Apply HeadRSym0 r')
sh' = Sing r' -> Sing (Apply HeadRSym0 r')
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply HeadRSym0 t)
sHeadR Sing r'
sr'
      st :: Sing (Apply TailRSym0 r)
st = Sing r -> Sing (Apply TailRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r
sr
      st' :: Sing (Apply TailRSym0 r')
st' = Sing r' -> Sing (Apply TailRSym0 r')
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r'
sr'
  in case Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
saneMergeRProof Sing r
sr Sing r'
sr' of
       Sub (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'') =>
Dict (Sane r'' ~ 'True)
Dict ->
         case Sing (Apply HeadRSym0 r)
sh of
           STuple2 sv si ->
             case Sing (Apply HeadRSym0 r')
sh' of
               STuple2 sv' si' ->
                 case Sing n1 -> Sing n1 -> Sing (Apply (Apply CompareSym0 n1) n1)
forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
sCompare Sing n1
sv Sing n1
sv' of
                   Sing (Apply (Apply CompareSym0 n1) n1)
SLT -> case Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'LT)
   :- (MergeR (TailR r) r' ~ 'Just (TailR r''))
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'LT)
   :- (MergeR (TailR r) r' ~ 'Just (TailR r''))
proofMergeLT Sing r
sr Sing r'
sr' of
                            Sub (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
 Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'LT) =>
Dict (MergeR (TailR r) r' ~ 'Just (TailR r''))
Dict ->
                              case Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
saneTailRProof Sing r
sr of
                                Sub (Sane r ~ 'True) => Dict (Sane (TailR r) ~ 'True)
Dict -> [(Int, Tensor (TailR r'') 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, Tensor (TailR r'') v)] -> Tensor r'' v)
-> [(Int, Tensor (TailR r'') v)] -> Tensor r'' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor (TailR r'') v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor (TailR r'') v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor (TailR r'') v)
-> (Int, Tensor r' v) -> (Int, Tensor (TailR r'') v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Tensor r' v
t -> Sing r'
-> Sing r' -> Tensor r' v -> Tensor r' v -> Tensor (TailR r'') v
forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v.
(Num v, 'Just r'' ~ MergeR r r') =>
Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
mult Sing r'
Sing (Apply TailRSym0 r)
st Sing r'
sr' Tensor r' v
t ([(Int, Tensor r' 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, Tensor r' v)]
ms'))) [(Int, Tensor r' v)]
ms
                   Sing (Apply (Apply CompareSym0 n1) n1)
SGT -> case Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'GT)
   :- (MergeR r (TailR r') ~ 'Just (TailR r''))
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'GT)
   :- (MergeR r (TailR r') ~ 'Just (TailR r''))
proofMergeGT Sing r
sr Sing r'
sr' of
                            Sub (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
 Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'GT) =>
Dict (MergeR r (TailR r') ~ 'Just (TailR r''))
Dict ->
                              case Sing r' -> (Sane r' ~ 'True) :- (Sane (TailR r') ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
saneTailRProof Sing r'
sr' of
                                Sub (Sane r' ~ 'True) => Dict (Sane (TailR r') ~ 'True)
Dict -> [(Int, Tensor (TailR r'') 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, Tensor (TailR r'') v)] -> Tensor r'' v)
-> [(Int, Tensor (TailR r'') v)] -> Tensor r'' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor (TailR r'') v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor (TailR r'') v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor (TailR r'') v)
-> (Int, Tensor r' v) -> (Int, Tensor (TailR r'') v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing r
-> Sing r' -> Tensor r v -> Tensor r' v -> Tensor (TailR r'') v
forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v.
(Num v, 'Just r'' ~ MergeR r r') =>
Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
mult Sing r
sr Sing r'
Sing (Apply TailRSym0 r')
st' ([(Int, Tensor r' 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, Tensor r' v)]
ms))) [(Int, Tensor r' v)]
ms'
                   Sing (Apply (Apply CompareSym0 n1) n1)
SEQ -> case Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ)
   :- ((IxCompare (Snd (HeadR r)) (Snd (HeadR r')) == 'EQ) ~ 'False)
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ)
   :- ((IxCompare (Snd (HeadR r)) (Snd (HeadR r')) == 'EQ) ~ 'False)
proofMergeIxNotEQ Sing r
sr Sing r'
sr' of
                            Sub (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
 Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ) =>
Dict ((IxCompare (Snd (HeadR r)) (Snd (HeadR r')) == 'EQ) ~ 'False)
Dict ->
                              case Sing n2 -> Sing n2 -> Sing (Apply (Apply IxCompareSym0 n2) n2)
forall a (t1 :: Ix a) (t2 :: Ix a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply IxCompareSym0 t1) t2)
sIxCompare Sing n2
si Sing n2
si' of
                                Sing (Apply (Apply IxCompareSym0 n2) n2)
SLT -> case Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,
    IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'LT)
   :- (MergeR (TailR r) r' ~ 'Just (TailR r''))
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,
    IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'LT)
   :- (MergeR (TailR r) r' ~ 'Just (TailR r''))
proofMergeIxLT Sing r
sr Sing r'
sr' of
                                         Sub (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
 Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,
 IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'LT) =>
Dict (MergeR (TailR r) r' ~ 'Just (TailR r''))
Dict ->
                                           case Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
saneTailRProof Sing r
sr of
                                             Sub (Sane r ~ 'True) => Dict (Sane (TailR r) ~ 'True)
Dict -> [(Int, Tensor (TailR r'') 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, Tensor (TailR r'') v)] -> Tensor r'' v)
-> [(Int, Tensor (TailR r'') v)] -> Tensor r'' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor (TailR r'') v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor (TailR r'') v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor (TailR r'') v)
-> (Int, Tensor r' v) -> (Int, Tensor (TailR r'') v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Tensor r' v
t -> Sing r'
-> Sing r' -> Tensor r' v -> Tensor r' v -> Tensor (TailR r'') v
forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v.
(Num v, 'Just r'' ~ MergeR r r') =>
Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
mult Sing r'
Sing (Apply TailRSym0 r)
st Sing r'
sr' Tensor r' v
t ([(Int, Tensor r' 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, Tensor r' v)]
ms'))) [(Int, Tensor r' v)]
ms
                                Sing (Apply (Apply IxCompareSym0 n2) n2)
SGT -> case Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,
    IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'GT)
   :- (MergeR r (TailR r') ~ 'Just (TailR r''))
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
    Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,
    IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'GT)
   :- (MergeR r (TailR r') ~ 'Just (TailR r''))
proofMergeIxGT Sing r
sr Sing r'
sr' of
                                         Sub (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'',
 Compare (Fst (HeadR r)) (Fst (HeadR r')) ~ 'EQ,
 IxCompare (Snd (HeadR r)) (Snd (HeadR r')) ~ 'GT) =>
Dict (MergeR r (TailR r') ~ 'Just (TailR r''))
Dict ->
                                           case Sing r' -> (Sane r' ~ 'True) :- (Sane (TailR r') ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
saneTailRProof Sing r'
sr' of
                                             Sub (Sane r' ~ 'True) => Dict (Sane (TailR r') ~ 'True)
Dict -> [(Int, Tensor (TailR r'') 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, Tensor (TailR r'') v)] -> Tensor r'' v)
-> [(Int, Tensor (TailR r'') v)] -> Tensor r'' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor (TailR r'') v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor (TailR r'') v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor (TailR r'') v)
-> (Int, Tensor r' v) -> (Int, Tensor (TailR r'') v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing r
-> Sing r' -> Tensor r v -> Tensor r' v -> Tensor (TailR r'') v
forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v.
(Num v, 'Just r'' ~ MergeR r r') =>
Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
mult Sing r
sr Sing r'
Sing (Apply TailRSym0 r')
st' ([(Int, Tensor r' 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, Tensor r' v)]
ms))) [(Int, Tensor r' v)]
ms'
mult Sing r
sr Sing r'
sr' Tensor r v
ZeroTensor Tensor r' v
ZeroTensor =
  case Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
saneMergeRProof Sing r
sr Sing r'
sr' of
    Sub (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'') =>
Dict (Sane r'' ~ 'True)
Dict -> Tensor r'' v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
mult Sing r
sr Sing r'
sr' Tensor r v
ZeroTensor (Scalar v
_) =
  case Sing r
-> Sing '[]
-> (Sane r ~ 'True, Sane '[] ~ 'True, MergeR r '[] ~ 'Just r)
   :- (Sane r ~ 'True)
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
saneMergeRProof Sing r
sr Sing r'
Sing '[]
sr' of
    Sub (Sane r ~ 'True, Sane '[] ~ 'True, MergeR r '[] ~ 'Just r) =>
Dict (Sane r ~ 'True)
Dict -> Tensor r'' v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
mult Sing r
sr Sing r'
sr' Tensor r v
ZeroTensor (Tensor [(Int, Tensor r' v)]
_) =
  case Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
saneMergeRProof Sing r
sr Sing r'
sr' of
    Sub (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'') =>
Dict (Sane r'' ~ 'True)
Dict -> Tensor r'' v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
mult Sing r
sr Sing r'
sr' (Scalar v
_) Tensor r' v
ZeroTensor =
  case Sing '[]
-> Sing r'
-> (Sane '[] ~ 'True, Sane r' ~ 'True, MergeR '[] r' ~ 'Just r')
   :- (Sane r' ~ 'True)
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
saneMergeRProof Sing r
Sing '[]
sr Sing r'
sr' of
    Sub (Sane '[] ~ 'True, Sane r' ~ 'True, MergeR '[] r' ~ 'Just r') =>
Dict (Sane r' ~ 'True)
Dict -> Tensor r'' v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
mult Sing r
sr Sing r'
sr' (Tensor [(Int, Tensor r' v)]
_) Tensor r' v
ZeroTensor =
  case Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
forall (r :: Rank) (r' :: Rank) (r'' :: Rank).
Sing r
-> Sing r'
-> (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'')
   :- (Sane r'' ~ 'True)
saneMergeRProof Sing r
sr Sing r'
sr' of
    Sub (Sane r ~ 'True, Sane r' ~ 'True, MergeR r r' ~ 'Just r'') =>
Dict (Sane r'' ~ 'True)
Dict -> Tensor r'' v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor

-- |Tensor multiplication. Generalized anks @r@, @r'@ of factors must not overlap. The product
-- rank is the merged rank @'MergeR' r r'@ of the factor ranks.
(&*) :: 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 -> Tensor r' v -> Tensor r'' v
(&*) = Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
forall (r :: Rank) (r' :: Rank) (r'' :: Rank) v.
(Num v, 'Just r'' ~ MergeR r r') =>
Sing r -> Sing r' -> Tensor r v -> Tensor r' v -> Tensor r'' v
mult (Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r) (Sing r'
forall k (a :: k). SingI a => Sing a
sing :: Sing r')

infixl 7 &*

contract' :: forall (r :: Rank) (r' :: Rank) v.
             (r' ~ ContractR r, Num v, Eq v)
             => Sing r -> Tensor r v -> Tensor r' v
contract' :: Sing r -> Tensor r v -> Tensor r' v
contract' Sing r
sr Tensor r v
t = case 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 Sing r' -> Sing r -> Decision (r' :~: r)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing r
sr of
                   Proved r' :~: r
Refl -> Tensor r v
Tensor r' v
t
                   Disproved Refuted (r' :~: r)
_ -> Sing r -> Tensor r v -> Tensor r' v
forall (r :: Rank) (r' :: Rank) v.
(r' ~ ContractR r, Num v, Eq v) =>
Sing r -> Tensor r v -> Tensor r' v
contract'' Sing r
sr Tensor r v
t

contract'' :: forall (r :: Rank) (r' :: Rank) v.
              (r' ~ ContractR r, Num v, Eq v)
              => Sing r -> Tensor r v -> Tensor r' v
contract'' :: Sing r -> Tensor r v -> Tensor r' v
contract'' Sing r
sr Tensor r v
ZeroTensor =
  case Sing r -> (Sane r ~ 'True) :- (Sane (ContractR r) ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (ContractR r) ~ 'True)
saneContractProof Sing r
sr of
    Sub (Sane r ~ 'True) => Dict (Sane (ContractR r) ~ 'True)
Dict -> Tensor r' v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
contract'' Sing r
_ (Scalar v
v) = v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar v
v
contract'' Sing r
sr (Tensor [(Int, Tensor r' v)]
ms) =
    case Sing r -> Sing (Apply TailRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r
sr of
       Sing (Apply TailRSym0 r)
SNil ->
         case Sing r -> (TailR r ~ '[]) :- (ContractR r ~ r)
forall (r :: Rank). Sing r -> (TailR r ~ '[]) :- (ContractR r ~ r)
singletonContractProof Sing r
sr of
           Sub (TailR r ~ '[]) => Dict (ContractR r ~ r)
Dict -> [(Int, Tensor r' 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, Tensor r' v)]
ms
       Sing (Apply TailRSym0 r)
st   ->
         case Sing r -> (Sane r ~ 'True) :- (Sane (ContractR r) ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (ContractR r) ~ 'True)
saneContractProof Sing r
sr of
           Sub (Sane r ~ 'True) => Dict (Sane (ContractR r) ~ 'True)
Dict ->
             let st' :: Sing (Apply TailRSym0 r')
st' = Sing r' -> Sing (Apply TailRSym0 r')
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r'
Sing (Apply TailRSym0 r)
st
                 sh :: Sing (Apply HeadRSym0 r)
sh  = Sing r -> Sing (Apply HeadRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply HeadRSym0 t)
sHeadR Sing r
sr
                 sv :: Sing (Apply FstSym0 (HeadR r))
sv  = Sing (HeadR r) -> Sing (Apply FstSym0 (HeadR r))
forall a b (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t)
sFst Sing (Apply HeadRSym0 r)
Sing (HeadR r)
sh
                 si :: Sing (Apply SndSym0 (HeadR r))
si  = Sing (HeadR r) -> Sing (Apply SndSym0 (HeadR r))
forall a b (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t)
sSnd Sing (Apply HeadRSym0 r)
Sing (HeadR r)
sh
                 sh' :: Sing (Apply HeadRSym0 r')
sh' = Sing r' -> Sing (Apply HeadRSym0 r')
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply HeadRSym0 t)
sHeadR Sing r'
Sing (Apply TailRSym0 r)
st
                 sv' :: Sing (Apply FstSym0 (HeadR r'))
sv' = Sing (HeadR r') -> Sing (Apply FstSym0 (HeadR r'))
forall a b (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t)
sFst Sing (Apply HeadRSym0 r')
Sing (HeadR r')
sh'
                 si' :: Sing (Apply SndSym0 (HeadR r'))
si' = Sing (HeadR r') -> Sing (Apply SndSym0 (HeadR r'))
forall a b (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t)
sSnd Sing (Apply HeadRSym0 r')
Sing (HeadR r')
sh'
             in case Sing (Fst (HeadR r))
Sing (Apply FstSym0 (HeadR r))
sv Sing (Fst (HeadR r))
-> Sing (Fst (HeadR r')) -> Sing (Fst (HeadR r) == Fst (HeadR r'))
forall k (a :: k) (b :: k).
SEq k =>
Sing a -> Sing b -> Sing (a == b)
%== Sing (Fst (HeadR r'))
Sing (Apply FstSym0 (HeadR r'))
sv' of
                  Sing (Fst (HeadR r) == Fst (HeadR r'))
SFalse ->
                    case Sing r
-> (r' ~ TailR r, TailR r' ~ TailR r',
    (Fst (HeadR r) == Fst (HeadR r')) ~ 'False)
   :- (TailR (ContractR r) ~ ContractR r')
forall (r :: Rank) (t :: Rank) (t' :: Rank).
Sing r
-> (t ~ TailR r, t' ~ TailR t,
    (Fst (HeadR r) == Fst (HeadR t)) ~ 'False)
   :- (TailR (ContractR r) ~ ContractR t)
contractTailDiffVProof Sing r
sr of
                      Sub (r' ~ TailR r, TailR r' ~ TailR r',
 (Fst (HeadR r) == Fst (HeadR r')) ~ 'False) =>
Dict (TailR (ContractR r) ~ ContractR r')
Dict -> [(Int, Tensor (ContractR r') 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, Tensor (ContractR r') v)] -> Tensor r' v)
-> [(Int, Tensor (ContractR r') v)] -> Tensor r' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor (ContractR r') v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor (ContractR r') v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor (ContractR r') v)
-> (Int, Tensor r' v) -> (Int, Tensor (ContractR r') v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing r' -> Tensor r' v -> Tensor (ContractR r') v
forall (r :: Rank) (r' :: Rank) v.
(r' ~ ContractR r, Num v, Eq v) =>
Sing r -> Tensor r v -> Tensor r' v
contract'' Sing r'
Sing (Apply TailRSym0 r)
st)) [(Int, Tensor r' v)]
ms
                  Sing (Fst (HeadR r) == Fst (HeadR r'))
STrue -> case Sing (Apply SndSym0 (HeadR r))
si of
                    SICon sa -> case Sing (Apply SndSym0 (HeadR r'))
si' of
                      SICov sb -> case Sing n
sa Sing n -> Sing n -> Sing (n == n)
forall k (a :: k) (b :: k).
SEq k =>
Sing a -> Sing b -> Sing (a == b)
%== Sing n
sb of
                        Sing (n == n)
STrue -> 
                          let ms' :: [Tensor (TailR (TailR r)) v]
ms' = ((Int, Tensor r' v) -> Maybe (Tensor (TailR r') v))
-> [(Int, Tensor r' v)] -> [Tensor (TailR r') v]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(Int
i, Tensor r' v
v) -> case Tensor r' v
v of
                                                           Tensor [(Int, Tensor r' v)]
vs ->
                                                             case ((Int, Tensor r' v) -> Bool)
-> [(Int, Tensor r' v)] -> [(Int, Tensor r' v)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
i', Tensor r' v
_) -> Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i') [(Int, Tensor r' v)]
vs of
                                                                  [] -> Maybe (Tensor (TailR r') v)
forall a. Maybe a
Nothing
                                                                  [(Int
_, Tensor r' v
v')] -> Tensor r' v -> Maybe (Tensor r' v)
forall a. a -> Maybe a
Just Tensor r' v
v'
                                                                  [(Int, Tensor r' v)]
_ -> String -> Maybe (Tensor (TailR r') v)
forall a. HasCallStack => String -> a
error String
"duplicate key in tensor assoc list"
                                                           Tensor r' v
ZeroTensor -> Maybe (Tensor (TailR r') v)
forall a. Maybe a
Nothing)
                                             [(Int, Tensor r' v)]
ms :: [Tensor (TailR (TailR r)) v]
                          in  case Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
saneTailRProof Sing r
sr of
                                Sub (Sane r ~ 'True) => Dict (Sane (TailR r) ~ 'True)
Dict ->
                                  case Sing r' -> (Sane r' ~ 'True) :- (Sane (TailR r') ~ 'True)
forall (r :: Rank).
Sing r -> (Sane r ~ 'True) :- (Sane (TailR r) ~ 'True)
saneTailRProof Sing r'
Sing (Apply TailRSym0 r)
st of
                                    Sub (Sane r' ~ 'True) => Dict (Sane (TailR r') ~ 'True)
Dict ->
                                      case Sing r
-> (r' ~ TailR r, TailR r' ~ TailR r',
    (Fst (HeadR r) == Fst (HeadR r')) ~ 'True, Snd (HeadR r) ~ 'ICon n,
    Snd (HeadR r') ~ 'ICov n, (n == n) ~ 'True)
   :- (ContractR (TailR r') ~ ContractR r)
forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol)
       (j :: Symbol).
Sing r
-> (t ~ TailR r, t' ~ TailR t,
    (Fst (HeadR r) == Fst (HeadR t)) ~ 'True, Snd (HeadR r) ~ 'ICon i,
    Snd (HeadR t) ~ 'ICov j, (i == j) ~ 'True)
   :- (ContractR t' ~ ContractR r)
contractTailSameVSameIProof Sing r
sr of
                                        Sub (r' ~ TailR r, TailR r' ~ TailR r',
 (Fst (HeadR r) == Fst (HeadR r')) ~ 'True, Snd (HeadR r) ~ 'ICon n,
 Snd (HeadR r') ~ 'ICov n, (n == n) ~ 'True) =>
Dict (ContractR (TailR r') ~ ContractR r)
Dict -> Sing (TailR r') -> Tensor (TailR r') v -> Tensor r' v
forall (r :: Rank) (r' :: Rank) v.
(r' ~ ContractR r, Num v, Eq v) =>
Sing r -> Tensor r v -> Tensor r' v
contract' Sing (Apply TailRSym0 r')
Sing (TailR r')
st' (Tensor (TailR r') v -> Tensor r' v)
-> Tensor (TailR r') v -> Tensor r' v
forall a b. (a -> b) -> a -> b
$ (Tensor (TailR r') v -> Tensor (TailR r') v -> Tensor (TailR r') v)
-> Tensor (TailR r') v
-> [Tensor (TailR r') v]
-> Tensor (TailR r') v
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Tensor (TailR r') v -> Tensor (TailR r') v -> Tensor (TailR r') v
forall (r :: Rank) (r' :: Rank) v.
(r ~ r', Num v, Eq v) =>
Tensor r v -> Tensor r' v -> Tensor r v
(&+) Tensor (TailR r') v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor [Tensor (TailR r') v]
[Tensor (TailR (TailR r)) v]
ms'
                        Sing (n == n)
SFalse ->
                          case Sing r
-> (r' ~ TailR r, TailR r' ~ TailR r',
    (Fst (HeadR r) == Fst (HeadR r')) ~ 'True, Snd (HeadR r) ~ 'ICon n,
    Snd (HeadR r') ~ 'ICov n, (n == n) ~ 'False)
   :- (TailR (ContractR r) ~ ContractR r')
forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol)
       (j :: Symbol).
Sing r
-> (t ~ TailR r, t' ~ TailR t,
    (Fst (HeadR r) == Fst (HeadR t)) ~ 'True, Snd (HeadR r) ~ 'ICon i,
    Snd (HeadR t) ~ 'ICov j, (i == j) ~ 'False)
   :- (TailR (ContractR r) ~ ContractR t)
contractTailSameVDiffIProof Sing r
sr of
                            Sub (r' ~ TailR r, TailR r' ~ TailR r',
 (Fst (HeadR r) == Fst (HeadR r')) ~ 'True, Snd (HeadR r) ~ 'ICon n,
 Snd (HeadR r') ~ 'ICov n, (n == n) ~ 'False) =>
Dict (TailR (ContractR r) ~ ContractR r')
Dict -> [(Int, Tensor (ContractR r') 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, Tensor (ContractR r') v)] -> Tensor r' v)
-> [(Int, Tensor (ContractR r') v)] -> Tensor r' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor (ContractR r') v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor (ContractR r') v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor (ContractR r') v)
-> (Int, Tensor r' v) -> (Int, Tensor (ContractR r') v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing r' -> Tensor r' v -> Tensor (ContractR r') v
forall (r :: Rank) (r' :: Rank) v.
(r' ~ ContractR r, Num v, Eq v) =>
Sing r -> Tensor r v -> Tensor r' v
contract'' Sing r'
Sing (Apply TailRSym0 r)
st)) [(Int, Tensor r' v)]
ms
                      SICon _ ->
                        case Sing r
-> (r' ~ TailR r, TailR r' ~ TailR r',
    (Fst (HeadR r) == Fst (HeadR r')) ~ 'True,
    Snd (HeadR r') ~ 'ICon n)
   :- (TailR (ContractR r) ~ ContractR r')
forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol).
Sing r
-> (t ~ TailR r, t' ~ TailR t,
    (Fst (HeadR r) == Fst (HeadR t)) ~ 'True, Snd (HeadR t) ~ 'ICon i)
   :- (TailR (ContractR r) ~ ContractR t)
contractTailSameVNoCovProof Sing r
sr of
                          Sub (r' ~ TailR r, TailR r' ~ TailR r',
 (Fst (HeadR r) == Fst (HeadR r')) ~ 'True,
 Snd (HeadR r') ~ 'ICon n) =>
Dict (TailR (ContractR r) ~ ContractR r')
Dict -> [(Int, Tensor (ContractR r') 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, Tensor (ContractR r') v)] -> Tensor r' v)
-> [(Int, Tensor (ContractR r') v)] -> Tensor r' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor (ContractR r') v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor (ContractR r') v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor (ContractR r') v)
-> (Int, Tensor r' v) -> (Int, Tensor (ContractR r') v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing r' -> Tensor r' v -> Tensor (ContractR r') v
forall (r :: Rank) (r' :: Rank) v.
(r' ~ ContractR r, Num v, Eq v) =>
Sing r -> Tensor r v -> Tensor r' v
contract'' Sing r'
Sing (Apply TailRSym0 r)
st)) [(Int, Tensor r' v)]
ms
                    SICov _ ->
                      case Sing r
-> (r' ~ TailR r, TailR r' ~ TailR r',
    (Fst (HeadR r) == Fst (HeadR r')) ~ 'True, Snd (HeadR r) ~ 'ICov n)
   :- (TailR (ContractR r) ~ ContractR r')
forall (r :: Rank) (t :: Rank) (t' :: Rank) (i :: Symbol).
Sing r
-> (t ~ TailR r, t' ~ TailR t,
    (Fst (HeadR r) == Fst (HeadR t)) ~ 'True, Snd (HeadR r) ~ 'ICov i)
   :- (TailR (ContractR r) ~ ContractR t)
contractTailSameVNoConProof Sing r
sr of
                        Sub (r' ~ TailR r, TailR r' ~ TailR r',
 (Fst (HeadR r) == Fst (HeadR r')) ~ 'True,
 Snd (HeadR r) ~ 'ICov n) =>
Dict (TailR (ContractR r) ~ ContractR r')
Dict -> [(Int, Tensor (ContractR r') 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, Tensor (ContractR r') v)] -> Tensor r' v)
-> [(Int, Tensor (ContractR r') v)] -> Tensor r' v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor (ContractR r') v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor (ContractR r') v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor (ContractR r') v)
-> (Int, Tensor r' v) -> (Int, Tensor (ContractR r') v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing r' -> Tensor r' v -> Tensor (ContractR r') v
forall (r :: Rank) (r' :: Rank) v.
(r' ~ ContractR r, Num v, Eq v) =>
Sing r -> Tensor r v -> Tensor r' v
contract'' Sing r'
Sing (Apply TailRSym0 r)
st)) [(Int, Tensor r' v)]
ms

-- |Tensor contraction. Contracting a tensor is the identity function on non-contractible tensors.
-- Otherwise, the result is the contracted tensor with the contracted labels removed from the
-- generalized rank.
contract :: 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 -> Tensor r' v
contract = Sing r -> Tensor r v -> Tensor r' v
forall (r :: Rank) (r' :: Rank) v.
(r' ~ ContractR r, Num v, Eq v) =>
Sing r -> Tensor r v -> Tensor r' v
contract' (Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r)

-- |Tensor transposition. Given a vector space and two index labels, the result is a tensor with
-- the corresponding entries swapped. Only possible if the indices are part of the rank. The
-- generalized rank remains untouched.
transpose :: 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 vs -> Sing a -> Sing b -> Tensor r v -> Tensor r v
transpose Sing vs
_ Sing a
_ Sing b
_ Tensor r v
ZeroTensor = Tensor r v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
transpose Sing vs
_ Sing a
_ Sing b
_ (Scalar v
_) = String -> Tensor r v
forall a. HasCallStack => String -> a
error String
"This is not possible, might yet have to convince the type system."
transpose Sing vs
v Sing a
a Sing b
b t :: Tensor r v
t@(Tensor [(Int, Tensor r' v)]
ms) =
  case Sing a
a Sing a -> Sing b -> Sing (Apply (Apply CompareSym0 a) b)
forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
`sCompare` Sing b
b of
    Sing (Apply (Apply CompareSym0 a) b)
SEQ -> Tensor r v
t
    Sing (Apply (Apply CompareSym0 a) b)
SGT -> case Sing vs
-> Sing b
-> Sing a
-> Sing r
-> Sing (Apply (Apply (Apply (Apply CanTransposeSym0 vs) b) 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 vs
v Sing b
b Sing a
a (Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r) Sing (CanTranspose vs b a r)
-> Sing 'True -> Decision (CanTranspose vs b 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 CanTranspose vs b a r :~: 'True
Refl -> Sing vs -> Sing b -> 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 vs
v Sing b
b Sing a
a Tensor r v
t
    Sing (Apply (Apply CompareSym0 a) b)
SLT ->
      let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
          sh :: Sing (Apply HeadRSym0 r)
sh = Sing r -> Sing (Apply HeadRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply HeadRSym0 t)
sHeadR Sing r
sr
          sv :: Sing (Apply FstSym0 (HeadR r))
sv = Sing (HeadR r) -> Sing (Apply FstSym0 (HeadR r))
forall a b (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t)
sFst Sing (Apply HeadRSym0 r)
Sing (HeadR r)
sh
          si :: Sing (Apply SndSym0 (HeadR r))
si = Sing (HeadR r) -> Sing (Apply SndSym0 (HeadR r))
forall a b (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t)
sSnd Sing (Apply HeadRSym0 r)
Sing (HeadR r)
sh
          st :: Sing (Apply TailRSym0 r)
st = Sing r -> Sing (Apply TailRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r
sr
      in Sing r' -> (SingI r' => Tensor r v) -> Tensor r v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r'
Sing (Apply TailRSym0 r)
st ((SingI r' => Tensor r v) -> Tensor r v)
-> (SingI r' => Tensor r v) -> Tensor r v
forall a b. (a -> b) -> a -> b
$
         case Sing (Fst (HeadR r))
Sing (Apply FstSym0 (HeadR r))
sv Sing (Fst (HeadR r)) -> Sing vs -> Decision (Fst (HeadR r) :~: vs)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing vs
v of
           Proved Fst (HeadR r) :~: vs
Refl -> case Sing (Snd (HeadR r))
Sing (Apply SndSym0 (HeadR r))
si Sing (Snd (HeadR r)) -> Sing a -> Decision (Snd (HeadR r) :~: a)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a
a of
             Proved Snd (HeadR r) :~: a
Refl -> let sr' :: Sing (Apply (Apply RemoveUntilSym0 b) r)
sr' = Sing b -> Sing r -> Sing (Apply (Apply RemoveUntilSym0 b) r)
forall s n (t1 :: Ix s) (t2 :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply RemoveUntilSym0 t1) t2)
sRemoveUntil Sing b
b Sing r
sr
                            in Sing
  (Case_6989586621679113446
     b r b r b r (Equals_6989586621679117897 a b))
-> (SingI
      (Case_6989586621679113446
         b r b r b r (Equals_6989586621679117897 a b)) =>
    Tensor r v)
-> Tensor r v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing
  (Case_6989586621679113446
     b r b r b r (Equals_6989586621679117897 a b))
Sing (Apply (Apply RemoveUntilSym0 b) r)
sr' ((SingI
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b)) =>
  Tensor r v)
 -> Tensor r v)
-> (SingI
      (Case_6989586621679113446
         b r b r b r (Equals_6989586621679117897 a b)) =>
    Tensor r v)
-> Tensor r v
forall a b. (a -> b) -> a -> b
$
                               case Sing
  (Case_6989586621679113446
     b r b r b r (Equals_6989586621679117897 a b))
-> Sing
     (Apply
        SaneSym0
        (Case_6989586621679113446
           b r b r b r (Equals_6989586621679117897 a b)))
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing
  (Case_6989586621679113446
     b r b r b r (Equals_6989586621679117897 a b))
Sing (Apply (Apply RemoveUntilSym0 b) r)
sr' Sing
  (Sane
     (Case_6989586621679113446
        b r b r b r (Equals_6989586621679117897 a b)))
-> Sing 'True
-> Decision
     (Sane
        (Case_6989586621679113446
           b r b r b r (Equals_6989586621679117897 a b))
      :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
                                 Proved Sane
  (Case_6989586621679113446
     b r b r b r (Equals_6989586621679117897 a b))
:~: 'True
Refl ->
                                   let tl :: [([Int],
  Tensor
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b))
    v)]
tl  = Sing b
-> Tensor r v
-> [([Int],
     Tensor
       (Case_6989586621679113446
          b r b r b r (Equals_6989586621679117897 a b))
       v)]
forall (a :: Ix Symbol) (r :: Rank) (r' :: Rank) v.
(SingI r, SingI r', RemoveUntil a r ~ r', Sane r ~ 'True,
 Sane r' ~ 'True) =>
Sing a -> Tensor r v -> [([Int], Tensor r' v)]
toTListUntil Sing b
b Tensor r v
t
                                       tl' :: [([Int],
  Tensor
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b))
    v)]
tl' = (([Int],
  Tensor
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b))
    v)
 -> ([Int],
     Tensor
       (Case_6989586621679113446
          b r b r b r (Equals_6989586621679117897 a b))
       v))
-> [([Int],
     Tensor
       (Case_6989586621679113446
          b r b r b r (Equals_6989586621679117897 a b))
       v)]
-> [([Int],
     Tensor
       (Case_6989586621679113446
          b r b r b r (Equals_6989586621679117897 a b))
       v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
i:[Int]
is, Tensor
  (Case_6989586621679113446
     b r b r b r (Equals_6989586621679117897 a b))
  v
val) -> ([Int] -> Int
forall a. [a] -> a
last [Int]
is Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: ([Int] -> [Int]
forall a. [a] -> [a]
init [Int]
is [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
i]),Tensor
  (Case_6989586621679113446
     b r b r b r (Equals_6989586621679117897 a b))
  v
val)) [([Int],
  Tensor
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b))
    v)]
tl
                                       tl'' :: [([Int],
  Tensor
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b))
    v)]
tl'' = (([Int],
  Tensor
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b))
    v)
 -> ([Int],
     Tensor
       (Case_6989586621679113446
          b r b r b r (Equals_6989586621679117897 a b))
       v)
 -> Ordering)
-> [([Int],
     Tensor
       (Case_6989586621679113446
          b r b r b r (Equals_6989586621679117897 a b))
       v)]
-> [([Int],
     Tensor
       (Case_6989586621679113446
          b r b r b r (Equals_6989586621679117897 a b))
       v)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\([Int]
i,Tensor
  (Case_6989586621679113446
     b r b r b r (Equals_6989586621679117897 a b))
  v
_) ([Int]
i',Tensor
  (Case_6989586621679113446
     b r b r b r (Equals_6989586621679117897 a b))
  v
_) -> [Int]
i [Int] -> [Int] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` [Int]
i') [([Int],
  Tensor
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b))
    v)]
tl'
                                   in  [([Int],
  Tensor
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b))
    v)]
-> Tensor r v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, Sane r' ~ 'True, SingI r, SingI r') =>
[([Int], Tensor r v)] -> Tensor r' v
fromTList [([Int],
  Tensor
    (Case_6989586621679113446
       b r b r b r (Equals_6989586621679117897 a b))
    v)]
tl''
             Disproved Refuted (Snd (HeadR r) :~: a)
_ -> case Sing vs
-> Sing a
-> Sing b
-> Sing r'
-> Sing (Apply (Apply (Apply (Apply CanTransposeSym0 vs) a) b) 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 vs
v Sing a
a Sing b
b Sing r'
Sing (Apply TailRSym0 r)
st of
                              Sing (Apply (Apply (Apply (Apply CanTransposeSym0 vs) a) b) r')
STrue -> [(Int, Tensor r' 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, Tensor r' v)] -> Tensor r v)
-> [(Int, Tensor r' v)] -> Tensor r v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor r' v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor r' v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor r' v)
-> (Int, Tensor r' v) -> (Int, Tensor r' v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing vs -> Sing a -> Sing b -> 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 vs
v Sing a
a Sing b
b)) [(Int, Tensor r' v)]
ms
           Disproved Refuted (Fst (HeadR r) :~: vs)
_ -> case Sing vs
-> Sing a
-> Sing b
-> Sing r'
-> Sing (Apply (Apply (Apply (Apply CanTransposeSym0 vs) a) b) 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 vs
v Sing a
a Sing b
b Sing r'
Sing (Apply TailRSym0 r)
st of
                            Sing (Apply (Apply (Apply (Apply CanTransposeSym0 vs) a) b) r')
STrue -> [(Int, Tensor r' 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, Tensor r' v)] -> Tensor r v)
-> [(Int, Tensor r' v)] -> Tensor r v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor r' v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor r' v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor r' v)
-> (Int, Tensor r' v) -> (Int, Tensor r' v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing vs -> Sing a -> Sing b -> 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 vs
v Sing a
a Sing b
b)) [(Int, Tensor r' v)]
ms

-- |Transposition of multiple labels. Given a vector space and a transposition rule, the
-- result is a tensor with the corresponding entries swapped. Only possible if the indices are
-- part of the generalized rank. The generalized rank remains untouched.
transposeMult :: 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 vs -> Sing tl -> Tensor r v -> Tensor r v
transposeMult Sing vs
_ Sing tl
_ Tensor r v
ZeroTensor = Tensor r v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
transposeMult Sing vs
sv Sing tl
stl tens :: Tensor r v
tens@(Tensor [(Int, Tensor r' v)]
ms) =
    let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
        sh :: Sing (Apply HeadRSym0 r)
sh = Sing r -> Sing (Apply HeadRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply HeadRSym0 t)
sHeadR Sing r
sr
        st :: Sing (Apply TailRSym0 r)
st = Sing r -> Sing (Apply TailRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r
sr
        sr' :: Sing (Apply TailSym0 r)
sr' = Sing r -> Sing (Apply TailSym0 r)
forall a (t :: [a]). Sing t -> Sing (Apply TailSym0 t)
sTail Sing r
sr
        sts :: Sing (Apply (Apply (Apply TranspositionsSym0 vs) tl) r)
sts = Sing vs
-> Sing tl
-> Sing r
-> Sing (Apply (Apply (Apply TranspositionsSym0 vs) tl) 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 vs
sv Sing tl
stl Sing r
sr
    in case Sing vs
sv Sing vs -> Sing (Fst (HeadR r)) -> Decision (vs :~: Fst (HeadR r))
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing (HeadR r) -> Sing (Apply FstSym0 (HeadR r))
forall a b (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t)
sFst Sing (Apply HeadRSym0 r)
Sing (HeadR r)
sh of
         Proved vs :~: Fst (HeadR r)
Refl ->
           case Sing (Tail r) -> Sing (Apply SaneSym0 (Tail r))
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing (Tail r)
Sing (Apply TailSym0 r)
sr' Sing (Sane (Tail r))
-> Sing 'True -> Decision (Sane (Tail 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 (Tail r) :~: 'True
Refl ->
               case Sing (Apply (Apply (Apply TranspositionsSym0 vs) tl) r)
sts of
                 SJust sts' ->
                   Sing (Fst (Head r))
-> (SingI (Fst (Head r)) => Tensor r v) -> Tensor r v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI (Sing (Head r) -> Sing (Apply FstSym0 (Head r))
forall a b (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t)
sFst (Sing r -> Sing (Apply HeadSym0 r)
forall a (t :: [a]). Sing t -> Sing (Apply HeadSym0 t)
sHead Sing r
sr)) ((SingI (Fst (Head r)) => Tensor r v) -> Tensor r v)
-> (SingI (Fst (Head r)) => Tensor r v) -> Tensor r v
forall a b. (a -> b) -> a -> b
$
                   Sing (Tail r) -> (SingI (Tail r) => Tensor r v) -> Tensor r v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing (Tail r)
Sing (Apply TailSym0 r)
sr' ((SingI (Tail r) => Tensor r v) -> Tensor r v)
-> (SingI (Tail r) => Tensor r v) -> Tensor r v
forall a b. (a -> b) -> a -> b
$
                   let sn :: Sing (Apply LengthILSym0 (Snd (Head r)))
sn = Sing (Snd (Head r)) -> Sing (Apply LengthILSym0 (Snd (Head r)))
forall a (t :: IList a). Sing t -> Sing (Apply LengthILSym0 t)
sLengthIL (Sing (Head r) -> Sing (Apply SndSym0 (Head r))
forall a b (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t)
sSnd (Sing r -> Sing (Apply HeadSym0 r)
forall a (t :: [a]). Sing t -> Sing (Apply HeadSym0 t)
sHead Sing r
sr))
                       n :: Demote N
n  = Sing (LengthIL (Snd (Head r))) -> Demote N
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing (Apply LengthILSym0 (Snd (Head r)))
Sing (LengthIL (Snd (Head r)))
sn
                       ts :: Demote [(N, N)]
ts  = Sing n -> Demote [(N, N)]
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
sts'
                       ts' :: [Int]
ts' = [(N, N)] -> [Int] -> [Int]
go [(N, N)]
Demote [(N, N)]
ts ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ N -> Int -> [Int]
take' N
Demote N
n Int
0
                       xs :: [([Int], Tensor (Tail r) v)]
xs  = Tensor r v -> [([Int], Tensor (Tail r) v)]
forall (r :: Rank) v.
(SingI r, Sane r ~ 'True) =>
Tensor r v -> [([Int], Tensor (Tail r) v)]
toTListWhile Tensor r v
tens
                       xs' :: [([Int], Tensor (Tail r) v)]
xs' = (([Int], Tensor (Tail r) v) -> ([Int], Tensor (Tail r) v))
-> [([Int], Tensor (Tail r) v)] -> [([Int], Tensor (Tail r) v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Int] -> [Int])
-> ([Int], Tensor (Tail r) v) -> ([Int], Tensor (Tail r) v)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([Int] -> [Int] -> [Int]
transposeIndices [Int]
ts')) [([Int], Tensor (Tail r) v)]
xs
                       xs'' :: [([Int], Tensor (Tail r) v)]
xs'' = (([Int], Tensor (Tail r) v)
 -> ([Int], Tensor (Tail r) v) -> Ordering)
-> [([Int], Tensor (Tail r) v)] -> [([Int], Tensor (Tail r) v)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\([Int]
i,Tensor (Tail r) v
_) ([Int]
i',Tensor (Tail r) v
_) -> [Int]
i [Int] -> [Int] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` [Int]
i') [([Int], Tensor (Tail r) v)]
xs'
                   in  [([Int], Tensor (Tail r) v)] -> Tensor r v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, Sane r' ~ 'True, SingI r, SingI r') =>
[([Int], Tensor r v)] -> Tensor r' v
fromTList [([Int], Tensor (Tail r) v)]
xs''
         Disproved Refuted (vs :~: Fst (HeadR r))
_ ->
           Sing r' -> (SingI r' => Tensor r v) -> Tensor r v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r'
Sing (Apply TailRSym0 r)
st ((SingI r' => Tensor r v) -> Tensor r v)
-> (SingI r' => Tensor r v) -> Tensor r v
forall a b. (a -> b) -> a -> b
$
           case Sing (Transpositions vs tl r')
-> Sing (Apply IsJustSym0 (Transpositions vs tl r'))
forall a (t :: Maybe a). Sing t -> Sing (Apply IsJustSym0 t)
sIsJust (Sing vs
-> Sing tl
-> Sing r'
-> Sing (Apply (Apply (Apply TranspositionsSym0 vs) tl) 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 vs
sv Sing tl
stl Sing r'
Sing (Apply TailRSym0 r)
st) Sing (IsJust (Transpositions vs tl r'))
-> Sing 'True
-> Decision (IsJust (Transpositions vs tl 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 vs tl r') :~: 'True
Refl -> [(Int, Tensor r' 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, Tensor r' v)] -> Tensor r v)
-> [(Int, Tensor r' v)] -> Tensor r v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor r' v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor r' v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor r' v)
-> (Int, Tensor r' v) -> (Int, Tensor r' v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing vs -> Sing tl -> 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 vs
sv Sing tl
stl)) [(Int, Tensor r' v)]
ms
  where
    take' :: N -> Int -> [Int]
    take' :: N -> Int -> [Int]
take' N
Z Int
i = [Int
i]
    take' (S N
n) Int
i = Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: N -> Int -> [Int]
take' N
n (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

    transposeIndices :: [Int] -> [Int] -> [Int]
    transposeIndices :: [Int] -> [Int] -> [Int]
transposeIndices [Int]
ts' [Int]
is = ((Int, Int) -> Int) -> [(Int, Int)] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Int) -> Int
forall a b. (a, b) -> b
snd ([(Int, Int)] -> [Int]) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> a -> b
$
                              ((Int, Int) -> (Int, Int) -> Ordering)
-> [(Int, Int)] -> [(Int, Int)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(Int
i,Int
_) (Int
i',Int
_) -> Int
i Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
i') ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$
                              [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
ts' [Int]
is

    go :: [(N,N)] -> [Int] -> [Int]
    go :: [(N, N)] -> [Int] -> [Int]
go [] [Int]
is = [Int]
is
    go ((N
s,N
t):[(N, N)]
ts) (Int
i:[Int]
is) =
      case Int
s' Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
i of
        Ordering
EQ -> Int
t' Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [(N, N)] -> [Int] -> [Int]
go [(N, N)]
ts [Int]
is
        Ordering
GT -> Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [(N, N)] -> [Int] -> [Int]
go ((N
s,N
t)(N, N) -> [(N, N)] -> [(N, N)]
forall a. a -> [a] -> [a]
:[(N, N)]
ts) [Int]
is
        Ordering
LT -> String -> [Int]
forall a. HasCallStack => String -> a
error (String -> [Int]) -> String -> [Int]
forall a b. (a -> b) -> a -> b
$ String
"illegal permutation" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [(N, N)] -> String
forall a. Show a => a -> String
show ((N
s,N
t)(N, N) -> [(N, N)] -> [(N, N)]
forall a. a -> [a] -> [a]
:[(N, N)]
ts) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\t" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Int] -> String
forall a. Show a => a -> String
show (Int
iInt -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[Int]
is)
     where
      s' :: Int
s' = N -> Int
toInt N
s
      t' :: Int
t' = N -> Int
toInt N
t
    go [(N, N)]
_ [] = String -> [Int]
forall a. HasCallStack => String -> a
error String
"cannot transpose elements of empty list"

-- |Tensor relabelling. Given a vector space and a relabelling rule, the result is a tensor
-- with the resulting generalized rank after relabelling. Only possible if labels to be
-- renamed are part of the generalized rank and if uniqueness of labels after
-- relabelling is preserved.
relabel :: forall (vs :: VSpace Symbol Nat) (rl :: RelabelRule 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 vs -> Sing rl -> Tensor r1 v -> Tensor r2 v
relabel Sing vs
_ Sing rl
_ Tensor r1 v
ZeroTensor = Tensor r2 v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
relabel Sing vs
sv Sing rl
srl tens :: Tensor r1 v
tens@(Tensor [(Int, Tensor r' v)]
ms) =
    let sr1 :: Sing r1
sr1 = Sing r1
forall k (a :: k). SingI a => Sing a
sing :: Sing r1
        sr2 :: Sing r2
sr2 = Sing r2
forall k (a :: k). SingI a => Sing a
sing :: Sing r2
        sh :: Sing (Apply HeadRSym0 r1)
sh = Sing r1 -> Sing (Apply HeadRSym0 r1)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply HeadRSym0 t)
sHeadR Sing r1
sr1
        sr1' :: Sing (Apply TailRSym0 r1)
sr1' = Sing r1 -> Sing (Apply TailRSym0 r1)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r1
sr1
        sr2' :: Sing (Apply TailRSym0 r2)
sr2' = Sing r2 -> Sing (Apply TailRSym0 r2)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r2
sr2
        sr1'' :: Sing (Apply TailSym0 r1)
sr1'' = Sing r1 -> Sing (Apply TailSym0 r1)
forall a (t :: [a]). Sing t -> Sing (Apply TailSym0 t)
sTail Sing r1
sr1
        sts :: Sing (Apply (Apply RelabelTranspositionsSym0 rl) (Snd (Head r1)))
sts = Sing rl
-> Sing (Snd (Head r1))
-> Sing
     (Apply (Apply RelabelTranspositionsSym0 rl) (Snd (Head r1)))
forall a (t1 :: NonEmpty (a, a)) (t2 :: IList a).
SOrd a =>
Sing t1
-> Sing t2 -> Sing (Apply (Apply RelabelTranspositionsSym0 t1) t2)
sRelabelTranspositions Sing rl
srl (Sing (Head r1) -> Sing (Apply SndSym0 (Head r1))
forall a b (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t)
sSnd (Sing r1 -> Sing (Apply HeadSym0 r1)
forall a (t :: [a]). Sing t -> Sing (Apply HeadSym0 t)
sHead Sing r1
sr1))
    in case Sing vs
sv Sing vs
-> Sing (Fst (HeadR r1)) -> Decision (vs :~: Fst (HeadR r1))
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing (HeadR r1) -> Sing (Apply FstSym0 (HeadR r1))
forall a b (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t)
sFst Sing (Apply HeadRSym0 r1)
Sing (HeadR r1)
sh of
         Proved vs :~: Fst (HeadR r1)
Refl ->
           case Sing (Tail r1) -> Sing (Apply SaneSym0 (Tail r1))
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing (Tail r1)
Sing (Apply TailSym0 r1)
sr1'' Sing (Sane (Tail r1))
-> Sing 'True -> Decision (Sane (Tail r1) :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
             Proved Sane (Tail r1) :~: 'True
Refl ->
               case Sing (Apply (Apply RelabelTranspositionsSym0 rl) (Snd (Head r1)))
sts of
                 SJust sts' ->
                   Sing (Fst (Head r1))
-> (SingI (Fst (Head r1)) => Tensor r2 v) -> Tensor r2 v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI (Sing (Head r1) -> Sing (Apply FstSym0 (Head r1))
forall a b (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t)
sFst (Sing r1 -> Sing (Apply HeadSym0 r1)
forall a (t :: [a]). Sing t -> Sing (Apply HeadSym0 t)
sHead Sing r1
sr1)) ((SingI (Fst (Head r1)) => Tensor r2 v) -> Tensor r2 v)
-> (SingI (Fst (Head r1)) => Tensor r2 v) -> Tensor r2 v
forall a b. (a -> b) -> a -> b
$
                   Sing (Tail r1) -> (SingI (Tail r1) => Tensor r2 v) -> Tensor r2 v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing (Tail r1)
Sing (Apply TailSym0 r1)
sr1'' ((SingI (Tail r1) => Tensor r2 v) -> Tensor r2 v)
-> (SingI (Tail r1) => Tensor r2 v) -> Tensor r2 v
forall a b. (a -> b) -> a -> b
$
                   let sn :: Sing (Apply LengthILSym0 (Snd (Head r1)))
sn = Sing (Snd (Head r1)) -> Sing (Apply LengthILSym0 (Snd (Head r1)))
forall a (t :: IList a). Sing t -> Sing (Apply LengthILSym0 t)
sLengthIL (Sing (Head r1) -> Sing (Apply SndSym0 (Head r1))
forall a b (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t)
sSnd (Sing r1 -> Sing (Apply HeadSym0 r1)
forall a (t :: [a]). Sing t -> Sing (Apply HeadSym0 t)
sHead Sing r1
sr1))
                       n :: Demote N
n  = Sing (LengthIL (Snd (Head r1))) -> Demote N
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing (Apply LengthILSym0 (Snd (Head r1)))
Sing (LengthIL (Snd (Head r1)))
sn
                       ts :: Demote [(N, N)]
ts  = Sing n -> Demote [(N, N)]
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
sts'
                       ts' :: [Int]
ts' = [(N, N)] -> [Int] -> [Int]
go [(N, N)]
Demote [(N, N)]
ts ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ N -> Int -> [Int]
take' N
Demote N
n Int
0
                       xs :: [([Int], Tensor (Tail r1) v)]
xs  = Tensor r1 v -> [([Int], Tensor (Tail r1) v)]
forall (r :: Rank) v.
(SingI r, Sane r ~ 'True) =>
Tensor r v -> [([Int], Tensor (Tail r) v)]
toTListWhile Tensor r1 v
tens
                       xs' :: [([Int], Tensor (Tail r1) v)]
xs' = (([Int], Tensor (Tail r1) v) -> ([Int], Tensor (Tail r1) v))
-> [([Int], Tensor (Tail r1) v)] -> [([Int], Tensor (Tail r1) v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Int] -> [Int])
-> ([Int], Tensor (Tail r1) v) -> ([Int], Tensor (Tail r1) v)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([Int] -> [Int] -> [Int]
transposeIndices [Int]
ts')) [([Int], Tensor (Tail r1) v)]
xs
                       xs'' :: [([Int], Tensor (Tail r1) v)]
xs'' = (([Int], Tensor (Tail r1) v)
 -> ([Int], Tensor (Tail r1) v) -> Ordering)
-> [([Int], Tensor (Tail r1) v)] -> [([Int], Tensor (Tail r1) v)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\([Int]
i,Tensor (Tail r1) v
_) ([Int]
i',Tensor (Tail r1) v
_) -> [Int]
i [Int] -> [Int] -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` [Int]
i') [([Int], Tensor (Tail r1) v)]
xs'
                   in  [([Int], Tensor (Tail r1) v)] -> Tensor r2 v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, Sane r' ~ 'True, SingI r, SingI r') =>
[([Int], Tensor r v)] -> Tensor r' v
fromTList [([Int], Tensor (Tail r1) v)]
xs''
         Disproved Refuted (vs :~: Fst (HeadR r1))
_ ->
           case Sing vs
-> Sing rl
-> Sing r'
-> Sing (Apply (Apply (Apply RelabelRSym0 vs) rl) 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 vs
sv Sing rl
srl Sing r'
Sing (Apply TailRSym0 r1)
sr1' Sing (RelabelR vs rl r')
-> Sing ('Just (TailR r2))
-> Decision (RelabelR vs rl r' :~: 'Just (TailR r2))
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing (TailR r2) -> SMaybe ('Just (TailR r2))
forall a (n :: a). Sing n -> SMaybe ('Just n)
SJust Sing (Apply TailRSym0 r2)
Sing (TailR r2)
sr2' of
             Proved RelabelR vs rl r' :~: 'Just (TailR r2)
Refl ->
               case Sing (TailR r2) -> Sing (Apply SaneSym0 (TailR r2))
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing (Apply TailRSym0 r2)
Sing (TailR r2)
sr2' Sing (Sane (TailR r2))
-> Sing 'True -> Decision (Sane (TailR r2) :~: 'True)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ SBool 'True
Sing 'True
STrue of
                 Proved Sane (TailR r2) :~: 'True
Refl -> Sing r' -> (SingI r' => Tensor r2 v) -> Tensor r2 v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r'
Sing (Apply TailRSym0 r1)
sr1' ((SingI r' => Tensor r2 v) -> Tensor r2 v)
-> (SingI r' => Tensor r2 v) -> Tensor r2 v
forall a b. (a -> b) -> a -> b
$ Sing (TailR r2) -> (SingI (TailR r2) => Tensor r2 v) -> Tensor r2 v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing (Apply TailRSym0 r2)
Sing (TailR r2)
sr2' ((SingI (TailR r2) => Tensor r2 v) -> Tensor r2 v)
-> (SingI (TailR r2) => Tensor r2 v) -> Tensor r2 v
forall a b. (a -> b) -> a -> b
$ [(Int, Tensor (TailR r2) v)] -> Tensor r2 v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, TailR r ~ r') =>
[(Int, Tensor r' v)] -> Tensor r v
Tensor ([(Int, Tensor (TailR r2) v)] -> Tensor r2 v)
-> [(Int, Tensor (TailR r2) v)] -> Tensor r2 v
forall a b. (a -> b) -> a -> b
$ ((Int, Tensor r' v) -> (Int, Tensor (TailR r2) v))
-> [(Int, Tensor r' v)] -> [(Int, Tensor (TailR r2) v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> Tensor (TailR r2) v)
-> (Int, Tensor r' v) -> (Int, Tensor (TailR r2) v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing vs -> Sing rl -> Tensor r' v -> Tensor (TailR r2) v
forall (vs :: VSpace Symbol Nat) (rl :: RelabelRule 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 vs
sv Sing rl
srl)) [(Int, Tensor r' v)]
ms
  where
    take' :: N -> Int -> [Int]
    take' :: N -> Int -> [Int]
take' N
Z Int
i = [Int
i]
    take' (S N
n) Int
i = Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: N -> Int -> [Int]
take' N
n (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

    transposeIndices :: [Int] -> [Int] -> [Int]
    transposeIndices :: [Int] -> [Int] -> [Int]
transposeIndices [Int]
ts' [Int]
is = ((Int, Int) -> Int) -> [(Int, Int)] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Int) -> Int
forall a b. (a, b) -> b
snd ([(Int, Int)] -> [Int]) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> a -> b
$
                              ((Int, Int) -> (Int, Int) -> Ordering)
-> [(Int, Int)] -> [(Int, Int)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(Int
i,Int
_) (Int
i',Int
_) -> Int
i Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
i') ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$
                              [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
ts' [Int]
is

    go :: [(N,N)] -> [Int] -> [Int]
    go :: [(N, N)] -> [Int] -> [Int]
go [] [Int]
is = [Int]
is
    go ((N
s,N
t):[(N, N)]
ts) (Int
i:[Int]
is) =
      case Int
s' Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Int
i of
        Ordering
EQ -> Int
t' Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [(N, N)] -> [Int] -> [Int]
go [(N, N)]
ts [Int]
is
        Ordering
GT -> Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [(N, N)] -> [Int] -> [Int]
go ((N
s,N
t)(N, N) -> [(N, N)] -> [(N, N)]
forall a. a -> [a] -> [a]
:[(N, N)]
ts) [Int]
is
        Ordering
LT -> String -> [Int]
forall a. HasCallStack => String -> a
error (String -> [Int]) -> String -> [Int]
forall a b. (a -> b) -> a -> b
$ String
"illegal permutation" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [(N, N)] -> String
forall a. Show a => a -> String
show ((N
s,N
t)(N, N) -> [(N, N)] -> [(N, N)]
forall a. a -> [a] -> [a]
:[(N, N)]
ts) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\t" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [Int] -> String
forall a. Show a => a -> String
show (Int
iInt -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[Int]
is)
     where
      s' :: Int
s' = N -> Int
toInt N
s
      t' :: Int
t' = N -> Int
toInt N
t
    go [(N, N)]
_ [] = String -> [Int]
forall a. HasCallStack => String -> a
error String
"cannot transpose elements of empty list"

-- |Get assocs list from @'Tensor'@. Keys are length-typed vectors of indices.
toList :: forall r v n.
          (SingI r, SingI n, LengthR r ~ n) =>
          Tensor r v -> [(Vec n Int, v)]
toList :: Tensor r v -> [(Vec n Int, v)]
toList Tensor r v
ZeroTensor = []
toList (Scalar v
s) = [(Vec n Int
forall a. Vec 'Z a
VNil, v
s)]
toList (Tensor [(Int, Tensor r' v)]
ms) =
  let st :: Sing (Apply TailRSym0 r)
st = Sing r -> Sing (Apply TailRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR (Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r)
      sn :: Sing n
sn = Sing n
forall k (a :: k). SingI a => Sing a
sing :: Sing n
      sm :: Sing (Apply LengthRSym0 r')
sm = Sing r' -> Sing (Apply LengthRSym0 r')
forall s n (t :: [(VSpace s n, IList s)]).
Sing t -> Sing (Apply LengthRSym0 t)
sLengthR Sing r'
Sing (Apply TailRSym0 r)
st
  in case Sing (Apply TailRSym0 r)
st of
       Sing (Apply TailRSym0 r)
SNil ->
         case Sing n
sn of
           SS SZ -> ((Int, Tensor r' v) -> Maybe (Vec n Int, v))
-> [(Int, Tensor r' v)] -> [(Vec n Int, v)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\(Int
i, Tensor r' v
x) -> case Tensor r' v
x of
                                           Tensor r' v
ZeroTensor -> Maybe (Vec n Int, v)
forall a. Maybe a
Nothing
                                           Scalar v
s   -> (Vec ('S 'Z) Int, v) -> Maybe (Vec ('S 'Z) Int, v)
forall a. a -> Maybe a
Just (Int -> Vec 'Z Int -> Vec ('S 'Z) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
VCons Int
i Vec 'Z Int
forall a. Vec 'Z a
VNil, v
s)) [(Int, Tensor r' v)]
ms
       Sing (Apply TailRSym0 r)
_    ->
         case Sing n
sn of
           SS sm' ->
             Sing n -> (SingI n => [(Vec n Int, v)]) -> [(Vec n Int, v)]
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sm' ((SingI n => [(Vec n Int, v)]) -> [(Vec n Int, v)])
-> (SingI n => [(Vec n Int, v)]) -> [(Vec n Int, v)]
forall a b. (a -> b) -> a -> b
$
             case Sing (Apply LengthRSym0 r')
Sing (LengthR r')
sm Sing (LengthR r') -> Sing n -> Decision (LengthR r' :~: n)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
sm' of
               Proved LengthR r' :~: n
Refl ->
                 ((Int, Tensor r' v) -> [(Vec ('S n) Int, v)])
-> [(Int, Tensor r' v)] -> [(Vec ('S n) Int, v)]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap (\(Int
i, Tensor r' v
v) -> case Tensor r' v
v of
                                         Tensor [(Int, Tensor r' v)]
_   -> ((Vec n Int, v) -> (Vec ('S n) Int, v))
-> [(Vec n Int, v)] -> [(Vec ('S n) Int, v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Vec n Int -> Vec ('S n) Int)
-> (Vec n Int, v) -> (Vec ('S n) Int, v)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Int -> Vec n Int -> Vec ('S n) Int
forall a (n :: N). a -> Vec n a -> Vec ('S n) a
VCons Int
i)) (Sing r' -> (SingI r' => [(Vec n Int, v)]) -> [(Vec n Int, v)]
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r'
Sing (Apply TailRSym0 r)
st ((SingI r' => [(Vec n Int, v)]) -> [(Vec n Int, v)])
-> (SingI r' => [(Vec n Int, v)]) -> [(Vec n Int, v)]
forall a b. (a -> b) -> a -> b
$ Tensor r' v -> [(Vec n 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
v)
                                         Tensor r' v
ZeroTensor -> []) [(Int, Tensor r' v)]
ms

-- |Construct @'Tensor'@ from assocs list. Keys are length-typed vectors of indices. Generalized
-- rank is passed explicitly as singleton.
fromList' :: forall r v n.
             (Sane r ~ 'True, LengthR r ~ n) =>
             Sing r -> [(Vec n Int, v)] -> Tensor r v
fromList' :: Sing r -> [(Vec n Int, v)] -> Tensor r v
fromList' Sing r
_  [] = Tensor r v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
fromList' Sing r
sr [(Vec n Int, v)]
xs =
    let 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
        st :: Sing (Apply TailRSym0 r)
st = Sing r -> Sing (Apply TailRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r
sr
        sm :: Sing (Apply LengthRSym0 (TailR r))
sm = Sing (TailR r) -> Sing (Apply LengthRSym0 (TailR r))
forall s n (t :: [(VSpace s n, IList s)]).
Sing t -> Sing (Apply LengthRSym0 t)
sLengthR Sing (Apply TailRSym0 r)
Sing (TailR r)
st
    in case Sing (Apply LengthRSym0 r)
sn of
         Sing (Apply LengthRSym0 r)
SZ ->
           case Sing r
sr Sing r -> Sing '[] -> Decision (r :~: '[])
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing '[]
forall a. SList '[]
SNil of
             Proved r :~: '[]
Refl -> v -> Tensor '[] v
forall v. v -> Tensor '[] v
Scalar (v -> Tensor '[] v) -> v -> Tensor '[] v
forall a b. (a -> b) -> a -> b
$ (Vec n Int, v) -> v
forall a b. (a, b) -> b
snd ([(Vec n Int, v)] -> (Vec n Int, v)
forall a. [a] -> a
head [(Vec n Int, v)]
xs)
         SS sm' ->
           Sing n -> (SingI n => Tensor r v) -> Tensor r v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sm' ((SingI n => Tensor r v) -> Tensor r v)
-> (SingI n => Tensor r v) -> Tensor r v
forall a b. (a -> b) -> a -> b
$
           case Sing (Apply LengthRSym0 (TailR r))
Sing (LengthR (TailR r))
sm Sing (LengthR (TailR r))
-> Sing n -> Decision (LengthR (TailR r) :~: n)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing n
sm' of
             Proved LengthR (TailR r) :~: n
Refl ->
               Sing (TailR r) -> (SingI (TailR r) => Tensor r v) -> Tensor r v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing (Apply TailRSym0 r)
Sing (TailR r)
st ((SingI (TailR r) => Tensor r v) -> Tensor r v)
-> (SingI (TailR r) => Tensor r v) -> Tensor r v
forall a b. (a -> b) -> a -> b
$
               case Sing (TailR r) -> Sing (Apply SaneSym0 (TailR r))
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing (Apply TailRSym0 r)
Sing (TailR r)
st Sing (Sane (TailR r))
-> Sing 'True -> Decision (Sane (TailR 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 (TailR r) :~: 'True
Refl ->
                       case ((Vec n Int, v) -> (Int, (Vec n Int, v)))
-> [(Vec n Int, v)] -> [(Int, (Vec n Int, v))]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
i `VCons` Vec n Int
is,v
v) -> (Int
i,(Vec n Int
is ,v
v))) [(Vec n Int, v)]
xs of
                         [(Int, (Vec n Int, v))]
xs' -> [(Int, Tensor (TailR r) 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, Tensor (TailR r) v)] -> Tensor r v)
-> [(Int, Tensor (TailR r) v)] -> Tensor r v
forall a b. (a -> b) -> a -> b
$ ([(Vec n Int, v)] -> Tensor (TailR r) v)
-> (Int, [(Vec n Int, v)]) -> (Int, Tensor (TailR r) v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sing (TailR r) -> [(Vec n Int, v)] -> Tensor (TailR r) v
forall (r :: Rank) v (n :: N).
(Sane r ~ 'True, LengthR r ~ n) =>
Sing r -> [(Vec n Int, v)] -> Tensor r v
fromList' Sing (Apply TailRSym0 r)
Sing (TailR r)
st) ((Int, [(Vec n Int, v)]) -> (Int, Tensor (TailR r) v))
-> [(Int, [(Vec n Int, v)])] -> [(Int, Tensor (TailR r) v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, (Vec n Int, v))] -> [(Int, [(Vec n Int, v)])]
forall k a. Eq k => [(k, a)] -> [(k, [a])]
myGroup [(Int, (Vec n Int, v))]
xs'
  where
    myGroup :: Eq k => [(k,a)] -> [(k, [a])]
    myGroup :: [(k, a)] -> [(k, [a])]
myGroup [(k, a)]
ys =
      let ys' :: [[(k, a)]]
ys' = ((k, a) -> (k, a) -> Bool) -> [(k, a)] -> [[(k, a)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\(k
i,a
_) (k
i',a
_) -> k
i k -> k -> Bool
forall a. Eq a => a -> a -> Bool
== k
i') [(k, a)]
ys
      in ([(k, a)] -> (k, [a])) -> [[(k, a)]] -> [(k, [a])]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[(k, a)]
x -> ((k, a) -> k
forall a b. (a, b) -> a
fst ((k, a) -> k) -> (k, a) -> k
forall a b. (a -> b) -> a -> b
$ [(k, a)] -> (k, a)
forall a. [a] -> a
head [(k, a)]
x, ((k, a) -> a) -> [(k, a)] -> [a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (k, a) -> a
forall a b. (a, b) -> b
snd [(k, a)]
x)) [[(k, a)]]
ys'

-- |Construct @'Tensor'@ from assocs list. Keys are length-typed vectors of indices.
fromList :: forall r v n.
            (SingI r, Sane r ~ 'True, LengthR r ~ n) =>
            [(Vec n Int, v)] -> Tensor r v
fromList :: [(Vec n Int, v)] -> Tensor r v
fromList =
  let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
  in Sing r -> [(Vec n Int, v)] -> Tensor r v
forall (r :: Rank) v (n :: N).
(Sane r ~ 'True, LengthR r ~ n) =>
Sing r -> [(Vec n Int, v)] -> Tensor r v
fromList' Sing r
sr

-- |Decompose tensor into assocs list with keys being lists of indices for the first vector space
-- and values being the tensors with lower rank for the remaining vector spaces.
toTListWhile :: forall r v.
                (SingI r, Sane r ~ 'True) =>
                Tensor r v -> [([Int], Tensor (Tail r) v)]
toTListWhile :: Tensor r v -> [([Int], Tensor (Tail r) v)]
toTListWhile (Tensor [(Int, Tensor r' v)]
ms) =
  let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
      st :: Sing (Apply TailRSym0 r)
st = Sing r -> Sing (Apply TailRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r
sr
  in case Sing r'
Sing (Apply TailRSym0 r)
st Sing r' -> Sing (Tail r) -> Decision (r' :~: Tail r)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing r -> Sing (Apply TailSym0 r)
forall a (t :: [a]). Sing t -> Sing (Apply TailSym0 t)
sTail Sing r
sr of
       Proved r' :~: Tail r
Refl -> ((Int, Tensor r' v) -> ([Int], Tensor r' v))
-> [(Int, Tensor r' v)] -> [([Int], Tensor r' v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> [Int]) -> (Int, Tensor r' v) -> ([Int], Tensor r' v)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Int -> [Int]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure) [(Int, Tensor r' v)]
ms
       Disproved Refuted (r' :~: Tail r)
_ ->
         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'
Sing (Apply TailRSym0 r)
st 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 TailSym0 r)
forall a (t :: [a]). Sing t -> Sing (Apply TailSym0 t)
sTail Sing r
sr Sing (Tail r) -> Sing (Tail r') -> Decision (Tail r :~: Tail r')
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing r' -> Sing (Apply TailSym0 r')
forall a (t :: [a]). Sing t -> Sing (Apply TailSym0 t)
sTail Sing r'
Sing (Apply TailRSym0 r)
st of
               Proved Tail r :~: Tail r'
Refl ->
                 Sing r'
-> (SingI r' => [([Int], Tensor (Tail r) v)])
-> [([Int], Tensor (Tail r) v)]
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r'
Sing (Apply TailRSym0 r)
st ((SingI r' => [([Int], Tensor (Tail r) v)])
 -> [([Int], Tensor (Tail r) v)])
-> (SingI r' => [([Int], Tensor (Tail r) v)])
-> [([Int], Tensor (Tail r) v)]
forall a b. (a -> b) -> a -> b
$
                 Sing (Fst (Head r'))
-> (SingI (Fst (Head r')) => [([Int], Tensor (Tail r) v)])
-> [([Int], Tensor (Tail r) v)]
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI (Sing (Head r') -> Sing (Apply FstSym0 (Head r'))
forall a b (t :: (a, b)). Sing t -> Sing (Apply FstSym0 t)
sFst (Sing r' -> Sing (Apply HeadSym0 r')
forall a (t :: [a]). Sing t -> Sing (Apply HeadSym0 t)
sHead Sing r'
Sing (Apply TailRSym0 r)
st)) ((SingI (Fst (Head r')) => [([Int], Tensor (Tail r) v)])
 -> [([Int], Tensor (Tail r) v)])
-> (SingI (Fst (Head r')) => [([Int], Tensor (Tail r) v)])
-> [([Int], Tensor (Tail r) v)]
forall a b. (a -> b) -> a -> b
$
                 let ms' :: [(Int, [([Int], Tensor (Tail r) v)])]
ms' = ((Int, Tensor r' v) -> (Int, [([Int], Tensor (Tail r) v)]))
-> [(Int, Tensor r' v)] -> [(Int, [([Int], Tensor (Tail r) v)])]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> [([Int], Tensor (Tail r) v)])
-> (Int, Tensor r' v) -> (Int, [([Int], Tensor (Tail r) v)])
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Tensor r' v -> [([Int], Tensor (Tail r) v)]
forall (r :: Rank) v.
(SingI r, Sane r ~ 'True) =>
Tensor r v -> [([Int], Tensor (Tail r) v)]
toTListWhile) [(Int, Tensor r' v)]
ms
                 in  ((Int, [([Int], Tensor (Tail r) v)])
 -> [([Int], Tensor (Tail r) v)])
-> [(Int, [([Int], Tensor (Tail r) v)])]
-> [([Int], Tensor (Tail r) v)]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap (\(Int
i, [([Int], Tensor (Tail r) v)]
xs) -> (([Int], Tensor (Tail r) v) -> ([Int], Tensor (Tail r) v))
-> [([Int], Tensor (Tail r) v)] -> [([Int], Tensor (Tail r) v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Int] -> [Int])
-> ([Int], Tensor (Tail r) v) -> ([Int], Tensor (Tail r) v)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:)) [([Int], Tensor (Tail r) v)]
xs) [(Int, [([Int], Tensor (Tail r) v)])]
ms'

-- |Decompose tensor into assocs list with keys being lists of indices up to and including the
-- desired label, and values being tensors of corresponding lower rank.
toTListUntil :: forall (a :: Ix Symbol) r r' v.
                (SingI r, SingI r', RemoveUntil a r ~ r', Sane r ~ 'True, Sane r' ~ 'True) =>
                Sing a -> Tensor r v -> [([Int], Tensor r' v)]
toTListUntil :: Sing a -> Tensor r v -> [([Int], Tensor r' v)]
toTListUntil Sing a
sa (Tensor [(Int, Tensor r' v)]
ms) =
    let sr :: Sing r
sr = Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r
        st :: Sing (Apply TailRSym0 r)
st = Sing r -> Sing (Apply TailRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r
sr
        sh :: Sing (Apply HeadRSym0 r)
sh = Sing r -> Sing (Apply HeadRSym0 r)
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply HeadRSym0 t)
sHeadR Sing r
sr
    in case Sing (HeadR r) -> Sing (Apply SndSym0 (HeadR r))
forall a b (t :: (a, b)). Sing t -> Sing (Apply SndSym0 t)
sSnd Sing (Apply HeadRSym0 r)
Sing (HeadR r)
sh Sing (Snd (HeadR r)) -> Sing a -> Decision (Snd (HeadR r) :~: a)
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ Sing a
sa of
         Proved Snd (HeadR r) :~: a
Refl -> Sing r'
-> (SingI r' => [([Int], Tensor r' v)]) -> [([Int], Tensor r' v)]
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r'
Sing (Apply TailRSym0 r)
st ((SingI r' => [([Int], Tensor r' v)]) -> [([Int], Tensor r' v)])
-> (SingI r' => [([Int], Tensor r' v)]) -> [([Int], Tensor r' v)]
forall a b. (a -> b) -> a -> b
$
                        case Sing r'
Sing (Apply TailRSym0 r)
st Sing r' -> Sing r' -> Decision (r' :~: r')
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ (Sing r'
forall k (a :: k). SingI a => Sing a
sing :: Sing r') of
                          Proved r' :~: r'
Refl -> ((Int, Tensor r' v) -> ([Int], Tensor r' v))
-> [(Int, Tensor r' v)] -> [([Int], Tensor r' v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> [Int]) -> (Int, Tensor r' v) -> ([Int], Tensor r' v)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Int -> [Int]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure) [(Int, Tensor r' v)]
ms
         Disproved Refuted (Snd (HeadR r) :~: a)
_ ->
           Sing r'
-> (SingI r' => [([Int], Tensor r' v)]) -> [([Int], Tensor r' v)]
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r'
Sing (Apply TailRSym0 r)
st ((SingI r' => [([Int], Tensor r' v)]) -> [([Int], Tensor r' v)])
-> (SingI r' => [([Int], Tensor r' v)]) -> [([Int], Tensor r' v)]
forall a b. (a -> b) -> a -> b
$
           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'
Sing (Apply TailRSym0 r)
st 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 a -> Sing r' -> Sing (Apply (Apply RemoveUntilSym0 a) r')
forall s n (t1 :: Ix s) (t2 :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply RemoveUntilSym0 t1) t2)
sRemoveUntil Sing a
sa Sing r'
Sing (Apply TailRSym0 r)
st Sing
  (Case_6989586621679113446
     a r' a r' a r' (Equals_6989586621679117897 (Snd (HeadR r')) a))
-> Sing r'
-> Decision
     (Case_6989586621679113446
        a r' a r' a r' (Equals_6989586621679117897 (Snd (HeadR r')) a)
      :~: r')
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ (Sing r'
forall k (a :: k). SingI a => Sing a
sing :: Sing r') of
                 Proved Case_6989586621679113446
  a r' a r' a r' (Equals_6989586621679117897 (Snd (HeadR r')) a)
:~: r'
Refl ->
                   let ms' :: [(Int, [([Int], Tensor r' v)])]
ms' = ((Int, Tensor r' v) -> (Int, [([Int], Tensor r' v)]))
-> [(Int, Tensor r' v)] -> [(Int, [([Int], Tensor r' v)])]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tensor r' v -> [([Int], Tensor r' v)])
-> (Int, Tensor r' v) -> (Int, [([Int], Tensor r' v)])
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Sing a -> Tensor r' v -> [([Int], Tensor r' v)]
forall (a :: Ix Symbol) (r :: Rank) (r' :: Rank) v.
(SingI r, SingI r', RemoveUntil a r ~ r', Sane r ~ 'True,
 Sane r' ~ 'True) =>
Sing a -> Tensor r v -> [([Int], Tensor r' v)]
toTListUntil Sing a
sa)) [(Int, Tensor r' v)]
ms
                   in  ((Int, [([Int], Tensor r' v)]) -> [([Int], Tensor r' v)])
-> [(Int, [([Int], Tensor r' v)])] -> [([Int], Tensor r' v)]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> [b]) -> t a -> [b]
concatMap (\(Int
i, [([Int], Tensor r' v)]
xs) -> (([Int], Tensor r' v) -> ([Int], Tensor r' v))
-> [([Int], Tensor r' v)] -> [([Int], Tensor r' v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Int] -> [Int]) -> ([Int], Tensor r' v) -> ([Int], Tensor r' v)
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Int
i Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:)) [([Int], Tensor r' v)]
xs) [(Int, [([Int], Tensor r' v)])]
ms'

-- |Construct tensor from assocs list. Keys are lists of indices, values are
-- tensors of lower rank. Used internally for tensor algebra.
fromTList :: forall r r' v.(Sane r ~ 'True, Sane r' ~ 'True, SingI r, SingI r') =>
                           [([Int], Tensor r v)] -> Tensor r' v
fromTList :: [([Int], Tensor r v)] -> Tensor r' v
fromTList [] = Tensor r' v
forall (r :: Rank) v. (Sane r ~ 'True) => Tensor r v
ZeroTensor
fromTList xs :: [([Int], Tensor r v)]
xs@(([Int]
i0,Tensor r v
t0):[([Int], Tensor r v)]
ys)
  | [Int] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [Int]
i0 = if [([Int], Tensor r v)] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [([Int], Tensor r v)]
ys
              then case (Sing r
forall k (a :: k). SingI a => Sing a
sing :: Sing r) Sing r -> Sing r' -> Decision (r :~: r')
forall k (a :: k) (b :: k).
SDecide k =>
Sing a -> Sing b -> Decision (a :~: b)
%~ (Sing r'
forall k (a :: k). SingI a => Sing a
sing :: Sing r') of
                     Proved r :~: r'
Refl -> Tensor r v
Tensor r' v
t0
              else String -> Tensor r' v
forall a. HasCallStack => String -> a
error (String -> Tensor r' v) -> String -> Tensor r' v
forall a b. (a -> b) -> a -> b
$ String
"illegal assocs in fromTList : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [[Int]] -> String
forall a. Show a => a -> String
show ((([Int], Tensor r v) -> [Int]) -> [([Int], Tensor r v)] -> [[Int]]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Int], Tensor r v) -> [Int]
forall a b. (a, b) -> a
fst [([Int], Tensor r v)]
xs)
  | Bool
otherwise =
      let sr' :: Sing r'
sr' = Sing r'
forall k (a :: k). SingI a => Sing a
sing :: Sing r'
          st' :: Sing (Apply TailRSym0 r')
st' = Sing r' -> Sing (Apply TailRSym0 r')
forall s n (t :: [(VSpace s n, IList s)]).
SOrd s =>
Sing t -> Sing (Apply TailRSym0 t)
sTailR Sing r'
sr'
      in Sing (TailR r') -> (SingI (TailR r') => Tensor r' v) -> Tensor r' v
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing (Apply TailRSym0 r')
Sing (TailR r')
st' ((SingI (TailR r') => Tensor r' v) -> Tensor r' v)
-> (SingI (TailR r') => Tensor r' v) -> Tensor r' v
forall a b. (a -> b) -> a -> b
$
        case Sing (TailR r') -> Sing (Apply SaneSym0 (TailR r'))
forall a b (t :: [(VSpace a b, IList a)]).
(SOrd a, SOrd b) =>
Sing t -> Sing (Apply SaneSym0 t)
sSane Sing (Apply TailRSym0 r')
Sing (TailR r')
st' of
          Sing (Apply SaneSym0 (TailR r'))
STrue -> [(Int, Tensor (TailR r') 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, Tensor (TailR r') v)] -> Tensor r' v)
-> [(Int, Tensor (TailR r') v)] -> Tensor r' v
forall a b. (a -> b) -> a -> b
$ ((Int, [([Int], Tensor r v)]) -> (Int, Tensor (TailR r') v))
-> [(Int, [([Int], Tensor r v)])] -> [(Int, Tensor (TailR r') v)]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (([([Int], Tensor r v)] -> Tensor (TailR r') v)
-> (Int, [([Int], Tensor r v)]) -> (Int, Tensor (TailR r') v)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [([Int], Tensor r v)] -> Tensor (TailR r') v
forall (r :: Rank) (r' :: Rank) v.
(Sane r ~ 'True, Sane r' ~ 'True, SingI r, SingI r') =>
[([Int], Tensor r v)] -> Tensor r' v
fromTList) [(Int, [([Int], Tensor r v)])]
xs'''
  where
    xs' :: [(Int, ([Int], Tensor r v))]
xs' = (([Int], Tensor r v) -> (Int, ([Int], Tensor r v)))
-> [([Int], Tensor r v)] -> [(Int, ([Int], Tensor r v))]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
i:[Int]
is,Tensor r v
v) -> (Int
i,([Int]
is,Tensor r v
v))) [([Int], Tensor r v)]
xs
    xs'' :: [[(Int, ([Int], Tensor r v))]]
xs'' = ((Int, ([Int], Tensor r v)) -> (Int, ([Int], Tensor r v)) -> Bool)
-> [(Int, ([Int], Tensor r v))] -> [[(Int, ([Int], Tensor r v))]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\(Int
i,([Int], Tensor r v)
_) (Int
i',([Int], Tensor r v)
_) -> Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i') [(Int, ([Int], Tensor r v))]
xs'
    xs''' :: [(Int, [([Int], Tensor r v)])]
xs''' = ([(Int, ([Int], Tensor r v))] -> (Int, [([Int], Tensor r v)]))
-> [[(Int, ([Int], Tensor r v))]] -> [(Int, [([Int], Tensor r v)])]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[(Int, ([Int], Tensor r v))]
x -> ((Int, ([Int], Tensor r v)) -> Int
forall a b. (a, b) -> a
fst ((Int, ([Int], Tensor r v)) -> Int)
-> (Int, ([Int], Tensor r v)) -> Int
forall a b. (a -> b) -> a -> b
$ [(Int, ([Int], Tensor r v))] -> (Int, ([Int], Tensor r v))
forall a. [a] -> a
head [(Int, ([Int], Tensor r v))]
x, ((Int, ([Int], Tensor r v)) -> ([Int], Tensor r v))
-> [(Int, ([Int], Tensor r v))] -> [([Int], Tensor r v)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, ([Int], Tensor r v)) -> ([Int], Tensor r v)
forall a b. (a, b) -> b
snd [(Int, ([Int], Tensor r v))]
x)) [[(Int, ([Int], Tensor r v))]]
xs''