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)

AllC TensorMonoid shape => Cast Nat a => Cast Nat (Tensor shape a)

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)

AllC IsConcrete shape => Materialise (Tensor shape a)

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

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

Random a => AllC TensorMonoid shape => Traversable (Tensor shape) => Random (Tensor shape a)

Num a => AllC TensorMonoid shape => AllDisplay2D shape a => TensorCubEvidence shape => ScientificDisplay (Tensor shape a)

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

Sqrt a => AllC TensorMonoid shape => Sqrt (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:12659} : ConsistentWith a as} -> axisName = a .name => Elem axisName (a :: as)

There : {auto {conArg:12681} : 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:12724} : 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`

Totality: total
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

Totality: total
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

Totality: total
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:12887} : 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:12920} : ConsistentWith a as} -> p a -> Any p (a :: as)

There : {auto {conArg:12946} : 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:13000} : 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)

AllC TensorMonoid shape => Cast Nat a => Cast Nat (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)

AllC IsConcrete shape => Materialise (Tensor shape a)

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

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

Random a => AllC TensorMonoid shape => Traversable (Tensor shape) => Random (Tensor shape a)

Num a => AllC TensorMonoid shape => AllDisplay2D shape a => TensorCubEvidence shape => ScientificDisplay (Tensor shape a)

Sqrt a => AllC TensorMonoid shape => Sqrt (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:13033} : ConsistentWith a as} -> p (a .cont) -> AnyC p (a :: as)

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

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

Totality: total
Visibility: public export

toVect : TensorShape k -> Vect k Axis

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

Totality: total
Visibility: public export

toList : TensorShape k -> List Axis

Totality: total
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

Totality: total
Visibility: public export

toAll : AllC p shape -> All p (conts shape)

  A property of every axis's container, as a property of the list `conts`

Totality: total
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

Totality: total
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.

Totality: total
Visibility: public export

axisNames : TensorShape k -> Vect k AxisName

  Names of the axes in a tensor shape

Totality: total
Visibility: public export

axisSizes : TensorShape k -> Vect k Cont

  Sizes of the axes in a tensor shape

Totality: total
Visibility: public export

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

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

Totality: total
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.

Totality: total
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:13397} : ConsistentWith ax as} -> UniqueElem axisName (ax :: as)

There : IsSucc rank => UniqueElem axisName as => IsNo (decEq axisName (ax .name)) => {auto {conArg:13427} : 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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

removedNotElem : (toRemove : AxisName) -> (as : TensorShape (S rank)) -> {auto uElem : UniqueElem toRemove as} -> NotElem toRemove (removeAxis toRemove as)

  After removing the (unique) axis name `toRemove`, said name no longer
  appears in the shape

Totality: total
Visibility: public export

notElemAfterRemoving : (x : AxisName) -> (as : TensorShape (S rank)) -> NotElem x as -> (toRemove : AxisName) -> {auto uElem : UniqueElem toRemove as} -> NotElem x (removeAxis toRemove as)

  A name absent from a shape is still absent after removing an axis

Totality: total
Visibility: public export

indexAfterRemoving : (x : AxisName) -> (as : TensorShape (S rank)) -> (e : Elem x as) -> (toRemove : AxisName) -> {auto uElem : UniqueElem toRemove as} -> IsNo (decEq x toRemove) => (e' : Elem x (removeAxis toRemove as) ** index (removeAxis toRemove as) x = index as x)

  A name different from `toRemove` that appears in a shape still appears
  after the removal, and indexes the same container

Totality: total
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)

  Proof that an axis `a` is consistent with `as` after removing the axis 
  name `toRemove` from `as`

Totality: total
Visibility: public export

TensorTest1 : TensorShape 3

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export