From 2482c497293f6118bf05fb2ed0aa2aacd563bb81 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Nov 2015 22:02:00 -0800 Subject: [PATCH] test(frontends/lean): add #replace command for debugging purposes --- src/frontends/lean/builtin_cmds.cpp | 38 +++++++++++++++++++++++++ src/frontends/lean/token_table.cpp | 2 +- tests/lean/replace1.lean | 41 +++++++++++++++++++++++++++ tests/lean/replace1.lean.expected.out | 10 +++++++ 4 files changed, 90 insertions(+), 1 deletion(-) create mode 100644 tests/lean/replace1.lean create mode 100644 tests/lean/replace1.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index da67182d9..34814186d 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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 & 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 from; + buffer 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)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 5783e2251..ef5d20c6f 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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 aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/tests/lean/replace1.lean b/tests/lean/replace1.lean new file mode 100644 index 000000000..7629fecd7 --- /dev/null +++ b/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)] diff --git a/tests/lean/replace1.lean.expected.out b/tests/lean/replace1.lean.expected.out new file mode 100644 index 000000000..3b8418855 --- /dev/null +++ b/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₂