| Age | Commit message (Collapse) | Author |
|---|
|
us are not convertible
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14980 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14952 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14950 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- namegen.ml: if a matching variable has the same name as a constructor,
rename it, even if the conflicting constructor name is defined in a
different module;
- constrextern.ml: protect code for printing cases as terms are from
requesting info in the global env when printers are called from ocamldebug
since the global env is undefined in this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14947 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the type (mandatory) and the fields (optional)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14940 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Functions without _env use the global env.
- More comments about when letin are counted.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14908 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
|
|
unfolded fixpoints when calling destruct). However, this might break
compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
applicability of first-order unification in tactic unification). Don't
try to unify the type (this would require a unification power that
unification.ml does not have - and some contribs complain about
that). Just reject first-order unification of metavariables of
higher-order types when their types are obviously incompatible.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14817 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
meta in the tactic unification algorithm ("auto" becomes much slower
if it takes into account the type of metas).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14813 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
instantiating them in the unification algorithm used for tactics.
This allows to discard ill-typed uses of first-order unification which
otherwise would have been fatal (this incidentally allows to partially
restore some compatibility with 8.3 that was broken after eta was
added in unification).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14812 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
between branches.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14811 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
as to ensure the warning is flushed in real time. Made systematic the
use of if_warn instead of if_verbose when the warning is intended to
signal something anormal (if_warn is activated when compiling
verbosely and when working interactively while if_verbose is activated
only when working interactively and when loading verbosely).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14803 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
|
|
is imported): in case of nested modules, activation was done as soon
as the outermost module was imported.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14775 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
mechanism, section discharge is not ready for that.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14765 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
|
|
r14737 (when to expand an alias). However, the heuristic remains
different as before r14737 since we stopped taking into account the
dependency in the predicate to take the decision of expanding or not.
Let's see if we can eventually fine-tuning this.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14760 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
|
|
not in pattern-matching compilation.
Also extended to the Var case the preference given to using the term
to match as alias rather than its expansion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14737 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14736 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(bug was introduced in r14703 when postprocessing started to traverse
inner cases).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14728 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
are declared as such, but I suspect Coq to contain some more.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 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
|
|
Example:
Arguments eq_refl {B y}, [B] y.
Check (eq_refl (B := nat)).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The problem that this patch tries to solve is that sometimes the
unfolding behaviour of simpl is too aggressive, frequently exposing
match constructs. Moreover one may want some constants to never be
unfolded by simpl (like in the Math-Comp library where the nosimpl hack
is pervasive). Finally, one may want some constants to be volatile,
always unfolded by simple when applied to enough arguments, even if they
do not hide a fixpoint or a match.
A new vernacular command to be indroduced in a following patch attaches
to constants an extra-logical piece of information. It declares wich
arguments must be checked to evaluate to a constructor before performing
the unfolding of the constant (in the same spirit simpl considers as
such the recursive argument of an inner fixpoint).
Examples:
Arguments minus !x !y.
(* x and y must evaluate to a constructor for simpl to unfold minus *)
(S x - y) --- simpl ---> (S x - y)
(S x - S y) --- simpl ---> (x - y)
Definition fcomp A B C (f : B -> C) (g : A -> B) x := f (g x).
Arguments fcomp A B C f g x /.
Infix "\o" := fcomp (at level 50, left associativity) : nat_scope.
(* fcomp hides no fix, but simpl will unfold if applied to 6 arguments *)
(fun x => (f \o g) x) = f \o g --- simpl ---> (fun x => f (g x)) = f \o g
Arguments minus x y : simpl never.
(* simpl will never unfold minus *)
(S x - S y) --- simpl ---> (S x - S y)
Definition nid (x : nat) := x.
Arguments nid / x.
(* nid is volatile, unfolded by simpl when applied to 0 or more arguments *)
nid --- simpl ---> (fun x => x)
Arguments minus x y : simpl nomatch.
(* triggers for minus the "new" simpl heuristic I discussed with Hugo:
if reducing the fix would leave a match in "head" position
then don't unfold
a suggestion for a better name (for "nomatch") would be appreciated *)
(0 - y) --- simpl ---> 0
(S x - y) --- simpl ---> (S x - y)
(S x - S y) --- simpl ---> (x - y)
(minus 0) --- simpl ---> (minus 0)
(* This last test does not work as one may expect, i.e.
(minus 0) --- simpl ---> (fun _ => 0)
The point is that simpl is implemented as "strong whd_simpl"
and after unfolding minus you have
(fun m => match 0 => 0 | S n' => ...n' - m'... end)
that is already in whd and exposes a match, that of course "strong"
would reduce away but at that stage we don't know, and reducing by
hand under the lambda is against whd reduction. So further discussion
on that idea is needed. *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14716 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
to the dependencies in the real arguments (a.k.a. indices) of the
terms to match.
This allows in particular to make the example from bug report #2404
work.
TODO: move the computation of dependencies in compile_branch at the time
of splitting a branch (where the computation is done now, it does not allow
to support dependent matching on the second argument of a constructor of
type "forall b, (if b then Vector.t n else nat) -> Vector.t n -> foo").
TODO: take dependencies in Var's into account and take dependencies within
non-Rel arguments also into account (as in "match v (f t) with ... end"
where v is a Var and the type of (f t) depends on it).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14711 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for finding the initial predicate, since their type can be dependent
on previous terms to match and they may have to be generalized.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14710 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pattern-matching problem generated for the return clause were not the
name of patterns (no counter-example though, revealed by using
generalization more intensively).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14709 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
seems to provide a better rendering in pattern-matching
compilation. Did it also in compile_generalization but not sure the
uj_typ is not dropped anyway.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14708 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
between initial arguments (if not rel). Predicate now assumed dependent
by default.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14706 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14705 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14704 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14703 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14702 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
main criterion is to look at whether the alias to the term to match is
dependent in the return predicate or not. Since the exact return
predicate is often found late, the detection is done after the
subproblem is fully compiled, when a maximum amount of (local)
information on typing is known.
Eventually, we should go to a model where all possible partial
expansions of an alias are usable at typing time. Indeed the current
heuristic (like the previous one) is not fully safe since it might
decide not to expand an alias in a branch whose type does not depend
of the alias but the typing of the branch internally needs the
expansion (as e.g. in "fun (H:forall n, n=0->Prop) n => match n with 0
as x => H x eq_refl | _ => True end").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14701 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14699 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
declarations, in the usual backward mode,
the new token ":>>" declares the subinstance as a forward hint.
Both declare a coercion in other contexts. Cleanup the code for declarations for less confusion between
coercions and subinstance hints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
subclasses during type-checking.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14678 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14674 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This adds two experimental features to the typeclass implementation:
- Path cuts: a way to specify through regular expressions on instance names
search pathes that should be avoided (e.g. [proper_flip proper_flip]).
Regular expression matching is implemented through naïve derivatives.
- Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no
longer applied backwards, but introducing a specific [Equivalence] in the
environment register a [Reflexive] hint as well. Currently not
backwards-compatible, the next patch will allow to specify direction
of subclasses hints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pattern-matching when it turns after typing phase that no dependencies exists.
Incidentally, renamed regeneralize_index into relocate_index and make
it works both way (to generalize and to ungeneralize). This avoids
using replace_tomatch for ungeneralization which does not support
modifying the "deps".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14669 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
applies to terms to match that are not necessarily rel's.
Also simplified build_initial_predicate.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14668 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
of dependent types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14667 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
same in every branches while they should have been adjusted to the
names locally used in the branch. Fixing it by remembering an index
of the declaration to abstract in the env together with the
declaration itself.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14666 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(technically, since the signature "tomatch" of terms to match and of
terms to generalize is typed in a context that does not consider terms
to match as binders while the return predicate do consider them as
binders, the adjusment of the context of the "tomatch" to the context
of the predicate needs lifting in each missing part of the "tomatch"
context, what was not done)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14664 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
consequences up to now, but maybe because this type is often later on
thrown away).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14663 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
late for being taken into account in generalized declarations. Do it
build_branch as it was for specialization of the predicate.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14661 85f007b7-540e-0410-9357-904b9bb8a0f7
|
