From 6bfd4eb9cf71dac888e8e5eb67ebe33cce7f96bb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Sep 2016 12:18:52 -0700 Subject: [PATCH] feat(frontends/lean): add 'instance' keyword --- library/init/instances.lean | 16 +++++---------- library/init/logic.lean | 6 ++---- src/emacs/lean-syntax.el | 10 +++++----- src/frontends/lean/decl_attributes.cpp | 27 +++++++++++++++++++------- src/frontends/lean/decl_attributes.h | 6 ++---- src/frontends/lean/decl_cmds.cpp | 9 +++++++++ src/frontends/lean/token_table.cpp | 2 +- 7 files changed, 44 insertions(+), 32 deletions(-) diff --git a/library/init/instances.lean b/library/init/instances.lean index e22d1b5663..3eaaef8007 100644 --- a/library/init/instances.lean +++ b/library/init/instances.lean @@ -8,23 +8,17 @@ import init.meta.mk_dec_eq_instance init.subtype init.meta.occurrences init.sum open tactic subtype universe variables u v -attribute [instance] -def subtype_decidable_eq {A : Type u} {p : A → Prop} [decidable_eq A] : decidable_eq {x : A // p x} := +instance subtype.decidable_eq {A : Type u} {p : A → Prop} [decidable_eq A] : decidable_eq {x : A // p x} := by mk_dec_eq_instance -set_option trace.app_builder true -attribute [instance] -def list_decidable_eq {A : Type u} [decidable_eq A] : decidable_eq (list A) := +instance list.decidable_eq {A : Type u} [decidable_eq A] : decidable_eq (list A) := by mk_dec_eq_instance -attribute [instance] -def occurrences_decidable_eq : decidable_eq occurrences := +instance occurrences.decidable_eq : decidable_eq occurrences := by mk_dec_eq_instance -attribute [instance] -def unit_decidable_eq : decidable_eq unit := +instance unit.decidable_eq : decidable_eq unit := by mk_dec_eq_instance -attribute [instance] -def sum_decidable {A : Type u} {B : Type v} [decidable_eq A] [decidable_eq B] : decidable_eq (A ⊕ B) := +instance sum.decidable {A : Type u} {B : Type v} [decidable_eq A] [decidable_eq B] : decidable_eq (A ⊕ B) := by mk_dec_eq_instance diff --git a/library/init/logic.lean b/library/init/logic.lean index eb06d03f4d..75af81dbca 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -639,12 +639,10 @@ inductive [class] decidable (p : Prop) export decidable (is_true is_false) -attribute [instance] -definition decidable_true : decidable true := +instance decidable.true : decidable true := is_true trivial -attribute [instance] -definition decidable_false : decidable false := +instance decidable.false : decidable false := is_false not_false -- We use "dependent" if-then-else to be able to communicate the if-then-else condition diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 512406a6e0..b83c82e323 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -14,7 +14,7 @@ "print" "theorem" "proposition" "example" "abstract" "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes" "alias" "help" "precedence" "reserve" "declare_trace" "add_key_equivalence" - "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" + "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance" "eval" "vm_eval" "check" "end" "reveal" "this" "suppose" "using_well_founded" "namespace" "section" "fields" "find_decl" "attribute" "local" "set_option" "extends" "include" "omit" "classes" @@ -131,7 +131,7 @@ ;; attributes after definitions (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) + "hypothesis" "definition" "meta_definition" "instance" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace))) (zero-or-more whitespace) @@ -141,7 +141,7 @@ (2 'font-lock-doc-face) (4 'font-lock-function-name-face)) (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) + "hypothesis" "definition" "meta_definition" "instance" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace))) (zero-or-more whitespace) @@ -149,7 +149,7 @@ (2 'font-lock-doc-face) (3 'font-lock-function-name-face)) (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) + "hypothesis" "definition" "meta_definition" "instance" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (zero-or-more "{" (zero-or-more (not (any "}"))) "}" (zero-or-more whitespace))) (zero-or-more whitespace) @@ -180,7 +180,7 @@ ;; universe/inductive/theorem... "names" (without attributes) (,(rx word-start (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary" - "hypothesis" "definition" "meta_definition" "constant" "meta_constant")) + "hypothesis" "definition" "meta_definition" "instance" "constant" "meta_constant")) word-end (zero-or-more whitespace) (group (zero-or-more (not (any " \t\n\r{(["))))) diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index efa9cf92c4..39d13e4212 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -27,8 +27,14 @@ void decl_attributes::parse(parser & p) { throw parser_error("cannot remove attribute globally (solution: use 'local attribute')", pos); p.next(); } - auto name = p.check_id_next("invalid attribute declaration, identifier expected"); - if (name == "priority") { + name id; + if (p.curr_is_command()) { + id = p.get_token_info().value(); + p.next(); + } else { + id = p.check_id_next("invalid attribute declaration, identifier expected"); + } + if (id == "priority") { if (deleted) throw parser_error("cannot remove priority attribute", pos); auto pos = p.pos(); @@ -44,14 +50,14 @@ void decl_attributes::parse(parser & p) { throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos); } } else { - if (!is_attribute(p.env(), name)) - throw parser_error(sstream() << "unknown attribute [" << name << "]", pos); + if (!is_attribute(p.env(), id)) + throw parser_error(sstream() << "unknown attribute [" << id << "]", pos); - auto const & attr = get_attribute(p.env(), name); + auto const & attr = get_attribute(p.env(), id); if (!deleted) { for (auto const & entry : m_entries) { if (!entry.deleted() && are_incompatible(*entry.m_attr, attr)) { - throw parser_error(sstream() << "invalid attribute [" << name + throw parser_error(sstream() << "invalid attribute [" << id << "], declaration was already marked with [" << entry.m_attr->get_name() << "]", pos); @@ -60,7 +66,7 @@ void decl_attributes::parse(parser & p) { } auto data = deleted ? attr_data_ptr() : attr.parse_data(p); m_entries = cons({&attr, data}, m_entries); - if (name == "parsing_only") + if (id == "parsing_only") m_parsing_only = true; } if (p.curr_is_token(get_comma_tk())) { @@ -75,6 +81,13 @@ void decl_attributes::parse(parser & p) { } } +void decl_attributes::add_attribute(environment const & env, name const & attr_name) { + if (!is_attribute(env, attr_name)) + throw exception(sstream() << "unknown attribute [" << attr_name << "]"); + auto const & attr = get_attribute(env, attr_name); + m_entries = cons({&attr, get_default_attr_data()}, m_entries); +} + environment decl_attributes::apply(environment env, io_state const & ios, name const & d) const { buffer entries; to_buffer(m_entries, entries); diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h index 70554c0a6b..c36f779d72 100644 --- a/src/frontends/lean/decl_attributes.h +++ b/src/frontends/lean/decl_attributes.h @@ -16,10 +16,7 @@ public: struct entry { attribute const * m_attr; attr_data_ptr m_params; - - bool deleted() const { - return !static_cast(m_params); - } + bool deleted() const { return !static_cast(m_params); } }; private: bool m_persistent; @@ -28,6 +25,7 @@ private: optional m_prio; public: decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false) {} + void add_attribute(environment const & env, name const & attr_name); void parse(parser & p); environment apply(environment env, io_state const & ios, name const & d) const; list const & get_entries() const { return m_entries; } diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 1728ab2351..42b44ca3bf 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -569,6 +569,14 @@ static environment reveal_cmd(parser & p) { return p.reveal_theorems(ds); } +static environment instance_cmd(parser & p) { + bool persistent = true; + decl_attributes attributes(true); + attributes.add_attribute(p.env(), "instance"); + bool is_private = false; bool is_protected = true; bool is_noncomputable = false; + return definition_cmd_core(p, def_cmd_kind::Definition, is_private, is_protected, is_noncomputable, attributes); +} + void register_decl_cmds(cmd_table & r) { add_cmd(r, cmd_info("universe", "declare a universe level", universe_cmd)); add_cmd(r, cmd_info("universes", "declare universe levels", universes_cmd)); @@ -591,6 +599,7 @@ void register_decl_cmds(cmd_table & r) { add_cmd(r, cmd_info("reveal", "reveal given theorems", reveal_cmd)); add_cmd(r, cmd_info("include", "force section parameter/variable to be included", include_cmd)); add_cmd(r, cmd_info("attribute", "set declaration attributes", attribute_cmd)); + add_cmd(r, cmd_info("instance", "declare a new instance", instance_cmd)); add_cmd(r, cmd_info("omit", "undo 'include' command", omit_cmd)); add_cmd(r, cmd_info("mutual_definition", "declare a mutually recursive definition", definition_cmd, false)); add_cmd(r, cmd_info("mutual_meta_definition", "declare a mutually recursive meta_definition", definition_cmd, false)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 92b4b684e3..dcf7e44693 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) { "tactic_infixl", "tactic_infixr", "tactic_infix", "tactic_postfix", "tactic_prefix", "tactic_notation", "exit", "set_option", "open", "export", "override", "tactic_hint", "add_begin_end_tactic", "set_begin_end_tactic", - "multiple_instances", "find_decl", "attribute", "persistent", + "multiple_instances", "find_decl", "attribute", "persistent", "instance", "mutual_inductive", "include", "omit", "migrate", "init_quotient", "init_hits", "declare_trace", "register_simp_ext", "run_command", "add_key_equivalence", "#erase_cache",