mathlib documentation

core / init.meta.vm

meta constant vm_obj :

Type

@[protected, 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 :

vm_obj → 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 :

vm_obj → list 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 :

For simple and mpz vm_obj's

meta constant vm_obj.to_name :

vm_obj → name

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

meta constant vm_obj.to_level :

vm_obj → level

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

meta constant vm_obj.to_expr :

vm_obj → expr

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

meta constant vm_obj.to_declaration :

vm_obj → declaration

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

meta constant vm_obj.to_environment :

vm_obj → environment

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

meta constant vm_obj.to_tactic_state :

vm_obj → tactic_state

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

meta constant vm_obj.to_format :

vm_obj → 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

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 :

vm_decl → vm_decl_kind

meta constant vm_decl.to_name :

vm_decl → name

meta constant vm_decl.idx :

vm_decl → ℕ

Internal function index associated with the given VM declaration.

meta constant vm_decl.arity :

vm_decl → ℕ

Number of arguments needed to execute the given VM declaration.

meta constant vm_decl.pos :

vm_decl → option pos

Return source position if available

meta constant vm_decl.olean :

vm_decl → option string

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

meta constant vm_decl.args_info :

vm_decl → list vm_local_info

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

meta constant vm_decl.override_idx :

vm_decl → option ℕ

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 β

@[protected, instance]

meta def vm_core.monad :

meta def vm (α : Type) :

Type

meta constant vm.get_env :

meta constant vm.get_decl :

name → vm vm_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 :

ℕ → vm vm_decl

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

meta def vm.get_override :

vm_decl → vm vm_decl

meta constant vm.get_options :

meta constant vm.stack_size :

meta constant vm.stack_obj :

ℕ → vm vm_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 :

ℕ → 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 :

ℕ → vm format

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

meta constant vm.pp_expr :

expr → vm format

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 :

vm_obj → vm string

Convert the given vm_obj into a string

meta constant vm.put_str :

string → vm unit

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 :

name → vm (list 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.