Cleaning comAssumption.ml

[herbelin]

Kind: cleanup

This PR is a step towards merging the different paths for Context and Variables (and their variants).

It includes

• relying on a generic interp_named_context_evars to interpret contexts
• checking that evars are resolved the same way
• a new kind of declaration kind for x:=t in Context
• experimenting removing the special case of Context outside sections for Module Type (finally done in #18254)
• a few more sanity checks
• coqdoc location for Variables like it was for Context
• a step towards possibly supporting Program Context

To deal with the residual differences of interpretation between Variable/Parameter and Context, we introduce the following parameterization:

• Variable/Parameter call interp_named_context_evars with the share flag on while Context calls it with the share flag off. For instance, Variables A B : Type shares the universe level but Context (A B : Type) introduces two universe levels. See also #13477.
• Deactivation of implicit arguments in Context is done by calling interp_named_context_evars with implicit mode off.
• Context tries to declare variables in classes as instances but not Variable/Parameter.

Notes:

• Implicit arguments in declarations show the following limits:

  Section A.
  Set Implicit Arguments.
  Variables (f1 : _ )                     (x1 : f1 0 (eq_refl 0) = 0).
  Variables (f2 : forall n:nat, n=n->nat) (x2 : f2   (eq_refl 0) = 0).
  About f1.
  About f2. (* same type and implicit arguments as f1 *)
  

• What to do with the discrepancy between the first and the other monomorphic axioms of a bunch of declarations (see #13477)
• Should local definitions in Context be polymorphic when Universe Polymorphism is on? Currently, it is no.

---

Depends on #18396 (merged) and #18397.

• [x] Added / updated test-suite
• [ ] Corresponding documentation was added / updated
• [ ] Entry added in the changelog

[silene]

As this is still a draft, I am postponing it to 8.15.

[coqbot-app[bot]]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app[bot]]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[coqbot-app[bot]]

This PR was not rebased after 30 days despite the warning, it is now closed.

[herbelin]

Status of last rebase:

• rather than trying to unify the semantics of Variables/Parameter and Context, we unify only the code, using flags to specialize it to either semantics (i.e. whether class instances are declared, which is done, or whether implicit arguments are used, whether A B:T is the same T or two copies of T, polymorphism of local definitions, which is not done; in particular Equality Scheme in test-suite fails for this reason)
• there is still a syntactic difference (list of assumptions with possibly :> and @{i} for Variables/Parameters all syntax of binders for Context)

@coqbot run full ci

Overlays needed at least for elpi, coq-lsp, metacoq.

[herbelin]

Rebased, including fixing redundant dumpglob in constrintern.ml and following the usage of having dumpglob done in vernacentries.ml.

Remarks from above comment still apply.

[ejgallego]

Also, do you think declare_local could/should better go in declare.ml? Or a part of it. For instance, in other declare_foo, assumption_message/definition_message and maybe_declare_manual_implicits are done in declare.ml so maybe should they be done here also in declare.ml?

I have no idea right now, maybe we could setup a meeting with people interested on the Declare API and try to come up with a roadmap for it?

[proux01]

@herbelin what is the status of this, can it be reviewed / merged ?

[herbelin]

@herbelin what is the status of this, can it be reviewed / merged ?

I applied the API suggestions of @ejgallego (making the API quite nice and regular I would say) and it apparently needs two other overlays. Otherwise, it is ready to be reviewed.

It currently has quite a lot of atomic commits (all compiling individually), but smashing some of them could also be done if useful.

[proux01]

Ok, I'll try to review in the coming weeks.

[herbelin]

Note: there are about 10 commits concerned with documenting other files than comAssumption.ml, or adding utilities in other files, or adding tests, which could go to other stand-alone PRs if ever it might help. Now going to reword the message to make this more visible.

[proux01]

Thanks for the offer, I'll tell you while reviewing if ever I'm not confident merging any of those.

[herbelin]

@coqbot run full ci

[coqbot-app[bot]]

:red_circle: CI failure at commit b7f4b2e0dcfdfa43bb1f09c47804a97109ed0e14 without any failure in the test-suite

:heavy_check_mark: Corresponding job for the base commit 08de5508102c406667491681a334e2e5b05ce6d9 succeeded

:grey_question: Ask me to try to extract a minimal test case that can be added to the test-suite

:runner: @coqbot ci minimize will minimize the following target: ci-elpi_test

• You can also pass me a specific list of targets to minimize as arguments.

[herbelin]

The elpi error is true: I inadvertantly modified the behavior of interp_context whose only known client is elpi. I'm waiting for @gares feedback to know if I restore the previous behavior or if he considers that it is better to change elpi.

[herbelin]

@coqbot run full ci

[herbelin]

And thanks a lot for the careful reading.

[proux01]

@coqbot run full ci

[proux01]

@coqbot merge now

[coqbot-app[bot]]

@proux01: Please take care of the following overlays:

• 13445-herbelin-master+reworking-assumptions.sh