feat(frontends/lean): add calc_subst, calc_refl, calc_trans commands for configuring calc-expressions

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

src/frontends/lean/builtin_cmds.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/private.h"
 #include "library/locals.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/calc.h"
 #include "frontends/lean/notation_cmd.h"
 
 namespace lean {
@@ -517,6 +518,7 @@ cmd_table init_cmd_table() {
     add_cmd(r, cmd_info("postfix",      "declare a new postfix notation", postfix_cmd));
     add_cmd(r, cmd_info("notation",     "declare a new notation", notation_cmd));
     add_cmd(r, cmd_info("#setline",     "modify the current line number, it only affects error/report messages", set_line_cmd));
+    register_calc_cmds(r);
     return r;
 }
 

src/frontends/lean/calc.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/buffer.h"
 #include "kernel/environment.h"
 #include "library/module.h"
+#include "frontends/lean/parser.h"
 
 namespace lean {
 struct calc_ext : public environment_extension {
@@ -144,4 +145,25 @@ static void calc_trans_reader(deserializer & d, module_idx, shared_environment &
         });
 }
 register_module_object_reader_fn g_calc_trans_reader(g_calc_trans_key, calc_trans_reader);
+
+environment calc_subst_cmd(parser & p) {
+    name id = p.check_id_next("invalid 'calc_subst' command, identifier expected");
+    return add_calc_subst(p.env(), id);
+}
+
+environment calc_refl_cmd(parser & p) {
+    name id = p.check_id_next("invalid 'calc_refl' command, identifier expected");
+    return add_calc_refl(p.env(), id);
+}
+
+environment calc_trans_cmd(parser & p) {
+    name id = p.check_id_next("invalid 'calc_trans' command, identifier expected");
+    return add_calc_trans(p.env(), id);
+}
+
+void register_calc_cmds(cmd_table & r) {
+    add_cmd(r, cmd_info("calc_subst",     "set the substitution rule that is used by the calculational proof '{...}' notation", calc_subst_cmd));
+    add_cmd(r, cmd_info("calc_refl",      "set the reflexivity rule for an operator, this command is relevant for the calculational proof '{...}' notation", calc_refl_cmd));
+    add_cmd(r, cmd_info("calc_trans",     "set the transitivity rule for a pair of operators, this command is relevant for the calculational proof '{...}' notation", calc_trans_cmd));
+}
 }

src/frontends/lean/calc.h

@@ -5,10 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "kernel/environment.h"
-
+#include "frontends/lean/cmd_table.h"
 namespace lean {
-environment add_calc_subst(environment const & env, name const & subst);
-environment add_calc_refl(environment const & env, name const & refl);
-environment add_calc_trans(environment const & env, name const & trans);
+void register_calc_cmds(cmd_table & r);
 }

src/frontends/lean/parser.h

@@ -117,7 +117,6 @@ class parser {
     expr parse_nud_notation();
     expr parse_led_notation(expr left);
     expr parse_nud();
-    expr parse_led(expr left);
     expr parse_id();
     expr parse_numeral_expr();
     expr parse_decimal_expr();
@@ -209,6 +208,7 @@ public:
     local_environment parse_binders(buffer<parameter> & r);
 
     expr parse_expr(unsigned rbp = 0);
+    expr parse_led(expr left);
     expr parse_scoped_expr(unsigned num_params, parameter const * ps, local_environment const & lenv, unsigned rbp = 0);
     expr parse_scoped_expr(buffer<parameter> & ps, local_environment const & lenv, unsigned rbp = 0) {
         return parse_scoped_expr(ps.size(), ps.data(), lenv, rbp);

src/frontends/lean/token_table.cpp

@@ -66,7 +66,7 @@ token_table init_token_table() {
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "abbreviation", "inductive", "record", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "notation", "exit", "set_option",
-                               "using", "#setline", nullptr};
+                               "using", "calc_subst", "calc_refl", "calc_trans", "#setline", nullptr};
 
     std::pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

tests/lean/calc1.lean

@@ -0,0 +1,18 @@
+variable A : Type.{1}
+definition [inline] bool : Type.{1} := Type.{0}
+variable eq : A → A → bool
+infixl `=` 50 := eq
+variable subst (P : A → bool) (a b : A) (H1 : a = b) (H2 : P a) : P b
+variable eq_trans (a b c : A) (H1 : a = b) (H2 : b = c) : a = c
+variable eq_refl (a : A) : a = a
+variable le : A → A → bool
+infixl `≤` 50 := le
+variable le_trans (a b c : A) (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
+variable le_refl (a : A) : a ≤ a
+variable eq_le_trans (a b c : A) (H1 : a = b) (H2 : b ≤ c) : a ≤ c
+calc_subst subst
+calc_refl  eq_refl
+calc_refl  le_refl
+calc_trans eq_trans
+calc_trans le_trans
+calc_trans eq_le_trans