From 47994fe14ec7982d5b727c4f8a4f29ae9abce95c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Nov 2017 16:27:45 -0800 Subject: [PATCH] chore(library): remove id_locked --- library/init/meta/simp_tactic.lean | 2 +- library/init/meta/tactic.lean | 30 ++++--------------- src/library/app_builder.cpp | 8 +++-- src/library/app_builder.h | 6 ++-- src/library/constants.cpp | 12 +++----- src/library/constants.h | 3 +- src/library/constants.txt | 3 +- src/library/tactic/change_tactic.cpp | 4 +-- src/library/tactic/smt/congruence_closure.cpp | 2 +- src/library/tactic/smt/smt_state.cpp | 2 +- tests/lean/anc1.lean.expected.out | 2 +- tests/lean/run/check_constants.lean | 3 +- 12 files changed, 28 insertions(+), 49 deletions(-) diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index bf3749b518..4a396ce54b 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -468,7 +468,7 @@ private meta def loop (cfg : simp_config) (discharger : tactic unit) (to_unfold to_expr ``(@false.rec %%tgt %%new_fact_pr) >>= exact else do h0_type ← infer_type h, - let new_fact_pr := mk_id_locked_proof new_h_type new_fact_pr, + let new_fact_pr := mk_id_proof new_h_type new_fact_pr, new_es ← update_simp_lemmas es new_fact_pr, new_r ← update_simp_lemmas r new_fact_pr, let new_r := {new_type := new_h_type, pr := new_pr, ..e} :: new_r, diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 7705eadfc9..3f9069e4be 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -1146,26 +1146,6 @@ meta def any_of {α β} : list α → (α → tactic β) → tactic β end end list -/- - Define id_locked using meta-programming because we don't have - syntax for setting reducibility_hints. - - See module init.meta.declaration. - - Remark: id_locked is used in the builtin implementation of tactic.change --/ -run_cmd do - let l := level.param `l, - let Ty : pexpr := expr.sort l, - type ← to_expr ``(Π {α : %%Ty}, α → α), - val ← to_expr ``(λ {α : %%Ty} (a : α), a), - add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt) - -lemma id_locked_eq {α : Type u} (a : α) : id_locked a = a := -rfl - -attribute [inline] id_locked - /- Define id_rhs using meta-programming because we don't have syntax for setting reducibility_hints. @@ -1201,18 +1181,18 @@ meta instance : monad task := bind_pure_comp_eq_map := undefined} namespace tactic -meta def mk_id_locked_proof (prop : expr) (pr : expr) : expr := -expr.app (expr.app (expr.const ``id_locked [level.zero]) prop) pr +meta def mk_id_proof (prop : expr) (pr : expr) : expr := +expr.app (expr.app (expr.const ``id [level.zero]) prop) pr -meta def mk_id_locked_eq (lhs : expr) (rhs : expr) (pr : expr) : tactic expr := +meta def mk_id_eq (lhs : expr) (rhs : expr) (pr : expr) : tactic expr := do prop ← mk_app `eq [lhs, rhs], - return $ mk_id_locked_proof prop pr + return $ mk_id_proof prop pr meta def replace_target (new_target : expr) (pr : expr) : tactic unit := do t ← target, assert `htarget new_target, swap, ht ← get_local `htarget, - locked_pr ← mk_id_locked_eq t new_target pr, + locked_pr ← mk_id_eq t new_target pr, mk_eq_mpr locked_pr ht >>= exact end tactic diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 7983ec9eda..829fa6ba2b 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -1125,9 +1125,13 @@ expr mk_ite(type_context & ctx, expr const & c, expr const & t, expr const & e) return mk_app(ctx, get_ite_name(), 5, mask, args); } -expr mk_id_locked(type_context & ctx, expr const & type, expr const & h) { +expr mk_id(type_context & ctx, expr const & type, expr const & h) { level lvl = get_level(ctx, type); - return mk_app(mk_constant(get_id_locked_name(), {lvl}), type, h); + return mk_app(mk_constant(get_id_name(), {lvl}), type, h); +} + +expr mk_id(type_context & ctx, expr const & h) { + return mk_id(ctx, ctx.infer(h), h); } expr mk_id_rhs(type_context & ctx, expr const & h) { diff --git a/src/library/app_builder.h b/src/library/app_builder.h index 92d9831dd5..25ee6529b3 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -180,8 +180,10 @@ expr mk_false_rec(type_context & ctx, expr const & c, expr const & H); /* (if c then t else e) */ expr mk_ite(type_context & ctx, expr const & c, expr const & t, expr const & e); -/* (id_locked type h) */ -expr mk_id_locked(type_context & ctx, expr const & type, expr const & h); +/* (@id type h) */ +expr mk_id(type_context & ctx, expr const & type, expr const & h); +/* (id h) */ +expr mk_id(type_context & ctx, expr const & h); /* (id_rhs h) */ expr mk_id_rhs(type_context & ctx, expr const & h); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 1a8268b004..9d12b0af87 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -49,7 +49,6 @@ name const * g_decidable = nullptr; name const * g_decidable_to_bool = nullptr; name const * g_distrib = nullptr; name const * g_dite = nullptr; -name const * g_id = nullptr; name const * g_empty = nullptr; name const * g_Exists = nullptr; name const * g_eq = nullptr; @@ -127,7 +126,7 @@ name const * g_heq_symm = nullptr; name const * g_heq_trans = nullptr; name const * g_heq_of_eq = nullptr; name const * g_hole_command = nullptr; -name const * g_id_locked = nullptr; +name const * g_id = nullptr; name const * g_id_rhs = nullptr; name const * g_id_delta = nullptr; name const * g_if_neg = nullptr; @@ -431,7 +430,6 @@ void initialize_constants() { g_decidable_to_bool = new name{"decidable", "to_bool"}; g_distrib = new name{"distrib"}; g_dite = new name{"dite"}; - g_id = new name{"id"}; g_empty = new name{"empty"}; g_Exists = new name{"Exists"}; g_eq = new name{"eq"}; @@ -509,7 +507,7 @@ void initialize_constants() { g_heq_trans = new name{"heq", "trans"}; g_heq_of_eq = new name{"heq_of_eq"}; g_hole_command = new name{"hole_command"}; - g_id_locked = new name{"id_locked"}; + g_id = new name{"id"}; g_id_rhs = new name{"id_rhs"}; g_id_delta = new name{"id_delta"}; g_if_neg = new name{"if_neg"}; @@ -814,7 +812,6 @@ void finalize_constants() { delete g_decidable_to_bool; delete g_distrib; delete g_dite; - delete g_id; delete g_empty; delete g_Exists; delete g_eq; @@ -892,7 +889,7 @@ void finalize_constants() { delete g_heq_trans; delete g_heq_of_eq; delete g_hole_command; - delete g_id_locked; + delete g_id; delete g_id_rhs; delete g_id_delta; delete g_if_neg; @@ -1196,7 +1193,6 @@ name const & get_decidable_name() { return *g_decidable; } name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; } name const & get_distrib_name() { return *g_distrib; } name const & get_dite_name() { return *g_dite; } -name const & get_id_name() { return *g_id; } name const & get_empty_name() { return *g_empty; } name const & get_Exists_name() { return *g_Exists; } name const & get_eq_name() { return *g_eq; } @@ -1274,7 +1270,7 @@ name const & get_heq_symm_name() { return *g_heq_symm; } name const & get_heq_trans_name() { return *g_heq_trans; } name const & get_heq_of_eq_name() { return *g_heq_of_eq; } name const & get_hole_command_name() { return *g_hole_command; } -name const & get_id_locked_name() { return *g_id_locked; } +name const & get_id_name() { return *g_id; } name const & get_id_rhs_name() { return *g_id_rhs; } name const & get_id_delta_name() { return *g_id_delta; } name const & get_if_neg_name() { return *g_if_neg; } diff --git a/src/library/constants.h b/src/library/constants.h index 77a117ec79..0a72436a07 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -51,7 +51,6 @@ name const & get_decidable_name(); name const & get_decidable_to_bool_name(); name const & get_distrib_name(); name const & get_dite_name(); -name const & get_id_name(); name const & get_empty_name(); name const & get_Exists_name(); name const & get_eq_name(); @@ -129,7 +128,7 @@ name const & get_heq_symm_name(); name const & get_heq_trans_name(); name const & get_heq_of_eq_name(); name const & get_hole_command_name(); -name const & get_id_locked_name(); +name const & get_id_name(); name const & get_id_rhs_name(); name const & get_id_delta_name(); name const & get_if_neg_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 90e7505fad..a663c49778 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -44,7 +44,6 @@ decidable decidable.to_bool distrib dite -id empty Exists eq @@ -122,7 +121,7 @@ heq.symm heq.trans heq_of_eq hole_command -id_locked +id id_rhs id_delta if_neg diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp index 8822234bd5..31aebe2d5a 100644 --- a/src/library/tactic/change_tactic.cpp +++ b/src/library/tactic/change_tactic.cpp @@ -24,11 +24,11 @@ vm_obj change_core(expr const & e, bool check, tactic_state const & s) { /* We use the proof term - (@id_locked (g->get_type()) new_M) + (@id (g->get_type()) new_M) to create a "checkpoint". See discussion at issue #1260 */ - expr pr = mk_id_locked(ctx, g->get_type(), new_M); + expr pr = mk_id(ctx, g->get_type(), new_M); mctx.assign(head(s.goals()), pr); list new_gs(new_M, tail(s.goals())); return tactic::mk_success(set_mctx_goals(s, mctx, new_gs)); diff --git a/src/library/tactic/smt/congruence_closure.cpp b/src/library/tactic/smt/congruence_closure.cpp index 26bf765942..5ac11e389f 100644 --- a/src/library/tactic/smt/congruence_closure.cpp +++ b/src/library/tactic/smt/congruence_closure.cpp @@ -1149,7 +1149,7 @@ expr congruence_closure::mk_proof(expr const & lhs, expr const & rhs, expr const } else if (H == *g_refl_mark) { expr type = heq_proofs ? mk_heq(m_ctx, lhs, rhs) : mk_eq(m_ctx, lhs, rhs); expr proof = heq_proofs ? mk_heq_refl(m_ctx, lhs) : mk_eq_refl(m_ctx, lhs); - return mk_app(mk_constant(get_id_locked_name(), {mk_level_zero()}), type, proof); + return mk_app(mk_constant(get_id_name(), {mk_level_zero()}), type, proof); } else if (is_cc_theory_proof(H)) { return expand_delayed_cc_proofs(*this, get_cc_theory_proof_arg(H)); } else { diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index 9dccf8d592..91c878dde7 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -260,7 +260,7 @@ static expr_pair preprocess_forward(type_context & ctx, defeq_can_state & dcs, s } else if (r.get_new() == type) { return mk_pair(type, h); } else { - return mk_pair(r.get_new(), mk_id_locked(ctx, r.get_new(), h)); + return mk_pair(r.get_new(), mk_id(ctx, r.get_new(), h)); } } diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out index 1cde88afcc..ae60f01479 100644 --- a/tests/lean/anc1.lean.expected.out +++ b/tests/lean/anc1.lean.expected.out @@ -3,7 +3,7 @@ anc1.lean:5:0: warning: declaration '[anonymous]' uses sorry ⟨1, _⟩ : Σ' (x : ℕ), x > 0 show true, from true.intro : true -Exists.intro 1 (id_locked (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0 +Exists.intro 1 (id (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from ⟨Hb, Ha⟩ : ∀ (A B C : Prop), A → B → C → B ∧ A λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A ∧ C ∧ A, from ⟨Hb, ⟨Ha, ⟨Hc, Ha⟩⟩⟩ : diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index fa8ce105fd..a04d4b3347 100644 --- a/tests/lean/run/check_constants.lean +++ b/tests/lean/run/check_constants.lean @@ -49,7 +49,6 @@ run_cmd script_check_id `decidable run_cmd script_check_id `decidable.to_bool run_cmd script_check_id `distrib run_cmd script_check_id `dite -run_cmd script_check_id `id run_cmd script_check_id `empty run_cmd script_check_id `Exists run_cmd script_check_id `eq @@ -127,7 +126,7 @@ run_cmd script_check_id `heq.symm run_cmd script_check_id `heq.trans run_cmd script_check_id `heq_of_eq run_cmd script_check_id `hole_command -run_cmd script_check_id `id_locked +run_cmd script_check_id `id run_cmd script_check_id `id_rhs run_cmd script_check_id `id_delta run_cmd script_check_id `if_neg