Language.Reflection

Reexports

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

Definitions

data LookupDir : Type

Totality: total
Visibility: public export
Constructors:

ProjectDir : LookupDir

  The dir of the `ipkg`-file, or the current dir if there is no one

SourceDir : LookupDir

  The source dir set in the `ipkg`-file, or the current dir if there is no one

CurrentModuleDir : LookupDir

  The dir where the current module is located
  
  For the module `Language.Reflection` it would be `<source_dir>/Language/`

SubmodulesDir : LookupDir

  The dir where submodules of the current module are located
  
  For the module `Language.Reflection` it would be `<source_dir>/Language/Reflection/`

BuildDir : LookupDir

  The dir where built files are located, set in the `ipkg`-file and defaulted to `build`

data Elab : Type -> Type

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

Totality: total
Visibility: export
Constructors:

Pure : a -> Elab a

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

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

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

Fail : FC -> String -> Elab a

Warn : FC -> String -> Elab ()

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

ResugarTerm : Maybe Nat -> TTImp -> Elab String

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))

GetVis : Name -> Elab (List (Name, Visibility))

GetLocalType : Name -> Elab TTImp

GetCons : Name -> Elab (List Name)

GetReferredFns : Name -> Elab (List Name)

GetCurrentFn : Elab (SnocList Name)

Declare : List Decl -> Elab ()

ReadFile : LookupDir -> String -> Elab (Maybe String)

WriteFile : LookupDir -> String -> String -> Elab ()

IdrisDir : LookupDir -> Elab String

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

warnAt : FC -> String -> m ()

  Report a warning 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

resugarTerm : Maybe Nat -> TTImp -> m String

  Resugar given term to a pretty string

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 names and their types

getVis : Name -> m (List (Name, Visibility))

  Get the visibility associated with a name. Returns all matching names and their visibilities

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

getReferredFns : Name -> m (List Name)

  Get all the name of function definitions that a given definition refers to (transitively)

getCurrentFn : m (SnocList Name)

  Get the name of the current and outer functions, if we are in a function

declare : List Decl -> m ()

  Make some top level declarations

readFile : LookupDir -> String -> m (Maybe String)

  Read the contents of a file, if it is present

writeFile : LookupDir -> String -> String -> m ()

  Writes to a file, replacing existing contents, if were present

idrisDir : LookupDir -> m String

  Returns the specified type of dir related to the current idris project

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