| Commit message (Collapse) | Author | Age |
... | |
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15500 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15490 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
|
|
|
|
|
|
| |
known instances in unification.ml). This refines the fix to bug #1918.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15444 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15418 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@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15385 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Stuff about reductions now in genredexpr.mli, operations in redops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15307 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
+ comment correction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15253 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15246 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
coercion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15245 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@15204 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
|
|
|
|
|
|
| |
Same for check_leq instead of check_geq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 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
|
|
|
|
|
|
| |
by default typeclass resolution is not launched on goal evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15074 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The optimisation done of Namegen.visibly_occur_id did not preserve
the previous behavior when pr_constr/constr_extern/detype were
called on a term with free rel variables. We backtrack on it to
go back to the 8.2 behavior.
Seized this opportunity to clarify the meaning of the at_top flag
in constrextern.ml and printer.ml and to rename it into
goal_concl_style. The badly-named at_top flag was introduced in
Coq 6.3 in 1999 to mean that when printing variables bound in the
goal, names had to avoid the names of the variables of the goal
context, so as to keep naming stable when using "intro"; in
r4458, printing improved by not avoiding names that were short
names of global definitions, e.g. "S", or "O" (except when the
at_top flag was on for compatibility reasons).
Other printing strategies could be possible in the
non-goal-concl-style mode. For instance, all bound variables
could be made distinct in a given expression, even if no clash
occur, therefore following so-called Barendregt's
convention. This could be done by setting "avoid"
to "ids_of_rel_context (rel_context env)" in extern_constr and
extern_type (and then, Namegen.visibly_occur_id could be
re-simplified again!).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15067 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
|
|
|
|
|
|
|
|
| |
- (Regular) Casts become typing constraints again.
- Coerce tycon to inductive type when applying bidirectional typechecking hint.
- Coerce lambda expressions to tycon, might require coercions now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15058 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
- reinstall (x : T | P) binder syntax extension.
- fix a wrong Evd.define in coercion code.
- Simplify interface of eterm_obligations to take a single evar_map.
- Fix a slightly subtle bug related to resolvability of evars: some
were marked unresolvable and never set back to resolvable across calls
to typeclass resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
simpl was accessing the reduction stack at position n when
the length of the stack was exactly n.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
It is now possible to tell simpl to unfold a constant
that hides no "match" but is applied to concrete arguments.
Arguments id _ !n.
Goal forall x, id x = id 2.
intros; simpl.
x : nat
========
id x = 2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15048 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
of evars.
Used when interpreting a constr in Ltac: resolution is now launched if the constr
is casted.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15038 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15037 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
|