From d334bb1fa7e45fbc049522ac13ab70b8af27f90e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Aug 2018 15:55:06 -0700 Subject: [PATCH] chore(*): remove more stuff --- library/init/meta/declaration.lean | 21 - library/init/meta/default.lean | 2 +- library/init/meta/exceptional.lean | 53 -- library/init/meta/expr.lean | 162 ----- library/init/meta/has_reflect.lean | 58 -- library/init/meta/interaction_monad.lean | 8 +- library/init/meta/level.lean | 9 - library/init/meta/pexpr.lean | 29 - library/init/meta/tactic.lean | 17 +- src/frontends/lean/builtin_exprs.cpp | 1 - src/frontends/lean/decl_util.cpp | 4 - src/frontends/lean/elaborator.cpp | 58 +- src/frontends/lean/inductive_cmds.cpp | 2 - src/frontends/lean/interactive.cpp | 1 - src/library/equations_compiler/elim_match.cpp | 1 - src/library/equations_compiler/wf_rec.cpp | 8 +- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/cases_tactic.cpp | 3 - src/library/tactic/clear_tactic.cpp | 2 - src/library/tactic/elaborate.cpp | 72 -- src/library/tactic/elaborate.h | 18 - src/library/tactic/induction_tactic.cpp | 1 - src/library/tactic/init_module.cpp | 3 - src/library/tactic/intro_tactic.cpp | 1 - src/library/tactic/kabstract.cpp | 1 - src/library/tactic/subst_tactic.cpp | 2 - src/library/tactic/tactic_state.cpp | 626 ------------------ src/library/tactic/tactic_state.h | 3 - src/library/vm/CMakeLists.txt | 3 +- src/library/vm/init_module.cpp | 17 - src/library/vm/interaction_state_imp.h | 19 +- src/library/vm/vm.cpp | 12 - src/library/vm/vm_declaration.cpp | 214 ------ src/library/vm/vm_declaration.h | 21 - src/library/vm/vm_exceptional.cpp | 88 --- src/library/vm/vm_exceptional.h | 21 - src/library/vm/vm_expr.cpp | 353 ---------- src/library/vm/vm_expr.h | 21 - src/library/vm/vm_level.cpp | 101 --- src/library/vm/vm_level.h | 17 - src/library/vm/vm_list.cpp | 15 - src/library/vm/vm_pexpr.cpp | 51 -- src/library/vm/vm_pexpr.h | 11 - 43 files changed, 19 insertions(+), 2113 deletions(-) delete mode 100644 library/init/meta/declaration.lean delete mode 100644 library/init/meta/exceptional.lean delete mode 100644 library/init/meta/expr.lean delete mode 100644 library/init/meta/has_reflect.lean delete mode 100644 library/init/meta/level.lean delete mode 100644 library/init/meta/pexpr.lean delete mode 100644 src/library/tactic/elaborate.cpp delete mode 100644 src/library/tactic/elaborate.h delete mode 100644 src/library/vm/vm_declaration.cpp delete mode 100644 src/library/vm/vm_declaration.h delete mode 100644 src/library/vm/vm_exceptional.cpp delete mode 100644 src/library/vm/vm_exceptional.h delete mode 100644 src/library/vm/vm_expr.cpp delete mode 100644 src/library/vm/vm_expr.h delete mode 100644 src/library/vm/vm_level.cpp delete mode 100644 src/library/vm/vm_level.h delete mode 100644 src/library/vm/vm_pexpr.cpp delete mode 100644 src/library/vm/vm_pexpr.h diff --git a/library/init/meta/declaration.lean b/library/init/meta/declaration.lean deleted file mode 100644 index c9e87eca9b..0000000000 --- a/library/init/meta/declaration.lean +++ /dev/null @@ -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 diff --git a/library/init/meta/default.lean b/library/init/meta/default.lean index cb085ef630..837eed3edd 100644 --- a/library/init/meta/default.lean +++ b/library/init/meta/default.lean @@ -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 diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean deleted file mode 100644 index 039f46933e..0000000000 --- a/library/init/meta/exceptional.lean +++ /dev/null @@ -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} diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean deleted file mode 100644 index e3b3fa4624..0000000000 --- a/library/init/meta/expr.lean +++ /dev/null @@ -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 diff --git a/library/init/meta/has_reflect.lean b/library/init/meta/has_reflect.lean deleted file mode 100644 index 5ed05e5ac9..0000000000 --- a/library/init/meta/has_reflect.lean +++ /dev/null @@ -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} := `(_) diff --git a/library/init/meta/interaction_monad.lean b/library/init/meta/interaction_monad.lean index 184923069d..351c69123e 100644 --- a/library/init/meta/interaction_monad.lean +++ b/library/init/meta/interaction_monad.lean @@ -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 diff --git a/library/init/meta/level.lean b/library/init/meta/level.lean deleted file mode 100644 index 1c6ff62801..0000000000 --- a/library/init/meta/level.lean +++ /dev/null @@ -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) diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean deleted file mode 100644 index 21b3907f87..0000000000 --- a/library/init/meta/pexpr.lean +++ /dev/null @@ -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⟩ diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 68dc57bae0..a82860209f 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -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 diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index d4d0dd7cde..7fa9e2dc72 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -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" diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 5cac5645b2..a27bde3819 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -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)) { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index f9c85d25e3..7f79b66e77 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -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 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 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"); diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 5061e5aefd..64917e03b8 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -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" diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index a25aa3fbd2..ce73fbab1f 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -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" diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 088a23e9ba..4cde04a0fe 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -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(R.m_counter_examples, [&] (list const & e) { return mk_app(fn, e); }); return { {fn}, counter_examples }; diff --git a/src/library/equations_compiler/wf_rec.cpp b/src/library/equations_compiler/wf_rec.cpp index 6207fb2003..811a74027e 100644 --- a/src/library/equations_compiler/wf_rec.cpp +++ b/src/library/equations_compiler/wf_rec.cpp @@ -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()); } + */ } } diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 2820d18be6..2e41ce4d2d 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -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) diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 8186fe1753..6e9fc76aee 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -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" diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index 6ad91a2f03..9f3f3143de 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -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 { diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp deleted file mode 100644 index 9534b69c53..0000000000 --- a/src/library/tactic/elaborate.cpp +++ /dev/null @@ -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 -#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 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 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 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; -} -} diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h deleted file mode 100644 index 89c6d63ef4..0000000000 --- a/src/library/tactic/elaborate.h +++ /dev/null @@ -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(); -} diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index c1389a81f1..c069688a13 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -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" diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index f693bcd897..3221efe99f 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -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(); diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp index 0e5d9c83e5..b4ea86d117 100644 --- a/src/library/tactic/intro_tactic.cpp +++ b/src/library/tactic/intro_tactic.cpp @@ -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 { diff --git a/src/library/tactic/kabstract.cpp b/src/library/tactic/kabstract.cpp index b7ddea95ea..6e74c49746 100644 --- a/src/library/tactic/kabstract.cpp +++ b/src/library/tactic/kabstract.cpp @@ -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" diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index ea30733791..190da89543 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -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" diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 5d17e2629d..f0f948dc80 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -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 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 mdecl = s.get_main_goal_decl(); - if (!mdecl) return tactic::mk_success(e0, s); - local_context lctx = mdecl->get_context(); - optional 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 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(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 g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(s); - local_context lctx = g->get_context(); - optional 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 g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(s); - local_context lctx = g->get_context(); - buffer 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 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 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 const & gs, tactic_state const & s) { - buffer 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 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 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 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 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 g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(s); - try { - pair 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 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 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 g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(s); - local_context lctx = g->get_context(); - if (optional lis = lctx.get_frozen_local_instances()) { - buffer 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); } diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index 0dcd56beb4..d095d2df08 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -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(); } diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt index 55d3b6b551..b88b1b4972 100644 --- a/src/library/vm/CMakeLists.txt +++ b/src/library/vm/CMakeLists.txt @@ -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) diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp index 459981fc6e..4dc347641b 100644 --- a/src/library/vm/init_module.cpp +++ b/src/library/vm/init_module.cpp @@ -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(); } diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h index db355e2436..7d7d44d705 100644 --- a/src/library/vm/interaction_state_imp.h +++ b/src/library/vm/interaction_state_imp.h @@ -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::update_exception_state(vm_obj const & ex, State } template -vm_obj interaction_monad::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; - 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::mk_exception(std::exception_ptr const &, State const &) { + // vm_exceptional has been deleted + lean_unreachable(); } template diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 4f27c95f2c..90dd564dd8 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -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()); diff --git a/src/library/vm/vm_declaration.cpp b/src/library/vm/vm_declaration.cpp deleted file mode 100644 index f113aacd09..0000000000 --- a/src/library/vm/vm_declaration.cpp +++ /dev/null @@ -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(to_external(o)); -} - -declaration const & to_declaration(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(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 & 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(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(to_external(o)); -} - -constant_info const & to_constant_info(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(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 & 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(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() { -} -} diff --git a/src/library/vm/vm_declaration.h b/src/library/vm/vm_declaration.h deleted file mode 100644 index dec3b350db..0000000000 --- a/src/library/vm/vm_declaration.h +++ /dev/null @@ -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(); -} diff --git a/src/library/vm/vm_exceptional.cpp b/src/library/vm/vm_exceptional.cpp deleted file mode 100644 index 4debb75532..0000000000 --- a/src/library/vm/vm_exceptional.cpp +++ /dev/null @@ -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(to_external(o))); - return static_cast(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")); -} -} diff --git a/src/library/vm/vm_exceptional.h b/src/library/vm/vm_exceptional.h deleted file mode 100644 index 7c7036bdd3..0000000000 --- a/src/library/vm/vm_exceptional.h +++ /dev/null @@ -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(); -} diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp deleted file mode 100644 index aa919b2cd5..0000000000 --- a/src/library/vm/vm_expr.cpp +++ /dev/null @@ -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 -#include -#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(to_external(o)); -} - -expr const & to_expr(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(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 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(cidx(o)); -} - -vm_obj to_obj(binder_info bi) { - return mk_vm_simple(static_cast(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 objs; - for (pair_ref 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 & 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(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() { -} -} diff --git a/src/library/vm/vm_expr.h b/src/library/vm/vm_expr.h deleted file mode 100644 index c5aaadb6db..0000000000 --- a/src/library/vm/vm_expr.h +++ /dev/null @@ -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 const & e); -void initialize_vm_expr(); -void finalize_vm_expr(); -void initialize_vm_expr_builtin_idxs(); -} diff --git a/src/library/vm/vm_level.cpp b/src/library/vm/vm_level.cpp deleted file mode 100644 index 2e1778f244..0000000000 --- a/src/library/vm/vm_level.cpp +++ /dev/null @@ -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 -#include -#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(to_external(o)); -} - -level const & to_level(vm_obj const & o) { - lean_vm_check(dynamic_cast(to_external(o))); - return static_cast(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 & 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(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() { -} -} diff --git a/src/library/vm/vm_level.h b/src/library/vm/vm_level.h deleted file mode 100644 index b34024d5c3..0000000000 --- a/src/library/vm/vm_level.h +++ /dev/null @@ -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(); -} diff --git a/src/library/vm/vm_list.cpp b/src/library/vm/vm_list.cpp index 0f270dee0a..e492c2d2fb 100644 --- a/src/library/vm/vm_list.cpp +++ b/src/library/vm/vm_list.cpp @@ -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 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 const & ls) { return list_to_obj(ls); } vm_obj to_obj(list> const & ls) { return list_to_obj(ls); } vm_obj to_obj(buffer const & ls) { return to_obj(names(ls)); } -vm_obj to_obj(buffer const & ls) { return to_obj(levels(ls)); } -vm_obj to_obj(buffer const & ls) { return to_obj(to_list(ls)); } #define MK_TO_LIST(A, ToA) \ list to_list_ ## A(vm_obj const & o) { \ @@ -76,11 +70,8 @@ static list_ref 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 & r) { \ @@ -96,8 +87,6 @@ void to_buffer_ ## A(vm_obj const & o, buffer & r) { \ } MK_TO_BUFFER(name, to_name) -MK_TO_BUFFER(level, to_level) -MK_TO_BUFFER(expr, to_expr) template unsigned list_cases_on_core(list const & l, buffer & data) { @@ -130,10 +119,6 @@ unsigned list_cases_on(vm_obj const & o, buffer & data) { } else { if (auto l = dynamic_cast*>(to_external(o))) { return list_ref_cases_on_core(l->m_val, data); - } else if (auto l = dynamic_cast*>(to_external(o))) { - return list_cases_on_core(l->m_val, data); - } else if (auto l = dynamic_cast*>(to_external(o))) { - return list_ref_cases_on_core(l->m_val, data); } else { lean_unreachable(); } diff --git a/src/library/vm/vm_pexpr.cpp b/src/library/vm/vm_pexpr.cpp deleted file mode 100644 index 070eaa01a3..0000000000 --- a/src/library/vm/vm_pexpr.cpp +++ /dev/null @@ -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() { -} -} diff --git a/src/library/vm/vm_pexpr.h b/src/library/vm/vm_pexpr.h deleted file mode 100644 index e843096e30..0000000000 --- a/src/library/vm/vm_pexpr.h +++ /dev/null @@ -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(); -}