| Age | Commit message (Collapse) | Author |
|---|
|
This approach using `type t = { sec_prev: t option; sec_... }` makes
it easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.
We may instead consider using `type t = section * section list` which
needs some boilerplate to update.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
|
|
Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
Rather than in typeops
|
|
If you have access to a kernel name you also should have the
environment in which it is defined, barring hacks. In order to
disfavor hacks we make the standard lookups raise anomalies so that
people are forced to admit they rely on the internals of the
environment.
We find that hackers operated on the code for side effects, for
finding inductive schemes, for simpl and for Print Assumptions. They
attempted to operate on funind but the error handling code they wrote
would have raised another Not_found instead of being useful.
All these uses are indeed hacky so I am satisfied that we are not
forcing new hacks on callers.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
|
|
|
|
This ensures that side-effect declarations come with their body, in prevision
of the decoupling of the Safe_typign API for CEP 40.
|
|
proofs.
We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.
|
|
We separate the Term_typing inference API into two functions, one to
typecheck just the immediate part of an entry, and another one to check
after the fact that a delayed term is indeed a correct proof for an opaque
entry.
This commit is mostly moving code around, this should be 1:1 semantically.
|
|
The information is already there.
At some point we may want to clean up the Lib API to reduce redundancy
wrt kernel functions like [sections_are_opened], but I'm not doing now
as it would conflict with https://github.com/coq/coq/pull/10670
|
|
Reviewed-by: gares
|
|
|
|
We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.
Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.
|
|
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
|
|
This allows to remove the double declaration of monomorphic universes of
discharged section constants. This also makes it much clearer that only
the first declaration of a constant is allowed to declare delayed
constraints.
As a nice bonus, this simplifies the Opaqueproof API.
|
|
This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.
|
|
Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.
|
|
For now we only keep a count of the number of open sections, discriminating
between polymorphic and monomorphic ones.
|
|
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
The caller should push them first
|
|
|
|
It is not the role of the kernel to decide to force the body of an entry
to infer the section variable it uses, but the one of the upper layers.
We make this explicit in the type of entries so as to enforce that this
inference is performed beforehand.
Also removes auxilliary file stuff that doesn't look like it belongs in
the kernel either.
|
|
|
|
|
|
Even more invariants can be enforced this way.
|
|
|
|
Mere isomorphism for now, but will allow more invariants ultimately.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
|
|
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.
|
|
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.
|
|
Instead we do that on a by-need basis by reusing the section info already
stored in the opaque proof.
|
|
Reviewed-by: gares
Ack-by: maximedenes
|
|
We get rid of the future wrappers, as all callers are immediately forcing
the result.
|
|
Safe_typing is now responsible for hashconsing of all accessible structures,
except for opaque terms which are handled by Opaqueproof.
|
|
|
|
This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
|
|
|
