diff options
| -rw-r--r-- | kernel/nativevalues.ml | 3 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 9 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 6 |
3 files changed, 14 insertions, 4 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 51bf4c2738..56dac4ecdf 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -54,7 +54,8 @@ type atom = | Asort of sorts | Avar of identifier | Acase of annot_sw * accumulator * t * (t -> t) - | Afix of t array * t array * rec_pos * int + | Afix of t array * t array * rec_pos * int + (* types, bodies, rec_pos, pos *) | Acofix of t array * t array * int * t | Acofixe of t array * t array * int * t | Aprod of name * t * (t -> t) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 024af30ae8..274357adbc 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 be4ad7dbb3..c3a1f0d94b 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 = |