aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
...
* 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.
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
|
* Reverting the tentative try to restore the use of second-orderGravatar Hugo Herbelin2015-01-07
| | | | | | typed-based matching: it provokes a stack overflow in contrib ClassicalRealisability. To be investigated later on. (See 893a02f643858ba0b0172648e77af9ccb65f03df.)
* Propagating the relaxing of filtering started in 48509b6, fixed inGravatar Hugo Herbelin2015-01-06
| | | | 3cd718c, to the case of second_order_matching.
* Fixing old filter bug in second_order_matching.Gravatar Hugo Herbelin2015-01-06
|
* 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.
* Tentatively trying to restore the use of second-order typed-basedGravatar Hugo Herbelin2015-01-03
| | | | | | unification algorithm in consider_remaining_unif_problems. If it happens to be problematic, one can backtrack to the "optimization" from 3bd9cb26b which has a restriction on rels/vars.
* Fixing #3895 (thanks to PMP for diagnosis).Gravatar Hugo Herbelin2015-01-03
|
* An optimization in the use of unification candidates so as to get theGravatar Hugo Herbelin2015-01-01
| | | | | | following working: Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a.
* Simplifying second_order_matching: no need to invert the linearGravatar Hugo Herbelin2014-12-30
| | | | initial segment of the context of the evar.
* When pretyping [uconstr] closures, don't use the local Ltac variable ↵Gravatar Arnaud Spiwack2014-12-19
| | | | | | | environment. A closure is supposedly closed: all the relevant Ltac variables should be then. The last field [ltac_genargs], if I'm not mistaken, is there to represent the Ltac variables which are bound but not to something which makes sense in a term. They should be irrelevant at this point, since the uconstr has already been interpreted and these checks are supposed to have happened. (though I'm not entirely sure they do, it can be an interesting exercise to try and make [uconstr] behave weirdly) I'm not quite sure why it caused #3679, though. But it still seems to be solved.
* Back to the preferred ?n1:=?n2 order of evar-evar unification which got ↵Gravatar Hugo Herbelin2014-12-19
| | | | accidentally mixed up in 9aa416c0c6.
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
* Fix for #3154: use CUnix.sys_command to call native compiler.Gravatar Maxime Dénès2014-12-16
| | | | | Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra care with cmd.exe vs sh is no longer required.
* 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.
* New try on Fixing an evar_map bug revealed by commit 603b66f81 onGravatar Hugo Herbelin2014-12-15
| | | | unification flags (see also temporary revert in d083200ae5b).
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
|
* Fix merging of name maps in union of universe contexts.Gravatar Matthieu Sozeau2014-12-14
|
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
| | | | You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
| | | | | | | | - In evarconv, check_conv_record properly computes the parameters of primitive record projections for later unification, adding env and sigma as arguments. - In unification, backtrack on pattern-unification and not only application unification if eta for a record failed.
* Commit not ready. Sorry.Gravatar Hugo Herbelin2014-12-11
| | | | | | Revert "Fixing an evar_map bug revealed by commit 603b66f81 on unification flags." This reverts commit d083200ae5b391ceffaa0329a8e3a334036c7968.
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
| | | | in reporting the chain of causes when unification fails.
* Fine-tuning unification error (using OccurCheck in evarconv).Gravatar Hugo Herbelin2014-12-11
|
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
| | | | pattern-matching predicate.
* Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Gravatar Hugo Herbelin2014-12-11
| | | | This fixes current failure of RelationAlgebra.
* 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).
* Setup hook to change the unification algorithm used by evarconv,Gravatar Matthieu Sozeau2014-12-09
| | | | e.g. for MTac.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* Fixing wrong evar_map in return clause inference, revealed by 48509b611.Gravatar Hugo Herbelin2014-12-08
|
* 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
|
* More consistent printing of evars in evar_map debugging printer.Gravatar Hugo Herbelin2014-12-05
|
* Fix debugger Tactic Unification.Gravatar Hugo Herbelin2014-12-05
|
* Small cleaning and uniformization in unification flags:Gravatar Hugo Herbelin2014-12-05
| | | | | | | | | | - new function set_flags_for_type for setting flags when converting types of the terms to unify - it now sets all conversion flags, possibly restricting delta using modulo_delta_types - it is now used in w_unify_core_0 too - fixing/improving documentation of options - deprecating "Set Tactic Evars Pattern Unification"
* 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...
* Occur-check in refine.Gravatar Arnaud Spiwack2014-12-04
| | | | | | | | | | The occur check is done even if the flag [unsafe] is set to true. The rational is that a tactic cannot control where it takes pieces of terms from (and hence will not generally make terms which pass the occur-check), and it would be painful to ask every tactic which takes a term as an argument to do an occur check before [refine]. I reused the same error than used by unification. It gives a pretty nice error message. An alternative would be to have a dedicated error with pretty much the same error message. I'm not sure which is best, so I went for the simplest one. The same check is done in the compatibility layer. Fixes a reported bug which I cannot locate for some reason.
* Reactivating option "Set Printing Existential Instances" for asking printing ↵Gravatar Hugo Herbelin2014-12-04
| | | | full instances.
* 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.
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
| | | | | | | | | | | - Registering strict implicit arguments systematically (35fc7d728168) - Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6) - Fixing Coq compilation (894a3d16471) Systematically computing strict implicit arguments can lead to big computations, so I suspend this attempt, waiting for improved computation of implicit arguments, or alternative heuristics going toward having more conversion in rewrite.
* Fixing Coq compilation.Gravatar Pierre-Marie Pédrot2014-11-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:28:59 +0000