| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: mattam82
|
|
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.
|
|
|
|
primitive projection was wrongly supposed to be already inferred
Reviewed-by: gares
|
|
template poly
Reviewed-by: gares
Reviewed-by: herbelin
|
|
This is to make more explicit that arguments of the projection are not
kept.
We seize this opportunity to use QGlobRef equality on GlobRef.
|
|
type.
This was a case where expand_projections was calling find_mrectype
which was expecting the argument of the projection to be an inductive.
We could have ensured that this type is at least the appropriate
inductive applied to fresh evars, but this expand_projections was in
practice used for checking the applicability of canonical structures
and the unifiability of the parameters of the projections is anyway a
consequence of the unifiability of the principal argument of the
projections. So, the latter is enough.
|
|
locating fix
Reviewed-by: gares
|
|
Reviewed-by: gares
|
