refactor(*): normalize metaclass names

@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).

Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write

   definition foo [coercion] ...
   definition bla [forward] ...

and

  open [coercion] nat
  open [forward] nat

It is easier to remember and is uniform.
This commit is contained in:
Leonardo de Moura 2015-12-28 10:30:23 -08:00
parent 96bec8b4f9
commit f177082c3b
45 changed files with 112 additions and 105 deletions

View file

@ -17,11 +17,11 @@ namespace core
export empty (hiding elim)
export sum (hiding elim)
export sigma (hiding pr1 pr2)
export [notations] prod
export [notations] nat
export [notation] prod
export [notation] nat
export eq (idp idpath concat inverse transport ap ap10 cast tr_inv homotopy ap11 apd refl)
export [declarations] function
export [declaration] function
export equiv (to_inv to_right_inv to_left_inv)
export is_equiv (inv right_inv left_inv adjointify)
export [abbreviations] [declarations] is_trunc (trunctype hprop.mk hset.mk)
export [abbreviation] [declaration] is_trunc (trunctype hprop.mk hset.mk)
end core

View file

@ -373,5 +373,5 @@ namespace is_equiv
end is_equiv
export [unfold_hints] equiv
export [unfold_hints] is_equiv
export [unfold] equiv
export [unfold] is_equiv

View file

@ -60,4 +60,4 @@ notation f ` -[` op `]- ` g := combine f op g
end function
-- copy reducible annotations to top-level
export [reduce_hints] [unfold_hints] function
export [reducible] [unfold] function

View file

@ -7,7 +7,7 @@ Finite bags.
-/
import data.nat data.list.perm algebra.binary
open nat quot list subtype binary function eq.ops
open [declarations] perm
open [decl] perm
variable {A : Type}

View file

@ -7,7 +7,7 @@ Finite sets.
-/
import data.fintype.basic data.nat data.list.perm algebra.binary
open nat quot list subtype binary function eq.ops
open [declarations] perm
open [decl] perm
definition nodup_list (A : Type) := {l : list A | nodup l}

View file

@ -11,7 +11,7 @@ this bijection is implemeted using the Ackermann coding.
-/
import data.nat data.finset.equiv data.list
open nat binary
open - [notations] finset
open - [notation] finset
definition hf := nat
@ -479,7 +479,7 @@ theorem empty_mem_powerset (s : hf) : ∅ ∈ 𝒫 s :=
mem_powerset_of_subset (empty_subset s)
/- hf as lists -/
open - [notations] list
open - [notation] list
definition of_list (s : list hf) : hf :=
@equiv.to_fun _ _ list_nat_equiv_nat s

View file

@ -8,8 +8,8 @@ Definitions and properties of div and mod, following the SSReflect library.
Following SSReflect and the SMTlib standard, we define a % b so that 0 ≤ a % b < |b| when b ≠ 0.
-/
import data.int.order data.nat.div
open [coercions] [reduce_hints] nat
open [declarations] [classes] nat (succ)
open [coercion] [reducible] nat
open [declaration] [class] nat (succ)
open eq.ops
namespace int

View file

@ -22,7 +22,7 @@ The construction of the reals is arranged in four files.
-/
import data.nat data.rat.order data.pnat
open nat eq pnat
open - [coercions] rat
open - [coercion] rat
local postfix `⁻¹` := pnat.inv

View file

@ -163,7 +163,7 @@ theorem r_equiv_neg_abs_of_le_zero {s : reg_seq} (Hz : r_le s r_zero) : requiv (
end rat_seq
namespace real
open [classes] rat_seq
open [class] rat_seq
private theorem rewrite_helper9 (a b c : ) : b - c = (b - a) - (c - a) :=
by rewrite [-sub_add_eq_sub_sub_swap, sub_add_cancel]

View file

@ -581,7 +581,7 @@ theorem r_abs_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_abs s) (
end rat_seq
namespace real
open [classes] rat_seq
open [class] rat_seq
noncomputable protected definition inv (x : ) : :=
quot.lift_on x (λ a, quot.mk (rat_seq.r_inv a))

View file

@ -1015,7 +1015,7 @@ theorem r_le_of_reprs_le (s t : reg_seq) (Hle : ∀ n : +, r_le (r_const (reg
end rat_seq
open real
open [classes] rat_seq
open [class] rat_seq
namespace real
protected definition lt (x y : ) :=

View file

@ -156,4 +156,4 @@ theorem bijective_id : bijective (@id A) := and.intro injective_id surjective_id
end function
-- copy reducible annotations to top-level
export [reduce_hints] [unfold_hints] function
export [reducible] [unfold] function

View file

@ -38,7 +38,7 @@ protected definition metric_space [instance] : metric_space :=
open nat
open [classes] rat
open [class] rat
definition converges_to_seq (X : ) (y : ) : Prop :=
∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : , ∀ {n}, n ≥ N → abs (X n - y) < ε

View file

@ -54,10 +54,10 @@
'("persistent" "notation" "visible" "instance" "trans_instance"
"class" "parsing_only" "coercion" "unfold_full" "constructor"
"reducible" "irreducible" "semireducible" "quasireducible" "wf"
"whnf" "multiple_instances" "none" "decls" "declarations"
"coercions" "classes" "symm" "subst" "refl" "trans" "simp" "simps" "congr"
"forward" "no_pattern" "notations" "abbreviations" "begin_end_hints" "tactic_hints"
"reduce_hints" "unfold_hints" "aliases" "eqv" "intro" "intro!" "elim"
"whnf" "multiple_instances" "none" "decl" "declaration"
"relation" "symm" "subst" "refl" "trans" "simp" "congr"
"backward" "forward" "no_pattern" "begin_end" "tactic" "abbreviation"
"reducible" "unfold" "alias" "eqv" "intro" "intro!" "elim" "grinder"
"localrefinfo" "recursor"))
"lean modifiers")
(defconst lean-modifiers-regexp

View file

@ -78,8 +78,8 @@ bool is_begin_end_annotation(expr const & e) { return is_annotation(e, *g_begin_
bool is_begin_end_element_annotation(expr const & e) { return is_annotation(e, *g_begin_end_element); }
void initialize_begin_end_ext() {
g_class_name = new name("begin_end_hints");
g_key = new std::string("bepretac");
g_class_name = new name("begin_end");
g_key = new std::string("BEPRETAC");
begin_end_ext::initialize();
g_begin_end = new name("begin_end");
g_begin_end_element = new name("begin_end_element");

View file

@ -221,19 +221,26 @@ static optional<name> parse_metaclass(parser & p) {
p.next();
}
p.check_token_next(get_rbracket_tk(), "invalid 'open' command, ']' expected");
if (!is_metaclass(n) && n != get_decls_tk() && n != get_declarations_tk())
if (!is_metaclass(n) && n != get_decl_tk() && n != get_declaration_tk())
throw parser_error(sstream() << "invalid metaclass name '[" << n << "]'", pos);
return optional<name>(n);
} else if (p.curr() == scanner::token_kind::CommandKeyword) {
// Meta-classes whose name conflict with tokens of the form `[<id>]` `[<id>`
// Example: [class] and [unfold
name v = p.get_token_info().value();
if (v.is_atomic() && v.is_string() && v.size() > 2 && v.get_string()[0] == '[' && v.get_string()[v.size()-1] == ']') {
if (v.is_atomic() && v.is_string() && v.size() > 1 && v.get_string()[0] == '[') {
auto pos = p.pos();
p.next();
std::string s(v.get_string() + 1);
if (v.get_string()[v.size()-1] == ']')
s.pop_back();
name n(s);
if (!is_metaclass(n) && n != get_decls_tk() && n != get_declarations_tk())
if (!is_metaclass(n) && n != get_decl_tk() && n != get_declaration_tk())
throw parser_error(sstream() << "invalid metaclass name '[" << n << "]'", pos);
if (v.get_string()[v.size()-1] != ']') {
// Consume ']' for tokens such as `[unfold`
p.check_token_next(get_rbracket_tk(), "invalid 'open' command, ']' expected");
}
return optional<name>(n);
}
}
@ -245,12 +252,12 @@ static void parse_metaclasses(parser & p, buffer<name> & r) {
p.next();
buffer<name> tmp;
get_metaclasses(tmp);
tmp.push_back(get_decls_tk());
tmp.push_back(get_decl_tk());
while (true) {
if (optional<name> m = parse_metaclass(p)) {
tmp.erase_elem(*m);
if (*m == get_declarations_tk())
tmp.erase_elem(get_decls_tk());
if (*m == get_declaration_tk())
tmp.erase_elem(get_decl_tk());
} else {
break;
}
@ -299,8 +306,8 @@ environment open_export_cmd(parser & p, bool open) {
parse_metaclasses(p, metacls);
bool decls = false;
if (metacls.empty() ||
std::find(metacls.begin(), metacls.end(), get_decls_tk()) != metacls.end() ||
std::find(metacls.begin(), metacls.end(), get_declarations_tk()) != metacls.end())
std::find(metacls.begin(), metacls.end(), get_decl_tk()) != metacls.end() ||
std::find(metacls.begin(), metacls.end(), get_declaration_tk()) != metacls.end())
decls = true;
for (name const & n : metacls)
fingerprint = hash(fingerprint, n.hash());

View file

@ -437,11 +437,11 @@ cmd_table const & get_cmd_table(environment const & env) {
}
void initialize_parser_config() {
token_config::g_class_name = new name("notations");
token_config::g_key = new std::string("tk");
token_config::g_class_name = new name("notation");
token_config::g_key = new std::string("TK");
token_ext::initialize();
notation_config::g_class_name = new name("notations");
notation_config::g_key = new std::string("nota");
notation_config::g_class_name = new name("notation");
notation_config::g_key = new std::string("NOTA");
notation_ext::initialize();
g_ext = new cmd_ext_reg();
}

View file

@ -57,8 +57,8 @@ template class scoped_ext<tactic_hint_config>;
typedef scoped_ext<tactic_hint_config> tactic_hint_ext;
void initialize_tactic_hint() {
g_class_name = new name("tactic_hints");
g_key = new std::string("tachint");
g_class_name = new name("tactic");
g_key = new std::string("TACHINT");
tactic_hint_ext::initialize();
}

View file

@ -63,8 +63,8 @@ static name const * g_instances_tk = nullptr;
static name const * g_classes_tk = nullptr;
static name const * g_coercions_tk = nullptr;
static name const * g_arrow_tk = nullptr;
static name const * g_declarations_tk = nullptr;
static name const * g_decls_tk = nullptr;
static name const * g_declaration_tk = nullptr;
static name const * g_decl_tk = nullptr;
static name const * g_hiding_tk = nullptr;
static name const * g_exposing_tk = nullptr;
static name const * g_renaming_tk = nullptr;
@ -213,8 +213,8 @@ void initialize_tokens() {
g_classes_tk = new name{"classes"};
g_coercions_tk = new name{"coercions"};
g_arrow_tk = new name{"->"};
g_declarations_tk = new name{"declarations"};
g_decls_tk = new name{"decls"};
g_declaration_tk = new name{"declaration"};
g_decl_tk = new name{"decl"};
g_hiding_tk = new name{"hiding"};
g_exposing_tk = new name{"exposing"};
g_renaming_tk = new name{"renaming"};
@ -364,8 +364,8 @@ void finalize_tokens() {
delete g_classes_tk;
delete g_coercions_tk;
delete g_arrow_tk;
delete g_declarations_tk;
delete g_decls_tk;
delete g_declaration_tk;
delete g_decl_tk;
delete g_hiding_tk;
delete g_exposing_tk;
delete g_renaming_tk;
@ -514,8 +514,8 @@ name const & get_instances_tk() { return *g_instances_tk; }
name const & get_classes_tk() { return *g_classes_tk; }
name const & get_coercions_tk() { return *g_coercions_tk; }
name const & get_arrow_tk() { return *g_arrow_tk; }
name const & get_declarations_tk() { return *g_declarations_tk; }
name const & get_decls_tk() { return *g_decls_tk; }
name const & get_declaration_tk() { return *g_declaration_tk; }
name const & get_decl_tk() { return *g_decl_tk; }
name const & get_hiding_tk() { return *g_hiding_tk; }
name const & get_exposing_tk() { return *g_exposing_tk; }
name const & get_renaming_tk() { return *g_renaming_tk; }

View file

@ -65,8 +65,8 @@ name const & get_instances_tk();
name const & get_classes_tk();
name const & get_coercions_tk();
name const & get_arrow_tk();
name const & get_declarations_tk();
name const & get_decls_tk();
name const & get_declaration_tk();
name const & get_decl_tk();
name const & get_hiding_tk();
name const & get_exposing_tk();
name const & get_renaming_tk();

View file

@ -58,8 +58,8 @@ instances instances
classes classes
coercions coercions
arrow ->
declarations declarations
decls decls
declaration declaration
decl decl
hiding hiding
exposing exposing
renaming renaming

View file

@ -119,8 +119,8 @@ expr expand_abbreviations(environment const & env, expr const & e) {
}
void initialize_abbreviation() {
g_class_name = new name("abbreviations");
g_key = new std::string("abbrev");
g_class_name = new name("abbreviation");
g_key = new std::string("ABBREV");
abbrev_ext::initialize();
}

View file

@ -264,7 +264,7 @@ void open_aliases(lua_State * L) {
}
void initialize_aliases() {
g_aliases = new name("aliases");
g_aliases = new name("alias");
g_ext = new aliases_ext_reg();
}

View file

@ -148,8 +148,8 @@ list<gexpr> backward_rule_set::find(head_index const & h) const {
}
void initialize_backward_rule_set() {
g_class_name = new name("brs");
g_key = new std::string("brs");
g_class_name = new name("backward");
g_key = new std::string("BWD");
brs_ext::initialize();
register_prio_attribute("intro", "backward chaining",
[](environment const & env, io_state const &, name const & d, unsigned prio, name const & ns, bool persistent) {

View file

@ -114,7 +114,7 @@ void get_intro_lemmas(environment const & env, buffer<name> & r) {
void initialize_intro_elim_lemmas() {
g_class_name = new name("grinder");
g_key = new std::string("grinder");
g_key = new std::string("GRD");
intro_elim_ext::initialize();
register_prio_attribute("elim", "elimination rule that is eagerly applied by blast grinder",

View file

@ -579,8 +579,8 @@ io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets c
void initialize_simplifier_rule_set() {
g_prefix = new name(name::mk_internal_unique_name());
g_class_name = new name("simps");
g_key = new std::string("simp");
g_class_name = new name("simp");
g_key = new std::string("SIMP");
rrs_ext::initialize();
register_prio_attribute("simp", "simplification rule",
[](environment const & env, io_state const &, name const & d, unsigned prio, name const & ns, bool persistent) {

View file

@ -483,7 +483,7 @@ list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name c
void initialize_class() {
g_tmp_prefix = new name(name::mk_internal_unique_name());
g_source = new name("_source");
g_class_name = new name("classes");
g_class_name = new name("class");
g_key = new std::string("class");
class_ext::initialize();

View file

@ -373,8 +373,8 @@ environment add_coercion(environment const & env, io_state const &, name const &
void initialize_coercion() {
g_fun = new name("_Fun");
g_sort = new name("_Sort");
g_class_name = new name("coercions");
g_key = new std::string("coerce");
g_class_name = new name("coercion");
g_key = new std::string("COERCE");
coercion_ext::initialize();
register_attribute("coercion", "coercion",
[](environment const & env, io_state const & ios, name const & d, name const & ns, bool persistent) {

View file

@ -191,8 +191,8 @@ io_state_stream const & operator<<(io_state_stream const & out, light_rule_set c
}
void initialize_light_rule_set() {
g_class_name = new name("lrs");
g_key = new std::string("lrs");
g_class_name = new name("light");
g_key = new std::string("LIGHT");
lrs_ext::initialize();
register_param_attribute("light", "hint for simplifier",
[](environment const & env, io_state const &, name const & d, unsigned idx, name const & ns, bool persistent) {

View file

@ -163,8 +163,8 @@ environment erase_constructor_hint(environment const & env, name const & n, name
}
void initialize_normalize() {
g_unfold_hint_name = new name("unfold_hints");
g_key = new std::string("unfoldh");
g_unfold_hint_name = new name("unfold");
g_key = new std::string("UNFOLDH");
unfold_hint_ext::initialize();
register_params_attribute("unfold", "unfold definition when the given positions are constructors",
[](environment const & env, io_state const &, name const & d, list<unsigned> const & idxs, name const & ns, bool persistent) {

View file

@ -66,8 +66,8 @@ typedef scoped_ext<reducible_config> reducible_ext;
static name * g_tmp_prefix = nullptr;
void initialize_reducible() {
g_class_name = new name("reduce_hints");
g_key = new std::string("redu");
g_class_name = new name("reducible");
g_key = new std::string("REDU");
g_tmp_prefix = new name(name::mk_internal_unique_name());
reducible_ext::initialize();

View file

@ -327,8 +327,8 @@ is_relation_pred mk_is_relation_pred(environment const & env) {
}
void initialize_relation_manager() {
g_rel_name = new name("rel");
g_key = new std::string("rel");
g_rel_name = new name("relation");
g_key = new std::string("REL");
rel_ext::initialize();
register_attribute("refl", "reflexive relation",
[](environment const & env, io_state const &, name const & d, name const & ns, bool persistent) {

View file

@ -345,7 +345,7 @@ has_recursors_pred::has_recursors_pred(environment const & env):
void initialize_user_recursors() {
g_class_name = new name("recursor");
g_key = new std::string("urec");
g_key = new std::string("UREC");
recursor_ext::initialize();
register_opt_param_attribute("recursor", "user defined recursor",
[](environment const & env, io_state const &, name const & d, optional<unsigned> const & major, name const & ns, bool persistent) {

View file

@ -1,3 +1,3 @@
open "nat"
open [classes] "nat"
open [class] "nat"

View file

@ -1,2 +1,2 @@
bad_open.lean:1:5: error: invalid 'open/export' command, identifier expected
bad_open.lean:3:15: error: invalid 'open/export' command, identifier expected
bad_open.lean:3:13: error: invalid 'open/export' command, identifier expected

View file

@ -7,7 +7,7 @@ Finite bags.
-/
import data.nat data.list.perm algebra.binary
open nat quot list subtype binary function eq.ops algebra
open [declarations] perm
open [decl] perm
variable {A : Type}

View file

@ -11,7 +11,7 @@ section
end
section
open - [classes] nat
open - [class] nat
variable a : nat
check a + a
check add a a
@ -21,7 +21,7 @@ section
end
section
open - [classes] [decls] nat
open - [class] [decl] nat
variable a : nat
check a + a
check a + 1
@ -30,7 +30,7 @@ section
end
section
open [classes] nat
open [class] nat
definition foo3 : inhabited nat :=
_

View file

@ -7,9 +7,9 @@ namespace f2
end f2
namespace f3
export [declarations] f1
export - [declarations] f2
export [declaration] f1
export - [declaration] f2
end f3
export [declarations] f1
export - [declarations] f2
export [declaration] f1
export - [declaration] f2

View file

@ -1,5 +1,5 @@
import data.nat
open - [simps] nat
open - [simp] nat
definition Sum : nat → (nat → nat) → nat :=
sorry

View file

@ -31,7 +31,7 @@ section
end
section
open [notations] algebra
open [notation] algebra
open nat
-- check mul_struct nat << This is an error, we opened only the notation from algebra
variables a b c : nat

View file

@ -18,10 +18,10 @@ end int
section
-- Open "only" the notation and declarations from the namespaces nat and int
open [notations] nat
open [notations] int
open [decls] nat
open [decls] int
open [notation] nat
open [notation] int
open [decl] nat
open [decl] int
variables n m : nat
variables i j : int

View file

@ -20,17 +20,17 @@ constants n m : nat.nat
constants i j : int.int
section
open [notations] nat
open [notations] int
open [decls] nat
open [decls] int
open [notation] nat
open [notation] int
open [decl] nat
open [decl] int
check n+m
check i+j
-- check i+n -- Error
end
namespace int
open [decls] nat (nat)
open [decl] nat (nat)
-- Here is a possible trick for this kind of configuration
definition add_ni (a : nat) (b : int) := (of_nat a) + b
definition add_in (a : int) (b : nat) := a + (of_nat b)
@ -39,10 +39,10 @@ namespace int
end int
section
open [notations] nat
open [notations] int
open [declarations] nat
open [declarations] int
open [notation] nat
open [notation] int
open [declaration] nat
open [declaration] int
check n+m
check i+n
check n+i

View file

@ -17,10 +17,10 @@ attribute of_nat [coercion]
end int
-- Open "only" the notation and declarations from the namespaces nat and int
open [notations] nat
open [notations] int
open [decls] nat
open [decls] int
open [notation] nat
open [notation] int
open [decl] nat
open [decl] int
constants n m : nat
constants i j : int

View file

@ -1,6 +1,6 @@
import data.int
open [coercions] [classes] int
open [coercions] nat
open [coercion] [class] int
open [coercion] nat
definition lt1 (a b : int) := int.le (int.add a 1) b
infix `<` := lt1

View file

@ -41,13 +41,13 @@ section
end
section
open [notations] foo -- use only the notation
open [notation] foo -- use only the notation
check foo.a * foo.c
check a * c -- Error
end
section
open [decls] foo -- use only the declarations
open [decl] foo -- use only the declarations
check f a c
check a*c -- Error
end