Data.Tensor.Tensor

Reexports

Definitions

record Tensor : TensorShape rank -> Type -> Type

  Tensor is the core datatype of TensorType.
  Implementation-wise, it's a wrapper around the extension of `Cont.Tensor`
  to aid type inference, and to add the axis name functionality

Totality: total
Visibility: public export
Constructor: 

MkT : Ext (Tensor (conts shape)) a -> Tensor shape a

Projection: 

.GetT : Tensor shape a -> Ext (Tensor (conts shape)) a

Hints:

Abs a => AllC TensorMonoid shape => Abs (Tensor shape a)

AllAlgebra shape a => Algebra (Tensor shape) a

AllC TensorMonoid shape => Applicative (Tensor shape)

AllDisplay2D shape a => TensorCubEvidence shape => Display2D (Tensor shape a)

AllEq shape a => Eq (Tensor shape a)

Exp a => AllC TensorMonoid shape => Exp (Tensor shape a)

AllC IsFoldable shape => Foldable (Tensor shape)

Fractional a => AllC TensorMonoid shape => Fractional (Tensor shape a)

FromDouble a => AllC TensorMonoid shape => FromDouble (Tensor shape a)

Functor (Tensor shape)

Neg a => AllC TensorMonoid shape => Neg (Tensor shape a)

Num a => AllC TensorMonoid shape => Num (Tensor shape a)

Random a => Applicative (Tensor shape) => Traversable (Tensor shape) => Random (Tensor shape a)

AllDisplay2D shape a => TensorCubEvidence shape => Show (Tensor shape a)

AllTraversable shape => AllC IsFoldable shape => Traversable (Tensor shape)

.GetT : Tensor shape a -> Ext (Tensor (conts shape)) a

Visibility: public export

GetT : Tensor shape a -> Ext (Tensor (conts shape)) a

Visibility: public export

.shape : (0 _ : Tensor shape a) -> Vect rank Axis

Visibility: public export

.axisNames : (0 _ : Tensor shape a) -> Vect rank AxisName

Visibility: public export

.sizes : (0 _ : Tensor shape a) -> Vect rank Cont

Visibility: public export

.indexAxis : (0 _ : Tensor shape a) -> (axisName : AxisName) -> Elem axisName shape => Cont

Visibility: public export

.renameAxis : Tensor shape a -> (axisName : AxisName) -> (newAxisName : AxisName) -> Elem axisName shape => Tensor (rename shape axisName newAxisName) a

Visibility: public export

.rename : Tensor shape a -> (axisIndex : Fin rank) -> (newAxisName : AxisName) -> Tensor (rename shape axisIndex newAxisName) a

Visibility: public export

BatchSize : Axis

Visibility: public export

extract : Tensor [] a -> a

Visibility: public export

embed : a -> Tensor [] a

Visibility: public export

fromExtensionComposition : composeExtensions (conts shape) a -> Tensor shape a

  With the added data of the wrapper around (Ext (Tensor shape) a), this
  effectively states a list version of the following isomorphism
  Ext c . Ext d = Ext (c . d)

Visibility: public export

toExtensionComposition : Tensor shape a -> composeExtensions (conts shape) a

Visibility: public export

extractTopExt : {auto {conArg:17957} : ConsistentWith c cs} -> Tensor (c :: cs) a -> Ext (c .cont) (Tensor cs a)

  For this and the function below, the commented out definition is 'cleaner'
  but it requires non-erased `c` and `cs`

Visibility: public export

embedTopExt : {auto {conArg:18019} : ConsistentWith c cs} -> Ext (c .cont) (Tensor cs a) -> Tensor (c :: cs) a

Visibility: public export

extToVector : Ext (c .cont) a -> Tensor [c] a

  This is useful because container composition adds non-trivial data to the
  vector type (i.e. `c >@ Scalar` is not equal to `c`)

Visibility: public export

vectorToExt : Tensor [c] a -> Ext (c .cont) a

Visibility: public export

toNestedTensor : {auto {conArg:18211} : ConsistentWith c cs} -> Tensor (c :: cs) a -> Tensor [c] (Tensor cs a)

Visibility: public export

fromNestedTensor : {auto {conArg:18266} : ConsistentWith c cs} -> Tensor [c] (Tensor cs a) -> Tensor (c :: cs) a

Visibility: public export

tensorMapFirstAxis : {auto ccs : ConsistentWith c cs} -> {auto cds : ConsistentWith c ds} -> (Tensor cs a -> Tensor ds a) -> Tensor (c :: cs) a -> Tensor (c :: ds) a

  TODO generalise to function operating on an axis name instead of index

Visibility: public export

(<-$>) : {auto {conArg:18408} : ConsistentWith c cs} -> {auto {conArg:18412} : ConsistentWith c ds} -> (Tensor cs a -> Tensor ds a) -> Tensor (c :: cs) a -> Tensor (c :: ds) a

  Is meant to look like infix map (i.e. `<$>`) with the added difference
  that we keep the container on the left side untouched, hence the `<-$>`

Visibility: public export
Fixity Declaration: infixr operator, level 4

concreteTypeTensor : (shape : TensorShape rank) -> AllC IsConcrete shape => Type -> Type

Visibility: public export

concreteTypeFunctor : {auto {conArg:18521} : AllC IsConcrete shape} -> Functor (concreteTypeTensor shape)

Visibility: public export

concreteToExtensions : {auto {conArg:18565} : AllC IsConcrete shape} -> concreteTypeTensor shape a -> composeExtensions (conts shape) a

Visibility: public export

extensionsToConcreteType : {auto {conArg:18632} : AllC IsConcrete shape} -> composeExtensions (conts shape) a -> concreteTypeTensor shape a

Visibility: public export

toTensor : {auto {conArg:18693} : AllC IsConcrete shape} -> concreteTypeTensor shape a -> Tensor shape a

Visibility: public export

fromTensor : {auto {conArg:18735} : AllC IsConcrete shape} -> Tensor shape a -> concreteTypeTensor shape a

Visibility: public export

fromConcreteTy : {auto {conArg:18776} : AllC IsConcrete shape} -> concreteTypeTensor shape a -> Tensor shape a

  Many containers have a `FromConcrete` instance, allowing them to easily
  be converted to and from a (usually familiar) Idris type
  This works with tensors defined as a fold over containers, but it requires
  burdensome shape annotations everywhere
  The decision was made to wrap that fold in `Tensor` as above, and then
  (as this isn't a container anymore) provide equally named functions like
  the ones `FromConcrete` provides. Idris' name resolution should be able to
  detect which one needs to be used at call sites

Visibility: public export

toConcreteTy : {auto {conArg:18809} : AllC IsConcrete shape} -> Tensor shape a -> concreteTypeTensor shape a

Visibility: public export

(>#) : {auto {conArg:18841} : AllC IsConcrete shape} -> concreteTypeTensor shape a -> Tensor shape a

  Prefix operator for converting from a concrete type to a tensor
  We read it as a map `>` going into the tensor `#`

Visibility: public export
Fixity Declarations:
prefix operator, level 0
prefix operator, level 0

(#>) : {auto {conArg:18874} : AllC IsConcrete shape} -> Tensor shape a -> concreteTypeTensor shape a

  Prefix operator for converting from a tensor to concrete type
  We read it as a map `>` going out of the tensor `#`

Visibility: public export
Fixity Declarations:
prefix operator, level 0
prefix operator, level 0

(>#>) : {auto {conArg:18912} : AllC IsConcrete shapeOld} -> {auto {conArg:18918} : AllC IsConcrete shapeNew} -> (Tensor shapeOld a -> Tensor shapeNew b) -> concreteTypeTensor shapeOld a -> concreteTypeTensor shapeNew b

Visibility: public export
Fixity Declaration: infixr operator, level 0

(#>#) : {auto {conArg:18984} : AllC IsConcrete shapeOld} -> {auto {conArg:18990} : AllC IsConcrete shapeNew} -> (concreteTypeTensor shapeOld a -> concreteTypeTensor shapeNew b) -> Tensor shapeOld a -> Tensor shapeNew b

Visibility: public export
Fixity Declaration: infixr operator, level 0

restructure : Tensor (conts cs) =%> Tensor (conts ds) -> tensorShapesConsistent cs ds => Tensor cs a -> Tensor ds a

  A wrapper around `extMap`
  Allows us to define views, traversals and general reshaping

Visibility: public export

reshape : {auto {conArg:19110} : All IsCubical (conts oldShape)} -> {auto {conArg:19117} : All IsCubical (conts newShape)} -> Tensor oldShape a -> size (conts oldShape) = size (conts newShape) => tensorShapesConsistent oldShape newShape => Tensor newShape a

  Reshape is `restructure` for cubical tensors that leaves number of 
  elements unchanged.  This is currently by
  1) flattening out the entire tensor into a vector
  2) recast the type to be of the right shape
  3) unflatten the vector into the right shape
  Importantly, the content of tensors is never touched, only the shape is
  manipulated

Visibility: public export

tensorReplicate : AllC TensorMonoid shape => a -> Tensor shape a

Visibility: public export

liftA2Tensor : AllC TensorMonoid shape => Tensor shape a -> Tensor shape b -> Tensor shape (a, b)

Visibility: public export

data AllEq : TensorShape rank -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : Eq a => AllEq [] a

Cons : Eq (fullOf (c .cont) (Tensor cs a)) => {auto ne : ConsistentWith c cs} -> AllEq (c :: cs) a

Hint: 

AllEq shape a => Eq (Tensor shape a)

tensorEq : AllEq shape a => Tensor shape a -> Tensor shape a -> Bool

Visibility: public export

interfacePosEq : InterfaceOnPositions (Tensor [Vect n]) Eq

Visibility: public export

join : SeqMonoid (i .cont) => Tensor [i, i] a -> Tensor [i] a

  Captures both "diagonal" operation for vector (Naperian containers) and
  "concat"-like operation for lists 

Visibility: public export

diagonal : IsNaperian (i .cont) => Tensor [i, i] a -> Tensor [i] a

  Alias for `join` for Naperian containers

Visibility: public export

codiagonal : Num a => Tensor [i] a -> Tensor [i, i] a

Visibility: public export

tDiagVect : Tensor [("i" ~~> 2), ("j" ~~> 2)] Double

Visibility: public export

tDiagList : Tensor [("i" ~> List), ("j" ~> List)] Double

Visibility: public export

data AllAlgebra : TensorShape rank -> Type -> Type

  Unlike all other instantiations of 'AllX', `AllAlgebra` is not
  stating that each container in an list has an algebra, but rather
  'cumulatively'. For instance, `AllAlgebra [c, d] a` is not defined as
  `Algebra c a` and `Algebra d a`, bur rather as `Algebra c (Algebra d a)`
  and `Algebra d a`.

Totality: total
Visibility: public export
Constructors:

Nil : AllAlgebra [] a

Cons : Algebra (Ext (c .cont)) (Tensor cs a) => AllAlgebra cs a => {auto {conArg:21042} : ConsistentWith c cs} -> AllAlgebra (c :: cs) a

Hint: 

AllAlgebra shape a => Algebra (Tensor shape) a

reduceTensor : AllAlgebra shape a => Tensor shape a -> a

Visibility: public export

reduceFirstAxis : Algebra (Ext (s .cont)) (Tensor shape a) => {auto {conArg:21127} : ConsistentWith s shape} -> Tensor (s :: shape) a -> Tensor shape a

Visibility: public export

reduceSingleAxis : (toReduce : AxisName) -> {auto uElem : UniqueElem toReduce shape} -> Tensor shape a -> AllC TensorMonoid shape => Num a => IsFinite (index shape toReduce) => Tensor (removeAxis toReduce shape) a

  Reduces a tensor along an axis appearing only once in the shape
  In the presence of multiple axes (at least in the Naperian case) we
  first have to transpose them to the front, and then diagonalise.
  Using `IsFinite` instead of `Algebra` because `IsFinite` allows us to
  refer to only the container, instead of the underlying type `a`

Visibility: public export

tensorFoldr : AllC IsFoldable shape => (a -> acc -> acc) -> acc -> Tensor shape a -> acc

Visibility: public export

allFoldableFromAllCubical : All IsCubical shape -> AllC IsFoldable shape

Visibility: public export

data AllTraversable : TensorShape rank -> Type

Totality: total
Visibility: public export
Constructors:

Nil : AllTraversable []

Cons : Traversable (Ext (c .cont)) => AllTraversable cs => {auto {conArg:22070} : ConsistentWith c cs} -> AllTraversable (c :: cs)

Hint: 

AllTraversable shape => AllC IsFoldable shape => Traversable (Tensor shape)

tensorTraverse : AllTraversable shape => Applicative f => (a -> f b) -> Tensor shape a -> f (Tensor shape b)

Visibility: public export

transposeMatrix : {auto {conArg:22308} : ConsistentWith i [j]} -> {auto {conArg:22316} : ConsistentWith j [i]} -> IsNaperian i => IsNaperian j => Tensor [i, j] a -> Tensor [j, i] a

Visibility: public export

positions : Tensor [c] ((c .cont) .Pos sh)

  Like 'positions' from Naperian, but parametric, and not requiring the
  Naperian instance here

Visibility: public export

interface DisplayNestedCont : Cont -> Type

  Tensor-context rendering of container extensions.
  A separate interface from `Display2D (Ext c a)` because layered
  containers need to make separate choices (vertical bracket stacking for
  List/Vect, structural tree layout for trees)

Parameters: c
Methods:

boxedForSiblings : Grid Char -> Grid Char

  Action a parent of `c` needs to apply to `c`
  For instance, trees get boxed if they're multi-line, cubical
  containers do not apply any action. Defaults to boxing

displayNestedCont : Nat -> (Grid Char -> Grid Char) -> Ext c (Grid Char) -> Grid Char

  Given the content of `c` rendered as grids individually, render
  the layout given information of how many axes are below, and
  information on whether to box children, to keep visual separation
  Container can in principle decide whether to use `childBox` or not

Implementations:

DisplayNestedCont List

DisplayNestedCont (Vect n)

DisplayNestedCont BinTree

DisplayNestedCont BinTreeLeaf

DisplayNestedCont BinTreeNode

DisplayNestedCont Scalar

DisplayNestedCont Pair

boxedForSiblings : DisplayNestedCont c => Grid Char -> Grid Char

  Action a parent of `c` needs to apply to `c`
  For instance, trees get boxed if they're multi-line, cubical
  containers do not apply any action. Defaults to boxing

Visibility: public export

displayNestedCont : DisplayNestedCont c => Nat -> (Grid Char -> Grid Char) -> Ext c (Grid Char) -> Grid Char

  Given the content of `c` rendered as grids individually, render
  the layout given information of how many axes are below, and
  information on whether to box children, to keep visual separation
  Container can in principle decide whether to use `childBox` or not

Visibility: public export

data AllDisplay2D : TensorShape rank -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Nil : Display2D a => AllDisplay2D [] a

(::) : DisplayNestedCont (c .cont) -> AllDisplay2D cs a -> {auto {conArg:23131} : ConsistentWith c cs} -> TensorCubEvidence cs => AllDisplay2D (c :: cs) a

Hints:

AllDisplay2D shape a => TensorCubEvidence shape => Display2D (Tensor shape a)

AllDisplay2D shape a => TensorCubEvidence shape => Show (Tensor shape a)

scalarDisplay : AllDisplay2D shape a => Display2D a

  Recover the scalar-element `Display2D a` instance from a shape

Visibility: public export

maxWidthCubical : AllDisplay2D shape a => AllC IsFoldable shape => Tensor shape a -> Nat

  Fold through the content of the tensor, and return the maximum
  width of the displayed scalar element

Visibility: public export

renderCubicalWithWidth : AllDisplay2D shape a => All IsCubical shape => Nat -> Nat -> Tensor shape a -> Grid Char

  Render a cubical tensor given
  1) a specific width of content for each cell
  2) the number of outer bracket levels that need to surround the tensor

Visibility: public export

display2DTensorCubical : AllDisplay2D shape a => AllC IsFoldable shape => All IsCubical shape => Tensor shape a -> Grid Char

  Render a tensor we know is cubical: first compute the maximum width of 
  a scalar element that appears, then render.

Visibility: public export

dispatchTensorDisplay : AllDisplay2D shape a => TensorCubEvidence shape => Tensor shape a -> Grid Char

  Dispatch between cubical and non-cubical rendering.
  Is there a better way than with `TensorCubEvidence`?

Visibility: public export

dotWith : Algebra (Tensor shape) c => AllC TensorMonoid shape => (a -> b -> c) -> Tensor shape a -> Tensor shape b -> Tensor [] c

Visibility: public export

dot : Num a => Algebra (Tensor shape) a => AllC TensorMonoid shape => Tensor shape a -> Tensor shape a -> Tensor [] a

Visibility: public export

outerWith : TensorMonoid (i .cont) => TensorMonoid (j .cont) => {auto ac : ConsistentWith i [j]} -> (a -> b -> c) -> Tensor [i] a -> Tensor [j] b -> Tensor [i, j] c

Visibility: public export

outer : TensorMonoid (i .cont) => TensorMonoid (j .cont) => {auto ac : ConsistentWith i [j]} -> Num a => Tensor [i] a -> Tensor [j] a -> Tensor [i, j] a

Visibility: public export

matrixVectorProduct : Num a => TensorMonoid (j .cont) => AllAlgebra [j] a => {auto ac : ConsistentWith i [j]} -> Tensor [i, j] a -> Tensor [j] a -> Tensor [i] a

Visibility: public export

vectorMatrixProduct : Num a => TensorMonoid (i .cont) => {auto ac : ConsistentWith i [j]} -> Algebra (Ext (i .cont)) (Tensor [j] a) => Tensor [i] a -> Tensor [i, j] a -> Tensor [j] a

Visibility: public export

matMul : Num a => TensorMonoid (j .cont) => {auto ac1 : ConsistentWith i [j]} -> {auto ac2 : ConsistentWith j [k]} -> {auto ac3 : ConsistentWith i [k]} -> Algebra (Ext (j .cont)) (Tensor [k] a) => Tensor [i, j] a -> Tensor [j, k] a -> Tensor [i, k] a

Visibility: public export

matrixMatrixProduct : {auto ac1 : ConsistentWith i [j]} -> {auto ac2 : ConsistentWith k [j]} -> {auto ac3 : ConsistentWith k [i]} -> Num a => TensorMonoid (j .cont) => AllAlgebra [j] a => Tensor [i, j] a -> Tensor [k, j] a -> Tensor [k, i] a

Visibility: public export

tEx : Tensor [("i" ~~> 3), ("j" ~~> 4)] Integer

Visibility: public export

Ex2 : Tensor [("k" ~~> 12)] Integer

Visibility: public export

Ex3 : Tensor [("i" ~~> 2), ("j" ~~> 6)] Integer

Visibility: public export

data IndexTo : Tensor shape a -> (indexAxis : AxisName) -> UniqueElem indexAxis shape => Type

Totality: total
Visibility: public export
Constructors:

Nil : {auto {conArg:25666} : ConsistentWith ax as} -> {auto {conArg:25670} : NotElem (ax .name) as} -> IndexTo t (ax .name)

(::) : {auto {conArg:25699} : IsSucc rank} -> {auto {conArg:25706} : ConsistentWith ax as} -> {auto {conArg:25710} : UniqueElem indexAxis as} -> {auto {conArg:25714} : IsNo (decEq indexAxis (ax .name))} -> (p : (ax .cont) .Pos (shapeExt (extractTopExt t))) -> IndexTo (index (extractTopExt t) p) indexAxis -> IndexTo t indexAxis

indexShapeFw : (t : Tensor shape a) -> (indexAxis : AxisName) -> {auto inShape : UniqueElem indexAxis shape} -> IndexTo t indexAxis -> index shape indexAxis .Shp

  Here "axis shape" here meant in the container sense

Visibility: public export

data Index : (shape : TensorShape rank) -> Tensor shape a -> Type

  Datatype containing information needed to index into a Tensor
  Unlike with cubical tensors, where the underlying tensor is not 
  necessary, here we require the data of `t : Tensor shape a` too.
  Based on absolute positions

Totality: total
Visibility: public export
Constructors:

Nil : Index [] t

(::) : {auto {conArg:25904} : ConsistentWith ax as} -> (p : (ax .cont) .Pos (shapeExt (extractTopExt t))) -> Index as (index (extractTopExt t) p) -> Index (ax :: as) t

index : (t : Tensor shape a) -> Index shape t -> a

Visibility: public export

(@@) : (t : Tensor shape a) -> Index shape t -> a

Visibility: public export
Fixity Declarations:
infixr operator, level 9
prefix operator, level 10

set : (t : Tensor shape a) -> InterfaceOnPositions (Tensor (conts shape)) Eq => Index shape t -> a -> Tensor shape a

Visibility: public export

data IndexC : Vect rank Nat -> Type

Totality: total
Visibility: public export
Constructors:

Nil : IndexC []

(::) : Fin n -> IndexC ns -> IndexC (n :: ns)

treeExample1Test : Tensor [("myTree" ~> BinTree)] Double

Visibility: public export