aboutsummaryrefslogtreecommitdiff
path: root/interp/implicit_quantifiers.ml
AgeCommit message (Collapse)Author
2008-07-04Fixes in handling of implicit arguments:msozeau
- Now [ id : Class foo ] makes id an explicit argument, and [ Class foo ] is equivalent to [ {someid} : Class foo ]. This makes declarations such as "Class Ord [ eq : Eq a ]" have sensible implicit args. - Better handling of {} in class and record declarations, refactorize code for declaring structures and classes. - Fix merging of implicit arguments information on section closing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11204 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-21Code cleanup in typeclasses, remove dead and duplicated code.msozeau
Change from named_context to rel_context for class params and fields. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11163 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-12Fix "not an applied typeclass" error for legitimate classesmsozeau
applied to no parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10922 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-06Better parsing of typeclasses, any constr is allowed for ! bindings somsozeau
notations work and bug #1846 gets completely fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10890 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-12Add the ability to specify what to do with free variables in instancemsozeau
declarations. By default, print the list of implicitely generalized variables. Implement new commands Add Parametric Relation/Morphism for... parametric relations and morphisms. Now the Add * commands are strict about free vars and will fail if there remain some. Parametric just allows to give a variable context. Also, correct a bug in generalization of implicits that ordered the variables in the wrong order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10782 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-01Enhance handling of parameters in typeclass constraints: permit to specify ↵msozeau
any typeclass parameter by name anywhere in a typeclass constraint. This allows to share implementations easily and to give any subset of the parameters in any order in the constraints, whereas we are still restricted to a prefix of the typeclass parameters context when using "positional" specifications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10736 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-31- Fix for rewriting under dependent products.msozeau
- Use support for abbreviations with params added by Hugo for inverse. - Standard priorities for operators on relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10733 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
Example: "Notation reflexive R := (forall x, R x x)." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-23Fix a bug found by B. Grégoire when declaring morphisms in modulemsozeau
types. Change (again) the semantics of bindings and the binding modifier ! in typeclasses. Inside [ ], implicit binding where only parameters need to be given is the default, use ! to use explicit binding, which is equivalent to regular bindings except for generalization of free variables. Outside brackets (e.g. on the right of instance declarations), explicit binding is the default, and implicit binding can be used by adding ! in front. This avoids almost every use of ! in the standard library and in other examples I have. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
names, gives the ability to specify qualified classes in instance declarations. Use that in the class_tactics code. Refine the implementation of classes. For singleton classes the implementation of the class becomes a regular definition (into Type or Prop). The single method becomes a 'trivial' projection that allows to launch typeclass resolution. Each instance is just a definition as usual. Examples in theories/Classes/RelationClasses. This permits to define [Class reflexive A (R : relation A) := refl : forall x, R x x.]. The definition of [reflexive] that is generated is the same as the original one. We just need a way to declare arbitrary lemmas as instances of a particular class to retrofit existing reflexivity lemmas as typeclass instances of the [reflexive] class. Also debug rewriting under binders in setoid_rewrite to allow rewriting with lemmas which capture the bound variables when applied (works only with setoid_rewrite, as rewrite first matches the lemma with the entire, closed term). One can rewrite with [H : forall x, R (f x) (g x)] in the goal [exists x, P (f x)]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10697 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Move generally useful definition of nf_evar on contexts to evarutil.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10532 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-15Generalize instance declarations to any context, better name handling. Add ↵msozeau
hole kind info for topconstrs. Derive eta_expansion from functional extensionality axiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but ↵msozeau
implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10432 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-05Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ↵msozeau
evars and try to solve them too. Finally, rework tactics on setoids and design a saturating tactic to help solve goals on any setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10428 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-04Add partial setoids in theories/Classes, add SetoidDec class for setoids ↵msozeau
with a decidable equality. Fix name capture bug, again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10419 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-02Better resolution of implicit parameters in typeclass binders, add ↵msozeau
extensionality tactic to apply the axiom properly and fix test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10415 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Fix name capture bug and call the right pretyper in subtac.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10414 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Merged revisions ↵msozeau
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 05:10:12 +0000