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__Search : Int -> List 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.