| Commit message (Collapse) | Author | Age |
|\ |
|
| |
| |
| |
| | |
This eliminates 3 uses of Obj from TCB.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
|
| |
| |
| |
| |
| |
| | |
This field was not used inside the kernel and not used in
performance-critical code where caching is essential, so we extrude
the code that computes it out of the kernel.
|
|/
|
|
|
|
| |
This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
|
|
|
|
|
|
|
|
|
|
| |
Unluckily, this is completely wrong as we trust the inlined term to be
well-typed in some unavailable environment. To start with, the checker
should not even rely on substitutions as it does not trust functors,
but it does anyways. I have thus commented this code as a useful backdoor
for when Coq is used to implement the next blockchain Ponzi scheme.
We really need to sort this out though.
|
|\
| |
| |
| | |
coinductive types.
|
| |
| |
| |
| |
| | |
Instead of having the projection data in the constant data we have it
independently in the environment.
|
|\ \
| | |
| | |
| | | |
global env
|
|\ \ \
| | | |
| | | |
| | | | |
in CArray
|
| |/ /
|/| | |
|
|\ \ \ |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
instances
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| |_|/ /
|/| | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
The reduction machine of the checker was not taking into account the fact
that cofixpoints needed to be unfolded when applied against a projection.
|
| |_|/
|/| | |
|
| |/ |
|
|/ |
|
| |
|
|\ |
|
| | |
|
|/
|
|
| |
Makes printing rules more explicit and should close #6799.
|
| |
|
|\ |
|
|\ \ |
|
| |/
|/| |
|
|\ \ |
|
|\ \ \
| | | |
| | | |
| | | | |
constraints.
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
camlp4
|
| | | | |
| | | | |
| | | | |
| | | | | |
longer use camlp4.
|
| |/ / /
|/| | |
| | | |
| | | |
| | | | |
We defer the computation of the universe quantification to the upper layer,
outside of the kernel.
|
| |/ /
|/| | |
|
|\ \ \ |
|
| | |/ |
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
|/
|
|
|
|
|
|
|
|
| |
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
|
|
|
| |
This just shares the unfold_projection between Closure and Reduction.
|
| |
|
|
|
|
| |
Fixes #5747: "make validate" fails with "bad recursive trees"
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
Primitive projections were not correctly unfolded, leading to failure of
conversion checks in some cases. The kernel was strangely not affected by
this bug, and it was probably a remnant of some vestigial code.
|
| |
|
|
|
|
|
| |
We also have to update the checker to deserialize this additional data,
but it is not using it in type-checking yet.
|
| |
|
|
|
|
|
|
| |
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
|