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

fix: fixes #280

Browse source 
We are going to use a cleaner fix when we port this code to Lean.
This commit is contained in:
Leonardo de Moura 2021-01-19 17:57:21 -08:00
parent 8c6a510e65
commit e57a9fa78f
2 changed files with 66 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

92
src/library/compiler/llnf.cpp
View file

@ -565,51 +565,57 @@ class to_lambda_pure_fn {
for (unsigned i = 0; i < cnames.size(); i++) {
unsigned saved_fvars_size = m_fvars.size();
expr minor = args[i+1];
cnstr_info cinfo = get_cnstr_info(cnames[i]);
buffer<expr> fields;
for (field_info const & info : cinfo.m_field_info) {
lean_assert(is_lambda(minor));
switch (info.m_kind) {
case field_info::Irrelevant:
fields.push_back(mk_enf_neutral());
break;
case field_info::Object:
fields.push_back(mk_let_decl(mk_enf_object_type(), mk_app(mk_llnf_proj(info.m_idx), major)));
break;
case field_info::USize:
fields.push_back(mk_let_decl(info.get_type(), mk_uproj(major, info.m_idx)));
break;
case field_info::Scalar:
if (info.is_float()) {
fields.push_back(mk_let_decl(info.get_type(), mk_fproj(major, info.m_idx, info.m_offset)));
} else {
fields.push_back(mk_let_decl(info.get_type(), mk_sproj(major, info.m_size, info.m_idx, info.m_offset)));
}
break;
}
minor = binding_body(minor);
}
minor = instantiate_rev(minor, fields.size(), fields.data());
if (!is_let(minor))
minor = ensure_terminal(minor);
minor = visit(minor);
if (!is_enf_unreachable(minor)) {
/* If `minor` is not the constructor `i`, then this "g_cases_on" application is not the identity. */
unsigned cidx, nusizes, ssz;
if (!(is_llnf_cnstr(minor, cidx, nusizes, ssz) && cidx == i && nusizes == 0 && ssz == 0)) {
is_id = false;
}
minor = mk_let(saved_fvars_size, minor);
#if 0 // See comment below
if (num_reachable > 0 && minor != some_reachable) {
all_eq = false;
}
#endif
some_reachable = minor;
args[i+1] = minor;
if (minor == mk_enf_neutral()) {
// This can happen when a branch returns a proposition
num_reachable++;
some_reachable = minor;
} else {
args[i+1] = minor;
cnstr_info cinfo = get_cnstr_info(cnames[i]);
buffer<expr> fields;
for (field_info const & info : cinfo.m_field_info) {
lean_assert(is_lambda(minor));
switch (info.m_kind) {
case field_info::Irrelevant:
fields.push_back(mk_enf_neutral());
break;
case field_info::Object:
fields.push_back(mk_let_decl(mk_enf_object_type(), mk_app(mk_llnf_proj(info.m_idx), major)));
break;
case field_info::USize:
fields.push_back(mk_let_decl(info.get_type(), mk_uproj(major, info.m_idx)));
break;
case field_info::Scalar:
if (info.is_float()) {
fields.push_back(mk_let_decl(info.get_type(), mk_fproj(major, info.m_idx, info.m_offset)));
} else {
fields.push_back(mk_let_decl(info.get_type(), mk_sproj(major, info.m_size, info.m_idx, info.m_offset)));
}
break;
}
minor = binding_body(minor);
}
minor = instantiate_rev(minor, fields.size(), fields.data());
if (!is_let(minor))
minor = ensure_terminal(minor);
minor = visit(minor);
if (!is_enf_unreachable(minor)) {
/* If `minor` is not the constructor `i`, then this "g_cases_on" application is not the identity. */
unsigned cidx, nusizes, ssz;
if (!(is_llnf_cnstr(minor, cidx, nusizes, ssz) && cidx == i && nusizes == 0 && ssz == 0)) {
is_id = false;
}
minor = mk_let(saved_fvars_size, minor);
#if 0 // See comment below
if (num_reachable > 0 && minor != some_reachable) {
all_eq = false;
}
#endif
some_reachable = minor;
args[i+1] = minor;
num_reachable++;
} else {
args[i+1] = minor;
}
}
}
if (num_reachable == 0) {

17
tests/lean/run/280.lean Normal file
View file

@ -0,0 +1,17 @@
inductive S where
| P
| I
open S
inductive Expr : S → Type where
| lit : Int → Expr I
| eq : Expr I → Expr I → Expr P
def Val : S → Type
| P => Prop
| I => Int
def eval : {s : S} → Expr s → Val s
| _, (Expr.lit n) => n
| _, (Expr.eq e₁ e₂) => eval e₁ = eval e₂