aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
| | | | | | | | | | | - reinstall (x : T | P) binder syntax extension. - fix a wrong Evd.define in coercion code. - Simplify interface of eterm_obligations to take a single evar_map. - Fix a slightly subtle bug related to resolvability of evars: some were marked unresolvable and never set back to resolvable across calls to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes bug: #2692 (Arguments/simpl off by 1)Gravatar gareuselesinge2012-03-19
| | | | | | | simpl was accessing the reduction stack at position n when the length of the stack was exactly n. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arguments/simpl: allow ! even on non fixpointsGravatar gareuselesinge2012-03-19
| | | | | | | | | | | | | | | It is now possible to tell simpl to unfold a constant that hides no "match" but is applied to concrete arguments. Arguments id _ !n. Goal forall x, id x = id 2. intros; simpl. x : nat ======== id x = 2 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix merge and add missing file.Gravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revise API of understand_ltac to be parameterized by a flag for resolution ↵Gravatar msozeau2012-03-14
| | | | | | | | | of evars. Used when interpreting a constr in Ltac: resolution is now launched if the constr is casted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge fixesGravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15037 85f007b7-540e-0410-9357-904b9bb8a0f7
* Everything compiles again.Gravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 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
* A bit of cleaning: unifying push_rels and push_rel_context.Gravatar herbelin2012-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15031 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
| | | | | | | | did not handle let-ins and was wrongly specified). Thanks to Pierre Boutillier and Pierre-Marie Pédrot for pointing out the source of the bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Glob_term.predicate_pattern: No number of parameters with letins.Gravatar pboutill2012-03-02
| | | | | | | | | Detyping is wrong about it and as far as I understand no one but Constrextern uses it. Constrextern has now the same machinery for all patterns. Revert if I miss something. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15022 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
| | | | | | | | This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf. An other wrong externalize function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 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
* Univ: a univ_depends function to avoid a hack in InductiveopsGravatar letouzey2012-03-01
| | | | | | | | | | | univ_depends checks whether a universe variable appears or is equal to a universe. In comparison with the previous hack in inductiveops based on try...catching UniverseInconsistency, this should be semantically equivalent, simplier, and more robust in case we allow someday an unsafe mode where merge_constraints would be a no-op. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15013 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
* Bug #2041: unfold at betaiotaZETA normalize like unfoldGravatar pboutill2012-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an pattern / occurence syntax for vm_compute.Gravatar ppedrot2012-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Printing bugs with match patterns:Gravatar herbelin2012-01-27
| | | | | | | | | | | - namegen.ml: if a matching variable has the same name as a constructor, rename it, even if the conflicting constructor name is defined in a different module; - constrextern.ml: protect code for printing cases as terms are from requesting info in the global env when printers are called from ocamldebug since the global env is undefined in this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for Program Instance not separately checking the resolution of evars of ↵Gravatar msozeau2012-01-23
| | | | | | the type (mandatory) and the fields (optional) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductiveops.nb_*{,_env} cleaningGravatar pboutill2012-01-16
| | | | | | | - Functions without _env use the global env. - More comments about when letin are counted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14908 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
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
| | | | | | | unfolded fixpoints when calling destruct). However, this might break compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 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
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
| | | | | | | | | | as to ensure the warning is flushed in real time. Made systematic the use of if_warn instead of if_verbose when the warning is intended to signal something anormal (if_warn is activated when compiling verbosely and when working interactively while if_verbose is activated only when working interactively and when loading verbosely). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14803 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
* Fixing a bug of commit r13310 (activating coercions only when moduleGravatar herbelin2011-12-07
| | | | | | | is imported): in case of nested modules, activation was done as soon as the outermost module was imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14775 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on synchronizing universe counter with resetGravatar herbelin2011-12-06
| | | | | | mechanism, section discharge is not ready for that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14765 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
* Fixed a small regression in pattern-matching compilation introduced inGravatar herbelin2011-12-04
| | | | | | | | | r14737 (when to expand an alias). However, the heuristic remains different as before r14737 since we stopped taking into account the dependency in the predicate to take the decision of expanding or not. Let's see if we can eventually fine-tuning this. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14760 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
* Finally used typing to decide whether an alias needs to be expanded orGravatar herbelin2011-11-28
| | | | | | | | | not in pattern-matching compilation. Also extended to the Var case the preference given to using the term to match as alias rather than its expansion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14737 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing dependencies postprocessing bug in pattern-matching compilation.Gravatar herbelin2011-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14736 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug in postprocessing dependencies in pattern-matching compilationGravatar herbelin2011-11-26
| | | | | | | (bug was introduced in r14703 when postprocessing started to traverse inner cases). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14732 85f007b7-540e-0410-9357-904b9bb8a0f7
* avoid relying on weak invariant in cbv.mlGravatar bgregoir2011-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14728 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
* 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
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
| | | | | | | | Example: Arguments eq_refl {B y}, [B] y. Check (eq_refl (B := nat)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Configurable simpl tacticGravatar gareuselesinge2011-11-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The problem that this patch tries to solve is that sometimes the unfolding behaviour of simpl is too aggressive, frequently exposing match constructs. Moreover one may want some constants to never be unfolded by simpl (like in the Math-Comp library where the nosimpl hack is pervasive). Finally, one may want some constants to be volatile, always unfolded by simple when applied to enough arguments, even if they do not hide a fixpoint or a match. A new vernacular command to be indroduced in a following patch attaches to constants an extra-logical piece of information. It declares wich arguments must be checked to evaluate to a constructor before performing the unfolding of the constant (in the same spirit simpl considers as such the recursive argument of an inner fixpoint). Examples: Arguments minus !x !y. (* x and y must evaluate to a constructor for simpl to unfold minus *) (S x - y) --- simpl ---> (S x - y) (S x - S y) --- simpl ---> (x - y) Definition fcomp A B C (f : B -> C) (g : A -> B) x := f (g x). Arguments fcomp A B C f g x /. Infix "\o" := fcomp (at level 50, left associativity) : nat_scope. (* fcomp hides no fix, but simpl will unfold if applied to 6 arguments *) (fun x => (f \o g) x) = f \o g --- simpl ---> (fun x => f (g x)) = f \o g Arguments minus x y : simpl never. (* simpl will never unfold minus *) (S x - S y) --- simpl ---> (S x - S y) Definition nid (x : nat) := x. Arguments nid / x. (* nid is volatile, unfolded by simpl when applied to 0 or more arguments *) nid --- simpl ---> (fun x => x) Arguments minus x y : simpl nomatch. (* triggers for minus the "new" simpl heuristic I discussed with Hugo: if reducing the fix would leave a match in "head" position then don't unfold a suggestion for a better name (for "nomatch") would be appreciated *) (0 - y) --- simpl ---> 0 (S x - y) --- simpl ---> (S x - y) (S x - S y) --- simpl ---> (x - y) (minus 0) --- simpl ---> (minus 0) (* This last test does not work as one may expect, i.e. (minus 0) --- simpl ---> (fun _ => 0) The point is that simpl is implemented as "strong whd_simpl" and after unfolding minus you have (fun m => match 0 => 0 | S n' => ...n' - m'... end) that is already in whd and exposes a match, that of course "strong" would reduce away but at that stage we don't know, and reducing by hand under the lambda is against whd reduction. So further discussion on that idea is needed. *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extend the computation of dependencies in pattern-matching compilationGravatar herbelin2011-11-21
| | | | | | | | | | | | | | | | | | | to the dependencies in the real arguments (a.k.a. indices) of the terms to match. This allows in particular to make the example from bug report #2404 work. TODO: move the computation of dependencies in compile_branch at the time of splitting a branch (where the computation is done now, it does not allow to support dependent matching on the second argument of a constructor of type "forall b, (if b then Vector.t n else nat) -> Vector.t n -> foo"). TODO: take dependencies in Var's into account and take dependencies within non-Rel arguments also into account (as in "match v (f t) with ... end" where v is a Var and the type of (f t) depends on it). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add matching on non-inductive types in building an inversion problemGravatar herbelin2011-11-21
| | | | | | | for finding the initial predicate, since their type can be dependent on previous terms to match and they may have to be generalized. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Old naming bug in pattern-matching compilation: names in theGravatar herbelin2011-11-21
| | | | | | | | pattern-matching problem generated for the return clause were not the name of patterns (no counter-example though, revealed by using generalization more intensively). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14709 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inlining let-in (i.e. trace of aliases) in extract_predicate for whatGravatar herbelin2011-11-21
| | | | | | | | seems to provide a better rendering in pattern-matching compilation. Did it also in compile_generalization but not sure the uj_typ is not dropped anyway. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14708 85f007b7-540e-0410-9357-904b9bb8a0f7
* In pattern-matching compilation, now taking into account the dependenciesGravatar herbelin2011-11-21
| | | | | | | between initial arguments (if not rel). Predicate now assumed dependent by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14706 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimizing the compilation of unused aliases in pattern-matching.Gravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifying history management in pattern-matching compilation.Gravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14704 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 16:49:18 +0000