diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 705f3c1801..7b3643823e 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -8,4 +8,4 @@ init_module.cpp type_util.cpp decl_attributes.cpp prenum.cpp print_cmd.cpp elaborator.cpp match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp tactic_evaluator.cpp -parser_state.cpp) +equations_validator.cpp parser_state.cpp) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 8a0dbba2ab..f0be1da1ff 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "frontends/lean/elaborator.h" #include #include "util/flet.h" #include "util/thread.h" @@ -14,6 +13,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/replace_fn.h" #include "kernel/instantiate.h" +#include "kernel/scope_pos_info_provider.h" #include "kernel/inductive/inductive.h" #include "library/trace.h" #include "library/user_recursors.h" @@ -22,7 +22,6 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/placeholder.h" #include "library/explicit.h" -#include "kernel/scope_pos_info_provider.h" #include "library/choice.h" #include "library/string.h" #include "library/class.h" @@ -57,6 +56,8 @@ Author: Leonardo de Moura #include "frontends/lean/tactic_evaluator.h" #include "frontends/lean/structure_cmd.h" #include "frontends/lean/structure_instance.h" +#include "frontends/lean/equations_validator.h" +#include "frontends/lean/elaborator.h" namespace lean { MK_THREAD_LOCAL_GET(type_context_cache_manager, get_tcm, true /* use binder information at infer_cache */); @@ -2302,129 +2303,6 @@ void elaborator::check_inaccessible_annotations(expr const & lhs) { } } -/* Recursive equation pattern validation.*/ -class validate_equation_lhs_fn : public replace_visitor { - elaborator & m_elab; - expr m_ref; - - type_context & ctx() { return m_elab.m_ctx; } - environment const & env() { return m_elab.env(); } - - optional expand(expr const & e) { - /* We don't simply use whnf because we want to avoid exposing the internal implementation - of definitions compiled using the equation compiler */ - { - /* Try without use delta reduction */ - type_context::transparency_scope scope(ctx(), transparency_mode::None); - expr new_e = ctx().whnf(e); - if (new_e != e) return some_expr(new_e); - } - if (auto new_e = ctx().reduce_projection(e)) - return new_e; - /* Try to unfold using refl equations */ - if (auto new_e = dunfold(ctx(), e)) - return new_e; - /* Last resort, whnf using current setting */ - expr new_e = ctx().whnf(e); - if (new_e != e) return some_expr(new_e); - return none_expr(); - } - - [[ noreturn ]] void throw_invalid_pattern(char const * msg, expr const & e) { - throw elaborator_exception(m_ref, format(msg) - + format(" (possible solution, mark term as inaccessible using '.( )')") - + m_elab.pp_indent(e)); - } - - virtual expr visit_local(expr const & e) override { - return e; - } - - virtual expr visit_lambda(expr const & e) override { - throw_invalid_pattern("invalid occurrence of lambda expression in pattern", e); - } - - virtual expr visit_pi(expr const & e) override { - throw_invalid_pattern("invalid occurrence of pi/forall expression in pattern", e); - } - - virtual expr visit_let(expr const & e) override { - return visit(instantiate(let_body(e), let_value(e))); - } - - virtual expr visit_sort(expr const & e) override { - throw_invalid_pattern("invalid occurrence of sort in pattern", e); - } - - virtual expr visit_meta(expr const & e) override { - throw_invalid_pattern("invalid occurrence of metavariable in pattern", e); - } - - [[ noreturn ]] void throw_invalid_app(expr const & e) { - if (is_constant(e)) - throw_invalid_pattern("invalid constant in pattern, it cannot be reduced to a constructor", e); - else - throw_invalid_pattern("invalid function application in pattern, it cannot be reduced to a constructor", e); - } - - virtual expr visit_app(expr const & e) override { - expr it = e; - while (true) { - if (is_nat_int_char_string_name_value(ctx(), it)) - return e; - if (!is_app(it) && !is_constant(it)) - return visit(it); - buffer args; - expr const & fn = get_app_args(it, args); - if (!is_constant(fn)) - throw_invalid_app(e); - - if (optional I = is_ginductive_intro_rule(env(), const_name(fn))) { - unsigned num_params = get_ginductive_num_params(env(), *I); - for (unsigned i = num_params; i < args.size(); i++) { - visit(args[i]); - } - return e; - } else if (optional info = has_inverse(env(), const_name(fn))) { - visit(args.back()); - return e; - } else { - if (auto r = expand(it)) { - it = *r; - } else { - throw_invalid_app(e); - } - } - } - } - - virtual expr visit_constant(expr const & e) override { - return visit_app(e); - } - - virtual expr visit_macro(expr const & e) override { - if (is_inaccessible(e)) { - return e; - } else if (auto r = ctx().expand_macro(e)) { - return visit(*r); - } else { - throw_invalid_pattern("invalid occurrence of macro expression in pattern", e); - } - } - -public: - validate_equation_lhs_fn(elaborator & elab, expr const & ref): - m_elab(elab), m_ref(ref) { - } - - void validate(expr const & lhs) { - buffer args; - get_app_args(lhs, args); - for (expr & arg : args) - visit(arg); - } -}; - expr elaborator::visit_equation(expr const & eq) { expr const & lhs = equation_lhs(eq); expr const & rhs = equation_rhs(eq); @@ -2443,7 +2321,7 @@ expr elaborator::visit_equation(expr const & eq) { expr new_lhs_type = instantiate_mvars(infer_type(new_lhs)); expr new_rhs = visit(rhs, some_expr(new_lhs_type)); new_rhs = enforce_type(new_rhs, new_lhs_type, "equation type mismatch", eq); - validate_equation_lhs_fn(*this, lhs).validate(instantiate_mvars(new_lhs)); + validate_equation_lhs(*this, new_lhs, lhs); return copy_tag(eq, mk_equation(new_lhs, new_rhs, ignore_equation_if_unused(eq))); } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 9bf1b644d6..07ceb5f6f7 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -112,7 +112,6 @@ private: bool is_def_eq(expr const & e1, expr const & e2); bool try_is_def_eq(expr const & e1, expr const & e2); bool assign_mvar(expr const & e1, expr const & e2) { lean_assert(is_metavar(e1)); return is_def_eq(e1, e2); } - expr instantiate_mvars(expr const & e); bool is_uvar_assigned(level const & l) const { return m_ctx.is_assigned(l); } bool is_mvar_assigned(expr const & e) const { return m_ctx.is_assigned(e); } @@ -271,6 +270,7 @@ public: expr mk_pi(buffer const & params, expr const & type) { return m_ctx.mk_pi(params, type); } expr mk_lambda(buffer const & params, expr const & type) { return m_ctx.mk_lambda(params, type); } expr infer_type(expr const & e) { return m_ctx.infer(e); } + expr instantiate_mvars(expr const & e); void set_instance_fingerprint() { m_ctx.set_instance_fingerprint(); } expr elaborate(expr const & e); expr elaborate_type(expr const & e); diff --git a/src/frontends/lean/equations_validator.cpp b/src/frontends/lean/equations_validator.cpp new file mode 100644 index 0000000000..adc702223e --- /dev/null +++ b/src/frontends/lean/equations_validator.cpp @@ -0,0 +1,142 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/replace_visitor.h" +#include "library/inverse.h" +#include "library/inductive_compiler/ginductive.h" +#include "library/equations_compiler/equations.h" +#include "library/equations_compiler/util.h" +#include "library/tactic/unfold_tactic.h" +#include "frontends/lean/elaborator.h" + +namespace lean { +/* Recursive equation pattern validation.*/ +class validate_equation_lhs_fn : public replace_visitor { + elaborator & m_elab; + expr m_ref; + + type_context & ctx() { return m_elab.m_ctx; } + environment const & env() { return m_elab.env(); } + + optional expand(expr const & e) { + /* We don't simply use whnf because we want to avoid exposing the internal implementation + of definitions compiled using the equation compiler */ + { + /* Try without use delta reduction */ + type_context::transparency_scope scope(ctx(), transparency_mode::None); + expr new_e = ctx().whnf(e); + if (new_e != e) return some_expr(new_e); + } + if (auto new_e = ctx().reduce_projection(e)) + return new_e; + /* Try to unfold using refl equations */ + if (auto new_e = dunfold(ctx(), e)) + return new_e; + /* Last resort, whnf using current setting */ + expr new_e = ctx().whnf(e); + if (new_e != e) return some_expr(new_e); + return none_expr(); + } + + [[ noreturn ]] void throw_invalid_pattern(char const * msg, expr const & e) { + throw elaborator_exception(m_ref, format(msg) + + format(" (possible solution, mark term as inaccessible using '.( )')") + + m_elab.pp_indent(e)); + } + + virtual expr visit_local(expr const & e) override { + return e; + } + + virtual expr visit_lambda(expr const & e) override { + throw_invalid_pattern("invalid occurrence of lambda expression in pattern", e); + } + + virtual expr visit_pi(expr const & e) override { + throw_invalid_pattern("invalid occurrence of pi/forall expression in pattern", e); + } + + virtual expr visit_let(expr const & e) override { + return visit(instantiate(let_body(e), let_value(e))); + } + + virtual expr visit_sort(expr const & e) override { + throw_invalid_pattern("invalid occurrence of sort in pattern", e); + } + + virtual expr visit_meta(expr const & e) override { + throw_invalid_pattern("invalid occurrence of metavariable in pattern", e); + } + + [[ noreturn ]] void throw_invalid_app(expr const & e) { + if (is_constant(e)) + throw_invalid_pattern("invalid constant in pattern, it cannot be reduced to a constructor", e); + else + throw_invalid_pattern("invalid function application in pattern, it cannot be reduced to a constructor", e); + } + + virtual expr visit_app(expr const & e) override { + expr it = e; + while (true) { + if (is_nat_int_char_string_name_value(ctx(), it)) + return e; + if (!is_app(it) && !is_constant(it)) + return visit(it); + buffer args; + expr const & fn = get_app_args(it, args); + if (!is_constant(fn)) + throw_invalid_app(e); + + if (optional I = is_ginductive_intro_rule(env(), const_name(fn))) { + unsigned num_params = get_ginductive_num_params(env(), *I); + for (unsigned i = num_params; i < args.size(); i++) { + visit(args[i]); + } + return e; + } else if (optional info = has_inverse(env(), const_name(fn))) { + visit(args.back()); + return e; + } else { + if (auto r = expand(it)) { + it = *r; + } else { + throw_invalid_app(e); + } + } + } + } + + virtual expr visit_constant(expr const & e) override { + return visit_app(e); + } + + virtual expr visit_macro(expr const & e) override { + if (is_inaccessible(e)) { + return e; + } else if (auto r = ctx().expand_macro(e)) { + return visit(*r); + } else { + throw_invalid_pattern("invalid occurrence of macro expression in pattern", e); + } + } + +public: + validate_equation_lhs_fn(elaborator & elab, expr const & ref): + m_elab(elab), m_ref(ref) { + } + + void validate(expr const & lhs) { + buffer args; + get_app_args(lhs, args); + for (expr & arg : args) + visit(arg); + } +}; + +void validate_equation_lhs(elaborator & elab, expr const & lhs, expr const & ref) { + validate_equation_lhs_fn(elab, ref).validate(elab.instantiate_mvars(lhs)); +} +} diff --git a/src/frontends/lean/equations_validator.h b/src/frontends/lean/equations_validator.h new file mode 100644 index 0000000000..361bd51be9 --- /dev/null +++ b/src/frontends/lean/equations_validator.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "frontends/lean/elaborator.h" +namespace lean { +void validate_equation_lhs(elaborator & elab, expr const & lhs, expr const & ref); +}