aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
...
* | Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | For compatibility, the default is to parse as ident and not as pattern.
* | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}.
* | Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | - Avoid dummy use of unit - Do not decide as early as parsing the default level for pattern - Prepare to further extensions
* | Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | Renaming it register_grammars_by_name.
* | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms.
* | Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"...
* | Renaming binders into binderlists in egramcoq.ml.Gravatar Hugo Herbelin2018-02-20
| |
* | Introducing an intermediary type "constr_prod_entry_key" for grammar ↵Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | productions. This type describes the grammar non-terminal. It typically contains ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is the type for metasyntax.ml and egramcoq.ml to communicate together. The type constr_prod_entry_key with ETConstr, ETBinder, is now used only in metasyntax.ml. This allows to get rid of some "assert false" in uselessly matching over ETConstrList in metasyntax.ml and of some "assert false" in uselessly matching over ETBinder in egramcoq.ml. Also exporting less of extend.mli in API.
* | Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Gravatar Hugo Herbelin2018-02-20
|/
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | longer use camlp4.
* [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
|
* [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
|
* [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
|
* Merge PR #6433: [flags] Move global time flag into an attribute.Gravatar Maxime Dénès2017-12-29
|\
* | [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | | | | | | | | | | | | | Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
| * [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
|/ | | | One less global flag.
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
| | | | | | | | | | | | Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
* Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵Gravatar Maxime Dénès2017-12-14
|\ | | | | | | same right-hand side.
| * Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
| | | | | | | | This is to have a better symmetry between CCases and GCases.
* | [summary] Allow typed projections from global state + rework of internals.Gravatar Emilio Jesus Gallego Arias2017-12-09
|/ | | | | | | | | | | | | | | | | | | In the transition towards a less global state handling we have the necessity of mix imperative setting [notably for the modules/section code] and functional handling of state [notably in the STM]. In that scenario, it is very convenient to have typed access to the Coq's `summary`. Thus, I reify the API to support typed access to the `summary`, and implement such access in a couple of convenient places. We also update some internal datatypes to simplify the `frozen` data type. We also remove the use of hashes as it doesn't really make things faster, and most operations are now over `Maps` anyways. I believe this goes in line with recent work by @ppedrot. We also deprecate the non-typed accessors, which were only supposed to be used in the STM, which is now ported to the finer primitives.
* Proper nametab handling of global universe namesGravatar Matthieu Sozeau2017-12-01
| | | | | | | | They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced
* Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| | | | | | | | | | We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
* Merge PR #6253: Fixing inconsistent associativity of level 10 in the table ↵Gravatar Maxime Dénès2017-11-29
|\ | | | | | | of levels
| * A cosmetic standardization: adding a space in g_constr.ml4.Gravatar Hugo Herbelin2017-11-27
| |
| * Releasing level "11" of "pattern".Gravatar Hugo Herbelin2017-11-27
| | | | | | | | | | | | Was introduced in 0917ce7c to fix #4272, but it seems that we can fix it by just merging levels 10 and 11. This prevents the worry of fixing the associativity of level 11 to left in 0917ce7c.
| * Fixing associativity registered for level 10.Gravatar Hugo Herbelin2017-11-27
| | | | | | | | | | | | Apparently a long-standing bug, coupled with a pattern/constr associativity inconsistency introduced while fixing another pattern/constr level inconsistency (bug #4272, 0917ce7c).
* | Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
|/
* Merge PR #6167: Fixing factorization of recursive notations with an atomic ↵Gravatar Maxime Dénès2017-11-23
|\ | | | | | | separator
* \ Merge PR #6200: Remove pidentref grammar entry.Gravatar Maxime Dénès2017-11-23
|\ \
| | * Fixing factorization of recursive notations in the case of an atomic separator.Gravatar Hugo Herbelin2017-11-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This addresses a limitation found in math-comp seq.v file. See the example in test suite file success/Notations2.v. To go further and accept recursive notations with a separator made of several tokens, and assuming camlp5 unchanged, one would need to declare an auxiliary entry for this sequence of tokens and use it as an "atomic" (non-terminal) separator. See PR #6167 for details.
| * | Remove pidentref grammar entry.Gravatar Gaëtan Gilbert2017-11-20
| |/ | | | | | | Replaced by ident_decl in #688.
* / [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
|/ | | | | | | | | | | | | Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`.
* Fix FIXME: use OCaml 4.02 generative functors when available.Gravatar Gaëtan Gilbert2017-11-01
| | | | 4.02.3 has been the minimal OCaml version for a while now.
* Parse [Proof using Type] without translating Type to an id.Gravatar Gaëtan Gilbert2017-10-10
|
* [vernac] Remove "Proof using" hacks from parser.Gravatar Emilio Jesus Gallego Arias2017-10-10
| | | | | | | | | We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.
* Merge PR #1114: Generic handling of nameable objects for pluginsGravatar Maxime Dénès2017-10-09
|\
* \ Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵Gravatar Maxime Dénès2017-10-06
|\ \ | | | | | | | | | "_something")
| * | Distinguishing pseudo-letters out of the set of unicode letters.Gravatar Hugo Herbelin2017-10-05
| | | | | | | | | | | | | | | This includes _ and insecable space which can be used in idents and this allows more precise heuristics.
| | * Implementing a generic mechanism for locating named objects from Coq side.Gravatar Pierre-Marie Pédrot2017-10-03
| |/ |/|
* | Merge PR #1094: Fixing a little parsing bug with level 90 introduced in ↵Gravatar Maxime Dénès2017-10-03
|\ \ | | | | | | | | | 3e70ea9c.
* \ \ Merge PR #1040: Efficient fresh name generationGravatar Maxime Dénès2017-10-03
|\ \ \
* | | | [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| |_|/ |/| | | | | | | | | | | | | | | | | We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
| * | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/ / | | | | | | | | The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
* | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \
| | * Fixing a little parsing bug with level 90 introduced in 3e70ea9c.Gravatar Hugo Herbelin2017-09-25
| |/ |/| | | | | | | | | | | | | Unfortunately, some manual synchronization is needed between the constr parser and the table of constr/pattern levels. We do this synchronization which was missing in the commit moving "x -> y" to a user-level notation.
* | Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
| |
| * Allow declaring universe binders with no constraints with @{|}Gravatar Gaëtan Gilbert2017-09-19
| |
| * Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
| * Allow empty instance parsing @{}Gravatar Matthieu Sozeau2017-09-19
|/
* Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Gravatar Maxime Dénès2017-09-15
|\ | | | | | | top of the linking chain.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 04:46:26 +0000