| Age | Commit message (Collapse) | Author |
|---|
|
```
git grep --name-only 'should goes' | xargs sed s'/should goes/should go/g' -i
```
|
|
|
|
|
|
This parsing/printing method for nat should be just as fast as
the previous dedicated code. Moreover, we could now parse large
literals as nat numbers, by leaving them in a half-abstract form
such as (Nat.of_uint 123456). This form is convertible to the
closed (S (S (S ...))) form, so it shouldn't be a big deal for
compatibility, except for if some Ltac stuff relies on (S ...) to be
present after parsing. Of course, forcing the computation of
a (Nat.of_uint ....) may take a while or raise a Stack Overflow.
|
|
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.
|
|
|
|
This is prim token notations for inductive *types*, not values.
So we're speaking of a scope where 0 is the type nat, 1 is the type bool, etc.
To my knowledge, this feature hasn't ever been used, and is very unlikely
to be used ever, so let's clean the code a bit by removing it.
|
|
|
|
This cleanup prepares for forthcoming synchronization of prim_token_interpreter
wrt to Summary. These chains of prim_token_interpreter were anyway never used,
only one interpreter was declared per numeral scope.
After sync wrt Summary, we'll anyway be able to backtrack to a previous
interpreter.
|
|
|
|
|
|
|
|
|
|
|
|
This allows to use fixed commits and not just branches or tags.
We keep using git clone when $FORCE_GIT is set (for projects on
gforge.inria.fr and projects pulling dependencies through git submodules).
fiat-parsers also calls git submodule, but inside its own Makefile.
|
|
|
|
|
|
|
|
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
|
|
We'd like to use `(lang 1.1)` features. Elpi needs update as recent
`ppx_tools_versioned` changes broke it.
|
|
|
|
|
|
error" argument in make
|
|
|
|
|
|
"treat errors as warnings" flag (-W) is applied. "1" or undefined
includes the flag, other values or undefined omit it.
Removed the "-warn-error" parameter to configure. "-profile XXX" will
no longer cause these flags to be used.
|
|
As per https://github.com/coq/coq/pull/8167#issuecomment-416929865
|
|
As per https://github.com/coq/coq/pull/8349#pullrequestreview-150456919
|
|
|
|
|
|
context after "Set Diffs"
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This tests the outputs of extraction, to some extent.
|
|
|
|
|
|
This has become mostly garbage since GitLab CI became our main CI platform.
|
|
And fix wrong indentation.
|
|
|
