| Age | Commit message (Collapse) | Author |
|---|
|
Dune will complain about these leftovers / dead files in the tree.
|
|
|
|
Looks like this bug was introduced when unification started raising the
UnableToUnify exception in 8ac929ea128f1f7353b3f4d532b642e769542e55 .
I now turn this exception into a PretypeError that is correctly catched
and printed.
|
|
|
|
|
|
Thanks to Emilio and Pierre-Marie Pédrot for pointers.
|
|
Aliases of global references can now be used in numeral notations
|
|
Now we support using inductive constructors and section-local variables
as numeral notation printing and parsing functions.
I'm not sure that I got the econstr conversion right.
|
|
|
|
As per https://github.com/coq/coq/pull/8064#pullrequestreview-145971522
|
|
As per https://github.com/coq/coq/pull/8064#discussion_r209875616
I decided to make it a warning because it seems more flexible that way;
users to are flipping back and forth between option types and not option
types while designing won't have to update their `abstract after`
directives to do so, and users who don't want to allow this can make it an
actual error message.
|
|
Also make `Check S` no longer anomaly
Add a couple more test cases for numeral notations
Also add another possibly-confusing error message to the doc.
Respond to Hugo's doc request with Zimmi48's suggestion
From https://github.com/coq/coq/pull/8064/files#r204191608
|
|
|
|
Some of this code is cargo-culted or kludged to work.
As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter. In
this case, the function registration must be synchronized with the
document state, but the functions should not be marshelled / stored
in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
In this case, the registration must be synchronized, and the function
should be marshelled / stored in the .vo.
In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.
In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.
The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality. For
plugins, a simple string suffices, as long as the string does not clash
between different plugins. In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files. Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.
----
Some of this code is response to comments on the PR
----
Some code is to fix an issue that bignums revealed:
Both Int31 and bignums registered numeral notations in int31_scope. We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins. This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).
|
|
|
|
|
|
|
|
|
|
|
|
```
git grep --name-only 'should goes' | xargs sed s'/should goes/should go/g' -i
```
|
|
|
|
This way, we could fully bypass bigint.ml.
The previous mechanism of parsing/printing Z is kept for now.
Currently, the conversion functions accepted by Numeral Notation foo
may have the following types.
for parsing:
int -> foo
int -> option foo
uint -> foo
uint -> option foo
Z -> foo
Z -> option foo
for printing:
foo -> int
foo -> option int
foo -> uint
foo -> option uint
foo -> Z
foo -> option Z
Notes:
- The Declare ML Module is directly done in Prelude
- When doing a Numeral Notation, having the Z datatype around
isn't mandatory anymore (but the error messages suggest that
it can still be used).
- An option (abstract after ...) allows to keep large numbers in
an abstract form such as (Nat.of_uint 123456) instead of reducing
to (S (S (S ...))) and ending immediately with Stack Overflow.
- After checking with Matthieu, there is now a explicit check
and an error message in case of polymorphic inductive types
|
|
|
|
|
|
This is a portion of roglo's PR#156 introducing a Numeral Notation
command : we deal here with inductive types via conversion fonctions
from/to Z written in Coq.
For an example, see plugins/syntax/NatSyntaxViaZ.v
This commit does not include the part about printing via some ltac.
Using ltac was meant for dealing with real numbers, let's see first what
become PR#415 about a compact representation for real literals.
|
|
The first part (e.g. register_bignumeral_interpretation) deals only with
the interp/uninterp closures. It should typically be done as a side
effect during a syntax plugin loading. No prim notation are active yet
after this phase.
The second part (enable_prim_token_interpretation) activates the prim
notation. It is now correctly talking to Summary and to the LibStack.
To avoid "phantom" objects in libstack after a mere Require, this
second part should be done inside a Mltop.declare_cache_obj
The link between the two parts is a prim_token_uid (a string), which
should be unique for each primitive notation. When this primitive
notation is specific to a scope, the scope_name could be used as uid.
Btw, the list of "patterns" for detecting when an uninterpreter should
be considered is now restricted to a list of global_reference
(inductive constructors, or injection functions such as IZR).
The earlier API was accepting a glob_constr list, but was actually
only working well for global_reference.
A minimal compatibility is provided (declare_numeral_interpreter),
but is discouraged, since it is known to store uncessary objects
in the libstack.
|
|
Without this, the library segment of all .vo except Notations.vo starts
with two TOKEN objects (declaration of tokens "->" and "<-").
This is due to side effects creating these objects during the dynlink
of ltac_plugin.cmxs, more precisely the two Metasyntax.add_token_obj in
Extraargs. It's quite cleaner to register these two side effects via
Mltop.declare_cache_obj, so that the two objects only live in
Notations.vo, and are loaded from there.
|
|
|
|
|
|
The previous implementation was calling a lot of useless unification
even though the net effect of the tactic was simply to add a binding to
the environment.
Interestingly the base tactic was used in several higher level tactics,
including evar and ssreflect pose.
Part of the fix for #8245.
|
|
- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
entries. This typically corresponds to rules of the form
'Notation "[ x ]" := x (x custom myconstr).' but also
'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
are natively recognized.
Incidentally merging ETConstr and ETConstrAsBinder.
Noticed in passing that parsing binder as custom was not done as in
constr.
Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
|
|
This trace of V7 syntax remained unnoticed (since July 2004).
|
|
|
|
|
|
case of missing record field
|
|
IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like
`Global Set SsrHave NoTCResolution`. I don't think it is needed (just
let the user write the desired locality), but if it is, the right way of
doing it is to let clients of Goptions specify a default locality.
|
|
|
|
|
|
|
|
As stated in the manual, the fourier tactic is subsumed by lra.
|
|
While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.
This is used to provide better error messages on missing record
fields.
|
|
|
