aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* 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
* Fixing incorrect change to pattern-unification over Meta's introducedGravatar herbelin2011-11-06
| | | | | | | | | | | | | | | 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
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
| | | | | | | | | | | | | | | | | These annotations are purely optional, but could be quite helpful when trying to understand the code, and in particular trying to trace which which data-structure may end in the libobject part of a vo. By the way, we performed some code simplifications : - in Library, a part of the REQUIRE objects was unused. - in Declaremods, we removed some checks that were marked as useless, this allows to slightly simplify the stored objects. To investigate someday : in recordops, the RECMETHODS is storing some evar_maps. This is ok for the moment, but might not be in the future (cf previous commit on auto hints). This RECMETHODS was not detected by my earlier tests : not used in the stdlib ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14627 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deactivating second-order pattern-matching in evarconv for 8.4.Gravatar herbelin2011-10-26
| | | | | | Kept in "destruct" though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14619 85f007b7-540e-0410-9357-904b9bb8a0f7
* When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyGravatar letouzey2011-10-26
| | | | | | | | | | | | | Here Foo is Univ.constraints, Univ.universes, Evd.evar_map, Evd.Metamap Ok, all these structures are currently ocaml's maps or similar, with a unique empty value, and (=) can be used on them in this particular case. But using Foo.is_empty is safer : it will work even if the underlying representation changes. Example : for spotting non-legitimate use of (=) we might embed a type into a record with a functional field. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing use of type constraint for refining the "return" clause of "match".Gravatar herbelin2011-10-25
| | | | | | | Adams Chlipala's ltamer now compatible with forthcoming 8.4; thanks to Matthieu for how to reactivate inh_conv_coerces_to. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14596 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r14585 (ill-typed restriction bug).Gravatar herbelin2011-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r1492 (useless changes were inadvertantly committed)Gravatar herbelin2011-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14593 85f007b7-540e-0410-9357-904b9bb8a0f7
* New strategy to infer return predicate of match construct whenGravatar herbelin2011-10-25
| | | | | | | | | | | | | | | | | | | | 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
* Still more unification in typing.mlGravatar herbelin2011-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14591 85f007b7-540e-0410-9357-904b9bb8a0f7
* More unification in type_of and addition of e_type_of to get the newGravatar herbelin2011-10-24
| | | | | | evar_map after instantiations possibly happened. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14586 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing another bug revealing ill-typed use of evar restriction.Gravatar herbelin2011-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14585 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing instance/filter mismatch in materialize_evar + documentation.Gravatar herbelin2011-10-24
| | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-07 15:23:33 +0000