| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
We use private types to ensure apriori hashconsing, and get rid of the
use of recursive modules. The hash of the universe list is also inlined
into each node instead of relying on a supplementary indirection.
|
|
|
|
|
|
inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.
|
|
|
|
subst_univs_levels.
|
|
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one
used before introduction of hMaps in LMap/LSet.
|
|
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
|
|
larger than Type.1 etc...
|
|
of the argument is smaller than the other one.
|
|
Names and arguments were uniformized, and some functions were redesigned to
take their typical use-case into account.
|
|
|
|
variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
|
|
function, so plain pointer equality is sufficient.
|
|
|
|
|
|
and disable hashconsing of substituted instances which had a huge performance
penalty in general. They are hashconsed when put in the environment only now.
|
|
kernel in library/universes.ml.
|
|
generated by a mutual inductive definition (bug found in CFGV). Actually this
code can move out of the kernel.
|
|
|
|
univ_depends.
Also add a missing constraint when generating a fresh universe for a template polymorphic
inductive in that case.
|
|
|
|
|
|
conclusion, and results of
unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x
speedup in Ncring_polynom.
|
|
redundant in canonical arcs.
|
|
by the printing options (i.e. when "Print Universes" is set).
|
|
by the printer anyway.
|
|
to recover the trace of a universe inconsistency. Changed its name too btw.
|
|
a O(1) check, contrasting with the previous O(n) behaviour that rendered
universe constraint checking prohibitive on big files. I expect a 20% speedup
on such files.
|
|
- More cleanup. remove unneeded functions in universes
|
|
|
|
handling from
the instance/contexts and substitution code.
|
|
Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
|
|
|
|
|
|
|
|
allowing fast conversion to be used during unification while respecting the
semantics of unification w.r.t universes.
- Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv
is used for module subtyping.
- Outside, infer_conv is wrapped in Reductionops to register the right constraints
in an evarmap.
- In univ, add a flag to universes to cache the fact that they are >= Set, the
most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).
|
|
slightly more efficient than plain balanced maps.
|
|
|
|
- Finish the change to level-to-level substitutions, in the checker.
|
|
- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.
|
|
cases of Type (* Prop *) <= Set.
- Do check types of metavariables at the end of apply's unification,
if it failed at the beginning (otherwise universe constraints can be incomplete).
|
|
correctly when comparing stacks.
- Disallow Type i <= Prop/Set constraints, that would otherwise allow
constraints that make a universe lower than Prop.
- Fix stm/lemmas that was pushing constraints to the global context,
it is done depending on the constant/variable polymorphic status now.
- Adapt generalized rewriting in Type code to these fixes.
|
|
needed during
unification.
|
|
|
|
This should be now linear instead of the cubic Bellman-Ford algorithm.
The new algorithm assumes that the universe graph is a DAG if we remove
the {Le, Eq}-cycles, which is the case when the graph is consistent.
Luckily we only use the sorting algorithm on such consistent graphs,
in the Print Sorted Universes command.
|
|
eagerly solve l <= k constraints as k := l when k is a fresh variable coming
from a template type. This has the effect of fixing the variable at the first
instantiation of the parameters of template polymorphic inductive and avoiding
to generate useless <= constraints that need to be minimized afterwards.
|
