aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2020-11-20A step towards supporting pattern cast deeplier.Hugo Herbelin
We at least support a cast at the top of patterns in notations.
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
We introduce a class of open binders which includes "x", "x:t", "'pat" and a class of closed binders which includes "x", "(x:t)", "'pat".
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵Hugo Herbelin
deprecated.
2020-10-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-10-10Adding and using locations on identifiers in constr_expr where they were ↵Hugo Herbelin
missing.
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended.
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-27Avoid lookup up too many characters.Guillaume Melquiond
This would cause issues in noninteractive mode. For example, when using Drop, the first character of the OCaml code would be read by Coq's REPL instead of OCaml's REPL. The peek_string function is quite inefficient, since the Stream module does not provide any good function to lookup arbitrary characters (or to push back characters).
2020-09-27Make "xxx:{{" always start a quotation, whether registered or not.Guillaume Melquiond
This commit also prevents quotations using "(" and "[" from gobbling sentences. As a consequence, dynamically-registered quotations can no longer modify where Coq sentences stop.
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-09-11[parsing] Simplify bigintPierre Roux
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-08-25Moving production_level_eq to extend.ml for separation of concerns.Hugo Herbelin
Add a mli file and uniformize indentation on the way.
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2020-05-09Add a `with_strategy` tacticJason Gross
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g., `Opaque foo` doesn't break some automation which tries to unfold `foo`. We have some timeouts in the strategy success file. We should not run into issues, because we are not really testing how long these take. We could just as well use `Timeout 60` or longer, we just want to make sure the file dies more quickly rather than taking over 10^100 steps. Note that this tactic does not play well with `abstract`; I have a potentially controversial change that fixes this issue. One of the lines in the doc comes from https://github.com/coq/coq/pull/12129#issuecomment-619771556 Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr> Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr> Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
2020-05-06Stop keeping outdated static list of keywords.Hugo Herbelin
The real list is computed by tok_using in CLexer.
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[parsing] Move comments lexer extensions to base lexer interfaceEmilio Jesus Gallego Arias
This makes sense as a step towards a more functional handling of the state.
2020-03-25[gramlib] Remove warning function parameter in favor of standard mechanism.Emilio Jesus Gallego Arias
If we need more fine-tuning we should manage the warnings with the standard Coq mechanism.
2020-03-25[parsing] Move `coq_parsable` custom logic to Grammar.Emilio Jesus Gallego Arias
Latest refactorings allow us to make the signature Coq parser a standard `Grammar.S` one; the only bit needed is to provide the extra capabilities to the `Lexer` signature w.r.t. to comments state. The handling of Lexer state is still a bit ad-hoc, in particular it is global whereas it should be fully attached to the parsable. This may work ok in batch mode but the current behavior may be buggy in the interactive context. This PR doesn't solve that but it is a step towards a more functional solution.
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio Jesus Gallego Arias
There is not need to re-export Gramlib's API in a non-structured way anymore. We thus expose the core Gramlib interface to users and remove redundant functions. A question about whether to move more parts of the API to `Gramlib` is still open, as well as on naming.
2020-03-25[parsing] Remove unneeded `Extend.entry` type.Emilio Jesus Gallego Arias
This is not needed anymore after the unification.
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
We remove Coq's wrapper over gramlib's grammar constructors.
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's.
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's.
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-22Adding bignat to parse positive numbers; bigint now includes negative ints.Hugo Herbelin
Warning: in notations, the name "bigint" actually meant "bignat". A clarification will eventually be needed.
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-17Dead code in g_prim.mlgHugo Herbelin
2020-03-13Merge PR #11688: When parsing a negative integer, ensure that the minus sign ↵Emilio Jesus Gallego Arias
is contiguous to the number. Reviewed-by: ejgallego
2020-03-08Merge PR #11714: [gramlib] Refactor gramlib interface.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
We make the primitives for backtrace-enriched exceptions canonical in the `Exninfo` module, deprecating all other aliases. At some point dependencies between `CErrors` and `Exninfo` were a bit complex, after recent clean-ups the roles seem much clearer so we can have a single place for `iraise` and `capture`.
2020-03-03When parsing negative integer, ensure minus sign is contiguous to the number.Hugo Herbelin
For instance, formerly, "Set Inline Level - 1" was succeeding. Now only "Set Inline Level -1" succeeds. (Even though -1 does not make sense for a Inline Level, but that's then a semantic issue. Other options may accept negative numbers in general.)
2020-03-01[parser] lk_int -> lk_natMaxime Dénès
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2020-03-01Move lookahead combinators to PcoqMaxime Dénès
They were in Ltac2, but they are of general interest
2020-02-28[gramlib] Refactor gramlib interface.Emilio Jesus Gallego Arias
This is in preparation for making the Gramlib interface the canonical one; see #11647 . I tried to implement some of the ideas that were floated around in a chat with Pierre-Marie, suggestions / comments are welcome.
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-02-23Cancelling precedences in Set Printing Parentheses only at border of notations.Hugo Herbelin
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 15:20:37 +0000