From 2d22bb8ea2d2a87227a0ca3a7e27a5ca04802f68 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 May 2015 19:09:44 -0700 Subject: [PATCH] feat(frontends/lean/builtin_cmds): do not unfold proofs in the eval command In the future, we should probably add an option for unfolding proofs. --- src/frontends/lean/builtin_cmds.cpp | 4 ++- src/library/normalize.cpp | 43 +++++++++++++++++----------- src/library/normalize.h | 2 +- tests/lean/rateval.lean | 6 ++++ tests/lean/rateval.lean.expected.out | 1 + tests/lean/run/rat_rfl.lean | 7 +++++ 6 files changed, 45 insertions(+), 18 deletions(-) create mode 100644 tests/lean/rateval.lean create mode 100644 tests/lean/rateval.lean.expected.out create mode 100644 tests/lean/run/rat_rfl.lean diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 9fbd645fe..d946d41fa 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -547,7 +547,9 @@ environment eval_cmd(parser & p) { r = tc->whnf(e).first; } else { type_checker tc(p.env()); - r = normalize(tc, ls, e); + bool eta = false; + bool eval_nested_prop = false; + r = normalize(tc, ls, e, eta, eval_nested_prop); } flycheck_information info(p.regular_stream()); if (info.enabled()) { diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 63ef05469..df0f6803c 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -171,6 +171,9 @@ class normalize_fn { bool m_save_cnstrs; constraint_seq m_cnstrs; bool m_use_eta; + bool m_eval_nested_prop; + + environment const & env() const { return m_tc.env(); } expr normalize_binding(expr const & e) { expr d = normalize(binding_domain(e)); @@ -182,19 +185,19 @@ class normalize_fn { optional has_unfold_c_hint(expr const & f) { if (!is_constant(f)) return optional(); - return ::lean::has_unfold_c_hint(m_tc.env(), const_name(f)); + return ::lean::has_unfold_c_hint(env(), const_name(f)); } bool has_unfold_f_hint(expr const & f) { - return is_constant(f) && ::lean::has_unfold_f_hint(m_tc.env(), const_name(f)); + return is_constant(f) && ::lean::has_unfold_f_hint(env(), const_name(f)); } optional is_constructor_like(expr const & e) { - if (is_constructor_app(m_tc.env(), e)) + if (is_constructor_app(env(), e)) return some_expr(e); expr const & f = get_app_fn(e); - if (is_constant(f) && has_constructor_hint(m_tc.env(), const_name(f))) { - if (auto r = unfold_term(m_tc.env(), e)) + if (is_constant(f) && has_constructor_hint(env(), const_name(f))) { + if (auto r = unfold_term(env(), e)) return r; else return some_expr(e); @@ -211,7 +214,7 @@ class normalize_fn { expr new_app = mk_rev_app(f, args); if (is_rec) return some_expr(normalize(new_app)); - else if (optional r = unfold_app(m_tc.env(), new_app)) + else if (optional r = unfold_app(env(), new_app)) return some_expr(normalize(*r)); } } @@ -231,14 +234,16 @@ class normalize_fn { bool modified = false; expr f = get_app_rev_args(e, args); for (expr & a : args) { - expr new_a = normalize(a); + expr new_a = a; + if (m_eval_nested_prop || !m_tc.is_prop(m_tc.infer(a).first).first) + new_a = normalize(a); if (new_a != a) modified = true; a = new_a; } if (has_unfold_f_hint(f)) { if (!is_pi(m_tc.whnf(m_tc.infer(e).first).first)) { - if (optional r = unfold_app(m_tc.env(), mk_rev_app(f, args))) + if (optional r = unfold_app(env(), mk_rev_app(f, args))) return normalize(*r); } } @@ -247,7 +252,7 @@ class normalize_fn { return *r; } if (is_constant(f)) { - if (auto idx = inductive::get_elim_major_idx(m_tc.env(), const_name(f))) { + if (auto idx = inductive::get_elim_major_idx(env(), const_name(f))) { if (auto r = unfold_recursor_major(f, *idx, args)) return *r; } @@ -255,7 +260,7 @@ class normalize_fn { if (!modified) return e; expr r = mk_rev_app(f, args); - if (is_constant(f) && inductive::is_elim_rule(m_tc.env(), const_name(f))) { + if (is_constant(f) && inductive::is_elim_rule(env(), const_name(f))) { return normalize(r); } else { return r; @@ -309,14 +314,20 @@ class normalize_fn { } public: - normalize_fn(type_checker & tc, bool save, bool eta): + normalize_fn(type_checker & tc, bool save, bool eta, bool nested_prop = true): m_tc(tc), m_ngen(m_tc.mk_ngen()), m_pred([](expr const &) { return true; }), - m_save_cnstrs(save), m_use_eta(eta) {} + m_save_cnstrs(save), m_use_eta(eta), m_eval_nested_prop(nested_prop) { + if (!is_standard(env())) + m_eval_nested_prop = true; + } - normalize_fn(type_checker & tc, std::function const & fn, bool eta): // NOLINT + normalize_fn(type_checker & tc, std::function const & fn, bool eta, bool nested_prop = true): // NOLINT m_tc(tc), m_ngen(m_tc.mk_ngen()), - m_pred(fn), m_save_cnstrs(true), m_use_eta(eta) {} + m_pred(fn), m_save_cnstrs(true), m_use_eta(eta), m_eval_nested_prop(nested_prop) { + if (!is_standard(env())) + m_eval_nested_prop = true; + } expr operator()(expr const & e) { m_cnstrs = constraint_seq(); @@ -350,9 +361,9 @@ expr normalize(type_checker & tc, expr const & e, bool eta) { return normalize_fn(tc, save_cnstrs, eta)(e); } -expr normalize(type_checker & tc, level_param_names const & ls, expr const & e, bool eta) { +expr normalize(type_checker & tc, level_param_names const & ls, expr const & e, bool eta, bool eval_nested_prop) { bool save_cnstrs = false; - return normalize_fn(tc, save_cnstrs, eta)(ls, e); + return normalize_fn(tc, save_cnstrs, eta, eval_nested_prop)(ls, e); } expr normalize(type_checker & tc, expr const & e, constraint_seq & cs, bool eta) { diff --git a/src/library/normalize.h b/src/library/normalize.h index 6cc20117d..238c54bbc 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -19,7 +19,7 @@ expr normalize(environment const & env, level_param_names const & ls, expr const /** \brief Similar to expr normalize(environment const & env, expr const & e), but uses the converter associated with \c tc. */ expr normalize(type_checker & tc, expr const & e, bool eta = false); -expr normalize(type_checker & tc, level_param_names const & ls, expr const & e, bool eta = false); +expr normalize(type_checker & tc, level_param_names const & ls, expr const & e, bool eta = false, bool eval_nested_prop = true); /** \brief Return the \c e normal form with respect to \c tc, and store generated constraints into \c cs. */ diff --git a/tests/lean/rateval.lean b/tests/lean/rateval.lean new file mode 100644 index 000000000..1133b32c6 --- /dev/null +++ b/tests/lean/rateval.lean @@ -0,0 +1,6 @@ +import data.rat +open nat int rat + +attribute rat.of_int [coercion] + +eval (8 * 6⁻¹) + 1 diff --git a/tests/lean/rateval.lean.expected.out b/tests/lean/rateval.lean.expected.out new file mode 100644 index 000000000..5527fa089 --- /dev/null +++ b/tests/lean/rateval.lean.expected.out @@ -0,0 +1 @@ +quot.mk (prerat.mk 14 6 (mul_denom_pos (prerat.mul (prerat.of_int 8) (prerat.inv (prerat.of_int 6))) prerat.one)) diff --git a/tests/lean/run/rat_rfl.lean b/tests/lean/run/rat_rfl.lean new file mode 100644 index 000000000..068bc12b2 --- /dev/null +++ b/tests/lean/run/rat_rfl.lean @@ -0,0 +1,7 @@ +import data.rat +open rat + +attribute rat.of_int [coercion] + +example : 1 + 2⁻¹ + 3 = 3 + 2⁻¹ + 1⁻¹ := +rfl