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

feat(frontends/lean): add '[local]' notation, closes #322

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-16 20:51:42 -08:00
parent b7725c2949
commit 28c63e685b
13 changed files with 102 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/emacs/lean-syntax.el
View file

@ -116,7 +116,7 @@
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; modifiers
(,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
"\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[whnf\]" "\[decls\]" "\[strict\]"))
"\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[whnf\]" "\[decls\]" "\[strict\]" "\[local\]"))
. 'font-lock-doc-face)
(,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
;; tactics

99
src/frontends/lean/notation_cmd.cpp
View file

@ -78,20 +78,8 @@ void check_not_forbidden(char const * tk) {
}
}
struct notation_modifiers {
bool m_parse_only;
notation_modifiers():m_parse_only(false) {}
void parse(parser & p) {
if (p.curr_is_token(get_parsing_only_tk())) {
p.next();
m_parse_only = true;
}
}
};
static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve) -> pair<notation_entry, optional<token_entry>> {
notation_modifiers mod;
mod.parse(p);
static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve, bool parse_only)
-> pair<notation_entry, optional<token_entry>> {
std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
char const * tks = tk.c_str();
check_not_forbidden(tks);
@ -180,16 +168,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
switch (k) {
case mixfix_kind::infixl:
return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
dummy, overload, reserve, mod.m_parse_only), new_token);
dummy, overload, reserve, parse_only), new_token);
case mixfix_kind::infixr:
return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
dummy, overload, reserve, mod.m_parse_only), new_token);
dummy, overload, reserve, parse_only), new_token);
case mixfix_kind::postfix:
return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
dummy, overload, reserve, mod.m_parse_only), new_token);
dummy, overload, reserve, parse_only), new_token);
case mixfix_kind::prefix:
return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
dummy, overload, reserve, mod.m_parse_only), new_token);
dummy, overload, reserve, parse_only), new_token);
}
} else {
p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected");
@ -201,25 +189,25 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
#if defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
mk_app(f, Var(1), Var(0)), overload, reserve, mod.m_parse_only), new_token);
mk_app(f, Var(1), Var(0)), overload, reserve, parse_only), new_token);
#endif
case mixfix_kind::infixr:
return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
mk_app(f, Var(1), Var(0)), overload, reserve, mod.m_parse_only), new_token);
mk_app(f, Var(1), Var(0)), overload, reserve, parse_only), new_token);
case mixfix_kind::postfix:
return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
mk_app(f, Var(0)), overload, reserve, mod.m_parse_only), new_token);
mk_app(f, Var(0)), overload, reserve, parse_only), new_token);
case mixfix_kind::prefix:
return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
mk_app(f, Var(0)), overload, reserve, mod.m_parse_only), new_token);
mk_app(f, Var(0)), overload, reserve, parse_only), new_token);
}
}
lean_unreachable(); // LCOV_EXCL_LINE
}
static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve,
buffer<token_entry> & new_tokens) {
auto nt = parse_mixfix_notation(p, k, overload, reserve);
buffer<token_entry> & new_tokens, bool parse_only) {
auto nt = parse_mixfix_notation(p, k, overload, reserve, parse_only);
if (nt.second)
new_tokens.push_back(*nt.second);
return nt.first;
@ -401,15 +389,13 @@ static optional<pair<action, parse_table>> find_next(optional<parse_table> const
return optional<pair<action, parse_table>>();
}
static notation_entry parse_notation_core(parser & p, bool overload, bool reserve, buffer<token_entry> & new_tokens) {
static notation_entry parse_notation_core(parser & p, bool overload, bool reserve, buffer<token_entry> & new_tokens, bool parse_only) {
buffer<expr> locals;
buffer<transition> ts;
parser::local_scope scope(p);
bool is_nud = true;
optional<parse_table> pt;
optional<parse_table> reserved_pt;
notation_modifiers mod;
mod.parse(p);
if (p.curr_is_numeral()) {
lean_assert(p.curr_is_numeral());
mpz num = p.get_num_val().get_numerator();
@ -418,7 +404,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
auto e_pos = p.pos();
expr e = p.parse_expr();
check_notation_expr(e, e_pos);
return notation_entry(num, e, overload, mod.m_parse_only);
return notation_entry(num, e, overload, parse_only);
} else if (p.curr_is_identifier()) {
parse_notation_local(p, locals);
is_nud = false;
@ -518,7 +504,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
throw parser_error("invalid notation declaration, empty notation is not allowed", p.pos());
n = parse_notation_expr(p, locals);
}
return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, reserve, mod.m_parse_only);
return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, reserve, parse_only);
}
bool curr_is_notation_decl(parser & p) {
@ -529,22 +515,23 @@ bool curr_is_notation_decl(parser & p) {
static notation_entry parse_notation(parser & p, bool overload, bool reserve, buffer<token_entry> & new_tokens,
bool allow_local) {
bool parse_only = false;
flet<bool> set_allow_local(g_allow_local, allow_local);
if (p.curr_is_token(get_infix_tk()) || p.curr_is_token(get_infixl_tk())) {
p.next();
return parse_mixfix_notation(p, mixfix_kind::infixl, overload, reserve, new_tokens);
return parse_mixfix_notation(p, mixfix_kind::infixl, overload, reserve, new_tokens, parse_only);
} else if (p.curr_is_token(get_infixr_tk())) {
p.next();
return parse_mixfix_notation(p, mixfix_kind::infixr, overload, reserve, new_tokens);
return parse_mixfix_notation(p, mixfix_kind::infixr, overload, reserve, new_tokens, parse_only);
} else if (p.curr_is_token(get_postfix_tk())) {
p.next();
return parse_mixfix_notation(p, mixfix_kind::postfix, overload, reserve, new_tokens);
return parse_mixfix_notation(p, mixfix_kind::postfix, overload, reserve, new_tokens, parse_only);
} else if (p.curr_is_token(get_prefix_tk())) {
p.next();
return parse_mixfix_notation(p, mixfix_kind::prefix, overload, reserve, new_tokens);
return parse_mixfix_notation(p, mixfix_kind::prefix, overload, reserve, new_tokens, parse_only);
} else if (p.curr_is_token(get_notation_tk())) {
p.next();
return parse_notation_core(p, overload, reserve, new_tokens);
return parse_notation_core(p, overload, reserve, new_tokens, parse_only);
} else {
throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'prefix', "
"'postfix' or 'notation' expected", p.pos());
@ -583,9 +570,9 @@ static void check_token(char const * tk) {
}
}
static environment add_user_token(environment const & env, token_entry const & e) {
static environment add_user_token(environment const & env, token_entry const & e, bool persistent) {
check_token(e.m_token.c_str());
return add_token(env, e);
return add_token(env, e, persistent);
}
static environment add_user_token(environment const & env, char const * val, unsigned prec) {
@ -593,23 +580,47 @@ static environment add_user_token(environment const & env, char const * val, uns
return add_token(env, val, prec);
}
struct notation_modifiers {
bool m_persistent;
bool m_parse_only;
notation_modifiers():m_persistent(true), m_parse_only(false) {}
void parse(parser & p) {
while (true) {
if (p.curr_is_token(get_local_tk())) {
p.next();
m_persistent = false;
} else if (p.curr_is_token(get_parsing_only_tk())) {
p.next();
m_parse_only = true;
} else {
return;
}
}
}
};
static environment notation_cmd_core(parser & p, bool overload, bool reserve) {
flet<bool> set_allow_local(g_allow_local, in_context(p.env()));
notation_modifiers mods;
mods.parse(p);
flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !mods.m_persistent);
environment env = p.env();
buffer<token_entry> new_tokens;
auto ne = parse_notation_core(p, overload, reserve, new_tokens);
auto ne = parse_notation_core(p, overload, reserve, new_tokens, mods.m_parse_only);
for (auto const & te : new_tokens)
env = add_user_token(env, te);
env = add_notation(env, ne);
env = add_user_token(env, te, mods.m_persistent);
env = add_notation(env, ne, mods.m_persistent);
return env;
}
static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool reserve) {
flet<bool> set_allow_local(g_allow_local, in_context(p.env()));
auto nt = parse_mixfix_notation(p, k, overload, reserve);
notation_modifiers mods;
mods.parse(p);
flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !mods.m_persistent);
auto nt = parse_mixfix_notation(p, k, overload, reserve, mods.m_parse_only);
environment env = p.env();
if (nt.second)
env = add_user_token(env, *nt.second);
env = add_notation(env, nt.first);
env = add_user_token(env, *nt.second, mods.m_persistent);
env = add_notation(env, nt.first, mods.m_persistent);
return env;
}

8
src/frontends/lean/parser_config.cpp
View file

@ -107,8 +107,8 @@ std::string * token_config::g_key = nullptr;
template class scoped_ext<token_config>;
typedef scoped_ext<token_config> token_ext;
environment add_token(environment const & env, token_entry const & e) {
return token_ext::add_entry(env, get_dummy_ios(), e);
environment add_token(environment const & env, token_entry const & e, bool persistent) {
return token_ext::add_entry(env, get_dummy_ios(), e, persistent);
}
environment add_token(environment const & env, char const * val, unsigned prec) {
@ -307,8 +307,8 @@ std::string * notation_config::g_key = nullptr;
template class scoped_ext<notation_config>;
typedef scoped_ext<notation_config> notation_ext;
environment add_notation(environment const & env, notation_entry const & e) {
return notation_ext::add_entry(env, get_dummy_ios(), e);
environment add_notation(environment const & env, notation_entry const & e, bool persistent) {
return notation_ext::add_entry(env, get_dummy_ios(), e, persistent);
}
environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts,

4
src/frontends/lean/parser_config.h
View file

@ -58,8 +58,8 @@ inline bool operator!=(notation_entry const & e1, notation_entry const & e2) {
/** \brief Apply \c f to expressions embedded in the notation entry */
notation_entry replace(notation_entry const & e, std::function<expr(expr const &)> const & f);
environment add_token(environment const & env, token_entry const & e);
environment add_notation(environment const & env, notation_entry const & e);
environment add_token(environment const & env, token_entry const & e, bool persistent = true);
environment add_notation(environment const & env, notation_entry const & e, bool persistent = true);
environment add_token(environment const & env, char const * val, unsigned prec);
environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,

2
src/frontends/lean/token_table.cpp
View file

@ -82,7 +82,7 @@ void init_token_table(token_table & t) {
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[parsing-only]", "reducible", "irreducible",
"evaluate", "check", "eval", "[whnf]", "[strict]", "[priority", "print", "end", "namespace", "section", "import",
"evaluate", "check", "eval", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "import",
"inductive", "record", "structure", "module", "universe", "universes",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
"exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",

4
src/frontends/lean/tokens.cpp
View file

@ -93,6 +93,7 @@ static name * g_prefix = nullptr;
static name * g_notation = nullptr;
static name * g_call = nullptr;
static name * g_persistent = nullptr;
static name * g_local = nullptr;
static name * g_root = nullptr;
static name * g_fields = nullptr;
@ -183,12 +184,14 @@ void initialize_tokens() {
g_notation = new name("notation");
g_call = new name("call");
g_persistent = new name("[persistent]");
g_local = new name("[local]");
g_root = new name("_root_");
g_fields = new name("fields");
}
void finalize_tokens() {
delete g_persistent;
delete g_local;
delete g_root;
delete g_fields;
delete g_prev;
@ -364,6 +367,7 @@ name const & get_prefix_tk() { return *g_prefix; }
name const & get_notation_tk() { return *g_notation; }
name const & get_call_tk() { return *g_call; }
name const & get_persistent_tk() { return *g_persistent; }
name const & get_local_tk() { return *g_local; }
name const & get_root_tk() { return *g_root; }
name const & get_fields_tk() { return *g_fields; }
}

1
src/frontends/lean/tokens.h
View file

@ -95,6 +95,7 @@ name const & get_prefix_tk();
name const & get_notation_tk();
name const & get_call_tk();
name const & get_persistent_tk();
name const & get_local_tk();
name const & get_root_tk();
name const & get_fields_tk();
}

12
src/library/scoped_ext.h
View file

@ -202,16 +202,14 @@ public:
if (auto h = get_fingerprint(e)) {
env = update_fingerprint(env, *h);
}
if (in_context(env)) {
if (in_context(env) || !persistent) {
return update(env, get(env)._add_tmp_entry(env, ios, e));
} else {
name n = get_namespace(env);
if (persistent) {
env = module::add(env, get_serialization_key(), [=](serializer & s) {
s << n;
write_entry(s, e);
});
}
env = module::add(env, get_serialization_key(), [=](serializer & s) {
s << n;
write_entry(s, e);
});
return update(env, get(env)._add_entry(env, ios, e));
}
}

2
tests/lean/run/e6.lean
View file

@ -12,7 +12,7 @@ namespace int
constant add : int → int → int
infixl + := add
constant of_nat : nat → int
coercion of_nat
coercion [persistent] of_nat
end int
open int

2
tests/lean/run/e9.lean
View file

@ -15,7 +15,7 @@ namespace int
end int
namespace int_coercions
coercion int.of_nat
coercion [persistent] int.of_nat
end int_coercions
-- Open "only" the notation and declarations from the namespaces nat and int

16
tests/lean/run/group4.lean
View file

@ -80,26 +80,26 @@ print prefix algebra.comm_monoid
structure Semigroup :=
mk :: (carrier : Type) (struct : semigroup carrier)
coercion Semigroup.carrier
instance Semigroup.struct
coercion [persistent] Semigroup.carrier
instance [persistent] Semigroup.struct
structure CommSemigroup :=
mk :: (carrier : Type) (struct : comm_semigroup carrier)
coercion CommSemigroup.carrier
instance CommSemigroup.struct
coercion [persistent] CommSemigroup.carrier
instance [persistent] CommSemigroup.struct
structure Monoid :=
mk :: (carrier : Type) (struct : monoid carrier)
coercion Monoid.carrier
instance Monoid.struct
coercion [persistent] Monoid.carrier
instance [persistent] Monoid.struct
structure CommMonoid :=
mk :: (carrier : Type) (struct : comm_monoid carrier)
coercion CommMonoid.carrier
instance CommMonoid.struct
coercion [persistent] CommMonoid.carrier
instance [persistent] CommMonoid.struct
end algebra

16
tests/lean/run/group5.lean
View file

@ -78,26 +78,26 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
structure Semigroup :=
(carrier : Type) (struct : semigroup carrier)
coercion Semigroup.carrier
instance Semigroup.struct
coercion [persistent] Semigroup.carrier
instance [persistent] Semigroup.struct
structure CommSemigroup :=
(carrier : Type) (struct : comm_semigroup carrier)
coercion CommSemigroup.carrier
instance CommSemigroup.struct
coercion [persistent] CommSemigroup.carrier
instance [persistent] CommSemigroup.struct
structure Monoid :=
(carrier : Type) (struct : monoid carrier)
coercion Monoid.carrier
instance Monoid.struct
coercion [persistent] Monoid.carrier
instance [persistent] Monoid.struct
structure CommMonoid :=
(carrier : Type) (struct : comm_monoid carrier)
coercion CommMonoid.carrier
instance CommMonoid.struct
coercion [persistent] CommMonoid.carrier
instance [persistent] CommMonoid.struct
end algebra

11
tests/lean/run/local_notation.lean Normal file
View file

@ -0,0 +1,11 @@
import logic
section
variables {A : Type}
variables f : A → A → A
infixl [local] `+++`:10 := f
variables a b c : A
check f a b
check a +++ b
end