| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.
|
|
This will enable to define numeral notation on non inductive by using
an inductive type as proxy and those translations to translate to/from
the actual type to the inductive type.
|
|
|
|
|
|
|
|
We add hexadecimal numerals according to the following regexp
0[xX][0-9a-fA-F][0-9a-fA-F_]*(\.[0-9a-fA-F_]+)?([pP][+-]?[0-9][0-9_]*)?
This is unfortunately a rather large commit. I suggest reading it in
the following order:
* test-suite/output/ZSyntax.{v,out} new test
* test-suite/output/Int63Syntax.{v,out} ''
* test-suite/output/QArithSyntax.{v,out} ''
* test-suite/output/RealSyntax.{v,out} ''
* test-suite/output/FloatSyntax.{v,out} ''
* interp/numTok.ml{i,} extending numeral tokens
* theories/Init/Hexadecimal.v adaptation of Decimal.v
for the new hexadecimal Numeral Notation
* theories/Init/Numeral.v new interface for Numeral Notation (basically,
a numeral is either a decimal or an hexadecimal)
* theories/Init/Nat.v add hexadecimal numeral notation to nat
* theories/PArith/BinPosDef.v '' positive
* theories/ZArith/BinIntDef.v '' Z
* theories/NArith/BinNatDef.v '' N
* theories/QArith/QArith_base.v '' Q
* interp/notation.ml{i,} adapting implementation of numeral notations
* plugins/syntax/numeral.ml ''
* plugins/syntax/r_syntax.ml adapt parser for real numbers
* plugins/syntax/float_syntax.ml adapt parser for primitive floats
* theories/Init/Prelude.v register parser for nat
* adapting the test-suite (test-suite/output/NumeralNotations.{v,out}
and test-suite/output/SearchPattern.out)
* remaining ml files (interp/constrex{tern,pr_ops}.ml where two open
had to be permuted)
|
|
Add headers to a few files which were missing them.
|
|
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
|
|
Since their introduction, these notations were incorrectly using the
proof-local environment.
|
|
Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.
This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`
See examples of each use case in the next two commits.
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
|
|
|
|
As per https://github.com/coq/coq/pull/8965#issuecomment-441440779
|
|
This fixes #8401
Supersedes / closes #8407
Vernacular-command-registered numeral notations now live in the summary,
and the interpretation function for them is hard-coded.
Plugin-registered numeral notations are still unsynchronized, and only
the UIDs of these functions gets synchronized. I am not 100% sure why
this is fine, but the test-suite file working suggests that it is fine.
I think it is because worker delegation correctly handles
non-synchronized state which is declared at `Declare ML Module`-time.
This final commit changes the synchronization of numeral notations (and
deletes no-longer-used declarations in notation.mli that were introduced
temporarily in the last commit). Since the interpretation can now be
done in notation.ml, we no longer need to register unique ids for
numeral notation (un)interp functions, and can instead synchronize the
underlying constants with the document state. This is the change that
actually fixes #8401.
|
|
Move most of the rest of the stuff from numeral.ml to notation.ml. Now
that we use exceptions to print error messages, all of the
interpretation code for numeral notations can be moved to notation.ml.
This is commit 1/4 in the fix for #8401.
This is a pure cut/paste commit, modulo fixing name qualifications due
to moved things, and exposing some stuff in notation.mli (to be removed
in the next commit, where we finish the numeral notation reworking).
|
|
Switch to using exceptions rather than user errors. This will be
required because the machinery for printing constrs is not available in
notation.ml, so we move the error message printing to himsg.ml instead.
This is commit 2/4 in the fix for #8401.
|
|
Move various things from from numeral.ml to notation.ml and
notation.mli; this is required to allow the vernac command to continue
living in numeral.ml while preparing to move all of the numeral notation
interpretation logic to notation.ml
This is commit 1/4 in the fix for #8401.
This is a pure cut/paste commit, modulo adding section-heading comments.
|
|
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
|
