| Age | Commit message (Collapse) | Author |
|---|
|
For now we only normalize sorts, and we leave instances for the next
commit.
|
|
|
|
The kernel does fishy things with casts, such that ensuring there are no
two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr
view as well.
|
|
This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance
difference was not conclusive enough to pay for the code ugliness.
|
|
We do one step of loop unrolling, limit the number of allocations and
mark the function as inline.
|
|
|
|
This broke the build of iris-coq in the EConstr branch. Each time you
use unsafe_type_of, I loose a night of sleep, so please stop.
|
|
Was breaking e.g. fiat-crypto.
|
|
This is while waiting for a possible different solution, if ever such
a different solution is adopted, since the coq.inria.fr/library has
currently a broken link and someone rightly complained about it.
|
|
|
|
After 5db9588098f9f, some extra evar-normalization remained (compared to trunk)
that would change the semantics e.g. of change bindings under Ltac match.
This is just circumventing a fundamental flaw in the treatment of patterns.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We were doing fishy things in the Term_typing file, where side-effects were
not considered in the right uniquization order because of the uniq_seff_rev
function. It probably did not matter after a9b76df because effects were
(mostly) uniquize upfront, but this is not clear because of the use of the
transparente API in the module.
Now everything has to go through the opaque API, so that a proper dependence
order is ensured.
|
|
We move it from Entries to Term_typing and export the few functions needed
to manipulate it in this module.
|
|
Fixes Coq bug 5345 (https://coq.inria.fr/bugs/show_bug.cgi?id=5345):
Cannot use names bound in matches inside Ltac definitions.
|
|
|
|
|
|
|
|
This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is
an 8.6 only commit.
|
|
|
|
|
|
This way, after we merge PR#220, scripts can be fixed in a way that is
compatible with the 8.6 and trunk branches.
|
|
|
|
This makes sense for clients willing to link to richpp.
|
|
|
|
|
|
|
|
|
|
This adds at least support for camlp5 6.14 (in addition to 6.17).
|
|
We need to do a bit of hacking, but it should be fine for the short
term.
c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83
|
|
|
|
There are now two field structures for R: one in RealField and one in
RIneq. The first one is used to prove that IZR is a morphism which is
needed to define the second one.
|
|
This prevents Coq from unfolding IZR in ring_simplify and field_simplify.
This is a change of behavior for users of morphism rings, so they might have
to pass the postprocess option to Add Ring/Field if they want morphisms to be
automatically expanded.
There are two predefined morphisms in the standard library: IDphi (when
polynomial coefficients have the same type as constants) and gen_phiZ (when
the only available constants are 0 and 1). They are hardcoded as transparent.
|
|
There are two main issues. First, (-cst)%R is no longer syntactically
equal to (-(cst))%R (though they are still convertible). This breaks some
rewriting rules.
Second, the ring/field_simplify tactics did not know how to refold
real constants. This defect is no longer hidden by the pretty-printer,
which makes these tactics almost unusable on goals containing large
constants.
This commit also modifies the ring/field tactics so that real constant
reification is now constant time rather than linear.
Note that there is now a bit of code duplication between z_syntax and
r_syntax. This should be fixed once plugin interdependencies are supported.
Ideally the r_syntax plugin should just disappear by declaring IZR as a
coercion. Unfortunately the coercion mechanism is not powerful enough yet,
be it for parsing (need the ability for a scope to delegate constant
parsing to another scope) or printing (too many visible coercions left).
|
|
|
|
That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not
convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means
that, after reduction, real constants no longer exponentially blow up.
Note that I was not able to fix the test-suite for the declarative mode,
so the missing proof terms have been admitted.
|
|
A bang indicates an argument that must be reduced, a star indicates an
argument that must be handled recursively.
PEeval: R r0 r1 add mul sub opp C phi Cpow powphi pow varmap pol
0 1 2 3 4 5 6 7 8! 9 10! 11 12* 13!
FEeval: R r0 r1 add mul sub opp div inv C phi Cpow powphi pow varmap pol
0 1 2 3 4 5 6 7 8 9 10! 11 12! 13 14* 15!
Pphi_dev: R r0 r1 add mul sub opp C c0 c1 ceq phi sign varmap pol
0 1 2 3 4 5 6 7 8! 9! 10! 11! 12! 13* 14!
Pphi_pow: R r0 r1 add mul sub opp C c0 c1 ceq phi Cpow powphi pow sign varmap pol
0 1 2 3 4 5 6 7 8! 9! 10! 11! 12 13! 14 15! 16* 17!
display_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi sign varmap num den
0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13! 14* 15! 16!
display_pow_linear: R r0 r1 add mul sub opp div C c0 c1 ceq phi Cpow powphi pow sign varmap num den
0 1 2 3 4 5 6 7 8 9! 10!11! 12! 13 14! 15 16! 17* 18! 19!
PCond: R r0 r1 add mul sub opp eq C phi Cpow powphi pow varmap pol
0 1 2 3 4 5 6 7 8 9! 10 11! 12 13* 14!
|
|
|
