test(frontends/lean): add #replace command for debugging purposes

src/frontends/lean/builtin_cmds.cpp

@@ -41,6 +41,7 @@ Author: Leonardo de Moura
 #include "library/decl_stats.h"
 #include "library/app_builder.h"
 #include "library/meng_paulson.h"
+#include "library/fun_info_manager.h"
 #include "library/definitional/projection.h"
 #include "library/simplifier/simp_rule_set.h"
 #include "compiler/preprocess_rec.h"
@@ -1242,6 +1243,42 @@ static environment trans_cmd(parser & p) {
     return env;
 }
 
+static void parse_expr_vector(parser & p, buffer<expr> & r) {
+    p.check_token_next(get_lbracket_tk(), "invalid command, '[' expected");
+    while (true) {
+        expr e; level_param_names ls;
+        std::tie(e, ls) = parse_local_expr(p);
+        r.push_back(e);
+        if (!p.curr_is_token(get_comma_tk()))
+            break;
+        p.next();
+    }
+    p.check_token_next(get_rbracket_tk(), "invalid command, ']' expected");
+}
+
+static environment replace_cmd(parser & p) {
+    environment const & env = p.env();
+    auto pos = p.pos();
+    app_builder b(env);
+    expr e; level_param_names ls;
+    buffer<expr> from;
+    buffer<expr> to;
+    std::tie(e, ls) =  parse_local_expr(p);
+    p.check_token_next(get_comma_tk(), "invalid #replace command, ',' expected");
+    parse_expr_vector(p, from);
+    p.check_token_next(get_comma_tk(), "invalid #replace command, ',' expected");
+    parse_expr_vector(p, to);
+    if (from.size() != to.size())
+        throw parser_error("invalid #replace command, from/to vectors have different size", pos);
+    tmp_type_context ctx(env, p.ios());
+    fun_info_manager infom(ctx);
+    auto r = replace(infom, e, from, to);
+    if (!r)
+        throw parser_error("#replace commad failed", pos);
+    p.regular_stream() << *r << "\n";
+    return env;
+}
+
 void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("open",              "create aliases for declarations, and use objects defined in other namespaces",
                         open_cmd));
@@ -1270,6 +1307,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#trans",            "(for debugging purposes)", trans_cmd));
     add_cmd(r, cmd_info("#symm",             "(for debugging purposes)", symm_cmd));
     add_cmd(r, cmd_info("#compile",          "(for debugging purposes)", compile_cmd));
+    add_cmd(r, cmd_info("#replace",          "(for debugging purposes)", replace_cmd));
     add_cmd(r, cmd_info("#accessible",       "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
     add_cmd(r, cmd_info("#decl_stats",       "(for debugging purposes) display declaration statistics", decl_stats_cmd));
     add_cmd(r, cmd_info("#relevant_thms",    "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd));

src/frontends/lean/token_table.cpp

@@ -119,7 +119,7 @@ void init_token_table(token_table & t) {
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
-         "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#app_builder", "#refl", "#symm", "#trans", nullptr};
+         "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#app_builder", "#refl", "#symm", "#trans", "#replace", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

tests/lean/replace1.lean

@@ -0,0 +1,41 @@
+constant f : Π {A : Type}, A → A → A
+variables a b c : nat
+variables H : a = b
+
+set_option pp.all true
+
+#replace f a a, [a], [b]
+#replace f (f a b) b, [a,b], [b,a]
+
+variables x y : bool
+
+-- [nat] and [bool] are instances of the telescope (A : Type),
+-- but the resulting expression is type incorrect.
+-- Thus, #replace correctly detects the error.
+#replace f a a, [nat], [bool] -- Error
+-- An error is not detected in the following one,
+-- since there is no telescope s.t., [a] and [x] are instances of.
+#replace f a a, [a], [x]
+-- The following should work, [nat, a] and [bool, x] are instances
+-- of the telescope (A : Type, a : A), and the result is type correct
+#replace f a a, [nat, a], [bool, x]
+
+variable p : nat → Prop
+variable H1 : p a
+
+-- [b] and [a] are instances of the telescope (x : nat),
+-- but the resulting expression is type incorrect.
+-- Thus, #replace correctly detects the error.
+#replace @eq.rec nat a (λ x : nat, p x) H1 b H, [b], [a]         -- Error
+-- There is no telescope s.t. [H] and [eq.refl a] are instances of.
+#replace @eq.rec nat a (λ x : nat, p x) H1 b H, [H], [eq.refl a]
+-- [b, H] and [a, eq.refl a] are both instances of the telescope
+-- (x : nat, H : a = x), and the resulting expression is type correct
+#replace @eq.rec nat a (λ x : nat, p x) H1 b H, [b, H], [a, eq.refl a]
+
+constant bv : nat → Type₁
+
+variables v₁ v₂ : bv 10
+
+#replace v₁ = v₂, [(10:nat)], [(11:nat)] -- Error
+#replace (λ v₁ v₂ : bv 10, v₁ = v₂), [(10:nat)], [(11:nat)]

tests/lean/replace1.lean.expected.out

@@ -0,0 +1,10 @@
+@f.{1} nat b b
+@f.{1} nat (@f.{1} nat b a) a
+replace1.lean:15:9: error: #replace commad failed
+@f.{1} nat x x
+@f.{1} bool x x
+replace1.lean:29:9: error: #replace commad failed
+@eq.rec.{0 1} nat a (λ (x : nat), p x) H1 b (@eq.refl.{1} nat a)
+@eq.rec.{0 1} nat a (λ (x : nat), p x) H1 a (@eq.refl.{1} nat a)
+replace1.lean:40:9: error: #replace commad failed
+λ (v₁ v₂ : bv 11), @eq.{1} (bv 11) v₁ v₂