fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant

src/frontends/lean/builtin_exprs.cpp

@@ -128,7 +128,7 @@ static environment open_tactic_namespace(parser & p) {
 }
 
 static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
-    parser::no_undef_id_error_scope scope(p);
+    parser::undef_id_to_local_scope scope(p);
     environment env = open_tactic_namespace(p);
     expr t = p.parse_scoped_expr(0, nullptr, env);
     return p.mk_by(t, pos);
@@ -140,7 +140,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
     optional<expr> pre_tac = get_begin_end_pre_tactic(p.env());
     buffer<expr> tacs;
     bool first = true;
-    parser::no_undef_id_error_scope scope(p);
+    parser::undef_id_to_local_scope scope(p);
     environment env = open_tactic_namespace(p);
     while (!p.curr_is_token(get_end_tk())) {
         if (first) {

src/frontends/lean/inductive_cmd.cpp

@@ -698,7 +698,7 @@ struct inductive_cmd_fn {
     }
 
     environment operator()() {
-        parser::no_undef_id_error_scope err_scope(m_p);
+        parser::undef_id_to_const_scope err_scope(m_p);
         buffer<inductive_decl> decls;
         {
             parser::local_scope scope(m_p);

src/frontends/lean/parser.cpp

@@ -75,12 +75,10 @@ parser::local_scope::~local_scope() {
     m_p.m_env = m_env;
 }
 
-parser::no_undef_id_error_scope::no_undef_id_error_scope(parser & p):m_p(p), m_old(m_p.m_no_undef_id_error) {
-    m_p.m_no_undef_id_error = true;
-}
-parser::no_undef_id_error_scope::~no_undef_id_error_scope() {
-    m_p.m_no_undef_id_error = m_old;
-}
+parser::undef_id_to_const_scope::undef_id_to_const_scope(parser & p):
+    flet<undef_id_behavior>(p.m_undef_id_behavior, undef_id_behavior::AssumeConstant) {}
+parser::undef_id_to_local_scope::undef_id_to_local_scope(parser & p):
+    flet<undef_id_behavior>(p.m_undef_id_behavior, undef_id_behavior::AssumeLocal) {}
 
 static name * g_tmp_prefix = nullptr;
 
@@ -104,7 +102,7 @@ parser::parser(environment const & env, io_state const & ios,
         m_parser_scope_stack = s->m_parser_scope_stack;
     }
     m_num_threads = num_threads;
-    m_no_undef_id_error = false;
+    m_undef_id_behavior = undef_id_behavior::Error;
     m_found_errors = false;
     m_used_sorry = false;
     updt_options();
@@ -1067,8 +1065,12 @@ expr parser::id_to_expr(name const & id, pos_info const & p) {
         r = save_pos(mk_choice(new_as.size(), new_as.data()), p);
         save_overload(*r);
     }
-    if (!r && m_no_undef_id_error)
-        r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
+    if (!r) {
+        if (m_undef_id_behavior == undef_id_behavior::AssumeConstant)
+            r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p);
+        else if (m_undef_id_behavior == undef_id_behavior::AssumeLocal)
+            r = save_pos(mk_local(id, mk_expr_placeholder()), p);
+    }
     if (!r)
         throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
     save_type_info(*r);

src/frontends/lean/parser.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include <utility>
 #include <vector>
+#include "util/flet.h"
 #include "util/script_state.h"
 #include "util/name_map.h"
 #include "util/exception.h"
@@ -80,6 +81,8 @@ typedef std::vector<snapshot> snapshot_vector;
 
 enum class keep_theorem_mode { All, DiscardImported, DiscardAll };
 
+enum class undef_id_behavior { Error, AssumeConstant, AssumeLocal };
+
 class parser {
     environment             m_env;
     io_state                m_ios;
@@ -105,7 +108,7 @@ class parser {
     // By default, when the parser finds a unknown identifier, it signs an error.
     // When the following flag is true, it creates a constant.
     // This flag is when we are trying to parse mutually recursive declarations.
-    bool                    m_no_undef_id_error;
+    undef_id_behavior       m_undef_id_behavior;
     optional<bool>          m_has_num;
     optional<bool>          m_has_string;
     optional<bool>          m_has_tactic_decls;
@@ -371,11 +374,13 @@ public:
     /** \brief Return all local level declarations */
     list<pair<name, level>> const & get_local_level_entries() const { return m_local_level_decls.get_entries(); }
     /** \brief By default, when the parser finds a unknown identifier, it signs an error.
-        This scope object temporarily changes this behavior. In any scope where this object
-        is declared, the parse creates a constant even when the identifier is unknown.
-        This behavior is useful when we are trying to parse mutually recursive declarations.
+        These scope objects temporarily change this behavior. In any scope where this object
+        is declared, the parse creates a constant/local even when the identifier is unknown.
+        This behavior is useful when we are trying to parse mutually recursive declarations and
+        tactics.
     */
-    struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); };
+    struct undef_id_to_const_scope : public flet<undef_id_behavior> { undef_id_to_const_scope(parser & p); };
+    struct undef_id_to_local_scope : public flet<undef_id_behavior> { undef_id_to_local_scope(parser &); };
 
     /** \brief Elaborate \c e, and tolerate metavariables in the result. */
     std::tuple<expr, level_param_names> elaborate_relaxed(expr const & e, list<expr> const & ctx = list<expr>());

tests/lean/run/tree2.lean

@@ -0,0 +1,84 @@
+import logic data.prod
+open eq.ops prod tactic
+
+inductive tree (A : Type) :=
+leaf : A → tree A,
+node : tree A → tree A → tree A
+
+inductive one.{l} : Type.{max 1 l} :=
+star : one
+
+set_option pp.universes true
+
+namespace tree
+  section
+    universe variables l₁ l₂
+    variable {A : Type.{l₁}}
+    variable (C : tree A → Type.{l₂})
+    definition below (t : tree A) : Type :=
+    rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂)
+  end
+
+  section
+    universe variables l₁ l₂
+    variable {A : Type.{l₁}}
+    variable {C : tree A → Type.{l₂}}
+    definition below_rec_on (t : tree A) (H : Π (n : tree A), below C n → C n) : C t
+    := have general : C t × below C t, from
+        rec_on t
+          (λa, (H (leaf a) one.star, one.star))
+          (λ (l r : tree A) (Hl : C l × below C l) (Hr : C r × below C r),
+            have b : below C (node l r), from
+              (pr₁ Hl, pr₁ Hr, pr₂ Hl, pr₂ Hr),
+            have c : C (node l r), from
+              H (node l r) b,
+            (c, b)),
+       pr₁ general
+  end
+
+  definition no_confusion_type {A : Type} (P : Type) (t₁ t₂ : tree A) : Type :=
+  cases_on t₁
+   (λ a₁, cases_on t₂
+     (λ a₂,    (a₁ = a₂ → P) → P)
+     (λ l₂ r₂, P))
+   (λ l₁ r₁, cases_on t₂
+     (λ a₂,    P)
+     (λ l₂ r₂, (l₁ = l₂ → r₁ = r₂ → P) → P))
+
+  set_option pp.universes true
+  check no_confusion_type
+
+  definition no_confusion {A : Type} {P : Type} {t₁ t₂ : tree A} : t₁ = t₂ → no_confusion_type P t₁ t₂ :=
+  assume e₁ : t₁ = t₂,
+    have aux₁ : t₁ = t₁ → no_confusion_type P t₁ t₁, from
+      take h, cases_on t₁
+        (λ a,   assume h : a = a → P, h (eq.refl a))
+        (λ l r, assume h : l = l → r = r → P, h (eq.refl l) (eq.refl r)),
+    eq.rec aux₁ e₁ e₁
+
+  check no_confusion
+
+  theorem leaf_ne_tree {A : Type} (a : A) (l r : tree A) : leaf a ≠ node l r :=
+  assume h : leaf a = node l r,
+  no_confusion h
+
+  constant A : Type₁
+  constants l₁ l₂ r₁ r₂ : tree A
+  axiom node_eq : node l₁ r₁ = node l₂ r₂
+  check no_confusion node_eq
+
+  definition tst : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂ := no_confusion node_eq
+  check tst (λ e₁ e₂, e₁)
+
+  theorem node.inj1 {A : Type} (l₁ l₂ r₁ r₂ : tree A) : node l₁ r₁ = node l₂ r₂ → l₁ = l₂ :=
+  assume h,
+    have trivial : (l₁ = l₂ → r₁ = r₂ → l₁ = l₂) → l₁ = l₂, from no_confusion h,
+    trivial (λ e₁ e₂, e₁)
+
+  theorem node.inj2 {A : Type} (l₁ l₂ r₁ r₂ : tree A) : node l₁ r₁ = node l₂ r₂ → l₁ = l₂ :=
+  begin
+    intro h,
+    apply (no_confusion h),
+    intros, assumption
+  end
+end tree