michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/util): remove hack that overrides priority namespace

Browse source 
closes #789
This commit is contained in:
Leonardo de Moura 2015-08-11 18:01:40 -07:00
parent 0b8f57841a
commit 66a59d5b51
5 changed files with 18 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/frontends/lean/util.cpp
View file

@ -429,14 +429,6 @@ environment open_prec_aliases(environment const & env) {
return overwrite_aliases(env, prec, name()); return overwrite_aliases(env, prec, name());
} }
name get_priority_namespace() {
return name("std", "priority");
}
environment open_priority_aliases(environment const & env) {
return overwrite_aliases(env, get_priority_namespace(), name());
}
char const * open_binder_string(binder_info const & bi, bool unicode) { char const * open_binder_string(binder_info const & bi, bool unicode) {
if (bi.is_implicit()) return "{"; if (bi.is_implicit()) return "{";
else if (bi.is_inst_implicit()) return "["; else if (bi.is_inst_implicit()) return "[";
@ -457,33 +449,18 @@ expr postprocess(environment const & env, expr const & e) {
return eta_reduce(expand_abbreviations(env, unfold_untrusted_macros(env, e))); return eta_reduce(expand_abbreviations(env, unfold_untrusted_macros(env, e)));
} }
struct elim_choice_fn : public replace_visitor {
name m_prio_ns;
elim_choice_fn():m_prio_ns(get_priority_namespace()) {}
virtual expr visit_macro(expr const & e) {
if (is_choice(e)) {
for (unsigned i = 0; i < get_num_choices(e); i++) {
expr const & c = get_choice(e, i);
if (is_constant(c) && const_name(c).get_prefix() == m_prio_ns)
return c;
}
throw exception("invalid priority expression, it contains overloaded symbols");
} else {
return replace_visitor::visit_macro(e);
}
}
};
optional<unsigned> parse_priority(parser & p) { optional<unsigned> parse_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_aliases(open_num_notation(p.env())); environment env = open_num_notation(p.env());
parser::local_scope scope(p, env); parser::local_scope scope(p, env);
expr val = p.parse_expr(); expr val = p.parse_expr();
val = elim_choice_fn()(val); for_each(val, [](expr const & e, unsigned) {
if (is_choice(e))
throw exception("invalid priority expression, it contains overloaded symbols");
return true;
});
val = normalize(p.env(), val); val = normalize(p.env(), val);
if (optional<mpz> mpz_val = to_num(val)) { if (optional<mpz> mpz_val = to_num(val)) {
if (!mpz_val->is_unsigned_int()) if (!mpz_val->is_unsigned_int())

2
tests/lean/inst.lean
View file

@ -8,7 +8,7 @@ definition val {A : Type} (c : C A) : A :=
C.rec (λa, a) c C.rec (λa, a) c
constant magic (A : Type) : A constant magic (A : Type) : A
definition C_magic [instance] [priority max] (A : Type) : C A := definition C_magic [instance] [priority std.priority.max] (A : Type) : C A :=
C.mk (magic A) C.mk (magic A)
definition C_prop [instance] : C Prop := definition C_prop [instance] : C Prop :=

6
tests/lean/run/notation_priority.lean
View file

@ -13,15 +13,15 @@ example : a + b = f a b := rfl
infix [priority 15] + := g infix [priority 15] + := g
example : a + b = g a b := rfl example : a + b = g a b := rfl
infix [priority default+1] + := f infix [priority std.priority.default+1] + := f
infix + := g infix + := g
example : a + b = f a b := rfl example : a + b = f a b := rfl
infix [priority default+2] + := g infix [priority std.priority.default+2] + := g
example : a + b = g a b := rfl example : a + b = g a b := rfl
infix + := f infix + := f
infix + := g infix + := g
example : a + b = f a b := rfl example : a + b = f a b := rfl
infix [priority default+1] + := g infix [priority std.priority.default+1] + := g
example : a + b = g a b := rfl example : a + b = g a b := rfl

4
tests/lean/run/priority_test.lean
View file

@ -3,7 +3,7 @@ open nat
structure foo [class] := structure foo [class] :=
(a : nat) (b : nat) (a : nat) (b : nat)
definition i1 [instance] [priority default+1] : foo := definition i1 [instance] [priority std.priority.default+1] : foo :=
foo.mk 1 1 foo.mk 1 1
definition i2 [instance] : foo := definition i2 [instance] : foo :=
@ -12,7 +12,7 @@ foo.mk 2 2
example : foo.a = 1 := example : foo.a = 1 :=
rfl rfl
definition i3 [instance] [priority default+2] : foo := definition i3 [instance] [priority std.priority.default+2] : foo :=
foo.mk 3 3 foo.mk 3 3
example : foo.a = 3 := example : foo.a = 3 :=

12
tests/lean/run/priority_test2.lean
View file

@ -3,13 +3,13 @@ open nat
structure foo [class] := structure foo [class] :=
(a : nat) (b : nat) (a : nat) (b : nat)
definition i1 [instance] [priority default-2] : foo := definition i1 [instance] [priority std.priority.default-2] : foo :=
foo.mk 1 1 foo.mk 1 1
example : foo.a = 1 := example : foo.a = 1 :=
rfl rfl
definition i2 [instance] [priority default-1] : foo := definition i2 [instance] [priority std.priority.default-1] : foo :=
foo.mk 2 2 foo.mk 2 2
example : foo.a = 2 := example : foo.a = 2 :=
@ -21,23 +21,23 @@ foo.mk 3 3
example : foo.a = 3 := example : foo.a = 3 :=
rfl rfl
definition i4 [instance] [priority default-1] : foo := definition i4 [instance] [priority std.priority.default-1] : foo :=
foo.mk 4 4 foo.mk 4 4
example : foo.a = 3 := example : foo.a = 3 :=
rfl rfl
attribute i4 [priority default+2] attribute i4 [priority std.priority.default+2]
example : foo.a = 4 := example : foo.a = 4 :=
rfl rfl
attribute i1 [priority default+3] attribute i1 [priority std.priority.default+3]
example : foo.a = 1 := example : foo.a = 1 :=
rfl rfl
attribute i2 [instance] [priority default+4] attribute i2 [instance] [priority std.priority.default+4]
example : foo.a = 2 := example : foo.a = 2 :=
rfl rfl