| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego
|
|
`coe_source` and `coe_target` fields of type `cl_typ` have been added to
`coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a
coercion. The `coercion` record has also been replaced with `coe_info_typ`.
|
|
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: gares
Ack-by: LasseBlaauwbroek
Ack-by: silene
Ack-by: vbgl
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
raised.
Reviewed-by: jfehrle
|
|
|
|
native_compute is called.
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
called (fix #13849).
The libraries are eventually linked in native_norm and native_conv_gen,
just before mk_norm_code and mk_conv_code are called.
This commit also renames call_linker as execute_library to better reflect
its role. It also makes link_library independent from it, since their
error handling are completely opposite.
|
|
|
|
|
|
Otherwise, the interpreter sees already unified evars as accumulators
rather than actual constants, thus preventing the computations from
progressing.
This was caused by 6b61b63bb8626827708024cbea1312a703a54124, which removed
evar normalization. The effect went unnoticed because the computed term is
still convertible to the reduced term, except that it is the lazy
machinery that ends up reducing it, rather than the bytecode one.
So, performances became abysmal, seemingly at random.
|
|
Reviewed-by: ppedrot
|
|
Towards #5154 (but insufficient)
|
|
Reviewed-by: ppedrot
|
|
|
|
Instead of storing the bare fixpoint and its unfolded body in the term,
incurring a cost for their lifts under contexts, we simply store them
in the side map used to track the relation between a fresh problem evar
and its minimal arity. We also replace the hacky evarmap used to track
instantiation with a mere set.
|
|
|
|
|
|
Reviewed-by: mattam82
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
|
|
We know statically that whd_betaiota is a local reduction function, so it
does not need to access the rel_context of its environment argument.
|
|
|
|
This also allows to move the strong variant of cbn to the Cbn module.
|
|
Also works for simpl.
|
|
|
|
|
|
|
|
It is equivalent but makes the code more similar to the PCase vs. Case case (aha).
|
|
|
|
This partially fixes #13732 and matches what we do in detype_sort
|
|
The infamous whd_betaiota_deltazeta_for_iota_state function is critical for
unification, and it seems that eagerly reducing let-bindings appearing in
case branches was a bad idea for efficiency. Instead, when try to preserve
the old behaviour where a dummy beta-let cut was introduced.
|
|
Since we have eta-expansion guaranteed by the term representation, we do
not have any more to do a little dance to try to recognize eta-expanded
branches and return predicate.
Still not able to compile the elpi test, but a good step towards it.
|
|
|
|
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.
|
|
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.
|
|
|
|
Reviewed-by: gares
|
|
Reviewed-by: mattam82
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
tactics.
Reviewed-by: ppedrot
|
|
projection expansion.
Reviewed-by: ejgallego
|
|
We additionally check that occurrence 0 is invalid in simpl at,
unfold at, etc.
|
|
No need to call the whole whd_gen machinery when a simple matching over
a term would suffice.
Note that this changes a bit the semantics, but I suspect that the previous
code was buggy. Indeed, whd_nored also pushes cases and fixpoints on the
stack, so that an applied canonical projection inside such a context would
also match. But the caller in unification performs an approximate check where
the term needs to be an application or a projection, which would prevent
such complex situations most of the time, e.g. it would work with a dummy
commutative cut but not their corresponding vanilla match.
|
|
There functions export the internal stack representation. The only real user
is unification, which is suffering from major performance issues due to the
naive representation of substitutions in processes.
|
|
|
|
This was revealed on the rewriter contrib with the compact-case-repr branch.
|
