| Age | Commit message (Collapse) | Author |
|---|
|
This is to match the parsing policy (see #11091).
In particular, we deactivate also argument scopes, consistently with
what is done at parsing time.
|
|
The CApp(CRef f,[]) encoding required to match the NApp(NRef f,[])
encoding of @f was lost.
It remains to let printing match parsing wrt the deactivation of
implicit arguments and argument scopes in such case. See next commit.
|
|
When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
|
|
We fix also an index error in deciding when to explicit print a
non-inferable implicit argument.
|
|
Reviewed-by: ejgallego
|
|
Also renamed it to relative_entry_level.
Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused
Should not change global semantics (except error message in pr_arg).
|
|
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.
|
|
This is in anticipation of defining a new type
type specific_notation = LastLonelyNotation | NotationInScope
|
|
|
|
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.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
This was already possible manually using "{ _ }" in the type of
declaration. This was also possible for type classes. So, no reason to
forbid in Arguments.
|
|
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Instead of various termops and globnames aliases.
|
|
- Implicit arguments in the return clause and in the branches
of a match were not checked.
- Implicit arguments in each declaration of intern_context were not
restarted.
- Additionally, in intern_context, we take into account ids from the
env on top of which intern_context is called.
- A better approximation of the check for manual implicit in notations
improved (though not fully correct because the exact context of
interpretation of a binder in a notation with recursive binders is
not known).
We also rename impl_binder_index into binder_block_names in anticipation of
checking redundancies also for non-implicit arguments.
|
|
WithoutTypeConstraint says it can be a term. In particular, if it has
manual implicit arguments, these will be allowed only in leading
lambdas. I.e. it can start with "fun {x}" but not with "forall {x}".
New constructor UnknownIfTermOrType allows to be both a term or a
type. In particular, if it allowed start both with "fun {x}" and
"forall {x}".
|
|
+ tests in the test-suite for non max local implicit arguments
|
|
|
|
|
|
|
|
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
|
|
only-printing notations
Ack-by: cpitclaudel
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: ejgallego
|
|
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.
|
|
- Warn in some places where {x:T} is not assumed to occur (e.g. in
argument of an application, or of a match).
- Warn when an implicit argument occurs several times with the same name.
- Accept local anonymous {_:T} with explicitation possible using name `arg_k`.
We obtain this by using a flag (impl_binder_index) which tells if we
are in a position where implicit arguments matter and, if yes, the
index of the next binder.
|
|
This moves the encoding of "n" as "arg_n" closer to the user interface level.
Note however that Constrintern.build_impl is not able yet to use ExplByPos.
See further commits.
|
|
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.
|
|
`Fixpoint` with a let binder
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
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.
|
|
|
|
Fixes #9428. (Again.)
This is a cherry-pick of 68927ac4/4b02fbd9 bugfixes, because 0251c800 reverted them.
Corrects a 8.9.1 → 8.10.0 regression.
(cherry picked from commit 68927ac48b1ce8fe30edef24defdcdc84173a5a5)
|
|
We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.
This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.
The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.
This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
|
