feat(frontends/lean): recursive equation preprocessor

To make the equation compiler more convenient to use, we will add a
couple of preprocessing steps.
This commit adds the first one of them. In this step, we use
type inference to refine pattern variables, and we relax the
restrictions on inaccessible annotations.

We will also add a preprocessing step that implements the "complete
transition" step before we execute the elim_match step.

library/init/data/nat/lemmas.lean

@@ -268,7 +268,6 @@ protected lemma le_of_add_le_add_left {k n m : ℕ} (h : k + n ≤ k + m) : n
 match le.dest h with
 | ⟨w, hw⟩ := @le.intro _ _ w
   begin
-    dsimp at hw,
     rw [nat.add_assoc] at hw,
     apply nat.add_left_cancel hw
   end

library/init/logic.lean

@@ -156,13 +156,13 @@ heq.rec_on h (eq.refl α)
 end
 
 lemma eq_rec_heq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (eq.rec_on h p : φ a') == p
-| a ._ rfl p := heq.refl p
+| a _ rfl p := heq.refl p
 
 lemma heq_of_eq_rec_left {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : (eq.rec_on e p₁ : φ a') = p₂), p₁ == p₂
-| a ._ p₁ p₂ (eq.refl ._) h := eq.rec_on h (heq.refl p₁)
+| a _ p₁ p₂ rfl h := eq.rec_on h (heq.refl p₁)
 
 lemma heq_of_eq_rec_right {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
-| a ._ p₁ p₂ (eq.refl ._) h :=
+| a _ p₁ p₂ rfl h :=
   have p₁ = p₂, from h,
   this ▸ heq.refl p₁
 
@@ -170,19 +170,10 @@ lemma of_heq_true {a : Prop} (h : a == true) : a :=
 of_eq_true (eq_of_heq h)
 
 lemma eq_rec_compose : ∀ {α β φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α), (eq.rec_on p₁ (eq.rec_on p₂ a : β) : φ) = eq.rec_on (eq.trans p₂ p₁) a
-| α ._ ._ (eq.refl ._) (eq.refl ._) a := rfl
-
-lemma eq_rec_eq_eq_rec : ∀ {α₁ α₂ : Sort u} {p : α₁ = α₂} {a₁ : α₁} {a₂ : α₂}, (eq.rec_on p a₁ : α₂) = a₂ → a₁ = eq.rec_on (eq.symm p) a₂
-| α ._ rfl a ._ rfl := rfl
-
-lemma eq_rec_of_heq_left : ∀ {α₁ α₂ : Sort u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂), (eq.rec_on (type_eq_of_heq h) a₁ : α₂) = a₂
-| α ._ a ._ (heq.refl ._) := rfl
-
-lemma eq_rec_of_heq_right {α₁ α₂ : Sort u} {a₁ : α₁} {a₂ : α₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ :=
-eq_rec_eq_eq_rec (eq_rec_of_heq_left h)
+| α _ _ rfl rfl a := rfl
 
 lemma cast_heq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a == a
-| α ._ (eq.refl ._) a := heq.refl a
+| α _ rfl a := heq.refl a
 
 /- and -/
 

library/init/meta/interactive.lean

@@ -229,9 +229,9 @@ hypotheses (or `*`), or in the goal if no `at` clause is specified, provided tha
 `A` and `B` are definitionally equal.
 -/
 meta def change (q : parse texpr) : parse (tk "with" *> texpr)? → parse location → tactic unit
-| none (loc.ns [none]) := do e ← i_to_expr q, change_core e none 
-| none (loc.ns [some h]) := do eq ← i_to_expr q, eh ← get_local h, change_core eq (some eh) 
-| none _ := fail "change-at does not support multiple locations" 
+| none (loc.ns [none]) := do e ← i_to_expr q, change_core e none
+| none (loc.ns [some h]) := do eq ← i_to_expr q, eh ← get_local h, change_core eq (some eh)
+| none _ := fail "change-at does not support multiple locations"
 | (some w) l :=
   do u ← mk_meta_univ,
      ty ← mk_meta_var (sort u),

src/frontends/lean/CMakeLists.txt

@@ -8,5 +8,5 @@ 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 module_parser.cpp
-equations_validator.cpp parser_state.cpp interactive.cpp completion.cpp
+parser_state.cpp interactive.cpp completion.cpp
 user_notation.cpp user_command.cpp)

src/frontends/lean/elaborator.cpp

@@ -62,7 +62,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/prenum.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/structure_instance.h"
-#include "frontends/lean/equations_validator.h"
 #include "frontends/lean/elaborator.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_COERCIONS
@@ -1223,9 +1222,6 @@ optional<expr> elaborator::process_optional_and_auto_params(expr type, expr cons
             new_arg = mk_local(mk_fresh_name(), binding_name(type), d, binding_info(type));
             eta_args.push_back(new_arg);
         }
-        // implicit arguments are tagged as inaccessible in patterns
-        if (found && m_in_pattern)
-            new_arg = copy_tag(ref, mk_inaccessible(new_arg));
         new_args.push_back(new_arg);
         type = instantiate(binding_body(type), new_arg);
         if (found) {
@@ -1268,9 +1264,6 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
             new_arg = mk_metavar(d, ref);
             if (bi.is_inst_implicit())
                 info.new_instances.push_back(new_arg);
-            // implicit arguments are tagged as inaccessible in patterns
-            if (m_in_pattern)
-                new_arg = copy_tag(ref, mk_inaccessible(new_arg));
         } else if (i < args.size()) {
             // explicit argument
             expr const & arg_ref = args[i];
@@ -1282,11 +1275,11 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
 
                    This is important when we are elaborating terms such as
 
-                   l^.map (λ ⟨a, b⟩, a + b)
+                   l.map (λ ⟨a, b⟩, a + b)
 
                    where (l : list (nat × nat))
 
-                   We elaborate l when we process l^.map, and convert it into
+                   We elaborate l when we process l.map, and convert it into
 
                    list.map (λ ⟨a, b⟩, a + b) (as-is l)
 
@@ -2203,6 +2196,10 @@ static expr copy_domain(unsigned num, expr const & source, expr const & target)
     }
 }
 
+static void throw_ill_formed_equation(expr const & ref) {
+    throw elaborator_exception(ref, "ill-formed match/equation expression");
+}
+
 static void check_equations_arity(buffer<expr> const & eqns) {
     buffer<optional<unsigned>> fidx2arity;
     for (expr eqn : eqns) {
@@ -2217,7 +2214,7 @@ static void check_equations_arity(buffer<expr> const & eqns) {
             expr const & fn  = get_app_fn(lhs);
             unsigned arity   = get_app_num_args(lhs);
             if (!is_var(fn) || var_idx(fn) >= nbinders)
-                throw elaborator_exception(eqn, "ill-formed match/equations expression");
+                throw_ill_formed_equation(eqn);
             unsigned fidx    = nbinders - var_idx(fn) - 1;
             if (fidx >= fidx2arity.size())
                 fidx2arity.resize(fidx+1, optional<unsigned>());
@@ -2232,7 +2229,7 @@ static void check_equations_arity(buffer<expr> const & eqns) {
         } else if (is_no_equation(eqn)) {
             /* do nothing */
         } else {
-            throw elaborator_exception(curr, "ill-formed match/equations expression");
+            throw_ill_formed_equation(curr);
         }
     }
 }
@@ -2266,13 +2263,307 @@ expr elaborator::mk_aux_meta_def(expr const & e, expr const & ref) {
     return new_c;
 }
 
+static void mvar_dep_sort_aux(type_context & ctx, expr const & m,
+                              name_set const & mvar_names, name_set & visited, buffer<expr> & result) {
+    if (visited.contains(mlocal_name(m)))
+        return;
+    for_each(ctx.instantiate_mvars(ctx.infer(m)), [&](expr const & e, unsigned) {
+            if (is_metavar(e) && mvar_names.contains(mlocal_name(e))) {
+                mvar_dep_sort_aux(ctx, e, mvar_names, visited, result);
+                return false; // do not visit types
+            }
+            if (is_local(e)) {
+                return false; // do not visit types
+            }
+            return true;
+        });
+    visited.insert(mlocal_name(m));
+    result.push_back(m);
+}
+
+/* Topological sort based on dependencies. */
+static void mvar_dep_sort(type_context & ctx, buffer<expr> & mvars) {
+    name_set visited;
+    buffer<expr> result;
+    name_set mvar_names;
+    for (expr const & m : mvars)
+        mvar_names.insert(mlocal_name(m));
+    for (expr const & m : mvars)
+        mvar_dep_sort_aux(ctx, m, mvar_names, visited, result);
+    mvars.clear();
+    mvars.append(result);
+}
+
+/* We preprocess the equation left-hand-side by first elaborating it using metavariables.
+   This process allows us to refine pattern variables whose value is fixed by type inference.
+   Before processing the right-hand-side, we must convert back these metavariables into
+   pattern variables (i.e., local constants).
+   This visitor collects metavariables that must be converted into pattern variables, and
+   validates the equation left-hand-side. */
+class validate_and_collect_lhs_mvars : public replace_visitor {
+    elaborator &    m_elab;
+    bool            m_has_invalid_pattern = false;
+    expr            m_ref;
+    /* m_mctx0 is the metavariable context before processing the equation.
+       Only metavariables created when processing the equation can be
+       converted into pattern variables. */
+    metavar_context m_mctx0;
+    buffer<expr> &  m_unassigned_mvars;
+    name_set        m_collected;
+
+    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();
+    }
+
+    void throw_invalid_pattern(char const * msg, expr const & e) {
+        m_elab.report_or_throw(
+            elaborator_exception(m_ref, format(msg)
+                + format(" (possible solution, mark term as inaccessible using '.( )')")
+                + m_elab.pp_indent(e))
+            .ignore_if(m_elab.has_synth_sorry(e)));
+        m_has_invalid_pattern = true;
+    }
+
+    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);
+        return e;
+    }
+
+    virtual expr visit_pi(expr const & e) override {
+        throw_invalid_pattern("invalid occurrence of pi/forall expression in pattern", e);
+        return 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);
+        return e;
+    }
+
+    virtual expr visit_meta(expr const & m) override {
+        if (is_metavar_decl_ref(m) && !m_mctx0.find_metavar_decl(m)) {
+            if (!m_collected.contains(mlocal_name(m))) {
+                m_unassigned_mvars.push_back(m);
+                m_collected.insert(mlocal_name(m));
+            }
+            return m;
+        } else {
+            throw_invalid_pattern("invalid occurrence of metavariable in pattern", m);
+            return m;
+        }
+    }
+
+    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);
+                return 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);
+                    return 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 if (is_synthetic_sorry(e)) {
+            return e;
+        } else {
+            throw_invalid_pattern("invalid occurrence of macro expression in pattern", e);
+            return e;
+        }
+    }
+
+public:
+    validate_and_collect_lhs_mvars(elaborator & elab, expr const & ref, metavar_context const & mctx0,
+                                   buffer<expr> & unassigned_mvars):
+        m_elab(elab),
+        m_ref(ref),
+        m_mctx0(mctx0),
+        m_unassigned_mvars(unassigned_mvars) {
+    }
+
+    bool operator()(expr const & lhs) {
+        buffer<expr> args;
+        get_app_args(lhs, args);
+        for (expr & arg : args)
+            visit(arg);
+        return m_has_invalid_pattern;
+    }
+};
+
+expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
+    expr const & ref = e;
+    type_context::tmp_locals fns(m_ctx);
+    expr it = e;
+    for (unsigned i = 0; i < num_fns; i++) {
+        if (!is_lambda(it))
+            throw_ill_formed_equation(ref);
+        expr d     = instantiate_rev_locals(binding_domain(it), fns);
+        expr new_d = visit(d, none_expr());
+        expr ref_d = get_ref_for_child(binding_domain(it), it);
+        expr fn    = copy_tag(binding_domain(it), push_local(fns, binding_name(it), new_d, binding_info(it), ref_d));
+        save_identifier_info(fn);
+        it = binding_body(it);
+    }
+    if (is_no_equation(it)) {
+        return fns.mk_lambda(it);
+    } else {
+        metavar_context mctx0 = m_ctx.mctx();
+        it = instantiate_rev_locals(it, fns);
+        buffer<expr> local_mvars;
+        buffer<expr> type_mvars;
+        while (is_lambda(it)) {
+            expr type = mk_type_metavar(it);
+            type_mvars.push_back(type);
+            expr mvar = copy_tag(binding_domain(it), m_ctx.mk_metavar_decl(binding_name(it), m_ctx.lctx(), type));
+            local_mvars.push_back(mvar);
+            it = binding_body(it);
+        }
+        if (!is_equation(it))
+            throw_ill_formed_equation(ref);
+        expr lhs    = instantiate_rev(equation_lhs(it), local_mvars);
+        expr lhs_fn = get_app_fn(lhs);
+        if (is_explicit_or_partial_explicit(lhs_fn))
+            lhs_fn = get_explicit_or_partial_explicit_arg(lhs_fn);
+        if (!is_local(lhs_fn))
+            throw_ill_formed_equation(ref);
+        expr new_lhs;
+        {
+            flet<bool> set(m_in_pattern, true);
+            new_lhs = visit(lhs, none_expr());
+            synthesize_no_tactics();
+        }
+        new_lhs = instantiate_mvars(new_lhs);
+        // tout() << "LHS: " << new_lhs << "\n";
+        // collect unassigned metavariables not in mctx0
+        buffer<expr> unassigned_mvars;
+        validate_and_collect_lhs_mvars(*this, ref, mctx0, unassigned_mvars)(new_lhs);
+        // sort using dependencies
+        mvar_dep_sort(m_ctx, unassigned_mvars);
+        // create local variables for each unassigned metavar
+        type_context::tmp_locals new_locals(m_ctx);
+        for (expr & m : unassigned_mvars) {
+            expr type      = instantiate_mvars(m_ctx.infer(m));
+            expr new_local = new_locals.push_local(mlocal_pp_name(m), type, binder_info());
+            m_ctx.assign(m, new_local);
+            // tout() << "new local >> " << m << ", " << mlocal_name(m) << " : " << type << "\n";
+        }
+        // replace metavariables with new locals
+        new_lhs           = instantiate_mvars(new_lhs);
+        expr new_lhs_type = instantiate_mvars(infer_type(new_lhs));
+        // process rhs
+        buffer<expr> rhs_subst;
+        for (expr const & local_mvar : local_mvars) {
+            expr s = instantiate_mvars(local_mvar);
+            if (!is_local(s)) {
+                /* The `as_is` macro affects how applications are elaborated.
+                   See comment at first_pass method.
+                   So, we only use it if it is really needed. That is,
+                   the metavariable was fixed to a non trivial term by type inference rules.
+                   For example, in the following definition
+
+                   ```
+                   inductive Vec (A : Type) : nat → Type
+                   | nil {} : Vec 0
+                   | cons   : Π {n}, A → Vec n → Vec (succ n)
+
+                   open Vec
+
+                   def append1 {A : Type} : Π {m n : nat}, Vec A m -> Vec A n -> Vec A (n + m)
+                   | n m nil         ys := ys
+                   | n m (cons x xs) ys := cons x (append1 xs ys)
+                   ```
+
+                   The variable n is refined to 0 and (succ n') in the first and second equations.
+                */
+                s = mk_as_is(s);
+            }
+            rhs_subst.push_back(s);
+        }
+        expr rhs     = instantiate_rev(equation_rhs(it), rhs_subst);
+        expr new_rhs = visit(rhs, some_expr(new_lhs_type));
+        // synthesize_no_tactics();
+        // new_rhs       = instantiate_mvars(new_rhs);
+        new_rhs       = enforce_type(new_rhs, new_lhs_type, "equation type mismatch", it);
+        // tout() << "lhs: " << new_lhs << "\n";
+        // tout() << "rhs: " << new_rhs << "\n";
+        expr new_eq = copy_tag(it, mk_equation(new_lhs, new_rhs, ignore_equation_if_unused(it)));
+        expr r = copy_tag(ref, fns.mk_lambda(new_locals.mk_lambda(new_eq)));
+        // tout() << "r:   " << r << "\n";
+        return r;
+    }
+}
+
 expr elaborator::visit_equations(expr const & e) {
     expr const & ref = e;
     buffer<expr> eqs;
     buffer<expr> new_eqs;
     optional<expr> new_tacs;
-    flet<list<expr_pair>> save_stack(m_inaccessible_stack, m_inaccessible_stack);
-    list<expr_pair> saved_inaccessible_stack = m_inaccessible_stack;
     equations_header const & header = get_equations_header(e);
     unsigned num_fns = header.m_num_fns;
     to_equations(e, eqs);
@@ -2297,18 +2588,17 @@ expr elaborator::visit_equations(expr const & e) {
                 /* Replace first num_fns domains of eq with the ones in first_eq.
                    This is a trick/hack to ensure the fns in each equation have
                    the same elaborated type. */
-                new_eq   = copy_tag(eq, visit(copy_domain(num_fns, *first_eq, eq), none_expr()));
+                new_eq   = copy_tag(eq, visit_equation(copy_domain(num_fns, *first_eq, eq), num_fns));
                 new_eqs.push_back(new_eq);
             }
         } else {
-            new_eq   = copy_tag(eq, visit(eq, none_expr()));
+            new_eq   = copy_tag(eq, visit_equation(eq, num_fns));
             first_eq = new_eq;
             new_eqs.push_back(new_eq);
         }
     }
     check_equations_arity(new_eqs);
     synthesize();
-    check_inaccessible(saved_inaccessible_stack);
     expr new_e;
     if (new_tacs) {
         new_e = copy_tag(e, mk_equations(header, new_eqs.size(), new_eqs.data(), *new_tacs));
@@ -2358,42 +2648,17 @@ void elaborator::check_inaccessible_annotations(expr const & lhs) {
     }
 }
 
-expr elaborator::visit_equation(expr const & eq) {
-    expr const & lhs = equation_lhs(eq);
-    expr const & rhs = equation_rhs(eq);
-    expr lhs_fn = get_app_fn(lhs);
-    if (is_explicit_or_partial_explicit(lhs_fn))
-        lhs_fn = get_explicit_or_partial_explicit_arg(lhs_fn);
-    if (!is_local(lhs_fn))
-        throw exception("ill-formed equation");
-    expr new_lhs;
-    {
-        flet<bool> set(m_in_pattern, true);
-        new_lhs = visit(lhs, none_expr());
-        check_inaccessible_annotations(new_lhs);
-        synthesize_no_tactics();
-    }
-    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(*this, new_lhs, lhs);
-    return copy_tag(eq, mk_equation(new_lhs, new_rhs, ignore_equation_if_unused(eq)));
-}
-
 expr elaborator::visit_inaccessible(expr const & e, optional<expr> const & expected_type) {
     if (!m_in_pattern)
         throw elaborator_exception(e, "invalid occurrence of 'inaccessible' annotation, "
                                    "it must only occur in patterns");
-    expr const & ref = e;
-    expr m = mk_metavar(expected_type, ref);
     expr a = get_annotation_arg(e);
     expr new_a;
     {
         flet<bool> set(m_in_pattern, false);
         new_a = visit(a, expected_type);
     }
-    m_inaccessible_stack = cons(mk_pair(m, new_a), m_inaccessible_stack);
-    return copy_tag(e, mk_inaccessible(m));
+    return copy_tag(e, mk_inaccessible(new_a));
 }
 
 elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr const & s, expr const & s_type) {
@@ -2913,8 +3178,7 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
         lean_assert(!is_app_fn); // visit_convoy is used in this case
         return visit_equations(e);
     } else if (is_equation(e)) {
-        lean_assert(!is_app_fn);
-        return visit_equation(e);
+        throw elaborator_exception(e, "unexpected occurrence of equation");
     } else if (is_field_notation(e)) {
         return visit_field(e, expected_type);
     } else if (is_expr_quote(e)) {
@@ -3362,41 +3626,6 @@ void elaborator::synthesize() {
     process_holes();
 }
 
-void elaborator::check_inaccessible(list<expr_pair> const & old_stack) {
-    buffer<expr_pair> to_process;
-    while (!is_eqp(m_inaccessible_stack, old_stack)) {
-        to_process.push_back(head(m_inaccessible_stack));
-        m_inaccessible_stack = tail(m_inaccessible_stack);
-    }
-    if (to_process.empty()) return;
-
-    unsigned i = to_process.size();
-    while (i > 0) {
-        --i;
-        expr_pair const & p = to_process[i];
-        expr const & m = p.first;
-        lean_assert(is_metavar(m));
-        if (!m_ctx.is_assigned(m)) {
-            throw elaborator_exception(m, "invalid use of inaccessible term, it is not fixed by other arguments");
-        }
-        expr v = instantiate_mvars(m);
-        if (has_expr_metavar(v)) {
-            throw elaborator_exception(m, format("invalid use of inaccessible term, "
-                                                 "it is not completely fixed by other arguments") +
-                                       pp_indent(v))
-                .ignore_if(has_synth_sorry({v}));
-        }
-        if (!is_def_eq(v, p.second)) {
-            auto pp_fn = mk_pp_ctx();
-            throw elaborator_exception(m, format("invalid use of inaccessible term, the provided term is") +
-                                       pp_indent(pp_fn, p.second) +
-                                       line() + format("but is expected to be") +
-                                       pp_indent(pp_fn, v))
-                .ignore_if(has_synth_sorry({v, p.second}));
-        }
-    }
-}
-
 void elaborator::report_error(tactic_state const & s, char const * state_header,
                               char const * msg, expr const & ref) {
     auto tc = std::make_shared<type_context>(m_env, m_opts, m_ctx.mctx(), m_ctx.lctx());
@@ -3441,7 +3670,6 @@ elaborator::snapshot::snapshot(elaborator const & e) {
     m_saved_numeral_types      = e.m_numeral_types;
     m_saved_tactics            = e.m_tactics;
     m_saved_holes              = e.m_holes;
-    m_saved_inaccessible_stack = e.m_inaccessible_stack;
 }
 
 void elaborator::snapshot::restore(elaborator & e) {
@@ -3451,7 +3679,6 @@ void elaborator::snapshot::restore(elaborator & e) {
     e.m_numeral_types      = m_saved_numeral_types;
     e.m_tactics            = m_saved_tactics;
     e.m_holes              = m_saved_holes;
-    e.m_inaccessible_stack = m_saved_inaccessible_stack;
 }
 
 /**
@@ -3860,8 +4087,6 @@ struct resolve_names_fn : public replace_visitor {
         return mk_choice(new_args.size(), new_args.data());
     }
 
-
-
     virtual expr visit(expr const & e) override {
         if (is_placeholder(e) || is_by(e) || is_hole(e) || is_as_is(e) || is_emptyc_or_emptys(e) || is_as_atomic(e)) {
             return e;

src/frontends/lean/elaborator.h

@@ -28,7 +28,7 @@ class elaborator {
 public:
     class checkpoint;
 private:
-    friend class validate_equation_lhs_fn;
+    friend class validate_and_collect_lhs_mvars;
     typedef std::vector<pair<expr, expr>> to_check_sorts;
     enum class arg_mask {
         AllExplicit /* @ annotation */,
@@ -48,7 +48,6 @@ private:
     list<expr>        m_numeral_types;
     list<expr_pair>   m_tactics;
     list<expr_pair>   m_holes;
-    list<expr_pair>   m_inaccessible_stack;
 
     /* m_depth is only used for tracing */
     unsigned          m_depth{0};
@@ -63,7 +62,6 @@ private:
         list<expr>             m_saved_numeral_types;
         list<expr_pair>        m_saved_tactics;
         list<expr_pair>        m_saved_holes;
-        list<expr_pair>        m_saved_inaccessible_stack;
 
         snapshot(elaborator const & elab);
         void restore(elaborator & elab);
@@ -238,7 +236,7 @@ private:
     expr visit_equations(expr const & e);
     void check_pattern_inaccessible_annotations(expr const & p);
     void check_inaccessible_annotations(expr const & lhs);
-    expr visit_equation(expr const & eq);
+    expr visit_equation(expr const & eq, unsigned num_fns);
     expr visit_inaccessible(expr const & e, optional<expr> const & expected_type);
 
     struct field_resolution {
@@ -281,7 +279,6 @@ private:
     void synthesize_using_tactics();
     void synthesize_no_tactics();
     void synthesize();
-    void check_inaccessible(list<expr_pair> const & old_stack);
 
     void finalize_core(sanitize_param_names_fn & S, buffer<expr> & es,
                        bool check_unassigned, bool to_simple_metavar, bool collect_local_ctx);

src/frontends/lean/equations_validator.cpp

@@ -1,158 +0,0 @@
-/*
-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 "kernel/instantiate.h"
-#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;
-    bool           m_has_invalid_pattern = false;
-    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();
-    }
-
-    void throw_invalid_pattern(char const * msg, expr const & e) {
-        m_elab.report_or_throw(
-            elaborator_exception(m_ref, format(msg)
-                + format(" (possible solution, mark term as inaccessible using '.( )')")
-                + m_elab.pp_indent(e))
-            .ignore_if(m_elab.has_synth_sorry(e)));
-        m_has_invalid_pattern = true;
-    }
-
-    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);
-        return e;
-    }
-
-    virtual expr visit_pi(expr const & e) override {
-        throw_invalid_pattern("invalid occurrence of pi/forall expression in pattern", e);
-        return 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);
-        return e;
-    }
-
-    virtual expr visit_meta(expr const & e) override {
-        throw_invalid_pattern("invalid occurrence of metavariable in pattern", e);
-        return e;
-    }
-
-    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);
-                return 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);
-                    return 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 if (is_synthetic_sorry(e)) {
-            return e;
-        } else {
-            throw_invalid_pattern("invalid occurrence of macro expression in pattern", e);
-            return e;
-        }
-    }
-
-public:
-    validate_equation_lhs_fn(elaborator & elab, expr const & ref):
-        m_elab(elab), m_ref(ref) {
-    }
-
-    bool validate(expr const & lhs) {
-        buffer<expr> args;
-        get_app_args(lhs, args);
-        for (expr & arg : args)
-            visit(arg);
-        return m_has_invalid_pattern;
-    }
-};
-
-bool validate_equation_lhs(elaborator & elab, expr const & lhs, expr const & ref) {
-    return validate_equation_lhs_fn(elab, ref).validate(elab.instantiate_mvars(lhs));
-}
-}

src/frontends/lean/equations_validator.h

@@ -1,11 +0,0 @@
-/*
-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 {
-bool validate_equation_lhs(elaborator & elab, expr const & lhs, expr const & ref);
-}

src/library/type_context.h

@@ -340,6 +340,7 @@ public:
     local_context const & lctx() const { return m_lctx; }
     metavar_context const & mctx() const { return m_mctx; }
     expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
+    expr mk_metavar_decl(name const & pp_n, local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(pp_n, ctx, type); }
     level mk_univ_metavar_decl() { return m_mctx.mk_univ_metavar_decl(); }
 
     name get_unused_name(name const & prefix, unsigned & idx) const { return m_lctx.get_unused_name(prefix, idx); }

tests/lean/run/eqn_preprocessor1.lean

@@ -0,0 +1,58 @@
+open nat
+
+inductive Vec (A : Type) : nat → Type
+| nil {} : Vec 0
+| cons   : Π {n}, A → Vec n → Vec (succ n)
+
+open Vec
+
+def append1 {A : Type} : Π {m n : nat}, Vec A m -> Vec A n -> Vec A (n + m)
+| _ m nil         ys := ys
+| _ m (cons x xs) ys := cons x (append1 xs ys)
+
+def append2 {A : Type} : Π {m n : nat}, Vec A m -> Vec A n -> Vec A (n + m)
+| _ _ nil         ys := ys
+| _ _ (cons x xs) ys := cons x (append2 xs ys)
+
+def append3 {A : Type} : Π {m n : nat}, Vec A m -> Vec A n -> Vec A (n + m)
+| ._ m nil         ys := ys
+| ._ m (cons x xs) ys := cons x (append1 xs ys)
+
+
+inductive Fin : nat → Type
+| fzero : Π {n}, Fin (nat.succ n)
+
+open Fin
+
+def fmin1 : Π {n : nat} (x y : Fin n),  Fin n
+| ._ fzero fzero := fzero
+
+def fmin2 : Π {n : nat} (x y : Fin n),  Fin n
+| _ fzero fzero := fzero
+
+def fmin3 : Π {n : nat} (x y : Fin n),  Fin n
+| n fzero fzero := fzero
+
+def fmin4 : Π {n : nat} (x y : Fin n),  Fin n
+| .(succ n) (@fzero n) (@fzero .(n)) := fzero
+
+def fmin5 : Π {n : nat} (x y : Fin n),  Fin n
+| .(succ n) (@fzero .(n)) (@fzero n) := fzero
+
+def fmin6 : Π {n : nat} (x y : Fin n),  Fin n
+| .(succ _) fzero fzero := fzero
+
+example (n : nat) (x y : Fin n) : fmin1 x y = fmin2 x y :=
+begin cases x, cases y, refl end
+
+example (n : nat) (x y : Fin n) : fmin1 x y = fmin3 x y :=
+begin cases x, cases y, refl end
+
+example (n : nat) (x y : Fin n) : fmin1 x y = fmin4 x y :=
+begin cases x, cases y, refl end
+
+example (n : nat) (x y : Fin n) : fmin1 x y = fmin5 x y :=
+begin cases x, cases y, refl end
+
+example (n : nat) (x y : Fin n) : fmin1 x y = fmin6 x y :=
+begin cases x, cases y, refl end