aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
* [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes.
* [location] Remove `Loc.internal_ghost`Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it.
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | Now it is a private field, locations are optional.
* [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
|
* [location] More located use.Gravatar Emilio Jesus Gallego Arias2017-04-24
|
* [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location.
* [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | | | | | | This is first of a series of patches, converting `constrexpr` pattern data type from ad-hoc location handling to `Loc.located`. Along Coq, we can find two different coding styles for handling objects with location information: one style uses `'a Loc.located`, whereas other data structures directly embed `Loc.t` in their constructors. Handling all located objects uniformly would be very convenient, and would allow optimizing certain cases, in particular making located smarter when there is no location information, as it is the case for all terms coming from the kernel. `git grep 'Loc.t \*'` gives an overview of the remaining work to do. We've also added an experimental API for `located` to the `Loc` module, `Loc.tag` should be used to add locations objects, making it explicit in the code when a "located" object is created.
* Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\
* | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| |
| * [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
|/ | | | | | | | | Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
* Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵Gravatar Maxime Dénès2017-04-12
|\ | | | | | | record fields.
* | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | | | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\ \
* | | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is the good parts of PR #360. IIUC, these vernacular were meant mostly for debugging and they are not supposed to be of any use these days. Back and join are still there not to break the testing infrastructure, but some day they should go away.
| * | Applying same convention as in Definition for parsing type in a let in.Gravatar Hugo Herbelin2017-03-24
| | |
| * | 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
|/ /
| * Supporting arbitrary binders in record fields, including e.g. patterns.Gravatar Hugo Herbelin2017-03-23
| |
| * Removing a redundant line in the syntax of record fields.Gravatar Hugo Herbelin2017-03-23
| |
| * Factorizing/unifying code in dealing with binders.Gravatar Hugo Herbelin2017-03-23
| | | | | | | | | | | | | | | | | | | | | | | | Note: This reveals a little bug yet to fix in g_vernac.ml4. In Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'. the "id" are wrongly unfolded and in Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop. an unexpected cast remains in the body of f.
| * Improving the API of constrexpr_ops.mli.Gravatar Hugo Herbelin2017-03-23
|/ | | | | | | | | | | | Deprecating abstract_constr_expr in favor of mkCLambdaN, prod_constr_expr in favor of mkCProdN. Note: They did not do exactly the same, the first ones were interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type, what I think is the correct thing to do. So, there is also a "fix" of semantic here.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
|\
* | [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | [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.
* | [safe-string] parsing/cLexerGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | | | | No functional change.
| * don't require printing-only notation to be productiveGravatar Ralf Jung2017-02-16
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\|
| * Fixing lexing of strings in comments for beautifier.Gravatar Hugo Herbelin2016-12-02
| | | | | | | | Was a bug introduced in 0ad6edc1.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\|
| * Fix #5174: Underinformative syntax error messages in the new arguments syntaxGravatar Maxime Dénès2016-11-30
| | | | | | | | | | We introduce a bit of compatibility parsing code to print deprecation warnings.
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Gravatar Maxime Dénès2016-11-18
| | | | | | | | | | | | | | | | | | This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration.
| * [stm] Remove STM-related vernacularsGravatar Emilio Jesus Gallego Arias2016-11-17
| | | | | | | | | | | | | | | | | | I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed.
| * Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ | | | | | | | | | Was PR#339: Documenting type class options, typeclasses eauto
| * | Removing obsolete parsing of strings à la v7 in comments.Gravatar Hugo Herbelin2016-11-05
| | | | | | | | | | | | This was for the translator and is not relevant for the beautifier.
| * | Merge remote-tracking branch 'github/pr/340' into v8.6Gravatar Maxime Dénès2016-11-03
| |\ \ | | | | | | | | | | | | Was PR#340: Fix various shortcomings of the warnings infrastructure.
| | | * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
| * | | Better Arguments compatibility.Gravatar Maxime Dénès2016-11-02
| | |/ | |/| | | | | | | | | | With multiple arguments list, repeating the "/" modifier used to be mandatory. So instead of forbidding it, we issue a deprecation warning.
| | * Fix various shortcomings of the warnings infrastructure.Gravatar Maxime Dénès2016-11-02
| |/ | | | | | | | | | | | | | | | | | | | | | | | | - The flags are now interpreted from left to right, without any other precedence rule. The previous one did not make much sense in interactive mode. - Set Warnings and Set Warnings Append are now synonyms, and have the "append" semantics, which is the most natural one for warnings. - Warnings on unknown warnings are now printed only once (previously the would be repeated on further calls to Set Warnings, sections closing, module requiring...). - Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced to "-foo" (if foo exists, "" otherwise).
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ | | | | | | | | | Was PR#319: More error tagging, try to fix bug 5135
| * \ Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
| |\ \ | | | | | | | | | | | | Was PR#337: Fix arguments
| | * | Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add *a lot* of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | |
| * | | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-24
| | | | | | | | | | | | | | | | + a few improvements on 5f1dd4c40 (lexing of { and }).
| * | | Adding a primitive to recover the set of keywords from the lexer.Gravatar Pierre-Marie Pédrot2016-10-21
| | | | | | | | | | | | | | | | This is useful for debugging purposes.