max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(*): remove more stuff

Browse source
This commit is contained in:
Leonardo de Moura 2018-08-23 15:55:06 -07:00
parent 17ae59b5b0
commit d334bb1fa7
43 changed files with 19 additions and 2113 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
library/init/meta/declaration.lean
View file

@ -1,21 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.lean.declaration
export lean (constant_info reducibility_hints)
namespace lean
namespace constant_info
/-- Instantiate a universe polymorphic declaration type with the given universes. -/
meta constant instantiate_type_univ_params : constant_info → list level → option expr
/-- Instantiate a universe polymorphic declaration value with the given universes. -/
meta constant instantiate_value_univ_params : constant_info → list level → option expr
end constant_info
end lean

2
library/init/meta/default.lean
View file

@ -5,4 +5,4 @@ Authors: Leonardo de Moura
-/
prelude
import init.meta.name init.meta.options init.meta.format
import init.meta.level init.meta.expr init.meta.tactic
import init.meta.tactic

53
library/init/meta/exceptional.lean
View file

@ -1,53 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.control.monad init.meta.format init.util
/-
Remark: we use a function that produces a format object as the exception information.
Motivation: the formatting object may be big, and we may create it on demand.
-/
meta inductive exceptional (α : Type)
| success : α → exceptional
| exception : (options → format) → exceptional
section
open exceptional
variables {α : Type}
variables [has_to_string α]
protected meta def exceptional.to_string : exceptional α → string
| (success a) := to_string a
| (exception .(α) e) := "Exception: " ++ to_string (e options.mk)
meta instance : has_to_string (exceptional α) :=
has_to_string.mk exceptional.to_string
end
namespace exceptional
variables {α β : Type}
protected meta def to_bool : exceptional α → bool
| (success _) := tt
| (exception .(α) _) := ff
protected meta def to_option : exceptional α → option α
| (success a) := some a
| (exception .(α) _) := none
@[inline] protected meta def bind (e₁ : exceptional α) (e₂ : α → exceptional β) : exceptional β :=
exceptional.cases_on e₁
(λ a, e₂ a)
(λ f, exception β f)
@[inline] protected meta def return (a : α) : exceptional α :=
success a
@[inline] meta def fail (f : format) : exceptional α :=
exception α (λ u, f)
end exceptional
meta instance : monad exceptional :=
{pure := @exceptional.return, bind := @exceptional.bind}

162
library/init/meta/expr.lean
View file

@ -1,162 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.level init.control.monad init.lean.expr init.meta.format
universes u v
-- TODO(Leo): move this stuff to a different place
structure pos :=
(line : nat)
(column : nat)
instance : decidable_eq pos
| ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ := if h₁ : l₁ = l₂ then
if h₂ : c₁ = c₂ then is_true (eq.rec_on h₁ (eq.rec_on h₂ rfl))
else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₂ h₂))
else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₁ h₁))
meta instance : has_to_format pos :=
⟨λ ⟨l, c⟩, "⟨" ++ l ++ ", " ++ c ++ "⟩"⟩
export lean (expr binder_info kvmap expr.bvar expr.fvar expr.sort expr.const expr.mvar expr.app expr.lam expr.pi expr.elet expr.lit expr.mdata expr.proj expr.quote)
def expr.mk_bvar (n : nat) : expr :=
expr.bvar n
/-- Compares expressions, including binder names. -/
meta constant lean.expr.has_decidable_eq : decidable_eq expr
attribute [instance] lean.expr.has_decidable_eq
/-- Compares expressions while ignoring binder names. -/
meta constant lean.expr.alpha_eqv : expr → expr → bool
notation a ` =ₐ `:50 b:50 := lean.expr.alpha_eqv a b = bool.tt
protected meta constant lean.expr.to_string : expr → string
meta instance : has_to_string (expr) := ⟨lean.expr.to_string⟩
meta instance : has_to_format (expr) := ⟨λ e, e.to_string⟩
/- Coercion for letting users write (f a) instead of (expr.app f a) -/
meta instance : has_coe_to_fun (expr) :=
{ F := λ e, expr → expr, coe := λ e, expr.app e }
meta constant lean.expr.hash : expr → nat
/-- Compares expressions, ignoring binder names, and sorting by hash. -/
meta constant lean.expr.lt : expr → expr → bool
/-- Compares expressions, ignoring binder names. -/
meta constant lean.expr.lex_lt : expr → expr → bool
meta constant lean.expr.fold {α : Type} : expr → α → (expr → nat → α → α) → α
/-- `has_var e` returns true iff e has free variables. -/
meta constant lean.expr.has_bvar_idx : expr → nat → bool
/-- (reflected a) is a special opaque container for a closed `expr` representing `a`.
It can only be obtained via type class inference, which will use the representation
of `a` in the calling context. Local constants in the representation are replaced
by nested inference of `reflected` instances.
The quotation expression `(a) (outside of patterns) is equivalent to `reflect a`
and thus can be used as an explicit way of inferring an instance of `reflected a`. -/
@[class] meta def reflected {α : Sort u} : α → Type :=
λ _, expr
@[inline] meta def reflected.to_expr {α : Sort u} {a : α} : reflected a → expr :=
id
@[instance] protected meta constant lean.expr.reflect (e : expr) : reflected e
@[instance] protected meta constant string.reflect (s : string) : reflected s
protected meta constant lean.expr.subst : expr → expr → expr
@[inline] meta def reflected.subst {α : Sort v} {β : α → Sort u} {f : Π a : α, β a} {a : α} :
reflected f → reflected a → reflected (f a) :=
λ ef ea, match ef with
| (expr.lam _ _ _ _) := (lean.expr.subst ef ea)
| _ := expr.app ef ea
attribute [irreducible] reflected reflected.subst reflected.to_expr
@[inline] meta instance {α : Sort u} (a : α) : has_coe (reflected a) expr :=
⟨reflected.to_expr⟩
protected meta def reflect {α : Sort u} (a : α) [h : reflected a] : reflected a := h
meta instance {α} (a : α) : has_to_format (reflected a) :=
⟨λ h, to_fmt h.to_expr⟩
namespace lean.expr
open decidable
def app_fn : expr → expr
| (app f a) := f
| a := a
def app_arg : expr → expr
| (app f a) := a
| a := a
def get_app_fn : expr → expr
| (app f a) := get_app_fn f
| a := a
def get_app_num_args : expr → nat
| (app f a) := get_app_num_args f + 1
| e := 0
def get_app_args_aux : list expr → expr → list expr
| r (app f a) := get_app_args_aux (a::r) f
| r e := r
def get_app_args : expr → list expr :=
get_app_args_aux []
def mk_app : expr → list expr → expr
| e [] := e
| e (x::xs) := mk_app (lean.expr.app e x) xs
def const_name : expr → name
| (const n ls) := n
| e := name.anonymous
def is_constant : expr → bool
| (const n ls) := tt
| e := ff
def is_fvar : expr → bool
| (fvar n) := tt
| e := ff
def fvar_id : expr → name
| (fvar n) := n
| e := name.anonymous
def is_constant_of : expr → name → bool
| (const n₁ ls) n₂ := n₁ = n₂
| e n := ff
def is_app_of (e : expr) (n : name) : bool :=
is_constant_of (get_app_fn e) n
def is_napp_of (e : expr) (c : name) (n : nat) : bool :=
is_app_of e c ∧ get_app_num_args e = n
def is_eq : expr → option (expr × expr)
| `((%%a : %%_) = %%b) := some (a, b)
| _ := none
def is_pi : expr → bool
| (pi _ _ _ _) := tt
| e := ff
def is_let : expr → bool
| (elet _ _ _ _) := tt
| e := ff
open format
end lean.expr

58
library/init/meta/has_reflect.lean
View file

@ -1,58 +0,0 @@
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
prelude
import init.meta.expr init.util init.meta.pexpr
@[reducible] meta def {u} has_reflect (α : Sort u) := Π a : α, reflected a
section
local attribute [semireducible] reflected uint32 uint64
meta instance nat.reflect : has_reflect ℕ
| n := if n = 0 then `(0 : ℕ)
else if n = 1 then `(1 : ℕ)
else if n % 2 = 0 then `(bit0 %%(nat.reflect (n / 2)) : ℕ)
else `(bit1 %%(nat.reflect (n / 2)) : ℕ)
meta instance uint32.reflect : has_reflect uint32
| ⟨n, pr⟩ := `(uint32.of_nat n)
meta instance uint64.reflect : has_reflect uint64
| ⟨n, pr⟩ := `(uint64.of_nat n)
end
/- Instances that [derive] depends on. All other basic instances are defined at the end of
derive.lean. -/
meta instance name.reflect : has_reflect name
| name.anonymous := `(name.anonymous)
| (name.mk_string n s) := `(λ n, name.mk_string n s).subst (name.reflect n)
| (name.mk_numeral n i) := `(λ n, name.mk_numeral n i).subst (name.reflect n)
meta instance list.reflect {α : Type} [has_reflect α] [reflected α] : has_reflect (list α)
| [] := `([])
| (h::t) := `(λ t, h :: t).subst (list.reflect t)
meta instance punit.reflect : has_reflect punit
| () := `(_)
meta instance bool.reflect : has_reflect bool
| tt := `(_)
| ff := `(_)
meta instance prod.reflect {α β : Type} [has_reflect α] [has_reflect β] [reflected α] [reflected β] : has_reflect (α × β)
| (a, b) := `(_)
meta instance sum.reflect {α β : Type} [has_reflect α] [has_reflect β] [reflected α] [reflected β] : has_reflect (sum α β)
| (sum.inl a) := `(_)
| (sum.inr b) := `(_)
meta instance option.reflect {α : Type} [has_reflect α] [reflected α] : has_reflect (option α)
| none := `(_)
| (some a) := `(_)
meta instance pos.reflect : has_reflect pos
| {line := l, column := c} := `(_)

8
library/init/meta/interaction_monad.lean
View file

@ -6,8 +6,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
prelude
import init.function init.data.option.basic init.util
import init.control.combinators init.control.monad init.control.alternative init.control.monad_fail
import init.data.nat.div init.meta.exceptional init.meta.format
import init.meta.pexpr init.data.repr init.data.string.basic init.data.to_string
import init.data.nat.div init.meta.format
import init.data.repr init.data.string.basic init.data.to_string init.meta.pos
universes u v
@ -70,11 +70,11 @@ interaction_monad_bind t₁ (λ a, t₂)
meta instance interaction_monad.monad : monad m :=
{map := @interaction_monad_fmap, pure := @interaction_monad_return, bind := @interaction_monad_bind}
meta def interaction_monad.mk_exception {α : Type u} {β : Type v} [has_to_format β] (msg : β) (ref : option expr) (s : state) : result state α :=
meta def interaction_monad.mk_exception {α : Type u} {β : Type v} [has_to_format β] (msg : β) (s : state) : result state α :=
exception (some (λ _, to_fmt msg)) none s
meta def interaction_monad.fail {α : Type u} {β : Type v} [has_to_format β] (msg : β) : m α :=
λ s, interaction_monad.mk_exception msg none s
λ s, interaction_monad.mk_exception msg s
meta def interaction_monad.silent_fail {α : Type u} : m α :=
λ s, exception none none s

9
library/init/meta/level.lean
View file

@ -1,9 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.name init.lean.level
export lean (level level.zero level.succ level.max level.imax level.param level.of_nat level.has_param)

29
library/init/meta/pexpr.lean
View file

@ -1,29 +0,0 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.meta.expr
universes u v
/-- Quoted expressions. They can be converted into expressions by using a tactic. -/
meta constant pexpr : Type
-- @[reducible] meta def pexpr := expr ff
protected meta constant pexpr.of_expr : expr → pexpr
protected meta constant pexpr.to_expr : pexpr → expr
@[instance] protected meta constant pexpr.reflect (e : pexpr) : reflected e
protected meta constant pexpr.subst : pexpr → pexpr → pexpr
meta class has_to_pexpr (α : Sort u) :=
(to_pexpr : α → pexpr)
meta def to_pexpr {α : Sort u} [has_to_pexpr α] : α → pexpr :=
has_to_pexpr.to_pexpr
meta instance : has_to_pexpr pexpr :=
⟨id⟩
meta instance : has_to_pexpr expr :=
⟨pexpr.of_expr⟩

17
library/init/meta/tactic.lean
View file

@ -6,8 +6,8 @@ Authors: Leonardo de Moura
prelude
import init.function init.data.option.basic init.util
import init.control.combinators init.control.monad init.control.alternative init.control.monad_fail
import init.data.nat.div init.meta.exceptional init.meta.format
import init.meta.pexpr init.data.repr init.data.string.basic init.meta.interaction_monad
import init.data.nat.div init.meta.format
import init.data.repr init.data.string.basic init.meta.interaction_monad
meta constant tactic_state : Type
@ -21,10 +21,6 @@ namespace tactic_state
Remark: the parameter `target_lhs_only` is a temporary hack used to implement
the `conv` monad. It will be removed in the future. -/
meta constant to_format (s : tactic_state) (target_lhs_only : bool := ff) : format
/-- Format expression with respect to the main goal in the tactic state.
If the tactic state does not contain any goals, then format expression
using an empty local context. -/
meta constant format_expr : tactic_state → expr → format
meta constant get_options : tactic_state → options
meta constant set_options : tactic_state → options → tactic_state
end tactic_state
@ -32,9 +28,6 @@ end tactic_state
meta instance : has_to_format tactic_state :=
⟨tactic_state.to_format⟩
meta instance : has_to_string tactic_state :=
⟨λ s, (to_fmt s).to_string s.get_options⟩
@[reducible] meta def tactic := interaction_monad tactic_state
@[reducible] meta def tactic_result := interaction_monad.result tactic_state
@ -71,15 +64,9 @@ variables {α : Type u}
end tactic
meta def tactic_format_expr (e : expr) : tactic format :=
do s ← tactic.read, return (tactic_state.format_expr s e)
meta class has_to_tactic_format (α : Type u) :=
(to_tactic_format : α → tactic format)
meta instance : has_to_tactic_format expr :=
⟨tactic_format_expr⟩
meta def tactic.pp {α : Type u} [has_to_tactic_format α] : α → tactic format :=
has_to_tactic_format.to_tactic_format

1
src/frontends/lean/builtin_exprs.cpp
View file

@ -20,7 +20,6 @@ Author: Leonardo de Moura
#include "library/string.h"
#include "library/trace.h"
#include "library/kernel_serializer.h"
#include "library/tactic/elaborate.h"
#include "library/equations_compiler/equations.h"
#include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/decl_cmds.h"

4
src/frontends/lean/decl_util.cpp
View file

@ -19,7 +19,6 @@ Author: Leonardo de Moura
#include "library/explicit.h"
#include "library/reducible.h"
#include "library/scoped_ext.h"
#include "library/tactic/elaborate.h"
#include "frontends/lean/util.h"
#include "frontends/lean/decl_util.h"
#include "frontends/lean/tokens.h"
@ -135,7 +134,6 @@ void collect_locals_ignoring_tactics(expr const & e, collected_locals & ls) {
if (!has_local(e)) return;
for_each(e, [&](expr const & e, unsigned) {
if (!has_local(e)) return false;
if (is_by(e)) return false; // do not visit children
if (is_local(e)) ls.insert(e);
return true;
});
@ -147,8 +145,6 @@ name_set collect_univ_params_ignoring_tactics(expr const & e, name_set const & l
for_each(e, [&](expr const & e, unsigned) {
if (!has_param_univ(e)) {
return false;
} else if (is_by(e)) {
return false;
} else if (is_sort(e)) {
collect_univ_params_core(sort_level(e), r);
} else if (is_constant(e)) {

58
src/frontends/lean/elaborator.cpp
View file

@ -41,11 +41,9 @@ Author: Leonardo de Moura
#include "library/aux_definition.h"
#include "library/check.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_expr.h"
#include "library/compiler/vm_compiler.h"
#include "library/tactic/kabstract.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/tactic_evaluator.h"
#include "library/equations_compiler/compiler.h"
#include "library/equations_compiler/util.h"
@ -1195,20 +1193,8 @@ struct elaborator::first_pass_info {
buffer<expr> eta_args;
};
expr elaborator::mk_auto_param(expr const & name_lit, expr const & expected_type, expr const & ref) {
auto c = name_lit_to_name(name_lit);
if (!c)
throw elaborator_exception(ref, format("invalid auto_param, name literal expected for identifying tactic") +
pp_indent(name_lit));
auto d = m_env.find(*c);
if (!d)
throw elaborator_exception(ref, sstream() << "invalid auto_param, unknown tactic '" << *c << "'");
if (!m_ctx.is_def_eq(d->get_type(), mk_tactic_unit()))
throw elaborator_exception(ref, format("invalid auto_param, invalid tactic '") + format(*c) +
format("' type should be (tactic unit)") +
pp_indent(d->get_type()));
expr t = copy_pos(ref, mk_by(copy_pos(ref, mk_constant(*c))));
return visit(t, some_expr(expected_type));
expr elaborator::mk_auto_param(expr const &, expr const &, expr const &) {
throw exception("auto_param has been disabled (we removed the tactic framework");
}
@ -4165,20 +4151,6 @@ static expr resolve_local_name(environment const & env, local_context const & lc
return *r;
}
vm_obj tactic_resolve_local_name(vm_obj const & vm_id, vm_obj const & vm_s) {
name const & id = to_name(vm_id);
tactic_state const & s = tactic::to_state(vm_s);
try {
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
expr src; // dummy
bool ignore_aliases = false;
return tactic::mk_success(to_obj(resolve_local_name(s.env(), g->get_context(), id, src, ignore_aliases, names())), s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
struct resolve_names_fn : public replace_visitor {
environment const & m_env;
local_context const & m_lctx;
@ -4249,7 +4221,7 @@ struct resolve_names_fn : public replace_visitor {
}
virtual expr visit(expr const & e) override {
if (is_placeholder(e) || is_by(e) || is_as_is(e) || is_emptyc_or_emptys(e) || is_as_atomic(e)) {
if (is_placeholder(e) || is_as_is(e) || is_emptyc_or_emptys(e) || is_as_atomic(e)) {
return e;
} else if (is_choice(e)) {
return visit_choice(e);
@ -4265,27 +4237,6 @@ expr resolve_names(environment const & env, local_context const & lctx, expr con
return resolve_names_fn(env, lctx)(e);
}
static vm_obj tactic_save_type_info(vm_obj const &, vm_obj const & _e, vm_obj const & ref, vm_obj const & _s) {
expr const & e = to_expr(_e);
tactic_state s = tactic::to_state(_s);
if (!get_global_info_manager() || !get_pos_info_provider()) return tactic::mk_success(s);
auto pos = get_pos_info_provider()->get_pos_info(to_expr(ref));
if (!pos) return tactic::mk_success(s);
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context();
try {
expr type = ctx.infer(e);
get_global_info_manager()->add_type_info(*pos, type);
if (is_constant(e))
get_global_info_manager()->add_identifier_info(*pos, const_name(e));
else if (is_local(e))
get_global_info_manager()->add_identifier_info(*pos, local_pp_name(e));
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
return tactic::mk_success(s);
}
void initialize_elaborator() {
g_elab_strategy = new name("elab_strategy");
register_trace_class("elaborator");
@ -4326,9 +4277,6 @@ void initialize_elaborator() {
register_incompatible("elab_simple", "elab_as_eliminator");
register_incompatible("elab_with_expected_type", "elab_as_eliminator");
DECLARE_VM_BUILTIN(name({"tactic", "save_type_info"}), tactic_save_type_info);
DECLARE_VM_BUILTIN(name({"tactic", "resolve_name"}), tactic_resolve_local_name);
g_elaborator_coercions = new name{"elaborator", "coercions"};
register_bool_option(*g_elaborator_coercions, LEAN_DEFAULT_ELABORATOR_COERCIONS,
"(elaborator) if true, the elaborator will automatically introduce coercions");

2
src/frontends/lean/inductive_cmds.cpp
View file

@ -32,8 +32,6 @@ Authors: Daniel Selsam, Leonardo de Moura
#include "library/normalize.h"
#include "library/inductive_compiler/add_decl.h"
#include "library/tactic/tactic_evaluator.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_expr.h"
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/decl_util.h"
#include "frontends/lean/util.h"

1
src/frontends/lean/interactive.cpp
View file

@ -16,7 +16,6 @@ Author: Sebastian Ullrich
#include "library/documentation.h"
#include "library/attribute_manager.h"
#include "library/vm/vm.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_format.h"
#include "frontends/lean/completion.h"

1
src/library/equations_compiler/elim_match.cpp
View file

@ -1289,7 +1289,6 @@ eqn_compiler_result mk_nonrec(environment & env, elaborator & elab, metavar_cont
expr fn;
std::tie(env, fn) = mk_aux_definition(env, elab.get_options(), mctx, lctx, header,
fn_name, fn_actual_name, fn_type, R.m_fn);
unsigned eqn_idx = 1;
type_context_old ctx2(env, mctx, lctx, elab.get_cache(), transparency_mode::Semireducible);
auto counter_examples = map2<expr>(R.m_counter_examples, [&] (list<expr> const & e) { return mk_app(fn, e); });
return { {fn}, counter_examples };

8
src/library/equations_compiler/wf_rec.cpp
View file

@ -13,9 +13,6 @@ Author: Leonardo de Moura
#include "library/app_builder.h"
#include "library/aux_definition.h"
#include "library/replace_visitor_with_tc.h"
#include "library/vm/vm.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_expr.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/tactic_evaluator.h"
#include "library/equations_compiler/pack_domain.h"
@ -84,7 +81,7 @@ struct wf_rec_fn {
m_R_wf = mk_app(ctx, get_has_well_founded_wf_name(), 2, mask, args);
}
void mk_wf_relation(expr const & eqns, expr const & wf_tacs) {
void mk_wf_relation(expr const & eqns, expr const & /* wf_tacs */) {
lean_assert(get_equations_header(eqns).m_num_fns == 1);
type_context_old ctx = mk_type_context();
unpack_eqns ues(ctx, eqns);
@ -105,6 +102,8 @@ struct wf_rec_fn {
}
init_R_R_wf(ctx, d, *m_has_well_founded_inst);
} else {
throw exception("well_founded_tactics has been removed");
/*
expr rel_tac = mk_app(mk_constant(get_well_founded_tactics_rel_tac_name()), wf_tacs);
vm_obj vm_fn = to_obj(ues.get_fn(0));
@ -129,6 +128,7 @@ struct wf_rec_fn {
"failed to create well founded relation using tactic",
std::current_exception());
}
*/
}
}

2
src/library/tactic/CMakeLists.txt
View file

@ -1,5 +1,5 @@
add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp
intro_tactic.cpp revert_tactic.cpp clear_tactic.cpp
subst_tactic.cpp induction_tactic.cpp cases_tactic.cpp
hsubstitution.cpp elaborate.cpp init_module.cpp
hsubstitution.cpp init_module.cpp
elaborator_exception.cpp tactic_evaluator.cpp)

3
src/library/tactic/cases_tactic.cpp
View file

@ -14,9 +14,6 @@ Author: Leonardo de Moura
#include "library/app_builder.h"
#include "library/trace.h"
#include "library/constructions/injective.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_expr.h"
#include "library/inductive_compiler/ginductive.h"
#include "library/tactic/cases_tactic.h"
#include "library/tactic/intro_tactic.h"

2
src/library/tactic/clear_tactic.cpp
View file

@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/vm/vm_name.h"
#include "library/vm/vm_expr.h"
#include "library/tactic/tactic_state.h"
namespace lean {

72
src/library/tactic/elaborate.cpp
View file

@ -1,72 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <frontends/lean/elaborator.h>
#include "kernel/for_each_fn.h"
#include "library/annotation.h"
#include "library/message_builder.h"
#include "library/vm/vm_expr.h"
#include "library/tactic/elaborate.h"
#include "library/tactic/elaborator_exception.h"
#include "library/tactic/tactic_state.h"
namespace lean {
static name * g_by_name = nullptr;
expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); }
bool is_by(expr const & e) { return is_annotation(e, *g_by_name); }
expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); }
vm_obj tactic_to_expr(vm_obj const & qe, vm_obj const & allow_mvars, vm_obj const & subgoals, vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
metavar_context mctx = s.mctx();
try {
environment env = s.env();
auto e = to_expr(qe);
bool recover_from_errors = false;
elaborator elab(env, s.get_options(), s.decl_name(), mctx, g->get_context(), recover_from_errors);
expr r = elab.elaborate(resolve_names(env, g->get_context(), e));
if (!to_bool(allow_mvars))
elab.ensure_no_unassigned_metavars(r);
mctx = elab.mctx();
env = elab.env();
r = mctx.instantiate_mvars(r);
if (to_bool(subgoals) && has_expr_metavar(r)) {
buffer<expr> new_goals;
name_set found;
for_each(r, [&](expr const & e, unsigned) {
if (!has_expr_metavar(e)) return false;
if (is_metavar_decl_ref(e) && !found.contains(mvar_name(e))) {
mctx.instantiate_mvars_at_type_of(e);
new_goals.push_back(e);
found.insert(local_name(e));
}
return true;
});
list<expr> new_gs = cons(head(s.goals()), to_list(new_goals.begin(), new_goals.end(), tail(s.goals())));
return tactic::mk_success(to_obj(r), set_env_mctx_goals(s, env, mctx, new_gs));
} else {
return tactic::mk_success(to_obj(r), set_env_mctx(s, env, mctx));
}
} catch (elaborator_exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
void initialize_elaborate() {
g_by_name = new name("by");
register_annotation(*g_by_name);
DECLARE_VM_BUILTIN(name({"tactic", "to_expr"}), tactic_to_expr);
}
void finalize_elaborate() {
delete g_by_name;
}
}

18
src/library/tactic/elaborate.h
View file

@ -1,18 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
#include "library/metavar_context.h"
namespace lean {
expr mk_by(expr const & e);
bool is_by(expr const & e);
expr const & get_by_arg(expr const & e);
void initialize_elaborate();
void finalize_elaborate();
}

1
src/library/tactic/induction_tactic.cpp
View file

@ -15,7 +15,6 @@ Author: Leonardo de Moura
#include "library/aux_recursors.h"
#include "library/locals.h"
#include "library/app_builder.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_list.h"

3
src/library/tactic/init_module.cpp
View file

@ -11,7 +11,6 @@ Author: Leonardo de Moura
#include "library/tactic/subst_tactic.h"
#include "library/tactic/induction_tactic.h"
#include "library/tactic/cases_tactic.h"
#include "library/tactic/elaborate.h"
namespace lean {
void initialize_tactic_module() {
@ -22,10 +21,8 @@ void initialize_tactic_module() {
initialize_subst_tactic();
initialize_induction_tactic();
initialize_cases_tactic();
initialize_elaborate();
}
void finalize_tactic_module() {
finalize_elaborate();
finalize_cases_tactic();
finalize_induction_tactic();
finalize_subst_tactic();

1
src/library/tactic/intro_tactic.cpp
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
#include "library/util.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_expr.h"
#include "library/tactic/tactic_state.h"
namespace lean {

1
src/library/tactic/kabstract.cpp
View file

@ -12,7 +12,6 @@ Author: Leonardo de Moura
#include "library/head_map.h"
#include "library/trace.h"
#include "library/type_context.h"
#include "library/vm/vm_expr.h"
#include "library/tactic/occurrences.h"
#include "library/tactic/tactic_state.h"

2
src/library/tactic/subst_tactic.cpp
View file

@ -12,8 +12,6 @@ Author: Leonardo de Moura
#include "library/trace.h"
#include "library/locals.h"
#include "library/app_builder.h"
#include "library/vm/vm.h"
#include "library/vm/vm_expr.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/revert_tactic.h"
#include "library/tactic/intro_tactic.h"

626
src/library/tactic/tactic_state.cpp
View file

@ -20,15 +20,11 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h"
#include "library/aux_definition.h"
#include "library/inductive_compiler/ginductive.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_format.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_options.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_level.h"
#include "library/vm/vm_declaration.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_io.h"
@ -281,21 +277,10 @@ format pp_indented_expr(tactic_state const & s, expr const & e) {
return nest(get_pp_indent(s.get_options()), line() + s.pp_expr(fmtf, e));
}
vm_obj tactic_state_format_expr(vm_obj const & s, vm_obj const & e) {
return to_obj(pp_expr(tactic::to_state(s), to_expr(e)));
}
vm_obj mk_no_goals_exception(tactic_state const & s) {
return tactic::mk_exception("tactic failed, there are no goals to be solved", s);
}
vm_obj tactic_result(vm_obj const & o) {
tactic_state const & s = tactic::to_state(o);
metavar_context mctx = s.mctx();
expr r = mctx.instantiate_mvars(s.main());
return tactic::mk_success(to_obj(r), set_mctx(s, mctx));
}
vm_obj tactic_format_result(vm_obj const & o) {
tactic_state const & s = tactic::to_state(o);
metavar_context mctx = s.mctx();
@ -307,13 +292,6 @@ vm_obj tactic_format_result(vm_obj const & o) {
return tactic::mk_success(to_obj(fmt(r)), s);
}
vm_obj tactic_target(vm_obj const & o) {
tactic_state const & s = tactic::to_state(o);
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
return tactic::mk_success(to_obj(g->get_type()), s);
}
tactic_state_context_cache::tactic_state_context_cache(tactic_state & s):
persistent_context_cache(s.get_cache_id(), s.get_options()),
m_state(set_context_cache_id(s, get_id())) {
@ -362,408 +340,6 @@ type_context_old mk_cacheless_type_context_for(tactic_state const & s, transpare
return mk_type_context_for(s, m);
}
static void check_closed(char const * tac_name, expr const & e) {
if (has_loose_bvars(e))
throw exception(sstream() << "tactic '" << tac_name << "' failed, "
"given expression should not contain de-Bruijn variables, "
"they should be replaced with local constants before using this tactic");
}
vm_obj tactic_infer_type(vm_obj const & e, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context();
try {
check_closed("infer_type", to_expr(e));
return tactic::mk_success(to_obj(ctx.infer(to_expr(e))), s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_whnf(vm_obj const & e, vm_obj const & t, vm_obj const & unfold_ginductive, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context(to_transparency_mode(t));
try {
check_closed("whnf", to_expr(e));
if (to_bool(unfold_ginductive)) {
return tactic::mk_success(to_obj(ctx.whnf(to_expr(e))), s);
} else {
return tactic::mk_success(to_obj(whnf_ginductive_gintro_rule(ctx, to_expr(e))), s);
}
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_head_eta_expand(vm_obj const & e, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context();
try {
check_closed("head_eta_expand", to_expr(e));
return tactic::mk_success(to_obj(ctx.eta_expand(to_expr(e))), s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_head_eta(vm_obj const & e, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
try {
return tactic::mk_success(to_obj(try_eta(to_expr(e))), s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_head_beta(vm_obj const & e, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
try {
return tactic::mk_success(to_obj(annotated_head_beta_reduce(to_expr(e))), s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_head_zeta(vm_obj const & e0, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
try {
expr const & e = to_expr(e0);
check_closed("head_zeta", e);
if (!is_local(e)) return tactic::mk_success(e0, s);
optional<metavar_decl> mdecl = s.get_main_goal_decl();
if (!mdecl) return tactic::mk_success(e0, s);
local_context lctx = mdecl->get_context();
optional<local_decl> ldecl = lctx.find_local_decl(e);
if (!ldecl || !ldecl->get_value()) return tactic::mk_success(e0, s);
return tactic::mk_success(to_obj(*ldecl->get_value()), s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_zeta(vm_obj const & e0, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
try {
expr const & e = to_expr(e0);
check_closed("zeta", e);
optional<metavar_decl> mdecl = s.get_main_goal_decl();
if (!mdecl) return tactic::mk_success(e0, s);
local_context lctx = mdecl->get_context();
return tactic::mk_success(to_obj(zeta_expand(lctx, e)), s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_is_class(vm_obj const & e, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context();
try {
check_closed("is_class", to_expr(e));
return tactic::mk_success(mk_vm_bool(static_cast<bool>(ctx.is_class(to_expr(e)))), s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_mk_instance(vm_obj const & e, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context();
try {
check_closed("mk_instance", to_expr(e));
if (auto r = ctx.mk_class_instance(to_expr(e))) {
tactic_state new_s = set_mctx(s, ctx.mctx());
return tactic::mk_success(to_obj(*r), new_s);
} else {
auto thunk = [=]() {
format m("tactic.mk_instance failed to generate instance for");
m += pp_indented_expr(s, to_expr(e));
return m;
};
return tactic::mk_exception(thunk, s);
}
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
static vm_obj mk_unify_exception(char const * header, expr const & e1, expr const & e2, tactic_state const & s) {
auto thunk = [=]() {
format r(header);
unsigned indent = get_pp_indent(s.get_options());
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
type_context_old ctx = mk_cacheless_type_context_for(s, transparency_mode::All);
formatter fmt = fmtf(s.env(), s.get_options(), ctx);
expr e1_type = ctx.infer(e1);
expr e2_type = ctx.infer(e2);
format e1_fmt = fmt(e1);
format e1_type_fmt = fmt(e1_type);
format e2_fmt = fmt(e2);
format e2_type_fmt = fmt(e2_type);
r += nest(indent, line() + group(e1_fmt + line() + format(": ") + e1_type_fmt));
r += line() + format("and");
r += nest(indent, line() + group(e2_fmt + line() + format(": ") + e2_type_fmt));
return r;
};
return tactic::mk_exception(thunk, s);
}
vm_obj tactic_unify(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_obj const & approx, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context(to_transparency_mode(t));
try {
check_closed("unify", to_expr(e1));
check_closed("unify", to_expr(e2));
type_context_old::approximate_scope scope(ctx, to_bool(approx));
bool r = ctx.is_def_eq(to_expr(e1), to_expr(e2));
if (r) {
return tactic::mk_success(set_mctx(s, ctx.mctx()));
} else {
return mk_unify_exception("unify tactic failed, failed to unify",
to_expr(e1), to_expr(e2), s);
}
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_is_def_eq(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_obj const & approx, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context(to_transparency_mode(t));
try {
check_closed("is_def_eq", to_expr(e1));
check_closed("is_def_eq", to_expr(e2));
type_context_old::approximate_scope scope(ctx, to_bool(approx));
bool r = ctx.pure_is_def_eq(to_expr(e1), to_expr(e2));
if (r) {
return tactic::mk_success(s);
} else {
return mk_unify_exception("is_def_eq tactic failed, the following expressions are not definitionally equal "
"(remark: is_def_eq tactic does modify the metavariable assignment)",
to_expr(e1), to_expr(e2), s);
}
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_get_local(vm_obj const & n, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
local_context lctx = g->get_context();
optional<local_decl> d = lctx.find_local_decl_from_user_name(to_name(n));
if (!d) return tactic::mk_exception(sstream() << "get_local tactic failed, unknown '" << to_name(n) << "' local", s);
return tactic::mk_success(to_obj(d->mk_ref()), s);
}
vm_obj tactic_local_context(vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
local_context lctx = g->get_context();
buffer<expr> r;
lctx.for_each([&](local_decl const & d) { r.push_back(d.mk_ref()); });
return tactic::mk_success(to_obj(to_list(r)), s);
}
vm_obj tactic_get_unused_name(vm_obj const & n, vm_obj const & vm_i, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
name unused_name;
if (is_none(vm_i)) {
unused_name = g->get_context().get_unused_name(to_name(n));
} else {
unsigned i = force_to_unsigned(get_some_value(vm_i), 0);
unused_name = g->get_context().get_unused_name(to_name(n), i);
}
return tactic::mk_success(to_obj(unused_name), s);
}
vm_obj rotate_left(unsigned n, tactic_state const & s) {
buffer<expr> gs;
to_buffer(s.goals(), gs);
unsigned sz = gs.size();
if (sz == 0)
return tactic::mk_success(s);
n = n%sz;
std::rotate(gs.begin(), gs.begin() + n, gs.end());
return tactic::mk_success(set_goals(s, to_list(gs)));
}
vm_obj tactic_rotate_left(vm_obj const & n, vm_obj const & s) {
return rotate_left(force_to_unsigned(n, 0), tactic::to_state(s));
}
vm_obj tactic_get_goals(vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
return tactic::mk_success(to_obj(s.goals()), s);
}
vm_obj set_goals(list<expr> const & gs, tactic_state const & s) {
buffer<expr> new_gs;
metavar_context const & mctx = s.mctx();
for (expr const & g : gs) {
if (!mctx.find_metavar_decl(g)) {
return tactic::mk_exception("invalid set_goals tactic, expressions must be meta-variables "
"that have been declared in the current tactic_state", s);
}
if (!mctx.is_assigned(g))
new_gs.push_back(g);
}
return tactic::mk_success(set_goals(s, to_list(new_gs)));
}
vm_obj tactic_set_goals(vm_obj const & gs, vm_obj const & s) {
return set_goals(to_list_expr(gs), tactic::to_state(s));
}
vm_obj tactic_mk_meta_univ(vm_obj const & s) {
metavar_context mctx = tactic::to_state(s).mctx();
level u = mctx.mk_univ_metavar_decl();
return tactic::mk_success(to_obj(u), set_mctx(tactic::to_state(s), mctx));
}
vm_obj tactic_mk_meta_var(vm_obj const & t, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
metavar_context mctx = s.mctx();
local_context lctx;
if (optional<metavar_decl> g = s.get_main_goal_decl()) {
lctx = g->get_context();
}
expr m = mctx.mk_metavar_decl(lctx, to_expr(t));
return tactic::mk_success(to_obj(m), set_mctx(s, mctx));
}
vm_obj tactic_get_univ_assignment(vm_obj const & u, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
metavar_context mctx = s.mctx();
if (!is_mvar(to_level(u))) {
return tactic::mk_exception("get_univ_assignment tactic failed, argument is not an universe metavariable", s);
} else if (auto r = mctx.get_assignment(to_level(u))) {
return tactic::mk_success(to_obj(*r), s);
} else {
return tactic::mk_exception("get_univ_assignment tactic failed, universe metavariable is not assigned", s);
}
}
vm_obj tactic_get_assignment(vm_obj const & e, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
metavar_context mctx = s.mctx();
if (!is_metavar(to_expr(e))) {
return tactic::mk_exception("get_assignment tactic failed, argument is not a metavariable", s);
} else if (auto r = mctx.get_assignment(to_expr(e))) {
return tactic::mk_success(to_obj(*r), s);
} else {
return tactic::mk_exception("get_assignment tactic failed, metavariable is not assigned", s);
}
}
vm_obj tactic_is_assigned(vm_obj const & g, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
if (!is_metavar(to_expr(g))) {
return tactic::mk_exception("is_assigned tactic failed, argument is not a metavariable", s);
} else {
return tactic::mk_success(mk_vm_bool(s.mctx().is_assigned(to_expr(g))), s);
}
}
vm_obj tactic_state_get_options(vm_obj const & s) {
return to_obj(tactic::to_state(s).get_options());
}
vm_obj tactic_state_set_options(vm_obj const & s, vm_obj const & o) {
return to_obj(set_options(tactic::to_state(s), to_options(o)));
}
vm_obj tactic_mk_fresh_name(vm_obj const & s) {
return tactic::mk_success(to_obj(mk_fresh_name()), tactic::to_state(s));
}
vm_obj tactic_is_trace_enabled_for(vm_obj const & n) {
return mk_vm_bool(is_trace_class_enabled(to_name(n)));
}
vm_obj tactic_instantiate_mvars(vm_obj const & e, vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
metavar_context mctx = s.mctx();
expr r = mctx.instantiate_mvars(to_expr(e));
return tactic::mk_success(to_obj(r), set_mctx(s, mctx));
}
vm_obj tactic_add_decl(vm_obj const & _d, vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
try {
declaration d = to_declaration(_d);
environment new_env = module::add(s.env(), d);
new_env = vm_compile(new_env, d);
return tactic::mk_success(set_env(s, new_env));
} catch (throwable & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_open_namespaces(vm_obj const & s) {
environment env = tactic::to_state(s).env();
buffer<name> b;
to_buffer(get_namespaces(env), b);
get_opened_namespaces(env).to_buffer(b);
return tactic::mk_success(to_obj(b), tactic::to_state(s));
}
vm_obj tactic_doc_string(vm_obj const & n, vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
if (optional<std::string> doc = get_doc_string(s.env(), to_name(n))) {
return tactic::mk_success(to_obj(*doc), s);
} else {
return tactic::mk_exception(sstream() << "no doc string for '" << to_name(n) << "'", s);
}
}
vm_obj tactic_add_doc_string(vm_obj const & n, vm_obj const & doc, vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
try {
environment new_env = add_doc_string(s.env(), to_name(n), to_string(doc));
return tactic::mk_success(set_env(s, new_env));
} catch (throwable & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
/* meta constant module_doc_strings : tactic (list (option name × string)) */
vm_obj tactic_module_doc_strings(vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
buffer<doc_entry> entries;
get_module_doc_strings(s.env(), entries);
unsigned i = entries.size();
vm_obj r = mk_vm_simple(0);
while (i > 0) {
--i;
vm_obj decl_name;
if (auto d = entries[i].get_decl_name())
decl_name = mk_vm_some(to_obj(*d));
else
decl_name = mk_vm_none();
vm_obj doc = to_obj(entries[i].get_doc());
vm_obj e = mk_vm_pair(decl_name, doc);
r = mk_vm_constructor(1, e, r);
}
return tactic::mk_success(r, s);
}
vm_obj tactic_decl_name(vm_obj const & _s) {
auto & s = tactic::to_state(_s);
return tactic::mk_success(to_obj(s.decl_name()), s);
}
format tactic_state::pp() const {
type_context_old ctx = mk_cacheless_type_context_for(*this, transparency_mode::Semireducible);
expr ts_expr = mk_constant("tactic_state");
@ -789,21 +365,6 @@ format tactic_state::pp() const {
}
}
vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const & val, vm_obj const & lemma, vm_obj const & _s) {
tactic_state const & s = tactic::to_state(_s);
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
try {
pair<environment, expr> r =
to_bool(lemma) ?
mk_aux_lemma(s.env(), s.mctx(), g->get_context(), to_name(n), to_expr(type), to_expr(val))
: mk_aux_definition(s.env(), s.mctx(), g->get_context(), to_name(n), to_expr(type), to_expr(val));
return tactic::mk_success(to_obj(r.second), set_env(s, r.first));
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const & s) {
return tactic::mk_success(run_io(a), s);
}
@ -819,197 +380,10 @@ vm_obj io_run_tactic(vm_obj const &, vm_obj const & tac, vm_obj const &) {
return mk_ioe_result(tactic::get_success_value(r));
}
unsigned tactic_user_state::alloc(vm_obj const & v) {
unsigned r;
if (m_free_refs) {
r = head(m_free_refs);
m_free_refs = tail(m_free_refs);
} else {
r = m_next_idx;
m_next_idx++;
}
m_mem.insert(r, v);
return r;
}
void tactic_user_state::dealloc(unsigned ref) {
if (!m_mem.contains(ref)) {
throw exception("invalid ref dealloc, invalid reference");
}
m_free_refs = cons(ref, m_free_refs);
m_mem.erase(ref);
}
vm_obj tactic_user_state::read(unsigned ref) const {
if (auto v = m_mem.find(ref)) {
return *v;
} else {
throw exception("invalid read_ref, invalid reference");
}
}
void tactic_user_state::write(unsigned ref, vm_obj const & o) {
if (m_mem.contains(ref)) {
m_mem.insert(ref, o);
} else {
throw exception("invalid write_ref, invalid reference");
}
}
/*
meta constant using_new_ref {α : Type u} {β : Type v} (a : α) (t : ref α → tactic β) : tactic β
*/
vm_obj tactic_using_new_ref(vm_obj const &, vm_obj const &, vm_obj const & a, vm_obj const & t, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
try {
tactic_user_state us = s.us();
unsigned ref = us.alloc(a);
s = set_user_state(s, us);
vm_obj r = invoke(t, mk_vm_simple(ref), to_obj(s));
if (tactic::is_result_success(r)) {
vm_obj b = tactic::get_success_value(r);
s = tactic::to_state(tactic::get_success_state(r));
us = s.us();
us.dealloc(ref);
s = set_user_state(s, us);
return tactic::mk_success(b, s);
} else {
return r;
}
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
/*
meta constant read_ref {α : Type u} : ref α → tactic α
*/
vm_obj tactic_read_ref(vm_obj const &, vm_obj const & ref, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
try {
tactic_user_state const & us = s.us();
vm_obj r = us.read(cidx(ref));
return tactic::mk_success(r, s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
/*
meta constant write_ref {α : Type u} : ref α → α → tactic unit
*/
vm_obj tactic_write_ref(vm_obj const &, vm_obj const & ref, vm_obj const & v, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
try {
tactic_user_state us = s.us();
us.write(cidx(ref), v);
s = set_user_state(s, us);
return tactic::mk_success(s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_sleep(vm_obj const & msecs, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
if (optional<unsigned> m = try_to_unsigned(msecs)) {
chrono::milliseconds cm(*m);
sleep_for(cm);
return tactic::mk_success(s);
} else {
return tactic::mk_exception("sleep failed, argument is too big", s);
}
}
vm_obj tactic_type_check(vm_obj const & e, vm_obj const & m, vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
try {
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context(to_transparency_mode(m));
check(ctx, to_expr(e));
return tactic::mk_success(s);
} catch (exception & ex) {
return tactic::mk_exception(std::current_exception(), s);
}
}
vm_obj tactic_unfreeze_local_instances(vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
local_context lctx = g->get_context();
tactic_state_context_cache cache(s);
type_context_old ctx = cache.mk_type_context();
lctx.unfreeze_local_instances();
expr new_mvar = ctx.mk_metavar_decl(lctx, g->get_type());
ctx.assign(*s.get_main_goal(), new_mvar);
tactic_state new_s = set_mctx_goals(s, ctx.mctx(), cons(new_mvar, tail(s.goals())));
return tactic::mk_success(new_s);
}
vm_obj tactic_frozen_local_instances(vm_obj const & s0) {
tactic_state s = tactic::to_state(s0);
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
local_context lctx = g->get_context();
if (optional<local_instances> lis = lctx.get_frozen_local_instances()) {
buffer<expr> li_buffer;
for (local_instance const & li : *lis)
li_buffer.push_back(li.get_local());
return tactic::mk_success(mk_vm_some(to_obj(li_buffer)), s);
} else {
return tactic::mk_success(mk_vm_none(), s);
}
}
void initialize_tactic_state() {
DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}), tactic_state_format_expr);
DECLARE_VM_BUILTIN(name({"tactic_state", "to_format"}), tactic_state_to_format);
DECLARE_VM_BUILTIN(name({"tactic_state", "get_options"}), tactic_state_get_options);
DECLARE_VM_BUILTIN(name({"tactic_state", "set_options"}), tactic_state_set_options);
DECLARE_VM_BUILTIN(name({"tactic", "target"}), tactic_target);
DECLARE_VM_BUILTIN(name({"tactic", "result"}), tactic_result);
DECLARE_VM_BUILTIN(name({"tactic", "is_assigned"}), tactic_is_assigned);
DECLARE_VM_BUILTIN(name({"tactic", "format_result"}), tactic_format_result);
DECLARE_VM_BUILTIN(name({"tactic", "infer_type"}), tactic_infer_type);
DECLARE_VM_BUILTIN(name({"tactic", "whnf"}), tactic_whnf);
DECLARE_VM_BUILTIN(name({"tactic", "is_def_eq"}), tactic_is_def_eq);
DECLARE_VM_BUILTIN(name({"tactic", "head_eta_expand"}), tactic_head_eta_expand);
DECLARE_VM_BUILTIN(name({"tactic", "head_eta"}), tactic_head_eta);
DECLARE_VM_BUILTIN(name({"tactic", "head_beta"}), tactic_head_beta);
DECLARE_VM_BUILTIN(name({"tactic", "head_zeta"}), tactic_head_zeta);
DECLARE_VM_BUILTIN(name({"tactic", "zeta"}), tactic_zeta);
DECLARE_VM_BUILTIN(name({"tactic", "is_class"}), tactic_is_class);
DECLARE_VM_BUILTIN(name({"tactic", "mk_instance"}), tactic_mk_instance);
DECLARE_VM_BUILTIN(name({"tactic", "unify"}), tactic_unify);
DECLARE_VM_BUILTIN(name({"tactic", "get_local"}), tactic_get_local);
DECLARE_VM_BUILTIN(name({"tactic", "local_context"}), tactic_local_context);
DECLARE_VM_BUILTIN(name({"tactic", "get_unused_name"}), tactic_get_unused_name);
DECLARE_VM_BUILTIN(name({"tactic", "rotate_left"}), tactic_rotate_left);
DECLARE_VM_BUILTIN(name({"tactic", "get_goals"}), tactic_get_goals);
DECLARE_VM_BUILTIN(name({"tactic", "set_goals"}), tactic_set_goals);
DECLARE_VM_BUILTIN(name({"tactic", "mk_meta_univ"}), tactic_mk_meta_univ);
DECLARE_VM_BUILTIN(name({"tactic", "mk_meta_var"}), tactic_mk_meta_var);
DECLARE_VM_BUILTIN(name({"tactic", "get_univ_assignment"}), tactic_get_univ_assignment);
DECLARE_VM_BUILTIN(name({"tactic", "get_assignment"}), tactic_get_assignment);
DECLARE_VM_BUILTIN(name({"tactic", "mk_fresh_name"}), tactic_mk_fresh_name);
DECLARE_VM_BUILTIN(name({"tactic", "is_trace_enabled_for"}), tactic_is_trace_enabled_for);
DECLARE_VM_BUILTIN(name({"tactic", "instantiate_mvars"}), tactic_instantiate_mvars);
DECLARE_VM_BUILTIN(name({"tactic", "add_decl"}), tactic_add_decl);
DECLARE_VM_BUILTIN(name({"tactic", "doc_string"}), tactic_doc_string);
DECLARE_VM_BUILTIN(name({"tactic", "add_doc_string"}), tactic_add_doc_string);
DECLARE_VM_BUILTIN(name({"tactic", "module_doc_strings"}), tactic_module_doc_strings);
DECLARE_VM_BUILTIN(name({"tactic", "open_namespaces"}), tactic_open_namespaces);
DECLARE_VM_BUILTIN(name({"tactic", "decl_name"}), tactic_decl_name);
DECLARE_VM_BUILTIN(name({"tactic", "add_aux_decl"}), tactic_add_aux_decl);
DECLARE_VM_BUILTIN(name({"tactic", "unsafe_run_io"}), tactic_unsafe_run_io);
DECLARE_VM_BUILTIN(name({"tactic", "using_new_ref"}), tactic_using_new_ref);
DECLARE_VM_BUILTIN(name({"tactic", "read_ref"}), tactic_read_ref);
DECLARE_VM_BUILTIN(name({"tactic", "write_ref"}), tactic_write_ref);
DECLARE_VM_BUILTIN(name({"tactic", "sleep"}), tactic_sleep);
DECLARE_VM_BUILTIN(name({"tactic", "type_check"}), tactic_type_check);
DECLARE_VM_BUILTIN(name({"tactic", "unfreeze_local_instances"}), tactic_unfreeze_local_instances);
DECLARE_VM_BUILTIN(name({"tactic", "frozen_local_instances"}), tactic_frozen_local_instances);
DECLARE_VM_BUILTIN(name({"io", "run_tactic"}), io_run_tactic);
}

3
src/library/tactic/tactic_state.h
View file

@ -214,9 +214,6 @@ type_context_old mk_cacheless_type_context_for(tactic_state const & s, transpare
Code \
})
#define LEAN_TACTIC_TRY try {
#define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return tactic::mk_exception(std::current_exception(), S); }
void initialize_tactic_state();
void finalize_tactic_state();
}

3
src/library/vm/CMakeLists.txt
View file

@ -1,4 +1,3 @@
add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
vm_options.cpp vm_format.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
vm_declaration.cpp vm_list.cpp vm_pexpr.cpp
vm_options.cpp vm_format.cpp vm_list.cpp
vm_int.cpp init_module.cpp vm_array.cpp vm_pos_info.cpp vm_platform.cpp)

17
src/library/vm/init_module.cpp
View file

@ -12,12 +12,7 @@ Author: Leonardo de Moura
#include "library/vm/vm_name.h"
#include "library/vm/vm_options.h"
#include "library/vm/vm_format.h"
#include "library/vm/vm_level.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_pexpr.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_declaration.h"
#include "library/vm/vm_array.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_platform.h"
@ -32,12 +27,7 @@ void initialize_vm_core_module() {
initialize_vm_name();
initialize_vm_options();
initialize_vm_format();
initialize_vm_level();
initialize_vm_expr();
initialize_vm_pexpr();
initialize_vm_list();
initialize_vm_exceptional();
initialize_vm_declaration();
initialize_vm_array();
initialize_vm_string();
initialize_vm_platform();
@ -47,12 +37,7 @@ void finalize_vm_core_module() {
finalize_vm_platform();
finalize_vm_string();
finalize_vm_array();
finalize_vm_declaration();
finalize_vm_exceptional();
finalize_vm_list();
finalize_vm_pexpr();
finalize_vm_expr();
finalize_vm_level();
finalize_vm_format();
finalize_vm_options();
finalize_vm_name();
@ -65,8 +50,6 @@ void finalize_vm_core_module() {
void initialize_vm_module() {
initialize_vm();
initialize_vm_expr_builtin_idxs();
initialize_vm_exceptional_builtin_idxs();
initialize_vm_format_builtin_idxs();
initialize_vm_array_builtin_idxs();
}

19
src/library/vm/interaction_state_imp.h
View file

@ -14,15 +14,11 @@ Authors: Leonardo de Moura, Sebastian Ullrich
#include "library/message_builder.h"
#include "library/time_task.h"
#include "library/vm/interaction_state.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_format.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_options.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_level.h"
#include "library/vm/vm_declaration.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_pos_info.h"
@ -155,18 +151,9 @@ vm_obj interaction_monad<State>::update_exception_state(vm_obj const & ex, State
}
template<typename State>
vm_obj interaction_monad<State>::mk_exception(std::exception_ptr const & ex, State const & s) {
vm_obj _ex = lean::to_obj(ex);
vm_obj fn = mk_vm_closure(get_throwable_to_format_fun_idx(), 1, &_ex);
optional<pos_info> pos;
try {
std::rethrow_exception(ex);
} catch (exception_with_pos & ex) {
pos = ex.get_pos();
} catch (...) {
}
vm_obj _pos = pos ? mk_vm_some(mk_vm_pair(mk_vm_nat(pos->first), mk_vm_nat(pos->second))) : mk_vm_none();
return mk_exception(fn, _pos, s);
vm_obj interaction_monad<State>::mk_exception(std::exception_ptr const &, State const &) {
// vm_exceptional has been deleted
lean_unreachable();
}
template<typename State>

12
src/library/vm/vm.cpp
View file

@ -29,7 +29,6 @@ Author: Leonardo de Moura
#include "library/vm/vm.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_expr.h"
#include "library/normalize.h"
#ifndef LEAN_DEFAULT_PROFILER_FREQ
@ -2980,17 +2979,6 @@ void vm_state::run() {
m_stack.push_back(mk_vm_mpz(instr.get_mpz()));
m_pc++;
goto main_loop;
case opcode::Expr:
/** Instruction: pexpr e
stack before, after
... ...
v ==> v
e
*/
m_stack.push_back(to_obj(instr.get_expr()));
m_pc++;
goto main_loop;
case opcode::LocalInfo:
if (m_debugging)
push_local_info(instr.get_local_idx(), instr.get_local_info());

214
src/library/vm/vm_declaration.cpp
View file

@ -1,214 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/instantiate.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_level.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_option.h"
namespace lean {
/*
inductive reducibility_hint
| opaque : reducibility_hint
| abbrev : reducibility_hint
| regular : nat → bool → reducibility_hint
*/
vm_obj to_obj(reducibility_hints const & h) {
switch (h.kind()) {
case reducibility_hints_kind::Opaque: return mk_vm_simple(0);
case reducibility_hints_kind::Abbreviation: return mk_vm_simple(1);
case reducibility_hints_kind::Regular: return mk_vm_constructor(2, mk_vm_nat(h.get_height()));
}
lean_unreachable();
}
reducibility_hints to_reducibility_hints(vm_obj const & o) {
switch (cidx(o)) {
case 0: return reducibility_hints::mk_opaque();
case 1: return reducibility_hints::mk_abbreviation();
case 2: return reducibility_hints::mk_regular(force_to_unsigned(cfield(o, 0), 0));
}
lean_unreachable();
}
struct vm_declaration : public vm_external {
declaration m_val;
vm_declaration(declaration const & v):m_val(v) {}
virtual ~vm_declaration() {}
virtual void dealloc() override { delete this; }
virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_declaration(m_val); }
virtual vm_external * clone(vm_clone_fn const &) override { return new vm_declaration(m_val); }
};
bool is_declaration(vm_obj const & o) {
return is_external(o) && dynamic_cast<vm_declaration*>(to_external(o));
}
declaration const & to_declaration(vm_obj const & o) {
lean_vm_check(dynamic_cast<vm_declaration*>(to_external(o)));
return static_cast<vm_declaration*>(to_external(o))->m_val;
}
vm_obj to_obj(declaration const & n) {
return mk_vm_external(new vm_declaration(n));
}
vm_obj declaration_defn(vm_obj const & val) {
return to_obj(mk_definition(to_name(cfield(cfield(val, 0), 0)),
to_names(cfield(cfield(val, 0), 1)),
to_expr(cfield(cfield(val, 0), 2)),
to_expr(cfield(val, 1)),
to_reducibility_hints(cfield(val, 2)),
to_bool(cfield(val, 3))));
}
vm_obj declaration_thm(vm_obj const & val) {
return to_obj(mk_theorem(to_name(cfield(cfield(val, 0), 0)),
to_names(cfield(cfield(val, 0), 1)),
to_expr(cfield(cfield(val, 0), 2)),
to_expr(cfield(val, 1))));
}
vm_obj declaration_ax(vm_obj const & val) {
return to_obj(mk_axiom(to_name(cfield(cfield(val, 0), 0)),
to_names(cfield(cfield(val, 0), 1)),
to_expr(cfield(cfield(val, 0), 2)),
to_bool(cfield(val, 1))));
}
vm_obj mk_declaration_val(declaration const & d) {
return mk_vm_constructor(0, to_obj(d.get_name()), to_obj(d.get_univ_params()), to_obj(d.get_type()));
}
unsigned declaration_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
declaration const & d = to_declaration(o);
switch (d.kind()) {
case declaration_kind::Definition:
data.push_back(mk_vm_constructor(0, mk_declaration_val(d), to_obj(d.get_value()), to_obj(d.get_hints()), mk_vm_bool(d.is_meta())));
break;
case declaration_kind::Axiom:
data.push_back(mk_vm_constructor(0, mk_declaration_val(d), mk_vm_bool(d.is_meta())));
break;
case declaration_kind::Theorem:
data.push_back(mk_vm_constructor(0, mk_declaration_val(d), to_obj(d.get_value())));
break;
case declaration_kind::Inductive: lean_unreachable(); // TODO(Leo):
case declaration_kind::Constructor: lean_unreachable(); // TODO(Leo):
case declaration_kind::Recursor: lean_unreachable(); // TODO(Leo):
}
return static_cast<unsigned>(d.kind());
}
struct vm_constant_info : public vm_external {
constant_info m_val;
vm_constant_info(constant_info const & v):m_val(v) {}
virtual ~vm_constant_info() {}
virtual void dealloc() override { delete this; }
virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_constant_info(m_val); }
virtual vm_external * clone(vm_clone_fn const &) override { return new vm_constant_info(m_val); }
};
bool is_constant_info(vm_obj const & o) {
return is_external(o) && dynamic_cast<vm_constant_info*>(to_external(o));
}
constant_info const & to_constant_info(vm_obj const & o) {
lean_vm_check(dynamic_cast<vm_constant_info*>(to_external(o)));
return static_cast<vm_constant_info*>(to_external(o))->m_val;
}
vm_obj to_obj(constant_info const & n) {
return mk_vm_external(new vm_constant_info(n));
}
vm_obj constant_info_defn(vm_obj const & val) {
return to_obj(mk_definition(to_name(cfield(cfield(val, 0), 0)),
to_names(cfield(cfield(val, 0), 1)),
to_expr(cfield(cfield(val, 0), 2)),
to_expr(cfield(val, 1)),
to_reducibility_hints(cfield(val, 2)),
to_bool(cfield(val, 3))));
}
vm_obj constant_info_thm(vm_obj const & val) {
return to_obj(mk_theorem(to_name(cfield(cfield(val, 0), 0)),
to_names(cfield(cfield(val, 0), 1)),
to_expr(cfield(cfield(val, 0), 2)),
to_expr(cfield(val, 1))));
}
vm_obj constant_info_ax(vm_obj const & val) {
return to_obj(mk_axiom(to_name(cfield(cfield(val, 0), 0)),
to_names(cfield(cfield(val, 0), 1)),
to_expr(cfield(cfield(val, 0), 2)),
to_bool(cfield(val, 1))));
}
vm_obj mk_constant_info_val(constant_info const & d) {
return mk_vm_constructor(0, to_obj(d.get_name()), to_obj(d.get_univ_params()), to_obj(d.get_type()));
}
unsigned constant_info_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
constant_info const & d = to_constant_info(o);
switch (d.kind()) {
case constant_info_kind::Definition:
data.push_back(mk_vm_constructor(0, mk_constant_info_val(d), to_obj(d.get_value()), to_obj(d.get_hints()), mk_vm_bool(d.is_meta())));
break;
case constant_info_kind::Axiom:
data.push_back(mk_vm_constructor(0, mk_constant_info_val(d), mk_vm_bool(d.is_meta())));
break;
case constant_info_kind::Theorem:
data.push_back(mk_vm_constructor(0, mk_constant_info_val(d), to_obj(d.get_value())));
break;
case constant_info_kind::Quot: lean_unreachable(); // TODO(Leo):
case constant_info_kind::Inductive: lean_unreachable(); // TODO(Leo):
case constant_info_kind::Constructor: lean_unreachable(); // TODO(Leo):
case constant_info_kind::Recursor: lean_unreachable(); // TODO(Leo):
}
return static_cast<unsigned>(d.kind());
}
/*
/- Instantiate a universe polymorphic constant_info type with the given universes. -/
meta_constant constant_info.instantiate_type_univ_params : constant_info → list level → option expr
*/
vm_obj constant_info_instantiate_type_univ_params(vm_obj const & _d, vm_obj const & _ls) {
constant_info const & d = to_constant_info(_d);
levels ls = to_levels(_ls);
if (d.get_num_univ_params() != length(ls))
return mk_vm_none();
else
return mk_vm_some(to_obj(instantiate_type_univ_params(d, ls)));
}
/*
/- Instantiate a universe polymorphic constant_info type with the given universes. -/
meta_constant constant_info.instantiate_value_univ_params : constant_info → list level → option expr
*/
vm_obj constant_info_instantiate_value_univ_params(vm_obj const & _d, vm_obj const & _ls) {
constant_info const & d = to_constant_info(_d);
levels ls = to_levels(_ls);
if (!d.has_value() || d.get_num_univ_params() != length(ls))
return mk_vm_none();
else
return mk_vm_some(to_obj(instantiate_value_univ_params(d, ls)));
}
void initialize_vm_declaration() {
DECLARE_VM_BUILTIN(name({"lean", "constant_info", "defn_info"}), constant_info_defn);
DECLARE_VM_BUILTIN(name({"lean", "constant_info", "thm_info"}), constant_info_thm);
DECLARE_VM_BUILTIN(name({"lean", "constant_info", "axiom_info"}), constant_info_ax);
DECLARE_VM_BUILTIN(name({"lean", "constant_info", "instantiate_type_univ_params"}), constant_info_instantiate_type_univ_params);
DECLARE_VM_BUILTIN(name({"lean", "constant_info", "instantiate_value_univ_params"}), constant_info_instantiate_value_univ_params);
DECLARE_VM_CASES_BUILTIN(name({"lean", "constant_info", "cases_on"}), constant_info_cases_on);
}
void finalize_vm_declaration() {
}
}

21
src/library/vm/vm_declaration.h
View file

@ -1,21 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/vm/vm.h"
#include "kernel/declaration.h"
namespace lean {
bool is_declaration(vm_obj const & o);
declaration const & to_declaration(vm_obj const & o);
vm_obj to_obj(declaration const & n);
bool is_constant_info(vm_obj const & o);
constant_info const & to_constant_info(vm_obj const & o);
vm_obj to_obj(constant_info const & n);
void initialize_vm_declaration();
void finalize_vm_declaration();
}

88
src/library/vm/vm_exceptional.cpp
View file

@ -1,88 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/kernel_exception.h"
#include "library/trace.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_options.h"
#include "library/vm/vm_format.h"
namespace lean {
struct vm_throwable : public vm_external {
std::exception_ptr m_val;
vm_throwable(std::exception_ptr const & ex):m_val(ex) {}
virtual ~vm_throwable() {}
virtual void dealloc() override { delete this; }
virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_throwable(m_val); }
virtual vm_external * clone(vm_clone_fn const &) override { return new vm_throwable(m_val); }
};
std::exception_ptr const & to_throwable(vm_obj const & o) {
lean_vm_check(dynamic_cast<vm_throwable*>(to_external(o)));
return static_cast<vm_throwable*>(to_external(o))->m_val;
}
vm_obj to_obj(std::exception_ptr const & ex) {
return mk_vm_external(new vm_throwable(ex));
}
/** Implement two different signatures:
1) throwable -> options -> format
2) throwable -> unit -> format */
vm_obj throwable_to_format(vm_obj const & _ex, vm_obj const & _opts) {
std::exception_ptr const & ex = to_throwable(_ex);
if (!ex)
return to_obj(format("null-exception"));
try {
std::rethrow_exception(ex);
} catch (ext_exception & ex) {
if (is_simple(_opts)) {
io_state_stream ios = tout();
formatter fmt = ios.get_formatter();
return to_obj(ex.pp(fmt));
} else {
options opts = to_options(_opts);
scope_trace_env scope1(opts);
io_state_stream ios = tout();
formatter fmt = ios.get_formatter();
return to_obj(ex.pp(fmt));
}
} catch (formatted_exception & ex) {
return to_obj(ex.pp());
} catch (std::exception & ex) {
return to_obj(format(ex.what()));
} catch (...) {
return to_obj(format("unknown-exception"));
}
}
static unsigned g_throwable_to_format_fun_idx = -1;
unsigned get_throwable_to_format_fun_idx() {
return g_throwable_to_format_fun_idx;
}
vm_obj mk_vm_exceptional_success(vm_obj const & a) {
return mk_vm_constructor(0, a);
}
vm_obj mk_vm_exceptional_exception(std::exception_ptr const & ex) {
vm_obj _ex = to_obj(ex);
return mk_vm_constructor(1, mk_vm_closure(g_throwable_to_format_fun_idx, 1, &_ex));
}
void initialize_vm_exceptional() {
DECLARE_VM_BUILTIN("_throwable_to_format", throwable_to_format);
}
void finalize_vm_exceptional() {
}
void initialize_vm_exceptional_builtin_idxs() {
g_throwable_to_format_fun_idx = *get_vm_builtin_idx(name("_throwable_to_format"));
}
}

21
src/library/vm/vm_exceptional.h
View file

@ -1,21 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "runtime/exception.h"
#include "library/vm/vm.h"
namespace lean {
/* Convert exception into vm_exception */
vm_obj to_obj(std::exception_ptr const & ex);
/* Return fun_idx for vm_exception -> options -> format */
unsigned get_throwable_to_format_fun_idx();
vm_obj mk_vm_exceptional_success(vm_obj const & a);
vm_obj mk_vm_exceptional_exception(std::exception_ptr const & ex);
void initialize_vm_exceptional();
void finalize_vm_exceptional();
void initialize_vm_exceptional_builtin_idxs();
}

353
src/library/vm/vm_expr.cpp
View file

@ -1,353 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include <iostream>
#include "kernel/expr.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_fn.h"
#include "library/locals.h"
#include "library/sorry.h"
#include "library/util.h"
#include "library/expr_lt.h"
#include "library/deep_copy.h"
#include "library/comp_val.h"
#include "library/annotation.h"
#include "library/quote.h"
#include "library/string.h"
#include "library/vm/vm.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_format.h"
#include "library/vm/vm_options.h"
#include "library/vm/vm_option.h"
#include "library/vm/vm_level.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_pos_info.h"
#include "library/compiler/simp_inductive.h"
#include "library/compiler/nat_value.h"
namespace lean {
struct vm_expr : public vm_external {
expr m_val;
vm_expr(expr const & v):m_val(v) {}
virtual ~vm_expr() {}
virtual void dealloc() override { delete this; }
virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_expr(m_val); }
virtual vm_external * clone(vm_clone_fn const &) override { return new vm_expr(m_val); }
};
bool is_expr(vm_obj const & o) {
return is_external(o) && dynamic_cast<vm_expr*>(to_external(o));
}
expr const & to_expr(vm_obj const & o) {
lean_vm_check(dynamic_cast<vm_expr*>(to_external(o)));
return static_cast<vm_expr*>(to_external(o))->m_val;
}
vm_obj to_obj(expr const & e) {
return mk_vm_external(new vm_expr(e));
}
vm_obj to_obj(optional<expr> const & e) {
return e ? mk_vm_some(to_obj(*e)) : mk_vm_none();
}
binder_info to_binder_info(vm_obj const & o) {
lean_assert(is_simple(o));
return static_cast<binder_info>(cidx(o));
}
vm_obj to_obj(binder_info bi) {
return mk_vm_simple(static_cast<unsigned>(bi));
}
// The expr_bvar_intro function has an _intro suffix so that it doesn't clash
// with the expr_bvar class. This confuses GDB's python interface. The other
// introduction rules have the suffix for the same reason.
vm_obj expr_bvar_intro(vm_obj const & n) {
return to_obj(mk_bvar(nat(vm_nat_to_mpz1(n))));
}
vm_obj expr_sort_intro(vm_obj const & l) {
return to_obj(mk_sort(to_level(l)));
}
vm_obj expr_lit_intro(vm_obj const & l) {
switch (cidx(l)) {
case 0:
return to_obj(mk_lit(literal(to_string(cfield(l, 0)).c_str())));
case 1:
return to_obj(mk_lit(literal(vm_nat_to_mpz1(cfield(l, 0)))));
}
lean_unreachable();
}
vm_obj expr_const_intro(vm_obj const & n, vm_obj const & ls) {
return to_obj(mk_constant(to_name(n), to_levels(ls)));
}
vm_obj expr_mvar_intro(vm_obj const & n, vm_obj const & t) {
return to_obj(mk_metavar(to_name(n), to_expr(t)));
}
vm_obj expr_fvar_const_intro(vm_obj const & n) {
return to_obj(mk_local(to_name(n), to_name(n), expr(), mk_binder_info()));
}
vm_obj expr_app_intro(vm_obj const & f, vm_obj const & a) {
return to_obj(mk_app(to_expr(f), to_expr(a)));
}
vm_obj expr_lam_intro(vm_obj const & n, vm_obj const & bi, vm_obj const & t, vm_obj const & b) {
return to_obj(mk_lambda(to_name(n), to_expr(t), to_expr(b), to_binder_info(bi)));
}
vm_obj expr_pi_intro(vm_obj const & n, vm_obj const & bi, vm_obj const & t, vm_obj const & b) {
return to_obj(mk_pi(to_name(n), to_expr(t), to_expr(b), to_binder_info(bi)));
}
vm_obj expr_elet_intro(vm_obj const & n, vm_obj const & t, vm_obj const & v, vm_obj const & b) {
return to_obj(mk_let(to_name(n), to_expr(t), to_expr(v), to_expr(b)));
}
/*
inductive data_value
| of_string (v : string)
| of_nat (v : nat)
| of_bool (v : bool)
| of_name (v : name)
*/
vm_obj to_obj(data_value const & d) {
switch (d.kind()) {
case data_value_kind::String: return mk_vm_constructor(0, to_obj(d.get_string().to_std_string()));
case data_value_kind::Nat: return mk_vm_constructor(1, mk_vm_nat(d.get_nat().to_mpz()));
case data_value_kind::Bool: return mk_vm_constructor(2, mk_vm_bool(d.get_bool()));
case data_value_kind::Name: return mk_vm_constructor(3, to_obj(d.get_name()));
}
lean_unreachable();
}
vm_obj to_obj(kvmap const & m) {
buffer<vm_obj> objs;
for (pair_ref<name, data_value> const & p : m) {
objs.push_back(mk_vm_pair(to_obj(p.fst()), to_obj(p.snd())));
}
return to_obj(objs);
}
unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
expr const & e = to_expr(o);
switch (e.kind()) {
case expr_kind::BVar:
data.push_back(mk_vm_nat(bvar_idx(e).to_mpz()));
break;
case expr_kind::Sort:
data.push_back(to_obj(sort_level(e)));
break;
case expr_kind::Const:
data.push_back(to_obj(const_name(e)));
data.push_back(to_obj(const_levels(e)));
break;
case expr_kind::MVar:
data.push_back(to_obj(mvar_name(e)));
data.push_back(to_obj(mvar_type(e)));
break;
case expr_kind::FVar:
data.push_back(to_obj(fvar_name(e)));
break;
case expr_kind::App:
data.push_back(to_obj(app_fn(e)));
data.push_back(to_obj(app_arg(e)));
break;
case expr_kind::Lambda:
case expr_kind::Pi:
data.push_back(to_obj(binding_name(e)));
data.push_back(to_obj(binding_info(e)));
data.push_back(to_obj(binding_domain(e)));
data.push_back(to_obj(binding_body(e)));
break;
case expr_kind::Let:
data.push_back(to_obj(let_name(e)));
data.push_back(to_obj(let_type(e)));
data.push_back(to_obj(let_value(e)));
data.push_back(to_obj(let_body(e)));
break;
case expr_kind::Lit:
switch (lit_value(e).kind()) {
case literal_kind::String:
data.push_back(mk_vm_constructor(0, to_obj(std::string(lit_value(e).get_string().to_std_string()))));
break;
case literal_kind::Nat:
data.push_back(mk_vm_constructor(1, mk_vm_nat(lit_value(e).get_nat().to_mpz())));
break;
}
break;
case expr_kind::MData:
data.push_back(to_obj(mdata_data(e)));
data.push_back(to_obj(mdata_expr(e)));
break;
case expr_kind::Proj:
data.push_back(to_obj(proj_idx(e)));
data.push_back(to_obj(proj_expr(e)));
break;
case expr_kind::Quote:
data.push_back(mk_vm_bool(quote_is_reflected(e)));
data.push_back(to_obj(quote_value(e)));
break;
}
return static_cast<unsigned>(e.kind());
}
vm_obj expr_has_decidable_eq(vm_obj const & o1, vm_obj const & o2) {
return mk_vm_bool(is_bi_equal(to_expr(o1), to_expr(o2)));
}
vm_obj expr_alpha_eqv(vm_obj const & o1, vm_obj const & o2) {
return mk_vm_bool(to_expr(o1) == to_expr(o2));
}
vm_obj expr_to_string(vm_obj const & l) {
std::ostringstream out;
out << to_expr(l);
return to_obj(out.str());
}
vm_obj expr_lt(vm_obj const & o1, vm_obj const & o2) {
return mk_vm_bool(is_lt(to_expr(o1), to_expr(o2), true));
}
vm_obj expr_lex_lt(vm_obj const & o1, vm_obj const & o2) {
return mk_vm_bool(is_lt(to_expr(o1), to_expr(o2), false));
}
vm_obj expr_fold(vm_obj const &, vm_obj const & e, vm_obj const & a, vm_obj const & fn) {
vm_obj r = a;
for_each(to_expr(e), [&](expr const & o, unsigned d) {
r = invoke(fn, to_obj(o), mk_vm_nat(d), r);
return true;
});
return r;
}
vm_obj expr_has_bvar_idx(vm_obj const & e, vm_obj const & u) {
if (auto n = try_to_unsigned(u)) {
return mk_vm_bool(has_loose_bvar(to_expr(e), *n));
} else {
return mk_vm_false();
}
}
vm_obj expr_hash(vm_obj const & e) {
unsigned r = hash(to_expr(e)) % LEAN_VM_MAX_SMALL_NAT;
return mk_vm_simple(r); // make sure it is a simple value
}
vm_obj expr_get_nat_value(vm_obj const & o) {
expr e = to_expr(o);
if (is_nat_value(e)) {
auto n = mk_vm_nat(get_nat_value_value(e));
return mk_vm_constructor(1, { n });
} else {
return mk_vm_simple(0);
}
}
vm_obj expr_collect_univ_params(vm_obj const & o) {
names param_list;
collect_univ_params(to_expr(o), name_set()).for_each(
[&] (name const & n) { param_list = cons(n, param_list); });
return to_obj(param_list);
}
// TODO(Leo): move to a different file
vm_obj vm_mk_nat_val_ne_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_nat_val_ne_proof(to_expr(a), to_expr(b)));
}
vm_obj vm_mk_nat_val_lt_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_nat_val_lt_proof(to_expr(a), to_expr(b)));
}
vm_obj vm_mk_nat_val_le_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_nat_val_le_proof(to_expr(a), to_expr(b)));
}
vm_obj vm_mk_fin_val_ne_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_fin_val_ne_proof(to_expr(a), to_expr(b)));
}
vm_obj vm_mk_char_val_ne_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_char_val_ne_proof(to_expr(a), to_expr(b)));
}
vm_obj vm_mk_string_val_ne_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_string_val_ne_proof(to_expr(a), to_expr(b)));
}
vm_obj expr_subst(vm_obj const & _e1, vm_obj const & _e2) {
expr const & e1 = to_expr(_e1);
expr const & e2 = to_expr(_e2);
if (is_lambda(e1)) {
return to_obj(instantiate(binding_body(e1), e2));
} else {
return to_obj(e1);
}
}
vm_obj reflect_expr(vm_obj const & e) {
return to_obj(mk_elaborated_expr_quote(to_expr(e)));
}
vm_obj reflect_string(vm_obj const & s) {
return to_obj(from_string(to_string(s)));
}
void initialize_vm_expr() {
DECLARE_VM_BUILTIN(name({"lean", "expr", "var"}), expr_bvar_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "lit"}), expr_lit_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "fvar"}), expr_fvar_const_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "sort"}), expr_sort_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "const"}), expr_const_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "mvar"}), expr_mvar_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "app"}), expr_app_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "lam"}), expr_lam_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "pi"}), expr_pi_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "elet"}), expr_elet_intro);
DECLARE_VM_BUILTIN(name({"lean", "expr", "has_decidable_eq"}), expr_has_decidable_eq);
DECLARE_VM_BUILTIN(name({"lean", "expr", "alpha_eqv"}), expr_alpha_eqv);
DECLARE_VM_BUILTIN(name({"lean", "expr", "to_string"}), expr_to_string);
DECLARE_VM_BUILTIN(name({"lean", "expr", "lt"}), expr_lt);
DECLARE_VM_BUILTIN(name({"lean", "expr", "lex_lt"}), expr_lex_lt);
DECLARE_VM_BUILTIN(name({"lean", "expr", "fold"}), expr_fold);
DECLARE_VM_BUILTIN(name({"lean", "expr", "subst"}), expr_subst);
DECLARE_VM_BUILTIN(name({"lean", "expr", "has_bvar_idx"}), expr_has_bvar_idx);
DECLARE_VM_BUILTIN(name({"lean", "expr", "hash"}), expr_hash);
DECLARE_VM_CASES_BUILTIN(name({"lean", "expr", "cases_on"}), expr_cases_on);
DECLARE_VM_BUILTIN(name("string", "reflect"), reflect_string);
DECLARE_VM_BUILTIN(name({"lean", "expr", "reflect"}), reflect_expr);
DECLARE_VM_BUILTIN(name("mk_nat_val_ne_proof"), vm_mk_nat_val_ne_proof);
DECLARE_VM_BUILTIN(name("mk_nat_val_lt_proof"), vm_mk_nat_val_lt_proof);
DECLARE_VM_BUILTIN(name("mk_nat_val_le_proof"), vm_mk_nat_val_le_proof);
DECLARE_VM_BUILTIN(name("mk_fin_val_ne_proof"), vm_mk_fin_val_ne_proof);
DECLARE_VM_BUILTIN(name("mk_char_val_ne_proof"), vm_mk_char_val_ne_proof);
DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"), vm_mk_string_val_ne_proof);
}
void finalize_vm_expr() {
}
void initialize_vm_expr_builtin_idxs() {
}
}

21
src/library/vm/vm_expr.h
View file

@ -1,21 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/vm/vm.h"
#include "kernel/expr.h"
namespace lean {
binder_info to_binder_info(vm_obj const & o);
vm_obj to_obj(binder_info bi);
bool is_expr(vm_obj const & o);
expr const & to_expr(vm_obj const & o);
vm_obj to_obj(expr const & e);
vm_obj to_obj(optional<expr> const & e);
void initialize_vm_expr();
void finalize_vm_expr();
void initialize_vm_expr_builtin_idxs();
}

101
src/library/vm/vm_level.cpp
View file

@ -1,101 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include <iostream>
#include "kernel/level.h"
#include "library/vm/vm.h"
#include "library/vm/vm_string.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_format.h"
#include "library/vm/vm_options.h"
namespace lean {
struct vm_level : public vm_external {
level m_val;
vm_level(level const & v):m_val(v) {}
virtual ~vm_level() {}
virtual void dealloc() override { delete this; }
virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_level(m_val); }
virtual vm_external * clone(vm_clone_fn const &) override { return new vm_level(m_val); }
};
bool is_level(vm_obj const & o) {
return is_external(o) && dynamic_cast<vm_level*>(to_external(o));
}
level const & to_level(vm_obj const & o) {
lean_vm_check(dynamic_cast<vm_level*>(to_external(o)));
return static_cast<vm_level*>(to_external(o))->m_val;
}
vm_obj to_obj(level const & n) {
return mk_vm_external(new vm_level(n));
}
vm_obj level_zero() {
return to_obj(mk_level_zero());
}
vm_obj level_succ(vm_obj const & o) {
return to_obj(mk_succ(to_level(o)));
}
vm_obj level_max(vm_obj const & o1, vm_obj const & o2) {
return to_obj(mk_max_core(to_level(o1), to_level(o2)));
}
vm_obj level_imax(vm_obj const & o1, vm_obj const & o2) {
return to_obj(mk_imax_core(to_level(o1), to_level(o2)));
}
vm_obj level_param(vm_obj const & n) {
return to_obj(mk_univ_param(to_name(n)));
}
vm_obj level_mvar(vm_obj const & n) {
return to_obj(mk_univ_mvar(to_name(n)));
}
unsigned level_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
level const & l = to_level(o);
switch (l.kind()) {
case level_kind::Zero:
break;
case level_kind::Succ:
data.push_back(to_obj(succ_of(l)));
break;
case level_kind::Max:
data.push_back(to_obj(max_lhs(l)));
data.push_back(to_obj(max_rhs(l)));
break;
case level_kind::IMax:
data.push_back(to_obj(imax_lhs(l)));
data.push_back(to_obj(imax_rhs(l)));
break;
case level_kind::Param:
data.push_back(to_obj(param_id(l)));
break;
case level_kind::MVar:
data.push_back(to_obj(mvar_id(l)));
break;
}
return static_cast<unsigned>(l.kind());
}
void initialize_vm_level() {
DECLARE_VM_BUILTIN(name({"lean", "level", "zero"}), level_zero);
DECLARE_VM_BUILTIN(name({"lean", "level", "succ"}), level_succ);
DECLARE_VM_BUILTIN(name({"lean", "level", "max"}), level_max);
DECLARE_VM_BUILTIN(name({"lean", "level", "imax"}), level_imax);
DECLARE_VM_BUILTIN(name({"lean", "level", "param"}), level_param);
DECLARE_VM_BUILTIN(name({"lean", "level", "mvar"}), level_mvar);
DECLARE_VM_CASES_BUILTIN(name({"lean", "level", "cases_on"}), level_cases_on);
}
void finalize_vm_level() {
}
}

17
src/library/vm/vm_level.h
View file

@ -1,17 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/vm/vm.h"
#include "kernel/level.h"
namespace lean {
bool is_level(vm_obj const & o);
level const & to_level(vm_obj const & o);
vm_obj to_obj(level const & n);
void initialize_vm_level();
void finalize_vm_level();
}

15
src/library/vm/vm_list.cpp
View file

@ -6,8 +6,6 @@ Author: Leonardo de Moura
*/
#include "library/vm/vm_name.h"
#include "library/vm/vm_nat.h"
#include "library/vm/vm_level.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_list.h"
namespace lean {
@ -42,14 +40,10 @@ vm_obj list_ref_to_obj(list_ref<A> const & l) {
}
vm_obj to_obj(names const & ls) { return list_ref_to_obj(ls); }
vm_obj to_obj(levels const & ls) { return list_ref_to_obj(ls); }
vm_obj to_obj(list<expr> const & ls) { return list_to_obj(ls); }
vm_obj to_obj(list<list<expr>> const & ls) { return list_to_obj(ls); }
vm_obj to_obj(buffer<name> const & ls) { return to_obj(names(ls)); }
vm_obj to_obj(buffer<level> const & ls) { return to_obj(levels(ls)); }
vm_obj to_obj(buffer<expr> const & ls) { return to_obj(to_list(ls)); }
#define MK_TO_LIST(A, ToA) \
list<A> to_list_ ## A(vm_obj const & o) { \
@ -76,11 +70,8 @@ static list_ref<A> to_list_ref_ ## A(vm_obj const & o) { \
}
MK_TO_LIST_REF(name, to_name)
MK_TO_LIST_REF(level, to_level)
MK_TO_LIST(expr, to_expr)
names to_names(vm_obj const & o) { return to_list_ref_name(o); }
levels to_levels(vm_obj const & o) { return to_list_ref_level(o); }
#define MK_TO_BUFFER(A, ToA) \
void to_buffer_ ## A(vm_obj const & o, buffer<A> & r) { \
@ -96,8 +87,6 @@ void to_buffer_ ## A(vm_obj const & o, buffer<A> & r) { \
}
MK_TO_BUFFER(name, to_name)
MK_TO_BUFFER(level, to_level)
MK_TO_BUFFER(expr, to_expr)
template<typename A>
unsigned list_cases_on_core(list<A> const & l, buffer<vm_obj> & data) {
@ -130,10 +119,6 @@ unsigned list_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
} else {
if (auto l = dynamic_cast<vm_list_ref<name>*>(to_external(o))) {
return list_ref_cases_on_core(l->m_val, data);
} else if (auto l = dynamic_cast<vm_list<expr>*>(to_external(o))) {
return list_cases_on_core(l->m_val, data);
} else if (auto l = dynamic_cast<vm_list_ref<level>*>(to_external(o))) {
return list_ref_cases_on_core(l->m_val, data);
} else {
lean_unreachable();
}

51
src/library/vm/vm_pexpr.cpp
View file

@ -1,51 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/instantiate.h"
#include "library/placeholder.h"
#include "library/explicit.h"
#include "library/quote.h"
#include "library/vm/vm.h"
#include "library/vm/vm_expr.h"
#include "library/vm/vm_name.h"
#include "library/vm/vm_list.h"
#include "library/vm/vm_option.h"
#include "frontends/lean/util.h"
#include "frontends/lean/structure_instance.h"
namespace lean {
vm_obj pexpr_of_expr(vm_obj const & e) {
return to_obj(mk_as_is(to_expr(e)));
}
vm_obj pexpr_to_expr(vm_obj const & e) {
return e;
}
vm_obj pexpr_reflect(vm_obj const & e) {
return to_obj(mk_pexpr_quote_and_substs(to_expr(e), /* is_strict */ false));
}
vm_obj pexpr_subst(vm_obj const & _e1, vm_obj const & _e2) {
expr const & e1 = to_expr(_e1);
expr const & e2 = to_expr(_e2);
if (is_lambda(e1)) {
return to_obj(instantiate(binding_body(e1), e2));
} else {
return to_obj(e1);
}
}
void initialize_vm_pexpr() {
DECLARE_VM_BUILTIN(name({"pexpr", "of_expr"}), pexpr_of_expr);
DECLARE_VM_BUILTIN(name({"pexpr", "to_expr"}), pexpr_to_expr);
DECLARE_VM_BUILTIN(name({"pexpr", "reflect"}), pexpr_reflect);
DECLARE_VM_BUILTIN(name({"pexpr", "subst"}), pexpr_subst);
}
void finalize_vm_pexpr() {
}
}

11
src/library/vm/vm_pexpr.h
View file

@ -1,11 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
namespace lean {
void initialize_vm_pexpr();
void finalize_vm_pexpr();
}