aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.ml
Commit message (Collapse)AuthorAge
* More cleaningGravatar ppedrot2012-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrects a bug in the refine tactic which could drop evar bodies.Gravatar aspiwack2012-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15205 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a "Not_Found" bug related to commit 15061 on the use of evar candidates.Gravatar herbelin2012-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15184 85f007b7-540e-0410-9357-904b9bb8a0f7
* Speedup free_vars_and_rels_up_alias_expansion (evarconv)Gravatar gareuselesinge2012-04-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Small cache to avoid checking the same Rel or Var twice. Consider an unification problem like the following one: a := huge b := F1 a + F2 a c := G1 b + G2 b =============== ?i[c,b,a] == ?g[c,c,c] The old code, as the "not optimal" comment was suggesting, did process every item in the explicit substitution, even duplicated ones, unfolding the letins over and over. This was the cause of the huge slowdown in the definition of cormen_lup in Ssreflect/theories/matrix.v, that follows: Fixpoint cormen_lup {n} := match n return let M := 'M[F]_n.+1 in M -> M * M * M with | 0 => fun A => (1, 1, A) | _.+1 => fun A => let k := odflt 0 [pick k | A k 0 != 0] in let A1 : 'M_(1 + _) := xrow 0 k A in let P1 : 'M_(1 + _) := tperm_mx 0 k in let Schur := ((A k 0)^-1 *: dlsubmx A1) *m ursubmx A1 in let: (P2, L2, U2) := cormen_lup (drsubmx A1 - Schur) in let P := block_mx 1 0 0 P2 *m P1 in let L := block_mx 1 0 ((A k 0)^-1 *: (P2 *m dlsubmx A1)) L2 in let U := block_mx (ulsubmx A1) (ursubmx A1) 0 U2 in (P, L, U) end. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15116 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification: Fixing bug in materialize_evar (spotted by MathClasses).Gravatar herbelin2012-03-26
| | | | | | Also fixed apparent other bug in the presence of let-ins. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification: Added a heuristic to solve problems of the formGravatar herbelin2012-03-26
| | | | | | | | | | | | | | | | | | ?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to know if it occurs in rigid position or not. Such equations typically come from matching problems such as "match a return ?T[a] with pair a1 a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified with ?A. This possible dependency is kept since commits r15060-15062. The heuristic is to restrict ?T so that the dependency is removed, leading to a behavior similar to the one existing before these commits. This allows BGsection15.v, from contrib Ssreflect, to compile as it did before these commits. Also, removed one function exported without true need in r15061. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Little bug in r15061 leading to unusable debug mode.Gravatar herbelin2012-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use a careful analysis of dependencies in restricting instances toGravatar herbelin2012-03-20
| | | | | | | | | | | | | solve the following kind of code broken by being less restrictive on projecting: Set Printing Existential Instances. Parameter f : forall x, x=0 -> x=0 -> x=1 /\ x=2. Parameter g : forall y, y=0 /\ y=0. Check match g _ with conj a b => f _ a b end. (* and the return clause should not depend on the "_" *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15064 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep aGravatar herbelin2012-03-20
| | | | | | | | candidate for the possible projection (as was introduced in 8.4beta) but try also to imitate (as was done before 8.4beta but not done in 8.4beta). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15062 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized the use of evar candidates in type inference unification:Gravatar herbelin2012-03-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - use evar candidates instead of postponed conversion problems when it is known (according to the projection heuristic used) that an evar has only a fixed number of possible instances (as e.g. in equation ?n[x,x] = x, with x a variable); - this allows to be more robust in solving remaining problems: if several instanciations exist, and one is not compatible with a previous instantiation made among several choices for another evar, backtracking is now possible; - this allows in particular to fix regression #2670 (two postponed conversion problems solved in an inconsistent way); - but this requires more code. At the same time, a refactoring of the code has been made so as to hopefully clarify the elementary pieces of the algorithm. For instance, there are now generic functions for both applying a filter and giving candidates. The filter is systematically generalized so as to have the ccl of the evar well-typed even in situations where we could try on the contrary to restrict the evars occurring in the ccl. Anyway, when the representation of instances will be optimized using identity substitutions, it will no longer be useful to use the filter to shorten the size of the instances. Then, the filters will have, like candidates, the only role of restricting the search space for potential solutions to the unification problems. Also, solve_refl can now be used to restrict equations ?x[t1..tn]=?x[u1..un] up to conversion instead of up to unification. This (potententially) looses constraints but this avoids looping at the time of considering remaining problems and applying heuristics to them. Also added printing of evar candidates in debugging evar printers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganizing the structure of evarutil.ml (only restructuration, noGravatar herbelin2012-03-20
| | | | | | change of semantics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 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
* Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and ↵Gravatar msozeau2012-02-15
| | | | | | us are not convertible git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14980 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* Partly reverting r14539 about fully expanding "let-in"s and not justGravatar herbelin2011-10-17
| | | | | | | | | | | | | | 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
* 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
* Applied the trick of Chung-Kil Hur to solve second-order matchingGravatar herbelin2011-10-10
| | | | | | | 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
* Fixing buggy abberant code for Evarutil.expand_evarGravatar herbelin2011-10-10
| | | | | | 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
* Passed conv_algo to evar_define and move call to solve_refl toGravatar herbelin2011-10-10
| | | | | | | | | | | | | | 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
* Fix nf_evars_undefinedGravatar msozeau2011-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: replace generic list_distinct on constr by constr_list_distinctGravatar puech2011-07-29
| | | | | | This new function is a copy of Util's one, but working on Constrhash git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14365 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: replaced some generic = on constr by destructorsGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: generic equality on constr replaced by destructorsGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: generic equality on constr replaced by eq_constr (x2)Gravatar puech2011-07-29
| | | | | | added array_equal in Util git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarutil: generic equality on constr replaced by eq_constrGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14318 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
* Fixes in pruning, do not fail if pruning is impossible due to typing ↵Gravatar msozeau2011-06-10
| | | | | | constraints but postpone evar-evar problems git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14176 85f007b7-540e-0410-9357-904b9bb8a0f7
* More fixes in pruning/restriction of evars during unification.Gravatar msozeau2011-06-09
| | | | | | | | - Do not allow to filter variables that appear in the conclusion of an evar. - Do not attempt to restrict evars based on a substitution that does not contain only evars (fall back to the pattern fragment and do not lose solutions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14174 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in pruning in unification.Gravatar msozeau2011-06-08
| | | | | | | | | Properly normalize evars to reflect the already pruned evars in the type of dependent evars to allow more precise restriction of hyps. Directly check the type of an evar instance, allowing backtracking on ill-typed instanciations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14169 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix restrict_hyps to not allow filtering on a variable required to ↵Gravatar msozeau2011-06-07
| | | | | | | | | typecheck the evar's conclusion - Prevent extend_evar from creating ill-formed evars with de Bruijn-open conclusions. - Minor fix of define_evars_as_lambda, another mixup of named and de Bruijn indices. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14163 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
| | | | | | | - Fix pretyping to consider remaining unif problems with the right transparency information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13996 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
* Catch NotArity exception and transform it into an anomaly in retyping.Gravatar msozeau2011-04-11
| | | | | | | | | | Add a temporary fix in solve_simple_eqn to catch anomalies coming from retyping because the unification algorithm with metas doesn't respect the precondition that evar instances should be well-typed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13985 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix solve_simpl_eqn which was cheking instances types in the wrong ↵Gravatar msozeau2011-03-23
| | | | | | | | environment sometimes. - Remove compilation warning in classes.ml due to (as yet) unused code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13924 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
| | | | | | | | | | | | | evar, and simultaneously make type inference with universes work better. This only exports more functions from kernel/univ, to be able to work with a set of universe variables during type inference. Universe constraints are gradually added during type checking, adding information necessary e.g. to lower the level of unknown Type variables to Prop or Set. There does not seem to be a disastrous performance hit on the stdlib, but might have one on some contribs (hence the "Tentative"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Better error messages taking unif. constraints into account.Gravatar msozeau2011-03-11
| | | | | | | - Normalize evars in typeclasses eauto also before [intro]. - Disallow use of nf_evars variants that drop unif. constraints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13904 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 18:52:38 +0000