| Age | Commit message (Collapse) | Author |
|---|
|
When making a universe a variable we iterate through the universes
we're equal to and if we find one we update the substitution
accordingly.
NB: The bug called make_flexible_variable on Top.15 and
~~~
{Top.15 Top.14} |= Top.11 < Top.6
Top.14 < Top.5
Top.11 = Top.15
ALGEBRAIC UNIVERSES:{Top.17 Top.16}
UNDEFINED UNIVERSES:Top.17 := Top.14+1
Top.16 := Top.14+1
WEAK CONSTRAINTS:
~~~
so now we would add [Top.15 := Top.11].
|
|
|
|
cleanups
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The names are `uXXX` with `XXX` some number avoiding collision.
Note that there may be some collisions with polymorphic binders, eg
something like
~~~
Set Universe Polymorphism.
Section foo.
Universe u0.
Definition bar := Type.
(* bar@{u0} = Type@{u0} but this isn't the section u0 *)
Definition baz := Type@{u0}. (* this one is the section u0 *)
Definition foobar := Eval compute in baz -> Type.
(* Type@{u0} -> Type@{u0} but these aren't the same u0 *)
~~~
So maybe we should do a nametab lookup too. This is strictly a
printing issue (polymorphic binder names have no other use).
In the monomorphic case names are qualified by the parent definition
so it should be fine (barring module/definition collision but we
already have those).
Note that there are still unnamed universes as they didn't go through
UState (eg schemes).
|
|
|
|
There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.
|
|
|
|
|
|
|
|
|
|
[ci skip]
|
|
|
|
functions
|
|
|
|
printing.
|
|
This emphasizes that it works only on inductive types.
Also, the name is_template_polymorphic will be reused for a more
general version.
|
|
This is a step towards limiting calls to the global environment.
Incidentally unify naming evd -> sigma in Termops.
|
|
for the determination of evars that can be turned into obligations.
|
|
Fixes #8224, fixes #8427 .
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
In favor of a constr_of_monomorphic_global function. When people
move to the new Coqlib interface they will also see this deprecation
message encouraging them to think about the best move.
This commit changes a few references to constr_of_global and replaces
them with a constr_of_monomorphic_global which makes it apparent that
this is not the function to call to globalize polymorphic references.
The remaining parts using constr_of_monomorphic_global are easily
identifiable using this: omega, btauto, ring, funind and auto_ind_decl
mainly (this fixes firstorder). What this means is that the symbols
registered for these tactics have to be monomorphic for now.
|
|
In general, `Nametab` is not a module you want to open globally as it
exposes very generic identifiers such as `push` or `global`.
Thus, we remove all global opens and qualify `Nametab` access. The
patch is small and confirms the hypothesis that `Nametab` access
happens in few places thus it doesn't need a global open.
It is also very convenient to be able to use `grep` to see accesses to
the namespace table.
|
|
Thus the adhoc univops can be removed at the end of the deprecation period.
Should we keep exposing restrict_universe_context or make people go
through restrict?
restrict_universe_context is used directly only by newring, where it's
a choice between
let univs = UState.restrict_universe_context univs vars in
and
let univs = UState.(context_set (restrict (of_context_set univs) vars)) in
|
|
It's basically an occur check so it makes sense to put it in vars
|
|
Such a basic function can live in Univ rather than the higher level UnivGen.
|
|
They are impractical since we need to get the level out to register it
afterwards.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This is to move a standard combinator to the place it belongs to. An
alternative could have been to put it in termops.ml, but termops.ml is
now about econstr, so, even if it makes the kernel "bigger", constr.ml
seems to be the best place for this combinator. After all, this
combinator is canonical.
|
|
All the `evar_map` APIs were deprecated in 8.9, thus we deprecate the
combinators to discourage this style of programming.
Still a few places do use imperative style, but they are pretty
localized and should be cleaned up separately.
As these are the last bits of `e_` API remaining this PR closes #6342.
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
