| Age | Commit message (Collapse) | Author |
|---|
|
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
|
Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.
We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.
|
|
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
|
We address the easy ones, but they should probably be all removed.
|
|
|
|
|
|
|
|
This was introduced between v8.5 and v8.6 (presumably 63f3ca8).
|
|
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|
|
|
|
|
|
|
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
|
|
|
|
|
More precisely when matching
"f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z"
do not allow expansion of f since otherwise, we recursively have to
match "f t" with the same 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
|
|
To deal with existing notations starting with a "let" (see notation
"for" in output/Notation2.v) we adopt the pragmatic approach of
glueing only inner let by default.
Ideally, it might be nicer to detect if there is an overlap of
notation, and not to glue only in case of overlap. We could also
decide that a notation starting with a "let" should always be
protected by some constant, say "id", so as to avoid possible
collisions, but this would require changes user side.
|
|
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}"...
|
|
Reordering the maps for binders and terms while uninterpreting a
notation the same way it will be at the time of interpreting a
notation.
|
|
Factorizing the place where the different form of extended binders
(i.e. possibly including the 'pat form) are matched.
|
|
(binders shall be substitutable by arbitrary cases patterns).
Giving a proper status to the functions unifying different instance of
the same notation variable (up to alpha-renaming).
Note: The a priori change of semantics in "bind_binding_as_term_env"
which now apply renaming from "unify_id" (as it did in
"bind_bindinglist_as_term_env") should not have an effect since, as
the former comment said, this corresponds to a "Anonymous" case which
should not occur, since the term would have to be bound upwards.
|
|
Moving earlier functions which will be needed earlier.
|
|
|
|
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).
|
|
|
|
|
|
|
|
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.
|
|
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
|
|
|
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).
|
|
Conditions for printing 'pat were incomplete.
|
|
Was causing a failure to print recursive binders used twice or more in
the same notation.
|
|
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 internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
|
|
|
(from module List).
|
|
|
|
|
|
|
