| Age | Commit message (Collapse) | Author |
|---|
|
Preferring a notation which does require a delimiter, depending on
whether the coercion is removed or not, was done for primitive tokens.
We do it for all notations.
|
|
|
|
This adds an optional [Subgraph] part to the Print Universes command,
eg [Print Universes Subgraph(i j)] to print only constraints related
to i and j (and Prop/Set).
|
|
Use of boxes to ensure locality of formatting + use of a
prlist_with_sep so that there are breaking points only inbetween the
elements and not at the end of the list.
|
|
|
|
The names are `uXXX` with `XXX` some number avoiding collision.
Note that there may be some collisions with polymorphic binders, eg
something like
~~~
Set Universe Polymorphism.
Section foo.
Universe u0.
Definition bar := Type.
(* bar@{u0} = Type@{u0} but this isn't the section u0 *)
Definition baz := Type@{u0}. (* this one is the section u0 *)
Definition foobar := Eval compute in baz -> Type.
(* Type@{u0} -> Type@{u0} but these aren't the same u0 *)
~~~
So maybe we should do a nametab lookup too. This is strictly a
printing issue (polymorphic binder names have no other use).
In the monomorphic case names are qualified by the parent definition
so it should be fine (barring module/definition collision but we
already have those).
Note that there are still unnamed universes as they didn't go through
UState (eg schemes).
|
|
Otherwise
~~~
Unset Strict Universe Declaration.
Section bar.
Let baz := Type@{u}.
Definition k := baz.
End bar.
Section bar.
Let baz := Type@{u}.
Definition k' := baz.
End bar.
~~~
is broken (and has been since we stopped checking for repeated section names).
|
|
It was good enough for the makefile but not for emacs.
|
|
|
|
|
|
Coercions were missing.
|
|
|
|
Fixes #8736.
|
|
This refines the fix to #2169 by distinguishing the short and
non-short printing modes.
This prepares functionalization of printers by always passing env
rather than setting env to None in short mode. This is not strictly
necessary for the env which is not used for printing global references
but it shall be more consistent in style when passing e.g. the nametab
functionally.
We however keep the fallback printer used in case of error while
printing: due to missing registration of submodule fields in the
nametab, printing with types does not work if there are references to
an inner module.
|
|
- Simplex based linear prover
Unset Simplex to get Fourier elimination
For lia and nia, do not enumerate but generate cutting planes.
- Better non-linear support
Factorisation of the non-linear pre-processing
Careful handling of equation x=e, x is only eliminated if x is used linearly
- More opaque interfaces
(Linear solvers Simplex and Mfourier are independent)
- Set Dump Arith "file" so that lia,nia calls generate Coq goals
in filexxx.v. Used to collect benchmarks and regressions.
- Rationalise the test-suite
example.v only tests psatz Z
example_nia.v only tests lia, nia
In both files, the tests are in essence the same.
In particular, if a test is solved by psatz but not by nia,
we finish the goal by an explicit Abort.
There are additional tests in example_nia.v which require specific
integer reasoning out of scope of psatz.
|
|
|
|
|
|
|
|
|
|
|
|
compat updates to do as part of a release.
|
|
Mostly via `dev/tools/update-compat.py --cur-version=8.9`
We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).
We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).
|
|
Fixes #6764: Printing Notation regressed compared to 8.7
|
|
As noted by Jason Gross on coq-club (Aug 18, 2016), the "small
inversion" heuristic is not used consistently depending on whether the
variables in the type constraint are Rel or Var.
This commit simply gives uniformly preference to the inversion of the
predicate along the indices of the type over other heuristics.
The next three commits will improve further a uniform use of the
different heuristics.
----------------------------------------------------------------------
Here are some extra comments on how to go further with the inference
of the return predicate:
The "small inversion" heuristic build_inversion_problem (1) is
characterized by two features:
- small inversion properly speaking (a), i.e. that is for a match on
t:I params p1(u11..u1p1) ... pn(un1..unpn) with pi exposing the
constructor structure of the indices of the type of t, a return
clause of the form "fun x1..xn (y:I params x1..xn) => match x1..xn y with
| p1(z11..z1p1) ... pn(zn1..znpn) => ?T@{z11..znpn}
| _ => IDProp
end" is used,
- the dependent subterms in the external type constraint U are replaced
by existential variables (b) which can be filled either by projecting
(i.e. installing a dependency) or imitating (i.e. no dependency);
this is obtained by solving the constraint ?T@{u11..unpn} == U by
setting ?T@{z11..znpn} := U'(...?wij@{zij:=uij}...) where U has been
written under the form U'(...uij...) highlighting all occurrences of
each of the uij occurring in U; otherwise said the problem is reduced to
the question of instantiating each wij, deciding whether wij@{zij} := zij
(projection) or wij@{zij} := uij (imitation) [There may be different
way to expose the uij in U, e.g. in the presence of overlapping, or of
evars in U; this is left undetermined].
The two other heuristics used are:
- prepare_predicate_from_arsign_tycon (2): takes the external type
constraint U and decides that each subterm of the form xi or y for a
match on "y:I params x1 ... xn" is dependent; otherwise said, it
corresponds to the degenerated form of (1) where
- no constructor structure is exposed (i.e. each pi is trivial)
- only uij that are Rel are replaced by an evar ?wij and this evar is
directly instantiated by projection (hence creating a dependency),
- simple use of of an evar in case no type constraint is given (3):
this evar is not dependent on the indices nor on the term to match.
Heuristic (1) is not strictly more powerful than other heuristics
because of (at least) two weaknesses.
- The first weakness is due to feature (b), i.e. to letting
unification decide whether these evars have to create a dependency
(projection) or not (imitation).
In particular, the heuristic (2) gives priority to systematic
abstraction over the dependencies (i.e. giving priority to
projection over imitation) and it can then be better as the
following example (from RelationClasses.v) shows:
Fixpoint arrows (l : Tlist) (r : Type) : Type :=
match l with
| Tnil => r
| A :: l' => A -> arrows l' r
end.
Fixpoint predicate_all (l : Tlist) : arrows l Prop -> Prop :=
match l with
| Tnil => fun f => f
| A :: tl => fun f => forall x : A, predicate_all tl (f x)
end.
Using (1) fails. It proposes the predicate
"fun l' => arrows ?l[l':=l'] Prop" so that typing the first branch
leads to unify "arrows ?l[l:=Tnil] Prop == Prop", a problem about
which evarconv unification is not able (yet!) to see what are the
two possible solutions. Using (2) works. It instead directly
suggests that the predicate is "fun l => arrows l Prop" is used, so
that unification is not needed.
Even if in practice the (2) is good (and hence could be added to
(1)), it is not universally better. Consider e.g.
y:bool,H1:P y,H2:P y,f:forall y, P y -> Q y |-
match y as z return Q y with
| true => f y H1
| false => f y H2
end : Q y
There is no way to type it with clause "as z return Q z" even if
trying to generalize H1 and H2 so that they get type P z.
- A second weakness is due to the interaction between small inversion
and constructors having a type whose indices havex a less refined
constructor structure than in the term to match, as in:
Inductive I : nat -> Set :=
| C1 : forall n : nat, listn n -> I n
| C2 : forall n : nat, I n -> I n.
Check (fun x : I 0 => match x with
| C1 n l => 0
| C2 n c => 0
end).
where the inverted predicate is "in I n return match n with 0 => ?T | _ => IDProp end"
but neither C1 nor C2 have fine enough types so that n becomes
constructed. There is a generic solution to that kind of situation which
is to compile the above into
Check (fun x : I 0 => match x with
| C1 n l => match n with 0 => 0 | _ -> id end
| C2 n c => match n with 0 => 0 | _ -> id end
end).
but this is not implemented yet.
In the absence of this refinement, heuristic (3) can here work
better.
So, the current status of the claim is that for (1) to be strictly
more powerful than other current heuristics, work has to be done
- (A) at the unification level (by either being able to reduce problems of
the form "match ?x[constructor] with ... end = a-rigid-term", or, at
worst, by being able to use the heuristic favoring projecting for such
a problem), so that it is better than (2),
- (B) at the match compilation level, by enforcing that, in each branch,
the corresponding constructor is refined so has to match (or
discriminate) the constraints given by the type of the term to
match, and hence being better than (3).
Moreover, (2) and (3) are disjoint. Here is an example which (3) can
solve but not (2) (and (1) cannot because of (B)). [To be fixed in
next commit.]
Inductive I : bool -> bool -> Type := C : I true true | D x : I x x.
Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
match y with
| C => f y H1
| D _ => f y H2
end : Q y z.
Indeed, (2) infers "as y' in I b z return Q y z" which does not work.
Here is an example which (2) can solve but not (3) (and (1) cannot
because of (B) again). [To be fixed in 2nd next commit].
Check fun z P Q (y:I true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
match y with
| C => f y true H1
| D b => f y b H2
end : Q y z.
fix
|
|
This is actually a bit ad hoc at this stage in the sense that this is
specifically to prefer an informative first-order unification failure
over the currently always uninformative failure coming from
second-order unification.
When second-order unification shall be able to give more information,
one may consider alternative strategies, even maybe reporting not just
one but the list of failures in all (interesting) branches.
|
|
|
|
In particular we check if really used for internal debugging purpose
or to display a message to the user. In the latter case, we replace it
(when possible) by a higher-level printer (e.g. printing foo instead
of Top.foo). In the former case, we clarify that the use is a
debugging use.
Still not perfect (see a few FIXME).
|
|
|
|
This used to print Var (before #8475, even with explicit binders) but
now doesn't.
|
|
Comes with minor cleanups in exception catching and unnecessary mapi.
|
|
This restores the old behaviour that was printing qualified global names as
a representation of anonymous bound universes, at the cost of a ugly hack.
Ideally this should be handled by the callers, but for the time being the
trade-off is probably OK.
|
|
We simply declare the bound universes with their user-facing name in the
evarmap and call all printing functions on uninstantiated terms. We had to
tweak the universe name declaring function so that it would work properly
with bound universe variables and handle sections correctly.
This changes the output of polymorphic definitions with unnamed universe
variables. Now they are printed as Var(i) instead of the Module.n uid
that came from their absolute name.
|
|
This refines even further c24bcae8 (PR #924) and 6304c843:
- c24bcae8 fixed the order in the heuristic
- 6304c843 improved the order by preferring projections
There remained a dependency in the alphabetic order in selecting
unification candidates. The current commit fixes it.
We radically change the representation of the substitution to invert
by using a map indexed on the rank in the signature rather than on the
name of the variable.
More could be done to use numbers further, e.g. for representing
aliases.
Note that this has consequences on the test-suite (in
output/Notations.v) as some problems now infer a dependent return
clause.
|
|
As far as I know, this plugin is untested and barely maintained. I don't
think it has real use cases any more, so let's move it out from the repo
and see if somebody wants to take over and maintain it.
We also remove the documentation, which was telling our users to look at
ring to see an example of reification done using quote, when in fact it
wasn't using it anymore.
|
|
|
|
|
|
from compiles files
|
|
Removing in passing two Local which are no-ops in practice.
|
|
The recursion names in fix and cofix were not renamed like other
binders were.
|
|
This fixes the fix 1522b989 to #7192.
The remaining Not_found after 1522b989 should have rung a bell that
something was still strange.
|
|
|
|
|
|
- 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.
|
|
Print the expected and actual types for the option value (which is one
of bool, int, or string).
|
|
pattern (closes #7777)
|
|
This is particularly useful when the pattern is part of a disjunction.
Maybe this could be improved though, not mentioning the pattern when
there is no disjunction, but that would be more work.
|
|
No reason not to collapse inner applications with explicit arguments.
This is compatible with the ad hoc encoding of @f as GApp(f,[])/NApp(f,[]).
|
|
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.
|
|
We make it possible to deprecate tactics defined by `Ltac`, `Tactic
Notation` or ML.
For the first two variants, we anticipate the syntax of attributes:
`#[deprecated(since = "XX", note = "YY")]`
In ML, the syntax is:
```
let reflexivity_depr =
let open CWarnings in
{ since = "8.5"; note = "Use admit instead." }
TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr
[ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
END
```
A warning is shown at the point where the tactic is used (either
a direct call or when defining another tactic):
Tactic `foo` is deprecated since XX. YY
YY is typically meant to be "Use bar instead.".
|
|
In some cases, Format's inner boxes inside an outer box act as break
hints, even though there are already "better" break hints in the outer
box.
We work around this "feature" by not inserting a box around the
default printing rule for a notation if there is no effective break
points in the box.
See https://caml.inria.fr/mantis/view.php?id=7804 for the related
OCaml discussion.
|
