aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Collapse)AuthorAge
* Deactivating printing of {| |} for records when option Printing All is set.Gravatar herbelin2009-12-13
| | | | | | | Simplifying the printing of "in" clause keeping the same defaults as in parsing (e.g. "simpl" is printed "simpl" and not "simpl in *"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12582 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed incorrect computation of possible guard in presence of `{ ... } contexts.Gravatar herbelin2009-12-12
| | | | | | | Also removed used of local_binders_length and local_assums_length which are now incorrect due to the possible presence of `{ ... } contexts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12579 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more specific syntax "Include Self" for inclusion of partially-applied ↵Gravatar letouzey2009-12-07
| | | | | | | | | | | | | | | | | | | functors For Module F(X:SIG), making now a Include F will try to find the X fields in the current context, just as was doing earlier Include Self F. This specific syntax is removed, freeing the keyword "Self". Anyway, with the use of the syntax "<+" there was already hardly any need for syntax "Include Self". Idem for Include Type. Beware that a typo such as "Include F" instead of "Include F G" will produce a different message now, about a missing field instead of a not-enough-applied functor. By the way, some code clean-up and factorisation of inner recursive functions in declaremods.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
| | | | | | | | | | | | Fixed some bugs in -beautify and robustness of {struct} clause. Note: I tried to make the Automatic Introduction mode on by default for version >= 8.3 but it is to complicated to adapt even in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
| | | | | | | | | | Any place where <: was legal can now contain many <: declarations. Moreover we can say that the module type we are declaring is a subtype of an earlier module type. See DecidableType2 for examples. Also try to handle correctly the freeze/unfreeze summaries when simulating start/include/end (syntax ... := ... <+ ...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12532 85f007b7-540e-0410-9357-904b9bb8a0f7
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
| | | | | | | | | | | | | | | | | | | | "Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for "Module M (...). Include M1. Include M2. Include M3... End M." Moreover M2,M3,etc can be functors as long as they find what they need in what comes before them (see new command "Include Self"). The only real constraint is that M1,M2,M3,... should not have common elements (for the moment (?)). Same behavior for signature : Module Type M := M1 <+ M2 <+ M3. Note that this <+ is _not_ a primitive construct of the module language, for instance it cannot be used in signature (Module M <: M1 <+ M2 is illegal for the moment). Some example of use in Decidable2 and NZAxioms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7
* Experiment propagation of implicit arguments and arguments scope forGravatar herbelin2009-11-12
| | | | | | abbreviations of applied references. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12506 85f007b7-540e-0410-9357-904b9bb8a0f7
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
| | | | | | | | | | | | | | | | | | | | | | | | | | - Deactivation of short names registration and printing for abbreviations to identical names, what avoids printing uselessly qualified names binding where the short name is in fact equivalent. - New treatment of abbreviations to names: don't insert any maximally inserted implicit arguments at all at the time of the abbreviation and use the regular internalization strategy to have them inserted at use time. - The previous modifications altogether make redirections of qualified names easier and avoid the semantic change of r12349 and hence allows to keep "Notation b := @a" as it was before, i.e. as a notation for the deactivation of the implicit arguments of a. - Took benefit of these changes and updated nil/cons/list/app redefinition in "List.v". - Fixed parsing/printing notation bugs (loop on partially applied abreviations for constructors in constrintern.ml + bad reverting of notations with holes that captured non anonymous variables in match_cases_pattern). - Add support for parsing/printing abbreviations to @-like constructors and for reverting printing for abbreviations to constructors applied to parameters only (function extern_symbol_pattern). - Minor error messages fixes and minor APIs cleaning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deactivation of (intrusive) printing of abbreviations from non-imported modules.Gravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12487 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
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Cleaning and uniformisation in command.ml: - For better modularity and better visibility, two files got isolated out of command.ml: - lemmas.ml is about starting and saving a proof - indschemes.ml is about declaring inductive schemes - Decomposition of the functions of command.ml into a functional part and the imperative part - Inductive schemes: - New architecture in ind_tables.ml for registering scheme builders, and for sharing and generating on demand inductive schemes - Adding new automatically generated equality schemes (file eqschemes.ml) - "_congr" for equality types (completing here commit 12273) - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep", "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for rewriting schemes (warning, rew_forward_dep cannot be stated following the standard Coq pattern for inductive types: "t=u" cannot be the last argument of the scheme) - "_case", "_case_nodep", "_case_dep" for case analysis schemes - Preliminary step towards discriminate and injection working on any equality-like type (e.g. eq_true) - Restating JMeq_congr under the canonical form of congruence schemes - Renamed "Set Equality Scheme" into "Set Equality Schemes" - Added "Set Rewriting Schemes", "Set Case Analysis Schemes" - Activation of the automatic generation of boolean equality lemmas - Partial debug and error messages improvements for the generation of boolean equality and decidable equality - Added schemes for making dependent rewrite working (unfortunately with not a fully satisfactory design - see file eqschemes.ml) - Some names of ML function made more regular (see dev/doc/changes.txt) - Incidentally, added a flush to obsolete Local/Global syntax warning git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use generalizable variables info when internalizing arbitrary bindings,Gravatar msozeau2009-11-08
| | | | | | | not just type class applications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12479 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc fixes.Gravatar msozeau2009-11-06
| | | | | | | | | | | | | | - Correct backtracking function of coqdoc to handle the _p fields of lexers - Try a better typesetting of [[ ]] inline code considering it as blocks and not purely inline code like [ ] escapings. - Rework latex macros for better factorization and support external references in pdf output. - Better criterion for generalization of variables in dependent elimination tactic and better error message in [specialize_hypothesis]. - In autounfold, don't put the core unfolds by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
| | | | | | | Fixed pretty printing of record syntax. Allowed record syntax inside patterns. (Patch by Cedric Auger.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
| | | | | | | | | | | | | | | | | This allows easier handling of dependencies, for instance RelationClasses won't have to requires List (which itself requires part of Arith, etc). One of the underlying ideas is to provide setoid rewriting in Init someday. Thanks to some notations in List, this change should be fairly transparent to the user. For instance, one could see that List.length is a notation for (Datatypes.)length only when doing a Print List.length. For these notations not to be too intrusive, they are hidden behind an explicit Export of Datatypes at the end of List. This isn't very pretty, but quite handy. Notation.ml is patched to stop complaining in the case of reloading the same Delimit Scope twice. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revision 12439 continued, printing part (notations to names behaveGravatar herbelin2009-10-29
| | | | | | | | like the name they refer to). Fixing buggy test-suite implicit.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made that notations to names behave like the names they refer to wrtGravatar herbelin2009-10-28
| | | | | | | | | implicit arguments and scope (use Implicit Arguments or Arguments Scope commands instead if not the desired behaviour). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug when reporting unexisting reference to an inductiveGravatar herbelin2009-10-28
| | | | | | | | (introduced in r12323). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
| | | | | | | | | | | | | variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Local/Global revision 12418 continuedGravatar herbelin2009-10-26
| | | | | | | | - Fixing non-export of newly created Local Argument Scope. - Fixing bad discharge of local variables in nested sections (bug still exists in v8.2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12420 85f007b7-540e-0410-9357-904b9bb8a0f7
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
| | | | | | | | | - Clarification and documentation of the different styles of Local/Global modifiers in vernacexpr.ml - Addition of Global in sections for Open/Close Scope. - Addition of Local for Ltac when not in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
| | | | | | | | | | | | Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 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
* Fixed a notation bug when extending binder_constr with empty levelsGravatar herbelin2009-10-17
| | | | | | | | | (see Notations.v). Improved the "already occurs in a different scope" test and message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12383 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed error message "cannot infer the type of id" in presence ofGravatar herbelin2009-09-27
| | | | | | | | | notations for binders (the name of the notation was mistakenly taken). This happened e.g. when using Utf8.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12357 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12338 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
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
| | | | | | | | | | | | | | | string in most commands expecting a global name (e.g. 'Print "+"' for an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation, possibly surrounded by a scope delimiter). Support for such smart globals in VERNAC EXTEND to do. Added a file smartlocate.ml for high-level globalization functions. Mini-nettoyage metasyntax.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
| | | | | | | | | | only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
| | | | | | | | | | | | | | | (uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added "etransitivity".Gravatar herbelin2009-08-03
| | | | | | | | | | | | Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
| | | | | | | | | traînaient un peu partout dans le code depuis la fusion d'evar_map et evar_defs. Début du travail d'uniformisation des noms donnés aux evar_defs à travers le code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for r12197, the refined evars were not returned in case fail_evarGravatar msozeau2009-06-22
| | | | | | | was true. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12206 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use more consistent resolution parameters in Program and regular typingGravatar msozeau2009-06-18
| | | | | | | | and add an optional fail_evar flag to control resolution better in interpretation functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12197 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
| | | | | | | | | | | | | | - "*" implements Arthur Charguéraud's "introv" - "**" works as "; intros" (see also "*" in ssreflect). - Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui. - Shy attempt to seize the opportunity to clean Zarith_dec but Coq's library is really going anarchically (see a summary of the various formulations of total order, dichotomy of order and decidability of equality and in stdlib-project.tex in branch V8revised-theories). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
| | | | | | | | | | | | | as hints (see wish #2104). - New type hint_entry for interpreted hint. - Better centralization of functions dealing with evaluable_global_reference. - Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had uglily to be factorized by hand. - Typography in RefMan-tac.tex. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a small notation/scope bug:Gravatar vsiles2009-04-30
| | | | | | | | | When defining an inductive type with a reserved notation in a particuliar scope, the scope was not opened during the interpretation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12117 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
| | | | | | | | | | | | | reorganization of code) and documentation (in pcoq.mli) of the code for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic Notation, Notation); merged the two copies of interp_entry_name to avoid they diverge. - Added support in Tactic Notation for ne_..._list_sep in general and for (ne_)ident_list(_sep) in particular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
| | | | | | | | | | | | | | This commit concerns about the first half of the useless code mentionned by Oug for coqtop (without plugins). For the moment, Oug is used in a mode where any elements mentionned in a .mli is considered to be precious. This already allows to detect and remove about 600 lines, and more is still to come. Among the interesting points, the type Entries.specification_entry and its constructors SPExxx were never used. Large parts of cases.ml (and hence subtac_cases.ml) were also useless. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
| | | | | | | | | | | | | | | - The measure can now refer to all the formal arguments - The recursive calls can make all the arguments vary as well - Generalized to any relation and measure (new syntax {measure m on R}) This relies on an automatic curryfication transformation, the real fixpoint combinator is working on a sigma type of the arguments. Reduces to the previous impl in case only one argument is involved. The patch also introduces a new flag on implicit arguments that says if the argument has to be infered (default) or can be turned into a subgoal/obligation. Comes with a test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
| | | | | | | | | | | | | | | | | | | | | | | | * generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | par Evd). Ça s'accompagne de quelques autres modifications de l'interface (certaines fonctions étaient des doublons, ou des conversions entre evar_map et evar_defs). J'ai modifié un peu la structure de evd.ml aussi, pour éviter des fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai introduit des sous-modules pour les différentes couches. Il y a à l'heure actuelle une pénalité en performance assez sévère (due principalement à la nouvelle mouture de Evd.merge, si mon diagnostique est correct). Mais fera l'objet de plusieurs optimisations dans les commits à venir. Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un appel de Decl_proof_instr.mark_as_done visiblement, je suis pour l'instant incapable de comprendre ce qui cause cette erreur. J'espère qu'on pourra le déterminer rapidement. Ce commit est le tout premier commit dans le trunk en rapport avec les évolution futures de la machine de preuve, en vue en particulier d'obtenir un "vrai refine". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 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
* Fixing #2044 (bad printing of primitive notation at the head ofGravatar herbelin2009-02-06
| | | | | | | | | coercion to funclass) [added a new notation output test as the initial one is quite saturated in miscellaneous notations]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a bug in 11804 (support for _ in ident entry of notations). Gravatar herbelin2009-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11816 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
| | | | | | | | - Adding ability to use "_" in syntax for binders (as in "exists _:nat, True"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11804 85f007b7-540e-0410-9357-904b9bb8a0f7
* DISCLAIMERGravatar puech2009-01-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ========== This big patch is commited here with a HUGE experimental tag on it. It is probably not a finished job. The aim of committing it now, as agreed with Hugo, is to get some feedback from potential users to identify more clearly the directions the implementation could take. So please feel free to mail me any remarks, bug reports or advices at <puech@cs.unibo.it>. Here are the changes induced by it : For the user ============ * Search tools have been reimplemented to be faster and more general. Affected are [SearchPattern], [SearchRewrite] and [Search] (not [SearchAbout] yet). Changes are: - All of them accept general constructions, and previous syntactical limitations are abolished. In particular, one can for example [SearchPattern (nat -> Prop)], which will find [isSucc], but also [le], [gt] etc. - Patterns are typed. This means that you cannot search mistyped expressions anymore. I'm not sure if it's a good or a bad thing though (especially regarding coercions)... * New tool to automatically infer (some) Record/Typeclasses instances. Usage : [Record/Class *Infer* X := ...] flags a record/class as subject to instance search. There is also an option to activate/deactivate the search [Set/Unset Autoinstance]. It works by finding combinations of definitions (actually all kinds of objects) which forms a record instance, possibly parameterized. It is activated at two moments: - A complete search is done when defining a new record, to find all possible instances that could have been formed with past definitions. Example: Require Import List. Record Infer Monoid A (op:A->A->A) e := { assoc : forall x y z, op x (op y z) = op (op x y) z; idl : forall x, x = op x e ; idr : forall x, x = op e x }. new instance Monoid_autoinstance_1 : (Monoid nat plus 0) [...] - At each new declaration (Definition, Axiom, Inductive), a search is made to find instances involving the new object. Example: Parameter app_nil_beg : forall A (l:list A), l = nil ++ l. new instance Build_Monoid_autoinstance_12 : (forall H : Type, Monoid (list H) app nil) := (fun H : Type => Build_Monoid (list H) app nil ass_app (app_nil_beg H) (app_nil_end H)) For the developper ================== * New yet-to-be-named datastructure in [lib/dnet.ml]. Should do efficient one-to-many or many-to-one non-linear first-order filtering, faster than traditional methods like discrimination nets (so yes, the name of the file should probably be changed). * Comes with its application to Coq's terms [pretyping/term_dnet.ml]. Terms are represented so that you can search for patterns under products as fast as you would do not under products, and facilities are provided to express other kind of searches (head of application, under equality, whatever you need that can be expressed as a pattern) * A global repository of all objects defined and imported is maintained [toplevel/libtypes.ml], with all search facilities described before. * A certain kind of proof search in [toplevel/autoinstance.ml]. For the moment it is specialized on finding instances, but it should be generalizable and reusable (more on this in a few months :-). The bad news ============ * Compile time should increase by 0 to 15% (depending on the size of the Requires done). This could be optimized greatly by not performing substitutions on modules which are not functors I think. There may also be some inefficiency sources left in my code though... * Vo's also gain a little bit of weight (20%). That's inevitable if I wanted to store the big datastructure of objects, but could also be optimized some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
| | | | | | | | | identity. Add notations for compatibility and support for understanding these notations in the ml files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11729 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:32:32 +0000