Merge PR #9476: Constructor type information uses the expanded form.

Reviewed-by: SkySkimmer
Reviewed-by: gares

3 files changed, 42 insertions, 36 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index b12018cd66..3c1115d056 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -138,7 +138,7 @@ let get_sym_eq_data env (ind,u) =
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
   if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported.";
-  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let constrsign,ccl = mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments"; (* This can be relaxed... *)
@@ -173,7 +173,7 @@ let get_non_sym_eq_data env (ind,u) =
   let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
   if List.exists is_local_def realsign then
     error "Inductive equalities with local definitions in arity not supported";
-  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let constrsign,ccl = mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
@@ -776,7 +776,7 @@ let build_congr env (eq,refl,ctx) ind =
     error "Inductive equalities with local definitions in arity not supported.";
   let env_with_arity = push_rel_context arityctxt env in
   let ty = RelDecl.get_type (lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity) in
-  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
+  let constrsign,ccl = mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
   if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 708412720a..395b4928ce 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -106,22 +106,24 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
         && (Int.equal mip.mind_nrealargs 0)
       then
 	if is_strict_conjunction style (* strict conjunction *) then
-	  let ctx =
-	    (prod_assum sigma (snd
-	      (decompose_prod_n_assum sigma mib.mind_nparams (EConstr.of_constr mip.mind_nf_lc.(0))))) in
+          let (ctx, _) = mip.mind_nf_lc.(0) in
+          let ctx = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
 	  if
+            (* Constructor has a type of the form
+              c : forall (a_0 ... a_n : Type) (x_0 : A_0) ... (x_n : A_n). T **)
 	    List.for_all
 	      (fun decl -> let c = RelDecl.get_type decl in
 	                   is_local_assum decl &&
-			   isRel sigma c &&
-                           Int.equal (destRel sigma c) mib.mind_nparams) ctx
+                           Constr.isRel c &&
+                           Int.equal (Constr.destRel c) mib.mind_nparams) ctx
 	  then
 	    Some (hdapp,args)
 	  else None
 	else
+          let ctx, cty = mip.mind_nf_lc.(0) in
+          let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
           let ctyp = whd_beta_prod sigma
-            (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt)
-                       (EConstr.of_constr mip.mind_nf_lc.(0)) args) in
+            (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in
 	  let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
 	  if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
 	    (* Record or non strict conjunction *)
@@ -165,12 +167,13 @@ let is_tuple sigma t =
    it is strict if it has the form
    "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
 
-let test_strict_disjunction n lc =
-  let open Term in
-  Array.for_all_i (fun i c ->
-    match (prod_assum (snd (decompose_prod_n_assum n c))) with
-    | [LocalAssum (_,c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i)
-    | _ -> false) 0 lc
+let test_strict_disjunction (mib, mip) =
+  let n = List.length mib.mind_params_ctxt in
+  let check i (ctx, _) = match List.skipn n (List.rev ctx) with
+  | [LocalAssum (_, c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i)
+  | _ -> false
+  in
+  Array.for_all_i check 0 mip.mind_nf_lc
 
 let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
   let (hdapp,args) = decompose_app sigma t in
@@ -183,14 +186,16 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
         && (Int.equal mip.mind_nrealargs 0)
       then
 	if strict then
-	  if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
+          if test_strict_disjunction (mib, mip) then
 	    Some (hdapp,args)
 	  else
 	    None
 	else
-	  let cargs =
-	    Array.map (fun ar -> pi2 (destProd sigma (prod_applist sigma (EConstr.of_constr ar) args)))
-	      mip.mind_nf_lc in
+          let map (ctx, cty) =
+            let ar = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+            pi2 (destProd sigma (prod_applist sigma ar args))
+          in
+          let cargs = Array.map map mip.mind_nf_lc in
 	  Some (hdapp,Array.to_list cargs)
       else
 	None
@@ -225,10 +230,8 @@ let match_with_unit_or_eq_type sigma t =
   match EConstr.kind sigma hdapp with
     | Ind (ind , _) ->
         let (mib,mip) = Global.lookup_inductive ind in
-        let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
-        let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
-	if Int.equal nconstr 1 && zero_args constr_types.(0) then
+        if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then
 	  Some hdapp
 	else
 	  None
@@ -308,11 +311,13 @@ let match_with_equation env sigma t =
         let constr_types = mip.mind_nf_lc in
         let nconstr = Array.length mip.mind_consnames in
 	if Int.equal nconstr 1 then
-          if is_matching env sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then
+          let (ctx, cty) = constr_types.(0) in
+          let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+          if is_matching env sigma coq_refl_leibniz1_pattern cty then
 	    None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
-	  else if is_matching env sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then
+          else if is_matching env sigma coq_refl_leibniz2_pattern cty then
 	    None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-	  else if is_matching env sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then
+          else if is_matching env sigma coq_refl_jm_pattern cty then
 	    None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
 	  else raise NoEquationFound
         else raise NoEquationFound
@@ -378,8 +383,9 @@ let match_with_nodep_ind sigma t =
   | Ind (ind, _)  ->
      let (mib,mip) = Global.lookup_inductive ind in
      if Array.length (mib.mind_packets)>1 then None else
-       let nodep_constr c =
-         has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma (EConstr.of_constr c) in
+       let nodep_constr (ctx, cty) =
+        let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+         has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in
        if Array.for_all nodep_constr mip.mind_nf_lc then
          let params=
            if Int.equal mip.mind_nrealargs 0 then args else
@@ -400,7 +406,7 @@ let match_with_sigma_type sigma t =
         && (Int.equal mip.mind_nrealargs 0)
         && (Int.equal (Array.length mip.mind_consnames)1)
         && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma
-             (EConstr.of_constr mip.mind_nf_lc.(0))
+             (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx))
      then
        (*allowing only 1 existential*)
        Some (hdapp,args)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bfbce8f6eb..ec8d4d0e14 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -20,6 +20,7 @@ open Tacmach
 open Clenv
 open Tactypes
 
+module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 (************************************************************************)
@@ -223,8 +224,8 @@ let compute_induction_names = compute_induction_names_gen true
 (* Compute the let-in signature of case analysis or standard induction scheme *)
 let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
   let rec analrec c recargs =
-    match Constr.kind c, recargs with
-    | Prod (_,_,c), recarg::rest ->
+    match c, recargs with
+    | RelDecl.LocalAssum _ :: c, recarg::rest ->
         let rest = analrec c rest in
         begin match Declareops.dest_recarg recarg with
         | Norec | Imbr _  -> true :: rest
@@ -232,14 +233,13 @@ let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
             if rec_flag && Int.equal j k then true :: true :: rest
             else true :: rest
         end
-    | LetIn (_,_,_,c), rest -> false :: analrec c rest
-    | _, [] -> []
+    | RelDecl.LocalDef _ :: c, rest -> false :: analrec c rest
+    | [], [] -> []
     | _ -> anomaly (Pp.str "compute_constructor_signatures.")
   in
   let (mib,mip) = Global.lookup_inductive ity in
-  let n = mib.mind_nparams in
-  let lc =
-    Array.map (fun c -> snd (Term.decompose_prod_n_assum n c)) mip.mind_nf_lc in
+  let map (ctx, _) = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
+  let lc = Array.map map mip.mind_nf_lc in
   let lrecargs = Declareops.dest_subterms mip.mind_recargs in
   Array.map2 analrec lc lrecargs