aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
Commit message (Collapse)AuthorAge
* Delayed the computation of parameters in sort polymorphism ofGravatar herbelin2013-05-14
| | | | | | | | inductive types. This saves some computation, but also allows incidentally to retype terms with evars without failing if an inductive type as an argument whose type is an evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16526 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
| | | | | | | | | | | | | | | | | 1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
* A more informative message when the elimination predicate forGravatar herbelin2013-02-17
| | | | | | | | | | | | destruct, rewrite, etc. is not well-typed. Also added support for a more informative message when the elimination predicate is not well-formed while using the smart "second-order" unification algorithm. However the "abstract_list_all" algorithm seems to remain more informative though, so we still use this algorithm for reporting about ill-typed predicates. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved code from Pretype_error to EvarutilGravatar ppedrot2013-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16194 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Taking into account the possibility of having a type of type which isGravatar herbelin2012-12-18
| | | | | | | | an evar in typing.ml. Thanks to HoTT people for noticing the problem. Fixed behavior of e_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 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
* 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
* 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
* Still more unification in typing.mlGravatar herbelin2011-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14591 85f007b7-540e-0410-9357-904b9bb8a0f7
* More unification in type_of and addition of e_type_of to get the newGravatar herbelin2011-10-24
| | | | | | evar_map after instantiations possibly happened. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14586 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification in the return clause of match was not supported in solve_evars.Gravatar herbelin2011-10-11
| | | | | | This is now fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14548 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applied the trick of Chung-Kil Hur to solve second-order matchingGravatar herbelin2011-10-10
| | | | | | | problems with dependencies. Generalized it to matching over dependent tuples as explored by Dan Grayson. Currently used only in Evarconv. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14538 85f007b7-540e-0410-9357-904b9bb8a0f7
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
| | | | | | | | | | that the return predicate of the match construction is at an allowed sort, resulting in tactics possibly manipulating ill-typed terms. This is now fixed, Incidentally removed in pretyping an ill-placed coercion. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14508 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replaced printing number of ill-typed branch by printing name of constructorGravatar herbelin2011-04-08
| | | | | | | when a "match" is kernel-ill-typed (probably rarely visible from end user anyway but useful for debugging) + dead code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13969 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
* 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
* Added a function in typing.ml to solve evars of a constr w/o going back down ↵Gravatar herbelin2010-04-05
| | | | | | | | to rawconstr Also cleaned a bit typing.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12902 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
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
| | | | | | | | | traînaient un peu partout dans le code depuis la fusion d'evar_map et evar_defs. Début du travail d'uniformisation des noms donnés aux evar_defs à travers le code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | par Evd). Ça s'accompagne de quelques autres modifications de l'interface (certaines fonctions étaient des doublons, ou des conversions entre evar_map et evar_defs). J'ai modifié un peu la structure de evd.ml aussi, pour éviter des fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai introduit des sous-modules pour les différentes couches. Il y a à l'heure actuelle une pénalité en performance assez sévère (due principalement à la nouvelle mouture de Evd.merge, si mon diagnostique est correct). Mais fera l'objet de plusieurs optimisations dans les commits à venir. Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un appel de Decl_proof_instr.mark_as_done visiblement, je suis pour l'instant incapable de comprendre ce qui cause cette erreur. J'espère qu'on pourra le déterminer rapidement. Ce commit est le tout premier commit dans le trunk en rapport avec les évolution futures de la machine de preuve, en vue en particulier d'obtenir un "vrai refine". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
| | | | | | | | | | | | | | | | | | | | | | - vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application de refresh_universes dans typing.ml et retyping.ml : lesGravatar herbelin2008-03-15
| | | | | | | | | | | | | appels à type_of et get_type_of sont souvent utilisés pour construire des termes à partir de types; on ne rajoute pas non plus de contraintes inutiles parce que type_of et get_type_of ne changent pas le graphe de contraintes; tout ce qu'on perd est une information utilisateur sur le type en lui-même mais puisque pretty.ml n'appelle ni type_of ni get_type_of, ces informations sur la représentation interne des univers restent a priori accessibles pour l'utilisateur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification des types + clause filtrage manquante + uniformisation localeGravatar herbelin2007-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9879 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour le rapport de bug #1325 par rétablissement duGravatar herbelin2007-01-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | comportement pré-inductifs polymorphes vis à vis du test d'inclusion des hypothèses de section (i.e. test dans le noyau mais pas dans typing.ml qui est le typeur utilisé généralement par les tactiques). En effet, les variables de section sont vues par les tactiques comme des variables locales qui sont modifiables (p.ex. par conversion). Mais le changement de la signature des variables de section fait échouer le typage noyau (qui exige une égalité syntaxique des types de ces variables) pour les demandes de typage en provenance des tactiques. Quelle est la bonne solution ? - Faut-il comparer les variables de section modulo réduction dans le noyau ? - Faut-il continuer à utiliser un typeur qui ne teste pas les hyps de section pour les tactiques, comme c'était le cas avant les inductifs polymorphes (c'est la solution pragmatique adoptée pour résoudre #1325) - Faut-il éviter la confusion entre variables de section et variables de but ? Incidemment, branchement de Tacmach.hnf_type_of sur Retyping, ce qui, outre des calculs de typage allégés pour les tactiques, évite aussi de tomber sur le comportement du bug #1325. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9510 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
* - 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
* 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
* 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
* essai de typage des instantiations d\'evarsGravatar barras2005-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 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
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
* hiding the meta_map in evar_defsGravatar barras2004-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 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
* test de conversion laissait echapper exception NotConvertibleGravatar barras2004-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5746 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai suppression nf_betaiota dans type_ofGravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3397 85f007b7-540e-0410-9357-904b9bb8a0f7
* petite erreur dans le typage des let-inGravatar barras2002-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2573 85f007b7-540e-0410-9357-904b9bb8a0f7
* typage du produit: type_judgment appele avec contexte incorrectGravatar barras2002-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2488 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
* Rétablissement de la persistance des Cast; typage des LetIn sans recours à ↵Gravatar herbelin2001-11-08
| | | | | | Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2171 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 13:54:41 +0000