Merge PR #1082: Fixing Print for inductive types with let-in in parameters

8 files changed, 44 insertions, 13 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 159d2ea66..da7042713 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -882,6 +882,18 @@ let hnf_prod_app env t n =
 let hnf_prod_applist env t nl =
   List.fold_left (hnf_prod_app env) t nl
 
+let hnf_prod_applist_assum env n c l =
+  let rec app n subst t l =
+    if Int.equal n 0 then
+      if l == [] then substl subst t
+      else anomaly (Pp.str "Too many arguments.")
+    else match kind (whd_allnolet env t), l with
+    | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+    | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+    | _, [] -> anomaly (Pp.str "Not enough arguments.")
+    | _ -> anomaly (Pp.str "Not enough prod/let's.") in
+  app n [] c l
+
 (* Dealing with arities *)
 
 let dest_prod env =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 0e6a2b819..6f7e3f8f8 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -105,6 +105,12 @@ val beta_app : constr -> constr -> constr
 (** Pseudo-reduction rule  Prod(x,A,B) a --> B[x\a] *)
 val hnf_prod_applist : env -> types -> constr list -> types
 
+(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to
+    the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it
+    returns [t] with the assumptions of [Γ] instantiated by [args] and
+    the local definitions of [Γ] expanded. *)
+val hnf_prod_applist_assum : env -> int -> types -> constr list -> types
+
 (** Compatibility alias for Term.lambda_appvect_assum *)
 val betazeta_appvect : int -> constr -> constr array -> constr
 
diff --git a/kernel/term.ml b/kernel/term.ml
index fae990d45..a4c92bd33 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -352,10 +352,11 @@ let lambda_applist_assum n c l =
   let rec app n subst t l =
     if Int.equal n 0 then
       if l == [] then substl subst t
-      else anomaly (Pp.str "Not enough arguments.")
+      else anomaly (Pp.str "Too many arguments.")
     else match kind_of_term t, l with
     | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
     | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+    | _, [] -> anomaly (Pp.str "Not enough arguments.")
     | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
   app n [] c l
 
@@ -377,10 +378,11 @@ let prod_applist_assum n c l =
   let rec app n subst t l =
     if Int.equal n 0 then
       if l == [] then substl subst t
-      else anomaly (Pp.str "Not enough arguments.")
+      else anomaly (Pp.str "Too many arguments.")
     else match kind_of_term t, l with
     | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
     | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+    | _, [] -> anomaly (Pp.str "Not enough arguments.")
     | _ -> anomaly (Pp.str "Not enough prod/let's.") in
   app n [] c l
 
diff --git a/kernel/term.mli b/kernel/term.mli
index c9a8cf6e1..b4597676a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -242,7 +242,7 @@ val lambda_applist : constr -> constr list -> constr
 val lambda_appvect : constr -> constr array -> constr
 
 (** In [lambda_applist_assum n c args], [c] is supposed to have the
-    form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it
+    form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it
     returns [c] with the assumptions of [Γ] instantiated by [args] and
     the local definitions of [Γ] expanded. *)
 val lambda_applist_assum : int -> constr -> constr list -> constr
@@ -251,15 +251,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr
 (** pseudo-reduction rule *)
 
 (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *)
-val prod_appvect : constr -> constr array -> constr
-val prod_applist : constr -> constr list -> constr
+val prod_appvect : types -> constr array -> types
+val prod_applist : types -> constr list -> types
 
 (** In [prod_appvect_assum n c args], [c] is supposed to have the
-    form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it
+    form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it
     returns [c] with the assumptions of [Γ] instantiated by [args] and
     the local definitions of [Γ] expanded. *)
-val prod_appvect_assum : int -> constr -> constr array -> constr
-val prod_applist_assum : int -> constr -> constr list -> constr
+val prod_appvect_assum : int -> types -> constr array -> types
+val prod_applist_assum : int -> types -> constr list -> types
 
 (** {5 Other term destructors. } *)
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b21fbf0eb..c93b41786 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -240,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk  =
       let (mib,mip) = Inductive.lookup_mind_specif env ind in
       let nparams = mib.mind_nparams in
       let params,realargs = Util.Array.chop nparams allargs in
+      let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
       let pT =
-	hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
+        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 *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 35487e09c..2cdb9be3f 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -93,10 +93,11 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
+  let nparamdecls = Context.Rel.length params in
   let args = Context.Rel.to_extended_list mkRel 0 params in
-  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
-  let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
+  let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in
   let envpar = push_rel_context params env in
   let inst =
     if Declareops.inductive_is_polymorphic mib then
@@ -173,10 +174,11 @@ let print_record env mind mib udecl =
   in
   let mip = mib.mind_packets.(0) in
   let params = Inductive.inductive_paramdecls (mib,u) in
+  let nparamdecls = Context.Rel.length params in
   let args = Context.Rel.to_extended_list mkRel 0 params in
-  let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
-  let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
+  let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
   let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index e912003f0..af202ea01 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,3 +1,7 @@
 The command has indeed failed with message:
 Last occurrence of "list'" must have "A" as 1st argument in
  "A -> list' A -> list' (A * A)%type".
+Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
+
+For foo: Argument scopes are [type_scope _]
+For Foo: Argument scopes are [type_scope _]
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
index 8db8956e3..8ff91268a 100644
--- a/test-suite/output/Inductive.v
+++ b/test-suite/output/Inductive.v
@@ -1,3 +1,7 @@
 Fail Inductive list' (A:Set) : Set :=
 | nil' : list' A
 | cons' : A -> list' A -> list' (A*A).
+
+(* Check printing of let-ins *)
+Inductive foo (A : Type) (x : A) (y := x) := Foo.
+Print foo.