aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/retyping.ml
Commit message (Collapse)AuthorAge
* Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenGravatar herbelin2013-02-05
| | | | | | variable names). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16185 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
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 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
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
| | | | | | Util module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 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
* 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
* Extraction: forbid Prop-polymorphism of inductives when extracting to OcamlGravatar letouzey2011-07-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | A particular case in sort-polymorphism of inductive types allows an informative type (such as prod) to have instances in Prop: (I,I) : True * True : Prop This is due to the fact that prod is a singleton type: indeed (I,I) has no informative content. But this invalidates an important invariant for the correctness of the extraction: inductive constructors stop having always the same sort as their inductive type. Consider for instance: Definition f (X:Type)(x:X*X)(g:X->nat) := g (fst x). Definition test := f _ (I,I) (fun _ => 0). Then the inductive element (I,I) is extracted as a logical part __, but during a strict evaluation (i.e. in Ocaml, not Haskell), this __ will be given to fst, and hence to a match, leading to a nasty result (potentially segfault). Haskell is not affected, since fst is never evaluated. This patch adds a check for this situation during any Ocaml extraction, leading for the moment to a fatal error. Some functions in inductive.ml and retyping.ml now have an extra optional argument ?(polyprop=true) that should stay untouched in regular Coq usage, while type-checking done during extraction will disable this prop-polymorphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14256 85f007b7-540e-0410-9357-904b9bb8a0f7
* Catch NotArity exception and transform it into an anomaly in retyping.Gravatar msozeau2011-04-11
| | | | | | | | | | Add a temporary fix in solve_simple_eqn to catch anomalies coming from retyping because the unification algorithm with metas doesn't respect the precondition that evar instances should be well-typed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13985 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
* 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
* A try at using sort variables during unification. Instead of refreshingGravatar msozeau2009-05-23
| | | | | | | | | | | | | universes as usual, we add the new universes to the sort constraints and do unification modulo those ([constr_unify_with_sorts]): this allows to instanciate Type i with Prop for example and keep track of it. The sort constraints are thrown away at the end of unification for the moment, but we can detect inconsistencies during unification. Make unification more symmetric as well w.r.t. substitution of defined metas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12137 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing bug #2084 (unification not checking sort constraints), hopingGravatar herbelin2009-04-08
| | | | | | | | | | | | | it does not cause a time penalty. - Removing of get_type_of_with_meta made possible by the evar_defs/evar_map merge. - Adding unfolding of Meta in reductionops (this assumes that reduction does not move Metas across binders...) - Renaming newly created fold_map_rel_context into map_rel_context_in_env. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack sur la mémoïsation de nf_evar.Gravatar aspiwack2009-03-04
| | | | | | | | | | | | | | | | L'expérience prouve que ce n'est pas franchement concluant. On peut se risquer à une explication : - nf_evar, version mémoïsée n'est pas tail recursive - On retarde la substitution des hypothèses de l'evar en échange de faire moins de substitutions d'evars. Intuitivement c'est intéressant seulement si il y a plus de substitutions d'evar dupliquées que d'hypothèses dupliquées. Ce qui ne doit pas être le cas (ne serait-ce que parce que dupliquer une evar duplique aussi ses variables libres). This reverts commit 066a564021788e995eb166ad6ed6e55611d6f593. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11958 85f007b7-540e-0410-9357-904b9bb8a0f7
* =?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et ↵Gravatar aspiwack2009-02-27
| | | | | | | | | | | | | | | | | | | | =20[whd=5Fevar]=20:=20les =20evar=5Fdefs=20gardent=20un=20cache=20des=20appels=20pr=C3=A9c=C3=A9dents.=20Le=20d=C3=A9faut=20de=20la =20m=C3=A9thodologie=20est=20que=20=C3=A7a=20int=C3=A9ragit=20assez=20mal=20avec=20la=20substitution=20des =20hypoth=C3=A8ses=20de=20l'evar=20(qui=20n'est=20pas=20mise=20en=20cache).=20En=20particulier=20les =20deux=20fonctions=20ne=20sont=20plus=20r=C3=A9cursives=20terminales.=20De=20plus=20un=20appel=20=C3=A0 =20l'une=20des=20deux=20fera=20n=C3=A9cessairement=20un=20parcours=20du=20terme=20pour=20appliquer =20la=20substitution.?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit D'un point de vue de l'effet observer, ça a un effet assez léger sur le trunk, je suis curieux de voir les effets sur les contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11950 85f007b7-540e-0410-9357-904b9bb8a0f7
* pushed evar reduction in kernelGravatar barras2009-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
| | | | | | | | | | | | - Really unify with types of metas when they contain metas _or_ evars (why not always?) (fixes bug #2027). - Better handling of evars in rewrite lemmas when using setoid_rewrite through rewrite (reported by Ralf Hinze). - Use retyping with metas when possible (check?) and improve an obscure error message in retyping. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11776 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
| | | | | | | | | | | | | | | | | | | | | | | inductive types was not taken into account). - Virtually extended tauto to - support arbitrary-length disjunctions and conjunctions, - support arbitrary complex forms of disjunctions and conjunctions when in the contravariant of an implicative hypothesis, - stick with the purely propositional fragment and not apply reflexivity. This is virtual in the sense that it is not activated since it breaks compatibility with the existing tauto. - Modified the notion of conjunction and unit type used in hipattern in a way that is closer to the intuitive meaning (forbid dependencies between parameters in conjunction; forbid indices in unit types). - Investigated how far "iff" could be turned into a direct inductive definition; modified tauto.ml4 so that it works with the current and the alternative definition. - Fixed a bug in the error message from lookup_eliminator. - Other minor changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
| | | | | | | | | | | | | | | | | automation. - Permitted to use evars in the intermediate steps of "apply in" (as expected in the test file apply.v). - Back on the systematic use of eq_rect (r11697) for implementing rewriting (some proofs, especially lemma DistOoVv in Lyon/RulerCompassGeometry/C14_Angle_Droit.v and tactic compute_vcg in Sophia-Antipolis/Semantics/example2.v are explicitly refering to the name of the lemmas used for rewriting). - Fixed at the same time a bug in get_sort_of (predicativity of Set was not taken into account). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11717 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixing r11433 again:Gravatar barras2008-10-07
| | | | | | | | | | | | | - backtrack on kernel modifications: the monomorphic instance of an inductive type is constrained to live in an universe higher (or equal) than all the instances - improved support for polymorphic inductive types at the refiner level: introduced type_of_inductive_knowing_conclusion that computes the instance to match the current conclusion universe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11435 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation de admit et Print Assumptions.Gravatar herbelin2008-06-09
| | | | | | | | | | | | - Relecture, mise à jour, correction d'erreurs et petite réorganisation du chapitre sur les commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers algébriques). - Suppression de la dépendance du initial.coq en les noms longs des fichiers de façons à ce que les dépendances ne soient que purement logique. - Encore un (petit) bug undo ide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 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
* 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
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
| | | | | | | | | 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
* 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
* 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
* 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
* Set is not always impredicativeGravatar barras2004-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5194 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
| | | | | | | | | Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
| | | | | | | | | | | - Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2963 85f007b7-540e-0410-9357-904b9bb8a0f7
* un cas inutile dans un pattern matchingGravatar letouzey2002-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2885 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
* exceptionmal ratrappeeGravatar barras2002-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2451 85f007b7-540e-0410-9357-904b9bb8a0f7
* Grossière erreur de typageGravatar herbelin2001-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2305 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
* Blindage, de peur que des types entrant non en forme normale ne provoque des ↵Gravatar herbelin2001-09-19
| | | | | | calculs sur les univers dans get_sort_family_of git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle fonction sort_family_of pour calculer la famille dans lequel vit un ↵Gravatar herbelin2001-09-19
| | | | | | type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2008 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
* Changement de la structure des points fixesGravatar barras2001-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 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
* nouvelle implantation de la reductionGravatar barras2001-03-01
| | | | | | | suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 12:52:50 +0000