Elaborator Reflection - Tactics

Proof State

elaborator

Tactics operate on the proof state. The proof state contains various pieces of information, at this stage, the important ones for us are:

from David Christiansen paper:

There are many other pieces of information in the proof state such as the names used but, for now, we will leave the system to handle these.

elab proof state

proof state

Elaborator Reflection

The Idris part of the code for elaborator reflection is in

 Idris-dev/libs/prelude/Language/Reflection/Elab.idr 

Before we look at the Elab monad we need to know how to construct terms.

Names TTName

Names in an Idris program are evaluated at runtime but sometimes we need a 'variable name' which can be referred to as an unevaluated symbol.

The names used in terms have different constructors depending on their type:

UN String A user-provided name
NS (UN "foo") ["B", "A"]) A name in some namespace
MN Int String Machine-chosen names
SN SpecialName Special names, to make conflicts impossible and language features predictable

 

A user defined name can be constructed like this:
Idris> UN "x"
UN "x" : TTName
 
Idris> NS (UN "x") ["b","a"]
NS (UN "x") ["b", "a"] : TTName
   

A machine-chosen name needs to be generated within an Elab monad (see below for details) and is unique within that monad:

This produced: {abc_140}{abc_141}

So although gensym "abc" was called twice each one had a different integer.

 

implementation Show TTName where
  show (UN s) = "`{{"++s++"}}"
  show (NS t a) = "{"++(show t)++"."++(show a)++"}"
  show (MN i s) = "{"++s++"_"++(show i)++"}"
  show (SN sn) = "TTName special name"
  
showGensym : String
showGensym = %runElab (do
         debugMessage [TextPart (
           show !(gensym "abc") ++
             show !(gensym "abc")
           )]
         )

 

Quasiquotation

Since names are used frequently in elaborator reflection there is a shortcut for constructing them:

 
Idris> `{{x}}
UN "x" : TTName
 
Idris> `{x}
No such variable x
Idris> :let x=2
Idris> `{x}
UN "x" : TTName
 
Idris> :let a=2
Idris> `(a)
P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
 
Idris> `(a:Integer)
P Ref (UN "a") (TConst (AType (ATInt ITBig))) : TT
 
Idris> `(~a)
2 : Integer

quasiquotation summary:

  Reification  
`{{n}} TTName Use for new names. Unresolved quotation of the name n.
`{n} TTName Use for existing names. Resolved quotation of the name n. n is a reference to a unique name in scope.
`(e)   expression e for which a type is inferable.
`(e:t)   expression e with a given type e.
~a   anti-quotation - sub region which can be evaluated rather than quoted.
(Var `{{x}}) Raw  

TT:

There is a notation for a term in TT as it is being constructed (based on a BNF-like grammar), this is used for example in the debug output, it is a compact way to see the state of the term so we use it here.

So internally the program is stored as a tree structure using the following syntax:

    Syntax More Information
term   t  
binding   b  
constant t ::= c  
variable t ::= x  
variable binding t ::= b.t so a dot '.' tells us this is some sort of binding.
application t ::= t t As with Idris, juxtaposition indicates function application. Note: we use the same symbol 't' for terms
Type constructor t ::= T  
Data constructor t ::= C  
function b::= λ c:t colon ':' separates parameters from body of binding.
let binding b::= let |-> t:t  
function b::= ∀ x:t  
Type universe c::= *i The universe hierarchy is usually handled automatically so we can just use * for the type of types.
integer literal c:== i  
integer type c:== Integer  
string literal c:== s  
string type c:== String  
focused hole   ?x : t Conor McBride 1999 thesis.
guess   ?x ≈ t : t Conor McBride 1999 thesis.

Sometimes the part of the term in focus is underlined.

 
||| Reflection of the well typed core language
data TT =
        ||| A reference to some name (P for Parameter)
        P NameType TTName TT |
        ||| de Bruijn variables
        V Int |
        ||| Bind a variable
        Bind TTName (Binder TT) TT |
        ||| Apply one term to another
        App TT TT |
        ||| Embed a constant
        TConst Const |
        ||| Erased terms
        Erased |
        ||| The type of types along (with universe constraints)
        TType TTUExp |
        ||| Alternative universes for dealing with uniqueness
UType Universe

TT stores local bound variables using De Bruijn index, when working in Idris this does not concern the user because string names are used for variables. Converting bound variables internally to index values means that the same variable name can be used, in different lambda terms, without ambiguity and without the need for α-substitution.

De Bruijn index which is a integer where:

Expression Notation

The notation assumes right-associativity, in the absence of brackets, the term to the right binds more tightly than the one on the left .

so, for nested lambda terms:

λ a . λ b . f 

means

λ a .( λ b . f)

and the same for function application:

f g x

means

f (g x) 

In contrast, in lambda calculus, function application is usually regarded as left-associative,

Here are some typical examples of the notation used for expressions:

Notation Meaning
? {hole_0} . {hole_0}

The term, to be derived, may start off in this state following something like this:

myScript : Elab ()
myScript= do

The dot '.' tells us this is some sort of binding.

?{hole_0} ≈ ? {hole_2} . {hole_2} . {hole_0}

Here is a slightly more complicated example arising from:

idNat : Nat -> Nat
idNat = %runElab (do

This introduces a guess that hole_0 = hole_2 .

?{hole_0} ≈ λ x . ? {hole_2} . {hole_2} . {hole_0}

Following on from the previous example a lambda function is introduced like this:

intro `{{x}}

So now the expression is wrapped in a lambda binding.

?{hole_0} ≈ λ x . ?{hole_2} ≈ x . {hole_2} . {hole_0}

Following on, we can use the fill tactic like this:

fill (Var `{{x}})

which introduces another guess.

?{hole_0} ≈ λ x . x . {hole_0}
The solve tactic completes the proof

 

Raw

 
data Raw =
         ||| Variables, global or local
         Var TTName |
         ||| Bind a variable
         RBind TTName (Binder Raw) Raw |
         ||| Application
         RApp Raw Raw |
         ||| The type of types
         RType |
         ||| Alternative universes for dealing with uniqueness
         RUType Universe |
         ||| Embed a constant
RConstant Const

 

Elab Tactics

 
||| A reflected elaboration script.
export
data Elab : Type -> Type where
  -- obligatory control stuff
  Prim__PureElab : a -> Elab a
  Prim__BindElab : {a, b : Type} -> Elab a -> (a -> Elab b) -> Elab b

  Prim__Try : {a : Type} -> Elab a -> Elab a -> Elab a
  Prim__TryCatch : {a : Type} -> Elab a -> (Err -> Elab a) -> Elab a
  Prim__Fail : {a : Type} -> 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 : {a : Type} -> List ErrorReportPart -> Elab a
  Prim__Metavar : TTName -> Elab ()

 

Here we look at each tactic in turn to see how they affect the proof state.

Binders

Introduction tactics for binders. The binder types are:

A precondition of these tactics is that the focused hole is of the form:

?h : t.h

that is, that the body of its scope consists directly of a reference to the hole-bound variable. If a hole binder were of the form:

?h : t1 -> t2.f h

and a tactic such as

intro `{{x}}

were applied, the result would be the term

?h : t2 . λ x:t1. f h

However this would cause the application of f to be ill-typed, as it expects an argument of type t1->t2, not an argument of type t2. Additionally, some binding tactics require that t, the type of the hole h, have a specific form, because the binder to be established may have a typing rule associated with it.

intro

intro state transition

Introduce a lambda binding around the current hole and focus on the body. Requires that the hole be in binding form (use 'attack' if it might not be).
@ n the name to use for the argument.

Signature:

intro : (n : TTName) -> Elab ()

Result

λn:t1.?h:[n/x]t2.h
    
intro'

Introduce a lambda binding around the current hole and focus on the body, using the name provided by the type of the hole.
Requires that the hole be immediately under its binder (use 'attack' if it might not be).

Signature:

intro' : Elab ()
forall

Introduce a dependent function type binding into the current hole, and focus on the body.
Requires that the hole be immediately under its binder (use 'attack' if it might not be).

Signature:

forall : TTName -> Raw -> Elab () 
patbind

Introduce a new pattern binding.
Requires that the hole be immediately under its binder (use 'attack' if it might not be).

Signature:

patbind : TTName -> Elab ()
letbind

Introduce a new let binding.
Requires that the hole be immediately under its binder (use 'attack' if it might not be).
@ n the name to let bind
@ ty the type of the term to be let-bound
@ tm the term to be bound

Signature:

letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()

Primitive Operators

gensym

Generate a unique name based on some hint.

Useful when establishing a new binder.
**NB**: the generated name is unique _for this run of the elaborator_. Do not assume that they are globally unique.

Signature:

gensym : (hint : String) -> Elab TTName
solve

Substitute a guess into a hole.

Substitute the focused guess throughout its scope, eliminating it and moving focus to the next element of the hole queue. Fail if the focus is not a guess.

Signature:

solve : Elab ()
fill

Place a term into a hole, unifying its type. Fails if the focus is not a hole.

Signature:

fill : (e : Raw) -> Elab ()

Place a term e with type tc into the focused hole:

?h : th.e'

and convert it to a guess:

?h ≈ e:t.e' 

and fail if the current focus is not a hole. The type t of the guess is constructed by unifying tc and th, which may instantiate holes that they refer to. Fail if the current focus is not a hole or if unification fails. This unification can result in the solution of further holes or the establishment of additional unsolved unification constraints.

apply

Attempt to apply an operator to fill the current hole, potentially solving arguments by unification.

A hole is established for each argument. The return value is the list of holes established for the arguments to the function.

Note that not all of the returned hole names still exist, as they may have been solved.
@ op the term to apply
@ argSpec - A list of booleans, one for each argument that the operator will be applied to. If true then attempt to solve the argument by unification.

Signature:

apply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)

Example: elaborating an application of a function f that takes one implicit and two explicit arguments might invoke:

apply `(f) [False, True, True]

Here is an example of an elab script that uses apply to insert the term plus Z (S Z) into a goal of type Nat.

do [x,y] <- apply `(plus) [False, False] 
solve
focus x; fill `(Z); solve
focus y; fill `(S Z); solve

The names of the established holes are returned.

Note: This was added to the original tactic language to allow elaborator reflection.

matchApply

Attempt to apply an operator to fill the current hole, potentially solving arguments by matching.
The return value is the list of holes established for the arguments to the function.
Note that not all of the returned hole names still exist, as they may have been solved.
@ op the term to apply
@ argSpec instructions for finding the arguments to the term, where the Boolean states whether or not to attempt to solve the argument by matching.

Signature:

matchApply : (op : Raw) -> (argSpec : List Bool) ->
                Elab (List TTName) 
focus

Move the focus to the specified hole, bringing it to the front of the hole queue. Fails if the hole does not exist.
@ hole the hole to focus on

Signature:

focus : (hole : TTName) -> Elab ()
unfocus

Send the currently-focused hole to the end of the hole queue and focus on the next hole.

Signature:

unfocus : TTName -> Elab ()
attack

Convert a hole to make it suitable for bindings - that is, transform it such that it has the form `?h : t . h` as opposed to `?h : t . f h`.
The binding tactics require that a hole be directly under its binding, or else the scopes of the generated terms won't make sense. This tactic creates a new hole of the proper form, and points the old hole at it.

Signature:

attack : Elab () 
claim

Establish a new hole binding named n with type t, surrounding the current focus.

Introduce a new hole with a specified name and type.
The new hole will be focused, and the previously-focused hole will be immediately after it in the hole queue. Because this tactic introduces a new binding, you may need to 'attack' first.

Signature:

claim : TTName -> Raw -> Elab ()
patvar

Convert a hole into a pattern variable.

Signature:

patvar : TTName -> Elab ()
compute

Normalise the goal.

Often this is not necessary because normanisation is applied during other tactics.

Signature:

compute : Elab ()
normalise

Normalise a term in some lexical environment
@ env the environment in which to compute (get one of these from `getEnv`)
@ term the term to normalise

Signature:

normalise : (env : List (TTName, Binder TT)) ->
          (term : TT) -> Elab TT
whnf

Reduce a closed term to weak-head normal form
@ term the term to reduce

Signature:

whnf : (term : TT) -> Elab TT
convertsInEnv

Check that two terms are convertible in the current context and in some environment.
@ env a lexical environment to compare the terms in (see `getEnv`)
@ term1 the first term to convert
@ term2 the second term to convert

Signature:

convertsInEnv : (env : List (TTName, Binder TT)) ->
                              (term1, term2 : TT) -> Elab ()
converts

Check that two terms are convertable in the current context and environment
@ term1 the first term to convert
@ term2 the second term to convert

converts : (term1, term2 : TT) -> Elab ()
  converts term1 term2 = convertsInEnv !getEnv term1 term2
      
getSourceLocation

Find the source context for the elaboration script

Signature:

getSourceLocation : Elab SourceLocation 
sourceLocation

Attempt to solve the current goal with the source code location

sourceLocation : Elab ()
  sourceLocation = do loc <- getSourceLocation
                      fill (quote loc)
                      solve
      
currentNamespace

Get the current namespace at the point of tactic execution. This allows scripts to define top-level names conveniently.
The namespace is represented as a reverse-order list of strings, just as in the representation of names.

Signature:

currentNamespace : Elab (List String)
rewriteWith

Attempt to rewrite the goal using an equality.
The tactic searches the goal for applicable subterms, and constructs a context for `replace` using them. In some cases, this is not possible, and `replace` must be called manually with an appropriate context.
Because this tactic internally introduces a `let` binding, it requires that the hole be immediately under its binder (use 'attack' if it might not be).

Signature:

rewriteWith : Raw -> Elab ()
resolveTC

Attempt to solve the current goal with an interface dictionary
@ fn the name of the definition being elaborated (to prevent Idris from looping)

Signature:

resolveTC : (fn : TTName) -> Elab ()
search

Use Idris's internal proof search.

Signature:

search : Elab ()
search'

Use Idris's internal proof search, with more control.
@ depth the search depth
@ hints additional names to try

Signature:

search' : (depth : Int) -> (hints : List TTName) -> Elab ()
operatorFixity

Look up the declared fixity for an operator.
The lookup fails if the operator does not yet have a fixity or if the string is not a valid operator.
@ operator the operator string to look up

Signature:

operatorFixity : (operator : String) -> Elab Fixity
debug

Halt elaboration, dumping the internal state for inspection.
This is intended for elaboration script developers, not for end-users. Use `fail` for final scripts.

Signature:

debug : Elab a

Only seems to compile if 'debug' is last tactic so comment out following tactics like this:

%language ElabReflection


idNat : Nat -> Nat
idNat = %runElab (do
         intro `{{x}}
         debug
         --    fill (Var `{{x}})
         --    solve
         )
debugMessage

Halt elaboration, dumping the internal state and displaying a message.
This is intended for elaboration script developers, not for end-users. Use `fail` for final scripts.
@ msg the message to display

Signature:

debugMessage : (msg : List ErrorReportPart) -> Elab a 

Only seems to compile if 'debug' is last tactic so comment out following tactics like this:

%language ElabReflection
idNat : Nat -> Nat
idNat = %runElab (do
         intro `{{x}}
         debugMessage [TextPart "error message"]
         --    fill (Var `{{x}})
         --    solve
         )
metavar

Create a new top-level metavariable to solve the current hole.
@ name the name for the top-level variable

Signature:

metavar : (name : TTName) -> Elab ()
runElab

Recursively invoke the reflected elaborator with some goal.
The result is the final term and its type.

Signature:

runElab : Raw -> Elab () -> Elab (TT, TT) 

Read and Write State

getEnv

Look up the lexical binding at the focused hole. Fails if no holes are present.

Signature:

getEnv : Elab (List (TTName, Binder TT))

returns the type: Elab (List (TTName, Binder TT))

getGoal

Get the name and type of the focused hole. Fails if not holes are present.

Signature:

getGoal : Elab (TTName, TT)
getHoles

Get the hole queue, in order.

getHoles : Elab (List TTName)
  getHoles = Prim__Holes
getGuess

If the current hole contains a guess, return it. Otherwise, fail.

getGuess : Elab TT
  getGuess = Prim__Guess
lookupTy

Look up the types of every overloading of a name.

lookupTy :  TTName -> Elab (List (TTName, NameType, TT))
  lookupTy n = Prim__LookupTy n
lookupTyExact

Get the type of a fully-qualified name. Fail if it doesn't resolve uniquely.

lookupTyExact : TTName -> Elab (TTName, NameType, TT)
  lookupTyExact n = case !(lookupTy n) of
          [res] => pure res
          []    => fail [NamePart n, TextPart "is not defined."]
          xs    => fail [NamePart n, TextPart "is ambiguous."]
lookupDatatype

Find the reflected representation of all datatypes whose names are overloadings of some name.

lookupDatatype : TTName -> Elab (List Datatype)
  lookupDatatype n = Prim__LookupDatatype n
lookupDatatypeExact

Find the reflected representation of a datatype, given its fully-qualified name. Fail if the name does not uniquely resolve to a datatype.

lookupDatatypeExact : TTName -> Elab Datatype
  lookupDatatypeExact n = case !(lookupDatatype n) of
        [res] => pure res
        []    => fail [TextPart 
              "No datatype named", NamePart n]
        xs    => fail [TextPart "More than one datatype named",
               NamePart n]
lookupFunDefn

Find the reflected function definition of all functions whose names are overloadings of some name.

lookupFunDefn : TTName -> Elab (List (FunDefn TT))
  lookupFunDefn n = Prim__LookupFunDefn n
lookupFunDefnExact

Find the reflected function definition of a function, given its fully-qualified name. Fail if the name does not uniquely resolve to a function.
export

  lookupFunDefnExact : TTName -> Elab (FunDefn TT)
  lookupFunDefnExact n = case !(lookupFunDefn n) of
         [res] => pure res
         []    => fail [TextPart
               "No function named", NamePart n]
         xs    => fail [TextPart "More than one function named",
               NamePart n]
lookupArgs

Get the argument specification for each overloading of a name.

lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
  lookupArgs n = Prim__LookupArgs n
lookupArgsExact

Get the argument specification for a name. Fail if the name does not uniquely resolve.

lookupArgsExact : TTName -> Elab (TTName, List FunArg, Raw)
  lookupArgsExact n = case !(lookupArgs n) of
          [res] => pure res
          []    => fail [NamePart n, TextPart "is not defined."]
          xs    => fail [NamePart n, TextPart "is ambiguous."]
check

Attempt to type-check a term, getting back itself and its type.
@ env the environment within which to check the type
@ tm the term to check

check : (env : List (TTName, Binder TT)) ->
          (tm : Raw) -> Elab (TT, TT)
  check env tm = Prim__Check env tm
      

Error Handling

tryCatch

`tryCatch t (\err => t')` will run `t`, and if it fails, roll back the elaboration state and run `t'`, but with access to the knowledge of why `t` failed.

Signature:

tryCatch : Elab a -> (Err -> Elab a) -> Elab a

Fixme - following does not work.

%language ElabReflection

id1 : Elab ()
id1 = do
          tryCatch (intro `{{x}}) 
             (\err -> (intro `{{x}}))
          fill (Var `{{x}})
          solve

idNat : Nat -> Nat
idNat = %runElab id1
fail

Halt elaboration with an error

Signature:

fail : List ErrorReportPart -> Elab a

Return type is given by last term so fail cant be at the the last term, we would expect fail to be in some sort of conditional statement:

%language ElabReflection

id1 : Elab ()
id1 = do
  intro `{{x}}
  fill (Var `{{x}})
  if True
    then
      fail [TextPart "error message"]
    else
      solve

idNat : Nat -> Nat
idNat = %runElab id1

Generating Data and Functions at Compile Time

We can construct a data structure at compile-time in an Elab monad.

This can allow proofs to be generated for user defined types or it could allow types to be automatically generated to support user defined types.

An example is the code, from Christensen-Brady joint paper ('Elaborator Reflection: Extending Idris in Idris'), that automatically generates accessibility predicates using the Bove-Capretta method.

The following simple outline example is adapted from https://github.com/idris-lang/Idris-dev/blob/master/test/meta002/DataDef.idr

module DataDef
%language ElabReflection

addData : Elab ()
addData = do
    let dataname : TTName = `{{DataDef.N}}
    declareDatatype $ Declare dataname [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)
    defineDatatype $ DefineDatatype dataname [
        Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased]
            (RApp (Var `{{DataDef.N}}) (Var `{{x}})),
        Constructor `{{MkN'}} [MkFunArg `{{x}} `(Nat) Explicit NotErased]
            (RApp (Var `{{DataDef.N}}) (RApp (Var `{S}) (Var `{{x}})))
    ]

%runElab addData

So this declares and defines the following data structure 'N' with a constructor 'MkN' which can have an implicit or an explicit Nat argument.

data N : Nat -> Type where
  MkN : N x
  MkN' : (x : Nat) -> N (S x)
λΠ> :t N
N : Nat -> Type
λΠ> N 2
N 2 : Type
λΠ> N 0
N 0 : Type
λΠ> :t MkN
MkN : N x

Here is another, more complicated, example from the same test file. This also creates a function.

module DataDef
%language ElabReflection

mkU : Elab ()
mkU = do
  let U = `{{DataDef.U}}
  let el = `{{DataDef.el}}
  declareDatatype $ Declare U [] `(Type)
  declareType $ Declare el [MkFunArg `{{code}} (Var U) Explicit NotErased] `(Type)
  defineDatatype $ DefineDatatype U [
      Constructor `{{Base}} [] (Var U),
      Constructor `{{Pi}}
        [MkFunArg `{{code}} (Var U) Explicit NotErased,
          MkFunArg `{{body}} `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)) Explicit NotErased]
        (Var U)
    ]
  defineFunction $ DefineFun el [
     MkFunClause (RBind `{{code}} (PVar (Var U))
         (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))
           (RApp (Var el)
             (RApp (RApp (Var `{{DataDef.Pi}})
                  (Var `{{code}}))
                (Var `{{body}})))))
      (RBind `{{code}} (PVar (Var U))
        (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))
          (RBind `{{x}} (Pi (RApp (Var el) (Var `{{code}})) `(Type))
            (RApp (Var el) (RApp (Var `{{body}}) (Var `{{x}})))))),
    MkFunClause (RApp (Var el) (Var `{{DataDef.Base}})) `(Bool)
  ]

%runElab mkU

This code generates the following data and function

data U : Type where
  Base : U
  Pi : (code : U) -> (el code -> U) -> U
el : U -> Type
el (Pi code body) = (x : el code) -> el (body x)
el Base = Bool
λΠ> :t U
U : Type
λΠ> :doc U
No documentation for U
λΠ> Base
Base : U
λΠ> DataDef.Pi
Pi : (code : U) -> (el code -> U) -> U
λΠ> 
 
λΠ> :t el
el : U -> Type
λΠ> el Base
Bool : Type

So these are the functions that we can use to create data and functions in the Elab monad:

declareType

Add a type declaration to the global context.

Signature:

declareType : TyDecl -> Elab () 
defineFunction

Define a function in the global context. The function must have already been declared, either in ordinary Idris code or using `declareType`.

Signature:

defineFunction : FunDefn Raw -> Elab ()
declareDatatype

Declare a datatype in the global context. This step only establishes the type constructor; use `defineDatatype` to give it constructors.

Signature:

declareDatatype : TyDecl -> Elab ()
defineDatatype
  

Signature:

 defineDatatype : DataDefn -> Elab ()
addImplementation

Register a new implementation for interface resolution.
@ ifaceName the name of the interface for which an implementation is being registered
@ implName the name of the definition to use in implementation search

Signature:

addImplementation : (ifaceName, implName : TTName) -> Elab () 
isTCName

Determine whether a name denotes an interface.
@ name a name that might denote an interface.

Signature:

isTCName : (name : TTName) -> Elab Bool 

The above functions use the following data/records:

Plicity

How an argument is provided in high-level Idris

data  Plicity=
  ||| The argument is directly provided at the application site
  Explicit |
  ||| The argument is found by Idris at the application site
  Implicit |
  ||| The argument is solved using interface resolution
  Constraint

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.

record FunArg where
  constructor MkFunArg
  name    : TTName
  type    : Raw
  plicity : Plicity
erasure : Erasure

TyConArg

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.

data TyConArg =
  ||| Parameters are uniform across the constructors
  TyConParameter FunArg |
  ||| Indices are not uniform
TyConIndex FunArg

TyDecl

A type declaration for a function or datatype

record TyDecl where
  constructor Declare

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

  ||| Each argument is in the scope of the names of previous arguments.
  arguments : List FunArg

  ||| The return type is in the scope of all the argument names.
  returnType : Raw

FunClause

A single pattern-matching clause

data FunClause : Type -> Type where
  MkFunClause : (lhs, rhs : a) -> FunClause a
  MkImpossibleClause : (lhs : a) -> FunClause a

FunDefn

A reflected function definition.

record FunDefn a where
  constructor DefineFun
  name : TTName
clauses : List (FunClause a)

ConstructorDefn

A constructor to be associated with a new datatype.

record ConstructorDefn where
  constructor Constructor

  ||| The name of the constructor. The name must _not_ be qualified -
  ||| that is, it should begin with the `UN` or `MN` constructors.
  name : TTName

  ||| The constructor arguments. Idris will infer which arguments are
  ||| datatype parameters.
  arguments : List FunArg

  ||| The specific type constructed by the constructor.
returnType : Raw

DataDefn

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

record DataDefn where
  constructor DefineDatatype
  ||| The name of the datatype being defined. It must be
  ||| fully-qualified, and it must have been previously declared as a
  ||| datatype.
name : TTName
CtorArg
data CtorArg = CtorParameter FunArg | CtorField FunArg

Datatype

A reflected datatype definition

record Datatype where
  constructor MkDatatype

  ||| The name of the type constructor
  name : TTName

  ||| The arguments to the type constructor
  tyConArgs : List TyConArg

  ||| The result of the type constructor
  tyConRes : Raw

  ||| The constructors for the family
constructors : List (TTName, List CtorArg, Raw)

 

 


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.