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
Totality: total
Visibility: public exporttry : Elaboration m => Elab a -> Elab a -> m a
Try the first elaborator. If it fails, reset the elaborator state and
run the second
Totality: total
Visibility: public exportlogMsg : Elaboration m => String -> Nat -> String -> m ()
Write a log message, if the log level is >= the given level
Totality: total
Visibility: public exportlogTerm : Elaboration m => String -> Nat -> String -> TTImp -> m ()
Write a log message and a rendered term, if the log level is >= the given level
Totality: total
Visibility: public exportlogSugaredTerm : Elaboration m => String -> Nat -> String -> TTImp -> m ()
Write a log message and a resugared & rendered term, if the log level is >= the given level
Totality: total
Visibility: public exportcheck : Elaboration m => TTImp -> m expected
Check that some TTImp syntax has the expected type
Returns the type checked value
Totality: total
Visibility: public exportquote : Elaboration m => (0 _ : val) -> m TTImp
Return TTImp syntax of a given value
Totality: total
Visibility: public exportlambda : Elaboration m => (0 x : Type) -> {0 ty : x -> Type} -> ((val : x) -> Elab (ty val)) -> m ((val : x) -> ty val)
Build a lambda expression
Totality: total
Visibility: public exportgoal : Elaboration m => 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`.
Totality: total
Visibility: public exportlocalVars : Elaboration m => m (List Name)
Get the names of the local variables in scope
Totality: total
Visibility: public exportgenSym : Elaboration m => String -> m Name
Generate a new unique name
Totality: total
Visibility: public exportinCurrentNS : Elaboration m => Name -> m Name
Given a name, return the name decorated with the current namespace
Totality: total
Visibility: public exportgetType : Elaboration m => Name -> m (List (Name, TTImp))
Given a possibly ambiguous name, get all the matching names and their types
Totality: total
Visibility: public exportgetInfo : Elaboration m => Name -> m (List (Name, NameInfo))
Get the metadata associated with a name. Returns all matching namea and their types
Totality: total
Visibility: public exportgetLocalType : Elaboration m => Name -> m TTImp
Get the type of a local variable
Totality: total
Visibility: public exportgetCons : Elaboration m => Name -> m (List Name)
Get the constructors of a fully qualified data type name
Totality: total
Visibility: public exportdeclare : Elaboration m => List Decl -> m ()
Make some top level declarations
Totality: total
Visibility: public exportfail : Elaboration m => String -> m a
Report an error in elaboration
Totality: total
Visibility: exportlogGoal : Elaboration m => String -> Nat -> String -> m ()
Log the current goal type, if the log level is >= the given level
Totality: total
Visibility: exportcatch : Elaboration m => Elab a -> m (Maybe a)
Catch failures and use the `Maybe` monad instead
Totality: total
Visibility: exportsearch : Elaboration m => (ty : Type) -> m (Maybe ty)
Run proof search to attempt to find a value of the input type.
Useful to check whether a give interface constraint is satisfied.
Totality: total
Visibility: export