IdrisDoc: Language.Reflection

Language.Reflection

reflectConstant : ReflConst a => a -> Const
quoteTTRaw : TT -> Raw
quoteTTBinderRaw : Binder TT -> Raw
quoteRawTT : Raw -> TT
quoteRawRaw : Raw -> Raw
quoteRawBinderTT : Binder Raw -> TT
quoteRawBinderRaw : Binder Raw -> Raw
data Universe : Type

The various universes involved in the uniqueness mechanism

NullType : Universe
UniqueType : Universe
AllTypes : Universe
data Tactic : Type

A representation of Idris's old tactics that can be returned from custom
tactic implementations. Generate these using applyTactic.

Try : Tactic -> Tactic -> Tactic

Try the first tactic and resort to the second one on failure

GoalType : String -> Tactic -> Tactic

Only run if the goal has the right type

Refine : TTName -> Tactic

Resolve function name, find matching arguments in the
context and compute the proof target

Seq : Tactic -> Tactic -> Tactic

Apply both tactics in sequence

Claim : TTName -> TT -> Tactic

Introduce a new hole with a particular type

Unfocus : Tactic

Move the current hole to the end

Trivial : Tactic

Intelligently construct the proof target from the context

Search : Int -> Tactic

Build a proof by applying contructors up to a maximum depth

Implementation : Tactic

Resolve an interface

Solve : Tactic

Infer the proof target from the context

Intros : Tactic

introduce all variables into the context

Intro : TTName -> Tactic

Introduce a named variable into the context, use the
first one if the given name is not found

ApplyTactic : TT -> Tactic

Invoke the reflected rep. of another tactic

Reflect : TT -> Tactic

Turn a value into its reflected representation

ByReflection : TT -> Tactic

Use a %reflection function

Fill : Raw -> Tactic

Turn a raw value back into a term

Exact : TT -> Tactic

Use the given value to conclude the proof

Focus : TTName -> Tactic

Focus on a particular hole

Rewrite : TT -> Tactic

Rewrite with an equality

Induction : TT -> Tactic

Perform induction on a particular expression

Case : TT -> Tactic

Perform case analysis on a particular expression

LetTac : TTName -> TT -> Tactic

Name a reflected term

LetTacTy : TTName -> TT -> TT -> Tactic

Name a reflected term and type it

Compute : Tactic

Normalise the goal

Skip : Tactic

Do nothing

Fail : List ErrorReportPart -> Tactic

Fail with an error message

SourceFC : Tactic

Attempt to fill the hole with source code information

data TTUExp : Type
UVar : String -> Int -> TTUExp

Universe variable

UVal : Int -> TTUExp

Explicit universe level

data TTName : Type
UN : String -> TTName

A user-provided name

NS : TTName -> List String -> TTName

A name in some namespace.

The namespace is in reverse order, so (NS (UN "foo") ["B", "A"])
represents the name A.B.foo

MN : Int -> String -> TTName

Machine-chosen names

SN : SpecialName -> TTName

Special names, to make conflicts impossible and language features
predictable

data TT : Type

Reflection of the well typed core language

P : NameType -> TTName -> TT -> TT

A reference to some name (P for Parameter)

V : Int -> TT

de Bruijn variables

Bind : TTName -> Binder TT -> TT -> TT

Bind a variable

App : TT -> TT -> TT

Apply one term to another

TConst : Const -> TT

Embed a constant

Erased : TT

Erased terms

TType : TTUExp -> TT

The type of types along (with universe constraints)

UType : Universe -> TT

Alternative universes for dealing with uniqueness

data SpecialName : Type
WhereN : Int -> TTName -> TTName -> SpecialName
WithN : Int -> TTName -> SpecialName
ImplementationN : TTName -> List String -> SpecialName
ParentN : TTName -> String -> SpecialName
MethodN : TTName -> SpecialName
CaseN : SourceLocation -> TTName -> SpecialName
ElimN : TTName -> SpecialName
ImplementationCtorN : TTName -> SpecialName
MetaN : TTName -> TTName -> SpecialName
record SourceLocation 

A source location in an Idris file

FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation

Either a source span or a source location. start and end
will be the same if it's a point location.

filename

The file name of the source location

start

The line and column of the beginning of the source span

end

The line and column of the end of the source span

filename : (rec : SourceLocation) -> String

The file name of the source location

start : (rec : SourceLocation) -> (Int, Int)

The line and column of the beginning of the source span

end : (rec : SourceLocation) -> (Int, Int)

The line and column of the end of the source span

interface ReflConst 
toConst : ReflConst a => a -> Const
data Raw : Type

Raw terms without types

Var : TTName -> Raw

Variables, global or local

RBind : TTName -> Binder Raw -> Raw -> Raw

Bind a variable

RApp : Raw -> Raw -> Raw

Application

RType : Raw

The type of types

RUType : Universe -> Raw

Alternative universes for dealing with uniqueness

RConstant : Const -> Raw

Embed a constant

interface Quotable 

Things with a canonical representation as a reflected term.

This interface is intended to be used during proof automation and the
construction of custom tactics.

quotedTy : Quotable a t => t

A representation of the type a.

This is to enable quoting polymorphic datatypes

quote : Quotable a t => a -> t

Quote a particular element of a.

Each equation should look something like quote (Foo x y) = `(Foo ~(quote x) ~(quote y))

data NativeTy : Type
IT8 : NativeTy
IT16 : NativeTy
IT32 : NativeTy
IT64 : NativeTy
data NameType : Type

Types of named references

Bound : NameType

A reference which is just bound, e.g. by intro

Ref : NameType

A reference to a de Bruijn-indexed variable

DCon : Int -> Int -> NameType

Data constructor with tag and number

TCon : Int -> Int -> NameType

Type constructor with tag and number

data IntTy : Type
ITFixed : NativeTy -> IntTy
ITNative : IntTy
ITBig : IntTy
ITChar : IntTy
FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation

Either a source span or a source location. start and end
will be the same if it's a point location.

filename

The file name of the source location

start

The line and column of the beginning of the source span

end

The line and column of the end of the source span

data ErrorReportPart : Type

Error reports are a list of report parts

TextPart : String -> ErrorReportPart

A human-readable string

NamePart : TTName -> ErrorReportPart

An Idris name (to be semantically coloured)

TermPart : TT -> ErrorReportPart

An Idris term, to be pretty printed

RawPart : Raw -> ErrorReportPart

A Raw term to be displayed by the compiler

SubReport : List ErrorReportPart -> ErrorReportPart

An indented sub-report, to provide more details

data Const : Type

Primitive constants

I : Int -> Const
BI : Integer -> Const
Fl : Double -> Const
Ch : Char -> Const
Str : String -> Const
B8 : Bits8 -> Const
B16 : Bits16 -> Const
B32 : Bits32 -> Const
B64 : Bits64 -> Const
AType : ArithTy -> Const
StrType : Const
VoidType : Const
Forgot : Const
WorldType : Const
TheWorld : Const
data Binder : (tmTy : Type) -> Type

Types annotations for bound variables in different
binding contexts

tmTy

the terms that can occur inside the binder, as type
annotations or bound values

Lam : (ty : a) -> Binder a

Lambdas

ty

the type of the argument

Pi : (ty : a) -> (kind : a) -> Binder a

Function types.

kind

The kind of arrow. Only relevant when dealing with
uniqueness, so you can usually pretend that this
field doesn't exist. For ordinary functions, use the
type of types here.

Let : (ty : a) -> (val : a) -> Binder a

A let binder

ty

the type of the bound variable

val

the bound value

Hole : (ty : a) -> Binder a

A hole that can occur during elaboration, and must be filled

ty

the type of the value that will eventually be put into the hole

GHole : (ty : a) -> Binder a

A hole that will later become a top-level metavariable

Guess : (ty : a) -> (val : a) -> Binder a

A hole with a solution in it. Computationally inert.

ty

the type of the value in the hole

val

the value in the hole

PVar : (ty : a) -> Binder a

A pattern variable. These bindings surround the terms that make
up the left and right sides of pattern-matching definition
clauses.

ty

the type of the pattern variable

PVTy : (ty : a) -> Binder a

The type of a pattern binding. This is to PVar as Pi is to
Lam.

ty

the type of the pattern variable

data ArithTy : Type
ATInt : IntTy -> ArithTy
ATDouble : ArithTy