From 00a05aea070121103baba2c03485127369f24538 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 23 Nov 2014 11:44:31 +0100 Subject: Fix #3824. de Bruijn error in normalization of fixpoints. This bug was affecting the VM and the native compiler, but only in the pretyper (not the kernel). Types of arguments of fixpoints were incorrectly normalized due to a missing lift. --- pretyping/nativenorm.ml | 9 +++++++-- pretyping/vnorm.ml | 6 +++++- 2 files changed, 12 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 024af30ae..274357adb 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -312,12 +312,17 @@ and nf_atom_type env atom = let ci = ans.asw_ci in mkCase(ci, p, a, branchs), tcase | Afix(tt,ft,rp,s) -> - let tt = Array.map (nf_type env) tt in + let tt = Array.map (fun t -> nf_type env t) tt in let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in let lvl = nb_rel env in + let nbfix = Array.length ft in let fargs = mk_rels_accu lvl (Array.length ft) in + (* Third argument of the tuple is ignored by push_rec_types *) let env = push_rec_types (name,tt,[||]) env in - let ft = Array.mapi (fun i v -> nf_val env (napply v fargs) tt.(i)) ft in + (* We lift here because the types of arguments (in tt) will be evaluated + in an environment where the fixpoints have been pushed *) + let norm_body i v = nf_val env (napply v fargs) (lift nbfix tt.(i)) in + let ft = Array.mapi norm_body ft in mkFix((rp,s),(name,tt,ft)), tt.(s) | Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) -> let tt = Array.map (nf_type env) tt in diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index be4ad7dbb..c3a1f0d94 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -275,8 +275,12 @@ and nf_fix env f = let ndef = Array.length vt in let ft = Array.map (fun v -> nf_val env v crazy_type) vt in let name = Array.init ndef (fun _ -> (Name (Id.of_string "Ffix"))) in + (* Third argument of the tuple is ignored by push_rec_types *) let env = push_rec_types (name,ft,ft) env in - let fb = Util.Array.map2 (fun v t -> nf_fun env v t) vb ft in + (* We lift here because the types of arguments (in tt) will be evaluated + in an environment where the fixpoints have been pushed *) + let norm_vb v t = nf_fun env v (lift ndef t) in + let fb = Util.Array.map2 norm_vb vb ft in mkFix ((rec_args,init),(name,ft,fb)) and nf_fix_app env f vargs = -- cgit v1.2.3