| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: ppedrot
|
|
This takes advantage of the mutability of the fconstr relevance mark.
|
|
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
I think the usage looks cleaner this way.
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
The use of a term is not needed for the fast typing algorithm of the
application case, so this tweak brings the best of both worlds.
|
|
There is little point to this as the type is dependent on an open value and
is never computed further.
|
|
|
|
|
|
We know that the two are living in a common type, so that it is useless
to perform the comparison check. Note that we only use this fast-path when
the branches are only made of lambda-abstractions, but this covers
all actual cases.
|
|
They are only used once, thus it is completely useless to reallocate arrays
that are going to be destructed immediately.
|
|
No reason to split the code, this function is only used once.
|
|
|
|
Just like in the Sixth Sense, it turns out it was dead code all along.
|
|
This is a partial resurrection of #6423 but only for the kernel.
IMHO, we pay a bit of price for this but it is a good safety
measure.
Only warning "4: fragile pattern matching" and "44: open hides a type"
are disabled.
We would like to enable 44 for sure once we do some alias cleanup.
|
|
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
|
|
|
|
Not sure if worth using in other places.
|
|
|
|
We eta-expand cofixpoints when needed, so that their call-by-need
evaluation is correctly implemented by VM and native_compute.
|
|
|
|
|
|
|
|
We expected `nparams + nrealargs + consnrealargs` but the `nrealargs`
should not be there. This breaks cumulativity of constructors for any
inductive with indices (so records still work, explaining why the test
case in #6747 works).
|
|
|
|
|
|
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
|
|
- Nothing to check in conversion as they have a common supertype
by typing.
- In inference, enforce that one is lower than the other.
|
|
|
|
Now that the cache is distinct, there should be no nasty side-effects changing
the value of one side while reducing the other.
|
|
|
|
|
|
|
|
|
|
information.
|
|
|
|
|
|
This ensures by construction that we never infer constraints outside
the variance model.
|
|
|
|
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 part in Reduction should be semantics preserving, but Reductionops
only tried cumulativity if equality fails. This is probably wrong so I
changed it.
|
|
|
|
This fixes the previous patch in rare corner-cases where unification code was
relying on both kernel conversion and specific transparent state.
|
|
This definitely qualifies as a micro-optimization, but it would not be
performed by Flambda. Indeed, it is unsound in general w.r.t. OCaml
semantics, as it involves a fixpoint and changes potential non-termination.
In our case it doesn't matter semantically, but it is indeed observable
on computation intensive developments like UniMath.
|
|
- use Redflags.red_projection
- share unfold_projection between CClosure and Reduction
|
