| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
compiler warnings).
I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It uses a term in front of a stack instead of a term in front of a list of applied
terms. From outside of eq_appr_x nothing should have changed.
Nasty evar instantiation bug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Semantic changes are :
- whd_nored_stack remplaces a defined meta by its value whereas the old whd_stack
didn't.
- Zcase and Zfix are alwais put on stack. iota_flag is checked by constructors and
cofix.
- simpl uses its own whd_ function that do not touch at matched term
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15634 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15618 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Mind that the behavior of MaybeFlexible, Flexible changes \! (we solve_pattern_eqn using the new list and not the old one)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15617 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15616 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15615 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
|
|
take care of checking progress when solving the remaining problems, distinguishing between solved and stuck conversions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15467 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
subroutine choose_less_dependent_instance. This might solve bug #2495
(only "might solve" because the bug does not come with a reproducible
example).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15461 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Corresponding operations in locusops.ml and miscops.ml
The type of occurrences is now a clear algebraic one instead of
a bool*list hard to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 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
|
|
Canonical Structure inference works on named terms only: i.e.
the projection and the value must be named (with few exceptions).
The set of named (head) terms is:
(Var _|Construct _|Ind _|Const _|Prod _|Sort _)
The set of unnamed is thus:
(Case _|Fix _|CoFix _|Evar _|Meta _|Rel _)
The MaybeFlex/MaybeFlex case, when no CS inference takes place,
unfolds the rhs only if it exposes a named term. If it exposes
an unnamed term, it tries to unfold on the lhs first. Note that
unnamed terms are whd normal terms, since iota and zeta are
performed by evar_apprec. So the algorithm behaves as before,
but stops unfolding the rhs 1 delta step before it exposes an
unnamed term. Then it starts unfolding the lhs. If the lhs
exposes a rigid term the rhs is naturally unfolded, going back
to same situation in which the algorithm was ending before.
But while it unfolds on the left, the rhs is still named, and
canonical structure inference can succeed.
Ex failing before, the "canon_" prefix marks projections/values
declared as canonical.
Record test := K { canon_proj : nat }
(* canon_proj x := math x with K y => y end *)
canon_val x := match x with 0 => 0 | S m => m end
Canonical Structure canon_struct x := K (canon_val x)
(* aliases *)
proj := canon_proj
val := canon_val
Old alg:
proj ? ===?=== val x
proj ? ===?=== canon_val x
proj ? ===?=== match x with ... end
canon_proj ? ===?=== match x with ... end (* no inference *)
match ? with K x...end ===?=== match x with 0 ...end (* FAIL *)
New alg:
proj ? ===?=== val x
proj ? ===?=== canon_val x
canon_proj ? ===?=== canon_val x (* inference works: ? := canon_struct *)
In case canon_struct is not declared for canon_proj and canon_val
it continues like that:
canon_proj ? ===?=== canon_val x
match ? with K x...end ===?=== canon_val x
match ? with K x...end ===?=== match x with 0 ...end (* FAIL *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15077 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
|
|
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
|
|
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
|
|
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
|
|
occurrences to abstract can be given. This allows to force "destruct"
to necessarily abstract over all occurrences of its main argument
(only the sub-arguments that occur in the inductive type of the main
argument have their occurrences constrained by typing). This
incidentally avoids "rewrite" succeeding in rewriting only a part of
the occurrences it has to rewrite. This repairs the failure of
RecursiveDefinition which failed after pattern unification fix from
r14642).
Full support for selecting occurrence of main argument still to be
done though.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14648 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Assume a pile of constants on the left, and a stuck canonical projection
on the right. We are going to unfold the left constants step by step,
and at every step, we are going to recheck that the very same projection
on the right is stuck. The new check for stuck canonical projections is
more expensive, we thus memoize it for the whole sequence of delta steps
on the left.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14646 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The check looks for 1 canonical projection applied to a meta/evar.
This fails to deal with telescopes that generate unification problems
containing something like "(pi_1 (pi_2 ?))" that is indeed a "stuck"
canonical projection but not of the form recognized by the previous
implementation. The same holds when pi_2 is a general function not
producing a constructor.
This patch checks if the argument of the canonical projection weak head
reduces to a constructor calling whd_betadeltaiota.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14645 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
|
|
Kept in "destruct" though.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14619 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
|
|
This complies with consider_remaining_unif_problems being the last
chance to solve constraints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14582 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
considering open problems
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
second-order matching) which was not working correctly in the general
case.
Also made that second-order matching for tactics (abstract_list_all)
uses this algorithm, along the lines of a proposal first experimented
by Dan Grayson (see unification.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14549 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14329 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
+ small typo fix in r14217
+ added compatibility of betaiota flag with 8.3 when "-compat 8.3" is given
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14223 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unification (evarconv.ml). Works better for compiling
math. comp. library while seems ok on other examples.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14153 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(it is a priori optimized but also able to reason modulo equality of
names and modulo alpha-conversion).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13945 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes
declared in sections.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
evar, and simultaneously make type inference with universes work better.
This only exports more functions from kernel/univ, to be able to work
with a set of universe variables during type inference. Universe
constraints are gradually added during type checking, adding information
necessary e.g. to lower the level of unknown Type variables to Prop or
Set. There does not seem to be a disastrous performance hit on the
stdlib, but might have one on some contribs (hence the "Tentative").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unification failure messages (it is not fully usable and was not
intended to be committed now, sorry for the noise).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
be unified with a (truly) rigid term would need to be able to project
non-atomic arguments of evars what is not done (consider e.g.
"Check (fun m n (H:m+n=n) => ((f_equal _ H) : S (m+n) = S n)).").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13894 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
be unified with a (truly) rigid term.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Made a distinction between truly rigid constructions (Rigid) and
possibly flexible constructions (match/fix/meta, now called
PseudoRigid) that are currently assimilated to rigid by lack of
appropriate study of their flexibility. One day, the flexibility of
these pseudo-rigid constructions will have to considered seriously.
- Removed useless Cast/Cast cases in Rigid/Rigid block (Cast
are removed in advance and LetIn are not considered Rigid).
- Moved LetIn into the MaybeFlexible class.
- Moved the Lambda/Lambda case upwards to factorize the rules for
eta-expansion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13882 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
governed in the latter case by a flag since (useful e.g. for setoid
rewriting which otherwise loops as it is implemented).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
