| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
then by last imported
Reviewed-by: Zimmi48
Ack-by: RalfJung
Ack-by: gares
|
|
This allows e.g. to support a notation of the form "x <== y <== z <= t"
standing for "x <= y /\ y <= z /\ z <= t".
|
|
This relies on finer-than partial order check with. In particular:
- number and order of notation metavariables does not matter
- take care of recursive patterns inclusion
|
|
|
|
|
|
|
|
[About] still says it.
Close #9056.
|
|
You can tell which it is from the `@{}` if you really care, and seeing
`Monomorphic List (A:Type)` with no indication that `Monomorphic` is
about universes can confuse people.
|
|
See discussion on coq-club starting on 23 August 2016.
|
|
|
|
No reason not to collapse inner applications with explicit arguments.
This is compatible with the ad hoc encoding of @f as GApp(f,[])/NApp(f,[]).
|
|
In some cases, Format's inner boxes inside an outer box act as break
hints, even though there are already "better" break hints in the outer
box.
We work around this "feature" by not inserting a box around the
default printing rule for a notation if there is no effective break
points in the box.
See https://caml.inria.fr/mantis/view.php?id=7804 for the related
OCaml discussion.
|
|
This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
|
|
|
|
notation to use among several of them"
This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing
changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
|
|
Also changed the API of pr_subgoals now using labels.
Also removed a trailing space in printing existentials.
|
|
|
|
For compatibility, the default is to parse as ident and not as pattern.
|
|
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}.
|
|
We reason up to order, and accept to match a final catch-all clauses
with any other clause.
This allows for instance to parse and print a notation of the form
"if t is S n then p else q".
|
|
This now works not only for parsing of fun/forall (as in 8.6), but
also for arbitraty notations with binders and for printing.
|
|
Example which is now reprinted as parsed:
fun '((x,y) as z) => (y,x)=z
|
|
For historical reasons (this was one of the first examples of
notations with binders), there was a special treatment for notations
whose right-hand side had the form "forall x, P" or "fun x => P". Not
only this is not necessary, but this prevents notations binding to
expressions such as "forall x, x>0 -> P" to be used in printing.
We let the general case absorb this particular case.
We add the integration of "let x:=c in ..." in the middle of a
notation with recursive binders as part of the binder list, reprinting
it "(x:=c)" (this was formerly the case only for the above particular
case).
Note that integrating "let" in sequence of binders is stil not the
case for the regular "forall"/"fun". Should we?
|
|
|
|
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.
|
|
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}"...
|
|
|
|
Seizing this opportunity to generalize the possibility for different
associativity into simply reversing the order or not. Also dropping
some dead code.
Example of recursive notation now working:
Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A).
|
|
This allows for instance to support recursive notations of the form:
Notation "! x .. y # A #" :=
(((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
(at level 200, x binder).
|
|
This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.
Example of (artificial) notation that this commit supports:
Notation "! x .. y # A #" :=
(.. (A,(forall x, True)) ..,(forall y, True))
(at level 200, x binder).
|
|
- The "terminator" of a recursive notation is now interpreted in the
environment in which it occurs rather than the environment at the
beginning of the recursive patterns.
Note that due to a tolerance in checking unbound variables of
notations, a variable unbound in the environment was still working
ok as long as no user-given variable was shadowing a private
variable of the notation - see the "exists_mixed" example in
test-suite.
Conversely, in a notation such as:
Notation "!! x .. y # A #" :=
((forall x, True), .. ((forall y, True), A) ..)
(at level 200, x binder).
Check !! a b # a=b #.
The unbound "a" was detected only at pretyping and not as expected
at internalizing time, due to "a=b" interpreted in context
containing a and b.
- Similarly, each binder is now interpreted in the environment in
which it occurs rather than as if the sequence of binders was
dependent from the left to the right (such a dependency was ok for
"forall" or "exists" but not in general).
For instance, in:
Notation "!! x .. y # A #" :=
((forall x, True), .. ((forall y, True), A) ..)
(at level 200, x binder).
Check !! (a:nat) (b:a=a) # True #.
The illegal dependency of the type of b in a was detected only at
pretyping time.
- If a let-in occurs in the sequence of binders of a notation with a
recursive pattern, it is now inserted in between the occurrences of
the iterator rather than glued with the forall/fun of the iterator.
For instance, in:
Notation "'exists_true' x .. y , P" :=
(exists x, True /\ .. (exists y, True /\ P) ..)
(at level 200, x binder).
Check exists_true '(x,y) (u:=0), x=y.
We now get
exists '(x, y), True /\ (let u := 0 in True /\ x = y)
while we had before the let-in breaking the repeated pattern:
exists '(x, y), (let u := 0 in True /\ x = y)
This is more compositional, and, in particular, the printer algorithm
now recognizes the pattern which is otherwise broken.
|
|
Was apparently forgotten in a67bd7f9.
|
|
See discussion on coq-club starting on 23 August 2016.
An open question: what priority to give to "abbreviations"?
|
|
|
|
When a proper notation variable occurred only in a recursive pattern
of the notation, the notation was wrongly considered non printable due
(the side effect that function compare_glob_constr and that
mk_glob_constr_eq does not do anymore was indeed done by aux' but
thrown away). This fixes it.
|
|
The two previous commits make the warning irrelevant and useless.
|
|
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
|
Since camlp5 parses from left, the last ", z" was parsed as part of an
arbitrary long list of "x1 , .. , xn" and a syntax error was raised
since an extra ", z" was still expected.
We support this by translating "x , .. , y , z" into "x , y , .. , z"
and reassembling the arguments appropriately after parsing.
|
|
|
|
This was preventing to work examples such as:
Notation "[ x ; .. ; y ; z ]" := ((x,((fun u => u), .. (y,(fun u =>u,z)) ..))).
|
|
|
|
|
|
Supporting accordingly printing of sequences of binders including binding
patterns.
|
|
|
|
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
|
|
|
|
Further work would include:
- Identify binders up to alpha-conversion (see #4932 with a list of
binders of length at least 2, or #4592 on printing notations such as
ex2).
A cool example that one could also consider supporting:
- Notation "[[ a , .. , b | .. | a , .. , b ]]" :=
(cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
|
|
immediately in the scope of another recursive pattern.
|
