diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-23 12:25:35 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-14 15:57:51 +0100 |
commit | 63d582c6cd12bc3f8134a5aa9e3bdbca0dd2e9ca (patch) | |
tree | 368bc9298c9694c705bb66d89638a96f54aa8a89 /kernel | |
parent | e0c06c7dac30b9959a3eb90b0c1d324f061a8660 (diff) |
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.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/reduction.ml | 12 | ||||
-rw-r--r-- | kernel/reduction.mli | 6 |
2 files changed, 18 insertions, 0 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b0f4a1e5f..7a4f25e63 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 573e4c8bd..ce019f021 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 |