aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Type inference unification: fixed a 8.4 bug in the presence of unificationGravatar herbelin2012-01-04
| | | | | | with evars under binders. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
| | | | | | | 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
* Continuing 14812 and 14813 (use type information to reduce theGravatar herbelin2011-12-18
| | | | | | | | | | 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
* Added a flag to control the use of typing when instantiating appliedGravatar herbelin2011-12-17
| | | | | | | 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
* Added ability to take the type of applied metas into account whenGravatar herbelin2011-12-17
| | | | | | | | | | 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
* Reorganizing Unification.unify_0 so as to more easily share codeGravatar herbelin2011-12-17
| | | | | | between branches. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14811 85f007b7-540e-0410-9357-904b9bb8a0f7
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
| | | | | | | | | | 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
* Introducing a notion of evar candidates to be used when an evar isGravatar herbelin2011-12-16
| | | | | | | | | | | | 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
* Fixing a bug of commit r13310 (activating coercions only when moduleGravatar herbelin2011-12-07
| | | | | | | 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
* Backtrack on synchronizing universe counter with resetGravatar herbelin2011-12-06
| | | | | | 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
* Registering universe and meta/evar counters as summaries so as toGravatar herbelin2011-12-05
| | | | | | | | 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
* Yet another fix about alias in testing if pattern unification applies.Gravatar herbelin2011-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14763 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a small regression in pattern-matching compilation introduced inGravatar herbelin2011-12-04
| | | | | | | | | 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
* Discarding let-ins from the instances of the evars in theGravatar herbelin2011-12-04
| | | | | | | | | | 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
* Finally used typing to decide whether an alias needs to be expanded orGravatar herbelin2011-11-28
| | | | | | | | | 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
* Fixing dependencies postprocessing bug in pattern-matching compilation.Gravatar herbelin2011-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14736 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug in postprocessing dependencies in pattern-matching compilationGravatar herbelin2011-11-26
| | | | | | | (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
* avoid relying on weak invariant in cbv.mlGravatar bgregoir2011-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a DEPRECATED flag in declaration of options. For now only two options ↵Gravatar ppedrot2011-11-24
| | | | | | 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
* Adds a pair of function in Evar_util to gather dependent evars in anGravatar aspiwack2011-11-23
| | | | | | | | | [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
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
| | | | | | | | 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
* Configurable simpl tacticGravatar gareuselesinge2011-11-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Extend the computation of dependencies in pattern-matching compilationGravatar herbelin2011-11-21
| | | | | | | | | | | | | | | | | | | 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
* Add matching on non-inductive types in building an inversion problemGravatar herbelin2011-11-21
| | | | | | | 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
* Old naming bug in pattern-matching compilation: names in theGravatar herbelin2011-11-21
| | | | | | | | 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
* Inlining let-in (i.e. trace of aliases) in extract_predicate for whatGravatar herbelin2011-11-21
| | | | | | | | 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
* In pattern-matching compilation, now taking into account the dependenciesGravatar herbelin2011-11-21
| | | | | | | 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
* Optimizing the compilation of unused aliases in pattern-matching.Gravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifying history management in pattern-matching compilation.Gravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14704 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing postprocessing bugs in pattern-matching compilation.Gravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14703 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing stuff about alias dependencies now become useless.Gravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14702 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changed the way to detect if an "as" patterns is expanded or not. TheGravatar herbelin2011-11-21
| | | | | | | | | | | | | | | | | | 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
* Dead code + refreshing some comments in cases.ml.Gravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore backward compatibility. ":>" declares subinstances in Class ↵Gravatar msozeau2011-11-18
| | | | | | | | | | 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
* Fix for subclasses implementation, allowing to register generalized classes ↵Gravatar msozeau2011-11-18
| | | | | | subclasses during type-checking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing new bug introduced in r14665 when fixing bug #1834.Gravatar herbelin2011-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
| | | | | | | | | | | | | | 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
* Adding postprocessing to remove "commutative cuts" expansions inGravatar herbelin2011-11-16
| | | | | | | | | | | 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
* Changed the way find_dependencies_signature is working so that itGravatar herbelin2011-11-16
| | | | | | | 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
* De Bruijn indices bug in pattern matching compilation in the presenceGravatar herbelin2011-11-16
| | | | | | of dependent types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14667 85f007b7-540e-0410-9357-904b9bb8a0f7
* Old generalization bug in pattern-matching: names were considered theGravatar herbelin2011-11-16
| | | | | | | | | 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
* Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).Gravatar herbelin2011-11-16
| | | | | | | | | | | (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
* Old typing bug in pattern-matching compilation (apparently w/oGravatar herbelin2011-11-16
| | | | | | | 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
* Specialization of tomatch in pattern-matching compilation was done tooGravatar herbelin2011-11-16
| | | | | | | 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
* A bit of documentation around cases.ml + ML modules uselessly openGravatar herbelin2011-11-16
| | | | | | + dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14660 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing dependencies lifting bug in pattern-matching compilationGravatar herbelin2011-11-16
| | | | | | | (no actual counterexample, revealed by experiments on more aggressive generalizations over dependent arguments). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refined second_order_matching so that a constraint on whichGravatar herbelin2011-11-08
| | | | | | | | | | | | | | | | 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
* optimization: memoization for is_open_canonical_projectionGravatar gareuselesinge2011-11-08
| | | | | | | | | | | 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
* Improved check is_open_canonical_projectionGravatar gareuselesinge2011-11-08
| | | | | | | | | | | | | | 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
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 13:22:12 +0000