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

feat(frontends/lean/elaborator): new encoding for structure updates {s with ...}

Browse source 
See discussion at #1438
https://github.com/leanprover/lean/pull/1438#discussion_r105007325

@digama0 With this commit, the original `array_list.write` will also
perform a destructive update when the reference counter for `l` is 1.

```lean def write {α} (l : array_list α) : fin l^.length → α → array_list α :=
λ ⟨n, h⟩ v, { l with data := l^.data^.write ⟨n, l^.lt_capacity h⟩ h v }
```
This commit is contained in:
Leonardo de Moura 2017-03-09 00:11:51 -08:00
parent 77f8479457
commit c58f61e925
2 changed files with 19 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/algebra/group.lean
View file

@ -210,6 +210,8 @@ meta def multiplicative_to_additive_pairs : list (name × name) :=
[/- map operations -/
(`mul, `add), (`one, `zero), (`inv, `neg),
(`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg),
/- map constructors -/
(`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk),
/- map structures -/
(`semigroup, `add_semigroup),
(`monoid, `add_monoid),

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

@ -2463,7 +2463,8 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
S_name << "' is not the name of a structure type");
lean_assert(fnames.size() == fvalues.size());
name src_S_name;
unsigned src_S_nparams = 0;
bool src_S_name_is_class = false;
unsigned src_S_nparams = 0;
if (src) {
src = visit(*src, none_expr());
synthesize_type_class_instances();
@ -2477,8 +2478,9 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
line() + format("which has type") +
pp_indent(pp_fn, type));
}
src_S_name = const_name(src_S);
src_S_nparams = *inductive::get_num_params(m_env, src_S_name);
src_S_name = const_name(src_S);
src_S_nparams = *inductive::get_num_params(m_env, src_S_name);
src_S_name_is_class = is_class(env(), src_S_name);
}
if (S_name.is_anonymous()) {
if (expected_type) {
@ -2513,6 +2515,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
expr c_type = infer_type(c);
buffer<expr> c_args;
buffer<std::tuple<name, expr, expr>> to_elaborate;
type_context::tmp_locals let_decls(m_ctx);
/* First check for explicit, implicit, parent, auto_param fields.
We create metavariables for parameters.
For auto_param fields, we create metavariable and use the specifed tactic to synthesize the field.
@ -2569,6 +2572,16 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
msg += std::get<2>(pp_data);
throw elaborator_exception(ref, msg);
}
if (!m_ctx.is_prop(c_arg_type) && !src_S_name_is_class) {
/* The condition (!src_S_name_is_class) is a temporary workaround
to address unification failures in the algebraic hierarchy.
We need to investigate why the extra let-expressions are affecting the unifier.
The condition (!m_ctx.is_prop(c_arg_type)) is an optimization.
To solve the issue described at #1438, we don't need to create
let-declarations for proofs since they will be erased. */
c_arg = let_decls.push_let(name("_src").append_after(let_decls.size()+1), c_arg_type, c_arg);
}
field2value.insert(S_fname, c_arg);
} else {
name full_S_fname = S_name + S_fname;
@ -2663,8 +2676,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
}
last_progress = progress;
}
return mk_app(c, c_args);
return let_decls.mk_lambda(mk_app(c, c_args));
}
static expr quote(expr const & e) {