From 397395bbc932d8e2da4609aad2d22e6e6c197a48 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Sep 2014 12:20:42 -0700 Subject: [PATCH] feat(frontends/lean): allow user to associate priorities to class-instances, closes #180 --- library/priority.lean | 6 ++ src/emacs/lean-syntax.el | 1 + src/frontends/lean/class.cpp | 93 ++++++++++++++++++++++++------ src/frontends/lean/class.h | 6 +- src/frontends/lean/decl_cmds.cpp | 24 ++++++-- src/frontends/lean/parse_table.cpp | 3 +- src/frontends/lean/token_table.cpp | 27 +++++---- src/frontends/lean/tokens.cpp | 4 ++ src/frontends/lean/tokens.h | 1 + tests/lean/inst.lean | 24 ++++++++ tests/lean/inst.lean.expected.out | 1 + 11 files changed, 153 insertions(+), 37 deletions(-) create mode 100644 library/priority.lean create mode 100644 tests/lean/inst.lean create mode 100644 tests/lean/inst.lean.expected.out diff --git a/library/priority.lean b/library/priority.lean new file mode 100644 index 000000000..ea309e247 --- /dev/null +++ b/library/priority.lean @@ -0,0 +1,6 @@ +import data.num + +namespace priority +definition default : num := 1000 +definition max : num := 4294967295 +end priority diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 54876e275..fce4d3bc1 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -72,6 +72,7 @@ ;; modifiers (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face) + (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face) ;; tactics (,(rx symbol-start (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "apply" "back" "beta" "done" "exact" "repeat") diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index 610fad622..4aa737a9a 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -11,34 +11,66 @@ Author: Leonardo de Moura #include "library/scoped_ext.h" #include "library/kernel_serializer.h" #include "library/reducible.h" +#include "library/num.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" #include "frontends/lean/tactic_hint.h" +#include "frontends/lean/tokens.h" + +#ifndef LEAN_INSTANCE_DEFAULT_PRIORITY +#define LEAN_INSTANCE_DEFAULT_PRIORITY 1000 +#endif namespace lean { struct class_entry { - bool m_class_cmd; - name m_class; - name m_instance; // only relevant if m_class_cmd == false - class_entry():m_class_cmd(false) {} - explicit class_entry(name const & c):m_class_cmd(true), m_class(c) {} - class_entry(name const & c, name const & i):m_class_cmd(false), m_class(c), m_instance(i) {} + bool m_class_cmd; + name m_class; + name m_instance; // only relevant if m_class_cmd == false + unsigned m_priority; // only relevant if m_class_cmd == false + class_entry():m_class_cmd(false), m_priority(0) {} + explicit class_entry(name const & c):m_class_cmd(true), m_class(c), m_priority(0) {} + class_entry(name const & c, name const & i, unsigned p): + m_class_cmd(false), m_class(c), m_instance(i), m_priority(p) {} }; struct class_state { typedef name_map> class_instances; - class_instances m_instances; + typedef name_map instance_priorities; + class_instances m_instances; + instance_priorities m_priorities; + + unsigned get_priority(name const & i) const { + if (auto it = m_priorities.find(i)) + return *it; + else + return LEAN_INSTANCE_DEFAULT_PRIORITY; + } + + list insert(name const & inst, unsigned priority, list const & insts) const { + if (!insts) + return to_list(inst); + else if (priority >= get_priority(head(insts))) + return list(inst, insts); + else + return list(head(insts), insert(inst, priority, tail(insts))); + } + void add_class(name const & c) { auto it = m_instances.find(c); if (!it) m_instances.insert(c, list()); } - void add_instance(name const & c, name const & i) { + + void add_instance(name const & c, name const & i, unsigned p) { auto it = m_instances.find(c); - if (!it) + if (!it) { m_instances.insert(c, to_list(i)); - else - m_instances.insert(c, cons(i, filter(*it, [&](name const & i1) { return i1 != i; }))); + } else { + auto lst = filter(*it, [&](name const & i1) { return i1 != i; }); + m_instances.insert(c, insert(i, p, lst)); + } + if (p != LEAN_INSTANCE_DEFAULT_PRIORITY) + m_priorities.insert(i, p); } }; @@ -52,7 +84,7 @@ struct class_config { if (e.m_class_cmd) s.add_class(e.m_class); else - s.add_instance(e.m_class, e.m_instance); + s.add_instance(e.m_class, e.m_instance, e.m_priority); } static name const & get_class_name() { return *g_class_name; @@ -64,7 +96,7 @@ struct class_config { if (e.m_class_cmd) s << true << e.m_class; else - s << false << e.m_class << e.m_instance; + s << false << e.m_class << e.m_instance << e.m_priority; } static entry read_entry(deserializer & d) { entry e; @@ -72,7 +104,7 @@ struct class_config { if (e.m_class_cmd) d >> e.m_class; else - d >> e.m_class >> e.m_instance; + d >> e.m_class >> e.m_instance >> e.m_priority; return e; } }; @@ -100,7 +132,7 @@ environment add_class(environment const & env, name const & n, bool persistent) } static name * g_tmp_prefix = nullptr; -environment add_instance(environment const & env, name const & n, bool persistent) { +environment add_instance(environment const & env, name const & n, unsigned priority, bool persistent) { declaration d = env.get(n); expr type = d.get_type(); name_generator ngen(*g_tmp_prefix); @@ -112,7 +144,11 @@ environment add_instance(environment const & env, name const & n, bool persisten type = instantiate(binding_body(type), mk_local(ngen.next(), binding_domain(type))); } name c = get_class_name(env, get_app_fn(type)); - return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n), persistent); + return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n, priority), persistent); +} + +environment add_instance(environment const & env, name const & n, bool persistent) { + return add_instance(env, n, LEAN_INSTANCE_DEFAULT_PRIORITY, persistent); } bool is_class(environment const & env, name const & c) { @@ -125,15 +161,38 @@ list get_class_instances(environment const & env, name const & c) { return ptr_to_list(s.m_instances.find(c)); } +optional parse_instance_priority(parser & p) { + if (p.curr_is_token(get_priority_tk())) { + p.next(); + auto pos = p.pos(); + expr val = p.parse_expr(); + val = type_checker(p.env()).whnf(val).first; + if (optional mpz_val = to_num(val)) { + if (!mpz_val->is_unsigned_int()) + throw parser_error("invalid 'priority', argument does not fit in a machine integer", pos); + p.check_token_next(get_rbracket_tk(), "invalid 'priority', ']' expected"); + return optional(mpz_val->get_unsigned_int()); + } else { + throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos); + } + } else { + return optional(); + } +} + environment add_instance_cmd(parser & p) { bool found = false; bool persistent = false; parse_persistent(p, persistent); + optional priority = parse_instance_priority(p); environment env = p.env(); while (p.curr_is_identifier()) { found = true; name c = p.check_constant_next("invalid 'class instance' declaration, constant expected"); - env = add_instance(env, c, persistent); + if (priority) + env = add_instance(env, c, *priority, persistent); + else + env = add_instance(env, c, persistent); } if (!found) throw parser_error("invalid 'class instance' declaration, at least one identifier expected", p.pos()); diff --git a/src/frontends/lean/class.h b/src/frontends/lean/class.h index 5c3a716eb..08f3ac003 100644 --- a/src/frontends/lean/class.h +++ b/src/frontends/lean/class.h @@ -13,13 +13,17 @@ Author: Leonardo de Moura namespace lean { /** \brief Add a new 'class' to the environment (if it is not already declared) */ environment add_class(environment const & env, name const & n, bool persistent = true); -/** \brief Add a new 'class instance' to the environment. */ +/** \brief Add a new 'class instance' to the environment with default priority. */ environment add_instance(environment const & env, name const & n, bool persistent = true); +/** \brief Add a new 'class instance' to the environment. */ +environment add_instance(environment const & env, name const & n, unsigned priority, bool persistent); /** \brief Return true iff \c c was declared with \c add_class . */ bool is_class(environment const & env, name const & c); /** \brief Return the instances of the given class. */ list get_class_instances(environment const & env, name const & c); name get_class_name(environment const & env, expr const & e); +/** \brief Parse priority for an class instance */ +optional parse_instance_priority(parser & p); void register_class_cmds(cmd_table & r); /** \brief Return true iff \c type is a class or Pi that produces a class. */ diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 4a78d1545..38f714d9a 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -149,10 +149,11 @@ environment axiom_cmd(parser & p) { } struct decl_modifiers { - bool m_is_instance; - bool m_is_coercion; - bool m_is_reducible; - decl_modifiers() { + bool m_is_instance; + bool m_is_coercion; + bool m_is_reducible; + optional m_priority; + decl_modifiers():m_priority() { m_is_instance = false; m_is_coercion = false; m_is_reducible = false; @@ -160,6 +161,7 @@ struct decl_modifiers { void parse(parser & p) { while (true) { + auto pos = p.pos(); if (p.curr_is_token(get_instance_tk())) { m_is_instance = true; p.next(); @@ -169,6 +171,10 @@ struct decl_modifiers { } else if (p.curr_is_token(get_reducible_tk())) { m_is_reducible = true; p.next(); + } else if (auto it = parse_instance_priority(p)) { + m_priority = *it; + if (!m_is_instance) + throw parser_error("invalid '[priority]' occurrence, declaration must be marked as an '[instance]'", pos); } else { break; } @@ -332,8 +338,14 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo if (real_n != n) env = add_expr_alias_rec(env, n, real_n); - if (modifiers.m_is_instance) - env = add_instance(env, real_n); + if (modifiers.m_is_instance) { + bool persistent = true; + if (modifiers.m_priority) { + env = add_instance(env, real_n, *modifiers.m_priority, persistent); + } else { + env = add_instance(env, real_n, persistent); + } + } if (modifiers.m_is_coercion) env = add_coercion(env, real_n, p.ios()); if (is_protected) diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index bd2525fa7..4592db00f 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -357,7 +357,8 @@ parse_table parse_table::add(unsigned num, transition const * ts, expr const & a return add_core(num, ts, new_a, overload); } -void parse_table::for_each(buffer & ts, std::function const &)> const & fn) const { +void parse_table::for_each(buffer & ts, + std::function const &)> const & fn) const { if (!is_nil(m_ptr->m_accept)) fn(ts.size(), ts.data(), m_ptr->m_accept); m_ptr->m_children.for_each([&](name const & k, pair const & p) { diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index aa125d020..b0debf4d1 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -71,19 +71,22 @@ void init_token_table(token_table & t) { pair builtin[] = {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, {"by", 0}, {"then", 0}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, - {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec}, {"using", 0}, - {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, - {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec}, - {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; + {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, + {"Type'", g_max_prec}, {"using", 0}, {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, + {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, + {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, + {"including", 0}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, + {nullptr, 0}}; - char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion", - "variables", "[persistent]", "[visible]", "[instance]", - "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "irreducible", - "evaluate", "check", "eval", "print", "end", "namespace", "section", "import", - "inductive", "record", "renaming", "extends", "structure", "module", "universe", - "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context", - "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "tactic_hint", - "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "#erase_cache", nullptr}; + char const * commands[] = + {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion", + "variables", "[persistent]", "[visible]", "[instance]", + "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "irreducible", + "evaluate", "check", "eval", "[priority", "print", "end", "namespace", "section", "import", + "inductive", "record", "renaming", "extends", "structure", "module", "universe", + "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context", + "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "tactic_hint", + "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "#erase_cache", nullptr}; pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index ea947b7f5..d573eccb4 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -63,6 +63,7 @@ static name * g_axiom = nullptr; static name * g_variable = nullptr; static name * g_opaque = nullptr; static name * g_instance = nullptr; +static name * g_priority = nullptr; static name * g_coercion = nullptr; static name * g_reducible = nullptr; static name * g_with = nullptr; @@ -140,6 +141,7 @@ void initialize_tokens() { g_axiom = new name("axiom"); g_variable = new name("variable"); g_instance = new name("[instance]"); + g_priority = new name("[priority"); g_coercion = new name("[coercion]"); g_reducible = new name("[reducible]"); g_with = new name("with"); @@ -185,6 +187,7 @@ void finalize_tokens() { delete g_axiom; delete g_variable; delete g_instance; + delete g_priority; delete g_coercion; delete g_reducible; delete g_in; @@ -295,6 +298,7 @@ name const & get_axiom_tk() { return *g_axiom; } name const & get_variable_tk() { return *g_variable; } name const & get_opaque_tk() { return *g_opaque; } name const & get_instance_tk() { return *g_instance; } +name const & get_priority_tk() { return *g_priority; } name const & get_coercion_tk() { return *g_coercion; } name const & get_reducible_tk() { return *g_reducible; } name const & get_class_tk() { return *g_class; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index bbe7e999f..fa8f5876e 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -65,6 +65,7 @@ name const & get_axiom_tk(); name const & get_variable_tk(); name const & get_opaque_tk(); name const & get_instance_tk(); +name const & get_priority_tk(); name const & get_coercion_tk(); name const & get_reducible_tk(); name const & get_class_tk(); diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean new file mode 100644 index 000000000..b7008e20f --- /dev/null +++ b/tests/lean/inst.lean @@ -0,0 +1,24 @@ +import logic data.prod priority +open priority +set_option pp.notation false + +inductive C (A : Type) := +mk : A → C A + +definition val {A : Type} (c : C A) : A := +C.rec (λa, a) c + +variable magic (A : Type) : A +definition C_magic [instance] [priority max] (A : Type) : C A := +C.mk (magic A) + +definition C_prop [instance] : C Prop := +C.mk true + +definition C_prod [instance] {A B : Type} (Ha : C A) (Hb : C B) : C (prod A B) := +C.mk (pair (val Ha) (val Hb)) + +-- C_magic will be used because it has max priority +definition test : C (prod Prop Prop) := _ + +eval test diff --git a/tests/lean/inst.lean.expected.out b/tests/lean/inst.lean.expected.out new file mode 100644 index 000000000..4c24c7b80 --- /dev/null +++ b/tests/lean/inst.lean.expected.out @@ -0,0 +1 @@ +C.mk (magic (prod Prop Prop))