| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
This works for contexts in Definition and co, but not yet for "fun" and co.
|
|
The motivations are:
- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
before this patch, there is a different treatment of `Definition f
'(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
to interpret `Definition f `pat := c : t`. With the patch, the fix
to avoid seeing a variable named `pat` works for both `fun 'x =>
...` and `Definition f 'x := ...`.
The drawbacks are:
- Counterpart to reflecting the concrete syntax more closerly, there
are more redundancies in the syntax. For instance, the case `CLetIn
(na,b,t,c)` can appears also in the form `CProdN (CLocalDef
(na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
|
|
Was apparently forgotten in a67bd7f9.
|
|
|
|
|
|
|
|
There is no way today to distinguish primitive projections from
compatibility constants, at least in the case of a record without
parameters.
We remedy to this by always using the r.(p) syntax when printing
primitive projections, even with Set Printing All.
The input syntax r.(p) is still elaborated to GApp, so that we can preserve
the compatibility layer. Hopefully we can make up a plan to get rid of that
layer, but it will require fixing a few problems.
|
|
|
|
|
|
This closes #5082 and closes #5778, but makes #6404 apply to `abstract`
as well as `transparent_abstract`. This is unfortunate, but I think it
is worth it to get `abstract` in the profile (and therefore not
misassign the time spent sending the subproof to the kernel). Another
alternative would have been to add a dedicated entry to `ltac_call_kind`
for `TacAbstract`, but I think it's better to just deal with #6404 all
at once.
The "better" solution here would have been to move `abstract` out of the
Ltac syntax tree and define it via `TACTIC EXTEND` like
`transparent_abstract`. However, the STM relies on its ability to
recognize `abstract` and `solve [ abstract ... ]` syntactically so that
it can handle `par: abstract`.
Note that had to add locations to `TacAbstract` nodes, as I could not
figure out how to call `push_trace` otherwise.
|
|
|
|
Adding a "let-in"-sensitive function hnf_prod_applist_assum to
instantiate parameters and using it for printing.
Thanks to PMP for reporting.
|
|
Moreover, when there are at least two clauses and the last most
factorizable one is a disjunction with no variables, turn it into a
catch-all clause.
Adding options
Unset Printing Allow Default Clause.
to deactivate the second behavior, and
Unset Printing Factorizable Match Patterns.
to deactivate the first behavior (deactivating the first one
deactivates also the second one).
E.g. printing
match x with Eq => 1 | _ => 0 end
gives
match x with
| Eq => 1
| _ => 0
end
or (with default clause deactivates):
match x with
| Eq => 1
| Lt | Gt => 0
end
More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
|
|
Fixes GH#6384 and GH#6385.
|
|
|
|
to use among several of them
|
|
|
|
|
|
|
|
|
|
|
|
- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.
E.g mono@{i} := Type@{i} is printed as
mono@{mono.i} := Type@{mono.i}.
There can be a name clash if there's a module and a constant of the
same name. It is detected and is an error if the constant is first
but is not detected and the name for the constant not
registered (??) if the constant comes second.
Accept VarRef when registering universe binders
Fix two problems found by Gaëtan where binders were not registered properly
Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs
Fix an issue of the stronger restrict universe context + no evd leak
This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
|
|
|
|
This allows us to enforce that it works without breaking the build
when it doesn't.
|
|
See discussion on coq-club starting on 23 August 2016.
An open question: what priority to give to "abbreviations"?
|
|
|
|
Note that this makes the following syntax valid:
Axiom foo@{i} bar : Type@{i}.
(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
|
|
Also nicer error when the constraints are impossible.
|
|
|
|
|
|
|
|
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
|
I think this only affects printing (in the new test you would get
[Var (0)] when printing runwrap) but is still ugly.
|
|
The rationale it that it is more common to do so and thus more
"natural" (principle of writing less whenever possible).
|
|
Was broken since 8.6.
|
|
|
|
|
|
Was broken since 8.6.
|
|
This concerns pr_value and message_of_value.
This has a few consequences. For instance, no more ad hoc message "a
term" or "a tactic", when not enough information is available for
printing, one gets a generic message "a value of type foobar".
But we also have more printers, satisfying e.g. request #5786.
|
|
Compared to the original proposition (59a594b in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
|
|
|
Also add an output test for Suggest Proof Using.
This changes the .aux output: instead of getting a key
>context_used "$hyps;$suggest"
where $hyps is a list of the used hypotheses and $suggest is the
;-separated suggestions (or the empty string if Suggest Proof Using is
unset), there is a key
>context_used "$hyps"
and if Suggest Proof Using is set also a key
>suggest_proof_using "$suggest"
For instance instead of
112 116 context_used "B A;A B;All"
we get
112 116 context_used "B A"
112 116 suggest_proof_using "A B;All"
|
