aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.mli
Commit message (Collapse)AuthorAge
* Small cleaning of interface in UnivGravatar ppedrot2012-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16006 85f007b7-540e-0410-9357-904b9bb8a0f7
* univ inconsistency error message gives evidence of a cycleGravatar barras2012-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15898 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
| | | | | | Same for check_leq instead of check_geq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 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
* When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyGravatar letouzey2011-10-26
| | | | | | | | | | | | | Here Foo is Univ.constraints, Univ.universes, Evd.evar_map, Evd.Metamap Ok, all these structures are currently ocaml's maps or similar, with a unique empty value, and (=) can be used on them in this particular case. But using Foo.is_empty is safer : it will work even if the underlying representation changes. Example : for spotting non-legitimate use of (=) we might embed a type into a record with a functional field. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hash-consing of mutual_inductive_body (and Univ.constraints)Gravatar letouzey2011-10-10
| | | | | | | | Inductive definitions aren't that big, but they may contain some constr (in types, rel_context, etc), hence if we hash-cons the constr in Definition but not these ones, we may loose some sharing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14544 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
| | | | | | | | | | | | | | | | | - An inductive is hidden inside case_info. (btw, maybe we could get rid of this ci_ind altogether, since the information is already in the predicate of the match) - Typical situation where user kn and canonical kn are initially (==) was not preserved by hconsing of constant / mutual_inductive - inductive = (mutual_inductive * int) and constructor = inductive * int were not properly shared This should fix the strange situation of Udine/PiCalc taking *more* vo space after the last round of hcons tweaks. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the hconsing of universesGravatar letouzey2011-09-07
| | | | | | | | | | | | | | | | | Two issues were preventing the hcons1_univ function to properly work - a launch of Names.hcons_names () at each hconsing of universe, hence one separated hash-table for dir-path created at each time, oups... - Bad handling of the universe sub-structure universe_level To check : is there an interest in making separate calls to Names.hcons_names () in separate places (Univ, Term, Declare) ? I think not. Btw the hconsing of Declare.hcons_constant_declaration is also probably wrong. To be fixed in a forthcoming patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
| | | | | | | | | | | | | evar, and simultaneously make type inference with universes work better. This only exports more functions from kernel/univ, to be able to work with a set of universe variables during type inference. Universe constraints are gradually added during type checking, adding information necessary e.g. to lower the level of unknown Type variables to Prop or Set. There does not seem to be a disastrous performance hit on the stdlib, but might have one on some contribs (hence the "Tentative"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13786 85f007b7-540e-0410-9357-904b9bb8a0f7
* More coherent comment orderingGravatar glondu2011-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13784 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* In Univ, unify order_request and constraint_typeGravatar glondu2010-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13614 85f007b7-540e-0410-9357-904b9bb8a0f7
* More generic Univ.dump_universesGravatar glondu2010-11-02
| | | | | | | | Instead of formatting directly to an output channel, provide an output function that handles formatting and I/O. This allows changing the output format. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13610 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
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 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
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
| | | | | | | | | | | | | | | | | | | dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 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
* 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
* ajout d'un printer pour les contraintes d'univers + correction d'un bug sur ↵Gravatar soubiran2008-06-06
| | | | | | les notations dans les alias de module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11063 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
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
| | | | | | | | | Variable, et plus de trucs useless qui traînaient par ma faute (y compris dans le noyau, la honte). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
| | | | | | | | | | | Printing Universes est active. Ajout de l'option "using" à la tactique non documentée "auto decomp". Ajout de la base "extcore" pour étendre "auto decomp" avec des principes élémentaires tels que le dépliage de "iff". Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des univers algébriques dans les types inférés dansGravatar herbelin2007-01-19
| | | | | | | | | les interfaces de module (bug similaire à #1302 mais pour les définitions -- au lieu des inductifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9505 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
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code v7 obsoleteGravatar herbelin2005-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6993 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
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-11-05
| | | | | | | | | | - reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des commentairesGravatar herbelin2001-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2031 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage aux univers algébriquesGravatar herbelin2001-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout hashconsing universGravatar herbelin2001-07-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Facilites pour le debogguage des univers.Gravatar coq2001-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration de la structure des universGravatar barras2001-03-28
| | | | | | | | elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte du repertoire dans le section path; utilisation de dirpath ↵Gravatar herbelin2000-11-28
| | | | | | pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pr_uniGravatar herbelin2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@666 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug univers (dummy_univ)Gravatar filliatr2000-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@664 85f007b7-540e-0410-9357-904b9bb8a0f7
* ensembles de contraintes d'universGravatar filliatr1999-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Libobject et Summary (partiel)Gravatar filliatr1999-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@36 85f007b7-540e-0410-9357-904b9bb8a0f7
* un petit effort de presentation dans les interfacesGravatar filliatr1999-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@31 85f007b7-540e-0410-9357-904b9bb8a0f7
* - abstractionGravatar filliatr1999-08-26
| | | | | | | | | - univers fonctionnels - erreurs de typage maintenant sous forme d'exception, déclarées dans Type_errors git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@24 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 01:36:47 +0000