aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.mli
AgeCommit message (Collapse)Author
2013-12-17Tentative fix of the guardedness checker by Christine and me. All stdlib and ↵Matthieu Sozeau
test-suite pass.
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
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
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-10Propagated information from the reduction tactics to the kernel soherbelin
that the kernel conversion solves the delta/delta critical pair the same way the tactics did. This allows to improve Qed time when slow down is due to conversion having (arbitrarily) made the wrong choice. Propagation is done thanks to a new kind of cast called REVERTcast. Notes: - Vm conversion not modified - size of vo generally grows because of additional casts - this remains a heuristic... for the record, when a reduction tactic is applied on the goal t leading to new goal t', this is translated in the kernel in a conversion t' <= t where, hence, reducing in t' must be preferred; what the propagation of reduction cast to the kernel does not do is whether it is preferable to first unfold c or to first compare u' and u in "c u' = c u"; in particular, intermediate casts are sometimes useful to solve this kind of issues (this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the combination "simpl;red" needs the intermediate cast to ensure Qed answers quickly); henceforth the merge of nested casts in mkCast is deactivated - for tactic "change", REVERTcast should be used when conversion is in the hypotheses, but convert_hyp does not (yet) support this (would require e.g. that convert_hyp overwrite some given hyp id with a body-cleared let-binding new_id := Cast(old_id,REVERTCast,t)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-13- Remove create_evar_defsmsozeau
- Be careful with consider_remaining_unif_problems: it might instantiate an evar, including the current goal! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
Note: I'm unsure about some subtyping error case apparently involving aliases of inductive types (middle of Subtyping.check_inductive); I bound it to some NotEqualInductiveAliases error, but this has to be checked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
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
2010-06-03"Improved" the form of the inferred type of "match" byherbelin
betaiota-reducing it automatically (this allows for instance to directly obtain the expected type for "match" expressions that have a "in I x return match x with ... end" automatically inferred return predicate feature (see e.g. Vhead and Vtail in Bvector.v). The need for this "optimization" was not noticed in V8.2 because in Bvector.v, betaiota was applied peremptorily at the end of sections. The need for it has been revealed by the removal of reduction at section closing when Arnaud introduced the new proof engine (should in particular make CoLoR compile). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13068 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- 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
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
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
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-11Ensures that let-in's in arities of inductive types work well. Maybe notherbelin
very useful in practice but as soon as let-in's were not forbidden in the internal data structure, better to do it. Moreover, this gets closer to the view were inductive definitions are uniformly built from "contexts". (checker not changed!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-06pushed evar reduction in kernelbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
de l'argument donné contient des métavariables (souhait #1408). Beaucoup d'infrastructure autour des constantes pour cela mais qu'on devrait pouvoir récupérer pour analyser plus finement le comportement des constantes en général : 1- Pour insérer les coercions, on utilise une transformation (expérimentale) de Metas vers Evars le temps d'appeler coercion.ml. 2- Pour la compatibilité, on s'interdit d'insérer une coercion entre classes flexibles parce que sinon l'insertion de coercion peut prendre précédence sur la résolution des evars ce qui peut changer les comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN). 3- Pour se souvenir rapidement de la nature flexible ou rigide du symbole de tête d'une constante vis à vis de l'évaluation, on met en place une table associant à chaque constante sa constante de tête (heads.ml) 4- Comme la table des constantes de tête a besoin de connaître l'opacité des variables de section, la partie tables de declare.ml va dans un nouveau decls.ml. Au passage, simplification de coercion.ml, correction de petits bugs (l'interface de Gset.fold n'était pas assez générale; specialize cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml]; whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml]) et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml, classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-20Add the ability to give a transparent_state for conversion, tomsozeau
parameterize what should be unfolded or not, by default unfolding everything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10819 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
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
2004-11-22compatibility with POWERPCgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20types vs constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2210 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- 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
2001-07-03Depliage des let-in dans le test de gardeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1822 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
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
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
les definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en ↵herbelin
compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Déplacement du type stack de Reduction vers Closure et utilisation pour ↵herbelin
accélérer la réduction dans Closure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1221 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22deplacement poly_args; iterateurs sur les segmentsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-02suppression des (* open Generic *)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@726 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Touche finale à la réduction du let in dans conv et closureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@647 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01whd_castapp_stack va de Term dans Reductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@632 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-26Retrait de whd_ise1_metasherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@616 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-15On laisse les LetIn dans les types des constructeurs et des éliminationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@612 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14Nouvelle version de frterm; ajout des contextes dans l'enviornnement de ↵herbelin
réduction de Closure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@602 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-12Vers la paramétrisation des fonctions de Reduction et vers la fusion deherbelin
Closure.stack avec une nouvelle abstraction des 'stacks' de Reduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@596 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Correction pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02Retrait de decomp_prod non conforme à sa specherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@496 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-22suppression de l'env/sigma dans les fonctions de reduction beta et iota seulsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@464 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:41:39 +0000