Fixing bug in native compiler with let patterns in fixpoint definitions.

Typical example: Fixpoint f (m : nat) (o := true) (n : nat) {struct n} := n.
Was raising an "index out of bounds" exception at compile-time.
Nota: this construction is still incorrectly handled by the VM.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16197 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 41 insertions, 12 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 6b9247476..9fee03ca1 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -615,13 +615,27 @@ let merge_branches t =
       let lf,env_n = push_rels (empty_env ()) ids in
       let t_params = Array.make ndef [||] in
       let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
+      let mk_let envi (id,def) t = MLlet (id,def,t) in
+      let mk_lam_or_let (params,lets,env) (id,def) =
+        let ln,env' = push_rel env id in
+        match def with
+        | None -> (ln::params,lets,env')
+        | Some lam -> (params, (ln,ml_of_lam env l lam)::lets,env')
+      in
       let ml_of_fix i body =
-	let idsi,bodyi = decompose_Llam body in
-	let paramsi, envi = push_rels env_n idsi in
-	t_norm_f.(i) <- fresh_gnorm l;
-	let bodyi = ml_of_lam envi l bodyi in
-	t_params.(i) <- paramsi;
-	mkMLlam paramsi bodyi in
+        let varsi, bodyi = decompose_Llam_Llet body in
+        let paramsi,letsi,envi = 
+          Array.fold_left mk_lam_or_let ([],[],env_n) varsi
+        in
+        let paramsi,letsi =
+          Array.of_list (List.rev paramsi), Array.of_list (List.rev letsi)
+        in
+        t_norm_f.(i) <- fresh_gnorm l;
+        let bodyi = ml_of_lam envi l bodyi in
+        t_params.(i) <- paramsi;
+        let bodyi = Array.fold_right (mk_let envi) letsi bodyi in
+        mkMLlam paramsi bodyi
+      in
       let tnorm = Array.mapi ml_of_fix tb in
       let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in
       let fv_params = fv_params env_n in
@@ -667,12 +681,12 @@ let merge_branches t =
       let t_params = Array.make ndef [||] in
       let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
       let ml_of_fix i body =
-	let idsi,bodyi = decompose_Llam body in
-	let paramsi, envi = push_rels env_n idsi in
-	t_norm_f.(i) <- fresh_gnorm l;
-	let bodyi = ml_of_lam envi l bodyi in
-	t_params.(i) <- paramsi;
-	mkMLlam paramsi bodyi in
+        let idsi,bodyi = decompose_Llam body in
+        let paramsi, envi = push_rels env_n idsi in
+        t_norm_f.(i) <- fresh_gnorm l;
+        let bodyi = ml_of_lam envi l bodyi in
+        t_params.(i) <- paramsi;
+        mkMLlam paramsi bodyi in
       let tnorm = Array.mapi ml_of_fix tb in
       let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in
       let fv_params = fv_params env_n in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 2ca274799..f530f6e2e 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -66,6 +66,20 @@ let decompose_Llam lam =
   | Llam(ids,body) -> ids, body
   | _ -> [||], lam
 
+let rec decompose_Llam_Llet lam =
+  match lam with
+  | Llam(ids,body) ->
+      let vars, body = decompose_Llam_Llet body in
+      Array.fold_right (fun x l -> (x, None) :: l) ids vars, body
+  | Llet(id,def,body) ->
+      let vars, body = decompose_Llam_Llet body in
+      (id,Some def) :: vars, body
+  | _ -> [], lam
+
+let decompose_Llam_Llet lam =
+  let vars, body = decompose_Llam_Llet lam in
+  Array.of_list vars, body
+
 (*s Operators on substitution *)
 let subst_id = subs_id 0
 let lift = subs_lift 
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 0c454256e..ada63ebb4 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -46,6 +46,7 @@ and lam_branches = (constructor * name array * lambda) array
 and fix_decl =  name array * lambda array * lambda array
 
 val decompose_Llam : lambda -> Names.name array * lambda
+val decompose_Llam_Llet : lambda -> (Names.name * lambda option) array * lambda
 
 val is_lazy : constr -> bool
 val mk_lazy : lambda -> lambda