aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2011-11-16Adding postprocessing to remove "commutative cuts" expansions inherbelin
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
2011-11-16Changed the way find_dependencies_signature is working so that itherbelin
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
2011-11-16De Bruijn indices bug in pattern matching compilation in the presenceherbelin
of dependent types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14667 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16Old generalization bug in pattern-matching: names were considered theherbelin
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
2011-11-16Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).herbelin
(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
2011-11-16Old typing bug in pattern-matching compilation (apparently w/oherbelin
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
2011-11-16Specialization of tomatch in pattern-matching compilation was done tooherbelin
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
2011-11-16A bit of documentation around cases.ml + ML modules uselessly openherbelin
+ dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14660 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-16Fixing dependencies lifting bug in pattern-matching compilationherbelin
(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
2011-11-08Refined second_order_matching so that a constraint on whichherbelin
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
2011-11-08optimization: memoization for is_open_canonical_projectiongareuselesinge
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
2011-11-08Improved check is_open_canonical_projectiongareuselesinge
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
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
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
2011-11-06Fixing incorrect change to pattern-unification over Meta's introducedherbelin
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
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
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
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Deactivating second-order pattern-matching in evarconv for 8.4.herbelin
Kept in "destruct" though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14619 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyletouzey
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
2011-10-25Fixing use of type constraint for refining the "return" clause of "match".herbelin
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
2011-10-25Continuing r14585 (ill-typed restriction bug).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14595 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Continuing r1492 (useless changes were inadvertantly committed)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14593 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25New strategy to infer return predicate of match construct whenherbelin
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
2011-10-25Still more unification in typing.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14591 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-24More unification in type_of and addition of e_type_of to get the newherbelin
evar_map after instantiations possibly happened. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14586 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-24Fixing another bug revealing ill-typed use of evar restriction.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14585 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-24Fixing instance/filter mismatch in materialize_evar + documentation.herbelin
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
2011-10-22Fail if some conv pbs remain after consider_remaining_unif_problems.herbelin
This complies with consider_remaining_unif_problems being the last chance to solve constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14582 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Now consider remaining conversion problems in solve_remaining_evars.herbelin
A step going towards a more uniform evar resolution protocol, currently: - solve simple constraints (+ actually some heuristics: f.o. unif and evar_define's heuristics) but postpone some of the remaining ones [evar_conv] - try type-classes resolution [resolve_typeclasses] - apply heuristics on remaining constraints and expect these constraints to be resolved [consider_remaining_unif_problems] - use the implicit tactic for yet open (unconstrained) evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14581 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Use also second-order unification if first-order fails at the time of ↵herbelin
considering open problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14580 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-22Fixing uncaught exception in pr_evar_map (pr_global failed for unknown ↵herbelin
global ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14578 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-17Partly reverting r14539 about fully expanding "let-in"s and not justherbelin
expanding them up to the last Var/Rel they are aliased to. The analysis made in r14539 about ill-typed pattern-unification in bug however, when abstracting over a "let-in" (in solve_pattern_eqn), the alias must be preserved for ensuring the correctness of typing. In short, "let-in"s are back considered for pattern-unification as constants of which we don't want to know the content but solve_pattern_eqn now takes into account that they have a value. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14568 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedherbelin
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
2011-10-11Unification in the return clause of match was not supported in solve_evars.herbelin
This is now fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14548 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
for the functions of unification.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14547 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11More on r14536 (an unused pattern-matching remained in the commit).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14546 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-11Various simplifications about constant_of_delta and mind_of_deltaletouzey
Most of the time, a constant name is built from: - a kernel_name for its user part - a delta_resolver applied to this kernel_name for its canonical part With this patch we avoid building unnecessary constants for immediately amending them (cf in particular the awkward code removed in safe_typing). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14545 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10More robust and uniform treatment of aliases in evarutil.mlherbelin
- Compute chain of aliases once for all so as to simplify code. - In is_unification_pattern, expand all vars/rels of the unification problem until they are no longer vars/rels so that the list of vars/rels used in the rhs is correct, and, the list of arguments of the evars eventually become irreducible vars/rels (in particular, this solves bug #2615). - Some points remain unclear, e.g. whether solve_evar_evar should reason with all let-in expanded or with let-in expanded only up to the last expansion which is still a var or rel. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14539 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Applied the trick of Chung-Kil Hur to solve second-order matchingherbelin
problems with dependencies. Generalized it to matching over dependent tuples as explored by Dan Grayson. Currently used only in Evarconv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14538 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Fixing buggy abberant code for Evarutil.expand_evarherbelin
by the way renamed into materialize_evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14537 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Little code simplification of instantiate_evar in evd.mlherbelin
(replace_vars was anyway optimized) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14536 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Added information about evar origin in pretty-printing evd for debugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14535 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-10Passed conv_algo to evar_define and move call to solve_refl toherbelin
evar_define so that it can recursively deal with evar/evar problems. Also, check_evar_instance now called after each instantiation. Also did a bit of file reformatting. The commit apparently induces a loss of some 0,4% on the compilation of the standard library. Maybe, introducing a heuristic to decide when to call check_evar_instance (which I guess is responsible for the overhead) might be a good thing to look at? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14534 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14523 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
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
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
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
2011-09-26Generalizing subst_term_occ so that it supports an arbitrary matchingherbelin
function but also restricting it to closed matching and consequently renaming it to subst_closed_term_occ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14498 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Adding subst_term up to convherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14497 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
resolution from Tacinterp to Pretyping (close to resolve_evars) so that final evar resolution can eventually be called from Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14496 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
that the kernel conversion solves the delta/delta critical pair the same way the tactics did. This allows to improve Qed time when slow down is due to conversion having (arbitrarily) made the wrong choice. Propagation is done thanks to a new kind of cast called REVERTcast. Notes: - Vm conversion not modified - size of vo generally grows because of additional casts - this remains a heuristic... for the record, when a reduction tactic is applied on the goal t leading to new goal t', this is translated in the kernel in a conversion t' <= t where, hence, reducing in t' must be preferred; what the propagation of reduction cast to the kernel does not do is whether it is preferable to first unfold c or to first compare u' and u in "c u' = c u"; in particular, intermediate casts are sometimes useful to solve this kind of issues (this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the combination "simpl;red" needs the intermediate cast to ensure Qed answers quickly); henceforth the merge of nested casts in mkCast is deactivated - for tactic "change", REVERTcast should be used when conversion is in the hypotheses, but convert_hyp does not (yet) support this (would require e.g. that convert_hyp overwrite some given hyp id with a body-cleared let-binding new_id := Cast(old_id,REVERTCast,t)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-08Two bugs in pattern-matching compilation:herbelin
- when several variables are generalized in a row (in compile_alias) - with constructors having more than one argument in some inductive family when the dependencies are used in the predicate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14388 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 10:57:56 +0000