From e178979061541cb583f90134f3e7a1a1a57baca3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Jun 2014 13:35:31 -0700 Subject: [PATCH] feat(frontends/lean): add calc_subst, calc_refl, calc_trans commands for configuring calc-expressions Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 2 ++ src/frontends/lean/calc.cpp | 22 ++++++++++++++++++++++ src/frontends/lean/calc.h | 7 ++----- src/frontends/lean/parser.h | 2 +- src/frontends/lean/token_table.cpp | 2 +- tests/lean/calc1.lean | 18 ++++++++++++++++++ tests/lean/calc1.lean.expected.out | 0 7 files changed, 46 insertions(+), 7 deletions(-) create mode 100644 tests/lean/calc1.lean create mode 100644 tests/lean/calc1.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 326520afd..39343ca86 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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; } diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp index 3ccc11b43..851f6bb9d 100644 --- a/src/frontends/lean/calc.cpp +++ b/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)); +} } diff --git a/src/frontends/lean/calc.h b/src/frontends/lean/calc.h index bfb36f3d2..cfed35885 100644 --- a/src/frontends/lean/calc.h +++ b/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); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 73e39d0c1..c8691b3fc 100644 --- a/src/frontends/lean/parser.h +++ b/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 & 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 & ps, local_environment const & lenv, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), lenv, rbp); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 8eca01816..7b58188ba 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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 aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/tests/lean/calc1.lean b/tests/lean/calc1.lean new file mode 100644 index 000000000..b013ff647 --- /dev/null +++ b/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 diff --git a/tests/lean/calc1.lean.expected.out b/tests/lean/calc1.lean.expected.out new file mode 100644 index 000000000..e69de29bb