fix(frontends/lean/decl_cmds): error localization problem for recursive equations

src/frontends/lean/decl_cmds.cpp

@@ -616,7 +616,10 @@ static void parse_equations_core(parser & p, buffer<expr> const & fns, buffer<ex
             }
             while (!p.curr_is_token(get_assign_tk()))
                 lhs_args.push_back(p.parse_expr(get_max_prec()));
-            lhs = p.save_pos(mk_app(lhs_args.size(), lhs_args.data()), lhs_pos);
+            lean_assert(lhs_args.size() > 0);
+            lhs = lhs_args[0];
+            for (unsigned i = 1; i < lhs_args.size(); i++)
+                lhs = copy_tag(lhs_args[i], mk_app(lhs, lhs_args[i]));
 
             unsigned num_undef_ids = p.get_num_undef_ids();
             for (unsigned i = prev_num_undef_ids; i < num_undef_ids; i++) {

tests/lean/bad_eqns.lean.expected.out

@@ -1,8 +1,8 @@
-bad_eqns.lean:4:2: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
+bad_eqns.lean:4:10: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
   0 + x
 in the following equation left-hand-side
   foo1 (0 + x)
-bad_eqns.lean:8:2: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
+bad_eqns.lean:8:10: error: invalid equation left-hand-side, variable 'y' only occurs in inaccessible terms in the following equation left-hand-side
   foo2 x y
 bad_eqns.lean:10:11: error: invalid recursive equations for 'foo3', inconsistent use of inaccessible term annotation, in some equations a pattern is a constructor, and in another it is an inaccessible term
 bad_eqns.lean:21:11: error: mutual recursion is not needed when defining non-recursive functions

tests/lean/error_loc_bug.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+
+Define propositional calculus, valuation, provability, validity, prove soundness.
+
+This file is based on Floris van Doorn Coq files.
+
+Similar to soundness.lean, but defines Nc in Type.
+The idea is to be able to prove soundness using recursive equations.
+-/
+import data.nat data.list
+open nat bool list decidable
+
+definition PropVar [reducible] := nat
+
+inductive PropF :=
+| Var  : PropVar → PropF
+| Bot  : PropF
+| Conj : PropF → PropF → PropF
+| Disj : PropF → PropF → PropF
+| Impl : PropF → PropF → PropF
+
+namespace PropF
+  notation `#`:max P:max := Var P
+  notation A ∨ B         := Disj A B
+  notation A ∧ B         := Conj A B
+  infixr `⇒`:27          := Impl
+  notation `⊥`           := Bot
+
+  definition Neg A       := A ⇒ ⊥
+  notation ~ A           := Neg A
+  definition Top         := ~⊥
+  notation `⊤`           := Top
+  definition BiImpl A B  := A ⇒ B ∧ B ⇒ A
+  infixr `⇔`:27          := BiImpl
+
+  definition valuation   := PropVar → bool
+
+  reserve infix `⊢`:26
+
+  /- Provability -/
+
+  inductive Nc : list PropF → PropF → Type :=
+  infix ⊢ := Nc
+  | Nax   : ∀ Γ A,   A ∈ Γ →             Γ ⊢ A
+  | ImpI  : ∀ Γ A B, A::Γ ⊢ B →          Γ ⊢ A ⇒ B
+  | ImpE  : ∀ Γ A B, Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
+  | BotC  : ∀ Γ A,   (~A)::Γ ⊢ ⊥ →       Γ ⊢ A
+  | AndI  : ∀ Γ A B, Γ ⊢ A → Γ ⊢ B →     Γ ⊢ A ∧ B
+  | AndE₁ : ∀ Γ A B, Γ ⊢ A ∧ B →         Γ ⊢ A
+  | AndE₂ : ∀ Γ A B, Γ ⊢ A ∧ B →         Γ ⊢ B
+  | OrI₁  : ∀ Γ A B, Γ ⊢ A →             Γ ⊢ A ∨ B
+  | OrI₂  : ∀ Γ A B, Γ ⊢ B →             Γ ⊢ A ∨ B
+  | OrE   : ∀ Γ A B C, Γ ⊢ A ∨ B → A::Γ ⊢ C → B::Γ ⊢ C → Γ ⊢ C
+
+  infix ⊢ := Nc
+  open Nc
+
+  -- Remark ⌞t⌟ indicates we should not pattern match on t.
+  -- In the following lemma, we only need to pattern match on Γ ⊢ A,
+  -- by pattern matching on A, we would be creating 10*6 cases instead of 10.
+
+  lemma weakening2 : ∀ {Γ A Δ}, Γ ⊢ A → Γ ⊆ Δ → Δ ⊢ A
+  | Γ ⌞A⌟     Δ (Nax Γ A Hin)          Hs := !Nax  (Hs A Hin)
+  | Γ ⌞A ⇒ B⌟ Δ (ImpI Γ A B H)         Hs := !ImpI (weakening2 H (cons_sub_cons A Hs))
+  | Γ ⌞B⌟     Δ (ImpE Γ A B H₁ H₂)     Hs := !ImpE (weakening2 H₁ Hs) (weakening2 H₂ Hs)
+  | Γ ⌞A⌟     Δ (BotC Γ A H)           Hs := !BotC (weakening2 H (cons_sub_cons (~A) Hs))
+  | Γ ⌞A ∧ B⌟ Δ (AndI Γ A B H₁ H₂)     Hs := !AndI (weakening2 H₁ Hs) (weakening2 H₂ Hs)
+  | Γ ⌞A⌟     Δ (AndE₁ Γ A B H)        Hs := !AndE₁ (weakening2 H Hs)
+  | Γ ⌞B⌟     Δ (AndE₂ Γ A B H)        Hs := !AndE₂ (weakening2 H Hs)
+  | Γ ⌞A ∧ B⌟ Δ (OrI₁ Γ A B H)         Hs := !OrI₁ (weakening2 H Hs)
+  | Γ ⌞A ∨ B⌟ Δ (OrI₂ Γ A B H)         Hs := !OrI₂ (weakening2 H Hs)
+  | Γ ⌞C⌟     Δ (OrE Γ A B C H₁ H₂ H₃) Hs :=
+       !OrE (weakening2 H₁ Hs) (weakening2 H₂ (cons_sub_cons A Hs)) (weakening2 H₃ (cons_sub_cons B Hs))
+
+end PropF

tests/lean/error_loc_bug.lean.expected.out

@@ -0,0 +1,8 @@
+error_loc_bug.lean:74:17: error: type mismatch at application
+  weakening2 (OrI₁ Γ A B H)
+term
+  OrI₁ Γ A B H
+has type
+  Γ ⊢ A ∨ B
+but is expected to have type
+  Γ ⊢ A ∧ B