aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarsolve.ml
Commit message (Collapse)AuthorAge
* Optimize occur_evar_upto_types, avoiding repeateadly looking into theGravatar Matthieu Sozeau2015-12-11
| | | | same evar.
* Fix bug #4293: ensure let-ins do not contain algebraic universes inGravatar Matthieu Sozeau2015-11-11
| | | | their type annotation.
* Univs: missing checks in evarsolve with candidates and missing aGravatar Matthieu Sozeau2015-11-04
| | | | whd_evar in refresh_universes.
* Univs: compatibility with 8.4.Gravatar Matthieu Sozeau2015-11-04
| | | | | When refreshing a type variable, always use a rigid universe to force the most general universe constraint, as in 8.4.
* Refresh rigid universes as well, and in 8.4 compatibility mode,Gravatar Matthieu Sozeau2015-11-02
| | | | make them rigid to disallow minimization.
* Fix lemma-overloadingGravatar Matthieu Sozeau2015-10-20
| | | | | | Update the evar_source of the solution evar in evar/evar problems to propagate the information that it does not necessarily have to be solved in Program mode.
* Do occur-check w.r.t existential's types also when instantiating an evar.Gravatar Matthieu Sozeau2015-10-19
|
* Occur-check in evar_define was not strong enough.Gravatar Matthieu Sozeau2015-10-14
|
* Fix rechecking of applications: it can be given ill-typed terms. Fixes ↵Gravatar Matthieu Sozeau2015-10-12
| | | | math-classes.
* Univs: Fix part of bug #4161Gravatar Matthieu Sozeau2015-10-02
| | | | Rechecking applications built by evarconv's imitation.
* Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).Gravatar Hugo Herbelin2015-07-16
| | | | This is a bug in a pretty old code, showing also in 8.3 and 8.4.
* Fixing bug #4240 (closure_of_filter was not ensuring refinement ofGravatar Hugo Herbelin2015-07-16
| | | | | former filter after 48509b61 and 3cd718c, because filtered let-ins were not any longer preserved).
* Fix bug #4101, noccur_evar's expand_projection can legitimately failGravatar Matthieu Sozeau2015-03-03
| | | | when called from w_unify, so we protect it.
* Fix bug introduced by my last commit, forgetting to adjust de BruijnGravatar Matthieu Sozeau2015-03-03
| | | | index lookup.
* Fix bug #4097.Gravatar Matthieu Sozeau2015-03-02
|
* Still continuing cf6a68b45, d64b5766a and 2734891ab7e on integratingGravatar Hugo Herbelin2015-02-25
| | | | | ensure_evar_independent into is_constrainable_in (a simpler approach closest to what existed before cf6a68b45).
* Optimizing noccur_evar wrt expansion of let-ins (fix for variant of #4076).Gravatar Hugo Herbelin2015-02-25
|
* An optimization on filtering evar instances with let-ins suggested byGravatar Hugo Herbelin2015-02-25
| | | | | | | | | | | | | | | | | | | inefficiency #4076. In an evar context like this one x:X, y:=f(x), z:Z(x,y) |- ?x : T(x,y,z) with unification problem a:A, b:=f(t(a)) |- ?x[x:=t(a);y:=b;z:=u(a,b)] = v(a,b,c) we now keep y after filtering, iff the name b occurs effectively in v(a,b,c), while before, we kept it as soon as its expansion f(t(a)) had free variables in v(a,b,c), which was more often, but useless since the point in keeping a let-in in the instance is precisely to reuse the name of the let-in while unifying with a right-hand side which mentions this name.
* Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a onGravatar Hugo Herbelin2015-02-24
| | | | integrating ensure_evar_independent into is_constrainable_in.
* Compensating 6fd763431 on postponing subtyping evar-evar problems.Gravatar Hugo Herbelin2015-02-23
| | | | | | | Pushing pending problems had the side-effect of later solving them in the opposite order as they arrived, resulting on different complexity (see e.g. #4076). We now take care of pushing them in reverse order so that they are treated in the same order.
* Fixing cf6a68b45 on integrating ensure_evar_independent into ↵Gravatar Hugo Herbelin2015-02-23
| | | | is_constrainable_in.
* Removing need for ensure_evar_independent by passing a force flag to ↵Gravatar Hugo Herbelin2015-02-21
| | | | is_constrainable_in to do the job of ensuring that ?p does not belong to the ti while solving ?p[...]:=?n[t1..tn].
* When looking for restrictions in ?n=?p problems, keep the type of let-bindings.Gravatar Hugo Herbelin2015-02-19
| | | | | | | | | | | | Bindings of the form [let x:T := M] are unfolded into [(M:T)], so that occur-check is done in [T] as well as in [M] (except when [M] is a variable, where it is hopefully not necessary). This is a way to fix #4062 (evars with type depending on themselves). The fix modifies the alias map (make_alias_map) but it should behave the same at all places using alias maps other than has_constrainable_free_vars.
* Univs: fix bug #3755. We were missing refreshements of universes inGravatar Matthieu Sozeau2015-02-14
| | | | unifications ?X ~= ?Y foo not catched by solve_evar_evar.
* Fixing #3997 (occur-check in the presence of primitive projections, patchGravatar Hugo Herbelin2015-02-12
| | | | from Matthieu).
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Not "Setting ?n=?p order to ?p:=?n to see if it solves someGravatar Hugo Herbelin2015-01-12
| | | | | | | incompatibilities wrt 8.4.", as it creates other problems (in Ergo and Compcert). This reverts commit bf388dfec041ab0fa74ae5d484600f6fcf515e4f.
* Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ↵Gravatar Hugo Herbelin2015-01-08
| | | | 8.4.
* Fixing 48509b61 which improved unification as expected but actuallyGravatar Hugo Herbelin2015-01-03
| | | | | | not using the intended test. By fixing the intended test, the need for a delta-expansion resulting from this commit in PFsection6.v (line 1255) of ssreflect disappears.
* Fixing #3895 (thanks to PMP for diagnosis).Gravatar Hugo Herbelin2015-01-03
|
* Back to the preferred ?n1:=?n2 order of evar-evar unification which got ↵Gravatar Hugo Herbelin2014-12-19
| | | | accidentally mixed up in 9aa416c0c6.
* Tentatively starting to use heuristics for evar-evar resolution: firstGravatar Hugo Herbelin2014-12-15
| | | | | | | | | | step, prefer QuestionMark's to other evars, to comply with the filtering made on VarInstance, GoalEvar and QuestionMark for type class resolution. Maybe evars to be resolved by type class instances should eventually be marked with a specific tag. At least, this solves the current problem with compiling cancel2.v in LemmaOverloading.
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
|
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
| | | | in reporting the chain of causes when unification fails.
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
| | | | pattern-matching predicate.
* Fixing orientation of postponed subtyping problems.Gravatar Hugo Herbelin2014-12-10
| | | | | | | | | | | In the case of conversion, postponing by preserving the initial orientation. Was wrong from its initial version in Jan 2014, but was not visible because evar-evar subtyping was approximated by evar-evar conversion. Thanks to Enrico for a very short example highlighting the problem. In particular, this fixes Ergo.
* Using a more aggressive test for resolving pattern equations ?n = ?p:Gravatar Hugo Herbelin2014-12-10
| | | | | | test pattern-unification after restriction of the evars so as to succeed earlier (no observational changes however in the examples at my disposal).
* Improved criterion for evar restriction in the configurationGravatar Hugo Herbelin2014-12-08
| | | | ?n[...] = ?p[...;x:=?n[...];...]. Indeed, x could be a solution for ?p.
* Improving evar restriction (this is a risky change, as I remember aGravatar Hugo Herbelin2014-12-07
| | | | | | | | similar optimization broke at some time some ssreflect code; we now treat the easy case of a let-in to a rel - a pattern common in pattern-matching compilation -; later on, we shall want to investigate whether any let-in found to refer to out of scope rels or vars can be filtered out).
* Improved tracking of the origin of evars.Gravatar Hugo Herbelin2014-12-07
|
* Had forgotten some debugging printer.Gravatar Hugo Herbelin2014-12-07
|
* New approach to deal with evar-evar unification problems in differentGravatar Hugo Herbelin2014-12-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | types: we downcast the evar in the higher type to the lower type. Then, we have the freedom to choose the order of instantiation according to the instances of the evars (e.g. choosing the instantiation for which pattern-unification is possible, if ever it is possible in only one way - as shown by an example in contribution Paco). This still does not preserve compatibility because it happens that type classes resolution is crucially dependent on the order of presentation of the ?n=?p problems. Consider e.g. an example taken from Containers. Both now and before e2fa65fccb9, one has this asymmetry: Context `{Helt : OrderedType elt}. Check forall x y r l h, @Equivalence.equiv _ _ _ x y -> In x (Node l x r h). --> @Equivalence.equiv QArith_base.Q QArith_base.Qeq QArith_base.Q_Setoid x y Context `{Helt : OrderedType elt}. Check forall x y r l h, In x (Node l x r h) -> @Equivalence.equiv _ _ _ x y. --> @Equivalence.equiv elt (@_eq elt Helt) (@OT_Equivalence elt Helt) Then, embedding this example within a bigger one which relies on the ?n=?n' resolution order, one can get two incompatible resolution of the same problem. To be continued...
* In solve_evar_evar, orient the heuristic over arities with differentGravatar Hugo Herbelin2014-12-03
| | | | | | types as it was before commit 710bae2a8c81a44. There is still at least one problem with bug #3392 to solve.
* When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifGravatar Hugo Herbelin2014-12-02
| | | | | | | | | | | possible, which is the "natural" way to orient an equation. At least it matters for matching subterms against patterns, so that it is the pattern variables which are substituted if ever the subterm has itself existential variables, as in: Goal exists x, S x = x. eexists. destruct (S _).
* Postponing the "evar <= evar" problems instead of solving them in anGravatar Hugo Herbelin2014-12-02
| | | | arbitrary direction as if it were an "evar = evar" problem.
* Being more scrupulous on preserving subtyping in evar-evar problems.Gravatar Hugo Herbelin2014-12-02
| | | | | Incidentally, this allows to make earlier the collapse of CUMUL to CONV when force is true.
* Being consistent in making arbitrary choices in recursive calls toGravatar Hugo Herbelin2014-12-02
| | | | | | | | | evar_define. Interestingly, the added choose in evarconv.ml allows solve_evar_evar to be observationally commutative, in the sense of not either fail or succeed in compiling the stdlib whether problems are given in the left-to-right or right-to-left order.
* Resolution of evar/evar problems: removed a test which should beGravatar Hugo Herbelin2014-12-02
| | | | subsumed by the call to project_evar_on_evar.
* Fixing #3634 (wrong env in "cannot instantiate because not in itsGravatar Hugo Herbelin2014-10-03
| | | | scope" error message).
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
| | | | | | | | | potentially different types, resulting in ill-typed terms due to eta. Projection expansion now fails gracefully on retyping errors. The proper fix to unification, checking that the heads for FO have unifiable types, is currently too strong, adding unnecessary universe constraints, so it is disabled for now. It might be quite expensive too also it's not noticeable on the stdlib.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:53:18 +0000