[econstr] Cleanup in vernac/classes.ml
#6392
Conversation
ejgallego
force-pushed
the
econstr+fix_class
branch
2 times, most recently
from
5bd14f5 to
bcbc88a
Compare
| 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.
Should we maybe have econstr applistc instead?
There was a problem hiding this comment.
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.
The other functions in this file could also be econstr.
There was a problem hiding this comment.
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.
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.
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.
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 | |||
|
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_entrywhich 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]. |
ejgallego
force-pushed
the
econstr+fix_class
branch
from
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.
Here you rename evm -> sigma but the one above you rename evars -> evd
There was a problem hiding this comment.
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.
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.
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.
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 |
| 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 |
| 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 |
ejgallego
force-pushed
the
econstr+fix_class
branch
from
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.
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 inby 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. |
ejgallego
force-pushed
the
econstr+fix_class
branch
from
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.
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.
Confirmed that let-lifting the function application fixes the missing constraint in crelationclasses.
There was a problem hiding this comment.
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.
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.
In fact the ref and the _evd are already gone in the next PR.
ejgallego
force-pushed
the
econstr+fix_class
branch
from
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.
ejgallego
force-pushed
the
econstr+fix_class
branch
from
49e4b36 to
7799626
Compare
ejgallego
added
the
needs: overlay
|
So thanks to @SkySkimmer this is starting to look ready for merging. With regards the |
ejgallego
changed the title
ejgallego
changed the title
vernac/classes.ml
|
@ejgallego AFAIU, |
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