aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
Commit message (Collapse)AuthorAge
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
| | | | | | by default typeclass resolution is not launched on goal evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Second step of integration of Program:Gravatar msozeau2012-03-14
| | | | | | | | - Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove support for "abstract typing constraints" that requires unicity of ↵Gravatar msozeau2012-03-14
| | | | | | | | | | | solutions to unification. Only allow bidirectional checking of constructor applications, enabled by a program_mode flag: it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated with delta-equivalent but not syntactically equivalent terms. Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 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
* 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
* 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
* 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
* 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
* 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
* 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
* Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedGravatar herbelin2011-10-11
| | | | | | | | | | | 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
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
| | | | | | for the functions of unification.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14547 85f007b7-540e-0410-9357-904b9bb8a0f7
* More robust and uniform treatment of aliases in evarutil.mlGravatar herbelin2011-10-10
| | | | | | | | | | | | | | - 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
* Generalizing subst_term_occ so that it supports an arbitrary matchingGravatar herbelin2011-09-26
| | | | | | | 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
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Fix unification: detect invalid evar instantiations due to scoping earlier.Gravatar msozeau2011-08-04
| | | | | | Add a debug printer for existential sets (used for frozen_evars in w_unify). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing two typos introduced in r14217 and r14223Gravatar herbelin2011-06-20
| | | | | | | | (due to unreverted debugging stuff): - wrong revert of betaiota flag to false in r14223 - wrong exception raised in r14217 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14224 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensured that the transparency state is used when flag betaiota is on for apply.Gravatar herbelin2011-06-19
| | | | | | | + small typo fix in r14217 + added compatibility of betaiota flag with 8.3 when "-compat 8.3" is given git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14223 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
| | | | | | | | | | use_pattern_unification common for evars and metas. As a compensation, add a flag use_meta_bound_pattern_unification to restore the old mechanism of pattern unification for metas applied to rels only (this is used e.g. by auto). Not sure yet, what could be the most appropriate set of flags. Added documentation of the flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Activating flags betaiota by default for applyGravatar herbelin2011-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14220 85f007b7-540e-0410-9357-904b9bb8a0f7
* The ad hoc version for first-order unification at toplevel of "?n argsGravatar herbelin2011-06-18
| | | | | | | | | | | = t" introduced in r14199 (w_typed_unify_list) tried to check types of metas more than what w_typed_unify used to before (and these types need delta to be convertible). Don't know if it is a weakness of the test for checking types but since checking types should not be necessary here, w_typed_unify_list now follows what w_unify_core_0 does more closely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14217 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added full pattern-unification on Meta for tactic unification.Gravatar herbelin2011-06-13
| | | | | | | No way to control it yet; maybe flag use_evars_pattern_unification should be generalized for that purpose. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
| | | | | | | | | strict subterms of the initial unification problem (inspired from ssreflect rewriting strategy). Not activated however (a few applications of setoid rewrite use this possibility on closed terms in the stdlib, e.g. "flip le p (min n m)" identified with "le (min n m) p"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups, typo in previous commitGravatar herbelin2011-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14192 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed what looks like a (very old) useless f.o. unification passGravatar herbelin2011-06-12
| | | | | | made after s.o. unification succeeds. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14191 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new flag for freezing evars in tactic unification. Used thisGravatar herbelin2011-06-12
| | | | | | | | | | | | | | | | flag to forbid rewriting tactics to instantiate an evar of the goal while looking for subterms (this is not clear that we always want that for rewrite but we certainly want it for autorewrite; see comments by Charguéraud on coqdev Oct 2010). In a few cases in the theories, a pre-existing evar of an hyp used for rewriting is instantiated by the rewriting step. Let's accept this at the current time. We have to make progress towards documenting and stabilizing the strategy for matching/unifying subterms in rewrite/induction/set... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14190 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
| | | | | | | | - seized the opportunity to align unification flags for functional induction to the ones of induction - also tried to add delta in the elim_flags used in tactics.ml - also tried to unify the rewrite flags in concl or in hyp (removed allow_K in hyps) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14186 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix merge, Cumul moved to CUMULGravatar msozeau2011-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
| | | | | | | | | Stop using hnf_constr in unify_type, which might unfold constants that are marked opaque for unification. Conflicts: pretyping/unification.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14092 85f007b7-540e-0410-9357-904b9bb8a0f7
* First phase removing obsolete support for eta up to conversion inGravatar herbelin2011-05-04
| | | | | | | | | | "apply" unification. Assuming w_unify_0 is not eventually abandoned, it remains to merge unify_with_eta into unify_0 (what unify_with_eta does and that unify_0 does not do is to select of two instances of the same meta the one with less lambda's; it is unclear whether this is useful heuristic). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow betaiota when checking unification of the types of metas (fixes ATBR ↵Gravatar msozeau2011-04-20
| | | | | | contrib). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a flag to control betaiota reduction during unification to maintain ↵Gravatar msozeau2011-04-18
| | | | | | backward compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unification of types of metavariables and error message for sort ↵Gravatar msozeau2011-04-16
| | | | | | unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14020 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Remove create_evar_defsGravatar msozeau2011-04-13
| | | | | | - Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Improve unification (beta-reduction, and same heuristic as evarconv for ↵Gravatar msozeau2011-04-13
| | | | | | reducing matches). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13993 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unify meta types with the right flags, add betaiotazeta reduction to ↵Gravatar msozeau2011-04-13
| | | | | | unification (potentially harmful) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proper typing of metavariables, type errors were completely ignored ↵Gravatar msozeau2011-04-13
| | | | | | before... Use sort constraint checking as in evarconv as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13990 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
| | | | | | | | | | | | | | | | conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solve evar instantiations in the right environment.Gravatar msozeau2011-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13899 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
| | | | | | | unification failure messages (it is not fully usable and was not intended to be committed now, sorry for the noise). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
| | | | | | | | error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
| | | | | | | | | | conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
| | | | | | | before the message is delivered to the user. Should avoid useless computation in heavily backtracking tactics (auto, try, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve handling of metas as evars in unification (patch by Hugo)Gravatar letouzey2010-09-30
| | | | | | | Pratical situation: simple eapply foo on a goal ?123, while foo is a (forall f, exists ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13479 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
| | | | | | | governed in the latter case by a flag since (useful e.g. for setoid rewriting which otherwise loops as it is implemented). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-21 00:59:48 +0000