mathlib documentation

core.​init.​meta.​vm

core.​init.​meta.​vm

meta constant vm_obj  :
Type

inductive vm_obj_kind  :
Type

meta constant 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  :
Type

inductive vm_decl_kind  :
Type

meta structure vm_local_info  :
Type

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.​kind  :

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.

meta constant vm_decl.​override_idx  :

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

meta constant vm_core  :
Type → Type

meta constant vm_core.​map {α β : Type} :
(α → β)vm_core αvm_core β

meta constant vm_core.​ret {α : Type} :
α → vm_core α

meta constant vm_core.​bind {α β : Type} :
vm_core α(α → vm_core β)vm_core β

@[instance]

meta def vm  :
Type → 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  :
vm name

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

meta constant vm.​call_stack_var_range  :
vm ( × )

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 α] :
α → vm unit

meta structure vm_monitor  :
Type → 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.