| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14749 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The MLcase has notably changed:
- No more case_info in it, but only a type annotation
- No more "one branch for one constructor", but rather a sequence
of patterns. Earlier "full" pattern correspond to pattern Pusual.
Patterns Pwild and Prel allow to encode optimized matchs without
hacks as earlier. Other pattern situations aren't used (yet)
by extraction, but only by P.N Tollitte's code.
A MLtuple constructor has been introduced. It isn't used by
the extraction for the moment, but only but P.N. Tollitte's code.
Many pretty-print functions in ocaml.ml and other have been reorganized
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The new vernacular "Arguments" attaches to constants the extra-logical
piece of information regarding implicit arguments, notation scopes and
the behaviour of the simpl tactic. The About vernacular is extended to
print the new extra logical data for simpl.
Examples:
Arguments foo {A B}%type f [T] x.
(* declares A B and T as implicit arguments, A B maximally inserted.
declares type_scope on A and B *)
Arguments foo {A%type b%nat} p%myscope q.
(* declares A and b as maximally inserted implicit arguments.
declares type_scope on A, nat_scope on b and the scope delimited by
myscope on p *)
Arguments foo (A B)%type c d.
(* declares A and b in type_scope, but not as implicit arguments. *)
Arguments foo A B c.
(* leaves implicit arguments and scopes declared for foo untouched *)
Arguments foo A B c : clear implicits
(* equivalente too Implicit Arguments foo [] *)
Arguments foo A B c : clear scopes
(* equivalente too Arguments Scope foo [_ _ _] *)
Arguments foo A B c : clear scopes, clear implicits
Arguments foo A B c : clear implicits, clear scopes
Arguments foo A B c : clear scopes and implicits
Arguments foo A B c : clear implicits and scopes
(* equivalente too Arguments Scope foo [_ _ _]. Implcit Arguments foo [] *)
Arguments foo A B c : default implicits.
(* equivalent to Implicit Arguments foo. *)
Arguments foo {A B} x , A [B] x.
(* equivalent to Implicit Arguments foo [[A] [B]] [B]. *)
Arguments foo a !b c !d.
(* foo is unfolded by simpl if b and d evaluate to a constructor *)
Arguments foo a b c / d.
(* foo is unfolded by simpl if applied to 3 arguments *)
Arguments foo a !b c / d.
(* foo is unfolded by simpl if applied to 3 arguments and if b
evaluates to a constructor *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14717 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
|
|
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@14703 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@14700 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
how the names of an ltac expression are globalized - allowing the
expression to be a constr and in some initial context - and when and
how this ltac expression is interpreted - now expecting a pure tactic
in a different context).
This incidentally found a Ltac bug in Ncring_polynom!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14674 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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14658 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
|
|
For instance, consider this inductive type:
Inductive Ind := A | B | C | D.
For detecting "match" on this type, one was forced earlier to write code
in Ltac using "match goal" and/or "context [...]" and long patterns such as:
match _ with A => _ | B => _ | C => _ | D => _ end
After this patch, this pattern can be shortened in many alternative ways:
match _ with A => _ | _ => _ end
match _ with B => _ | _ => _ end
match _ in Ind with _ => _ end
Indeed, if we want to detect a "match" of a given type, we can either
leave at least one branch where a constructor is explicit, or use a "in"
annotation.
Now, we can also detect any "match" regardless of its type:
match _ with _ => _ end
Note : this will even detect "match" over empty inductive types.
Compatibility should be preserved, since "match _ with end" will
continue to correspond only to empty inductive types.
Internally, the constr_pattern PCase has changed quite a lot, a few elements
are now grouped into a case_info_pattern record, while branches are now
lists of given sub-patterns.
NB: writing "match" with missing last branches in a constr pattern was actually
tolerated by Pattern.pattern_of_glob_constr earlier, since the number of
constructor per inductive is unknown there. And this was triggering an uncaught
exception in a array_fold_left_2 in Matching later. Oups. At least this patch
fixes this issue...
Btw: the code in Pattern.pattern_of_glob_constr was quadratic in the number
of branch in a match pattern. I doubt this was really a problem, but having now
linear code instead cannot harm ;-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14644 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
|
|
in hypotheses.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14638 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14604 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
#2168)
We replace Global.lookup_constant by our own code that looks for a module
and enters its implementation. This is still preliminary work, I would prefer
to understand more completely the part about module substitutions when
entering an applied functor. But this code already appears to work quite well.
Anyway, since we only search for constants, we don't need to reconstitute a
100% accurate environment, as long as the same objects are in it.
Note:
- Digging inside module structures is slower than just using
Global.lookup_constant. Hence we try to avoid it as long as we could.
Only in front of axioms (or in front of constant unknown to Global)
do we check whether we have an inner-module implementation for this
constant. There is some memoization of the search for internal
structure_body out of a module_path.
- In case of inner-module axioms, we might not be able to print
its type, but only its long name.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14594 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
|
|
In presence of inlining, it seems that no alias is propagated
on the canonical kernel_name. We modify [subst_con0] to enforce
this semantics. It seems to work well, but my understanding of
this code is still limited...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14587 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14585 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
pattern; this fixes stupid causes of failure of destruct shown
by compiling contrib Containers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14579 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14573 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14571 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14570 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
zeta reductions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14564 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14556 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14555 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
|
|
Btw, we also get rid of equalities on something else than elements or sets
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14525 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- We now handle things like (H : E.eq x x -> ...) by rewriting
E.eq x x into True.
- There was also a confusion between E.t and its various equivalent
(but syntactically different) forms. This should be solved by
preventing inlining during an inner functor application.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14520 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
If two distinct parameters of the inductive type contributes to
polymorphism, they must have distinct names, othewise an aliasing
problem of the form "fun x x => max(x,x)" happens.
Also insisted that a parameter contributes to universe polymorphism
only if the corresponding occurrence of Type is not hidden behind a
definition.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14511 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
that the return predicate of the match construction is at an allowed
sort, resulting in tactics possibly manipulating ill-typed terms. This
is now fixed,
Incidentally removed in pretyping an ill-placed coercion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14508 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Tactics set/remember and destruct/induction take benefit of it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14485 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Signed-off-by: Tom Prince <tom.prince@ualberta.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14484 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Add option -boot to the coqtop given to fake_ide
- Be sure that a dying coqtop subprocess cannot go unnoticed.
Before that, for repositories compiled without -local,
coqtop -ideslave was dying immediately because it was missing
its coqlib informations. Then the first command send via
Marshal.to_channel was triggering a SIGPIPE and hence the death
of fake_ide. Strangely, the return code was not necessarily
understood as non-zero (?!). We now catch SIGPIPE and do an
"exit 1".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14480 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
After a successful build, re-doing make world should almost do nothing.
For that:
- Many targets added to .PHONY, especially "tools" since a "tools"
directory exists. And anyway this is said to speed-up make a bit.
- Concerning fake_ide, mentionning the .cm* instead of the .ml*
avoid rebuilding these .cm*, and hence possibly many other things.
- in Makefile.doc: fix the rule building index_url.txt
- coqtop.* is now built by $(BESTCOQMKTOP) instead of $(COQMKTOP)
(which is the symlink). This avoids a situation where a first
"make" could redo just a few files while a second "make" will
rebuild many more. Typical scenario : touch the Makefile,
1st make was re-doing tolink.ml and then coqmktop, but no more,
a 2nd make was then detecting that coqtop and the stdlib was to
be redone
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14472 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This restriction was introduce to solve #808, whose underlying
issue (causing a anomaly) doesn't seem active anymore.
Semantic:
- Axiom in the middle of a proof : immediatly usable
(just as a Definition)
- Hypothesis or Variable : not visible in current proof, only
usable in the next ones.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14470 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- make clean really erases *.log
- some missing \n at end of files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This way, we can test each night that coqtop -ideslave handles
correctly some specific sequences of API calls.
For the moment, we add a few tests of the backtracking.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14456 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
arguments needed for correct typing of partial applications (knowing
that in practice, users should anyway better declare such arguments as
maximally inserted).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14404 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(it does not work)
Indeed, if a rule in operconstr at some level starts with an ident, it
has to be declared as a keyword because other rules whose leftmost
call is a call to operconstr will eventually the top level "200" even
thought this leftmost operconstr might be declared at a lower
level. This is for instance the reason why "True /\ forall x, x=0" is
parsed even though /\ expects arguments at level less than 80 and
forall is at level 200.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14399 85f007b7-540e-0410-9357-904b9bb8a0f7
|
