[econstr] Continue consolidation of EConstr API under interp.
#6511
Conversation
ejgallego
added
kind: cleanup
ejgallego
force-pushed
the
econstr+more_fix
branch
3 times, most recently
from
292d844 to
4f3d2dd
Compare
|
https://ci.inria.fr/coq/job/benchmark-part-of-the-branch/267/console |
ejgallego
force-pushed
the
econstr+more_fix
branch
2 times, most recently
from
c0d6836 to
dc137ee
Compare
|
I think you should get rid of |
That's a good point, even if I think in most cases this patch addresses the universe part doesn't matter. It looks like the current granularity is not the best. |
|
I think that indeed |
So what do you propose? Previously there was no |
There was a problem hiding this comment.
This looks to me like a courageous PR, which we had to do at some time, whether it is for scability (e.g. eventually supporting features such as implicit arguments on goal variables even if they contain evars), for a better control of the flow of execution.
I don't feel fully competent to tell what is best to do though, considering that I don't have so much expertise on the econstr issue.
I made some comments, but more as questions or suggestions than as certainties. In particular, even if I read the whole patch, there are places where I'm unable to evaluate if the compromise made should be pushed one step further now or if it is the right one at the current time. I'm thinking e.g. to tacintern where,
probably, the evar_map should eventually logically become part of the ist (wondering about the opinion of @ppedrot though).
interp/impargs.ml
Outdated
| let compute_implicits_with_manual env typ enriching l = | ||
| let compute_implicits_with_manual env _sigma typ enriching l = | ||
| (* XXX: FIXME *) | ||
| let typ = EConstr.Unsafe.to_constr typ in |
There was a problem hiding this comment.
Why not to move sigma towards compute_implicits_gen?
There was a problem hiding this comment.
Sounds like a good idea @herbelin, what should be done with the whd_all there?
There was a problem hiding this comment.
Ok, done, I used reductionops.whd_all, but I added a comment to the commit.
There was a problem hiding this comment.
CC @maximedenes I believe this PR introduced the performance issue Damien showed us yesterday. I'll try to undo this change and use kernel's whd_all (that is by need) instead of Reductionops.whd_all that is by name, and see how it goes.
CC @ppedrot @ejgallego note that the sigma threaded there is an empty one, created with from_env... #6511 (comment)
| @@ -2052,19 +2052,17 @@ let empty_ltac_sign = { | |||
| ltac_extra = Genintern.Store.empty; | |||
| } | |||
|
|
|||
| let intern_gen kind env | |||
| let intern_gen kind env sigma | |||
| ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) | |||
| c = | |||
There was a problem hiding this comment.
From the moment intern_gen knows the sigma, it should be possible to statically check that CHole nodes (representing a ?x) refer to existing evars, correct?
There was a problem hiding this comment.
That's a question for @ppedrot but I think so.
| let l',cls = compute_arguments_scope_full sigma typ in | ||
| let l1 = List.firstn n l' in | ||
| let cls1 = List.firstn n cls in | ||
| (req,r,0,l1@l,cls1) |
There was a problem hiding this comment.
I would pass the env and sigma one step above to rebuild_arguments_scope in anticipation of a purely functional rebuild method (or otherwise replace the FIXME by a comment saying that no evars are expected here).
There was a problem hiding this comment.
@herbelin I have done so, however note that inArgumentsScope doesn't keep track of this properly, we may rethink.
interp/notation.ml
Outdated
| let (scs,cls as o) = compute_arguments_scope_full t in | ||
| let sigma, env = Evd.empty, Global.env () in (* FIXME? *) | ||
| let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in | ||
| let (scs,cls as o) = compute_arguments_scope_full sigma typ in |
There was a problem hiding this comment.
Idem, I would pass env and sigma to declare_ref_arguments_scope, and further. Then, the day we want to support implicit arguments or scopes on goal variables (which could be useful with big proofs), this will almost be ready, even if the goal variable mentions an evar.
Or, alternatively, to replace the FIXME by a comment telling that terms with evars are not (yet) supported here.
There was a problem hiding this comment.
Done, but see the mess that we get on interp/declare.ml
| @@ -1614,7 +1617,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num | |||
| tcc_lemma_constr | |||
| is_mes functional_ref | |||
| (EConstr.of_constr rec_arg_type) | |||
| (EConstr.of_constr relation) rec_arg_num | |||
| relation rec_arg_num | |||
| term_id | |||
| using_lemmas | |||
| (List.length res_vars) | |||
There was a problem hiding this comment.
What to do in funind would require the opinion of an expert. Maintaining the status quo as done here seems otherwise the reasonable thing to do.
ejgallego
force-pushed
the
econstr+more_fix
branch
from
dc137ee to
ffc872e
Compare
There was a problem hiding this comment.
Evd.from_env should be better than Evd.empty essentially always (in the context of this PR it might not be strictly better ^^).
I strongly feel we need some system to be able to use functions both with econstr+evar map and just constr when it makes sense. I don't know how to make it work exactly though.
interp/constrintern.ml
Outdated
| @@ -2078,8 +2076,8 @@ let intern_pattern globalenv patt = | |||
|
|
|||
| (* All evars resolved *) | |||
|
|
|||
| let interp_gen kind env sigma ?(impls=empty_internalization_env) c = | |||
| let c = intern_gen kind ~impls env c in | |||
| let interp_gen kind env sigma ?(impls=empty_internalization_env) c : EConstr.t * UState.t = | |||
| open Constrexpr | ||
| open Notation_term | ||
| open Pretyping | ||
| open Misctypes | ||
|
|
There was a problem hiding this comment.
Why did open Misctypes move?
There was a problem hiding this comment.
I tend to do the opens in "hierarchy" order.
interp/modintern.ml
Outdated
| let c, ectx = interp_constr env (Evd.from_env env) c in | ||
| let sigma = Evd.from_env env in | ||
| let c, ectx = interp_constr env sigma c in | ||
| let c = EConstr.to_constr sigma c in |
There was a problem hiding this comment.
Isn't to_constr (Evd.from_env env) the same as unsafe to_constr except slower?
I think we should merge the ectx into sigma before doing to_constr so that we normalise any temporary universe variables used by interp_constr (although not doing that seems not to have been a problem in the past).
There was a problem hiding this comment.
What's the proper way to merge this?
interp/notation.ml
Outdated
| let sigma, env = Evd.empty, Global.env () in (*FIXME?*) | ||
| let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in | ||
| let scs,cls = compute_arguments_scope_full sigma typ in | ||
| (req,r,List.length scs,scs,cls) |
There was a problem hiding this comment.
It seems like we only use the evar map to pass it to Reductionops.whd_betaiotazeta as that works on econstr only. Shouldn't we instead define some Reductionops.NoEvars.whd_... which would operate on constr and take no evar map?
Also I think the FIXME is about discarding the universe context from type_of_global.
interp/notation.ml
Outdated
| of the manually given scopes to avoid further re-computations. *) | ||
| let sigma, env = Evd.empty, Global.env () in (*FIXME?*) | ||
| let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in | ||
| let l',cls = compute_arguments_scope_full sigma typ in |
There was a problem hiding this comment.
The branches do the same thing up to this point, ie the function is equivalent to
let rebuild_arguments_scope (req,r,n,l,_) =
let sigma, env = Evd.empty, Global.env () in
(*FIXME?*)
let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
let scs,cls = compute_arguments_scope_full sigma typ in
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
(req,r,List.length scs,scs,cls)
| ArgsScopeManual ->
(* Add to the manually given scopes the one found automatically
for the extra parameters of the section. Discard the classes
of the manually given scopes to avoid further re-computations. *)
let l1 = List.firstn n scs in
let cls1 = List.firstn n cls in
(req,r,0,l1@l,cls1)Shall we do this combination?
There was a problem hiding this comment.
If @herbelin is OK I'm all for it.
vernac/comAssumption.ml
Outdated
| @@ -153,7 +153,7 @@ let do_assumptions kind nl l = | |||
| let env = | |||
| push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in | |||
| let ienv = List.fold_right (fun (_,id) ienv -> | |||
| let impls = compute_internalization_data env Variable t imps in | |||
| let impls = compute_internalization_data env sigma Variable EConstr.(of_constr t) imps in | |||
There was a problem hiding this comment.
Should we make interp_assumption return an econstr instead?
vernac/comFixpoint.ml
Outdated
| @@ -229,7 +228,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = | |||
| let sigma, nf = nf_evars_and_universes sigma in | |||
| let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in | |||
| let fixdefs = List.map (Option.map nf) fixdefs in | |||
There was a problem hiding this comment.
You can also use to_constr instead of successive maps for fixdefs.
vernac/comInductive.ml
Outdated
| @@ -283,15 +283,16 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = | |||
| let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in | |||
|
|
|||
| let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in | |||
| let fullearities = List.map EConstr.of_constr fullarities in | |||
There was a problem hiding this comment.
If we remove the EConstr.Unsafe.to_constr in interp_ind_arity (and use econstr it_mkProd_or_LetIn and modify push_types to be econstr) this should disappear.
There was a problem hiding this comment.
Done, but futher cleanup with arities seems to be needed.
vernac/vernacentries.ml
Outdated
| @@ -1776,7 +1777,7 @@ let vernac_search ~atts s gopt r = | |||
| (* if goal selector is given and wrong, then let exceptions be raised. *) | |||
| | Some g -> snd (Pfedit.get_goal_context g) , Some g | |||
| in | |||
| let get_pattern c = snd (intern_constr_pattern env c) in | |||
| let get_pattern c = snd (intern_constr_pattern env Evd.empty c) in | |||
There was a problem hiding this comment.
At line 1775 keep the evar map from Pfedit.get_goal_context and at line 1776 use from_env.
vernac/vernacentries.ml
Outdated
| @@ -1795,7 +1796,7 @@ let vernac_search ~atts s gopt r = | |||
| | SearchHead c -> | |||
| (Search.search_by_head gopt (get_pattern c) r |> Search.prioritize_search) pr_search | |||
| | SearchAbout sl -> | |||
| (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r |> Search.prioritize_search) pr_search | |||
| (Search.search_about gopt (List.map (on_snd (interp_search_about_item env Evd.empty)) sl) r |> Search.prioritize_search) pr_search | |||
|
Thanks for the review Gaëtan (@SkySkimmer) I have scheduled a revision in my TODO list. |
ejgallego
force-pushed
the
econstr+more_fix
branch
from
ffc872e to
87a35df
Compare
ejgallego
force-pushed
the
econstr+more_fix
branch
from
87a35df to
d4e18ae
Compare
|
Ok, I've done a pass, still this PR is quite complicated but let's see how it goes. IMHO we should try to keep pushing stuff like this. |
ejgallego
force-pushed
the
econstr+more_fix
branch
from
d4e18ae to
d548ff1
Compare
|
Ok so the PR works well in Travis, it needs a bit more of review thou and then I'll need to do overlays for equations and ltac. [should be easy]. I'd like to get this and #6454 in 8.8 if possible. |
ejgallego
force-pushed
the
econstr+more_fix
branch
from
d548ff1 to
255b637
Compare
coq/coq#6511 contains EConstr-related changes.
coq/coq#6511 contains EConstr-related changes. This change seems indeed positive.
|
Approved by @SkySkimmer , but certainly this change could use another round of reviews. Prior comments were very effective at improving the PR. |
|
Rebasing, keeping the See you in a few days 🤖 |
ejgallego
force-pushed
the
econstr+more_fix
branch
3 times, most recently
from
171e8a3 to
0c95af5
Compare
|
@ppedrot Can you have one last look? |
|
@herbelin During the WG, @ejgallego asked if you could have a quick look to check the way he took your comments into account. |
|
I just had a quick look. That's ok to me. |
ejgallego
force-pushed
the
econstr+more_fix
branch
from
0c95af5 to
e1eda51
Compare
|
@ppedrot any final words on this PR? |
|
tsssss... |
|
Oh! I was about to push the merge! |
|
Feel free to decide to leave it to a followup PR if you prefer. |
Oh I guess I missed them due to the github interface collapsing. Will take care of them. |
This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag.
|
Ok, all comments should be addressed now, thanks. |
ejgallego
force-pushed
the
econstr+more_fix
branch
from
e1eda51 to
886a9c2
Compare
coq/coq#6511 contains EConstr-related changes. This change seems indeed positive.
coq/coq#6511 contains EConstr-related changes. This change seems indeed positive.
coq/coq#6511 contains EConstr-related changes.
[coq] Adapt to coq/coq#6511
coq#6511 contains EConstr-related changes.
This commit was motivated by true spurious conversions arising in my
to_constrdebug branch.The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in
vernac/*.We have opted for penalize [minimally] the few users coming from true
Constr-land, but I am sure we can tweak code in a much better way.In particular, it is not clear if internalization should take an
evar_mapeven in the cases where it is not triggered, see thechanges under
pluginsfor a good example.Also, the new return type of
Pretyping.understandshould undergocareful review.
We don't touch
Impargsas it is not clear how to proceed, however,the current type of
compute_implicits_genlooks very suspicious asit is called often with free evars.