IdrisDoc: Language.Reflection.Elab

Language.Reflection.Elab

Primitives and tactics for elaborator reflection.

Elaborator reflection allows Idris code to control Idris's
built-in elaborator, and re-use features like the unifier, the
type checker, and the hole mechanism.

Constructor : (name : TTName) -> (arguments : List FunArg) -> (returnType : Raw) -> ConstructorDefn
name

The name of the constructor. The name must not be qualified -
that is, it should begin with the UN or MN constructors.

arguments

The constructor arguments. Idris will infer which arguments are
datatype parameters.

returnType

The specific type constructed by the constructor.

record ConstructorDefn 

A constructor to be associated with a new datatype.

Constructor : (name : TTName) -> (arguments : List FunArg) -> (returnType : Raw) -> ConstructorDefn
name

The name of the constructor. The name must not be qualified -
that is, it should begin with the UN or MN constructors.

arguments

The constructor arguments. Idris will infer which arguments are
datatype parameters.

returnType

The specific type constructed by the constructor.

name : (rec : ConstructorDefn) -> TTName

The name of the constructor. The name must not be qualified -
that is, it should begin with the UN or MN constructors.

arguments : (rec : ConstructorDefn) -> List FunArg

The constructor arguments. Idris will infer which arguments are
datatype parameters.

returnType : (rec : ConstructorDefn) -> Raw

The specific type constructed by the constructor.

data CtorArg : Type
CtorParameter : FunArg -> CtorArg
CtorField : FunArg -> CtorArg
record DataDefn 

A definition of a datatype to be added during an elaboration script.

DefineDatatype : (name : TTName) -> (constructors : List ConstructorDefn) -> DataDefn
name

The name of the datatype being defined. It must be
fully-qualified, and it must have been previously declared as a
datatype.

constructors

A list of constructors for the datatype.

name : (rec : DataDefn) -> TTName

The name of the datatype being defined. It must be
fully-qualified, and it must have been previously declared as a
datatype.

constructors : (rec : DataDefn) -> List ConstructorDefn

A list of constructors for the datatype.

record Datatype 

A reflected datatype definition

MkDatatype : (name : TTName) -> (tyConArgs : List TyConArg) -> (tyConRes : Raw) -> (constructors : List (TTName, List CtorArg, Raw)) -> Datatype
name

The name of the type constructor

tyConArgs

The arguments to the type constructor

tyConRes

The result of the type constructor

constructors

The constructors for the family

name : (rec : Datatype) -> TTName

The name of the type constructor

tyConArgs : (rec : Datatype) -> List TyConArg

The arguments to the type constructor

tyConRes : (rec : Datatype) -> Raw

The result of the type constructor

constructors : (rec : Datatype) -> List (TTName, List CtorArg, Raw)

The constructors for the family

Declare : (name : TTName) -> (arguments : List FunArg) -> (returnType : Raw) -> TyDecl
name

The fully-qualified name of the function or datatype being declared.

arguments

Each argument is in the scope of the names of previous arguments.

returnType

The return type is in the scope of all the argument names.

DefineDatatype : (name : TTName) -> (constructors : List ConstructorDefn) -> DataDefn
name

The name of the datatype being defined. It must be
fully-qualified, and it must have been previously declared as a
datatype.

constructors

A list of constructors for the datatype.

DefineFun : (name : TTName) -> (clauses : List (FunClause a)) -> FunDefn a
data Elab : Type -> Type

A reflected elaboration script.

Prim__PureElab : a -> Elab a
Prim__BindElab : Elab a -> (a -> Elab b) -> Elab b
Prim__Try : Elab a -> Elab a -> Elab a
Prim__TryCatch : Elab a -> (Err -> Elab a) -> Elab a
Prim__Fail : List ErrorReportPart -> Elab a
Prim__Env : Elab (List (TTName, Binder TT))
Prim__Goal : Elab (TTName, TT)
Prim__Holes : Elab (List TTName)
Prim__Guess : Elab TT
Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
Prim__LookupDatatype : TTName -> Elab (List Datatype)
Prim__LookupFunDefn : TTName -> Elab (List (FunDefn TT))
Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)
Prim__SourceLocation : Elab SourceLocation
Prim__Namespace : Elab (List String)
Prim__Gensym : String -> Elab TTName
Prim__Solve : Elab ()
Prim__Fill : Raw -> Elab ()
Prim__Apply : Raw -> List Bool -> Elab (List (TTName, TTName))
Prim__MatchApply : Raw -> List Bool -> Elab (List (TTName, TTName))
Prim__Focus : TTName -> Elab ()
Prim__Unfocus : TTName -> Elab ()
Prim__Attack : Elab ()
Prim__Rewrite : Raw -> Elab ()
Prim__Claim : TTName -> Raw -> Elab ()
Prim__Intro : Maybe TTName -> Elab ()
Prim__Forall : TTName -> Raw -> Elab ()
Prim__PatVar : TTName -> Elab ()
Prim__PatBind : TTName -> Elab ()
Prim__LetBind : TTName -> Raw -> Raw -> Elab ()
Prim__Compute : Elab ()
Prim__Normalise : List (TTName, Binder TT) -> TT -> Elab TT
Prim__Whnf : TT -> Elab TT
Prim__Converts : List (TTName, Binder TT) -> TT -> TT -> Elab ()
Prim__DeclareType : TyDecl -> Elab ()
Prim__DefineFunction : FunDefn Raw -> Elab ()
Prim__DeclareDatatype : TyDecl -> Elab ()
Prim__DefineDatatype : DataDefn -> Elab ()
Prim__AddImplementation : TTName -> TTName -> Elab ()
Prim__IsTCName : TTName -> Elab Bool
Prim__ResolveTC : TTName -> Elab ()
Prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
Prim__Fixity : String -> Elab Fixity
Prim__Debug : List ErrorReportPart -> Elab a
Prim__Metavar : TTName -> Elab ()
data Erasure : Type

Erasure annotations reflect Idris's idea of what is intended to be
erased.

Erased : Erasure
NotErased : Erasure
data Fixity : Type
Infixl : Nat -> Fixity
Infixr : Nat -> Fixity
Infix : Nat -> Fixity
Prefix : Nat -> Fixity
record FunArg 

Function arguments

These are the simplest representation of argument lists, and are
used for functions. Additionally, because a FunArg provides enough
information to build an application, a generic type lookup of a
top-level identifier will return its FunArgs, if applicable.

MkFunArg : (name : TTName) -> (type : Raw) -> (plicity : Plicity) -> (erasure : Erasure) -> FunArg
name : (rec : FunArg) -> TTName
type : (rec : FunArg) -> Raw
plicity : (rec : FunArg) -> Plicity
erasure : (rec : FunArg) -> Erasure
data FunClause : Type -> Type

A single pattern-matching clause

MkFunClause : (lhs : a) -> (rhs : a) -> FunClause a
MkImpossibleClause : (lhs : a) -> FunClause a
record FunDefn a

A reflected function definition.

a
 
DefineFun : (name : TTName) -> (clauses : List (FunClause a)) -> FunDefn a
name : (rec : FunDefn a) -> TTName
clauses : (rec : FunDefn a) -> List (FunClause a)
MkDatatype : (name : TTName) -> (tyConArgs : List TyConArg) -> (tyConRes : Raw) -> (constructors : List (TTName, List CtorArg, Raw)) -> Datatype
name

The name of the type constructor

tyConArgs

The arguments to the type constructor

tyConRes

The result of the type constructor

constructors

The constructors for the family

MkFunArg : (name : TTName) -> (type : Raw) -> (plicity : Plicity) -> (erasure : Erasure) -> FunArg
data Plicity : Type

How an argument is provided in high-level Idris

Explicit : Plicity

The argument is directly provided at the application site

Implicit : Plicity

The argument is found by Idris at the application site

Constraint : Plicity

The argument is solved using interface resolution

data TyConArg : Type

Type constructor arguments

Each argument is identified as being either a parameter that is
consistent in all constructors, or an index that varies based on
which constructor is selected.

TyConParameter : FunArg -> TyConArg

Parameters are uniform across the constructors

TyConIndex : FunArg -> TyConArg

Indices are not uniform

record TyDecl 

A type declaration for a function or datatype

Declare : (name : TTName) -> (arguments : List FunArg) -> (returnType : Raw) -> TyDecl
name

The fully-qualified name of the function or datatype being declared.

arguments

Each argument is in the scope of the names of previous arguments.

returnType

The return type is in the scope of all the argument names.

name : (rec : TyDecl) -> TTName

The fully-qualified name of the function or datatype being declared.

arguments : (rec : TyDecl) -> List FunArg

Each argument is in the scope of the names of previous arguments.

returnType : (rec : TyDecl) -> Raw

The return type is in the scope of all the argument names.