fix: add "band-aid" for #341
closes #341 This is another instance of a compiler bug. It is in the code that is still written in C/C++. We need to infer types in the compiler, and we reused the kernel type checker for this. However, the compiler performs transformations that may produce type incorrect terms. This happens in code that makes heavy use of dependent types (like the new test). This is just a workaround for this particular instance of the problem. The definitive solution will only happen when we replace this part of the compiler with Lean code, and implement a custom `inferType` method for the compiler.
This commit is contained in:
Leonardo de Moura
parent
3eb91d4950
commit
1ea4bdb9cd
2 changed files with 173 additions and 43 deletions
|
|
@ -189,51 +189,57 @@ class eager_lambda_lifting_fn {
|
|||
}
|
||||
|
||||
expr lift_lambda(expr e, bool apply_simp) {
|
||||
lean_assert(is_lambda(e));
|
||||
buffer<expr> fvars;
|
||||
if (!collect_fvars(e, fvars)) {
|
||||
/* Hack: We use `try` here because previous compilation steps may have
|
||||
produced type incorrect terms. */
|
||||
try {
|
||||
lean_assert(is_lambda(e));
|
||||
buffer<expr> fvars;
|
||||
if (!collect_fvars(e, fvars)) {
|
||||
return e;
|
||||
}
|
||||
buffer<expr> params;
|
||||
while (is_lambda(e)) {
|
||||
expr param_type = instantiate_rev(binding_domain(e), params.size(), params.data());
|
||||
expr param = m_lctx.mk_local_decl(ngen(), binding_name(e), param_type, binding_info(e));
|
||||
params.push_back(param);
|
||||
e = binding_body(e);
|
||||
}
|
||||
e = instantiate_rev(e, params.size(), params.data());
|
||||
buffer<expr> new_params, to_copy;
|
||||
split_fvars(fvars, params, new_params, to_copy);
|
||||
/*
|
||||
Variables in `to_copy` only depend on global constants
|
||||
and other variables in `to_copy`. Moreover, `params` do not depend on them.
|
||||
It is wasteful to pass them as new parameters to the new lifted declaration.
|
||||
We can just copy them. The code duplication is not problematic because later at `extract_closed`
|
||||
we will create global names for closed terms, and eliminate the redundancy.
|
||||
*/
|
||||
e = m_lctx.mk_lambda(to_copy, e);
|
||||
e = m_lctx.mk_lambda(params, e);
|
||||
expr code = abstract(e, new_params.size(), new_params.data());
|
||||
unsigned i = new_params.size();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
local_decl const & decl = m_lctx.get_local_decl(new_params[i]);
|
||||
expr type = abstract(decl.get_type(), i, new_params.data());
|
||||
code = ::lean::mk_lambda(decl.get_user_name(), type, code);
|
||||
}
|
||||
if (apply_simp) {
|
||||
code = csimp(env(), code, m_cfg);
|
||||
}
|
||||
expr type = cheap_beta_reduce(type_checker(m_st).infer(code));
|
||||
name n = next_name();
|
||||
/* We add the auxiliary declaration `n` as a "meta" axiom to the environment.
|
||||
This is a hack to make sure we can use `csimp` to simplify `code` and
|
||||
other definitions that use `n`.
|
||||
We used a similar hack at `specialize.cpp`. */
|
||||
declaration aux_ax = mk_axiom(n, names(), type, true /* meta */);
|
||||
m_st.env() = env().add(aux_ax, false);
|
||||
m_new_decls.push_back(comp_decl(n, code));
|
||||
return mk_app(mk_constant(n), new_params);
|
||||
} catch (exception &) {
|
||||
return e;
|
||||
}
|
||||
buffer<expr> params;
|
||||
while (is_lambda(e)) {
|
||||
expr param_type = instantiate_rev(binding_domain(e), params.size(), params.data());
|
||||
expr param = m_lctx.mk_local_decl(ngen(), binding_name(e), param_type, binding_info(e));
|
||||
params.push_back(param);
|
||||
e = binding_body(e);
|
||||
}
|
||||
e = instantiate_rev(e, params.size(), params.data());
|
||||
buffer<expr> new_params, to_copy;
|
||||
split_fvars(fvars, params, new_params, to_copy);
|
||||
/*
|
||||
Variables in `to_copy` only depend on global constants
|
||||
and other variables in `to_copy`. Moreover, `params` do not depend on them.
|
||||
It is wasteful to pass them as new parameters to the new lifted declaration.
|
||||
We can just copy them. The code duplication is not problematic because later at `extract_closed`
|
||||
we will create global names for closed terms, and eliminate the redundancy.
|
||||
*/
|
||||
e = m_lctx.mk_lambda(to_copy, e);
|
||||
e = m_lctx.mk_lambda(params, e);
|
||||
expr code = abstract(e, new_params.size(), new_params.data());
|
||||
unsigned i = new_params.size();
|
||||
while (i > 0) {
|
||||
--i;
|
||||
local_decl const & decl = m_lctx.get_local_decl(new_params[i]);
|
||||
expr type = abstract(decl.get_type(), i, new_params.data());
|
||||
code = ::lean::mk_lambda(decl.get_user_name(), type, code);
|
||||
}
|
||||
if (apply_simp) {
|
||||
code = csimp(env(), code, m_cfg);
|
||||
}
|
||||
expr type = cheap_beta_reduce(type_checker(m_st).infer(code));
|
||||
name n = next_name();
|
||||
/* We add the auxiliary declaration `n` as a "meta" axiom to the environment.
|
||||
This is a hack to make sure we can use `csimp` to simplify `code` and
|
||||
other definitions that use `n`.
|
||||
We used a similar hack at `specialize.cpp`. */
|
||||
declaration aux_ax = mk_axiom(n, names(), type, true /* meta */);
|
||||
m_st.env() = env().add(aux_ax, false);
|
||||
m_new_decls.push_back(comp_decl(n, code));
|
||||
return mk_app(mk_constant(n), new_params);
|
||||
}
|
||||
|
||||
/* Given a free variable `x`, follow let-decls and return a pair `(x, v)`.
|
||||
|
|
|
|||
124
tests/lean/run/341.lean
Normal file
124
tests/lean/run/341.lean
Normal file
|
|
@ -0,0 +1,124 @@
|
|||
section
|
||||
variable (G : Type 1) (T : Type 1) (Tm : Type 1)
|
||||
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
|
||||
(getCtx : T → G) (getTy : Tm → T)
|
||||
inductive CtxSyntaxLayer where
|
||||
| emp : CtxSyntaxLayer
|
||||
| snoc : (Γ : G) → (t : T) → EG Γ (getCtx t) → CtxSyntaxLayer
|
||||
end
|
||||
section
|
||||
variable (G : Type 1) (T : Type 1) (Tm : Type 1)
|
||||
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
|
||||
(getCtx : T → G) (getTy : Tm → T)
|
||||
(GAlgebra : CtxSyntaxLayer G T EG getCtx → G)
|
||||
|
||||
inductive TySyntaxLayer where
|
||||
| top : {Γ : G} → TySyntaxLayer
|
||||
| bot : {Γ : G} → TySyntaxLayer
|
||||
| nat : {Γ : G} → TySyntaxLayer
|
||||
| arrow : {Γ : G} → (A B : T) → EG Γ (getCtx A) → EG Γ (getCtx B) → TySyntaxLayer
|
||||
|
||||
def getCtxStep : TySyntaxLayer G T EG getCtx → G
|
||||
| TySyntaxLayer.top (Γ := Γ) .. => Γ
|
||||
| TySyntaxLayer.bot (Γ := Γ) .. => Γ
|
||||
| TySyntaxLayer.nat (Γ := Γ) .. => Γ
|
||||
| TySyntaxLayer.arrow (Γ := Γ) .. => Γ
|
||||
end
|
||||
section
|
||||
variable (G : Type 1) (T : Type 1) (Tm : Type 1)
|
||||
(EG : G → G → Type) (ET : T → T → Type) (ETm : Tm → Tm → Type)
|
||||
(EGrfl : ∀ {Γ}, EG Γ Γ)
|
||||
(getCtx : T → G) (getTy : Tm → T)
|
||||
(GAlgebra : CtxSyntaxLayer G T EG getCtx → G) (TAlgebra : TySyntaxLayer G T EG getCtx → T)
|
||||
|
||||
inductive TmSyntaxLayer where
|
||||
| tt : {Γ : G} → TmSyntaxLayer
|
||||
| zero : {Γ : G} → TmSyntaxLayer
|
||||
| succ : {Γ : G} → TmSyntaxLayer
|
||||
| app : {Γ : G} → (A B : T) → (Actx : EG Γ (getCtx A)) → (Bctx : EG Γ (getCtx B))
|
||||
→ (f x : Tm)
|
||||
→ ET (getTy f) (TAlgebra (TySyntaxLayer.arrow A B Actx Bctx))
|
||||
→ ET (getTy x) A
|
||||
→ TmSyntaxLayer
|
||||
-- set options for debugging "(kernel) declaration has metavariables" errors
|
||||
--set_option trace.Elab.definition true
|
||||
--set_option pp.explicit true
|
||||
def getTyStep : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra → T
|
||||
| TmSyntaxLayer.tt (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.top (Γ:=Γ))
|
||||
| TmSyntaxLayer.zero (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.nat (Γ:=Γ))
|
||||
| TmSyntaxLayer.succ (Γ:=Γ) .. => TAlgebra (TySyntaxLayer.arrow (TAlgebra (TySyntaxLayer.nat (Γ:=Γ))) (TAlgebra (TySyntaxLayer.nat (Γ:=Γ))) EGrfl EGrfl)
|
||||
| TmSyntaxLayer.app (B:=B) .. => B
|
||||
end
|
||||
|
||||
structure SyntaxModel where
|
||||
Ctx : Type 1
|
||||
Ty : Type 1
|
||||
Tm : Type 1
|
||||
EC : Ctx → Ctx → Type
|
||||
ETy : Ty → Ty → Type
|
||||
ETm : Tm → Tm → Type
|
||||
getCtx : Ty → Ctx
|
||||
getTy : Tm → Ty
|
||||
interpCStep : CtxSyntaxLayer Ctx Ty EC getCtx → Ctx
|
||||
interpTyStep : TySyntaxLayer Ctx Ty EC getCtx → Ty
|
||||
interpTmStep : TmSyntaxLayer Ctx Ty Tm EC ETy getCtx getTy interpTyStep → Tm
|
||||
|
||||
namespace SetModel
|
||||
def Ctx := Type
|
||||
structure Ty where
|
||||
ctx : Ctx
|
||||
ty : ctx → Type
|
||||
structure Tm where
|
||||
ty : Ty
|
||||
tm : ∀ {Γ}, ty.ty Γ
|
||||
|
||||
def ECtx : Ctx → Ctx → Type := (PLift $ · = ·)
|
||||
def ETy : Ty → Ty → Type := (PLift $ · = ·)
|
||||
def ETm : Tm → Tm → Type := (PLift $ · = ·)
|
||||
|
||||
def interpCStep : CtxSyntaxLayer Ctx Ty ECtx Ty.ctx → Ctx
|
||||
| CtxSyntaxLayer.emp => Unit
|
||||
| CtxSyntaxLayer.snoc _ T (PLift.up rfl) => Σ γ : _, T.ty γ
|
||||
|
||||
def Ty.inj Γ T := Ty.mk Γ (λ _ => T)
|
||||
def Ty.Unit {Γ} := Ty.inj Γ _root_.Unit
|
||||
def Ty.Empty {Γ} := Ty.inj Γ _root_.Empty
|
||||
def Ty.Nat {Γ} := Ty.inj Γ _root_.Nat
|
||||
|
||||
def Tm.inj Γ {T} (t : T) := Tm.mk (Ty.inj Γ T) t
|
||||
|
||||
def interpTyStep : TySyntaxLayer Ctx Ty ECtx Ty.ctx → Ty
|
||||
| TySyntaxLayer.top (Γ:=Γ) => Ty.Unit (Γ:=Γ)
|
||||
| TySyntaxLayer.bot (Γ:=Γ) => Ty.Empty (Γ:=Γ)
|
||||
| TySyntaxLayer.nat (Γ:=Γ) => Ty.Nat (Γ:=Γ)
|
||||
| TySyntaxLayer.arrow (Γ:=Γ) A B (PLift.up Actx) (PLift.up Bctx) => Ty.mk Γ (λ γ => A.ty (cast Actx γ) → B.ty (cast Bctx γ))
|
||||
|
||||
def interpTmStep : TmSyntaxLayer Ctx Ty Tm ECtx ETy Ty.ctx Tm.ty interpTyStep → Tm
|
||||
| TmSyntaxLayer.tt (Γ:=Γ) => Tm.inj Γ Unit.unit
|
||||
| TmSyntaxLayer.zero (Γ:=Γ) => Tm.inj Γ (0 : Nat)
|
||||
| TmSyntaxLayer.succ (Γ:=Γ) => Tm.inj Γ Nat.succ
|
||||
| TmSyntaxLayer.app (Γ:=Γ) A B (PLift.up Actx) (PLift.up Bctx) (Tm.mk fty ftm) (Tm.mk (Ty.mk xctx xty) xtm) (PLift.up fTy) (PLift.up xTy)
|
||||
=> { ty := B
|
||||
, tm := fun {γ} =>
|
||||
(by
|
||||
simp at fTy xTy; subst fTy xTy; simp at Actx Bctx; subst Actx Bctx
|
||||
simp [interpTyStep, cast] at *
|
||||
exact (ftm xtm)
|
||||
)
|
||||
}
|
||||
|
||||
def Model : SyntaxModel :=
|
||||
{
|
||||
Ctx := Ctx
|
||||
, Ty := Ty
|
||||
, Tm := Tm
|
||||
, EC := ECtx
|
||||
, ETy := ETy
|
||||
, ETm := ETm
|
||||
, getCtx := Ty.ctx
|
||||
, getTy := Tm.ty
|
||||
, interpCStep := interpCStep
|
||||
, interpTyStep := interpTyStep
|
||||
, interpTmStep := interpTmStep
|
||||
}
|
||||
end SetModel
|
||||
Loading…
Add table
Reference in a new issue