| Age | Commit message (Collapse) | Author |
|---|
|
|
|
I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.
|
|
|
|
|
|
This makes setting the option outside of the synchronized summary impossible.
|
|
This introduces the warning “not-a-class” in the “typeclasses” category.
|
|
|
|
This avoids all the side effects associated with the manipulation of an
unresolvable flag. In the new design:
- The evar_map stores a set of evars that are candidates for typeclass
resolution, which can be retrieved and set.
We maintain the invariant that it always contains only undefined
evars.
- At the creation time of an evar (new_evar), we classify it as a
potential candidate of resolution.
- This uses a hook to test if the conclusion ends in a typeclass
application. (hook set in typeclasses.ml)
- This is an approximation if the conclusion is an existential (i.e.
not yet determined). In that case we register the evar as
potentially a typeclass instance, and later phases must consider
that case, dropping the evar if it is not a typeclass.
- One can pass the ~typeclass_candidate:false flag to new_evar to
prevent classification entirely. Typically this is for new goals
which should not ever be considered to be typeclass resolution
candidates.
- One can mark a subset of evars unresolvable later if
needed. Typically for clausenv, and marking future goals as
unresolvable even if they are typeclass goals. For clausenv for
example, after turing metas into evars we first (optionally) try a
typeclass resolution on the newly created evars and only then mark
the remaining newly created evars as subgoals. The intent of the
code looks clearer now.
This should prevent keeping testing if undefined evars are classes
all the time and crawling large sets when no typeclasses are present.
- Typeclass candidate evars stay candidates through
restriction/evar-evar solutions.
- Evd.add uses ~typeclass_candidate:false to avoid recomputing if the new
evar is a candidate. There's a deficiency in the API, in most use
cases of Evd.add we should rather use a:
`Evd.update_evar_info : evar_map -> Evar.t -> (evar_info -> evar_info)
-> evar_map`
Usually it is only about nf_evar'ing the evar_info's contents, which
doesn't change the evar candidate status.
- Typeclass resolution can now handle the set of candidates
functionally: it always starts from the set of candidates (and not the
whole undefined_map) and a filter on it, potentially splitting it in
connected components, does proof search for each component in an
evar_map with an empty set of typeclass evars (allowing clean
reentrancy), then reinstates the potential remaining unsolved
components and filtered out typeclass evars at the end of
resolution.
This means no more marking of resolvability/unresolvability
everywhere, and hopefully a more efficient implementation in general.
- This is on top of the cleanup of evar_info's currently but can
be made independent.
[typeclasses] Fix cases.ml: none of the new_evars should be typeclass candidates
Solve bug in inheritance of flags in evar-evar solutions.
Renaming unresolvable to typeclass_candidate (positive) and fix maybe_typeclass_hook
|
|
|
|
Removing a few Global.env in the way.
|
|
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
|
It seems these two functions don't belong there. We can remove one,
and place the other actually next to whether their semantics are
necessary.
Note that indeed the whole `Decls` file seems a bit suspicious, why we
do we register this information in a separate table instead of in the
main ones in `Lib` ?
At the suggestion of Gaëtan Gilbert we also remove unused function
`is_instance`.
|
|
|
|
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
|
|
|
|
Close #7562.
[api] move hint_info ast to tactics.
|
|
|
|
|
|
|
|
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|
`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
|
|
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|
|
|
|
|
Some code in typeclasses was even breaking the invariant that
use_polymorphic_flag should not be called twice, but that code was
morally dead it seems, so we remove it.
|
|
Typeclasses.typeclass
|
|
|
|
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.
|
|
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
|
|
|
There don't really bring anything, we also correct some minor nits
with the printing function.
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
This will allow to merge back `Names` with `API.Names`
|
|
|
|
|
|
|
|
This essentially means storing the abstract universe context in the typeclass
data, and abstracting it when necessary.
|
|
We return the abstract context instead of an arbitrary instantiation.
|
|
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
|
|
|
|
|
|
Also giving the proper local flag to the hint registration, even on a
Global instance, since the instance discharge manage itself the
redefinition of a hint.
|
|
|
|
It stores both universe constraints and subtyping information for
blocks of inductive declarations.
At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
|
|
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
|
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
|
|
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
|
|
|
|
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
