aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.
* Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | RawLocal -> CLocal
* Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | | | This is a bit long, but it is to keep a symmetry with constr_expr.
* "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|
* Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Gravatar Maxime Dénès2017-03-23
| | | | | This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit.
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\
| * Merge PR#495: funind: Ignore missing info for current functionGravatar Maxime Dénès2017-03-23
| |\
| * | Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | | | | | | This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.
* | | Mark ring morphisms as opaque.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
* | | Fix broken evaluation strategies for ring and field.Gravatar Guillaume Melquiond2017-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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!
* | | Remove duplicate lemmas.Gravatar Guillaume Melquiond2017-03-22
| | |
| | * funind: Ignore missing info for current functionGravatar Tej Chajed2017-03-22
| |/ | | | | | | | | | | 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".
* | [extraction] Flush formatters at end of output.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | 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.
* | [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | 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`.
* | [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | [pp] Force well-formed boxes by construction.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | We replace open/close box commands in favor of the create box ones.
* | [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter.
* | [pp] Remove `Pp.stras`.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | Mostly unused, we ought to limit spacing in the boxes themselves.
* | [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | 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.
* | [pp] Remove unused printing tagging infrastructure.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Merge PR#134: Enable `-safe-string`Gravatar Maxime Dénès2017-03-21
|\ \
* \ \ Merge PR#428: Report missing tactic arguments in error messageGravatar Maxime Dénès2017-03-17
|\ \ \
* \ \ \ Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-03-17
|\ \ \ \
* | | | | Attempt to improve error message when "apply in" fail.Gravatar Hugo Herbelin2017-03-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390.
| | | * | [safe-string] plugins/extractionGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | | | | | | | | | | | | | No functional change.
| | | * | [safe-string] ltac/profile_ltacGravatar Emilio Jesus Gallego Arias2017-03-14
| |_|/ / |/| | | | | | | | | | | | | | | No functional change, one extra copy introduced but it seems hard to avoid.
| | * | Report missing tactic arguments in error messageGravatar Tej Chajed2017-03-14
| |/ / |/| | | | | | | | | | | | | | Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
* | | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunGravatar Maxime Dénès2017-03-14
|\ \ \
* | | | Micromega: removing a constant preventing micromega to be loaded before Logic.v.Gravatar Hugo Herbelin2017-03-09
| | | | | | | | | | | | | | | | The constant was useless after 9f56baf which fixed #5073.
| | | * [ltac] Move dummy plugin to plugins folder.Gravatar Emilio Jesus Gallego Arias2017-03-03
| | | | | | | | | | | | | | | | This is needed to fix `Declare ML Module "ltac_plugin".
* | | | Merge PR#395: Allow hintdb to be parameters in a Ltac definition orGravatar Maxime Dénès2017-02-27
|\ \ \ \ | | | | | | | | | | | | | | | Tactic Notation
| | | * | TACTIC EXTEND now takes an optional level as argument.Gravatar Maxime Dénès2017-02-24
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The syntax is: TACTIC EXTEND foo AT LEVEL i This commit makes it possible to define tacticals like the ssreflect arrow without having to resort to GEXTEND statements and intepretation hacks. Note that it simply makes accessible through the ML interface what Tactic Notation already supports: Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
* | | | Revert "Add empty ltac_plugin file for forward compatibility."Gravatar Maxime Dénès2017-02-24
| | | | | | | | | | | | | | | | | | | | This reverts commit e8137ae63b3b19436755f372b595e7343e942894, was meant for 8.6 branch only.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
|\ \ \ \ | | |_|/ | |/| |
* | | | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
* | | | Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
| | | * [cleanup] Change Id.t option to Name.t in TacFunGravatar Tej Chajed2017-02-16
| |_|/ |/| |
* | | Merge PR#393: Replace Typeops with Fast_typeopsGravatar Maxime Dénès2017-02-08
|\ \ \
* | | | Revert "Extraction: avoid deprecated functions of module String"Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
* | | | Extraction cosmetic: no whitespaces in printing empty modulesGravatar Pierre Letouzey2017-02-07
| | | |
* | | | Extraction: remove the "print to devnull" hack now that pp isn't lazy anymoreGravatar Pierre Letouzey2017-02-07
| | | |
* | | | Extraction: avoid deprecated functions of module StringGravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | - A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co
* | | | Extraction: simplify the generated code for difficult name conflictsGravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | No more pp_alias_spec et pp_alias_decl. Instead, we use "include" and "module type of". The extracted code might hence need OCaml 3.12 (quite rarely)
* | | | Extraction : get_duplicates (via option) instead of check_duplicates (via ↵Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | Not_found) This clarifies the execution flow
* | | | Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017...
| | * Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017...
| * | Remove useless commentsGravatar Gaetan Gilbert2017-01-28
| | |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-01-19
|\ \ \ | | |/ | |/|
| | * Extend Fast_typeops to be a replacement for TypeopsGravatar Gaetan Gilbert2016-12-12
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This brings the fix in cad44fc for #2996 to the copy of Fast_typeops.check_hyps_inclusion. Fast_typeops.constant_type checks the universe constraints instead of outputting them. Since everyone who used Typeops.constant_type just discarded the constraints they've been switched to constant_type_in which should be the same in Fast_typeops and Typeops. There are some small differences in the interfaces: - Typeops.type_of_projection <-> Fast_typeops.type_of_projection_constant to avoid collision with the internally used type_of_projection (which gives the type of [Proj(p,c)]). - check_hyps_inclusion takes [('a -> constr)] and ['a] instead of [constr] for reporting errors.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 03:36:35 +0000