feat(frontends/lean): allow expressions to be used to define precedence, closes #335

This commit is contained in:
Leonardo de Moura 2014-11-29 18:29:48 -08:00
parent 2487e3b83d
commit 2c0472252e
11 changed files with 82 additions and 45 deletions

View file

@ -9,7 +9,7 @@ open decidable
structure subtype {A : Type} (P : A → Prop) := structure subtype {A : Type} (P : A → Prop) :=
tag :: (elt_of : A) (has_property : P elt_of) tag :: (elt_of : A) (has_property : P elt_of)
notation `{` binders:55 `|` r:(scoped 1 P, subtype P) `}` := r notation `{` binders:55 `|` r:(scoped:1 P, subtype P) `}` := r
namespace subtype namespace subtype
variables {A : Type} {P : A → Prop} variables {A : Type} {P : A → Prop}

View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: general_notation Module: general_notation
Authors: Leonardo de Moura, Jeremy Avigad Authors: Leonardo de Moura, Jeremy Avigad
-/ -/
import data.num.decl
/- General operations -/ /- General operations -/
@ -22,6 +23,9 @@ notation `take` binders `,` r:(scoped f, f) := r
/- Logical operations and relations -/ /- Logical operations and relations -/
definition std.prec.max : num := 1024 -- reflects max precedence used internally
definition std.prec.arrow : num := 25
reserve prefix `¬`:40 reserve prefix `¬`:40
reserve prefix `~`:40 reserve prefix `~`:40
reserve infixr `∧`:35 reserve infixr `∧`:35

View file

@ -1,6 +1,4 @@
import data.num import data.num.decl
namespace priority definition std.priority.default : num := 1000
definition default : num := 1000 definition std.priority.max : num := 4294967295
definition max : num := 4294967295
end priority

View file

@ -83,7 +83,7 @@ opaque definition revert_lst (ids : expr_list) : tactic := builtin
notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l
infixl `;`:15 := and_then infixl `;`:15 := and_then
notation `[` h:10 `|`:10 r:(foldl 10 `|` (e r, or_else r e) h) `]` := r notation `[` h:10 `|`:10 r:(foldl:10 `|` (e r, or_else r e) h) `]` := r
definition try (t : tactic) : tactic := [t | id] definition try (t : tactic) : tactic := [t | id]
definition repeat1 (t : tactic) : tactic := t ; repeat t definition repeat1 (t : tactic) : tactic := t ; repeat t

View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "library/kernel_serializer.h" #include "library/kernel_serializer.h"
#include "library/reducible.h" #include "library/reducible.h"
#include "library/num.h" #include "library/num.h"
#include "library/aliases.h"
#include "frontends/lean/parser.h" #include "frontends/lean/parser.h"
#include "frontends/lean/util.h" #include "frontends/lean/util.h"
#include "frontends/lean/tokens.h" #include "frontends/lean/tokens.h"
@ -180,10 +181,18 @@ list<name> get_class_instances(environment const & env, name const & c) {
return ptr_to_list(s.m_instances.find(c)); return ptr_to_list(s.m_instances.find(c));
} }
static environment open_priority_namespace(parser & p) {
name prio("std", "priority");
environment env = using_namespace(p.env(), p.ios(), prio);
return overwrite_aliases(env, prio, name());
}
optional<unsigned> parse_instance_priority(parser & p) { optional<unsigned> parse_instance_priority(parser & p) {
if (p.curr_is_token(get_priority_tk())) { if (p.curr_is_token(get_priority_tk())) {
p.next(); p.next();
auto pos = p.pos(); auto pos = p.pos();
environment env = open_priority_namespace(p);
parser::local_scope scope(p, env);
expr val = p.parse_expr(); expr val = p.parse_expr();
val = type_checker(p.env()).whnf(val).first; val = type_checker(p.env()).whnf(val).first;
if (optional<mpz> mpz_val = to_num(val)) { if (optional<mpz> mpz_val = to_num(val)) {

View file

@ -13,6 +13,8 @@ Author: Leonardo de Moura
#include "kernel/replace_fn.h" #include "kernel/replace_fn.h"
#include "library/scoped_ext.h" #include "library/scoped_ext.h"
#include "library/explicit.h" #include "library/explicit.h"
#include "library/num.h"
#include "library/aliases.h"
#include "frontends/lean/parser.h" #include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h" #include "frontends/lean/tokens.h"
@ -30,22 +32,42 @@ static std::string parse_symbol(parser & p, char const * msg) {
return n.to_string(); return n.to_string();
} }
static optional<unsigned> parse_optional_precedence(parser & p) { static environment open_prec_namespace(parser & p) {
name prec("std", "prec");
environment env = using_namespace(p.env(), p.ios(), prec);
return overwrite_aliases(env, prec, name());
}
static unsigned parse_precedence_core(parser & p) {
auto pos = p.pos();
if (p.curr_is_numeral()) { if (p.curr_is_numeral()) {
return optional<unsigned>(p.parse_small_nat()); return p.parse_small_nat();
} else if (p.curr_is_token_or_id(get_max_tk())) { } else {
environment env = open_prec_namespace(p);
parser::local_scope scope(p, env);
expr val = p.parse_expr(get_max_prec());
val = type_checker(p.env()).whnf(val).first;
if (optional<mpz> mpz_val = to_num(val)) {
if (!mpz_val->is_unsigned_int())
throw parser_error("invalid 'precedence', argument does not fit in a machine integer", pos);
return mpz_val->get_unsigned_int();
} else {
throw parser_error("invalid 'precedence', argument does not evaluate to a numeral", pos);
}
}
}
static optional<unsigned> parse_optional_precedence(parser & p) {
if (p.curr_is_token(get_colon_tk())) {
p.next(); p.next();
return optional<unsigned>(get_max_prec()); return some(parse_precedence_core(p));
} else { } else {
return optional<unsigned>(); return optional<unsigned>();
} }
} }
static unsigned parse_precedence(parser & p, char const * msg) { static unsigned parse_precedence(parser & p) {
auto r = parse_optional_precedence(p); return parse_precedence_core(p);
if (!r)
throw parser_error(msg, p.pos());
return *r;
} }
LEAN_THREAD_VALUE(bool, g_allow_local, false); LEAN_THREAD_VALUE(bool, g_allow_local, false);
@ -108,7 +130,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
throw parser_error("invalid notation declaration, invalid ':' occurrence " throw parser_error("invalid notation declaration, invalid ':' occurrence "
"(declaration matches reserved notation)", p.pos()); "(declaration matches reserved notation)", p.pos());
p.next(); p.next();
prec = parse_precedence(p, "invalid notation declaration, numeral or 'max' expected"); prec = parse_precedence(p);
} }
if (prec && k == mixfix_kind::infixr && *prec == 0) if (prec && k == mixfix_kind::infixr && *prec == 0)
@ -224,7 +246,7 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
p.next(); p.next();
if (p.curr_is_token(get_colon_tk())) { if (p.curr_is_token(get_colon_tk())) {
p.next(); p.next();
unsigned prec = parse_precedence(p, "invalid notation declaration, precedence (small numeral) expected"); unsigned prec = parse_precedence(p);
auto old_prec = get_precedence(get_token_table(env), tkcs); auto old_prec = get_precedence(get_token_table(env), tkcs);
if (!old_prec || prec != *old_prec) if (!old_prec || prec != *old_prec)
new_tokens.push_back(token_entry(tkcs, prec)); new_tokens.push_back(token_entry(tkcs, prec));
@ -287,7 +309,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
if (p.curr_is_token(get_colon_tk())) { if (p.curr_is_token(get_colon_tk())) {
p.next(); p.next();
if (p.curr_is_numeral() || p.curr_is_token_or_id(get_max_tk())) { if (p.curr_is_numeral() || p.curr_is_token_or_id(get_max_tk())) {
unsigned prec = parse_precedence(p, "invalid notation declaration, small numeral expected"); unsigned prec = parse_precedence(p);
return mk_expr_action(prec); return mk_expr_action(prec);
} else if (p.curr_is_token_or_id(get_prev_tk())) { } else if (p.curr_is_token_or_id(get_prev_tk())) {
p.next(); p.next();
@ -392,7 +414,7 @@ static optional<pair<action, parse_table>> find_next(optional<parse_table> const
static unsigned parse_binders_rbp(parser & p) { static unsigned parse_binders_rbp(parser & p) {
if (p.curr_is_token(get_colon_tk())) { if (p.curr_is_token(get_colon_tk())) {
p.next(); p.next();
return parse_precedence(p, "invalid binder/binders, precedence expected"); return parse_precedence(p);
} else { } else {
return 0; return 0;
} }
@ -695,7 +717,7 @@ static environment reserve_cmd(parser & p) {
static environment precedence_cmd(parser & p) { static environment precedence_cmd(parser & p) {
std::string tk = parse_symbol(p, "invalid precedence declaration, quoted symbol or identifier expected"); std::string tk = parse_symbol(p, "invalid precedence declaration, quoted symbol or identifier expected");
p.check_token_next(get_colon_tk(), "invalid precedence declaration, ':' expected"); p.check_token_next(get_colon_tk(), "invalid precedence declaration, ':' expected");
unsigned prec = parse_precedence(p, "invalid precedence declaration, numeral or 'max' expected"); unsigned prec = parse_precedence(p);
return add_user_token(p.env(), tk.c_str(), prec); return add_user_token(p.env(), tk.c_str(), prec);
} }

View file

@ -32,9 +32,9 @@ struct aliases_ext : public environment_extension {
name_map<name> m_inv_level_aliases; name_map<name> m_inv_level_aliases;
state():m_in_context(false) {} state():m_in_context(false) {}
void add_expr_alias(name const & a, name const & e) { void add_expr_alias(name const & a, name const & e, bool overwrite) {
auto it = m_aliases.find(a); auto it = m_aliases.find(a);
if (it) if (it && !overwrite)
m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; }))); m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; })));
else else
m_aliases.insert(a, to_list(e)); m_aliases.insert(a, to_list(e));
@ -45,8 +45,8 @@ struct aliases_ext : public environment_extension {
state m_state; state m_state;
list<state> m_scopes; list<state> m_scopes;
void add_expr_alias(name const & a, name const & e) { void add_expr_alias(name const & a, name const & e, bool overwrite) {
m_state.add_expr_alias(a, e); m_state.add_expr_alias(a, e, overwrite);
} }
void add_level_alias(name const & a, name const & l) { void add_level_alias(name const & a, name const & l) {
@ -57,25 +57,25 @@ struct aliases_ext : public environment_extension {
m_state.m_inv_level_aliases.insert(l, a); m_state.m_inv_level_aliases.insert(l, a);
} }
list<state> add_expr_alias_rec_core(list<state> const & scopes, name const & a, name const & e) { list<state> add_expr_alias_rec_core(list<state> const & scopes, name const & a, name const & e, bool overwrite) {
if (empty(scopes)) { if (empty(scopes)) {
return scopes; return scopes;
} else { } else {
state s = head(scopes); state s = head(scopes);
s.add_expr_alias(a, e); s.add_expr_alias(a, e, overwrite);
if (s.m_in_context) { if (s.m_in_context) {
return cons(s, add_expr_alias_rec_core(tail(scopes), a, e)); return cons(s, add_expr_alias_rec_core(tail(scopes), a, e, overwrite));
} else { } else {
return cons(s, tail(scopes)); return cons(s, tail(scopes));
} }
} }
} }
void add_expr_alias_rec(name const & a, name const & e) { void add_expr_alias_rec(name const & a, name const & e, bool overwrite = false) {
if (m_state.m_in_context) { if (m_state.m_in_context) {
m_scopes = add_expr_alias_rec_core(m_scopes, a, e); m_scopes = add_expr_alias_rec_core(m_scopes, a, e, overwrite);
} else { } else {
add_expr_alias(a, e); add_expr_alias(a, e, overwrite);
} }
} }
@ -138,15 +138,15 @@ static environment update(environment const & env, aliases_ext const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<aliases_ext>(ext)); return env.update(g_ext->m_ext_id, std::make_shared<aliases_ext>(ext));
} }
environment add_expr_alias(environment const & env, name const & a, name const & e) { environment add_expr_alias(environment const & env, name const & a, name const & e, bool overwrite) {
aliases_ext ext = get_extension(env); aliases_ext ext = get_extension(env);
ext.add_expr_alias(a, e); ext.add_expr_alias(a, e, overwrite);
return update(env, ext); return update(env, ext);
} }
environment add_expr_alias_rec(environment const & env, name const & a, name const & e) { environment add_expr_alias_rec(environment const & env, name const & a, name const & e, bool overwrite) {
aliases_ext ext = get_extension(env); aliases_ext ext = get_extension(env);
ext.add_expr_alias_rec(a, e); ext.add_expr_alias_rec(a, e, overwrite);
return update(env, ext); return update(env, ext);
} }
@ -187,14 +187,14 @@ bool is_exception(name const & n, name const & prefix, unsigned num_exceptions,
} }
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix, environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
unsigned num_exceptions, name const * exceptions) { unsigned num_exceptions, name const * exceptions, bool overwrite) {
aliases_ext ext = get_extension(env); aliases_ext ext = get_extension(env);
env.for_each_declaration([&](declaration const & d) { env.for_each_declaration([&](declaration const & d) {
if (!is_protected(env, d.get_name()) && if (!is_protected(env, d.get_name()) &&
is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) { is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
name a = d.get_name().replace_prefix(prefix, new_prefix); name a = d.get_name().replace_prefix(prefix, new_prefix);
if (!a.is_anonymous()) if (!a.is_anonymous())
ext.add_expr_alias(a, d.get_name()); ext.add_expr_alias(a, d.get_name(), overwrite);
} }
}); });
env.for_each_universe([&](name const & u) { env.for_each_universe([&](name const & u) {

View file

@ -11,12 +11,12 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
/** \brief Add the alias \c a for \c e. */ /** \brief Add the alias \c a for \c e. */
environment add_expr_alias(environment const & env, name const & a, name const & e); environment add_expr_alias(environment const & env, name const & a, name const & e, bool overwrite = false);
/** /**
\brief Add alias \c a for \c e, and also add it to all parent scopes \brief Add alias \c a for \c e, and also add it to all parent scopes
until in a namespace scope. until in a namespace scope.
*/ */
environment add_expr_alias_rec(environment const & env, name const & a, name const & e); environment add_expr_alias_rec(environment const & env, name const & a, name const & e, bool overwrite = false);
/** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */ /** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */
optional<name> is_expr_aliased(environment const & env, name const & t); optional<name> is_expr_aliased(environment const & env, name const & t);
@ -48,7 +48,10 @@ optional<name> get_level_alias(environment const & env, name const & n);
\remark \c new_prefix may be the anonymous name. \remark \c new_prefix may be the anonymous name.
*/ */
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix, environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
unsigned num_exceptions = 0, name const * exceptions = nullptr); unsigned num_exceptions = 0, name const * exceptions = nullptr, bool overwrite = false);
inline environment overwrite_aliases(environment const & env, name const & prefix, name const & new_prefix) {
return add_aliases(env, prefix, new_prefix, 0, nullptr, true);
}
bool is_exception(name const & n, name const & prefix, unsigned num_exceptions, name const * exceptions); bool is_exception(name const & n, name const & prefix, unsigned num_exceptions, name const * exceptions);

View file

@ -1,5 +1,4 @@
import logic data.prod priority import logic data.prod priority
open priority
set_option pp.notation false set_option pp.notation false
inductive C [class] (A : Type) := inductive C [class] (A : Type) :=

View file

@ -5,6 +5,7 @@ false|Prop
false.rec|Π (C : Type), false → C false.rec|Π (C : Type), false → C
false_elim|false → ?c false_elim|false → ?c
false.rec_on|Π (C : Type), false → C false.rec_on|Π (C : Type), false → C
false.cases_on|Π (C : Type), false → C
false.induction_on|∀ (C : Prop), false → C false.induction_on|∀ (C : Prop), false → C
not_false_trivial|¬ false not_false_trivial|¬ false
true_ne_false|¬ true = false true_ne_false|¬ true = false

View file

@ -2,13 +2,14 @@
-- Released under Apache 2.0 license as described in the file LICENSE. -- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad -- Author: Jeremy Avigad
-- Ported from Coq HoTT -- Ported from Coq HoTT
import general_notation
notation `assume` binders `,` r:(scoped f, f) := r notation `assume` binders `,` r:(scoped f, f) := r
notation `take` binders `,` r:(scoped f, f) := r notation `take` binders `,` r:(scoped f, f) := r
definition id {A : Type} (a : A) := a definition id {A : Type} (a : A) := a
definition compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x) definition compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x)
infixl `∘`:60 := compose infixr ∘ := compose
-- Path -- Path
-- ---- -- ----
@ -17,7 +18,7 @@ set_option unifier.max_steps 100000
inductive path {A : Type} (a : A) : A → Type := inductive path {A : Type} (a : A) : A → Type :=
idpath : path a a idpath : path a a
definition idpath := @path.idpath definition idpath := @path.idpath
infix `≈`:50 := path infix `≈` := path
-- TODO: is this right? -- TODO: is this right?
notation x `≈`:50 y `:>`:0 A:0 := @path A x y notation x `≈`:50 y `:>`:0 A:0 := @path A x y
notation `idp`:max := idpath _ -- TODO: can we / should we use `1`? notation `idp`:max := idpath _ -- TODO: can we / should we use `1`?
@ -32,7 +33,7 @@ path.rec (λu, u) q p
definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x := definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
path.rec (idpath x) p path.rec (idpath x) p
infixl `⬝`:75 := concat infixl `⬝` := concat
postfix `^`:100 := inverse postfix `^`:100 := inverse
-- In Coq, these are not needed, because concat and inv are kept transparent -- In Coq, these are not needed, because concat and inv are kept transparent
@ -201,7 +202,7 @@ definition ap01 := ap
definition pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type := definition pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type :=
Πx : A, f x ≈ g x Πx : A, f x ≈ g x
infix ``:50 := pointwise_paths infix `` := pointwise_paths
definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f g := definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f g :=
λx, path.rec_on H idp λx, path.rec_on H idp