| Age | Commit message (Collapse) | Author |
|---|
|
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!
|
|
|
|
|
|
|
|
Fixes [Coq bug #5372](https://coq.inria.fr/bugs/show_bug.cgi?id=5372)
"Anomaly: Not a valid information when defining mutual fixpoints that
are not mutual with Function".
|
|
|
|
|
|
|
|
|
|
|
|
I believe an unwanted shadowing was introduced by a4043608f704f0.
|
|
We try to address @silene 's concerns, which indeed are legitimate.
|
|
Following a suggestion by @ppedrot in #390, we require `Pp` clients to
be aware that they are using a "view" on the `std_ppcmds` type.
This is not extremely useful as people caring about the documents will
indeed have to follow changes in the view, but it costs little to play
on the safe side here for now.
We also introduce a more standard notation, `Pp.t` for the main type.
|
|
Format requires a top-level box to be present, this is similar to the
fix done in `Pp.string_of_ppcmds`.
|
|
Previous implementations of `Pp` flushed on newline, however,
depending on the formatter this may not be always the case.
We now alwayas flush the formatters before closing the file as this is
the intended behavior.
|
|
By default, we serialize messages to the "rich printing
representation" as it was done in 8.6, this ways clients don't have to
adapt unless they specifically request the new format using option
`--xml_format=Ppcmds`
|
|
This is a small, but convenient refactoring, as it will allow common
argument parsing.
|
|
In general we want to avoid this as much as we can, as it will need to
make choices regarding the output backend (width, etc...) and it is
expensive. It is better to serve the printing backends the pretty
print document itself.
|
|
- We avoid unnecessary use of Pp -> string conversion functions.
and the creation of intermediate buffers on logging.
- We rename local functions that share the name with the Coq stdlib,
this is usually dangerous as if the normal function is removed, code
may pick up the one in the stdlib, with different semantics.
|
|
Previously, tags were associated to terminal styles, which doesn't make
sense on terminal-free pretty printing scenarios.
This commit moves tag interpretation to the toplevel terminal handling
module `Topfmt`.
|
|
For legacy reasons, pretty printing required to provide a "tag"
interpretation function `pp_tag`. However such function was not of much
use as the backends (richpp and terminal) hooked at the `Format.tag`
level.
We thus remove this unused indirection layer and annotate expressions
with their `Format` tags.
This is a step towards moving the last bit of terminal code out of the
core system.
|
|
The IDE now gets core Coq's `std_ppcmds` document format which is
width-independent.
Thus, we follow [1] and make the `{proof,message}_view` object refresh
their contents when the container widget changes size (by listening to
GTK's `size_allocated` signal). The practical advantage is that now
CoqIDE always renders terms with the proper printing width set and
without a roundtrip to Coq.
This patch dispenses the need for the `printing width` option, which
could be removed altogether.
[1] http://stackoverflow.com/questions/40854571/change-gtksourceview-contents-on-resize/
|
|
We remove the "abstraction breaking" primitives and reduce the file to
the used fragment.
|
|
-> Candidate to be merge with the main feedback commit.
|
|
|
|
Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.
This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.
Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.
However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.
The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.
We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.
`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.
Thus, the new panorama is:
- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
to coqtop.
_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.
_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.
A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.
The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.
|
|
This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09
(the mllib dependencies that should be surely tweaked more).
The logic for `fatal_error` has no place in `CErrors`, this is
coqtop-specific code.
What is more, a libobject caller should handle the exception correctly,
I fail to see why the fix was needed on the first place.
|
|
|
|
|
|
We replace open/close box commands in favor of the create box ones.
|
|
We replace open/close tag commands by a well-balanced "tag" wrapper.
|
|
|
|
|
|
We also remove flushing operations `msg_with`, now the flushing
responsibility belong to the owner of the formatter.
|
|
Mostly unused, we ought to limit spacing in the boxes themselves.
|
|
This is what has always been used, so it doesn't represent a functional
change.
This is just a preliminary patch, but many more possibilities could be
done wrt tags.
|
|
Applications of it were not clear/unproven, it made printers more
complex (as they needed to be functors) and as it lacked examples it
confused some people.
The printers now tag unconditionally, it is up to the backends to
interpreted the tags.
Tagging (and indeed the notion of rich document) should be reworked in
a follow-up patch, so they are in sync, but this is a first step.
Tested, test-suite passes.
Notes:
- We remove the `Richprinter` module. It was only used in the
`annotate` IDE protocol call, its output was identical to the normal
printer (or even inconsistent if taggers were not kept manually in
sync).
- Note that Richpp didn't need a single change. In particular, its
main API entry point `Richpp.rich_pp` is not used by anyone.
|
|
The miscellaneous `msg_*` cleanup patches have finally enforced this
invariant.
|
|
We remove the custom logger handler in ide_slave, and handle everything
via feedback. This is an experimental patch but it seems to bring quite
a bit of cleanup and a more uniform handling to messaging.
|
|
|
|
|
|
|
|
|
|
(ProcThreeStInl.v, when the final "Defined" runs). I've verified that the
change here fixes the stack overflow there with Coq 8.5pl2.
In this version, all the recursive calls are in tail position. Instead of
taking a single list of instructions, `emit' here takes a curent list and a remaining
list of lists of instructions. That means the two calls elsewhere in the file now
add an empty list argument. The algorithm works on the current list until it's empty,
then works on the remaining lists. The most complex case is for Ksequence, where
one of the pieces becomes the new current list, and the other pieces are consed onto
the remaining sub-lists.
|
|
The `a.[i] <- x` notation is deprecated and we were getting a couple
of warnings.
|
|
The current future system is lazy when "chaining" (*) a resolved
future, which implies that chaining with a resolved future will produce
a non-resolved one.
This misfeature interacts badly with the "purification" optimization,
which in turn provokes a swarm of spurious state setting calls in real
use.
To solve this problem, we revert to the more natural semantics of
respecting the evaluation semantics when mapping over a future, indeed
respecting the previous resolution status.
This commit solves a kind of _critical_ bug in the current system,
with the particular bad path origination in `Future.split2` due to the
following accumulation of circumstances:
```
split2 x -> chain x (fun x -> fst x)
=>
let y = chain ~pure x (fun x -> fst x) in
if is_over x && greedy then ignore(force ~pure y);
y
=> [y <- Closure (fun x -> fst x)]
ignore(force (Closure (fun x -> fst x)))
=>
purify_future (force ~pure) (Closure (fun x -> fst x))
```
and then, the test in `purify_future` fails, triggering the
spurious state reset operation.
This problem was first noted at
https://sympa.inria.fr/sympa/arc/coqdev/2016-02/msg00081.html , and
seems related to https://coq.inria.fr/bugs/show_bug.cgi?id=5382
We fix the problem by making chaining eager, but other solutions would
be possible. Given that the main user of `chain` is `split2` which
does `snd/fst`, I recommend this solution.
The difference in calls to `unfreeze_state` is dramatic:
```
| File | Freeze Calls After | Freeze Calls Before |
|----------------------------------------+--------------------+---------------------|
| theories/Init/Notations.v | 0 | 0 |
| theories/Init/Logic.v | 57 | 614 |
| theories/Init/Datatypes.v | 13 | 132 |
| theories/Init/Logic_Type.v | 7 | 57 |
| theories/Init/Specif.v | 5 | 35 |
| theories/Init/Nat.v | 0 | 0 |
| theories/Init/Peano.v | 22 | 264 |
| theories/Init/Wf.v | 8 | 89 |
| theories/Init/Tactics.v | 2 | 24 |
| theories/Init/Tauto.v | 0 | 0 |
| theories/Init/Prelude.v | 0 | 0 |
| Bool/Bool.v | 104 | 1220 |
| Program/Basics.v | 0 | 0 |
| Classes/Init.v | 0 | 0 |
| Program/Tactics.v | 0 | 0 |
| Relations/Relation_Definitions.v | 0 | 0 |
| Classes/RelationClasses.v | 21 | 341 |
| Classes/Morphisms.v | 47 | 689 |
| Classes/CRelationClasses.v | 18 | 245 |
| Classes/CMorphisms.v | 50 | 587 |
| Classes/Morphisms_Prop.v | 3 | 127 |
| Classes/Equivalence.v | 6 | 105 |
| Classes/SetoidTactics.v | 0 | 0 |
| Setoids/Setoid.v | 4 | 33 |
| Structures/Equalities.v | 8 | 93 |
| Relations/Relation_Operators.v | 0 | 0 |
| Relations/Operators_Properties.v | 35 | 627 |
| Relations/Relations.v | 2 | 24 |
| Structures/Orders.v | 12 | 148 |
| Numbers/NumPrelude.v | 0 | 0 |
| Structures/OrdersTac.v | 13 | 234 |
| Structures/OrdersFacts.v | 73 | 931 |
| Structures/GenericMinMax.v | 82 | 1294 |
| Numbers/NatInt/NZAxioms.v | 0 | 0 |
| Numbers/NatInt/NZBase.v | 7 | 87 |
| Numbers/NatInt/NZAdd.v | 14 | 168 |
| Numbers/NatInt/NZMul.v | 12 | 144 |
| Logic/Decidable.v | 28 | 336 |
| Numbers/NatInt/NZOrder.v | 81 | 1174 |
| Numbers/NatInt/NZAddOrder.v | 24 | 288 |
| Numbers/NatInt/NZMulOrder.v | 46 | 552 |
| Numbers/NatInt/NZParity.v | 35 | 420 |
| Numbers/NatInt/NZPow.v | 29 | 348 |
| Numbers/NatInt/NZSqrt.v | 54 | 673 |
| Numbers/NatInt/NZLog.v | 64 | 797 |
| Numbers/NatInt/NZDiv.v | 49 | 588 |
| Numbers/NatInt/NZGcd.v | 36 | 432 |
| Numbers/NatInt/NZBits.v | 0 | 0 |
| Numbers/Natural/Abstract/NAxioms.v | 0 | 0 |
| Numbers/NatInt/NZProperties.v | 0 | 0 |
| Numbers/Natural/Abstract/NBase.v | 14 | 177 |
| Numbers/Natural/Abstract/NAdd.v | 6 | 72 |
| Numbers/Natural/Abstract/NOrder.v | 29 | 349 |
| Numbers/Natural/Abstract/NAddOrder.v | 5 | 60 |
| Numbers/Natural/Abstract/NMulOrder.v | 8 | 96 |
| Numbers/Natural/Abstract/NSub.v | 36 | 432 |
| Numbers/Natural/Abstract/NMaxMin.v | 18 | 216 |
| Numbers/Natural/Abstract/NParity.v | 4 | 48 |
| Numbers/Natural/Abstract/NPow.v | 26 | 312 |
| Numbers/Natural/Abstract/NSqrt.v | 9 | 108 |
| Numbers/Natural/Abstract/NLog.v | 0 | 0 |
| Numbers/Natural/Abstract/NDiv.v | 50 | 600 |
| Numbers/Natural/Abstract/NGcd.v | 14 | 168 |
| Numbers/Natural/Abstract/NLcm.v | 29 | 348 |
| Numbers/Natural/Abstract/NBits.v | 168 | 2016 |
| Numbers/Natural/Abstract/NProperties.v | 0 | 0 |
| Arith/PeanoNat.v | 77 | 990 |
| Arith/Le.v | 2 | 57 |
| Arith/Lt.v | 14 | 168 |
| Arith/Plus.v | 20 | 269 |
| Arith/Gt.v | 17 | 248 |
| Arith/Minus.v | 11 | 132 |
| Arith/Mult.v | 14 | 168 |
| Arith/Between.v | 19 | 299 |
| Logic/EqdepFacts.v | 26 | 539 |
| Logic/Eqdep_dec.v | 13 | 361 |
| Arith/Peano_dec.v | 3 | 26 |
| Arith/Compare_dec.v | 35 | 360 |
| Arith/Factorial.v | 3 | 36 |
| Arith/EqNat.v | 10 | 111 |
| Arith/Wf_nat.v | 18 | 173 |
| Arith/Arith_base.v | 0 | 0 |
| Numbers/BinNums.v | 0 | 0 |
| PArith/BinPosDef.v | 0 | 0 |
| PArith/BinPos.v | 229 | 2810 |
| NArith/BinNatDef.v | 0 | 0 |
| NArith/BinNat.v | 107 | 1330 |
| PArith/Pnat.v | 51 | 688 |
| NArith/Nnat.v | 30 | 360 |
| setoid_ring/Ring_theory.v | 43 | 756 |
| Lists/List.v | 195 | 2908 |
| setoid_ring/BinList.v | 6 | 90 |
| Numbers/Integer/Abstract/ZAxioms.v | 0 | 0 |
| Numbers/Integer/Abstract/ZBase.v | 3 | 36 |
| Numbers/Integer/Abstract/ZAdd.v | 46 | 552 |
| Numbers/Integer/Abstract/ZMul.v | 8 | 96 |
| Numbers/Integer/Abstract/ZLt.v | 21 | 252 |
| Numbers/Integer/Abstract/ZAddOrder.v | 45 | 543 |
| Numbers/Integer/Abstract/ZMulOrder.v | 24 | 288 |
| Numbers/Integer/Abstract/ZMaxMin.v | 22 | 264 |
| Numbers/Integer/Abstract/ZSgnAbs.v | 41 | 492 |
| Numbers/Integer/Abstract/ZParity.v | 6 | 72 |
| Numbers/Integer/Abstract/ZPow.v | 10 | 120 |
| Numbers/Integer/Abstract/ZDivTrunc.v | 68 | 816 |
| Numbers/Integer/Abstract/ZDivFloor.v | 70 | 840 |
| Numbers/Integer/Abstract/ZGcd.v | 29 | 348 |
| Numbers/Integer/Abstract/ZLcm.v | 50 | 600 |
| Numbers/Integer/Abstract/ZBits.v | 205 | 2460 |
| Numbers/Integer/Abstract/ZProperties.v | 0 | 0 |
| ZArith/BinIntDef.v | 0 | 0 |
| ZArith/BinInt.v | 212 | 2839 |
|----------------------------------------+--------------------+---------------------|
```
(*) I would call it `Future.map` better than chain.
|
