Language.Reflection

Reexports

import public Language.Reflection.TT
import public Language.Reflection.TTImp
import public Control.Monad.Trans

Definitions

data Elab : Type -> Type

  Elaboration scripts
  Where types/terms are returned, binders will have unique, if not
  necessarily human readabe, names

Totality: total
Visibility: export
Constructors:

Pure : a -> Elab a

Bind : Elab a -> (a -> Elab b) -> Elab b

Fail : FC -> String -> Elab a

Try : Elab a -> Elab a -> Elab a

LogMsg : String -> Nat -> String -> Elab ()

  Log a message. Takes a
  * topic
  * level
  * message

LogTerm : String -> Nat -> String -> TTImp -> Elab ()

  Print and log a term. Takes a
  * topic
  * level
  * message
  * term

LogSugaredTerm : String -> Nat -> String -> TTImp -> Elab ()

  Resugar, print and log a term. Takes a
  * topic
  * level
  * message
  * term

Check : TTImp -> Elab expected

Quote : (0 _ : val) -> Elab TTImp

Lambda : (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> ty val)

Goal : Elab (Maybe TTImp)

LocalVars : Elab (List Name)

GenSym : String -> Elab Name

InCurrentNS : Name -> Elab Name

GetType : Name -> Elab (List (Name, TTImp))

GetInfo : Name -> Elab (List (Name, NameInfo))

GetLocalType : Name -> Elab TTImp

GetCons : Name -> Elab (List Name)

Declare : List Decl -> Elab ()

Hints:

Alternative Elab
Applicative Elab
Elaboration Elab
Functor Elab
Monad Elab

interface Elaboration : (Type -> Type) -> Type

Parameters: m
Constraints: Monad m
Methods:

failAt : FC -> String -> m a

  Report an error in elaboration at some location

try : Elab a -> Elab a -> m a

  Try the first elaborator. If it fails, reset the elaborator state and
  run the second

logMsg : String -> Nat -> String -> m ()

  Write a log message, if the log level is >= the given level

logTerm : String -> Nat -> String -> TTImp -> m ()

  Write a log message and a rendered term, if the log level is >= the given level

logSugaredTerm : String -> Nat -> String -> TTImp -> m ()

  Write a log message and a resugared & rendered term, if the log level is >= the given level

check : TTImp -> m expected

  Check that some TTImp syntax has the expected type
  Returns the type checked value

quote : (0 _ : val) -> m TTImp

  Return TTImp syntax of a given value

lambda : (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (ty val)) -> m ((val : x) -> ty val)

  Build a lambda expression

goal : m (Maybe TTImp)

  Get the goal type of the current elaboration
  
  `Nothing` means the script is run in the top-level `%runElab` clause.
  If elaboration script is run in expression mode, this function will always return `Just`.
  In the case of unknown result type in the expression mode, returned `TTImp` would be an `IHole`.

localVars : m (List Name)

  Get the names of the local variables in scope

genSym : String -> m Name

  Generate a new unique name

inCurrentNS : Name -> m Name

  Given a name, return the name decorated with the current namespace

getType : Name -> m (List (Name, TTImp))

  Given a possibly ambiguous name, get all the matching names and their types

getInfo : Name -> m (List (Name, NameInfo))

  Get the metadata associated with a name. Returns all matching namea and their types

getLocalType : Name -> m TTImp

  Get the type of a local variable

getCons : Name -> m (List Name)

  Get the constructors of a fully qualified data type name

declare : List Decl -> m ()

  Make some top level declarations

Implementations:

Elaboration Elab
Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m)

failAt : Elaboration m => FC -> String -> m a

  Report an error in elaboration at some location