| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| | |
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
| |\ \
| |/
|/| |
|
| |\ \ |
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | | |
This should save a lot of useless reallocations and hashset crawling, which
end up costing a lot.
|
| |\ \ \ |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
As explained in edf85b9, the original commit that merged the module_body
and module_type_body representations, this was delayed to a later time
assumedly due to OCaml lack of GADTs. Actually, the only thing that was
needed was polymorphic recursion, which has been around already for a
relatively long time (since 3.12).
|
| |\ \ \ \
| |_|/ /
|/| | | |
|
| | |/ /
|/| |
| | |
| | | |
(from module List).
|
| | | | |
|
| |/ /
| |
| |
| |
| | |
Indeed OCaml has a similar file and this conflicts, at least in
debugger.
|
| |\ \ |
|
| | | | |
|
| | |/
| |
| |
| | |
It did not consider that the argument might be higher-order, e.g. [nat -> I].
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.
Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
|
| | |
| |
| |
| | |
This ought to ease the understanding of the code.
|
| | |
| |
| |
| | |
This was an easy to prove property that I somehow overlooked.
|
| | |
| |
| |
| |
| | |
This is actually useless, the code does not depend on the value of the
entry for side-effects.
|
| | |
| |
| |
| |
| |
| | |
Instead of relying on a mutable state in the object pushed on the libstack,
we export an API in the kernel that exports the side-effects of a given
entry in the global environment.
|
| | |
| |
| |
| |
| | |
We sprinkle a few GADTs in the kernel in order to statically ensure that
entries are pure, so that we get stronger invariants.
|
| | | |
|
| |/
|
|
|
| |
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We sort the dependency graph of API by following a logical declaration
order in `API.{ml,mli}` related to the actual dependency order of Coq
modules.
Things are a bit tricky here as Coq itself relies on the fact that
OCaml treats module interface and implementation separately
dependency-wise; however, when resorting module alias the design seems
to become more coupled.
Currently, API exposes both "namespaces", asserting a large number of
type equality between them, however the `API` namespace is not
self-contained.
In particular, this is a first step to solve problems such as
`Summary.frozen` being used in `API.mli` but not declared by the
`API.Summary` module, etc... In general we follow the invariant that a
type used in `API` must have been declared before.
Keep in mind that OCaml upstream has warned that it maybe tricky to
alias objects in this way. In particular, after API the old `mli` only
files have become full compilation units so we may want to be more
careful here.
The more "correct" declaration order allows us to remove the
`API.Prelude` module, as well as some other declarations that I
consider as spurious.
We still maintain the large number of type aliases which will be
removed in a future patch.
We follow linking order except for files in `intf`, which are
conceptually wrongly placed in the linking hierarchy but this doesn't
matter as the files don't contain any implementation.
We also move a couple of `.mli` only files to `.ml` so we are
consistent, and correct their linking order in `mllib`, even if that
doesn't matter as such `.ml`-only files contain no implementations.
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
The function turning a side-effect declaration into the corresponding
entry was crazily wrong, as it used a named universe context quantifying
over DeBruijn universe indices. Declaring such entries resulted
in random anomalies.
This fixes bug #5641.
|
| | |
| |
| |
| |
| | |
Before this patch, inductive subtyping was enforcing syntactic equality
of the variable instance, instead of reasoning up to alpha-renaming.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.
We also add a few tests for module subtyping in presence of polymorphic
constants.
|
| | |
| |
| |
| |
| |
| | |
Instead of returning either an instance or the set of constraints, we rather
return the corresponding abstracted context. We also push back all uses of
abstraction-breaking calls from these functions out of the kernel.
|
| | |
| |
| |
| |
| | |
This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
|
| | |
| |
| |
| |
| |
| | |
Global declarations used to carry universe instances with them, but it
turns out this information is not used anywhere. Instead, instances were
already properly encoded as the first argument of polymorphic definitions.
|
| |\ \ |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
This code was a sketch of what to do when we properly implement module-level
handling of instanciation of definitions by inductive types. It was completely
dead code, called after an error, and somewhat incorrect. Instead of letting
it bitrot, we remove it.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
These functions were messing with the deferred universe constraints in an
error-prone way, and were only used for printing as of today. We inline
the one used by the printer instead.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This was useless, because immediate constraints are assumed to already be in
the current environment, while deferred constraints are useless for the
conversion check of the definition types, as they only appear in the opaque
body.
This also clarifies a bit what is going on in the typing of module constraints
w.r.t. global universes.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
Only try using cumulativity in conversion/subtyping if the universe
instances are non-empty
|
| | | |
|
| | | |
|
| | | |
|
Maxime Dénès
Gaëtan Gilbert
Pierre-Marie Pédrot
Hugo Herbelin
Paul Steckler
Matej Košík
Matthieu Sozeau
Emilio Jesus Gallego Arias
Amin Timany