mathlib documentation

core.init.meta.vm

meta constant vm_obj :

Type

@[instance]

def vm_obj_kind.decidable_eq :

decidable_eq vm_obj_kind

inductive vm_obj_kind :

Type

simple : vm_obj_kind
constructor : vm_obj_kind
closure : vm_obj_kind
native_closure : vm_obj_kind
mpz : vm_obj_kind
name : vm_obj_kind
level : vm_obj_kind
expr : vm_obj_kind
declaration : vm_obj_kind
environment : vm_obj_kind
tactic_state : vm_obj_kind
format : vm_obj_kind
options : vm_obj_kind
other : vm_obj_kind

meta constant vm_obj.kind (a : vm_obj) :

meta constant vm_obj.cidx (a : vm_obj) :

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

meta constant vm_obj.fn_idx (a : vm_obj) :

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

meta constant vm_obj.fields (a : vm_obj) :

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 (a : vm_obj) :

For simple and mpz vm_obj's

meta constant vm_obj.to_name (a : vm_obj) :

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

meta constant vm_obj.to_level (a : vm_obj) :

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

meta constant vm_obj.to_expr (a : vm_obj) :

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

meta constant vm_obj.to_declaration (a : vm_obj) :

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

meta constant vm_obj.to_environment (a : vm_obj) :

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

meta constant vm_obj.to_tactic_state (a : 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 (a : vm_obj) :

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

bytecode : vm_decl_kind
builtin : vm_decl_kind
cfun : vm_decl_kind

meta structure vm_local_info :

Type

id : name
type : option expr

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 (a : vm_decl) :

meta constant vm_decl.to_name (a : vm_decl) :

meta constant vm_decl.idx (a : vm_decl) :

Internal function index associated with the given VM declaration.

meta constant vm_decl.arity (a : vm_decl) :

Number of arguments needed to execute the given VM declaration.

meta constant vm_decl.pos (a : vm_decl) :

Return source position if available

meta constant vm_decl.olean (a : vm_decl) :

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

meta constant vm_decl.args_info (a : vm_decl) :

list vm_local_info

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

meta constant vm_decl.override_idx (a : vm_decl) :

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

meta constant vm_core (a : Type) :

Type

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

meta constant vm_core.ret {α : Type} (a : α) :

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

@[instance]

meta def vm_core.monad :

meta def vm (α : Type) :

Type

meta constant vm.get_env :

meta constant vm.get_decl (a : name) :

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

meta constant vm.decl_of_idx (a : ℕ) :

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

meta def vm.get_override (a : vm_decl) :

meta constant vm.get_options :

meta constant vm.stack_size :

meta constant vm.stack_obj (a : ℕ) :

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 (a : ℕ) :

vm (name × option expr)

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 (a : ℕ) :

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

meta constant vm.pp_expr (a : 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 (a : ℕ) :

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

meta constant vm.call_stack_var_range (a : ℕ) :

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 (a : vm_obj) :

Convert the given vm_obj into a string

meta constant vm.put_str (a : string) :

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 (a : name) :

Return the list of declarations tagged with the given attribute.

meta def vm.trace {α : Type} [has_to_format α] (a : α) :

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.