feat(library/definitional/equations): add support for inaccessible patterns

src/frontends/lean/builtin_exprs.cpp

@@ -479,6 +479,10 @@ static expr parse_proof_qed(parser & p, unsigned, expr const *, pos_info const &
     return parse_proof_qed_core(p, pos);
 }
 
+static expr parse_inaccessible(parser & p, unsigned, expr const * args, pos_info const & pos) {
+    return p.save_pos(mk_inaccessible(args[0]), pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -492,6 +496,8 @@ parse_table init_nud_table() {
     r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0);
     r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);
     r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
+    r = r.add({transition("?(", Expr), transition(")", mk_ext_action(parse_inaccessible))}, x0);
+    r = r.add({transition("⌞", Expr), transition("⌟", mk_ext_action(parse_inaccessible))}, x0);
     r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
     r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
     r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);

src/frontends/lean/token_table.cpp

@@ -80,6 +80,7 @@ void init_token_table(token_table & t) {
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
+         {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0},
          {"<d", g_decreasing_prec}, {"local", 0}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
 
     char const * commands[] =

src/library/definitional/equations.cpp

@@ -7,11 +7,13 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/expr.h"
 #include "library/kernel_serializer.h"
+#include "library/annotation.h"
 
 namespace lean {
-static name * g_equations_name  = nullptr;
-static name * g_equation_name   = nullptr;
-static name * g_decreasing_name = nullptr;
+static name * g_equations_name    = nullptr;
+static name * g_equation_name     = nullptr;
+static name * g_decreasing_name   = nullptr;
+static name * g_inaccessible_name = nullptr;
 static std::string * g_equations_opcode  = nullptr;
 static std::string * g_equation_opcode   = nullptr;
 static std::string * g_decreasing_opcode = nullptr;
@@ -110,16 +112,21 @@ expr mk_equations(unsigned num, expr const * eqns, expr const & Hwf) {
     return mk_macro(*g_equations, args.size(), args.data());
 }
 
+expr mk_inaccessible(expr const & e) { return mk_annotation(*g_inaccessible_name, e); }
+bool is_inaccessible(expr const & e) { return is_annotation(e, *g_inaccessible_name); }
+
 void initialize_equations() {
     g_equations_name    = new name("equations");
     g_equation_name     = new name("equation");
     g_decreasing_name   = new name("decreasing");
+    g_inaccessible_name = new name("innaccessible");
     g_equations         = new macro_definition(new equations_macro_cell());
     g_equation          = new macro_definition(new equation_macro_cell());
     g_decreasing        = new macro_definition(new decreasing_macro_cell());
     g_equations_opcode  = new std::string("Eqns");
     g_equation_opcode   = new std::string("Eqn");
     g_decreasing_opcode = new std::string("Decr");
+    register_annotation(*g_inaccessible_name);
     register_macro_deserializer(*g_equations_opcode,
                                 [](deserializer &, unsigned num, expr const * args) {
                                     if (num == 0)
@@ -156,5 +163,6 @@ void finalize_equations() {
     delete g_equations_name;
     delete g_equation_name;
     delete g_decreasing_name;
+    delete g_inaccessible_name;
 }
 }

src/library/definitional/equations.h

@@ -26,6 +26,9 @@ expr const & equations_wf_proof(expr const & e);
 expr mk_equations(unsigned num, expr const * eqns);
 expr mk_equations(unsigned num, expr const * eqns, expr const & Hwf);
 
+expr mk_inaccessible(expr const & e);
+bool is_inaccessible(expr const & e);
+
 void initialize_equations();
 void finalize_equations();
 }