Data.Tensor.Axis

Reexports

Definitions

AxisName : Type

  The name for an axis is an arbitrary string

Visibility: public export

record Axis : Type

  An axis is a container (the "size" of the axis) together with its name

Totality: total
Visibility: public export
Constructor: 

(~>) : AxisName -> Cont -> Axis

Projections:

.cont : Axis -> Cont

.name : Axis -> AxisName

.name : Axis -> AxisName

Visibility: public export

name : Axis -> AxisName

Visibility: public export

.cont : Axis -> Cont

Visibility: public export

cont : Axis -> Cont

Visibility: public export

rename : Axis -> AxisName -> Axis

Visibility: public export

TTInternalName : AxisName

  In some cases we TensorType might need to assign a default name to an axis,
  one which is internal and will not be exposed to the user.
  This is the default name for such cases

Visibility: public export

(~~>) : AxisName -> Nat -> Axis

  A "constructor" for cubical axes

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

data IsCubical : Axis -> Type

  Follows the pattern of `IsCubical` from `Data.Container.Object.Instances`

Totality: total
Visibility: public export
Constructor: 

MkIsCubical : (name : AxisName) -> (n : Nat) -> IsCubical (name ~~> n)

dimHelper : IsCubical a -> Nat

Visibility: public export

dim : (0 a : Axis) -> IsCubical a => Nat

Visibility: public export

data IsNaperian : Axis -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsNaperian : (name : AxisName) -> (pos : Type) -> IsNaperian (name ~> Nap pos)

LogHelper : IsNaperian a => Type

Visibility: public export

Log : (0 a : Axis) -> IsNaperian a => Type

Visibility: public export

toContNaperian : IsNaperian a -> IsNaperian (a .cont)

Visibility: public export

cubicalShapeHelper : All IsCubical shape -> List Nat

Visibility: public export

cubicalShape : (0 shape : Vect r Axis) -> All IsCubical shape => List Nat

  Given a list of cubical axes, return the list of their dimensions

Visibility: public export

size : (0 shape : Vect r Axis) -> All IsCubical shape => Nat

  Size of a cubical tensor, i.e. its number of elements

Visibility: public export

data TensorShape : Nat -> Type

Totality: total
Visibility: public export
Constructors:

Nil : TensorShape 0

(::) : (a : Axis) -> (as : TensorShape k) -> NewAxisConsistent a as => TensorShape (S k)

Hints:

Abs a => All TensorMonoid (conts shape) => Abs (Tensor shape a)

AllAlgebra shape a => Algebra (Tensor shape) a

All TensorMonoid (conts shape) => Applicative (Tensor shape)

AllEq shape a => Eq (Tensor shape a)

Exp a => All TensorMonoid (conts shape) => Exp (Tensor shape a)

AllFoldable shape => Foldable (Tensor shape)

Fractional a => All TensorMonoid (conts shape) => Fractional (Tensor shape a)

FromDouble a => All TensorMonoid (conts shape) => FromDouble (Tensor shape a)

Functor (Tensor shape)

Neg a => All TensorMonoid (conts shape) => Neg (Tensor shape a)

Num a => All TensorMonoid (conts shape) => Num (Tensor shape a)

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

AllShow shape a => Show (Tensor shape a)

AllTraversable shape => AllFoldable shape => Traversable (Tensor shape)

toVect : TensorShape k -> Vect k Axis

Visibility: public export

data NewAxisConsistent : Axis -> TensorShape k -> Type

Totality: total
Visibility: public export
Constructors:

NewAxis : NotElem (a .name) (name <$> toVect as) -> NewAxisConsistent a as

ExistingAxis : (e : Elem (a .name) (name <$> toVect as)) -> (index (elemToFin e) (toVect as)) .cont = a .cont -> NewAxisConsistent a as

toList : TensorShape k -> List Axis

Visibility: public export

conts : TensorShape k -> List Cont

  Convenience function, turns it also into a list
  Because `Data.Container` uses lists with tensors

Visibility: public export

axisNames : TensorShape k -> Vect k AxisName

  Names of the axes in a tensor shape

Visibility: public export

axisSizes : TensorShape k -> Vect k Cont

  Sizes of the axes in a tensor shape

Visibility: public export

size : (shape : TensorShape k) -> All IsCubical (conts shape) => Nat

  Size of a tensor shape, i.e. its number of elements

Visibility: public export

data InShape : AxisName -> TensorShape k -> Nat -> Type

  Proof that an axis name appears in a tensor shape n times
  The proof indirectly carries data of the exact indices where it appears
  Notably, can appear zero times, this case is needed for recursion

Totality: total
Visibility: public export
Constructors:

Here : InShape axisName as n => {auto {conArg:17216} : NewAxisConsistent (axisName ~> a) as} -> InShape axisName ((axisName ~> a) :: as) (S n)

There : InShape axisName as n => {auto {conArg:17234} : NewAxisConsistent a as} -> InShape axisName (a :: as) n

.getByName : (shape : TensorShape k) -> (axisName : AxisName) -> InShape axisName shape n -> IsSucc n => Axis

  Recovers the axis from a shape given its name, and a prof that it is there
  Recovers the first occurence

Visibility: public export

removeAllOccurrences : (shape : TensorShape rank) -> (toDelete : AxisName) -> InShape toDelete shape k => (m : Nat ** TensorShape m)

Visibility: public export

removeDuplicates : (shape : TensorShape rank) -> (axisName : AxisName) -> InShape axisName shape k => IsSucc k => (m : Nat ** TensorShape m)

  TODO rethink this function?
  In a tensor shape removes all but the first occurence of an axis
  removeDuplicates ["x" ~> 1, "y" ~> 3, "x" ~> 1] "x" = ["x" ~> 1, "y" ~> 1]

Visibility: public export