Pasted

T[X'] = T[X':] | T[:X']
 
S[T[A' : X'], T[B' : Y'], T[C' : Z']] -- срез тензора, на самом деле тензор T[A', X', B' : X', Y', Z']. Используется чтобы передать часть размерностей в операции. Компонента T[B' : Y'] - "рабочий тензор"
 
 
_^ :: T[X'] -> T[Y'] -> T[X' : Y']
^_ :: T[X'] -> T[Y'] -> T[Y' : X']
 
_ :: T[X' : _] -> T[X']
^ :: T[_ : Y'] -> T[Y']
 
 
@ :: T[A' : B'] -> T[X' : Y'] -> T[A', X' : B', Y'] --тензорное произведение
@ :: T[A' : B'] -> T[0] -> T[A' : B'] --специализация, умножение на скаляр отличается по тому как оно работает
@ :: T[0] -> T[A' : B'] -> T[A' : B']
 
 
slice :: (Ind i) => (i a) -> (i b) -> T[A'{a}, X'{b-a}, B'] -> S[T[A'], T[X'], T[B']]
 
unslice :: S[T[A' : X'], T[B' : Y'], T[C' : Z']] -> T[A', B', C' : X', Y', Z'] --выводится, +дополнительно выводятся специализации
unslice S(h, x, t) = h @ x @ t
 
--декларации должны автовывестись из реализаций
slice_ a b t = ^_ (^ t) =<< (slice a b (_ t)) 
slice^ a b t - _^ (_ t) =<< (slice a b (^ t))
 
--ожидаемые декларации
slice_ :: (Ind i) => (i a) -> (i b) -> T[A'{a}, X'{b-a}, B' : U'] -> S[T[A'], T[X' : U'], T[B']]
slice^ :: (Ind i) => (i a) -> (i b) -> T[L' : A'{a}, X'{b-a}, B'] -> S[T[A'], T[L' : X'], T[B']]
 
take :: (Ind i) => (i a) -> T[A'{a}, X, B'] -> S[T[A'], T[X], B'] --выводится
take a t = slice a (a+1) t
 
take_ a t = slice_ a (a+1) t
take^ a t = slice^ a (a+1) t
 
transpose :: T[A, B] -> T[B, A]
 
contract :: T[X : X] -> T[1]
 
lower :: (Metric T) => T[: X] -> T[X :]
raise :: (Metric T) => T[X :] -> T[: X]
 
--пример использования (страшный псевдо-синтаксис)
a :: T[5, 3, 2 : 6, 7, 3]
unslice (contract =<< take_ 2 =<< take^ 3 a) :: T[5, 2 : 6, 7]
 
по порядку:
a :: T[5, 3, 2 : 6, 7, 3]
take^ 3 a :: S[T[: 6, 7], T[5, 3, 2 : 3], T[]]
take_ 2 =<< take^ 3 a :: S[T[5 : 6, 7], T[3 : 3], T[2 :]]
contract =<< take_ 2 =<< take^ 3 a :: S[T[5 : 6, 7], T[1], T[2 :]]
unslice (contract =<< take_ 2 =<< take^ 3 a :: S[T[5 : 6, 7], T[1], T[2 :]]) :: T[5, 2 : 6, 7]