From 63d582c6cd12bc3f8134a5aa9e3bdbca0dd2e9ca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 23 Sep 2017 12:25:35 +0200
Subject: Fixing a bug of Print for inductive types with let-ins in parameters.

Adding a "let-in"-sensitive function hnf_prod_applist_assum to
instantiate parameters and using it for printing.

Thanks to PMP for reporting.
---
 kernel/reduction.ml  | 12 ++++++++++++
 kernel/reduction.mli |  6 ++++++
 2 files changed, 18 insertions(+)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b0f4a1e5f1..7a4f25e633 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -938,6 +938,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 573e4c8bde..ce019f0216 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -103,6 +103,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
 
-- 
cgit v1.2.3