| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
|
|
|
| |
univ_depends.
Also add a missing constraint when generating a fresh universe for a template polymorphic
inductive in that case.
|
| |
|
|
| |
Every time you use abstract a kitten dies, please stop.
|
| | |
|
| |
|
|
| |
Fixes bug #3346.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
- Fix HoTT coq bug #80, implicit arguments with primitive projections were
wrongly automatically infered.
|
| | |
|
| |
|
|
|
|
|
| |
a projection constant only of the form
λ params (r : I params), match r with BuildR args => args_i end, without any
other user input and relies on it being typable (no more primitive projections
escaping this).
|
| |
|
|
|
|
| |
Ocaml does not remove the .cmi file if compilation fails, thus causing
subsequent native compilations to fail due to mismatching interfaces.
For the sake of homogeneity, also remove the .cmo/.cmxs file along the way.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
declare takes care of ignoring side effects that are available in the
global environment. This is yet another instance of what the "abominion"
(aka abstract) can do: the code was checking for the existence in the
environment of the elimination principle, and not regenerating it (nor
declaring the corresponding side effect) if the elimination principle
is used twice.
Of course to functionalize the imperative actions on the environment
when two proofs generated by abstract use the same elim principle,
such elim principle has to be inlined twice, once in each abstracted
proof. In other words, a side effect generated by a tactic inside
an abstract is *global* but will be made local, si it must always
be declared, no matter what.
Now the system works like this:
- side effects are always declared, even if a caching mechanism thinks
the constant is already there (it can be there, no need to regenerate it
but the intent to generate it *must* be declared anyhow)
- at Qed time, we filter the list of side effects and decide which ones are
really needed to be inlined.
bottom line: STOP using abstract.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
The call to the native compiler can fail due to the sheer amounts of -I
options passed to it. Indeed, it is easy to get the command line to exceed
512KB, thus causing various operating systems to reject it. This commit
avoids the issue by only passing the -I options that matter for the
currently compiled code.
Note that, in the worst case, this commit is still not sufficient on
Windows (32KB max), but this worst case should be rather uncommon and thus
can be ignored for now.
For the record, the command-line size mandated by Posix is 4KB.
|
| |
|
|
| |
This reverts commit c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
and the lookup operation proved to be costly when dealing with big libraries.
|
| |
|
|
| |
problem with hashconsing at the same time. This fixes bug# 3302.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Fix restriction of universe contexts to not forget about potentially useful
constraints.
|
| |
|
|
|
|
|
| |
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.
|
Matthieu Sozeau
Enrico Tassi
Hugo Herbelin
Pierre-Marie Pédrot
Guillaume Melquiond