diff options
| -rw-r--r-- | kernel/cinstr.mli | 6 | ||||
| -rw-r--r-- | kernel/clambda.ml | 1 | ||||
| -rw-r--r-- | kernel/nativeinstr.mli | 6 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 1 | ||||
| -rw-r--r-- | kernel/reduction.ml | 20 | ||||
| -rw-r--r-- | kernel/reduction.mli | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
7 files changed, 36 insertions, 3 deletions
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 4a3c03d85..f42c46175 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -31,7 +31,7 @@ and lambda = | Lprim of pconstant * int (* arity *) * instruction * lambda array | Lcase of case_info * reloc_table * lambda * lambda * lam_branches | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of int * lambda array | Lval of structured_constant | Lsort of Sorts.t @@ -39,6 +39,10 @@ and lambda = | Lproj of int * Constant.t * lambda | Luint of uint +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = { constant_branches : lambda array; nonconstant_branches : (Name.t array * lambda) array } diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 619dd608f..8389dd326 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -700,6 +700,7 @@ let rec lambda_of_constr env c = Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> + let rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in let ltypes = lambda_of_args env 0 type_bodies in Renv.push_rels env names; let lbodies = lambda_of_args env 0 rec_bodies in diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 9c17cc2b5..c319be32d 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -37,7 +37,7 @@ and lambda = (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl + | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) (* A fully applied constructor *) @@ -50,6 +50,10 @@ and lambda = | Llazy | Lforce +(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation +to be correct. Otherwise, memoization of previous evaluations will be applied +again to extra arguments (see #7333). *) + and lam_branches = (constructor * Name.t array * lambda) array and fix_decl = Name.t array * lambda array * lambda array diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index a49bf62b3..8b61ed0c5 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -570,6 +570,7 @@ let rec lambda_of_constr env sigma c = Lfix(rec_init, (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> + let rec_bodies = Array.map2 (Reduction.eta_expand !global_env) rec_bodies type_bodies in let ltypes = lambda_of_args env sigma 0 type_bodies in Renv.push_rels env names; let lbodies = lambda_of_args env sigma 0 rec_bodies in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 6cd3917c7..8ca596d48 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -862,6 +862,17 @@ let dest_prod env = in decrec env Context.Rel.empty +let dest_lam env = + let rec decrec env m c = + let t = whd_all env c in + match kind t with + | Lambda (n,a,c0) -> + let d = LocalAssum (n,a) in + decrec (push_rel d env) (Context.Rel.add d m) c0 + | _ -> m,t + in + decrec env Context.Rel.empty + (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = @@ -907,3 +918,12 @@ let is_arity env c = let _ = dest_arity env c in true with NotArity -> false + +let eta_expand env t ty = + let ctxt, codom = dest_prod env ty in + let ctxt',t = dest_lam env t in + let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in + let eta_args = List.rev_map mkRel (List.interval 1 d) in + let t = Term.applistc (Vars.lift d t) eta_args in + let t = Term.it_mkLambda_or_LetIn t (List.firstn d ctxt) in + Term.it_mkLambda_or_LetIn t ctxt' diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 2e10f98c5..e53ab6aef 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -118,9 +118,12 @@ val betazeta_appvect : int -> constr -> constr array -> constr val dest_prod : env -> types -> Context.Rel.t * types val dest_prod_assum : env -> types -> Context.Rel.t * types +val dest_lam : env -> types -> Context.Rel.t * constr val dest_lam_assum : env -> types -> Context.Rel.t * types exception NotArity val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *) val is_arity : env -> types -> bool + +val eta_expand : env -> constr -> types -> constr diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e07833204..12c82e20d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -955,7 +955,7 @@ let set_strategy e k l = { e with env = open Retroknowledge -(* the Environ.register function syncrhonizes the proactive and reactive +(* the Environ.register function synchronizes the proactive and reactive retroknowledge. *) let dispatch = |