Compiler.IR

For internal spidr use only.

Reexports

Definitions

data ValueType : Type

Totality: total
Visibility: public export
Constructors:

TensorType : Shape -> DType -> ValueType

  A concrete tensor type

TypeRef : Nat -> Nat -> ValueType

  Points to the type of the value at this index and tag

Hint: 

Show ValueType

record Env : Type

Totality: total
Visibility: public export
Constructor: 

MkEnv : Nat -> List (Nat, Op) -> Env

Projections:

.counter : Env -> Nat

  The global counter

.ops : Env -> List (Nat, Op)

  Local cached ops

.counter : Env -> Nat

  The global counter

Totality: total
Visibility: public export

counter : Env -> Nat

  The global counter

Totality: total
Visibility: public export

.ops : Env -> List (Nat, Op)

  Local cached ops

Totality: total
Visibility: public export

ops : Env -> List (Nat, Op)

  Local cached ops

Totality: total
Visibility: public export

empty : Env

Totality: total
Visibility: export

emptyFrom : Env -> Env

Totality: total
Visibility: export

updateCounterFrom : Env -> State Env ()

Totality: total
Visibility: export

data Value : Type

Totality: total
Visibility: public export
Constructor: 

V : Nat -> OpRef -> Value

record Fn : Nat -> Type

  An anonymous function. Approximates an MLIR `Region` or `Block` (these are somewhat synonymous
  in spidr since all regions have exactly one block). `tag` labels the parameter set.

Totality: total
Visibility: public export
Constructor: 

MkFn : Nat -> Vect arity ValueType -> Vect resultCount ValueType -> Vect resultCount Value -> Env -> Fn arity

Projections:

.env : Fn arity -> Env

.paramTypes : Fn arity -> Vect arity ValueType

0 .resultCount : Fn arity -> Nat

.resultTypes : ({rec:0} : Fn arity) -> Vect (resultCount {rec:0}) ValueType

.results : ({rec:0} : Fn arity) -> Vect (resultCount {rec:0}) Value

.tag : Fn arity -> Nat

Hint: 

Show (Fn arity)

.tag : Fn arity -> Nat

Totality: total
Visibility: public export

tag : Fn arity -> Nat

Totality: total
Visibility: public export

.paramTypes : Fn arity -> Vect arity ValueType

Totality: total
Visibility: public export

paramTypes : Fn arity -> Vect arity ValueType

Totality: total
Visibility: public export

.resultTypes : ({rec:0} : Fn arity) -> Vect (resultCount {rec:0}) ValueType

Totality: total
Visibility: public export

resultTypes : ({rec:0} : Fn arity) -> Vect (resultCount {rec:0}) ValueType

Totality: total
Visibility: public export

.results : ({rec:0} : Fn arity) -> Vect (resultCount {rec:0}) Value

Totality: total
Visibility: public export

results : ({rec:0} : Fn arity) -> Vect (resultCount {rec:0}) Value

Totality: total
Visibility: public export

.env : Fn arity -> Env

Totality: total
Visibility: public export

env : Fn arity -> Env

Totality: total
Visibility: public export

data BinaryOp : Type

Totality: total
Visibility: public export
Constructors:

Compare : ComparisonDirection -> BinaryOp

And : BinaryOp

Or : BinaryOp

Add : BinaryOp

Sub : BinaryOp

Mul : BinaryOp

Div : BinaryOp

Rem : BinaryOp

Pow : BinaryOp

Min : BinaryOp

Max : BinaryOp

ShiftRightLogical : BinaryOp

Hint: 

Show BinaryOp

data UnaryOp : Type

Totality: total
Visibility: public export
Constructors:

Not : UnaryOp

Neg : UnaryOp

Ceil : UnaryOp

Floor : UnaryOp

Abs : UnaryOp

Log : UnaryOp

Exp : UnaryOp

Logistic : UnaryOp

Sqrt : UnaryOp

Sin : UnaryOp

Cos : UnaryOp

Tan : UnaryOp

Tanh : UnaryOp

Erf : UnaryOp

ErfInv : UnaryOp

Square : UnaryOp

Asin : UnaryOp

Acos : UnaryOp

Atan : UnaryOp

Sinh : UnaryOp

Cosh : UnaryOp

Asinh : UnaryOp

Acosh : UnaryOp

Atanh : UnaryOp

Hint: 

Show UnaryOp

data Op : Type

Totality: total
Visibility: public export
Constructors:

NamedFunc : Fn arity -> Op

  Corresponds approximately to a FuncOp. The FuncOp's name is determined by the `Fn`s tag.
  We use the tag to correspond to both the parameter set and the function itself. I think this
  is OK because the function determines the parameter set (notably we don't introduce any
  regions with multiple blocks, so each FuncOp only has one block).
  
  The function is assumed **not** to capture variables, see `Passes.removeCaptures`.

CallByName : Nat -> List ValueType -> List Value -> Op

  Call a named function, by name.
  
  The named functions must be listed in the `Env`, else it will not be interpreted.

Lit : (shape : Shape) -> (dtype : DType) -> Literal shape (idrisType dtype) -> Op

Grad : Shape -> Fn 1 -> Value -> Op

MinValue : DType -> Op

MaxValue : DType -> Op

MinFiniteFloat : Op

MaxFiniteFloat : Op

Iota : Shape -> DType -> Nat -> Op

BitCastConvert : DType -> Shape -> Value -> Op

Convert : DType -> Shape -> Value -> Op

Reshape : DType -> Shape -> Value -> Op

Slice : List Nat -> List Nat -> List Nat -> Value -> Op

DynamicSlice : List Value -> List Nat -> Value -> Op

Concat : Nat -> Vect (S n) Value -> Op

Transpose : List Nat -> Value -> Op

Broadcast : DType -> Shape -> Shape -> Value -> Op

Map : Fn arity -> Vect arity Value -> ValueType -> Shape -> Op

Reduce : Fn (n + n) -> Vect n Value -> List Nat -> Vect n Value -> Op

Sort : Fn 2 -> Nat -> Bool -> Value -> Op

Reverse : List Nat -> Value -> Op

BinaryElementwise : BinaryOp -> Value -> Value -> Op

UnaryElementwise : UnaryOp -> Value -> Op

Select : Value -> Value -> Value -> Op

While : Fn n -> Fn n -> Vect n Value -> Op

If : ValueType -> Value -> Fn 0 -> Fn 0 -> Op

DotGeneral : List Nat -> List Nat -> List Nat -> List Nat -> ValueType -> Value -> Value -> Op

Cholesky : Value -> Op

TriangularSolve : Value -> Value -> Bool -> Op

Rng : Value -> ValueType -> Op

data OpRef : Type

Totality: total
Visibility: public export
Constructors:

BoundSet : Nat -> OpRef

Concrete : Op -> OpRef

Hint: 

Taggable OpRef

tagOpRef : Monad m => OpRef -> StateT Env m OpRef

Totality: total
Visibility: export

reserve : State Env Nat

Totality: total
Visibility: export