| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Also works for simpl.
|
|
MAKEPROD is just MAKEBLOCK2(0), but one word shorter. Since this opcode is
never encountered in the fast path, this optimization is not worth the
extra complexity.
|
|
The generated bytecode almost never needs to modify the field of an OCaml
object. The only exception is the laziness mechanism of coinductive types.
But it modifies field 2, and thus uses the generic opcode SETFIELD anyway.
|
|
The PUSHFIELDS opcode is a costly one, yet lots of constructors have at
most one usable argument (e.g., option, nat, positive, Z, Acc). For those
constructors, PUSHFIELDS(1) is replaced by GETFIELD(0);PUSH, assuming
the accu register is no longer used afterwards.
Replacing one single opcode by two opcodes might seem like a
pessimization, but it is not. Indeed, pattern-matching branches usually
start by filling the accu register with a constructor argument or the
value of a free variable or a constant. All of those offer peephole
optimizations for PUSH, which means that the number of opcodes actually
stay constant.
Note that, for the same reason, the assumption above holds in practice:
the accu register is no longer used after PUSHFIELDS.
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
We expose the representation function in UGraph and change the printer
signature to work over the representation instead of the abstract type.
Similarly, the topological sorting algorithm is moved to Vernacentries.
It is now even simpler.
|
|
Instead we export a representation function that gives a high-level view
of the data structure in terms of constraints.
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
We need this file for the upcoming kernel representation change there.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
notations.
Reviewed-by: jfehrle
Reviewed-by: proux01
Ack-by: Zimmi48
Ack-by: SkySkimmer
|
|
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
|
|
|
|
|
|
|
|
We use a variant of skewed lists enriched over a monoid, whose purpose is
to count the number of lifts added to the substitution. This makes addition
O(1) and lookup O(log n).
|
|
|
|
- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API)
- the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors
- Grants #13484: String notations for primitive arrays
- Fixes #13517: String notation printing fails with primitive integers inside lists
|
|
They are not used there, and removing the redundance of the the case
representation requires access to the environment, so we push their use
further up.
|
|
This is presumably not usable from the surface language. But an ML module
could easily create a proof of false by passing a negative number to
Const.mkInt.
|
|
|
|
Before this commit, function mask63 was called implicitly at each step.
|
|
|
|
|
|
of cases.
|
|
cumulative inductive types
Reviewed-by: SkySkimmer
|
|
types
|
|
|
|
|
|
This is just an experiment, but makes the uses of the API easier as we
don't mess with the global state anymore.
|
|
This allows proper treatment in notations, ie fixes #13303
The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).
This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:
~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~
When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.
Extern has a symmetrical problem:
~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)
Therefore extern also takes a universe binders argument.
Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)
As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.
Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
The Norm name was confusing enough to have introduced a few kernel
bugs, so it deserved to be changed as suggested in #13274.
Contrarily to what it seemingly meant, it was actually standing
for neutral terms rather than normal ones. I have kept the 4-letter
naming scheme for simplicity and renamed it into Ntrl.
|
|
Accumulators can grow arbitrarily large, even when well-typed. So, this
commit makes sure they are allocated on the major heap when they are too
large. If so, fields need to be filled with caml_initialize, in case they
point to the minor heap.
|
|
Ack-by: ppedrot
Reviewed-by: proux01
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
|
