feat(frontends/lean/parser): expr patterns

library/init/meta/contradiction_tactic.lean

@@ -50,12 +50,13 @@ private meta def contra_not_a_refl_rel_a : list expr → tactic unit
      <|>
      contra_not_a_refl_rel_a Hs
 
+set_option eqn_compiler.max_steps 256
 private meta def contra_constructor_eq : list expr → tactic unit
 | []        := failed
 | (H :: Hs) :=
   do t ← infer_type H >>= whnf,
-     match (is_eq t) with
-     | (some (lhs_0, rhs_0)) :=
+     match t with
+     | ``((%%lhs_0 : %%α) = %%rhs_0) :=
        do env ← get_env,
           lhs ← whnf lhs_0,
           rhs ← whnf rhs_0,
@@ -67,7 +68,7 @@ private meta def contra_constructor_eq : list expr → tactic unit
                   pr ← mk_app (I_name <.> "no_confusion") [tgt, lhs, rhs, H],
                   exact pr
           else contra_constructor_eq Hs
-     | none := contra_constructor_eq Hs
+     | _ := contra_constructor_eq Hs
      end
 
 meta def contradiction : tactic unit :=

library/init/meta/expr.lean

@@ -212,23 +212,23 @@ is_constant_of (get_app_fn e) n
 meta def is_napp_of (e : expr) (c : name) (n : nat) : bool :=
 is_app_of e c ∧ get_app_num_args e = n
 
-meta def is_false (e : expr) : bool :=
-is_constant_of e `false
+meta def is_false : expr → bool
+| ``(false) := tt
+| _         := ff
 
+set_option eqn_compiler.max_steps 256
 meta def is_not : expr → option expr
-| (app f a)     := if is_constant_of f `not then some a else none
-| (pi n bi a b) := if is_false b then some a else none
-| e             := none
+| ``(not %%a)     := some a
+| ``(%%a → false) := some a
+| e               := none
 
-meta def is_eq (e : expr) : option (expr × expr) :=
-if is_napp_of e `eq 3
-then some (app_arg (app_fn e), app_arg e)
-else none
+meta def is_eq : expr → option (expr × expr)
+| ``((%%a: %%α) = %%b) := some (a, b)
+| _                    := none
 
-meta def is_ne (e : expr) : option (expr × expr) :=
-if is_napp_of e `ne 3
-then some (app_arg (app_fn e), app_arg e)
-else none
+meta def is_ne : expr → option (expr × expr)
+| ``((%%a: %%α) ≠ %%b) := some (a, b)
+| _                    := none
 
 meta def is_bin_arith_app (e : expr) (op : name) : option (expr × expr) :=
 if is_napp_of e op 4
@@ -247,13 +247,10 @@ is_bin_arith_app e `le
 meta def is_ge (e : expr) : option (expr × expr) :=
 is_bin_arith_app e `ge
 
-meta def is_heq (e : expr) : option (expr × expr × expr × expr) :=
-if is_napp_of e `heq 4
-then some (app_arg (app_fn (app_fn (app_fn e))),
-           app_arg (app_fn (app_fn e)),
-           app_arg (app_fn e),
-           app_arg e)
-else none
+set_option eqn_compiler.max_steps 512
+meta def is_heq : expr → option (expr × expr × expr × expr)
+| ``(@heq %%α %%a %%β %%b) := some (α, a, β, b)
+| _                        := none
 
 meta def is_pi : expr → bool
 | (pi _ _ _ _) := tt

library/init/meta/mk_dec_eq_instance.lean

@@ -127,3 +127,7 @@ do env ← get_env,
    mk_dec_eq_instance_core
 
 end tactic
+
+/- instances of types in dependent files -/
+instance : decidable_eq ordering :=
+by tactic.mk_dec_eq_instance

script/gen_constants_cpp.py

@@ -33,10 +33,11 @@ def main(argv=None):
     if argv is None:
         argv = sys.argv[1:]
     infile        = argv[0]
-    basename, ext = os.path.splitext(infile)
-    cppfile       = basename + ".cpp"
-    hfile         = basename + ".h"
-    tst_file      = "../../tests/lean/run/check_" + basename + ".lean"
+    basedir, name = os.path.split(infile)
+    basename, ext = os.path.splitext(name)
+    cppfile       = os.path.join(basedir, basename + ".cpp")
+    hfile         = os.path.join(basedir, basename + ".h")
+    tst_file      = os.path.join(basedir, "../../tests/lean/run/check_" + basename + ".lean")
     constants     = []
     with open(infile, 'r') as f:
         for line in f:

src/frontends/lean/elaborator.cpp

@@ -2272,7 +2272,7 @@ class validate_equation_lhs_fn : public replace_visitor {
     virtual expr visit_app(expr const & e) override {
         expr it = e;
         while (true) {
-            if (is_nat_int_char_string_value(ctx(), it))
+            if (is_nat_int_char_string_name_value(ctx(), it))
                 return e;
             if (!is_app(it) && !is_constant(it))
                 return visit(it);

src/frontends/lean/parser.cpp

@@ -109,11 +109,14 @@ parser::local_scope::~local_scope() {
     m_p.m_env = m_env;
 }
 
+LEAN_THREAD_VALUE(id_behavior, g_outer_id_behavior, id_behavior::ErrorIfUndef);
+
 parser::quote_scope::quote_scope(parser & p, bool q, id_behavior i):
     m_p(p), m_id_behavior(m_p.m_id_behavior), m_old_in_quote(m_p.m_in_quote), m_in_quote(q),
     m_saved_in_pattern(p.m_in_pattern) {
     m_p.m_in_pattern = false;
     if (m_in_quote && !m_old_in_quote) {
+        g_outer_id_behavior = m_p.m_id_behavior;
         m_p.m_id_behavior = i;
         m_p.m_in_quote = true;
         m_p.push_local_scope(false);
@@ -122,7 +125,7 @@ parser::quote_scope::quote_scope(parser & p, bool q, id_behavior i):
             m_p.clear_expr_locals();
     } else if (!m_in_quote && m_old_in_quote) {
         lean_assert(m_p.m_quote_stack);
-        m_p.m_id_behavior = id_behavior::ErrorIfUndef;
+        m_p.m_id_behavior = g_outer_id_behavior;
         m_p.push_local_scope(false);
         m_p.m_in_quote = false;
         m_p.restore_parser_scope(head(m_p.m_quote_stack));
@@ -1712,9 +1715,95 @@ struct to_pattern_fn {
     }
 };
 
+static expr quote(unsigned u) {
+    return mk_app(mk_constant(get_char_of_nat_name()), mk_prenum(mpz(u)));
+}
+
+static expr quote(char const * str) {
+    return from_string(str);
+}
+
+static expr quote(name const & n) {
+    switch (n.kind()) {
+        case name_kind::ANONYMOUS:
+            return mk_constant({"name", "anonymous"});
+        case name_kind::NUMERAL:
+            return mk_app(mk_constant({"name", "mk_numeral"}), quote(n.get_numeral()), quote(n.get_prefix()));
+        case name_kind::STRING:
+            return mk_app(mk_constant({"name", "mk_string"}), quote(n.get_string()), quote(n.get_prefix()));
+    }
+    lean_unreachable();
+}
+
+static expr quote(expr const & e) {
+    switch (e.kind()) {
+        case expr_kind::Var:
+            return mk_app(mk_constant({"expr", "var"}), quote(var_idx(e)));
+        case expr_kind::Sort:
+            return mk_app(mk_constant({"expr", "sort"}), /* level */ mk_expr_placeholder());
+        case expr_kind::Constant:
+            return mk_app(mk_constant({"expr", "const"}), quote(const_name(e)), /* levels */ mk_expr_placeholder());
+        case expr_kind::Meta:
+            lean_unreachable();
+        case expr_kind::Local:
+            // pattern variable
+            return update_mlocal(e, mk_constant("expr"));
+        case expr_kind::App:
+            return mk_app(mk_constant({"expr", "app"}), quote(app_fn(e)), quote(app_arg(e)));
+        case expr_kind::Lambda:
+            return mk_app(mk_constant({"expr", "lam"}), quote(binding_name(e)), /* binding info */ mk_expr_placeholder(),
+                          quote(binding_domain(e)), quote(binding_body(e)));
+        case expr_kind::Pi:
+            return mk_app(mk_constant({"expr", "pi"}), quote(binding_name(e)), /* binding info */ mk_expr_placeholder(),
+                          quote(binding_domain(e)), quote(binding_body(e)));
+        case expr_kind::Let:
+            return mk_app(mk_constant({"expr", "let"}), quote(let_name(e)), quote(let_type(e)), quote(let_value(e)),
+                          quote(let_body(e)));
+        case expr_kind::Macro:
+            if (is_typed_expr(e))
+                return mk_typed_expr(quote(get_typed_expr_expr(e)), quote(get_typed_expr_type(e)));
+            throw parser_error("invalid quotation pattern, macros are not supported",
+                               get_pos_info_provider()->get_pos_info_or_some(e));
+    }
+    lean_unreachable();
+}
+
+static expr preprocess_quote_pattern(parser const & p, expr e) {
+    buffer<expr> aqs;
+    while (is_app_of(e, get_pexpr_subst_name())) {
+        expr arg1 = app_arg(app_fn(e));
+        expr arg2 = app_arg(e);
+        lean_assert(is_app_of(arg2, get_to_pexpr_name()));
+        aqs.push_back(app_arg(arg2));
+        e = arg1;
+    }
+    e = get_quote_expr(e);
+
+    metavar_context ctx;
+    local_context lctx;
+    elaborator elab(p.env(), p.get_options(), "_quotation_pattern", ctx, lctx, false);
+    e = elab.elaborate(e);
+
+    for (int i = aqs.size() - 1; i >= 0; i--) {
+        if (!is_local(aqs[i]))
+            throw parser_error("invalid quotation pattern, antiquotation must be a single variable", p.pos_of(aqs[i]));
+        e = instantiate(binding_body(e), aqs[i]);
+    }
+    return quote(e);
+}
+
 expr parser::patexpr_to_pattern(expr const & pat_or_expr, bool skip_main_fn, buffer<expr> & new_locals) {
     undef_id_to_local_scope scope(*this);
-    return to_pattern_fn(*this, new_locals)(pat_or_expr, skip_main_fn);
+    auto e = replace(pat_or_expr, [&](expr const & e) {
+        if (is_quote(e)) {
+            return some(preprocess_quote_pattern(*this, e));
+        } else if (is_app_of(e, get_pexpr_subst_name())) {
+            return some(preprocess_quote_pattern(*this, e));
+        } else {
+            return none_expr();
+        }
+    });
+    return to_pattern_fn(*this, new_locals)(e, skip_main_fn);
 }
 
 expr parser::parse_pattern_or_expr(unsigned rbp) {

src/library/constants.cpp

@@ -179,6 +179,7 @@ name const * g_mul_one = nullptr;
 name const * g_mul_zero = nullptr;
 name const * g_mul_zero_class = nullptr;
 name const * g_name_anonymous = nullptr;
+name const * g_name_mk_numeral = nullptr;
 name const * g_name_mk_string = nullptr;
 name const * g_nat = nullptr;
 name const * g_nat_of_num = nullptr;
@@ -550,6 +551,7 @@ void initialize_constants() {
     g_mul_zero = new name{"mul_zero"};
     g_mul_zero_class = new name{"mul_zero_class"};
     g_name_anonymous = new name{"name", "anonymous"};
+    g_name_mk_numeral = new name{"name", "mk_numeral"};
     g_name_mk_string = new name{"name", "mk_string"};
     g_nat = new name{"nat"};
     g_nat_of_num = new name{"nat", "of_num"};
@@ -922,6 +924,7 @@ void finalize_constants() {
     delete g_mul_zero;
     delete g_mul_zero_class;
     delete g_name_anonymous;
+    delete g_name_mk_numeral;
     delete g_name_mk_string;
     delete g_nat;
     delete g_nat_of_num;
@@ -1293,6 +1296,7 @@ name const & get_mul_one_name() { return *g_mul_one; }
 name const & get_mul_zero_name() { return *g_mul_zero; }
 name const & get_mul_zero_class_name() { return *g_mul_zero_class; }
 name const & get_name_anonymous_name() { return *g_name_anonymous; }
+name const & get_name_mk_numeral_name() { return *g_name_mk_numeral; }
 name const & get_name_mk_string_name() { return *g_name_mk_string; }
 name const & get_nat_name() { return *g_nat; }
 name const & get_nat_of_num_name() { return *g_nat_of_num; }

src/library/constants.h

@@ -181,6 +181,7 @@ name const & get_mul_one_name();
 name const & get_mul_zero_name();
 name const & get_mul_zero_class_name();
 name const & get_name_anonymous_name();
+name const & get_name_mk_numeral_name();
 name const & get_name_mk_string_name();
 name const & get_nat_name();
 name const & get_nat_of_num_name();

src/library/constants.txt

@@ -174,6 +174,7 @@ mul_one
 mul_zero
 mul_zero_class
 name.anonymous
+name.mk_numeral
 name.mk_string
 nat
 nat.of_num

src/library/equations_compiler/elim_match.cpp

@@ -285,7 +285,7 @@ struct elim_match_fn {
     bool is_value(type_context & ctx, expr const & e) {
         try {
             if (!m_use_ite) return false;
-            if (is_nat_int_char_string_value(ctx, e)) return true;
+            if (is_nat_int_char_string_name_value(ctx, e)) return true;
             // TODO(Leo, Sebastian): decide whether we ever want to have this behavior back
             // if (optional<name> I_name = is_constructor(e)) return is_nontrivial_enum(*I_name);
             return false;

src/library/equations_compiler/util.cpp

@@ -583,8 +583,20 @@ environment mk_simple_equation_lemma_for(environment const & env, options const
     return add_equation_lemma(env, opts, metavar_context(), ctx.lctx(), is_private, eqn_name, eqn_type, eqn_proof);
 }
 
-bool is_nat_int_char_string_value(type_context & ctx, expr const & e) {
-    if (to_char(ctx, e) || to_string(e)) return true;
+bool is_name_value(expr const & e) {
+    if (is_constant(e, get_name_anonymous_name()))
+        return true;
+    buffer<expr> args;
+    expr const & fn = get_app_args(e, args);
+    if (is_constant(fn, get_name_mk_string_name()) && args.size() == 2)
+        return is_string_value(args[0]) && is_name_value(args[1]);
+    if (is_constant(fn, get_name_mk_numeral_name()) && args.size() == 2)
+        return is_num(args[0]) && is_name_value(args[1]);
+    return false;
+}
+
+bool is_nat_int_char_string_name_value(type_context & ctx, expr const & e) {
+    if (is_char_value(ctx, e) || is_string_value(e) || is_name_value(e)) return true;
     if (is_signed_num(e)) {
         expr type = ctx.infer(e);
         if (ctx.is_def_eq(type, mk_nat_type()) || ctx.is_def_eq(type, mk_int_type()))

src/library/equations_compiler/util.h

@@ -101,7 +101,7 @@ environment mk_simple_equation_lemma_for(environment const & env, options const
 name mk_equation_name(name const & f_name, unsigned eqn_idx);
 
 /* Return true iff e is a nat, int, char or string value. */
-bool is_nat_int_char_string_value(type_context & ctx, expr const & e);
+bool is_nat_int_char_string_name_value(type_context & ctx, expr const & e);
 
 /* Given a variable (x : I A idx), where (I A idx) is an inductive datatype,
    for each constructor c of (I A idx), this function invokes fn(t, new_vars) where t is of the form (c A ...),

tests/lean/run/check_constants.lean

@@ -179,6 +179,7 @@ run_command script_check_id `mul_one
 run_command script_check_id `mul_zero
 run_command script_check_id `mul_zero_class
 run_command script_check_id `name.anonymous
+run_command script_check_id `name.mk_numeral
 run_command script_check_id `name.mk_string
 run_command script_check_id `nat
 run_command script_check_id `nat.of_num