aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretyping.ml
AgeCommit message (Collapse)Author
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
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
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
evdref si evar_defs ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-29- Débogueur: positionnement de set_detype_anonymous pour ne pasherbelin
échouer sur les Rel liées a des Anonymous et export de l'instance des evars vers le printeur du débogueur. - Suppression d'un reste de code mort lié à la V7 dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-27Suppression des type_app et body_of_type qui alourdissent inutilement le codeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. When the system accepts a fixpoint, it now prints which decreasing argument was used, e.g: plus is recursively defined (decreasing on 1st argument) The search is quite brute-force, and may need to be optimized for huge mutual fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback. N.B. in the standard library, only 4 functions have an decreasing argument different from the one that would be automatically infered: List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind And compiling with as few explicit struct as possible would add about 15s in compilation time for the whole standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an ↵msozeau
obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-12-29Protection contre une source possible de liaison de lambda anonymeherbelin
(utilisation du nom de la contrainte de type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9468 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-03Suppression source de complexité polynomiale introduite par le polymorphismeherbelin
dans les définitions alors même que ce polymorphisme est débranché git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9336 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
Amélioration affichage des univers. Réparation de petits oublis du premier commit. Essai d'une nouvelle stratégie : si le type d'une constante est mentionné explicitement, la constante est monomorphe dans Type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9314 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Remplacement des nf_evar (source de complexité polynomiale) par de laherbelin
réduction paresseuse. Accessoirement, suppression d'un test evar_defined inutile car sur résultat de whd_betadeltaiota qui contient la réduction evar de tête dans coercion.ml; code mort du commit précédent dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9223 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-06Suppression d'une source de complexité polynomiale dans le pretypageherbelin
(remplacement de la normalisation complète des evars dans les termes par une normalisation par nécessité - dans les types, c'est en général des expressions plus petites) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9220 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-15Report de l'heuristique d'unification premier ordre flexible/rigideherbelin
en dernière étape de la procédure d'unification - Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution de l'unification premier ordre flexible/rigide - Déplacement check_evars dans Evarutil Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ? (cf exemples d'application dans test-suite/success/evars.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9141 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Export de check_evars vers command.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9105 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-27Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte ↵herbelin
des inductifs maintenant retourne des sortes d'inductives qui ne sont pas des variables) et test de non-régression git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8992 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29The "clean integration of subtac" patch.msozeau
Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive). The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed. The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at TYPES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28- Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesherbelin
(i.e. cachées sous un nom de constante) sont considérées comme monomorphes. - Divers: renommage type_of_applied_inductive, un peu de documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8871 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Standardisation du nom des méthodes de Evdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-14Si un fixpoint a plusieurs arguments, mais un seul de type inductif, letouzey
ce patch dispense d'ecrire le { struct .. } En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind, l'index de l'argument inductif devient un int option au lieu d'un int. Les deux cas possibles: - Some n : les situations autorisées auparavant, a savoir {struct} explicite, ou bien un seul argument au total - None : le cas nouveau, qui redonne un entier lors du passage de rawconstr à constr si l'on trouve effectivement un unique argument ayant un type inductif, et une erreur sinon. Pour l'instant, on cherche l'inductif dans le type de manière syntaxique, mais il est jouable de rajouter un poil de reduction (au moins delta). Dans le détail, voici les coins que ce patch influence: - parsing/g_xml.ml4: continue pour l'instant a attendre un index explicite via un element xml "recIndex" - contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà un cas ctv_ID_OPT_NONE correspondant à l'absence de struct. Par contre, dans le détail, le code pour un CFix utilise l'index de recurrence pour recouper au besoin le type du fixpoint en deux. Est-ce que je me gourre en supposant que si l'on a besoin de couper ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de l'impression d'un constr, et donc que l'index aura été correctement résolu ? - contrib/subtac/subtac_command.ml: - contrib/funind/indfun.ml: dans les deux cas, j'ai fait le service minimum, le struct reste obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas dur à adapter pour ceux qui comprennent ces parties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8718 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-10Fixes for new unification, not used in default version as it really changes ↵msozeau
unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8695 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-10Actual fix for the unification problem in theories/Reals/Rtrigo_fun ↵msozeau
(previous and current version work). Changed the type of typing constraints so as to have all the necessary information on abstract tycons. Updates of subtac to use the new type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8693 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-07- Documentation of the Program tactics.msozeau
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22Subtac fixes, single fixpoint definitions are working again. Added a toggle ↵msozeau
on the pretyping module to allow or disallow binding of syntaxically inexistant variables (i.e., under an if when applied to an inductive where constructors have arguments). Does not change current behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8655 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default ↵msozeau
uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau
May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-04Correction message d'erreur ltac et adoption du modèle de message de Tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8125 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Localisation des erreurs de sorte du prétypageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8011 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Suppression résidus code v7 et traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7834 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Léger nettoyage et uniformisation + généralisation du point d'entrée ↵herbelin
ltac pour qu'il retourne les evar git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7361 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-07reparations de quelques petits bugs d\'unification + introduction de la ↵barras
notion de variable de sortes (mais pas encore utilise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7120 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-06essai de typage des instantiations d\'evarsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-15Backtrack sur la substitution combinée avec l'instanciation en réponse à ↵herbelin
l'inefficacité montrée dans le bug #932: suppression plutôt des Anonymous dans le contexte des evars (cf Evarutil) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6836 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-10A défaut de substitution paresseuse ou explicite, ajout d'une substitution ↵herbelin
optimisée pour le prétypage qui normalise les evars à la volée (cf bug #932) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6820 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Standardisation of function names about global references (especially, ↵herbelin
renaming of constr_of_reference into constr_of_global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-02Correction de la précédence des contexts de variables rel, ltac et varherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6660 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Relâchement obligation d'une contrainte de type sur les Hole en position ↵herbelin
terminale, pour plus grande généralité de understand_gen_tcc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6421 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15hiding the meta_map in evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-24Deplacement des fonctions de typage des predicate de Cases a la V7 de ↵herbelin
inductiveops vers pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6029 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25correspondance des records et noms de champs de records entre un module et ↵letouzey
sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:51:36 +0000