aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/indtypes.ml
Commit message (Collapse)AuthorAge
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
| | | | | | | | | No need to tell the world about the fact that constraints are implemented via caml's Set. Other modules just need to know about the empty and union functions (and addition functions "enforce_geq" and "enforce_eq" that were already there). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove suspiciously named "implicit" stuff from TermGravatar glondu2010-11-03
| | | | | | | The lambda_implicit series of functions are used only in Indtypes, so we move them there. In the checker, they are already there... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed (serious) bug #2353: non-recursive parameters of nested inductive ↵Gravatar barras2010-07-16
| | | | | | types were seen as real constructor arguments... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
| | | | | | | | | | | | | | | | | | | | | In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm property of "u" in the analysis of "t". Commutative cuts aren't compatible with typing so we need to ensure that term of "x"'s type and term of "u"'s have the same subterm_spec. Consequently,declaration.MRec argument has changed to the inductive name instead of only the number of the inductive in the mutual_inductive family. In subterm_specif and check_rec_call, arguments are stored in a stack. At each lambda, one element is popped to add in renv a smarter subterm_spec for the variable. subterm_spec of constructor's argument was added this way, the job is now done more often. Some eta contracted match branches are now accepted but enforcing eta-expansion of branches might be anyway a recommended invariant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug #2224 (Error message in positivity check fixed)Gravatar vsiles2010-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12974 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2156 (non positive occurrence error message displayed "Rel"'s).Gravatar herbelin2009-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12616 85f007b7-540e-0410-9357-904b9bb8a0f7
* This big commit addresses two problems:Gravatar soubiran2009-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
| | | | | | | | | very useful in practice but as soon as let-in's were not forbidden in the internal data structure, better to do it. Moreover, this gets closer to the view were inductive definitions are uniformly built from "contexts". (checker not changed!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
| | | | | | | | | | | | - Added dependency of mltop.ml4 into config/Makefile (see bug #2023). - Fixed bug #1963 (dependent inversion building a universe-ill-formed conversion problem). - Incidentally, moved "Large non-propositional inductive ..." error message to standard himsg.ml error displayer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11774 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
| | | | | | | | | | splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed minor environment issues when checking inductive typesGravatar barras2008-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11349 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
| | | | | | | | | | | | | | | | | contraintes bornant par le haut le type de l'inductif (ce qui peut arriver quand l'inductif est argument d'une constante) étaient oubliées : on pouvait se retrouver avec des inductifs dont le type des constructeurs, une fois instancié par des paramètres) n'était plus typable (seul leur réduit, après expansion des constantes, était typable). [kernel, test-suite] + Affichage des inductifs (via Print) en prenant la forme utilisateur des constructeurs. + Correction warning dans compilation gallina.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
| | | | | | | | | | | opportunity to extend the class of singleton types to (possibly mutual) recursive types with single constructors of which all arguments are in Prop. This covers Acc. Acc_rect can consequently be defined in the direct way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
| | | | | | | | | | majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de stratégie vis à vis du commit 10859 sur la gestion desGravatar herbelin2008-05-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | univers, suite à discussion avec Bruno : on franchit le cap et on ajoute le sous-typage Prop <= Set. On n'a donc plus besoin d'utiliser l'image de Prop dans la hiérarchie en dehors de la zone de calcul de la sorte la plus basse d'un inductif polymorphe (au passage, nous avons décidé de renommer Type -1 en Type 0-, pour bien indiquer qu'il se trouve au même niveau que Type 0). Coq se retrouve donc avec la hiérarchie Prop <= Set <= Type i et avec une copie de Prop (Type 0-) et une copie de Set (Type 0) dans la hiérarchie Type. En théorie, on pourrait donc supprimer "Prop Null" et "Prop Pos" de l'implémentation et ne travailler qu'avec "Type". L'ajout de Prop <= Set vaut à la fois dans le cas Set prédicatif et dans le cas Set imprédicatif (Prop et Set étant en bas de la hiérarchie, il n'y a pas d'incohérence connue). Dans le modéle ensembliste, Prop et Type 0- sont interprétés par exemple comme {{},{o}}, où "o" est un objet particulier interprétant les preuves, et il n'y a pas de Set imprédicatif. Dans un modèle de réalisabilité, Set imprédicatif est interprétable et Prop peut au choix s'interpréter comme Set ou comme booléen (cf la thèse de Miquel). Le sous-typage du côté ensembliste s'obtient en mettant au moins l'ensemble {{},{o}} dans l'interprétation de Set (ce qu'on fait de la même manière que Prop <= Type 1, avec conversion typée), et du côté réalisabilité en mettant l'ensemble {Typ(vide),Typ(unit)} dans l'interprétation de Set ("Typ" étant la coercion faisant d'un ensemble un terme), ce qui est fait dans la section 6.2.4 de la thèse d'Alexandre Miquel (modèle du CC implicite sans types inductifs). Il reste un problème pratique. Lorsqu'on donne Inductive unit:Type := tt:unit. Coq dit que unit est dans Prop. C'est correct parce qu'il n'y a pas de contraintes d'univers mais un peu déroutant même si la coercion "unit : Set" reste valide. Une suggestion est de ne rendre polymorphe que les inductifs dont on ne donne pas la sorte explicitement, comme dans Inductive unit := tt:unit. mais alors, comment indiquer l'absence de sorte explicite si le type a des paramètres réels (comme "vect") ?? PS: modification de sort_cmp dans checker/inductive.ml faite. --This line, and those below, will be ignored-- M kernel/univ.ml M kernel/univ.mli M kernel/inductive.ml M kernel/reduction.ml M kernel/indtypes.ml M checker/inductive.ml M checker/reduction.ml M pretyping/reductionops.ml M pretyping/termops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
| | | | | | | | | | | | | | | | | | | | | | (i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le principe de la hiérarchie d'univers est d'être cumulative -- et que Set en soit le niveau 0). Une solution aurait été de poser Prop <= Set mais on adopte une autre solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type et Prop <= Set, on garde la représentation de Prop au sein de la hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau sans aucune contrainte inférieure, appelons Type -1) et on adapte les fonctions de sous-typage et de typage pour qu'elle prenne en compte la règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets incidents dans Termops.refresh_universes et Univ.super). Petite uniformisation des noms d'univers et de sortes au passage (univ.ml, univ.mli, term.ml, term.mli et les autres fichiers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 ↵Gravatar barras2008-03-18
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug 1761 (unexpected anomaly when constructor type has invalidGravatar herbelin2008-01-05
| | | | | | | | conclusion) and improved error message when the conclusion of the type of a constructor is invalid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10425 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug in infos_and_sort: type of constructor was not reduced enoughGravatar barras2007-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10296 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppresion de la catégorie des inductifs singletons larges dontGravatar herbelin2007-02-09
| | | | | | | | l'élimination vers Set était autorisée: comme souligné par Benjamin, c'est incompatible avec EM + AC (report rev 9633 8.1) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9634 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1273 (problème avec les paramètres non récursivement ↵Gravatar notin2006-12-12
| | | | | | uniformes dans le cas de types mutuellement inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9445 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
| | | | | | | | | | (suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de 2 bugs critiques du polymorphisme d'universGravatar herbelin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9301 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
| | | | | | | | | (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
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
| | | | | | | | | | | - prise en compte du niveau à la déclaration du type comme une fonction des sortes des conclusions des paramètres uniformes - suppression du retypage de chaque instance de type inductif (trop coûteux) et donc abandon de l'idée de calculer une sorte minimale même dans des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction trou de typage des éliminations d'inductifs introduit dans ↵Gravatar herbelin2006-05-13
| | | | | | commit 7360 suite à mécompréhension du sens de isunit; ajout d'un test vérifiant l'absence de ce trou git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8811 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
| | | | | | | | | | | | 7833, et que la révision 8644 n'avait pas corrigé dans le bon sens; renommage en mind_consnrealdecls pour éviter la confusion de sens avec mind_nrealargs - Correction de la description du type one_inductive_body - Ajout test avec let-in dans params et dans type constructeur (fichier Case12.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug calcul consnrealargs + bug calcul occurrences non positives + modifs ↵Gravatar herbelin2006-03-18
| | | | | | cosmétiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8644 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2006-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7899 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la longueur de l'arité des constructeurs dans one_inductive_body ↵Gravatar herbelin2006-01-10
| | | | | | et dans case_info pour permettre l'indépendance de detyping (entre autres) envers l'environnement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7833 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ↵Gravatar herbelin2005-12-17
| | | | | | et suite correction bug #1028 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7660 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | 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
* parametres inductifsGravatar mohring2005-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7620 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Types inductifs parametriquesGravatar mohring2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression code inactif et commentaire apparemment incorrect (pour éviter ↵Gravatar herbelin2005-09-09
| | | | | | confusions suite à question de CSC) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7360 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #983Gravatar herbelin2005-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
| | | | | | | | | to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body) instead of looking it up in the environment. A version of the same functions with the old type is put in Inductiveops (outside the kernel). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* correspondance des records et noms de champs de records entre un module et ↵Gravatar letouzey2004-06-25
| | | | | | sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductive Types : seuls les petits types sont unitairesGravatar mohring2003-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5117 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif lexer: ident peut commencer par _Gravatar barras2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression StronglyClassical, StronglyConstructive devient plus ↵Gravatar herbelin2003-11-08
| | | | | | concretement ImpredicativeSet git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Message inductive largeGravatar herbelin2003-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4730 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 11:09:31 +0000