aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.ml
Commit message (Collapse)AuthorAge
* 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
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
* Check a list length before doing a List.chop (fix #3000)Gravatar letouzey2013-03-20
| | | | | | | I'm not completely sure that raising Not_found is the right thing to do here, but it seems reasonable... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16326 85f007b7-540e-0410-9357-904b9bb8a0f7
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
| | | | | | | | - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 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
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 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
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
| | | | | | | | This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf. An other wrong externalize function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 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
* Univ: a univ_depends function to avoid a hack in InductiveopsGravatar letouzey2012-03-01
| | | | | | | | | | | univ_depends checks whether a universe variable appears or is equal to a universe. In comparison with the previous hack in inductiveops based on try...catching UniverseInconsistency, this should be semantically equivalent, simplier, and more robust in case we allow someday an unsafe mode where merge_constraints would be a no-op. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductiveops.nb_*{,_env} cleaningGravatar pboutill2012-01-16
| | | | | | | - Functions without _env use the global env. - More comments about when letin are counted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
| | | | | | | | | No need to tell the world about the fact that constraints are implemented via caml's Set. Other modules just need to know about the empty and union functions (and addition functions "enforce_geq" and "enforce_eq" that were already there). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 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
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
| | | | | | | | | | | | | | | | | | | | | In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm property of "u" in the analysis of "t". Commutative cuts aren't compatible with typing so we need to ensure that term of "x"'s type and term of "u"'s have the same subterm_spec. Consequently,declaration.MRec argument has changed to the inductive name instead of only the number of the inductive in the mutual_inductive family. In subterm_specif and check_rec_call, arguments are stored in a stack. At each lambda, one element is popped to add in renv a smarter subterm_spec for the variable. subterm_spec of constructor's argument was added this way, the job is now done more often. Some eta contracted match branches are now accepted but enforcing eta-expansion of branches might be anyway a recommended invariant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 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
* fixed confusion between number of cstr arguments and number of pattern ↵Gravatar barras2010-03-12
| | | | | | variables (which include let-ins in cstr type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12864 85f007b7-540e-0410-9357-904b9bb8a0f7
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
* This big commit addresses two problems:Gravatar soubiran2009-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 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
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
| | | | | | | | | | | | | | interpreted as using the collection of their constructors as hints. - Add support for both "using" and "with" in "firstorder". Made the syntax of "using" compatible with the one of "auto" by separating lemmas by commas. Did not fully merge the syntax: auto accepts constr while firstorder accepts names (but are constr really useful?). - Added "Reserved Infix" as a specific shortcut of the corresponding "Reserved Notation". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
| | | | | | | | | 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
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
| | | | | | | | | | | | | | | - add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
| | | | | | | | | | | | | | | | predicate called from proof refiner was failing because it was not aware of evars instantiation; I added a nf_evar in 8.2 branch but for the trunk, I propose to remove the elimination predicate well-formation test; we therefore assume that tactics build correct elimination predicates in Case, is it not too much demanding?). - Seized the opportunity to remove dead kernel code about non dependent elimination predicates (all predicates are stored dependent by default since a few years now). - Anecdotic complement to commit 12229 (removal of obsolete comment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
| | | | | | | | | | 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
* 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
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
| | | | | | | | | | | | | | | | | contraintes bornant par le haut le type de l'inductif (ce qui peut arriver quand l'inductif est argument d'une constante) étaient oubliées : on pouvait se retrouver avec des inductifs dont le type des constructeurs, une fois instancié par des paramètres) n'était plus typable (seul leur réduit, après expansion des constantes, était typable). [kernel, test-suite] + Affichage des inductifs (via Print) en prenant la forme utilisateur des constructeurs. + Correction warning dans compilation gallina.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
| | | | | | | | | | majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
* Itération sur les sous-termes dans la vérification de la condition de gardeGravatar herbelin2007-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de control_only_guard, qui utilise maintenantGravatar notin2007-08-09
| | | | | | | | | | | | iter_constr_with_full_binders + documentation de Guarded. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/doc/refman/RefMan-pro.tex M trunk/pretyping/inductiveops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9707 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
* Ajout allowed_sortsGravatar herbelin2006-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9194 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
* - 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
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
| | | | | | | | | | | | 7833, et que la révision 8644 n'avait pas corrigé dans le bon sens; renommage en mind_consnrealdecls pour éviter la confusion de sens avec mind_nrealargs - Correction de la description du type one_inductive_body - Ajout test avec let-in dans params et dans type constructeur (fichier Case12.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 85f007b7-540e-0410-9357-904b9bb8a0f7
* oubli de code de debuggingGravatar herbelin2006-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8006 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fonctions retournant les arits des constructeurs et inductifs (suite)Gravatar herbelin2006-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7958 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fonctions retournant les arits des constructeurs et inductifsGravatar herbelin2006-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7955 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la longueur de l'arité des constructeurs dans one_inductive_body ↵Gravatar herbelin2006-01-10
| | | | | | et dans case_info pour permettre l'indépendance de detyping (entre autres) envers l'environnement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7833 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
* Types inductifs parametriquesGravatar mohring2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving subst_inductive from tacinterp to inductiveops for better for reuse ↵Gravatar herbelin2005-02-18
| | | | | | in recordops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6741 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 07:09:49 +0000