aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
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-11-16Using labels to document match_notation_constr.Hugo Herbelin
2020-11-16Fix #9569 (notations collect the spine binding variables at printing time).Hugo Herbelin
This allows to know which global references whose basename may be unexpectedly caught need to be qualified. Note: the alternative strategy, which is sometimes used, of renaming the binding variables so as to avoid collisions with the basename of a global reference is somehow less nice.
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-20Merge PR #13180: Respect Print Universes when printing primitive arrayscoqbot-app[bot]
Reviewed-by: herbelin
2020-10-13Merge PR #13099: Locating pattern identifiers (?id) by default at parsing ↵Pierre-Marie Pédrot
time and use location in some typing error messages Reviewed-by: ppedrot
2020-10-12Respect Print Universes when printing primitive arraysGaëtan Gilbert
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
The (old) original model for notations was to associated both a parsing and a printing rule to a notation. Progressively, it become more and more common to have only parsing notations or even multiple expressions printed with the same notation. The new model is to attach to a given scope, string and entry at most one either only-parsing or mixed-parsing-printing rules + an arbitrarily many unrelated only-printing rules. Additionally, we anticipate the ability to selectively activate/deactivate each of those. This allows to fix in particular #9682 but also to have more-to-the-point warnings in case a notation overrides or partially overrides another one. Rules for importing are not changed (see forthcoming #12984 though). We also improve the output of "Print Scopes" so that it adds when a notation is only-parsing, only-printing, or deactivated, or a combination of those. Fixes #4738 Fixes #9682 Fixes part 2 of #12908 Fixes #13112
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-08-25The body of a let is considered to be "in context" if its type is present.Hugo Herbelin
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-08-25Propagate in-context information for extra arguments of notations too.Hugo Herbelin
2020-08-25Dead code in adjust_implicit_arguments.Hugo Herbelin
2020-07-12Fixes #12682 (recursive notation printing bug with n-ary applications).Hugo Herbelin
A special case for recursive n-ary applications was missing when the head of the application was a reference.
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-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-15Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with ↵Emilio Jesus Gallego Arias
implicit types Reviewed-by: ejgallego
2020-05-14Fixes #12322 (anomaly when printing "fun" binders with implicit types).Hugo Herbelin
A pattern-matching clause was missing in 5f314036e4d (PR #11261). The anomaly triggered in configurations like "fun (x:T) y => ..." (even in the absence of "Implicit Types").
2020-05-09Add hexadecimal numeralsPierre Roux
We add hexadecimal numerals according to the following regexp 0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)? This is unfortunately a rather large commit. I suggest reading it in the following order: * test-suite/output/ZSyntax.{v,out} new test * test-suite/output/Int63Syntax.{v,out} '' * test-suite/output/QArithSyntax.{v,out} '' * test-suite/output/RealSyntax.{v,out} '' * test-suite/output/FloatSyntax.{v,out} '' * interp/numTok.ml{i,} extending numeral tokens * theories/Init/Hexadecimal.v adaptation of Decimal.v for the new hexadecimal Numeral Notation * theories/Init/Numeral.v new interface for Numeral Notation (basically, a numeral is either a decimal or an hexadecimal) * theories/Init/Nat.v add hexadecimal numeral notation to nat * theories/PArith/BinPosDef.v '' positive * theories/ZArith/BinIntDef.v '' Z * theories/NArith/BinNatDef.v '' N * theories/QArith/QArith_base.v '' Q * interp/notation.ml{i,} adapting implementation of numeral notations * plugins/syntax/numeral.ml '' * plugins/syntax/r_syntax.ml adapt parser for real numbers * plugins/syntax/float_syntax.ml adapt parser for primitive floats * theories/Init/Prelude.v register parser for nat * adapting the test-suite (test-suite/output/NumeralNotations.{v,out} and test-suite/output/SearchPattern.out) * remaining ml files (interp/constrex{tern,pr_ops}.ml where two open had to be permuted)
2020-05-02Fix #12159 (Numeral Notations do not play well with multiple scopes for the ↵Pierre Roux
same inductive) Numeral Notations now play better with multiple scopes for the same inductive. Previously, when multiple numeral notations where defined for the same inductive, only the last one was considered for printing. Now, we proceed as follows 1. keep only uninterpreters that produce an output (first List.map_filter) 2. keep only uninterpretation for scopes that either have a scope delimiter or are open (second List.map_filter) 3. the final selection is made according to the order of open scopes, (find_uninterpretation) or or according to the last defined notation if no appropriate scope is open (head of list at the end)
2020-04-11If a custom entry has global, a bound variable is valid in this entry.Hugo Herbelin
This is due to "global" being a syntactic notation, thus including ident. Parsing was automatically supporting this. This commit adds support for printing.
2020-04-11If a custom entry has global, an argument-free abbreviation is valid in this ↵Hugo Herbelin
entry. Parsing was automatically supporting this. This commit adds support for printing. Note: It would be more delicate to recognize that some given entry support applicative nodes hence abbreviations with arguments.
2020-04-11Renaming confusingly-named insert_coercion into insert_entry_coercion.Hugo Herbelin
This is to avoid confusion with typing coercions. No change of semantics.
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-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
Ack-by: herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-12Print implicit arguments in types of referencesSimonBoulier
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-23Not iterating recursive notations more than once.Hugo Herbelin
2020-02-23parens --> parenthesesAbhishek Anand (optiplex7010@home)
2020-02-23added the new optionAbhishek Anand (optiplex7010@home)
2020-02-22In printing patterns, distinguish the case of a notation to @id.Hugo Herbelin
This is a case which conventionally deactivates implicit arguments.
2020-02-22Fix index bug in computing implicit signature of abbrev. in pattern printing.Hugo Herbelin
2020-02-22Fix inheritance of argument scopes when printing notations in patterns.Hugo Herbelin
2020-02-22Use auxiliary function for externing record patterns.Hugo Herbelin
Also apply the same conditions for printing constructors as record instances in both terms and patterns.
2020-02-22Inherit argument scopes in notations to expressions of the form @f.Hugo Herbelin
This is a change of semantics.
2020-02-22Deactivate implicit arguments in printing notations bound to "@f".Hugo Herbelin
This is to match the parsing policy (see #11091). In particular, we deactivate also argument scopes, consistently with what is done at parsing time.
2020-02-22Fixing printing of notations bound to an expression of the form "@f".Hugo Herbelin
The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[]) encoding of @f was lost. It remains to let printing match parsing wrt the deactivation of implicit arguments and argument scopes in such case. See next commit.
2020-02-22Fixing a notation printing bug (missing a @ to reflect absence of imp. args).Hugo Herbelin
When a non-applied reference was matching a notation to the same reference, implicit arguments were lost.
2020-02-22Fixing anomaly from #11091 (incompatible printing with notation and imp. args).Hugo Herbelin
We fix also an index error in deciding when to explicit print a non-inferable implicit argument.
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego
2020-02-21Merge PR #11142: Slightly improving strategy about when to print coercion or ↵Emilio Jesus Gallego Arias
explicitly print implicit arguments Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding ↵Emilio Jesus Gallego Arias
notation format + new notion of format associated to a given interpretation Ack-by: maximedenes
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ↵Hugo Herbelin
entries)." This reverts commit 29919b725262dca76708192bde65ce82860747be. It was pushed by mistake as part of #11530. Sorry about it.
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
We do two changes: - We distinguish between a notion of format generically attached to notations and a new notion of format attached to interpreted notations. "Reserved Notation" attaches a format generically. "Notation" attaches the format specifically to the given interpretation, and additionally, attaches it generically if it is the first time the notation is defined. - We warn before overriding an explicitly reserved generic format, or a specific format.
2020-02-17Take "Implicit Types" into account when printing terms.Hugo Herbelin
2020-02-17Mini-improvements in when to skip coercions or explicitly print implicit args.Hugo Herbelin
If a return type is given to a match/if/let, then we are in context (and thus may skip coercions or not make explicit those implicit arguments inferable from context). Note that the notion of "inferable from context" remains anyway an approximation in the case of implicit arguments. The body of a fix/cofix is also in context. Also fixed an inconsistency with parsing in the scope used to print the body of a fix.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 03:10:38 +0000