Data.Tensor.Shape.Shape

Reexports

Definitions

data TensorShape : Nat -> Type

  Datatype defining the shape of a tensor
  It is a vector of consistently named axes

Totality: total
Visibility: public export
Constructors:

Nil : TensorShape 0

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

Hints:

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

AllAlgebra shape a => Algebra (Tensor shape) a

All IsCubical shape -> AllC IsFoldable shape

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)

data ConsistentWith : Axis -> TensorShape k -> Type

  An axis is named consistently with respect to an existing tensor shape
  if its name does not appear in the shape, or it if it appears and
  references the same container

Totality: total
Visibility: public export
Constructors:

NewAxis : NotElem (a .name) as -> ConsistentWith a as

ExistingAxis : (e : Elem (a .name) as) -> index as (a .name) = a .cont -> ConsistentWith a as

data Elem : AxisName -> TensorShape rank -> Type

  A proof that an axis name `a` is found in a tensor shape `as`
  Notably this could have been implemented to check whether the 
  *entire axis* is in vector, and not just the name.
  But since a tensor shape is more akin to a dictionary, keeping this form

Totality: total
Visibility: public export
Constructors:

Here : {auto {conArg:17303} : ConsistentWith a as} -> axisName = a .name => Elem axisName (a :: as)

There : {auto {conArg:17325} : ConsistentWith a as} -> Elem axisName as => Elem axisName (a :: as)

data NotElem : AxisName -> TensorShape rank -> Type

  A proof that an axis name `a` is not found in a tensor shape `as`

Totality: total
Visibility: public export
Constructors:

NotInEmpty : NotElem axisElem []

NotInNonEmpty : IsNo (decEq axisElem (a .name)) -> NotElem axisElem as => ({arg:17368} : ConsistentWith a as) -> NotElem axisElem (a :: as)

index : (shape : TensorShape rank) -> (axisName : AxisName) -> Elem axisName shape => Cont

  Indexing into a tensor shape.
  Could be many occurences - recovers the one provided by `isElem`

Visibility: public export

rename : TensorShape rank -> AxisName -> AxisName -> TensorShape rank

  to get rid of believe_me this might need to be put in a mutual block too

Visibility: public export

rename : TensorShape rank -> Fin rank -> AxisName -> TensorShape rank

  to get rid of believe_me this might need to be put in a mutual block too

Visibility: public export

data All : (Axis -> Type) -> TensorShape k -> Type

Totality: total
Visibility: public export
Constructors:

Nil : All p []

(::) : p a -> All p as -> {auto {conArg:17531} : ConsistentWith a as} -> All p (a :: as)

Hint: 

All IsCubical shape -> AllC IsFoldable shape

data Any : (Axis -> Type) -> TensorShape k -> Type

Totality: total
Visibility: public export
Constructors:

Here : {auto {conArg:17564} : ConsistentWith a as} -> p a -> Any p (a :: as)

There : {auto {conArg:17590} : ConsistentWith a as} -> Any p as -> Any p (a :: as)

data AllC : (Cont -> Type) -> TensorShape k -> Type

Totality: total
Visibility: public export
Constructors:

Nil : AllC p []

(::) : p (a .cont) -> AllC p as -> {auto {conArg:17644} : ConsistentWith a as} -> AllC p (a :: as)

Hints:

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

All IsCubical shape -> AllC IsFoldable shape

AllC TensorMonoid shape => Applicative (Tensor shape)

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)

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

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

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

data AnyC : (Cont -> Type) -> TensorShape k -> Type

Totality: total
Visibility: public export
Constructors:

Here : {auto {conArg:17677} : ConsistentWith a as} -> p (a .cont) -> AnyC p (a :: as)

There : {auto {conArg:17703} : ConsistentWith a as} -> AnyC p as -> AnyC p (a :: as)

tensorShapesConsistent : TensorShape k -> TensorShape k' -> Type

Visibility: public export

toVect : TensorShape k -> Vect k Axis

  (::) here pattern matches on the proof `axisConsistent` and discards it

Visibility: public export

toList : TensorShape k -> List Axis

Visibility: public export

conts : TensorShape k -> List Cont

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

Visibility: public export

renamePreservesConts : (shape : TensorShape rank) -> (axisName : AxisName) -> (newAxisName : AxisName) -> conts (rename shape axisName newAxisName) = conts shape

  Renaming the shape preserves the underlying data

Visibility: public export

renamePreservesConts : (shape : TensorShape rank) -> (axisIndex : Fin rank) -> (newAxisName : AxisName) -> conts (rename shape axisIndex newAxisName) = conts shape

  Renaming a shape at a specific index preserves the underlying containers.

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

0 TensorCubEvidence : TensorShape k -> Type

  Cubicality evidence for a tensor shape, using `Either` so that
  auto-search tries `Left prf` (positive evidence) before `Right ()`
  (fallback). Standard `Maybe` can't be used because `Nothing` is
  listed first in its definition and auto-search would always pick it.

Visibility: public export

data UniqueElem : AxisName -> TensorShape rank -> Type

  A proof that an axis name only appears once in the tensor shape

Totality: total
Visibility: public export
Constructors:

Here : axisName = ax .name => NotElem axisName as => {auto {conArg:17995} : ConsistentWith ax as} -> UniqueElem axisName (ax :: as)

There : IsSucc rank => UniqueElem axisName as => IsNo (decEq axisName (ax .name)) => {auto {conArg:18025} : ConsistentWith ax as} -> UniqueElem axisName (ax :: as)

forgetUnique : UniqueElem axisName as -> Elem axisName as

  Forgets that the axis name only appears once in the tensor shape

Visibility: public export

index : (shape : TensorShape rank) -> (axisName : AxisName) -> UniqueElem axisName shape => Cont

Visibility: public export

removeAxis : (toRemove : AxisName) -> (shape : TensorShape (S rank)) -> UniqueElem toRemove shape => TensorShape rank

Visibility: public export

consistentAfterRemoving : (a : Axis) -> (as : TensorShape (S rank)) -> ConsistentWith a as => (toRemove : AxisName) -> {auto uElem : UniqueElem toRemove as} -> ConsistentWith a (removeAxis toRemove as)

Visibility: public export

TensorTest1 : TensorShape 3

Visibility: public export

TensorTest2 : (i : Axis) -> ConsistentWith i [i]

Visibility: public export