From 40fb66bf077c199fab9104b55c9a953264ca3990 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Oct 2014 18:40:55 -0700 Subject: [PATCH] feat(frontends/lean): change default precedence to 1 --- library/algebra/function.lean | 3 --- library/logic/if.lean | 2 +- src/frontends/lean/notation_cmd.cpp | 6 +++--- src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/token_table.h | 12 ++++++++---- tests/lean/t10.lean | 2 +- 6 files changed, 14 insertions(+), 13 deletions(-) diff --git a/library/algebra/function.lean b/library/algebra/function.lean index d6f6cf11e..733df0cf5 100644 --- a/library/algebra/function.lean +++ b/library/algebra/function.lean @@ -37,9 +37,6 @@ precedence `∘`:60 precedence `∘'`:60 precedence `on`:1 precedence `$`:1 -precedence `-[`:1 -precedence `]-`:1 -precedence `⟨`:1 infixr ∘ := compose infixr ∘' := dcompose diff --git a/library/logic/if.lean b/library/logic/if.lean index b271ebc8d..175025151 100644 --- a/library/logic/if.lean +++ b/library/logic/if.lean @@ -10,7 +10,7 @@ open decidable tactic eq.ops definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A := decidable.rec_on H (assume Hc, t) (assume Hnc, e) -notation `if` c `then` t `else` e:45 := ite c t e +notation `if` c `then` t:45 `else` e:45 := ite c t e theorem if_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t := decidable.rec diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index d4c19699e..ad5c30bc3 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -130,7 +130,7 @@ static name parse_quoted_symbol_or_token(parser & p, buffer & new_t if (!old_prec || prec != *old_prec) new_tokens.push_back(token_entry(tkcs, prec)); } else if (!get_precedence(get_token_table(env), tkcs)) { - new_tokens.push_back(token_entry(tkcs, 0)); + new_tokens.push_back(token_entry(tkcs, LEAN_DEFAULT_PRECEDENCE)); } return tk; } else if (p.curr_is_keyword()) { @@ -253,12 +253,12 @@ static action parse_action(parser & p, name const & prev_token, unsigned default */ static unsigned get_default_prec(optional const & pt, name const & tk) { if (!pt) - return 0; + return LEAN_DEFAULT_PRECEDENCE; if (auto at = pt->find(tk)) { if (at->first.kind() == notation::action_kind::Expr) return at->first.rbp(); } - return 0; + return LEAN_DEFAULT_PRECEDENCE; } static notation_entry parse_notation_core(parser & p, bool overload, buffer & new_tokens) { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 7b1e278e5..f18e4d188 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -111,7 +111,7 @@ void init_token_table(token_table & t) { auto it3 = aliases; while (it3->first) { - t = add_token(t, it3->first, it3->second); + t = add_token(t, it3->first, it3->second, 0); it3++; } t = add_token(t, g_arrow_unicode, "->", get_arrow_prec()); diff --git a/src/frontends/lean/token_table.h b/src/frontends/lean/token_table.h index 675549403..2fef36766 100644 --- a/src/frontends/lean/token_table.h +++ b/src/frontends/lean/token_table.h @@ -11,6 +11,10 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/lua.h" +#ifndef LEAN_DEFAULT_PRECEDENCE +#define LEAN_DEFAULT_PRECEDENCE 1 +#endif + namespace lean { unsigned get_max_prec(); unsigned get_arrow_prec(); @@ -22,9 +26,9 @@ class token_info { public: token_info():m_command(true) {} token_info(char const * val): - m_command(true), m_token(val), m_value(val), m_precedence(0) {} + m_command(true), m_token(val), m_value(val), m_precedence(LEAN_DEFAULT_PRECEDENCE) {} token_info(char const * token, char const * val): - m_command(true), m_token(token), m_value(val), m_precedence(0) {} + m_command(true), m_token(token), m_value(val), m_precedence(LEAN_DEFAULT_PRECEDENCE) {} token_info(char const * val, unsigned prec): m_command(false), m_token(val), m_value(val), m_precedence(prec) {} token_info(char const * token, char const * val, unsigned prec): @@ -40,8 +44,8 @@ token_table mk_token_table(); token_table mk_default_token_table(); token_table add_command_token(token_table const & s, char const * token); token_table add_command_token(token_table const & s, char const * token, char const * val); -token_table add_token(token_table const & s, char const * token, unsigned prec = 0); -token_table add_token(token_table const & s, char const * token, char const * val, unsigned prec = 0); +token_table add_token(token_table const & s, char const * token, unsigned prec = LEAN_DEFAULT_PRECEDENCE); +token_table add_token(token_table const & s, char const * token, char const * val, unsigned prec = LEAN_DEFAULT_PRECEDENCE); void for_each(token_table const & s, std::function const & fn); void display(std::ostream & out, token_table const & s); token_table const * find(token_table const & s, char c); diff --git a/tests/lean/t10.lean b/tests/lean/t10.lean index b19cc36bf..8943c5260 100644 --- a/tests/lean/t10.lean +++ b/tests/lean/t10.lean @@ -9,7 +9,7 @@ constant x : N constant y : N constant z : N infixr `∧`:25 := and -notation `if` c `then` t `else` e := ite c t e +notation `if` c `then` t:45 `else` e:45 := ite c t e check if p ∧ q then f x else y check if p ∧ q then q else y constant list : Type.{1}