Fixing Print for inductive types with let-in in parameters #1082
Conversation
79bdff4 to
44cee4a
Compare
|
I'll try to review at least the VM part. |
|
@maximedenes: If you could check whether it is normal that |
|
I missed this bugfix in the list for 8.7+beta2. @maximedenes what do we do about this? |
|
@maximedenes: you intended to try to review at least the vm part of this PR at some time, right? Otherwise, same question as in #873: who should feel responsible for the non-staling of need flags? |
kernel/reduction.ml
Outdated
| 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.") |
There was a problem hiding this comment.
Isn't this rather too many arguments?
There was a problem hiding this comment.
Well spotted. The error actually also appears twice in term.ml. I fixed all of them.
kernel/reduction.mli
Outdated
| @@ -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 [m] and possibly with let-ins; it | |||
There was a problem hiding this comment.
Idem, was a copy-paste of the same typo in a comment of term.mli. Fixed here and in term.mli
kernel/term.mli
Outdated
| 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 |
44cee4a to
26512eb
Compare
|
@maximedenes: Maybe can I remove the |
|
I just looked at it, the fix looks reasonable, but we are probably missing a similar one in |
| @@ -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 = | |||
There was a problem hiding this comment.
Why do we take n? Is it just a safety measure?
There was a problem hiding this comment.
Oh, no, I understand now, it is to make sure that all local definitions are unfolded, if they are included in n.
pretyping/vnorm.ml
Outdated
| 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 |
There was a problem hiding this comment.
Is this going to change anything? If I understand correctly, it could unfold more local definitions, if they come after the arguments. But the next line does a whd_all anyway.
There was a problem hiding this comment.
Yes, I think I agree, this does not change the final semantics. The reason to do it is by separation of concerns. For instance, if you eventually change whd_all by some other reduction, or remove it, the instantiation of the telescope of the inductive type will remain correct while if the unfolding of the let's of the telescope is partly done by the function to instantiate the telescope and partly done with a further whd_all, this would not be true anymore.
There was a problem hiding this comment.
Isn't this morally replacing call by value by call by name on the LetIn part? I'm very tired so I may be completely wrong, but it seems that the new implementation will simply substitute the body of the LetIn before reducing it.
|
@herbelin Any plan to address @maximedenes' comment? |
|
@herbelin already replied, I need to read and think a bit. Sorry, I'm very overloaded. |
|
The linter fails and VST times out. I suppose we can ignore these errors, especially given that the 8.7.1 deadline is tomorrow (so merging today). @maximedenes this is just awaiting you to see if you understand Hugo's reply. |
…n doc. Was introduced in e8c47b6.
Adding a "let-in"-sensitive function hnf_prod_applist_assum to instantiate parameters and using it for printing. Thanks to PMP for reporting.
This enforces the intended meaning of the corresponding functions (prod_appvect*/prod_applist*).
26512eb to
42610a4
Compare
|
I magically |
I'm dismissing to make a step forward, but feel free to reopen to restart a discussion
|
@herbelin did you see my comment about this patch turning call by value into call by name (substituting the body of let-ins before reducing it) ? Is that accurate? |
|
@herbelin Can you answer to @maximedenes latest comment? |
|
In fact I believe some of my comments above were wrong, so I'll have another look this week. Anyway this will be merged before 8.7.2. |
|
@maximedenes Sorry to add to your load. I know you are busy. But please review this ASAP if you don't want to have it miss 8.7.2. (We need to account for CI time and other things.) |
Is this still an open question? (If yes, I do not see which comments you are talking about.) |
|
Will review today, as soon as I have a minute. |
…in in parameters
…et-in in parameters
…et-in in parameters
@ppedrot mentioned the following printing bug:
The first commit of this PR fixes this printing bug as well as a similar printing bug for records with trailing let-ins in parameters. The bug was caused by using
hnf_prod_applist(on-the-fly substitution of products) which is not let-in aware.In a second commit, I protectively changed a suspicious use of
hnf_prod_applistin computing the type of a vm_computedmatch(if I understand correctly). I was not able to say at once if the functionVnorm.nf_predicatewas doing the expected job w.r.t. let-ins (isn't aLetIncase missing? and what is thiscrazy_type?). I let it to the specialists.The checker (and the kernel) are also using
hnf_prod_applistbut in situations where already only a subset of the signature of parameters is considered (the signature of recursively uniform parameters). So, it does not seem to be a problem to me. After all, it is equivalent to have trailing let-in parameters and to uniformly distribute these let-in parameters on the constructors and on the arities.