aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
Commit message (Collapse)AuthorAge
* Remplacement de la dépendance de G_vernac en G_constr (sourceGravatar herbelin2006-12-03
| | | | | | | | d'incohérences dans les dépendances en l'absence de g_constr.mli) par une dépendance en Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations:Gravatar herbelin2006-10-09
| | | | | | | | | | | | - prise en compte des variables liées non liées par la notation (bug #1186), - test pour affichage des notations aussi sur les sous-ensembles des lieurs multiples (cf notation "#" dans output/Notations.v), - extension, correction et uniformisation de quelques fonctions sur les constr_expr et cases_pattern (avec incidences sur rawterm.ml, parsing et contrib/interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Annulation de l'essai de changement de sémantique du %scope (révision 9208).Gravatar herbelin2006-10-06
| | | | | | | | | Retour à une sémantique où les %scope s'appliquent à la sous-expression complète (trop de pbs: constantes polymorphes sans arguments scope, variables locales de type fonctionnel, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9218 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de changement de sémantique du %scope : Gravatar herbelin2006-10-05
| | | | | | | | | | | | | | | | 1- ne s'applique plus que sur la notation immédiate au lieu de s'appliquer récursivement pour toutes les notations de l'expression concernée; 2- désactive la pile de scope pour cette notation immédiate. Le point 2 est clairement préférable pour les notations de la forme 3%sc, où on ne veut pas que 3 soit interprété dans un autre scope que sc même si sc n'a pas de notations numériques. Le point 1 est plus discutable et risque aussi de poser des incompatibilité (mais le comportement récursif peut être rétabli en changeant la valeur de quelques booléens marqués "recursive" dans constrextern.ml, constrintern.ml, et notation.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9208 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1172 + correction en passant de la taille des paramètres de ↵Gravatar herbelin2006-07-07
| | | | | | famille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension des motifs disjonctifs au cas de disjonction de motifs multiplesGravatar herbelin2006-07-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added {measure x f} as a valid recursion order.Gravatar msozeau2006-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8969 85f007b7-540e-0410-9357-904b9bb8a0f7
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
| | | | | | | | | | | | | Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive). The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed. The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at TYPES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
| | | | | | | | des inductifs de la clause "in" du filtrage. - Débogage et extension du parseur xml (g_xml.ml4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8755 85f007b7-540e-0410-9357-904b9bb8a0f7
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ce patch dispense d'ecrire le { struct .. } En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind, l'index de l'argument inductif devient un int option au lieu d'un int. Les deux cas possibles: - Some n : les situations autorisées auparavant, a savoir {struct} explicite, ou bien un seul argument au total - None : le cas nouveau, qui redonne un entier lors du passage de rawconstr à constr si l'on trouve effectivement un unique argument ayant un type inductif, et une erreur sinon. Pour l'instant, on cherche l'inductif dans le type de manière syntaxique, mais il est jouable de rajouter un poil de reduction (au moins delta). Dans le détail, voici les coins que ce patch influence: - parsing/g_xml.ml4: continue pour l'instant a attendre un index explicite via un element xml "recIndex" - contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà un cas ctv_ID_OPT_NONE correspondant à l'absence de struct. Par contre, dans le détail, le code pour un CFix utilise l'index de recurrence pour recouper au besoin le type du fixpoint en deux. Est-ce que je me gourre en supposant que si l'on a besoin de couper ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de l'impression d'un constr, et donc que l'index aura été correctement résolu ? - contrib/subtac/subtac_command.ml: - contrib/funind/indfun.ml: dans les deux cas, j'ai fait le service minimum, le struct reste obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas dur à adapter pour ceux qui comprennent ces parties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
| | | | | | | | May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
* exporting the global reference to the inductive " \/ " in coqlib andGravatar bertot2006-01-25
| | | | | | | | eq_rawconstr in topconstr to prepare the introduction of the new version of functionnal induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
| | | | | | | et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression redondance coerce_to_id dans Pcoq et constrintern et ↵Gravatar herbelin2006-01-09
| | | | | | déplacement dans Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout rawconstr_of_aconstrGravatar herbelin2006-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵Gravatar herbelin2005-12-30
| | | | | | de chaîne de caractères tel que "foo" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 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
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
| | | | | | | "T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
* HUGE COMMITGravatar sacerdot2005-01-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1. when applying a functor F(X) := B to a module M, the obtained module is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the body of t in M}. In principle it is now easy to fine tune the behaviour to choose whether b or M.t must be used. This change implies modifications both inside and outside the kernel. 2. for each object in the library it is now necessary to define the behaviour w.r.t. the substitution {X.t := b}. Notice that in many many cases the pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken (in the sense that it used to break several invariants). This commit fixes the behaviours for most of the objects, excluded a) coercions: a future commit should allow any term to be declared as a coercion; moreover the invariant that just a coercion path exists between two classes will be broken by the instantiation. b) global references when used as arguments of a few tactics/commands In all the other cases the behaviour implemented is the one that looks to me as the one expected by the user (if possible): [ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ] a) argument scopes: not expanded b) SYNTAXCONSTANT: expanded c) implicit arguments: not expanded d) coercions: expansion to be done (for now not expanded) e) concrete syntax tree for patterns: expanded f) concrete syntax tree for raw terms: expanded g) evaluable references (used by unfold, delta expansion, etc.): not expanded h) auto's hints: expanded when possible (i.e. when the expansion of the head of the pattern is rigid) i) realizers (for program extraction): nothing is done since the actual code does not look for the realizer of definitions with a body; however this solution is fragile. l) syntax and notation: expanded m) structures and canonical structures: an invariant says that no parameter can happear in them ==> the substitution always yelds the original term n) stuff related to V7 syntax: since this part of the code is doomed to disappear, I have made no effort to fix a reasonable semantics; not expanded is the default one applied o) RefArgTypes: to be understood. For now a warning is issued whether expanded != not expanded, and the not expanded solution is chosen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage d'une bibliothèque de grands entiers naturels vers une ↵Gravatar herbelin2004-12-25
| | | | | | bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
| | | | | | | | | | | the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 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
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 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
* Motifs recursifs de notations: prise en compte de l'associativite et des ↵Gravatar herbelin2004-03-17
| | | | | | notations de pattern de filtrage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5516 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de motifs récursifs dans Notation; quelques simplifications ↵Gravatar herbelin2004-03-17
| | | | | | au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif des fixpoints pour que si on donne une notation au produit, les pts ↵Gravatar barras2004-03-05
| | | | | | fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Keep structure information for Fixpoint declaration and Fix termsGravatar bertot2004-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
| | | | | | | | | - fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Distinction entre 'as _' qui cache le terme filtre (si variable) et rien ↵Gravatar herbelin2003-11-19
| | | | | | dans case_item git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4949 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout CPatNotation; renommage map_aconstr_with_binders_locGravatar herbelin2003-11-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4755 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe plus liberale pour le type des arguments de filtrage du 'match'Gravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout construction If primitive dans constr_expr et rawconstrGravatar herbelin2003-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
* Paramétrisation vis à vis de existential_keyGravatar herbelin2003-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
| | | | | | | | | | | | | | Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout notation c.(f) en v8 pour les projections de RecordGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 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
* Prise en compte des scopes traversés dans les notationsGravatar herbelin2002-12-15
| | | | | | | | Traitement spécial pour le scope type_scope à l'internalisation Ajout "Locate Notation" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Préparation à la prise en compte des changements de scopes internes aux ↵Gravatar herbelin2002-12-03
| | | | | | notations; bugs d'affichage (confusion key/scope dans les délimiteurs); bug de non-indépendance des règles d'affichage et parsing vis à vis du nom des variables de la notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3365 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-déplacement du résultat de Grammar au niveau constr_exprGravatar herbelin2002-12-02
| | | | | | | | | | (globalisation uniquement des noms - sauf cases, fix, ..., pas d'implicites, pas d'interprétation des scopes - pas plus robuste qu'avant...). Diverses améliorations affichage et parsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3350 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réaffichage des Syntactic Definition (printer constr_expr).Gravatar herbelin2002-11-26
| | | | | | | | Affinement de la gestion des niveaux de constr. Cablage en dur du parsing et de l'affichage des délimiteurs de scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵Gravatar herbelin2002-11-24
| | | | | | améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de Cases dans abbreviatable constr (aconstr) [utilisé dans laGravatar herbelin2002-11-18
| | | | | | | contrib Suresnes/MiniC]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3252 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à une représentation des fixpoints plus primitive dans constr_expr ↵Gravatar herbelin2002-11-15
| | | | | | (càd avec indices) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 00:42:52 +0000