mathlib3 documentation

core / init.meta.vm

meta constant vm_obj  :
@[protected, instance]
inductive vm_obj_kind  :
Instances for vm_obj_kind
meta constant vm_obj.cidx  :

For simple and constructor vm_obj's, it returns the constructor tag/index. Return 0 otherwise.

meta constant vm_obj.fn_idx  :

For closure vm_obj's, it returns the internal function index.

meta constant vm_obj.fields  :

For constructor vm_obj's, it returns the data stored in the object. For closure vm_obj's, it returns the local arguments captured by the closure.

meta constant vm_obj.to_nat  :

For simple and mpz vm_obj's

meta constant vm_obj.to_name  :

For name vm_obj's, it returns the name wrapped by the vm_obj.

meta constant vm_obj.to_level  :

For level vm_obj's, it returns the universe level wrapped by the vm_obj.

meta constant vm_obj.to_expr  :

For expr vm_obj's, it returns the expression wrapped by the vm_obj.

For declaration vm_obj's, it returns the declaration wrapped by the vm_obj.

For environment vm_obj's, it returns the environment wrapped by the vm_obj.

For tactic_state vm_obj's, it returns the tactic_state object wrapped by the vm_obj.

meta constant vm_obj.to_format  :

For format vm_obj's, it returns the format object wrapped by the vm_obj.

meta constant vm_decl  :
inductive vm_decl_kind  :
Instances for vm_decl_kind
meta structure vm_local_info  :

Information for local variables and arguments on the VM stack. Remark: type is only available if it is a closed term at compilation time.

meta constant vm_decl.to_name  :
meta constant vm_decl.idx  :

Internal function index associated with the given VM declaration.

meta constant vm_decl.arity  :

Number of arguments needed to execute the given VM declaration.

meta constant vm_decl.pos  :

Return source position if available

meta constant vm_decl.olean  :

Return .olean file where the given VM declaration was imported from.

Return names .olean file where the given VM declaration was imported from.

If the given declaration is overridden by another declaration using the vm_override attribute, then this returns the overriding declaration.

meta constant vm_core  :
Instances for vm_core
meta constant vm_core.map {α β : Type} :
β) vm_core α vm_core β
meta constant vm_core.ret {α : Type} :
α vm_core α
meta constant vm_core.bind {α β : Type} :
@[protected, instance]
meta def vm_core.monad  :
@[reducible]
meta def vm (α : Type) :
meta constant vm.get_env  :
meta constant vm.get_decl  :

Returns the vm declaration associated with the given name. Remark: does not return the vm_override if present.

meta constant vm.decl_of_idx  :

Returns the vm declaration associated with the given index. Remark: does not return the vm_override if present.

meta constant vm.get_options  :
meta constant vm.stack_size  :
meta constant vm.stack_obj  :

Return the vm_obj stored at the given position on the execution stack. It fails if position >= vm.stack_size

meta constant vm.stack_obj_info  :

Return (name, type) for the object at the given position on the execution stack. It fails if position >= vm.stack_size. The name is anonymous if vm_obj is a transient value created by the compiler. Type information is only recorded if the type is a closed term at compilation time.

meta constant vm.pp_stack_obj  :

Pretty print the vm_obj at the given position on the execution stack.

meta constant vm.pp_expr  :

Pretty print the given expression.

meta constant vm.call_stack_size  :

Number of frames on the call stack.

meta constant vm.call_stack_fn  :

Return the function name at the given stack frame. Action fails if position >= vm.call_stack_size.

meta constant vm.call_stack_var_range  :

Return the range [start, end) for the given stack frame. Action fails if position >= vm.call_stack_size. The values start and end correspond to positions at the execution stack. We have that 0 <= start < end <= vm.stack_size

meta constant vm.curr_fn  :

Return the name of the function on top of the call stack.

meta constant vm.bp  :

Return the base stack pointer for the frame on top of the call stack.

meta constant vm.pc  :

Return the program counter.

meta constant vm.obj_to_string  :

Convert the given vm_obj into a string

meta constant vm.put_str  :
meta constant vm.get_line  :
meta constant vm.eof  :

Return tt if end of the input stream has been reached. For example, this can happen if the user presses Ctrl-D

meta constant vm.get_attribute  :

Return the list of declarations tagged with the given attribute.

meta def vm.trace {α : Type} [has_to_format α] (a : α) :
meta structure vm_monitor (α : Type) :
  • init : α
  • step : α vm α

A Lean VM monitor. Monitors are registered using the [vm_monitor] attribute.

If option 'debugger' is true, then the VM will initialize the vm_monitor state using the 'init' field, and will invoke the function 'step' before each instruction is invoked.