max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/type_context): should not have an implicit constructor, copy constructor, or assignment operator

Browse source
This commit is contained in:
Sebastian Ullrich 2018-01-31 14:53:28 +01:00 • committed by Leonardo de Moura
parent dc5e50e7f0
commit 6ab13a433d
6 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/elaborator.cpp
View file

@ -2826,7 +2826,7 @@ void elaborator::assign_field_mvar(name const & S_fname, expr const & mvar,
class unfold_projections_visitor : public replace_visitor {
private:
type_context m_ctx;
type_context & m_ctx;
protected:
expr visit_app(expr const & e) override {
expr e2 = replace_visitor::visit_app(e);
@ -2837,7 +2837,7 @@ protected:
return e2;
}
public:
unfold_projections_visitor(const type_context & ctx): m_ctx(ctx) {}
unfold_projections_visitor(type_context & ctx): m_ctx(ctx) {}
};
/* Predicated variant of `lean::instantiate_mvars`. It does not support delayed abstractions or universe mvars. */
@ -3071,7 +3071,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
// Example: `functor.map (functor.mk ?p1 ?m1 ?m2...) => ?m1`
auto reduce_and_check_deps = [&](expr & e) {
if (use_subobjects)
e = unfold_projections_visitor(m_env)(e);
e = unfold_projections_visitor(m_ctx)(e);
expr t = e;
name_set deps;
expr pretty = replace(t, [&](expr const & e) {

2
src/library/tactic/apply_tactic.cpp
View file

@ -203,8 +203,8 @@ static optional<tactic_state> apply(type_context & ctx, expr e, apply_cfg const
if ((cfg.m_unify && !ctx.unify(e_type, target)) ||
(!cfg.m_unify && !ctx.match(e_type, target))) {
if (out_error_obj) {
auto pp_ctx = ::lean::mk_pp_ctx(ctx.env(), s.get_options(), ctx.mctx(), ctx.lctx());
auto thunk = [=]() {
auto pp_ctx = ::lean::mk_pp_ctx(ctx.env(), s.get_options(), ctx.mctx(), ctx.lctx());
format msg = format("invalid apply tactic, failed to ");
if (cfg.m_unify)
msg += format("unify");

2
src/library/tactic/simplify.h
View file

@ -76,7 +76,7 @@ class simplify_core_fn {
protected:
typedef expr_struct_map<simp_result> simplify_cache;
type_context m_ctx;
type_context & m_ctx;
defeq_canonizer m_defeq_canonizer;
name m_rel;
simp_lemmas m_slss;

3
src/library/type_context.cpp
View file

@ -356,7 +356,8 @@ type_context::type_context(type_context_cache_ptr const & ptr, metavar_context c
}
type_context::~type_context() {
if (m_cache_manager)
// note: m_cache may have been moved out
if (m_cache_manager && m_cache)
m_cache_manager->recycle(m_cache);
}

6
src/library/type_context.h
View file

@ -700,12 +700,16 @@ public:
type_context(environment const & env, options const & o, local_context const & lctx,
transparency_mode m = transparency_mode::Reducible):
type_context(env, o, metavar_context(), lctx, m) {}
type_context(environment const & env, transparency_mode m = transparency_mode::Reducible):
explicit type_context(environment const & env, transparency_mode m = transparency_mode::Reducible):
type_context(env, options(), metavar_context(), local_context(), m) {}
type_context(environment const & env, options const & o, transparency_mode m = transparency_mode::Reducible):
type_context(env, o, metavar_context(), local_context(), m) {}
type_context(environment const & env, options const & o, metavar_context const & mctx, local_context const & lctx,
type_context_cache_manager & manager, transparency_mode m = transparency_mode::Reducible);
type_context(type_context const &) = delete;
type_context(type_context &&) = default;
type_context & operator=(type_context const &) = delete;
type_context & operator=(type_context &&) = default;
virtual ~type_context();
virtual environment const & env() const override { return m_cache->m_env; }

5
tests/lean/structure_instance_bug3.lean.expected.out
View file

@ -3,8 +3,3 @@ structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field
structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field 'bind' was not provided
structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field 'pure_bind' was not provided
structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field 'bind_assoc' was not provided
structure_instance_bug3.lean:1:23: error: unexpected field 'map_pure'
given field value
λ (α β : Type ?) (g : α → β) (x : α), eq.trans (eq.symm (?m_1 g (⁇ α x))) (⁇ α β x (⁇ β ∘ g))
expected field value
?m_1