| Age | Commit message (Collapse) | Author |
|---|
|
especially about unused definitions, unused opens and unused rec
flags.
The following patch uses information gathered using these warnings to
clean Coq source tree. In this patch, I focused on warnings whose fix
are very unlikely to introduce bugs.
(a) "unused rec flags". They cannot change the semantics of the program
but only allow the inliner to do a better job.
(b) "unused type definitions". I only removed type definitions that were
given to functors that do not require them. Some type definitions were
used as documentation to obtain better error messages, but were not
ascribed to any definition. I superficially mentioned them in one
arbitrary chosen definition to remove the warning. This is unaesthetic
but I did not find a better way.
(c) "unused for loop index". The following idiom of imperative
programming is used at several places: "for i = 1 to n do
that_side_effect () done". I replaced "i" with "_i" to remove the
warning... but, there is a combinator named "Util.repeat" that
would only cost us a function call while improving readibility.
Should'nt we use it?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
current evar to project; this may happen if this evar is dependent and
is involved in evar-evar conversion problem eventually solved by
instantiating the current evar; could maybe be optimized when the evar
to materialize has invertible instance in which case
define_evar_from_virtual_equation applied on the current evar could be
shortcut, avoiding to create an evar).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for emacs mode.
Hopefully fixes Bug 2678 this time. Much saner and more compact code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15573 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Some "dependent evars" were forgotten in the emacs mode.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15530 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15205 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15184 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Small cache to avoid checking the same Rel or Var twice.
Consider an unification problem like the following one:
a := huge
b := F1 a + F2 a
c := G1 b + G2 b
===============
?i[c,b,a] == ?g[c,c,c]
The old code, as the "not optimal" comment was suggesting,
did process every item in the explicit substitution, even
duplicated ones, unfolding the letins over and over.
This was the cause of the huge slowdown in the definition
of cormen_lup in Ssreflect/theories/matrix.v, that
follows:
Fixpoint cormen_lup {n} :=
match n return let M := 'M[F]_n.+1 in M -> M * M * M with
| 0 => fun A => (1, 1, A)
| _.+1 => fun A =>
let k := odflt 0 [pick k | A k 0 != 0] in
let A1 : 'M_(1 + _) := xrow 0 k A in
let P1 : 'M_(1 + _) := tperm_mx 0 k in
let Schur := ((A k 0)^-1 *: dlsubmx A1) *m ursubmx A1 in
let: (P2, L2, U2) := cormen_lup (drsubmx A1 - Schur) in
let P := block_mx 1 0 0 P2 *m P1 in
let L := block_mx 1 0 ((A k 0)^-1 *: (P2 *m dlsubmx A1)) L2 in
let U := block_mx (ulsubmx A1) (ursubmx A1) 0 U2 in
(P, L, U)
end.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15116 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Also fixed apparent other bug in the presence of let-ins.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to
know if it occurs in rigid position or not. Such equations typically
come from matching problems such as "match a return ?T[a] with pair a1
a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the
return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified
with ?A. This possible dependency is kept since commits r15060-15062.
The heuristic is to restrict ?T so that the dependency is removed,
leading to a behavior similar to the one existing before these commits.
This allows BGsection15.v, from contrib Ssreflect, to compile as it
did before these commits.
Also, removed one function exported without true need in r15061.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15082 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
solve the following kind of code broken by being less restrictive on
projecting:
Set Printing Existential Instances.
Parameter f : forall x, x=0 -> x=0 -> x=1 /\ x=2.
Parameter g : forall y, y=0 /\ y=0.
Check match g _ with conj a b => f _ a b end.
(* and the return clause should not depend on the "_" *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15064 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
candidate for the possible projection (as was introduced in 8.4beta)
but try also to imitate (as was done before 8.4beta but not done in
8.4beta).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15062 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- use evar candidates instead of postponed conversion problems when
it is known (according to the projection heuristic used) that an
evar has only a fixed number of possible instances (as e.g. in
equation ?n[x,x] = x, with x a variable);
- this allows to be more robust in solving remaining problems: if
several instanciations exist, and one is not compatible with a previous
instantiation made among several choices for another evar,
backtracking is now possible;
- this allows in particular to fix regression #2670 (two postponed
conversion problems solved in an inconsistent way);
- but this requires more code.
At the same time, a refactoring of the code has been made so as to
hopefully clarify the elementary pieces of the algorithm. For
instance, there are now generic functions for both applying a filter
and giving candidates. The filter is systematically generalized so as
to have the ccl of the evar well-typed even in situations where we
could try on the contrary to restrict the evars occurring in the
ccl.
Anyway, when the representation of instances will be optimized using
identity substitutions, it will no longer be useful to use the filter
to shorten the size of the instances. Then, the filters will have,
like candidates, the only role of restricting the search space for
potential solutions to the unification problems.
Also, solve_refl can now be used to restrict equations ?x[t1..tn]=?x[u1..un]
up to conversion instead of up to unification. This (potententially)
looses constraints but this avoids looping at the time of considering
remaining problems and applying heuristics to them.
Also added printing of evar candidates in debugging evar printers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15061 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
change of semantics).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
solutions to unification.
Only allow bidirectional checking of constructor applications, enabled by a program_mode flag:
it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated
with delta-equivalent but not syntactically equivalent terms.
Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
us are not convertible
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
with evars under binders.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14873 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
known in advance to be instantiable by only a finite number of terms.
When an evar with candidates remain unsolved after unification, the
first candidate is taken as a heuristic.
This is used in particular to reduce the number of pending conversion
problems when trying to infer the return clause of a pattern-matching
problem. As an example, this repairs test 2615.v.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
eventually get the same numbers when replaying (but does not work for
Undo/Abort which are still not plugged to the summary freezing
mechanism).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14764 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14763 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pattern-unification test. They were tolerated up to r14539. Also
expanded the let-ins not bound to rel or var in the right-hand side of
a term for which pattern-unification is tested (this expansion can
refer to a non-let variable that has to be taken into account in the
pattern-unification test).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14757 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
[evar_map].
We also gather some metadata on these evars: if they are still undefined,
and if not, which evars have been used in their (partial) instantiation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14720 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in r14199 (June 2011). Meta's implicitly depend on the context they are
defined in and this has to be taken into account for checking if
occurrences are distinct (in particular, no Var's are allowed as
arguments of a pattern-unifiable Meta). The example expected to be
accepted thanks to r14199 is not a pattern-unification problem (it has
more than one solution) and was anyway already accepted (strange).
Compared to before r14199, aliases expansion and restriction of
pattern unification check to variables occurring in the right-hand
side are however now taken into account.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14642 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14595 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14593 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
external type has evars. We now create a new ad hoc evar instead of
having evars as arguments of evars and use filters to resolved them as
was done since about r10124. In particular, this completes the
resolution of bug 2615.
Evar filters for occurrences might be obsolete as a consequence of
this commit.
Also, abstract_tycon, evar_define, second_order_matching which all
implement some form of second_order_matching should eventually be
merged (abstract_tycon looks for subterms up to delta while
second_order_matching currently looks for syntactic equal subterms,
evar_define doesn't consider the possible dependencies in
non-variables-nor-constructors subterms but has a better handling of
aliases, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14592 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14585 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Also fixing use of filter in second_order_matching.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14584 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
expanding them up to the last Var/Rel they are aliased to.
The analysis made in r14539 about ill-typed pattern-unification in bug
however, when abstracting over a "let-in" (in solve_pattern_eqn), the
alias must be preserved for ensuring the correctness of typing.
In short, "let-in"s are back considered for pattern-unification as
constants of which we don't want to know the content but
solve_pattern_eqn now takes into account that they have a value.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14568 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Compute chain of aliases once for all so as to simplify code.
- In is_unification_pattern, expand all vars/rels of the unification
problem until they are no longer vars/rels so that the list of
vars/rels used in the rhs is correct, and, the list of arguments of
the evars eventually become irreducible vars/rels (in particular,
this solves bug #2615).
- Some points remain unclear, e.g. whether solve_evar_evar should
reason with all let-in expanded or with let-in expanded only up
to the last expansion which is still a var or rel.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14539 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
problems with dependencies. Generalized it to matching over dependent
tuples as explored by Dan Grayson. Currently used only in Evarconv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14538 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by the way renamed into materialize_evar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14537 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
evar_define so that it can recursively deal with evar/evar problems.
Also, check_evar_instance now called after each instantiation.
Also did a bit of file reformatting.
The commit apparently induces a loss of some 0,4% on the compilation
of the standard library. Maybe, introducing a heuristic to decide when
to call check_evar_instance (which I guess is responsible for the
overhead) might be a good thing to look at?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14534 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14382 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This new function is a copy of Util's one, but working on Constrhash
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14365 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14352 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14332 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
added array_equal in Util
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14318 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
No way to control it yet; maybe flag use_evars_pattern_unification
should be generalized for that purpose.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14199 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
constraints but postpone evar-evar problems
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14176 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Do not allow to filter variables that appear in the conclusion of an evar.
- Do not attempt to restrict evars based on a substitution that does not contain only evars
(fall back to the pattern fragment and do not lose solutions).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14174 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Properly normalize evars to reflect the already pruned evars in the type
of dependent evars to allow more precise restriction of hyps.
Directly check the type of an evar instance, allowing backtracking on
ill-typed instanciations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14169 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
typecheck the evar's conclusion
- Prevent extend_evar from creating ill-formed evars with de Bruijn-open conclusions.
- Minor fix of define_evars_as_lambda, another mixup of named and de Bruijn indices.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14163 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fix pretyping to consider remaining unif problems with the
right transparency information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
