| Age | Commit message (Collapse) | Author |
|---|
|
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).
|
|
|
|
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.
|
|
|
|
cleanup of constrintern.ml
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
|
|
Namely, WrongNumargInductive and WrongNumargConstructor.
|
|
We also simplify the whole process of interpretation of cases pattern
on the way.
|
|
|
|
constants/inductives/constructors
Reviewed-by: SkySkimmer
|
|
Reviewed-by: mattam82
|
|
|
|
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.
|
|
|
|
To tie the knot (since the evar depends on the evar type and the
source of the evar type of the evar), we use an "update_source"
function.
An alternative could be to provide a function to build both an evar
with its evar type directly in evd.ml...
|
|
erroneously caught
Reviewed-by: ppedrot
|
|
Fixes #7430 and fixes #10968
This commit makes the following changes:
- Add an exception `Signal` used to convert OCaml signals to exceptions.
`Signal` is registered as critical in `CErrors` to avoid being caught in the
wrong `with` clauses.
- Make `Control.timeout` into a safer interface based on `option` instead of
exceptions.
- Modify `tclTIMEOUT` to fail with `CErrors.Timeout` instead of
`Logic_monad.Tac_timeout`, as was already advertised in the ocamldoc documentation.
- Removes `Logic_monad.Tac_timeout` altogether because it no longer has a use.
|
|
|
|
semantic.
|
|
|
|
|
|
Also includes minor layout or code changes.
|
|
We also align their type on (more) standard invariants.
|
