From b9451549d10dc7ffe289a7f4e393cc1d789b3b4c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Jul 2015 21:43:47 -0700 Subject: [PATCH] feat(frontends/lean): add `type` notation for referencing hypotheses --- library/theories/number_theory/primes.lean | 50 +++++++++++----------- src/frontends/lean/notation_cmd.cpp | 10 +++++ src/frontends/lean/notation_cmd.h | 2 + src/frontends/lean/parser.cpp | 34 +++++++++++++-- src/frontends/lean/parser.h | 9 ++++ src/frontends/lean/scanner.cpp | 8 +++- src/frontends/lean/scanner.h | 12 +++++- src/frontends/lean/tokens.cpp | 28 ++++++++++++ src/frontends/lean/tokens.h | 7 +++ src/frontends/lean/tokens.txt | 7 +++ 10 files changed, 136 insertions(+), 31 deletions(-) diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index 47728c03f..77bdc10af 100644 --- a/library/theories/number_theory/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -65,10 +65,10 @@ assume h d, obtain h₁ h₂, from h, h₂ m d lemma gt_one_of_pos_of_prime_dvd {i p : nat} : prime p → 0 < i → i mod p = 0 → 1 < i := assume ipp pos h, -have h₁ : p ≥ 2, from ge_two_of_prime ipp, -have p ∣ i, from dvd_of_mod_eq_zero h, -have p ≤ i, from le_of_dvd pos this, -lt_of_succ_le (le.trans h₁ this) +have p ≥ 2, from ge_two_of_prime ipp, +have p ∣ i, from dvd_of_mod_eq_zero h, +have p ≤ i, from le_of_dvd pos this, +lt_of_succ_le (le.trans `2 ≤ p` this) definition sub_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≠ 1 ∧ m ≠ n} := assume h₁ h₂, @@ -124,30 +124,30 @@ definition infinite_primes (n : nat) : {p | p ≥ n ∧ prime p} := let m := fact (n + 1) in have m ≥ 1, from le_of_lt_succ (succ_lt_succ (fact_pos _)), have m + 1 ≥ 2, from succ_le_succ this, -obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd this, -have p_ge_2 : p ≥ 2, from ge_two_of_prime prime_p, -have p_gt_0 : p > 0, from lt_of_succ_lt (lt_of_succ_le p_ge_2), +obtain p (pp : prime p) (pd : p ∣ m + 1), from sub_prime_and_dvd this, +have p ≥ 2, from ge_two_of_prime `prime p`, +have p > 0, from lt_of_succ_lt (lt_of_succ_le `p ≥ 2`), have p ≥ n, from by_contradiction (suppose ¬ p ≥ n, have p < n, from lt_of_not_ge this, have p ≤ n + 1, from le_of_lt (lt.step this), - have p ∣ m, from dvd_fact p_gt_0 this, - have p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ p_dvd_m1) this, + have p ∣ m, from dvd_fact `p > 0` this, + have p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ `p ∣ m + 1`) this, have p ≤ 1, from le_of_dvd zero_lt_one this, - absurd (le.trans p_ge_2 this) dec_trivial), -subtype.tag p (and.intro this prime_p) + absurd (le.trans `2 ≤ p` `p ≤ 1`) dec_trivial), +subtype.tag p (and.intro this `prime p`) lemma ex_infinite_primes (n : nat) : ∃ p, p ≥ n ∧ prime p := ex_of_sub (infinite_primes n) lemma odd_of_prime {p : nat} : prime p → p > 2 → odd p := λ pp p_gt_2, by_contradiction (λ hn, - have even_p : even p, from even_of_not_odd hn, - obtain k (hk : p = 2*k), from exists_of_even even_p, - assert two_div_p : 2 ∣ p, by rewrite [hk]; apply dvd_mul_right, - or.elim (eq_one_or_eq_self_of_prime_of_dvd pp two_div_p) - (λ h : 2 = 1, absurd h dec_trivial) - (λ h : 2 = p, by subst h; exact absurd p_gt_2 !lt.irrefl)) + have even p, from even_of_not_odd hn, + obtain k (hk : p = 2*k), from exists_of_even this, + assert 2 ∣ p, by rewrite [hk]; apply dvd_mul_right, + or.elim (eq_one_or_eq_self_of_prime_of_dvd pp this) + (suppose 2 = 1, absurd this dec_trivial) + (suppose 2 = p, by subst this; exact absurd p_gt_2 !lt.irrefl)) theorem dvd_of_prime_of_not_coprime {p n : ℕ} (primep : prime p) (nc : ¬ coprime p n) : p ∣ n := have H : gcd p n = 1 ∨ gcd p n = p, from eq_one_or_eq_self_of_prime_of_dvd primep !gcd_dvd_left, @@ -195,8 +195,8 @@ lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p | (succ n) hp hd := have p ∣ (m^n)*m, by rewrite [pow_succ at hd]; exact hd, or.elim (dvd_or_dvd_of_prime_of_dvd_mul hp this) - (λ h : p ∣ m^n, dvd_of_prime_of_dvd_pow hp h) - (λ h : p ∣ m, h) + (suppose p ∣ m^n, dvd_of_prime_of_dvd_pow hp this) + (suppose p ∣ m, this) lemma coprime_pow_of_prime_of_not_dvd {p m a : nat} : prime p → ¬ p ∣ a → coprime a (p^m) := λ h₁ h₂, coprime_pow_right m (coprime_swap (coprime_of_prime_of_not_dvd h₁ h₂)) @@ -205,21 +205,21 @@ lemma coprime_primes {p q : nat} : prime p → prime q → p ≠ q → coprime p λ hp hq hn, assert gcd p q ∣ p, from !gcd_dvd_left, or.elim (eq_one_or_eq_self_of_prime_of_dvd hp this) - (λ h : gcd p q = 1, h) - (λ h : gcd p q = p, + (suppose gcd p q = 1, this) + (assume h : gcd p q = p, assert gcd p q ∣ q, from !gcd_dvd_right, have p ∣ q, by rewrite -h; exact this, or.elim (eq_one_or_eq_self_of_prime_of_dvd hq this) - (λ h₁ : p = 1, by subst p; exact absurd hp not_prime_one) - (λ he : p = q, by contradiction)) + (suppose p = 1, by subst p; exact absurd hp not_prime_one) + (suppose p = q, by contradiction)) lemma coprime_pow_primes {p q : nat} (n m : nat) : prime p → prime q → p ≠ q → coprime (p^n) (q^m) := λ hp hq hn, coprime_pow_right m (coprime_pow_left n (coprime_primes hp hq hn)) lemma coprime_or_dvd_of_prime {p} (Pp : prime p) (i : nat) : coprime p i ∨ p ∣ i := by_cases - (λ h : p ∣ i, or.inr h) - (λ h : ¬ p ∣ i, or.inl (coprime_of_prime_of_not_dvd Pp h)) + (suppose p ∣ i, or.inr this) + (suppose ¬ p ∣ i, or.inl (coprime_of_prime_of_not_dvd Pp this)) lemma eq_one_or_dvd_of_dvd_prime_pow {p : nat} : ∀ {m i : nat}, prime p → i ∣ (p^m) → i = 1 ∨ p ∣ i | 0 := take i, assume Pp, begin rewrite [pow_zero], intro Pdvd, apply or.inl (eq_one_of_dvd_one Pdvd) end diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index de020c9fb..a126575e1 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -813,6 +813,7 @@ static environment dispatch_notation_cmd(parser & p, bool overload, notation_ent } environment local_notation_cmd(parser & p) { + parser::in_notation_ctx ctx(p); bool overload = false; // REMARK: local notation override global one notation_entry_group grp = notation_entry_group::Main; bool persistent = false; @@ -820,6 +821,7 @@ environment local_notation_cmd(parser & p) { } static environment reserve_cmd(parser & p) { + parser::in_notation_ctx ctx(p); bool overload = false; notation_entry_group grp = notation_entry_group::Reserve; bool persistent = true; @@ -849,4 +851,12 @@ void register_notation_cmds(cmd_table & r) { add_cmd(r, cmd_info("tactic_notation", "declare a new tacitc notation", tactic_notation_cmd)); add_cmd(r, cmd_info("reserve", "reserve notation", reserve_cmd)); } + +bool is_notation_cmd(name const & n) { + return + n == get_infix_tk() || n == get_infixl_tk() || n == get_infixr_tk() || n == get_postfix_tk() || + n == get_prefix_tk() || n == get_notation_tk() || n == get_precedence_tk() || + n == get_tactic_infix_tk() || n == get_tactic_infixl_tk() || n == get_tactic_infixr_tk() || n == get_tactic_postfix_tk() || + n == get_tactic_prefix_tk() || n == get_tactic_notation_tk(); +} } diff --git a/src/frontends/lean/notation_cmd.h b/src/frontends/lean/notation_cmd.h index 7e5d28228..98ffc15bb 100644 --- a/src/frontends/lean/notation_cmd.h +++ b/src/frontends/lean/notation_cmd.h @@ -21,4 +21,6 @@ notation_entry parse_notation(parser & p, bool overload, buffer & n environment local_notation_cmd(parser & p); void register_notation_cmds(cmd_table & r); + +bool is_notation_cmd(name const & cmd_name); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 4d9c40a97..c044be322 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -31,6 +31,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/scoped_ext.h" #include "library/explicit.h" +#include "library/typed_expr.h" #include "library/let.h" #include "library/num.h" #include "library/string.h" @@ -111,7 +112,8 @@ parser::parser(environment const & env, io_state const & ios, m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0), m_snapshot_vector(sv), m_info_manager(im), m_cache(nullptr), m_index(nullptr) { m_local_decls_size_at_beg_cmd = 0; - m_profile = ios.get_options().get_bool("profile", false); + m_in_backtick = false; + m_profile = ios.get_options().get_bool("profile", false); if (num_threads > 1 && m_profile) throw exception("option --profile cannot be used when theorems are compiled in parallel"); m_has_params = false; @@ -961,6 +963,7 @@ local_environment parser::parse_binders(buffer & r, buffer bool parser::parse_local_notation_decl(buffer * nentries) { if (curr_is_notation_decl(*this)) { + parser::in_notation_ctx ctx(*this); buffer new_tokens; bool overload = false; bool allow_local = true; @@ -1327,6 +1330,19 @@ expr parser::parse_string_expr() { return from_string(v); } +expr parser::parse_backtick_expr() { + auto p = pos(); + next(); + flet set(m_in_backtick, true); + expr type = parse_expr(); + if (curr() != scanner::token_kind::Backtick) { + throw parser_error("invalid expression, '`' expected", pos()); + } + next(); + expr assump = mk_by_plus(save_pos(mk_constant(get_tactic_assumption_name()), p), p); + return save_pos(mk_typed_expr(type, assump), p); +} + expr parser::parse_nud() { switch (curr()) { case scanner::token_kind::Keyword: return parse_nud_notation(); @@ -1334,6 +1350,7 @@ expr parser::parse_nud() { case scanner::token_kind::Numeral: return parse_numeral_expr(); case scanner::token_kind::Decimal: return parse_decimal_expr(); case scanner::token_kind::String: return parse_string_expr(); + case scanner::token_kind::Backtick: return parse_backtick_expr(); default: throw parser_error("invalid expression, unexpected token", pos()); } } @@ -1355,6 +1372,8 @@ unsigned parser::curr_lbp_core(bool as_tactic) const { case scanner::token_kind::CommandKeyword: case scanner::token_kind::Eof: case scanner::token_kind::ScriptBlock: case scanner::token_kind::QuotedSymbol: return 0; + case scanner::token_kind::Backtick: + return m_in_backtick ? 0 : get_max_prec(); case scanner::token_kind::Identifier: case scanner::token_kind::Numeral: case scanner::token_kind::Decimal: case scanner::token_kind::String: return get_max_prec(); @@ -1636,9 +1655,16 @@ void parser::parse_command() { name const & cmd_name = get_token_info().value(); m_cmd_token = get_token_info().token(); if (auto it = cmds().find(cmd_name)) { - next(); - m_local_decls_size_at_beg_cmd = m_local_decls.size(); - m_env = it->get_fn()(*this); + if (is_notation_cmd(cmd_name)) { + in_notation_ctx ctx(*this); + next(); + m_local_decls_size_at_beg_cmd = m_local_decls.size(); + m_env = it->get_fn()(*this); + } else { + next(); + m_local_decls_size_at_beg_cmd = m_local_decls.size(); + m_env = it->get_fn()(*this); + } } else { auto p = pos(); next(); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 1231655e5..6d80488b8 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -233,6 +233,9 @@ class parser { elaborator_context mk_elaborator_context(environment const & env, pos_info_provider const & pp); elaborator_context mk_elaborator_context(environment const & env, local_level_decls const & lls, pos_info_provider const & pp); + bool m_in_backtick; // true if parser `expr` notation + expr parse_backtick_expr(); + optional is_tactic_command(name & id); expr parse_tactic_option_num(); expr parse_tactic_led(expr left); @@ -511,6 +514,12 @@ public: /** parse all commands in the input stream */ bool operator()() { return parse_commands(); } + + class in_notation_ctx { + scanner::in_notation_ctx m_ctx; + public: + in_notation_ctx(parser & p):m_ctx(p.m_scanner) {} + }; }; bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 8bb5bba08..f6d6f78fe 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -437,7 +437,12 @@ auto scanner::scan(environment const & env) -> token_kind { case '\"': return read_string(); case '`': - return read_quoted_symbol(); + if (m_in_notation) { + return read_quoted_symbol(); + } else { + next(); + return token_kind::Backtick; + } case -1: return token_kind::Eof; default: @@ -471,6 +476,7 @@ scanner::scanner(std::istream & strm, char const * strm_name, unsigned line): m_line = line; m_spos = 0; m_upos = 0; + m_in_notation = false; if (std::getline(m_stream, m_curr_line)) { m_last_line = false; m_curr_line.push_back('\n'); diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index f1659b321..641a4e281 100644 --- a/src/frontends/lean/scanner.h +++ b/src/frontends/lean/scanner.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/name.h" +#include "util/flet.h" #include "util/numerics/mpq.h" #include "kernel/environment.h" #include "frontends/lean/token_table.h" @@ -22,7 +23,7 @@ namespace lean { */ class scanner { public: - enum class token_kind {Keyword, CommandKeyword, ScriptBlock, Identifier, Numeral, Decimal, String, QuotedSymbol, Eof}; + enum class token_kind {Keyword, CommandKeyword, ScriptBlock, Identifier, Numeral, Decimal, String, QuotedSymbol, Backtick, Eof}; protected: token_table const * m_tokens; std::istream & m_stream; @@ -45,6 +46,9 @@ protected: std::string m_buffer; std::string m_aux_buffer; + bool m_in_notation; + + [[ noreturn ]] void throw_exception(char const * msg); void next(); char curr() const { return m_curr; } @@ -80,6 +84,12 @@ public: token_info const & get_token_info() const { return m_token_info; } std::string const & get_stream_name() const { return m_stream_name; } + + class in_notation_ctx { + flet m_in_notation; + public: + in_notation_ctx(scanner & s):m_in_notation(s.m_in_notation, true) {} + }; }; std::ostream & operator<<(std::ostream & out, scanner::token_kind k); void initialize_scanner(); diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 808145c17..44c84e80b 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -126,12 +126,19 @@ static name const * g_foldr_tk = nullptr; static name const * g_foldl_tk = nullptr; static name const * g_binder_tk = nullptr; static name const * g_binders_tk = nullptr; +static name const * g_precedence_tk = nullptr; static name const * g_infix_tk = nullptr; static name const * g_infixl_tk = nullptr; static name const * g_infixr_tk = nullptr; static name const * g_postfix_tk = nullptr; static name const * g_prefix_tk = nullptr; static name const * g_notation_tk = nullptr; +static name const * g_tactic_infix_tk = nullptr; +static name const * g_tactic_infixl_tk = nullptr; +static name const * g_tactic_infixr_tk = nullptr; +static name const * g_tactic_postfix_tk = nullptr; +static name const * g_tactic_prefix_tk = nullptr; +static name const * g_tactic_notation_tk = nullptr; static name const * g_call_tk = nullptr; static name const * g_calc_tk = nullptr; static name const * g_obtain_tk = nullptr; @@ -266,12 +273,19 @@ void initialize_tokens() { g_foldl_tk = new name{"foldl"}; g_binder_tk = new name{"binder"}; g_binders_tk = new name{"binders"}; + g_precedence_tk = new name{"precedence"}; g_infix_tk = new name{"infix"}; g_infixl_tk = new name{"infixl"}; g_infixr_tk = new name{"infixr"}; g_postfix_tk = new name{"postfix"}; g_prefix_tk = new name{"prefix"}; g_notation_tk = new name{"notation"}; + g_tactic_infix_tk = new name{"tactic_infix"}; + g_tactic_infixl_tk = new name{"tactic_infixl"}; + g_tactic_infixr_tk = new name{"tactic_infixr"}; + g_tactic_postfix_tk = new name{"tactic_postfix"}; + g_tactic_prefix_tk = new name{"tactic_prefix"}; + g_tactic_notation_tk = new name{"tactic_notation"}; g_call_tk = new name{"call"}; g_calc_tk = new name{"calc"}; g_obtain_tk = new name{"obtain"}; @@ -407,12 +421,19 @@ void finalize_tokens() { delete g_foldl_tk; delete g_binder_tk; delete g_binders_tk; + delete g_precedence_tk; delete g_infix_tk; delete g_infixl_tk; delete g_infixr_tk; delete g_postfix_tk; delete g_prefix_tk; delete g_notation_tk; + delete g_tactic_infix_tk; + delete g_tactic_infixl_tk; + delete g_tactic_infixr_tk; + delete g_tactic_postfix_tk; + delete g_tactic_prefix_tk; + delete g_tactic_notation_tk; delete g_call_tk; delete g_calc_tk; delete g_obtain_tk; @@ -547,12 +568,19 @@ name const & get_foldr_tk() { return *g_foldr_tk; } name const & get_foldl_tk() { return *g_foldl_tk; } name const & get_binder_tk() { return *g_binder_tk; } name const & get_binders_tk() { return *g_binders_tk; } +name const & get_precedence_tk() { return *g_precedence_tk; } name const & get_infix_tk() { return *g_infix_tk; } name const & get_infixl_tk() { return *g_infixl_tk; } name const & get_infixr_tk() { return *g_infixr_tk; } name const & get_postfix_tk() { return *g_postfix_tk; } name const & get_prefix_tk() { return *g_prefix_tk; } name const & get_notation_tk() { return *g_notation_tk; } +name const & get_tactic_infix_tk() { return *g_tactic_infix_tk; } +name const & get_tactic_infixl_tk() { return *g_tactic_infixl_tk; } +name const & get_tactic_infixr_tk() { return *g_tactic_infixr_tk; } +name const & get_tactic_postfix_tk() { return *g_tactic_postfix_tk; } +name const & get_tactic_prefix_tk() { return *g_tactic_prefix_tk; } +name const & get_tactic_notation_tk() { return *g_tactic_notation_tk; } name const & get_call_tk() { return *g_call_tk; } name const & get_calc_tk() { return *g_calc_tk; } name const & get_obtain_tk() { return *g_obtain_tk; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 621dc6daa..d765a1248 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -128,12 +128,19 @@ name const & get_foldr_tk(); name const & get_foldl_tk(); name const & get_binder_tk(); name const & get_binders_tk(); +name const & get_precedence_tk(); name const & get_infix_tk(); name const & get_infixl_tk(); name const & get_infixr_tk(); name const & get_postfix_tk(); name const & get_prefix_tk(); name const & get_notation_tk(); +name const & get_tactic_infix_tk(); +name const & get_tactic_infixl_tk(); +name const & get_tactic_infixr_tk(); +name const & get_tactic_postfix_tk(); +name const & get_tactic_prefix_tk(); +name const & get_tactic_notation_tk(); name const & get_call_tk(); name const & get_calc_tk(); name const & get_obtain_tk(); diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt index a00f8abc4..708fb11fc 100644 --- a/src/frontends/lean/tokens.txt +++ b/src/frontends/lean/tokens.txt @@ -121,12 +121,19 @@ foldr foldr foldl foldl binder binder binders binders +precedence precedence infix infix infixl infixl infixr infixr postfix postfix prefix prefix notation notation +tactic_infix tactic_infix +tactic_infixl tactic_infixl +tactic_infixr tactic_infixr +tactic_postfix tactic_postfix +tactic_prefix tactic_prefix +tactic_notation tactic_notation call call calc calc obtain obtain