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
InstanceN : TTName -> List String -> SpecialName
InstanceCtorN : TTName -> SpecialName
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