feat(frontends/lea): add commands for creating and managing rewrite rule sets

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/emacs/lean-mode.el

@@ -24,7 +24,7 @@
 (define-generic-mode
     'lean-mode     ;; name of the mode to create
   '("--")          ;; comments start with
-  '("import" "definition" "variable" "variables" "print" "theorem" "axiom" "universe" "alias" "help" "environment" "options" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "scope" "pop_scope" "set_opaque" "set_option") ;; some keywords
+  '("import" "definition" "variable" "variables" "print" "theorem" "axiom" "universe" "alias" "help" "environment" "options" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "scope" "pop_scope" "set_opaque" "set_option" "rewrite_set" "add_rewrite" "enable_rewrite" "disable_rewrite") ;; some keywords
   '(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
     ("\\_<\\(calc\\|have\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
     ("\"[^\"]*\"" . 'font-lock-string-face)

src/frontends/lean/parser_cmds.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/placeholder.h"
 #include "library/io_state_stream.h"
+#include "library/simplifier/rewrite_rule_set.h"
 #include "frontends/lean/parser_imp.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/pp.h"
@@ -52,12 +53,19 @@ static name g_builtin_kwd("builtin");
 static name g_namespace_kwd("namespace");
 static name g_end_kwd("end");
 static name g_using_kwd("using");
+static name g_rewrite_set_kwd("rewrite_set");
+static name g_add_rewrite_kwd("add_rewrite");
+static name g_enable_rewrite_kwd("enable_rewrite");
+static name g_disable_rewrite_kwd("disable_rewrite");
 /** \brief Table/List with all builtin command keywords */
-static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
+static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd,
+                                        g_axiom_kwd, g_universe_kwd, g_eval_kwd,
                                         g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd,
-                                        g_set_option_kwd, g_set_opaque_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd,
+                                        g_set_option_kwd, g_set_opaque_kwd, g_env_kwd, g_options_kwd,
+                                        g_import_kwd, g_help_kwd, g_coercion_kwd,
                                         g_exit_kwd, g_print_kwd, g_pop_kwd, g_scope_kwd, g_alias_kwd, g_builtin_kwd,
-                                        g_namespace_kwd, g_end_kwd, g_using_kwd};
+                                        g_namespace_kwd, g_end_kwd, g_using_kwd, g_rewrite_set_kwd, g_add_rewrite_kwd,
+                                        g_enable_rewrite_kwd, g_disable_rewrite_kwd};
 // ==========================================
 
 list<name> const & parser_imp::get_command_keywords() {
@@ -330,6 +338,16 @@ void parser_imp::parse_print() {
             }
         } else if (opt_id == g_options_kwd) {
             regular(m_io_state) << pp(m_io_state.get_options()) << endl;
+        } else if (opt_id == g_rewrite_set_kwd) {
+            name rsid;
+            if (curr_is_identifier()) {
+                rsid = curr_name();
+                next();
+            } else {
+                rsid = get_default_rewrite_rule_set_id();
+            }
+            rewrite_rule_set rs = get_rewrite_rule_set(m_env, rsid);
+            regular(m_io_state) << rs << endl;
         } else {
             throw parser_error("invalid Show command, expression, 'Options' or 'Environment' expected", m_last_cmd_pos);
         }
@@ -812,6 +830,47 @@ void parser_imp::parse_using() {
     regular(m_io_state) << endl;
 }
 
+void parser_imp::parse_rewrite_set() {
+    next();
+    name id = check_identifier_next("invalid rewrite set declaration, identifier expected");
+    mk_rewrite_rule_set(m_env, id);
+}
+
+void parser_imp::parse_ids_and_rsid(buffer<name> & ids, name & rsid) {
+    while (curr_is_identifier()) {
+        ids.push_back(curr_name());
+        next();
+    }
+    if (ids.empty())
+        throw parser_error("invalid command, at least one identifier expected", m_last_cmd_pos);
+    if (curr_is_colon()) {
+        next();
+        rsid = check_identifier_next("invalid command, rewrite set name expected");
+    } else {
+        rsid = get_default_rewrite_rule_set_id();
+    }
+}
+
+void parser_imp::parse_add_rewrite() {
+    next();
+    buffer<name> th_names;
+    name rsid;
+    parse_ids_and_rsid(th_names, rsid);
+    for (auto id : th_names) {
+        add_rewrite_rules(m_env, rsid, id);
+    }
+}
+
+void parser_imp::parse_enable_rewrite(bool flag) {
+    next();
+    buffer<name> ids;
+    name rsid;
+    parse_ids_and_rsid(ids, rsid);
+    for (auto id : ids) {
+        enable_rewrite_rules(m_env, rsid, id, flag);
+    }
+}
+
 /** \brief Parse a Lean command. */
 bool parser_imp::parse_command() {
     m_elaborator.clear();
@@ -872,6 +931,14 @@ bool parser_imp::parse_command() {
         parse_end();
     } else if (cmd_id == g_using_kwd) {
         parse_using();
+    } else if (cmd_id == g_rewrite_set_kwd) {
+        parse_rewrite_set();
+    } else if (cmd_id == g_add_rewrite_kwd) {
+        parse_add_rewrite();
+    } else if (cmd_id == g_enable_rewrite_kwd) {
+        parse_enable_rewrite(true);
+    } else if (cmd_id == g_disable_rewrite_kwd) {
+        parse_enable_rewrite(false);
     } else if (m_cmd_macros && m_cmd_macros->find(cmd_id) != m_cmd_macros->end()) {
         parse_cmd_macro(cmd_id, m_last_cmd_pos);
     } else {

src/frontends/lean/parser_imp.h

@@ -419,6 +419,10 @@ private:
     void parse_namespace();
     void parse_end();
     void parse_using();
+    void parse_rewrite_set();
+    void parse_ids_and_rsid(buffer<name> & ids, name & rsid);
+    void parse_add_rewrite();
+    void parse_enable_rewrite(bool flag);
     bool parse_command();
     void sync_command();
     /*@}*/

src/library/simplifier/rewrite_rule_set.cpp

@@ -103,6 +103,11 @@ format rewrite_rule_set::pp(formatter const & fmt, options const & opts) const {
     return r;
 }
 
+io_state_stream const & operator<<(io_state_stream const & out, rewrite_rule_set const & rs) {
+    out << mk_pair(rs.pp(out.get_formatter(), out.get_options()), out.get_options());
+    return out;
+}
+
 class mk_rewrite_rule_set_obj : public neutral_object_cell {
     name m_rule_set_id;
 public:

src/library/simplifier/rewrite_rule_set.h

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "util/name.h"
 #include "kernel/environment.h"
 #include "kernel/formatter.h"
+#include "library/io_state_stream.h"
 
 namespace lean {
 class rewrite_rule_set;
@@ -88,6 +89,7 @@ public:
     /** \brief Pretty print this rule set. */
     format pp(formatter const & fmt, options const & opts) const;
 };
+io_state_stream const & operator<<(io_state_stream const & out, rewrite_rule_set const & rs);
 
 name const & get_default_rewrite_rule_set_id();
 /**

src/library/simplifier/simplifier.cpp

@@ -694,13 +694,17 @@ static int simplify_core(lua_State * L, ro_shared_environment const & env) {
     if (nargs == 1) {
         rules.push_back(get_rewrite_rule_set(env));
     } else {
-        luaL_checktype(L, 2, LUA_TTABLE);
-        name r;
-        int n = objlen(L, 2);
-        for (int i = 1; i <= n; i++) {
-            lua_rawgeti(L, 2, i);
-            rules.push_back(get_rewrite_rule_set(env, to_name_ext(L, -1)));
-            lua_pop(L, 1);
+        if (lua_isstring(L, 2)) {
+            rules.push_back(get_rewrite_rule_set(env, to_name_ext(L, 2)));
+        } else {
+            luaL_checktype(L, 2, LUA_TTABLE);
+            name r;
+            int n = objlen(L, 2);
+            for (int i = 1; i <= n; i++) {
+                lua_rawgeti(L, 2, i);
+                rules.push_back(get_rewrite_rule_set(env, to_name_ext(L, -1)));
+                lua_pop(L, 1);
+            }
         }
     }
     context ctx;

tests/lean/simp.lean

@@ -0,0 +1,37 @@
+variable f : Nat → Nat
+variable g : Nat → Nat → Nat
+rewrite_set fgrules
+
+axiom Axf1 : ∀ x, f (f x) = x
+add_rewrite Axf1 : fgrules
+
+axiom Axfg : ∀ x, g x x = x
+add_rewrite Axfg : fgrules
+
+variables a b : Nat
+
+print rewrite_set fgrules
+
+(*
+local t = parse_lean('g a (f (f a))')
+print(simplify(t, {'fgrules'}))
+*)
+
+disable_rewrite Axfg : fgrules
+
+(*
+local t = parse_lean('g a (f (f a))')
+print(simplify(t, {'fgrules'}))
+*)
+
+enable_rewrite Axfg : fgrules
+
+(*
+local t = parse_lean('g a (f (f a))')
+print(simplify(t, {'fgrules'}))
+*)
+
+(*
+local t = parse_lean('g a (f (f a))')
+print(simplify(t, 'fgrules'))
+*)

tests/lean/simp.lean.expected.out

@@ -0,0 +1,14 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+  Assumed: g
+  Assumed: Axf1
+  Assumed: Axfg
+  Assumed: a
+  Assumed: b
+Axfg : ∀ x : ℕ, g x x = x
+Axf1 : ∀ x : ℕ, f (f x) = x
+a	trans (congr2 (g a) (Axf1 a)) (Axfg a)
+g a a	congr2 (g a) (Axf1 a)
+a	trans (congr2 (g a) (Axf1 a)) (Axfg a)
+a	trans (congr2 (g a) (Axf1 a)) (Axfg a)