-
Notifications
You must be signed in to change notification settings - Fork 675
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[econstr] Cleanup in vernac/classes.ml
#6392
Conversation
5bd14f5
to
bcbc88a
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The nf_evars_and_universes and a couple almost-aliases like nf_evar_map_universes do universe minimization, so we can't just remove them.
I agree the name should mention minimization.
let pars = fst (List.chop lenpars args) in | ||
match cl.cl_impl with | ||
| IndRef ind -> | ||
let ind = ind, u in | ||
(Some (applistc (mkConstructUi (ind, 1)) args), | ||
applistc (mkIndU ind) pars) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should we maybe have econstr applistc instead?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would be more in favor of removing one of the two, having two versions seems a bit pointless, right? Are they used in some particular combinator?
val instance_constructor : typeclass Univ.puniverses -> constr list -> | ||
constr option * types | ||
val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list -> | ||
EConstr.t option * EConstr.t |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The other functions in this file could also be econstr.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am not sure, it looks to me like a few of these functions are expected to return ground terms, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When I looked there were a few which did unsafe to constr, I would say at least those should use econstr.
if abstract then | ||
begin | ||
let subst = List.fold_left2 | ||
(fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') | ||
[] subst (snd k.cl_context) | ||
in | ||
let (_, ty_constr) = instance_constructor (k,u) subst in | ||
let nf, subst = Evarutil.e_nf_evars_and_universes evars in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is required too, you just didn't hit a case where it was used.
Note to self: fixed but github doesn't see it on the next line.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Indeed Travis does show problems.
vernac/classes.ml
Outdated
@@ -372,10 +369,7 @@ let context poly l = | |||
let env = Global.env() in | |||
let evars = ref (Evd.from_env env) in | |||
let _, ((env', fullctx), impls) = interp_context_evars env evars l in | |||
let fullctx = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) fullctx in | |||
let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is also required.
Interesting, thanks for having a look @SkySkimmer . I have a few questions thou:
I guess again this boils down to what the meaning of |
Yes.
Nonexistant.
Should maybe.
I'm not sure what you mean by that. It's tricky because if you're doing multiple constants at once which refer to each other ( I think one thing we could do is provide a function val definition_entry_easy : (* name TBD *)
opaque:bool -> inline:bool -> ?types:EConstr.types ->
proof_state:Evd.evar_map -> polymorphic:bool -> udecl:UState.universe_decl ->
-> body:EConstr.t -> Safe_typing.private_constants definition_entry which handles universe minimization, declaring universe binders, extracting private constant stuff from the evd and maybe some other misc stuff (up to changing the arguments a bit). (the definition_entry gets fed to declare_constant) This should get actual design involving looking at what we do in core and what plugins do in the wild. |
Indeed you did read my mind. The current API is indeed problematic as the steps every client must do are very complex, and worse, dependent on low-level implementation details.
I meant that the client could just not care of universes and have some inference stuff done at QED time, but that may not work but polymorphism. I was just thinking out loud. But going back to the actual code, indeed, it looks like most API users would like to build a constant in the way you propose. I think for example a good test plugin could be coq-paramcoq [crazy stuff there now, it would be good to see if your proposed API would work for them]. I would go even further, protecting [making private] all the universe minimization functions etc... So all the layers above engine can only use the Clearly we have to do something that guarantees that minimization proceeds properly, adding 100 test cases seems not viable for me [mainly because we won't maintain them]. |
bcbc88a
to
7a89508
Compare
Ok, some cleanup and fixes as suggested by @SkySkimmer done, I went a bit further and also cleaned up |
@@ -112,22 +110,22 @@ let instance_hook k info global imps ?hook cst = | |||
Typeclasses.declare_instance (Some info) (not global) cst; | |||
(match hook with Some h -> h cst | None -> ()) | |||
|
|||
let declare_instance_constant k info global imps ?hook id decl poly evm term termtype = | |||
let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here you rename evm -> sigma but the one above you rename evars -> evd
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
More consistency needed indeed. The thing is that I am not so fond of sigma
, but I recall that this is the proper convention, right @ppedrot ?
let _evd = ref sigma in | ||
let impls, ((env', ctx), imps) = interp_context_evars env _evd ctx in | ||
let c', imps' = interp_type_evars_impls ~impls env' _evd tclass in | ||
let sigma = !_evd in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't like underscore variables.
How about
let sigma = ref sigma in
let impls, ... = ... in
let c', ... = ... in
let sigma = !sigma in
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That is temporal anyways, I have a patch migrating that not to use a ref. I like the underscore as it bugs people to fix it.
vernac/classes.ml
Outdated
Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); | ||
let univs = Evd.check_univ_decl ~poly !evars decl in | ||
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in | ||
(* Note, this imperative updates the evar_map! [Then used in to_constr] *) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
??
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Leftover comment, good catch.
Some (Inr (c, subst)) | ||
let _evd = ref sigma in | ||
let c = interp_casted_constr_evars env' _evd term cty in | ||
Some (Inr (c, subst)), !_evd |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just use let sigma
.
k.cl_props props subst)) | ||
in | ||
let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in | ||
let _evd = ref sigma in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
sigma
let fullctx = Context.Rel.map subst fullctx in | ||
let ce t = Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr t) in | ||
let sigma = Evd.from_env env in | ||
let _evd = ref sigma in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
sigma
7a89508
to
7e787c4
Compare
I've pushed a couple of minor nits, [keeping the More interestingly, at least in my Travis we got a case where FLambda fails but not the regular build, interesting! It could well be a flambda bug, but the blame is likely on my side. |
Note that I have a very large patch doing a pass on |
vernac/classes.ml
Outdated
let _, ((env', fullctx), impls) = interp_context_evars env _evd l in | ||
let sigma = !_evd in | ||
(* Note, we must use the normalized evar from now on! *) | ||
let evm,_ = Evarutil.nf_evars_and_universes sigma in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not use shadow sigma here?
How so? |
Let's wait for Travis, but basically I am replacing: let sigma, nf = Evarutil.nf_evar_map_universes sigma in
let c = EConstr.Unsafe.to_constr c in
let c = nf c in by let sigma, _ = Evarutil.nf_evars_and_universes sigma in
let c = to_constr sigma c in |
By the way I'm sure this interests at least @gasche , in this travis we are getting different results for Coq compiled with It could well be a Coq bug so not reporting upstream for now. |
Interesting indeed! Let me know if you manage to reproduce this locally, and if you have simplified reproduction instructions. There can be bugs in flambda, but it can also be the case that more aggressive optimizations change the evaluation order (in ways that are valid -- the evaluation order of OCaml programs is not uniquely specified -- but still result in observable differences in user code). We are trying to avoid these situations (they can be reported as issues that flambda people will try to fix), but they can still happen. |
7e787c4
to
e55376b
Compare
Reproduction should be easy, just try to compile the Coq commit 7e787c4 with 4.06.0 and 4.06.0+flambda. There were a couple of bugs in the patch [trying a fresh build], but given the nature of the code I found it interesting that only flambda showed a problem. Indeed, likely due to some dead code removal. |
vernac/classes.ml
Outdated
let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in | ||
let _evd = ref sigma in | ||
Some (Inl (type_ctx_instance (push_rel_context ctx' env') _evd | ||
kcl_props props subst)), !_evd |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This line is broken in flambda, it returns non-modified sigma
when we want the one modified by runnning type_ctx_instance
(at least in ocamldebug).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Confirmed that let-lifting the function application fixes the missing constraint in crelationclasses.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is typically a case where both evaluation orders are valid, so you should left-lift the type_ctx
application indeed if it needs to be performed before !_evd
is computed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh indeed that was my fault; I was not so careful as I was planning to remove that code anyways.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In fact the ref
and the _evd
are already gone in the next PR.
e55376b
to
49e4b36
Compare
This just removes a few type castings. Indeed, it seems that the upstream change was positive then.
We fix quite a few types, and perform some cleanup wrt to the evar_map, in particular we prefer to thread it now as otherwise it may become trickier to check when we are using the correct one. Thanks to @SkySkimmer for lots of comments and bug-finding.
49e4b36
to
7799626
Compare
So thanks to @SkySkimmer this is starting to look ready for merging. With regards the |
vernac/classes.ml
@ejgallego AFAIU, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks ready to me as well.
Thanks for the explanation, it is a bit hard to figure out what is the proper normalization to apply. |
Finally ready. |
|
[coq] Adapt to coq/coq#6392
We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.
Overlay: mattam82/Coq-Equations#34