| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
| |
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
polymorphic definitions.
- This implementation passes universes in separate arguments and does not
eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
|
| |
|
|
| |
Add a flag to disallow minimization to set
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Remove predicative flag and adapt to new invariant where every universe
must be declared, ensuring it is >= Set, safe_repr is not necessary
anymore.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| |
|
|
|
| |
hash-consing, so as to avoid having too many kinds of equalities with
same name.
|
| |
|
|
|
| |
We were throwing away constraints from 'with Definition' in module
type ascriptions.
|
| |
|
|
|
|
|
|
| |
We passed the arc to be marked as visited to the functions pushing the
neighbours on the remaining stack, but this can be actually done before
pushing them, as the [process_le] and [process_lt] functions do not rely
on the visited flag. This exposes more clearly the invariants of the
algorithm.
|
| |
|
|
|
| |
We lambda-lift by hand the graph traversal functions in Univ to allocate
less closures.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
printing functions touched in the kernel).
|
| |
|
|
|
| |
One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
|
| |
|
|
|
|
|
|
|
|
| |
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
Matthieu Sozeau
Guillaume Melquiond
Gregory Malecha
Matthieu Sozeau
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès