| Age | Commit message (Collapse) | Author |
|---|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
explicitly print implicit arguments
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
entries)."
This reverts commit 29919b725262dca76708192bde65ce82860747be.
It was pushed by mistake as part of #11530. Sorry about it.
|
|
We do two changes:
- We distinguish between a notion of format generically attached to
notations and a new notion of format attached to interpreted
notations. "Reserved Notation" attaches a format
generically. "Notation" attaches the format specifically to the given
interpretation, and additionally, attaches it generically if it is the
first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
a specific format.
|
|
|
|
If a return type is given to a match/if/let, then we are in context
(and thus may skip coercions or not make explicit those implicit
arguments inferable from context). Note that the notion of "inferable
from context" remains anyway an approximation in the case of implicit
arguments.
The body of a fix/cofix is also in context.
Also fixed an inconsistency with parsing in the scope used to print
the body of a fix.
|
|
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
|
|
Should be semantically equivalent.
|
|
Should be semantically equivalent.
|
|
|
|
We restrict to those that are actually related to typeclasses, and
perform the following renamings:
Classops --> Coercionops
Class --> ComCoercion
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
We renounce to the ad hoc rule preferring a notation w/o delimiter
for a term with coercions stripped over a notation for the
fully-applied terms with coercions not removed.
Instead, we interleave removal of coercions and search for notations:
we prefer a notation for the fully applied term, and, if not, try to
remove one coercion, and try again a notation for the remaining term,
and if not, try to remove the next coercion, etc.
Note: the flatten_application could be removed if prim_token were able
to apply on a prefix of an application node.
|
|
refined version of #8890 which prevents #11033.
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
|
|
We restrict #8890 so that it looks for a notation only for the fully
applied coercion.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
* map special floats to registered CRef's
* kernel/float64.mli: add {is_infinity, is_neg_infinity} functions
* kernel/float64.ml: Replace string_of_float with a safe pretty-printing function
Namely:
let to_string_raw f = Printf.sprintf "%.17g" f
let to_string f = if is_nan f then "nan" else to_string_raw f
Summary:
* printing a binary64 float in 17 decimal places and parsing it again
will yield the same float, e.g.:
let f1 = 1. +. (0x1p-53 +. 0x1p-105)
let f2 = float_of_string (to_string f1)
f1 = f2
* OCaml's string_of_float gives a sign to nan values which shouldn't be
displayed as all NaNs are considered equal here.
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
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.
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
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.
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
|
|
Conversely, Type existential variables now (explicitly) cover the Set
case.
Similarly for Prop and SProp.
|
|
We consistently use:
- UUnknown: to mean a rigid anonymous universe
(written Type in instances and Type as a sort)
[was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
(written _ in instances and Type@{_} as a sort)
[was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
(written id or qualid in instances and Type@{id} or Type@{qualid} or more
generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)
There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.
There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.
|
|
|
|
|
|
|
|
|
|
Ack-by: JasonGross
Ack-by: erikmd
Reviewed-by: maximedenes
Ack-by: proux01
|
|
We make clearer which arguments are optional and which are mandatory.
Some of these representations are tricky because of small differences
between Program and Function, which share the same infrastructure.
As a side-effect of this cleanup, Program Fixpoint can now be used with
e.g. {measure (m + n) R}. Previously, parentheses were required around
R.
|
|
|
|
A scope delimiter was missing for primitive integers constants.
Add related regression tests.
|
|
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.
|
|
|
|
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
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>
|
|
|
|
Thanks to Georges Gonthier for noticing it.
Expanding a few Pervasives.compare at this occasion.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
We do a couple of changes:
- Splitting notation keys into more categories to make table smaller.
This should (a priori) make printing faster (see #6416).
- Abbreviations are treated for printing like single notations: they
are pushed to the scope stack, so that in a situation such as
Open Scope foo_scope.
Notation foo := term.
Open Scope bar_scope.
one looks for notations first in scope bar_scope, then try to use
foo, they try for notations in scope foo_scope.
- We seize the opportunity of this commit to simplify
availability_of_notation which is now integrated to
uninterp_notation and which does not have to be called explicitly
anymore.
|
|
|
|
This makes setting the option outside of the synchronized summary impossible.
|
|
write_function
|
|
|
