| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Even more invariants can be enforced this way.
|
|
|
|
Mere isomorphism for now, but will allow more invariants ultimately.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Most of these files were introduced after #6543 but used older headers
copied from somewhere else.
|
|
|
|
|
|
This enforces more invariants statically.
|
|
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
|
|
Instead we get the symbols from a Environ.env.
We make them accessible to the produced code through a reference
managed by the kernel, similar to the return values except inverting
when it's written and when it's read.
|
|
|
|
We move the role data into the evarmap instead.
|
|
Preparing for it to be stored in an Environ.env.
|
|
side-effects
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
Reviewed-by: vbgl
|
|
Instead of having the monormorphic universes from the immediate
data separated from the ones from the body, we only rely on the
former. There is no reason to delay given that the body is always
force upfront.
|
|
Since the introduction of delayed section substitution, the opaque table
was already containing the same information.
|
|
This will allow an easier removal of the discharge segment in a later
commit.
|
|
Instead we do that on a by-need basis by reusing the section info already
stored in the opaque proof.
|
|
This lets us avoid having to cache the SearchBlacklist.elements call
in search as we can just use the set module's for_all function.
|
|
We do not partially abstract the section info. Instead, we reuse the same
code in cook_constr and cook_constant and pass the same section info.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Cooking
Reviewed-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.
In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.
|
|
Reviewed-by: gares
Ack-by: maximedenes
|
|
We use the right environment.
|
|
For now this is just a specialized version of the previous generic code.
This simplifies tracking of the changes.
|
|
It is guaranteed by Declare, but a little dynamic check does not hurt.
|
|
The only lawbreaker was the Add Ring command. We generate a type for
the declaration to fix the code.
|
|
|
|
We get rid of the future wrappers, as all callers are immediately forcing
the result.
|
|
|
|
This is the intended module for the feature provided by the inductive
discharge. This allows for a bit of code sharing and cleanup.
|
|
|
|
|
|
Safe_typing is now responsible for hashconsing of all accessible structures,
except for opaque terms which are handled by Opaqueproof.
|
|
Reviewed-by: Zimmi48
|
|
We simply pass them as arguments, now that they are not called by the
kernel anymore.
The checker definitely needs to access the opaque proofs. In order not to
touch the API at all, I added a hook there, but it could also be provided
as an additional argument, at the cost of changing all the upwards callers.
|
|
This function is breaking the indirect opaque abstraction, so we move it
outside of the kernel. Unluckily, there is no better place to put it, so
we leave it in Global.
The checker uses it in a fundamental way, so we reimplement it there, but
this will eventually get removed.
|
|
Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.
This also enhances debug printing, as the latter is unable to properly
print futures.
|
|
We know statically that the check function producing this forces its
argument, so there is no point in chaining futures lazily.
|
|
|
|
|
|
|
|
This seems more robust and avoids having another implementation of
`cp`.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: maximedenes
|
