refactor(frontends/lean/equations_validator): move validation code to another file

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)

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 <string>
 #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<expr> 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<expr> args;
-            expr const & fn = get_app_args(it, args);
-            if (!is_constant(fn))
-                throw_invalid_app(e);
-
-            if (optional<name> 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<inverse_info> 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<expr> 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)));
 }
 

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<expr> const & params, expr const & type) { return m_ctx.mk_pi(params, type); }
     expr mk_lambda(buffer<expr> 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);

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<expr> 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<expr> args;
+            expr const & fn = get_app_args(it, args);
+            if (!is_constant(fn))
+                throw_invalid_app(e);
+
+            if (optional<name> 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<inverse_info> 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<expr> 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));
+}
+}

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);
+}