Spidr.Data.Literal

Defines `Literal`, a single value or array of values with a specified shape.
`Literal` is similar to `Tensor`, but differs in a number of important ways:

* `Literal` offers a convenient syntax for constructing `Literal`s with boolean and numeric
  contents. For example, `True`, `1` and `[1, 2, 3]` are all valid `Literal`s. This makes it
  useful for constructing `Tensor`s.
* Operations on `Literal` are *not* accelerated by a graph compiler, so operations on large
  `Literal`s, and large sequences of operations on any `Literal`, can be expected to be slower
  than they would on an equivalent `Tensor`.
* `Literal` is implemented in pure Idris. As such, values can contain elements of any type, and
  implements a number of standard Idris interfaces. This, along with its convenient syntax,
  makes it particularly useful for testing operations on `Tensor`s.

Reexports

Definitions

data Literal : Shape -> Type -> Type

  A scalar or array of values.

Totality: total
Visibility: public export
Constructors:

Scalar : a -> Literal [] a

Nil : Literal (0 :: ds) a

(::) : Literal ds a -> Literal (d :: ds) a -> Literal (S d :: ds) a

Hints:

Applicative (Literal shape)

Cast (Array shape a) (Literal shape a)

Eq a => Eq (Literal shape a)

Foldable (Literal shape)

Functor (Literal shape)

Num a => Num (Literal [] a)

Show a => Show (Literal shape a)

Traversable (Literal shape)

Zippable (Literal shape)

fromInteger : Num a => Integer -> Literal [] a

Totality: total
Visibility: export

fromDouble : Double -> Literal [] Double

Totality: total
Visibility: export

True : Literal [] Bool

  Convenience aliases for scalar boolean literals.

Totality: total
Visibility: export

False : Literal [] Bool

  Convenience aliases for scalar boolean literals.

Totality: total
Visibility: export

all : Literal shape Bool -> Bool

  `True` if no elements are `False`. `all []` is `True`.

Totality: total
Visibility: export

negate : Neg a => Literal shape a -> Literal shape a

Totality: total
Visibility: export
Fixity Declaration: prefix operator, level 10

data All : (0 _ : (a -> Type)) -> Literal shape a -> Type

  An `All p xs` is an array (or scalar) of proofs about each element in `xs`.
  
  For example, an `All IsSucc xs` proves that every element in `xs` is non-zero.

Totality: total
Visibility: public export
Constructors:

Scalar : p x -> All p (Scalar x)

Nil : All p []

(::) : All p x -> All p xs -> All p (x :: xs)

data All2 : (a -> b -> Type) -> Literal shape a -> Literal shape b -> Type

  An `All2 p xs ys` is an array (or scalar) of pairwise proofs about elements in `xs` and `ys`.
  
  For example, an `All2 LT xs ys` proves that each number in `xs` is less than the number in
  `ys` at the same position.

Totality: total
Visibility: public export
Constructors:

Scalar : p a b -> All2 p (Scalar a) (Scalar b)

Nil : All2 p [] []

(::) : All2 p a b -> All2 p as bs -> All2 p (a :: as) (b :: bs)