Merge PR #7077: Preserving canonical structure of return predicate in vm_compute and native_compute (partial fix to #7068; also fixes #7076))

2 files changed, 30 insertions, 18 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 978ceed1e..3fce2f3c6 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -303,10 +303,10 @@ and nf_atom_type env sigma atom =
       let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
       let nparams = mib.mind_nparams in
       let params,realargs = Array.chop nparams allargs in
+      let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
       let pT = 
-	hnf_prod_applist env 
+        hnf_prod_applist_assum env nparamdecls
 	  (Inductiveops.type_of_inductive env ind) (Array.to_list params) in
-      let pT = whd_all env pT in
       let dep, p = nf_predicate env sigma ind mip params p pT in
       (* Calcul du type des branches *)
       let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in
@@ -362,20 +362,24 @@ and nf_atom_type env sigma atom =
 
 
 and  nf_predicate env sigma ind mip params v pT =
-  match kind_of_value v, kind pT with
-  | Vfun f, Prod _ ->
+  match kind (whd_allnolet env pT) with
+  | LetIn (name,b,t,pT) ->
+      let dep,body =
+        nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
+      dep, mkLetIn (name,b,t,body)
+  | Prod (name,dom,codom) -> begin
+    match kind_of_value v with
+    | Vfun f ->
       let k = nb_rel env in
       let vb = f (mk_rel_accu k) in
-      let name,dom,codom =
-	try decompose_prod env pT with
-	  DestKO ->
-	  CErrors.anomaly
-	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
-      in
       let dep,body = 
 	nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
       dep, mkLambda(name,dom,body)
-  | Vfun f, _ -> 
+    | _ -> false, nf_type env sigma v
+    end
+  | _ ->
+    match kind_of_value v with
+    | Vfun f ->
       let k = nb_rel env in
       let vb = f (mk_rel_accu k) in
       let name = Name (Id.of_string "c") in
@@ -385,7 +389,7 @@ and  nf_predicate env sigma ind mip params v pT =
       let dom = mkApp(mkIndU ind,Array.append params rargs) in
       let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in
       true, mkLambda(name,dom,body)
-  | _, _ -> false, nf_type env sigma v
+    | _ -> false, nf_type env sigma v
 
 and nf_evar env sigma evk ty args =
   let evi = try Evd.find sigma evk with Not_found -> assert false in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index a1ba4a6a9..14c9f49b1 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -266,7 +266,6 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
       let pT =
         hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
-      let pT = whd_all env pT in
       let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
       (* Calcul du type des branches *)
       let btypes = build_branches_type env sigma ind mib mip u params dep p in
@@ -288,15 +287,24 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
      nf_stk env sigma (mkProj(p',c)) ty stk
 
 and nf_predicate env sigma ind mip params v pT =
-  match whd_val v, kind pT with
-  | Vfun f, Prod _ ->
+  match kind (whd_allnolet env pT) with
+  | LetIn (name,b,t,pT) ->
+      let dep,body =
+        nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
+      dep, mkLetIn (name,b,t,body)
+  | Prod (name,dom,codom) -> begin
+    match whd_val v with
+    | Vfun f ->
       let k = nb_rel env in
       let vb = reduce_fun k f in
-      let name,dom,codom = decompose_prod env pT in
       let dep,body =
 	nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
       dep, mkLambda(name,dom,body)
-  | Vfun f, _ ->
+    | _ -> assert false
+    end
+  | _ ->
+    match whd_val v with
+    | Vfun f ->
       let k = nb_rel env in
       let vb = reduce_fun k f in
       let name = Name (Id.of_string "c") in
@@ -306,7 +314,7 @@ and nf_predicate env sigma ind mip params v pT =
       let dom = mkApp(mkIndU ind,Array.append params rargs) in
       let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in
       true, mkLambda(name,dom,body)
-  | _, _ -> false, nf_val env sigma v crazy_type
+    | _ -> false, nf_val env sigma v crazy_type
 
 and nf_args env sigma vargs ?from:(f=0) t =
   let t = ref t in