aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
...
| * More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Gravatar Hugo Herbelin2016-06-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When typing a "with clause fails, type classes are used to possibly help to insert coercions. If this heuristic fails, do not consider it anymore to be the best failure since it has made type classes choices which may be inconsistent with other constraints and on which no backtracking is possible anymore (see new example in test suite file 4782.v). This does not mean that using type classes at this point is good. It may find an instance which help to find a coercion, but which might still be a choice of instance and coercion which is incompatible with other constraints. I tend to think that a convenient way to go to deal with the absence of backtracking in inserting coercions would be to have special For the record, here is a some comments of what happens regarding f9695eb4b and 827663982. In the presence of an instance (x:=t) given in a "with" clause, with t:T, and x expected of type T', the situation is the following: Before f9695eb4b: - If T and T' are closed and T <= T' is not satisfiable (no coercion or not convertible), the test for possible insertion of a coercion is postponed to w_merge, even though there is no way to get more information since T ant T' are closed. As a result, t may be ill-typed and the unification may try to unify ill-formed terms, leading to #4872. - If T and T' are not closed and contains evars of type a type class, inference of type classes is tried. If it fails, e.g. because a wrong type class instance is found, it was postponed to w_merge as above, and the test for coercion is retried now interleaved with type classes. After f9695eb4b and 827663982e: - If T and T' are closed and T <= T' is not satisfiable (no coercion or not convertible), the test for possible insertion of a coercion is an immediate failure. This fixes #4872. - However, If T and T' are not closed and contains evars of type a type class, inference of type classes is tried. If it gives closed terms and fails, this is immediate failure without backtracking on type classes, resulting in the problem added here to file 4872.v. The current fix does not consider the result of the use of type classes while trying to insert a coercion to be the last word on it. So, it fails with an error which is not the error for conversion of closed terms (ConversionFailed), therefore in a way expected by f9695eb4b and 827663982e, and the "with" typing problem is then postponed again.
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
| |
* | Typeclasses:rename solve_instantiation* & use HookGravatar Matthieu Sozeau2016-06-16
| |
* | Refine 9cc95f5, unification of Let-In's, bug #3929Gravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | | | We unify types of let-ins in FO heuristic before their bodies, using cumulativity in either direction. This maintains the invariant that we are comparing terms in related types throughout unification. Also adapt test-suite file for bug #3929.
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
| | | | | | | | | | This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase.
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
| * | Allow `Pretyping.search_guard` to not check guardGravatar Arnaud Spiwack2016-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | This is a minimal modification to the pretyping interface which allows for toplevel fixed points to be accepted by the pretyper. Toplevel co-fixed points are accepted without this. However (co-)fixed point _nested_ inside a `Definition` or a `Fixpoint` are always checked for guardedness by the pretyper.
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
| | | | | | | | | | | | | | | | | | | | | The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
* | | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\ \ \ | | |/ | |/|
| * | evar_conv: Refine occur_rigidlyGravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | | | | | | | | This avoids postponing constraints which will surely produce an occur-check and allow to backtrack on first-order unifications producing those constraints directly (e.g. to apply eta). (fixes HoTT/HoTT with 8.5).
| * | Minor simplification in evarconv.Gravatar Hugo Herbelin2016-06-12
| | | | | | | | | | | | | | | | | | Function default_fail was always part of an ise_try. Its associated error message was anyway thrown away. It is then irrelevant and could be made simpler.
| * | Reserve exception "ConversionFailed" in unification for failure ofGravatar Hugo Herbelin2016-06-12
| | | | | | | | | | | | | | | | | | | | | conversion on closed terms. This will be useful to discriminate problems involving the "with" clause and which fails by lack of information or for deeper reasons.
| * | Protecting eta-expansion in evarconv.ml against ill-typed problems.Gravatar Hugo Herbelin2016-06-12
| | | | | | | | | | | | | | | | | | This can happen with the "with" clause (see e.g. #4782), but also with recursive calls in first-order unification (e.g. "?n a a b = f a" when a matching between "b" and "a" is tried before expanding f).
* | | A mini-optimization for free in unification.ml: test in O(1)Gravatar Hugo Herbelin2016-06-10
| | | | | | | | | | | | complexity comes before tests in O(n) complexity.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\| |
| * | Fixing #4644 (regression of unification on evar-evar problems with a match).Gravatar Hugo Herbelin2016-06-09
| | | | | | | | | | | | | | | Typically, a problem of the form "?x args = match ?y with ... end" was a failure even if miller-unification was applicable.
| * | Minor simplification in evarconv.ml.Gravatar Hugo Herbelin2016-06-09
| | |
| * | Reverting dbdff037 which does not seem to prevent to have #3638 fixedGravatar Hugo Herbelin2016-06-09
| | | | | | | | | | | | | | | on the contrary of message given in 23041481f, while it introduces a square time complexity of the size of the goal in subterm finding.
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
|\| |
* | | More informative error message when interpreting ltac variables in terms.Gravatar Pierre-Marie Pédrot2016-05-13
| | |
| * | Small optimization in evar resolution.Gravatar Pierre-Marie Pédrot2016-05-12
| | | | | | | | | | | | | | | Instead of rebuilding a whole set of evars just to make a typeclass filter, we use the source evarmap.
* | | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
| | |
* | | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| |
| * | Use the canonical name when looking for an eliminator (bug #4670).Gravatar Guillaume Melquiond2016-05-03
| | | | | | | | | | | | Disclaimer: I have no idea what I am doing.
| * | Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Gravatar Guillaume Melquiond2016-05-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When encountering a "simpl nomatch" constant, the reduction machinery tries to unfold it. If the subsequent partial reduction does not produce any match construct, it keeps going from the reduced term. Unfortunately, the reduced term has been refolded in the meantime, which means that some of the previous reduction steps have been canceled, thus causing an infinite loop. This patch delays the refolding till the very end, so that reduction always progresses. Disclaimer: I have no idea what I am doing here. The patch compiles the standard library and the test suite properly, so hopefully they contain enough tests to exercise the reduction machinery.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\| |
| * | Fix incorrect cbv reduction of primitive projections. (Bug #4634)Gravatar Guillaume Melquiond2016-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As noticed by Cyprien Mangin, projected terms cannot directly be used as head values. Indeed, they might be applications (e.g. constructors as in the bug report) whose arguments would thus be missing from the evaluation stack when doing any iota-reduction step. The only case where it would make sense is when the evaluation stack is empty, as an optimization. Indeed, in that case, the arguments are put on the stack, and then immediately put back inside the term.
* | | Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | This reverts commit 7e613daf7c71a4180725bddb40151c2b5a6348f4.
* | | Revert "More abstraction in cases.mli."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | This reverts commit 975e2a05050c704161aca3fbac96376eeda6fb4a.
* | | Revert "Add support for generalization also on named variables in ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | pattern-matching" This reverts commit be80899499094fc8a15362931e3cec650f2fb14e.
* | | Revert "Add support for deep dependencies in variables within the recursive ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | structure." This reverts commit eaca8dadf7dd8152a86f4fc75631754344268dbf.
* | | Revert "Fixing a De Bruijn bug in computing return predicate by inversion."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | This reverts commit 94e9e28ebaa33e11164ca07f225d998ca7f8e52c.
* | | Revert "Using existing names as a basis for the inner names of the ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | pattern-matching produced by an implicit "in" clause" This reverts commit ba9f53314ff6132d0013e53879395e0dc9d8038c.
* | | Revert "Vers un filtrage profond ..."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | This reverts commit d9f0daefb437955df8102de2b3c4c31749b6946e.
* | | Vers un filtrage profond ...Gravatar Hugo Herbelin2016-04-27
| | |
* | | Using existing names as a basis for the inner names of the pattern-matching ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | produced by an implicit "in" clause
* | | Fixing a De Bruijn bug in computing return predicate by inversion.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Add support for deep dependencies in variables within the recursive structure.Gravatar Hugo Herbelin2016-04-27
| | |
* | | Add support for generalization also on named variables in pattern-matchingGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | algorithm.
* | | More abstraction in cases.mli.Gravatar Hugo Herbelin2016-04-27
| | |
* | | When interpreting "match goal with ... end" in ltac, expand evars byGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | need at matching time rather than eagerly at the beginning of the call to "match". To be done for other constructs too, e.g. "match term with ... endp".
* | | Fixing a "This clause is redundant" error when interpreting the "in"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | clause of a "match" over an irrefutable pattern.
| * | Optimization in building a return clause by pattern-matching: do notGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | build a default case if the pattern is irrefutable. It did not matter in practice because we did not check for unused clauses in this case.
* | | Merging the ML tactic notation and plain Tactic Notation mechanisms.Gravatar Pierre-Marie Pédrot2016-04-25
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\| |
| * | Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
| | | | | | | | | | | | | | | while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion).
| | * Revert "Prevent pretyping from checking well-guardedness unnecessarily."Gravatar Arnaud Spiwack2016-04-05
| | | | | | | | | | | | This reverts commit 9f4e67a7c9f22ca853e76f4837a276a6111bf159.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:53:01 +0000