Primitives and tactics for elaborator reflection.
- 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.
- 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
- 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
- MkFunArg : (name : TTName) ->
(type : Raw) ->
(plicity : Plicity) ->
(erasure : Erasure) ->
FunArg
- 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
- 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)
- data FunClause : Type ->
Type
A single pattern-matching clause
- MkFunClause : (lhs : a) ->
(rhs : a) ->
FunClause a
- MkImpossibleClause : (lhs : a) ->
FunClause a
- 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 Fixity : Type
- Infixl : Nat ->
Fixity
- Infixr : Nat ->
Fixity
- Infix : Nat ->
Fixity
- Prefix : Nat ->
Fixity
- data Erasure : Type
Erasure annotations reflect Idris's idea of what is intended to be
erased.
- Erased : Erasure
- NotErased : Erasure
- 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__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 ()
- DefineFun : (name : TTName) ->
(clauses : List (FunClause a)) ->
FunDefn a
- 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.
- 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.
- 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
- 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.
- data CtorArg : Type
- CtorParameter : FunArg ->
CtorArg
- CtorField : FunArg ->
CtorArg
- 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.
- 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.