aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/termops.ml
Commit message (Collapse)AuthorAge
* introduced Termops.eq_constr (and constr_cmp) that compares terms up to ↵Gravatar barras2008-05-28
| | | | | | alpha AND universe erasure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11010 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
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
| | | | | | | | | | | noms illégaux si le type auquel elle s'appliquait n'était pas pur ascii). [util.ml, termops.ml] - Simplification de la procédure d'initialisation (apparemment des résidus obsolètes de la V5.10) et messages d'erreurs [lib.ml, toplevel.ml, coqtop.ml] - Quelques pattern-matching incomplets [topconstr.ml, detyping.ml] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
| | | | | | | | | | constantes qui avait été mise en place pour la 8.1gamma puis abandonné pour cause entre autres d'inefficacité. Cette fois, on restreind le polymorphisme au seul cas d'alias vers un inductif. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
| | | | | | | | | | - pour le "try", la nouvelle erreur CannotFindWellTypedAbstraction doit être catchable - pour accomoder Type -1 dans le discharge, il faut un refresh_universes strict - bugs dans les fichiers de test-suite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10861 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
* * Factorizing code : context_chop was used in several files (even as ↵Gravatar vsiles2008-03-17
| | | | | | | | | | | chop_context) so I moved it to termops.ml * Fixing a little bug in the Boolean to Leibniz transition in automatic boolean declaration git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
| | | | | | | | Ajout de l'option with à (e)destruct et (e)induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 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
* - Ajout de la possibilité d'utiliser la notation Record pour lesGravatar herbelin2007-06-30
| | | | | | | | | | coinductifs à un constructeur (suggestion de Georges). - Si pas de sorte ou arité mentionnée dans Inductive/CoInductive/Record, Type est utilisé comme défaut. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | apply afin de reculer au plus tard les décisions irréversibles et en particulier de pouvoir typer les with-bindings modulo coercions : - l'unification des types des métas données en with-bindings est retardé à après l'unification (unify_0) de telle sorte que les instances trouvées par unify_0 soient prioritaires et que la décision d'insérer éventuellement des coercions autour des valeurs données en with-bindings se fasse au dernier moment; - toujours pour permettre d'insérer ultimement des coercions, l'instantiation des with-bindings ne se fait plus l'appel unify_0 (cf clenv_unique_resolver); - pour permettre ce retardement sans limiter le test de conversion que unify_0 fait sur les termes clos, on transmet à unify_0 les métas données en with-bindings (ainsi l'instantiation de ces métas peut être faite dynamiquement au moment du test de clôture); - parce que les métas données en with-bindings qui sont en position de rédex (cas d'un "apply f_equal with (f:=fun ...)" peuvent simplifier le problème d'unification (et elles ne sont pas de toutes façons pas réinférables au premier ordre), on continue à les substituer avant l'appel à unify_0 (cf meta_reducible_instance); - pour l'unification du second-ordre, on continue d'instancier les with-bindings et d'unifier les types des with-bindings avant unification; - reste à régler un problème de compatibilité lorsque le résultat de l'unification des types des with-bindings est utilisé pour rendre un terme clos et pour permettre à unify_0 d'utiliser la conversion. + meilleure compatibilité de apply, split, left, right pour le code qui l'utilise avec des bindings clos + nettoyage et uniformisation des clenv_match_args, clenv_missing, et assimilés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Confusion sur le paramètre à donner à concrete_name lors du commit 9450Gravatar herbelin2006-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Alignement de la politique de renommage de rename_bound_var (utilisé pourGravatar herbelin2006-12-13
| | | | | | | | résoudre la clause with de apply/elim) sur la politique de renommage de concrete_name git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9450 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
| | | | | | | | | | cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml) + test régression bug #1041 + allègement syntaxe tactique evar + essai de ne pas faire dépendre les evars des variables anonymes afin de résoudre le bug #932 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Évitement des noms de constructeurs dans les motifs de filtrage de "match"Gravatar herbelin2006-12-09
| | | | | | | (un peu de doc de termops.mli au passage) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9424 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
* Déplacement de on_judgment_type de Typeops vers TermopsGravatar herbelin2006-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9221 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
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
| | | | | | | prédicat de filtrage après le terme filtré conformément à l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8003 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en conformité de l'ordre des occurrences de pattern avec l'affichageGravatar herbelin2006-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8001 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
* 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
* Sur le conseil de X.Leroy: x=[||] devient Array.length x=0Gravatar letouzey2005-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added subtac contrib.Gravatar coq2005-05-25
| | | | | | | Added some debug printer in termops. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout it_mkNamedProd_wo_LetInGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6740 85f007b7-540e-0410-9357-904b9bb8a0f7
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 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
* Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)Gravatar herbelin2004-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6030 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
* preparation pour release (suite)Gravatar barras2004-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement array_map_left and co dans UtilGravatar herbelin2004-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5343 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des defs syntaxiques dans is_global et global_reference qui ↵Gravatar herbelin2003-11-24
| | | | | | passent donc de Termops a Constrintern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de iter_constr_with_full_binders dans TermopsGravatar herbelin2003-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement next_global_ident_away dans TermopsGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le nom '_' n'est plus valable en v8 pour nommer les variablesGravatar herbelin2003-10-02
| | | | | | | dépendantes qui par hasard aurait été déclarées Anonymous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4512 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de l'afficheur pour que les variables liées aient un nom ↵Gravatar herbelin2003-09-23
| | | | | | indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de Declare vers TermopsGravatar herbelin2003-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4396 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵Gravatar herbelin2003-09-12
| | | | | | interp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4365 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
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte application partielle dans dependentGravatar herbelin2002-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3478 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit netoyage dans libGravatar coq2002-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allègement du noyauGravatar herbelin2002-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3254 85f007b7-540e-0410-9357-904b9bb8a0f7
* nom de fonction plus simpleGravatar barras2002-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3149 85f007b7-540e-0410-9357-904b9bb8a0f7
* retour en arriere concernant la recherche d'occurence modulo expansion des ↵Gravatar barras2002-10-09
| | | | | | letins, ce qui conduisait a des comportement peu intuitifs. On priviligiera l'utilisation de la tactique Subst. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction de bugs:Gravatar barras2002-08-16
| | | | | | | | | | | - subst_term_gen ne depliait pas les constantes locales de maniere uniforme - la tactique Simpl ne simplifiait pas les constantes definies dans le contexte de but - la conversion d'un constr vers identificateur ne prenait pas en compte les inductifs et constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2971 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 10:46:32 +0000