data Tag : Type- Totality: total
Visibility: public export
Constructors:
DataCon : Int -> Name -> Tag A data constructor. Use the tag to dispatch / construct.
Here the Name is only for documentation purposes and should not
be used.
TypeCon : Name -> Tag A type constructor. We do not have a unique tag associated to types
and so we match on names instead.
data Var : Type A variable in a toplevel function definition
When generating the syntax tree of imperative
statements and expressions, we decide - based on
codegen directives - which Idris names to keep
and which names to convert to short, mangled
versions.
Totality: total
Visibility: public export
Constructors:
VName : Name -> Var An unaltered name - usually a toplevel function
or a function argument with an explicitly given
name
VLoc : Int -> Var Index of a local variables
VRef : Int -> Var Index of a mangled toplevel function
data Minimal : Type A minimal expression.
Totality: total
Visibility: public export
Constructors:
MVar : Var -> Minimal A variable
MProjection : Nat -> Minimal -> Minimal A projection targeting the field of a data type.
We include these here since it allows us to
conveniently carry around a `SortedMap Name Minimal`
for name resolution during the generation of the
imperative syntax tree.
data Effect : Type The effect of a statement or a block of statements.
`Returns` means the
result of the final expression will be returned as
the current function's result, while `ErrorWithout v`
is a reminder, that the block of code will eventually
assign a value to `v` and will fail to do so if
`v` hasn't previously been declared.
This is used as a typelevel index to prevent us from
making some common stupid errors like declaring a variable
twice, or having several `return` statements in the same
block of code.
Totality: total
Visibility: public export
Constructors:
Returns : EffectErrorWithout : Var -> Effect
data Exp : Type An expression in a function definition.
Totality: total
Visibility: public export
Constructors:
EMinimal : Minimal -> Exp A variable or projection. Minimal expressions
will always be inlined unless explicitly bound
in an Idris2 `let` expression.
ELam : List Var -> Stmt (Just Returns) -> Exp Lambda expression
An empty argument list represents a delayed computation
EApp : Exp -> List Exp -> Exp Function application.
In case of a zero-argument list, we might also be
dealing with forcing a delayed computation.
ECon : Tag -> ConInfo -> List Exp -> Exp Saturated construtor application.
The tag either represents the name of a type constructor
(when we are pattern matching on types) or the index
of a data constructor.
EOp : PrimFn arity -> Vect arity Exp -> Exp Primitive operation
EExtPrim : Name -> List Exp -> Exp Externally defined primitive operation.
EPrimVal : Constant -> Exp A constant primitive.
EErased : Exp An erased value.
data Stmt : Maybe Effect -> Type An imperative statement in a function definition.
This is indexed over the `Effect` the statement,
will have.
An `effect` of `Nothing` means that the result of
the statement is `undefined`: The declaration of
a constant or assignment of a previously declared
variable. When we sequence statements in a block
of code, all but the last one of them must have
effect `Nothing`. This makes sure we properly declare variables
exactly once before eventually assigning them.
It makes also sure a block of code does not contain
several `return` statements (until they are the
results of the branches of a `switch` statement).
Totality: total
Visibility: public export
Constructors:
Return : Exp -> Stmt (Just Returns) Returns the result of the given expression.
Const : Var -> Exp -> Stmt Nothing Introduces a new constant by assigning the result
of a single expression to the given variable.
Assign : (v : Var) -> Exp -> Stmt (Just (ErrorWithout v)) Assigns the result of an expression to the given variable.
This will result in an error, if the variable has not
yet been declared.
Declare : (v : Var) -> Stmt (Just (ErrorWithout v)) -> Stmt Nothing Declares (but does not yet assign) a new mutable
variable. This is the only way to "saturate"
a `Stmt (Just $ ErrorWithout v)`.
ConSwitch : (e : Effect) -> Minimal -> List (EConAlt e) -> Maybe (Stmt (Just e)) -> Stmt (Just e) Switch statement from a pattern match on
data or type constructors. The result of each branch
will have the given `Effect`.
The scrutinee has already been lifted to
the outer scope to make sure it is only
evaluated once.
ConstSwitch : (e : Effect) -> Exp -> List (EConstAlt e) -> Maybe (Stmt (Just e)) -> Stmt (Just e) Switch statement from a pattern on
a constant. The result of each branch
will have the given `Effect`.
Error : String -> Stmt (Just any) A runtime exception.
Block : List1 (Stmt Nothing) -> Stmt e -> Stmt e A code block consisting of one or more
imperative statements.
record EConAlt : Effect -> Type Single branch in a pattern match on a data or
type constructor.
Totality: total
Visibility: public export
Constructor: MkEConAlt : Tag -> ConInfo -> Stmt (Just e) -> EConAlt e
Projections:
.body : EConAlt e -> Stmt (Just e).conInfo : EConAlt e -> ConInfo.tag : EConAlt e -> Tag
.tag : EConAlt e -> Tag- Totality: total
Visibility: public export tag : EConAlt e -> Tag- Totality: total
Visibility: public export .conInfo : EConAlt e -> ConInfo- Totality: total
Visibility: public export conInfo : EConAlt e -> ConInfo- Totality: total
Visibility: public export .body : EConAlt e -> Stmt (Just e)- Totality: total
Visibility: public export body : EConAlt e -> Stmt (Just e)- Totality: total
Visibility: public export record EConstAlt : Effect -> Type Single branch in a pattern match on a constant
Totality: total
Visibility: public export
Constructor: MkEConstAlt : Constant -> Stmt (Just e) -> EConstAlt e
Projections:
.body : EConstAlt e -> Stmt (Just e).constant : EConstAlt e -> Constant
.constant : EConstAlt e -> Constant- Totality: total
Visibility: public export constant : EConstAlt e -> Constant- Totality: total
Visibility: public export .body : EConstAlt e -> Stmt (Just e)- Totality: total
Visibility: public export body : EConstAlt e -> Stmt (Just e)- Totality: total
Visibility: public export toMinimal : Exp -> Maybe Minimal- Totality: total
Visibility: export prepend : List (Stmt Nothing) -> Stmt (Just e) -> Stmt (Just e)- Totality: total
Visibility: export declare : Stmt (Just (ErrorWithout v)) -> Stmt Nothing- Totality: total
Visibility: export