From d92679f9692fff459f3e4e2af940e9de1f2f67e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 20 May 2018 09:42:44 -0700 Subject: [PATCH] refactor(*): replace `name` with `lean.name` --- library/init/meta/attribute.lean | 4 +- library/init/meta/contradiction_tactic.lean | 2 +- library/init/meta/injection_tactic.lean | 2 +- library/init/meta/interactive.lean | 2 +- library/init/meta/name.lean | 90 ++++----------------- src/frontends/lean/util.cpp | 6 +- src/library/constants.cpp | 24 +++--- src/library/constants.h | 6 +- src/library/constants.txt | 6 +- src/library/equations_compiler/util.cpp | 6 +- src/library/module.cpp | 6 -- src/library/util.cpp | 4 +- src/library/vm/vm_name.cpp | 14 ++-- tests/lean/run/check_constants.lean | 6 +- 14 files changed, 57 insertions(+), 121 deletions(-) diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean index 0ef1b3bbb9..32d9b2fedc 100644 --- a/library/init/meta/attribute.lean +++ b/library/init/meta/attribute.lean @@ -26,9 +26,9 @@ meta structure user_attribute (cache_ty : Type := unit) (param_ty : Type := unit not be applied after all. Declaring an `after_set` handler without a `before_unset` handler will make the attribute non-removable. -/ -(after_set : option (Π (decl : _root_.name) (prio : nat) (persistent : bool), command) := none) +(after_set : option (Π (decl : lean.name) (prio : nat) (persistent : bool), command) := none) /- Optional handler that will be called before the attribute is removed from a declaration. -/ -(before_unset : option (Π (decl : _root_.name) (persistent : bool), command) := none) +(before_unset : option (Π (decl : lean.name) (persistent : bool), command) := none) (cache_cfg : user_attribute_cache_cfg cache_ty . user_attribute.dflt_cache_cfg) [reflect_param : has_reflect param_ty] /- Parser that will be invoked after parsing the attribute's name. The parse result will be reflected diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean index d032995e41..b3cd140f0a 100644 --- a/library/init/meta/contradiction_tactic.lean +++ b/library/init/meta/contradiction_tactic.lean @@ -63,7 +63,7 @@ private meta def contra_constructor_eq : list expr → tactic unit is_constructor_app env rhs ∧ const_name (get_app_fn lhs) ≠ const_name (get_app_fn rhs) then do tgt ← target, - I_name ← return $ name.get_prefix (const_name (get_app_fn lhs)), + I_name ← return $ lean.name.get_prefix (const_name (get_app_fn lhs)), pr ← mk_app (I_name <.> "no_confusion") [tgt, lhs, rhs, H], exact pr else contra_constructor_eq Hs diff --git a/library/init/meta/injection_tactic.lean b/library/init/meta/injection_tactic.lean index da6f279d08..4fa9010029 100644 --- a/library/init/meta/injection_tactic.lean +++ b/library/init/meta/injection_tactic.lean @@ -57,7 +57,7 @@ do else fail "injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor" else do tgt ← target, - let I_name := name.get_prefix n_fl, + let I_name := lean.name.get_prefix n_fl, pr ← mk_app (I_name <.> "no_confusion") [tgt, lhs, rhs, h], exact pr, return ([], ns) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 11b3bf4504..4e800c185a 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -578,7 +578,7 @@ private meta def is_case_simple_tag : tag → bool | _ := ff private meta def is_case_tag : tag → option nat -| (name.mk_numeral `_case n :: _) := some n.to_nat +| (name.mk_numeral `_case n :: _) := some n | _ := none private meta def tag_match (t : tag) (pre : list name) : bool := diff --git a/library/init/meta/name.lean b/library/init/meta/name.lean index 3ec3ae08cf..a6e9591cf5 100644 --- a/library/init/meta/name.lean +++ b/library/init/meta/name.lean @@ -6,11 +6,7 @@ Authors: Leonardo de Moura prelude import init.data.ordering.basic init.coe init.data.to_string init.lean.name -/-- Reflect a C++ name object. The VM replaces it with the C++ implementation. -/ -inductive name -| anonymous : name -| mk_string : name → string → name -| mk_numeral : name → uint32 → name +export lean (name name.anonymous name.mk_string name.mk_numeral mk_str_name mk_num_name mk_simple_name) /-- Gadget for automatic parameter support. This is similar to the opt_param gadget, but it uses the tactic declaration names tac_name to synthesize the argument. @@ -22,67 +18,13 @@ inductive name @[simp] lemma {u} auto_param_eq (α : Sort u) (n : name) : auto_param α n = α := rfl -instance : inhabited name := -⟨name.anonymous⟩ - -def mk_str_name (n : name) (s : string) : name := -name.mk_string n s - -def mk_num_name (n : name) (v : nat) : name := -name.mk_numeral n (uint32.of_nat v) - -def mk_simple_name (s : string) : name := -mk_str_name name.anonymous s - -instance string_to_name : has_coe string name := -⟨mk_simple_name⟩ - infix ` <.> `:65 := mk_str_name -open name - -def name.get_prefix : name → name -| anonymous := anonymous -| (mk_string p _) := p -| (mk_numeral p _) := p - -def name.update_prefix : name → name → name -| anonymous new_p := anonymous -| (mk_string p s) new_p := mk_string new_p s -| (mk_numeral p v) new_p := mk_numeral new_p v - -/- The (decidable_eq string) has not been defined yet. - So, we disable the use of if-then-else when compiling the following definitions. -/ -set_option eqn_compiler.ite false - -def name.to_string_with_sep (sep : string) : name → string -| anonymous := "[anonymous]" -| (mk_string anonymous s) := s -| (mk_numeral anonymous v) := repr v -| (mk_string n s) := name.to_string_with_sep n ++ sep ++ s -| (mk_numeral n v) := name.to_string_with_sep n ++ sep ++ repr v - -private def name.components' : name -> list name -| anonymous := [] -| (mk_string n s) := mk_string anonymous s :: name.components' n -| (mk_numeral n v) := mk_numeral anonymous v :: name.components' n - -def name.components (n : name) : list name := -(name.components' n).reverse - -protected def name.to_string : name → string := -name.to_string_with_sep "." - -instance : has_to_string name := -⟨name.to_string⟩ - -/- TODO(Leo): provide a definition in Lean. -/ -meta constant name.has_decidable_eq : decidable_eq name /- Both cmp and lex_cmp are total orders, but lex_cmp implements a lexicographical order. -/ meta constant name.cmp : name → name → ordering meta constant name.lex_cmp : name → name → ordering meta constant name.append : name → name → name -meta constant name.is_internal : name → bool +meta constant lean.name.is_internal : name → bool protected meta def name.lt (a b : name) : Prop := name.cmp a b = ordering.lt @@ -93,28 +35,28 @@ meta instance : decidable_rel name.lt := meta instance : has_lt name := ⟨name.lt⟩ -attribute [instance] name.has_decidable_eq - meta instance : has_append name := ⟨name.append⟩ /-- `name.append_after n i` return a name of the form n_i -/ -meta constant name.append_after : name → nat → name +meta constant lean.name.append_after : name → nat → name -meta def name.is_prefix_of : name → name → bool +meta def lean.name.is_prefix_of : name → name → bool | p name.anonymous := ff | p n := - if p = n then tt else name.is_prefix_of p n.get_prefix + if p = n then tt else lean.name.is_prefix_of p n.get_prefix -meta def name.replace_prefix : name → name → name → name +open lean.name + +meta def lean.name.replace_prefix : name → name → name → name | anonymous p p' := anonymous -| (mk_string c s) p p' := if c = p then mk_string p' s else mk_string (name.replace_prefix c p p') s -| (mk_numeral c v) p p' := if c = p then mk_numeral p' v else mk_numeral (name.replace_prefix c p p') v +| (mk_string c s) p p' := if c = p then mk_string p' s else mk_string (lean.name.replace_prefix c p p') s +| (mk_numeral c v) p p' := if c = p then mk_numeral p' v else mk_numeral (lean.name.replace_prefix c p p') v -meta def name.to_lean_name : name → lean.name -| name.anonymous := lean.name.anonymous -| (name.mk_string n s) := n.to_lean_name.mk_string s -| (name.mk_numeral n u) := n.to_lean_name.mk_numeral u.to_nat +def lean.name.components' : name -> list name +| anonymous := [] +| (mk_string n s) := mk_string anonymous s :: lean.name.components' n +| (mk_numeral n v) := mk_numeral anonymous v :: lean.name.components' n -meta instance : has_coe name lean.name := -⟨name.to_lean_name⟩ +def lean.name.components (n : name) : list name := +n.components'.reverse diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 95ebda0436..a086cd7529 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -358,11 +358,11 @@ expr quote(char const * str) { expr quote(name const & n) { switch (n.kind()) { case name_kind::ANONYMOUS: - return mk_constant(get_name_anonymous_name()); + return mk_constant(get_lean_name_anonymous_name()); case name_kind::NUMERAL: - return mk_app(mk_constant(get_name_mk_numeral_name()), quote(n.get_prefix()), quote(n.get_numeral())); + return mk_app(mk_constant(get_lean_name_mk_numeral_name()), quote(n.get_prefix()), quote(n.get_numeral())); case name_kind::STRING: - return mk_app(mk_constant(get_name_mk_string_name()), quote(n.get_prefix()), quote(n.get_string())); + return mk_app(mk_constant(get_lean_name_mk_string_name()), quote(n.get_prefix()), quote(n.get_string())); } lean_unreachable(); } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 33f723f535..361dcb09dd 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -137,9 +137,9 @@ name const * g_list_cons = nullptr; name const * g_match_failed = nullptr; name const * g_monad = nullptr; name const * g_monad_fail = nullptr; -name const * g_name_anonymous = nullptr; -name const * g_name_mk_numeral = nullptr; -name const * g_name_mk_string = nullptr; +name const * g_lean_name_anonymous = nullptr; +name const * g_lean_name_mk_numeral = nullptr; +name const * g_lean_name_mk_string = nullptr; name const * g_nat = nullptr; name const * g_nat_succ = nullptr; name const * g_nat_zero = nullptr; @@ -382,9 +382,9 @@ void initialize_constants() { g_match_failed = new name{"match_failed"}; g_monad = new name{"monad"}; g_monad_fail = new name{"monad_fail"}; - g_name_anonymous = new name{"name", "anonymous"}; - g_name_mk_numeral = new name{"name", "mk_numeral"}; - g_name_mk_string = new name{"name", "mk_string"}; + g_lean_name_anonymous = new name{"lean", "name", "anonymous"}; + g_lean_name_mk_numeral = new name{"lean", "name", "mk_numeral"}; + g_lean_name_mk_string = new name{"lean", "name", "mk_string"}; g_nat = new name{"nat"}; g_nat_succ = new name{"nat", "succ"}; g_nat_zero = new name{"nat", "zero"}; @@ -628,9 +628,9 @@ void finalize_constants() { delete g_match_failed; delete g_monad; delete g_monad_fail; - delete g_name_anonymous; - delete g_name_mk_numeral; - delete g_name_mk_string; + delete g_lean_name_anonymous; + delete g_lean_name_mk_numeral; + delete g_lean_name_mk_string; delete g_nat; delete g_nat_succ; delete g_nat_zero; @@ -873,9 +873,9 @@ name const & get_list_cons_name() { return *g_list_cons; } name const & get_match_failed_name() { return *g_match_failed; } name const & get_monad_name() { return *g_monad; } name const & get_monad_fail_name() { return *g_monad_fail; } -name const & get_name_anonymous_name() { return *g_name_anonymous; } -name const & get_name_mk_numeral_name() { return *g_name_mk_numeral; } -name const & get_name_mk_string_name() { return *g_name_mk_string; } +name const & get_lean_name_anonymous_name() { return *g_lean_name_anonymous; } +name const & get_lean_name_mk_numeral_name() { return *g_lean_name_mk_numeral; } +name const & get_lean_name_mk_string_name() { return *g_lean_name_mk_string; } name const & get_nat_name() { return *g_nat; } name const & get_nat_succ_name() { return *g_nat_succ; } name const & get_nat_zero_name() { return *g_nat_zero; } diff --git a/src/library/constants.h b/src/library/constants.h index 6976ab90cf..d5cbf0477f 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -139,9 +139,9 @@ name const & get_list_cons_name(); name const & get_match_failed_name(); name const & get_monad_name(); name const & get_monad_fail_name(); -name const & get_name_anonymous_name(); -name const & get_name_mk_numeral_name(); -name const & get_name_mk_string_name(); +name const & get_lean_name_anonymous_name(); +name const & get_lean_name_mk_numeral_name(); +name const & get_lean_name_mk_string_name(); name const & get_nat_name(); name const & get_nat_succ_name(); name const & get_nat_zero_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index ea015271cc..d0970a471c 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -132,9 +132,9 @@ list.cons match_failed monad monad_fail -name.anonymous -name.mk_numeral -name.mk_string +lean.name.anonymous +lean.name.mk_numeral +lean.name.mk_string nat nat.succ nat.zero diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 27ffbc4b6b..81dd04e756 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -842,13 +842,13 @@ environment mk_simple_equation_lemma_for(environment const & env, options const } bool is_name_value(expr const & e) { - if (is_constant(e, get_name_anonymous_name())) + if (is_constant(e, get_lean_name_anonymous_name())) return true; buffer args; expr const & fn = get_app_args(e, args); - if (is_constant(fn, get_name_mk_string_name()) && args.size() == 2) + if (is_constant(fn, get_lean_name_mk_string_name()) && args.size() == 2) return is_name_value(args[0]) && is_string_value(args[1]); - if (is_constant(fn, get_name_mk_numeral_name()) && args.size() == 2) + if (is_constant(fn, get_lean_name_mk_numeral_name()) && args.size() == 2) return is_name_value(args[0]) && is_num(args[1]); return false; } diff --git a/src/library/module.cpp b/src/library/module.cpp index e3dfce7082..b8caf97042 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -439,12 +439,6 @@ environment update_module_defs(environment const & env, declaration const & d) { } } -static name sorry_decl_name(name const & n) { - if (n.is_string() && n.get_string()[0] == '_') - return sorry_decl_name(n.get_prefix()); - return n; -} - struct sorry_warning_tag : public log_entry_cell {}; environment add(environment const & env, certified_declaration const & d) { diff --git a/src/library/util.cpp b/src/library/util.cpp index bbb0d4d89b..45334742a0 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -1095,9 +1095,9 @@ optional is_aux_meta_rec_name(name const & n) { } optional name_lit_to_name(expr const & name_lit) { - if (is_constant(name_lit, get_name_anonymous_name())) + if (is_constant(name_lit, get_lean_name_anonymous_name())) return optional(name()); - if (is_app_of(name_lit, get_name_mk_string_name(), 2)) { + if (is_app_of(name_lit, get_lean_name_mk_string_name(), 2)) { if (auto p = name_lit_to_name(app_arg(app_fn(name_lit)))) if (auto str = to_string(app_arg(name_lit))) return optional(name(*p, str->c_str())); diff --git a/src/library/vm/vm_name.cpp b/src/library/vm/vm_name.cpp index 478f0add98..dfec32c667 100644 --- a/src/library/vm/vm_name.cpp +++ b/src/library/vm/vm_name.cpp @@ -89,16 +89,16 @@ vm_obj name_is_internal(vm_obj const & n) { } void initialize_vm_name() { - DECLARE_VM_BUILTIN(name({"name", "anonymous"}), name_anonymous); - DECLARE_VM_BUILTIN(name({"name", "mk_string"}), name_mk_string); - DECLARE_VM_BUILTIN(name({"name", "mk_numeral"}), name_mk_numeral); - DECLARE_VM_BUILTIN(name({"name", "has_decidable_eq"}), name_has_decidable_eq); + DECLARE_VM_BUILTIN(name({"lean", "name", "anonymous"}), name_anonymous); + DECLARE_VM_BUILTIN(name({"lean", "name", "mk_string"}), name_mk_string); + DECLARE_VM_BUILTIN(name({"lean", "name", "mk_numeral"}), name_mk_numeral); + DECLARE_VM_BUILTIN(name({"lean", "name", "has_decidable_eq"}), name_has_decidable_eq); DECLARE_VM_BUILTIN(name({"name", "cmp"}), name_cmp); DECLARE_VM_BUILTIN(name({"name", "lex_cmp"}), name_lex_cmp); - DECLARE_VM_BUILTIN(name({"name", "append_after"}), name_append_after); DECLARE_VM_BUILTIN(name({"name", "append"}), name_append); - DECLARE_VM_BUILTIN(name({"name", "is_internal"}), name_is_internal); - DECLARE_VM_CASES_BUILTIN(name({"name", "cases_on"}), name_cases_on); + DECLARE_VM_BUILTIN(name({"lean", "name", "is_internal"}), name_is_internal); + DECLARE_VM_BUILTIN(name({"lean", "name", "append_after"}), name_append_after); + DECLARE_VM_CASES_BUILTIN(name({"lean", "name", "cases_on"}), name_cases_on); } void finalize_vm_name() { diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index d127b3f417..5d3a5ad91c 100644 --- a/tests/lean/run/check_constants.lean +++ b/tests/lean/run/check_constants.lean @@ -137,9 +137,9 @@ run_cmd script_check_id `list.cons run_cmd script_check_id `match_failed run_cmd script_check_id `monad run_cmd script_check_id `monad_fail -run_cmd script_check_id `name.anonymous -run_cmd script_check_id `name.mk_numeral -run_cmd script_check_id `name.mk_string +run_cmd script_check_id `lean.name.anonymous +run_cmd script_check_id `lean.name.mk_numeral +run_cmd script_check_id `lean.name.mk_string run_cmd script_check_id `nat run_cmd script_check_id `nat.succ run_cmd script_check_id `nat.zero