From e85b1f1ac07fb8ce117f1e5d0f0c55fc7397ba7d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Feb 2014 15:56:54 -0800 Subject: [PATCH] feat(library/elaborator): expose elaborator configuration options Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend_elaborator.cpp | 26 +++++----- src/frontends/lean/frontend_elaborator.h | 4 +- src/frontends/lean/parser_cmds.cpp | 14 +++--- src/frontends/lean/parser_imp.cpp | 10 +++- src/frontends/lean/parser_imp.h | 9 ++++ src/library/elaborator/elaborator.cpp | 56 +++++++++++++++++++--- 6 files changed, 90 insertions(+), 29 deletions(-) diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 871d0fe6f..5ed76cb7c 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -426,12 +426,8 @@ class frontend_elaborator::imp { } }; - metavar_env elaborate_core() { - // std::stable_sort(m_ucs.begin(), m_ucs.end(), - // [](unification_constraint const & c1, unification_constraint const & c2) { - // return !is_choice(c1) && is_choice(c2); - // }); - elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data()); + metavar_env elaborate_core(options const & opts) { + elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data(), opts); return elb.next(); } @@ -442,7 +438,7 @@ public: m_normalizer(m_env) { } - std::pair elaborate(expr const & e) { + std::pair elaborate(expr const & e, options const & opts) { // std::cout << "Elaborate " << e << "\n"; clear(); expr new_e = preprocessor(*this)(e); @@ -453,14 +449,15 @@ public: // formatter fmt = mk_simple_formatter(); // std::cout << c.pp(fmt, options(), nullptr, false) << "\n"; // } - metavar_env new_menv = elaborate_core(); + metavar_env new_menv = elaborate_core(opts); return mk_pair(new_menv->instantiate_metavars(new_e), new_menv); } else { return mk_pair(new_e, metavar_env()); } } - std::tuple elaborate(name const & n, expr const & t, expr const & e) { + std::tuple elaborate(name const & n, expr const & t, expr const & e, + options const & opts) { // std::cout << "Elaborate " << t << " : " << e << "\n"; clear(); expr new_t = preprocessor(*this)(t); @@ -475,7 +472,7 @@ public: // formatter fmt = mk_simple_formatter(); // std::cout << c.pp(fmt, options(), nullptr, false) << "\n"; // } - metavar_env new_menv = elaborate_core(); + metavar_env new_menv = elaborate_core(opts); return std::make_tuple(new_menv->instantiate_metavars(new_t), new_menv->instantiate_metavars(new_e), new_menv); @@ -511,9 +508,12 @@ public: frontend_elaborator::frontend_elaborator(environment const & env):m_ptr(std::make_shared(env)) {} frontend_elaborator::~frontend_elaborator() {} -std::pair frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); } -std::tuple frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) { - return m_ptr->elaborate(n, t, e); +std::pair frontend_elaborator::operator()(expr const & e, options const & opts) { + return m_ptr->elaborate(e, opts); +} +std::tuple frontend_elaborator::operator()(name const & n, expr const & t, expr const & e, + options const & opts) { + return m_ptr->elaborate(n, t, e, opts); } expr const & frontend_elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); } void frontend_elaborator::clear() { m_ptr->clear(); } diff --git a/src/frontends/lean/frontend_elaborator.h b/src/frontends/lean/frontend_elaborator.h index e04107e53..f6219e478 100644 --- a/src/frontends/lean/frontend_elaborator.h +++ b/src/frontends/lean/frontend_elaborator.h @@ -29,13 +29,13 @@ public: /** \brief Elaborate the given expression. */ - std::pair operator()(expr const & e); + std::pair operator()(expr const & e, options const & opts); /** \brief Elaborate the given type and expression. The typeof(e) == t. This information is used by the elaborator. The result is a new elaborated type and expression. */ - std::tuple operator()(name const & n, expr const & t, expr const & e); + std::tuple operator()(name const & n, expr const & t, expr const & e, options const & opts); /** \brief If \c e is an expression instantiated by the elaborator, then it diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp index 81e392eac..3d473cacf 100644 --- a/src/frontends/lean/parser_cmds.cpp +++ b/src/frontends/lean/parser_cmds.cpp @@ -148,7 +148,7 @@ void parser_imp::parse_def_core(bool is_definition) { pre_val = mk_abstraction(expr_kind::Lambda, parameters, val_body); } } - auto r = m_elaborator(id, pre_type, pre_val); + auto r = elaborate(id, pre_type, pre_val); expr type = std::get<0>(r); expr val = std::get<1>(r); metavar_env menv = std::get<2>(r); @@ -212,7 +212,7 @@ void parser_imp::parse_variable_core(bool is_var) { expr type_body = parse_expr(); pre_type = mk_abstraction(expr_kind::Pi, parameters, type_body); } - auto p = m_elaborator(pre_type); + auto p = elaborate(pre_type); expr type = p.first; metavar_env menv = p.second; if (has_metavar(type)) @@ -273,7 +273,7 @@ void parser_imp::parse_axiom() { /** \brief Parse 'Eval' expr */ void parser_imp::parse_eval() { next(); - expr v = m_elaborator(parse_expr()).first; + expr v = elaborate(parse_expr()).first; normalizer norm(m_env); expr r = norm(v); regular(m_io_state) << r << endl; @@ -360,7 +360,7 @@ void parser_imp::parse_print() { next(); regular(m_io_state) << msg << endl; } else { - expr v = m_elaborator(parse_expr()).first; + expr v = elaborate(parse_expr()).first; regular(m_io_state) << v << endl; } } @@ -368,7 +368,7 @@ void parser_imp::parse_print() { /** \brief Parse 'Check' expr */ void parser_imp::parse_check() { next(); - auto p = m_elaborator(parse_expr()); + auto p = elaborate(parse_expr()); check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration"); expr v = p.first; expr t = type_check(v, m_env); @@ -709,7 +709,7 @@ void parser_imp::parse_builtin() { expr type; if (curr_is_colon()) { next(); - auto p = m_elaborator(parse_expr()); + auto p = elaborate(parse_expr()); check_no_metavar(p, "invalid builtin declaration, type still contains metavariables after elaboration"); type = p.first; } else { @@ -717,7 +717,7 @@ void parser_imp::parse_builtin() { parse_var_decl_parameters(parameters); check_colon_next("invalid builtin declaration, ':' expected"); expr type_body = parse_expr(); - auto p = m_elaborator(mk_abstraction(expr_kind::Pi, parameters, type_body)); + auto p = elaborate(mk_abstraction(expr_kind::Pi, parameters, type_body)); check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration"); type = p.first; } diff --git a/src/frontends/lean/parser_imp.cpp b/src/frontends/lean/parser_imp.cpp index e5d317ca5..f41beee28 100644 --- a/src/frontends/lean/parser_imp.cpp +++ b/src/frontends/lean/parser_imp.cpp @@ -126,6 +126,14 @@ void parser_imp::parse_script(bool as_expr) { void parser_imp::parse_script_expr() { return parse_script(true); } +std::pair parser_imp::elaborate(expr const & e) { + return m_elaborator(e, m_io_state.get_options()); +} + +std::tuple parser_imp::elaborate(name const & n, expr const & t, expr const & e) { + return m_elaborator(n, t, e, m_io_state.get_options()); +} + void parser_imp::sync_command() { // Keep consuming tokens until we find a Command or End-of-file show_prompt(); @@ -217,7 +225,7 @@ bool parser_imp::parse_commands() { /** \brief Parse an expression. */ expr parser_imp::parse_expr_main() { try { - auto p = m_elaborator(parse_expr()); + auto p = elaborate(parse_expr()); check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration"); return p.first; } catch (parser_error & ex) { diff --git a/src/frontends/lean/parser_imp.h b/src/frontends/lean/parser_imp.h index e7e6e6621..4504f5264 100644 --- a/src/frontends/lean/parser_imp.h +++ b/src/frontends/lean/parser_imp.h @@ -242,6 +242,15 @@ private: void parse_script(bool as_expr = false); void parse_script_expr(); + /** + @name Elaborator interface + */ + /*@{*/ +private: + std::pair elaborate(expr const & e); + std::tuple elaborate(name const & n, expr const & t, expr const & e); + /*@}*/ + /** @name Parse Universe levels diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 6a00621f7..aaf59d26b 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/list.h" #include "util/splay_tree.h" #include "util/interrupt.h" +#include "util/sstream.h" #include "kernel/for_each_fn.h" #include "kernel/formatter.h" #include "kernel/free_vars.h" @@ -25,9 +26,40 @@ Author: Leonardo de Moura #include "library/elaborator/elaborator.h" #include "library/elaborator/elaborator_justification.h" +#ifndef LEAN_ELABORATOR_MAX_STEPS +#define LEAN_ELABORATOR_MAX_STEPS 100000 +#endif + +#ifndef LEAN_ELABORATOR_USE_NORMALIZER +#define LEAN_ELABORATOR_USE_NORMALIZER true +#endif + +#ifndef LEAN_ELABORATOR_INJECTIVITY +#define LEAN_ELABORATOR_INJECTIVITY true +#endif + namespace lean { static name g_x_name("x"); +static name g_elaborator_max_steps {"elaborator", "max_steps"}; +static name g_elaborator_use_normalizer {"elaborator", "use_normalizer"}; +static name g_elaborator_injectivity {"elaborator", "injectivity"}; + +RegisterUnsignedOption(g_elaborator_max_steps, LEAN_ELABORATOR_MAX_STEPS, "(elaborator) maximum number of steps"); +RegisterBoolOption(g_elaborator_use_normalizer, LEAN_ELABORATOR_USE_NORMALIZER, + "(elaborator) invoke normalizer during elaboration"); +RegisterBoolOption(g_elaborator_injectivity, LEAN_ELABORATOR_INJECTIVITY, "(elaborator) reduce unification constrainst of the form f(t1, t2) ≈ f(s1, s2) into t1 ≈ s1 and t2 ≈ s2 even if f-applications are not in head normal form"); + +unsigned get_elaborator_max_steps(options const & opts) { + return opts.get_unsigned(g_elaborator_max_steps, LEAN_ELABORATOR_MAX_STEPS); +} +bool get_elaborator_use_normalizer(options const & opts) { + return opts.get_bool(g_elaborator_use_normalizer, LEAN_ELABORATOR_USE_NORMALIZER); +} +bool get_elaborator_injectivity(options const & opts) { + return opts.get_bool(g_elaborator_injectivity, LEAN_ELABORATOR_INJECTIVITY); +} + class elaborator::imp { typedef splay_tree name_set; typedef list cnstr_list; @@ -148,16 +180,26 @@ class elaborator::imp { justification m_conflict; bool m_first; level m_U; // universe U used for builtin kernel axioms + unsigned m_num_steps; // options bool m_use_justifications; bool m_use_normalizer; bool m_assume_injectivity; + unsigned m_max_steps; - void set_options(options const &) { + void set_options(options const & o) { m_use_justifications = true; - m_use_normalizer = true; - m_assume_injectivity = true; + m_use_normalizer = get_elaborator_use_normalizer(o); + m_assume_injectivity = get_elaborator_injectivity(o); + m_max_steps = get_elaborator_max_steps(o); + } + + void check_system() { + check_interrupted(); + if (m_num_steps > m_max_steps) + throw exception(sstream() << "elaborator maximum number of steps (" << m_max_steps << ") exceeded, the maximum number of steps can be increased by setting the option elaborator::max_steps (remark: the elaborator uses higher order unification, which may trigger non-termination"); + m_num_steps++; } justification mk_assumption() { @@ -683,7 +725,7 @@ class elaborator::imp { context const & ctx = get_context(c); bool modified = false; while (true) { - check_interrupted(); + check_system(); expr new_a = normalize_step(ctx, a); expr new_b = normalize_step(ctx, b); if (new_a == a && new_b == b) { @@ -1899,11 +1941,13 @@ public: m_next_id = 0; m_first = true; m_U = m_env->get_uvar("U"); + m_num_steps = 0; // display(std::cout); } metavar_env next() { - check_interrupted(); + m_num_steps = 0; + check_system(); if (m_conflict) throw elaborator_exception(m_conflict); if (!m_case_splits.empty()) { @@ -1920,7 +1964,7 @@ public: throw elaborator_exception(m_conflict); } while (true) { - check_interrupted(); + check_system(); cnstr_list & active_cnstrs = m_state.m_active_cnstrs; if (!empty(active_cnstrs)) { unification_constraint c = head(active_cnstrs);