aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Misc small fixes : warning, dep cycles, ocamlbuild...Gravatar letouzey2010-04-26
| | | | | | | | | | | | - git ignore g_decl_mode.ml - exhaustive match for pp_vernac (BeginSubproof, ...) - for ocamlbuild, remove a spurious cycle in recordops.mli (unnecessary open of Classops), and fixes of *.itargets and _tags The compilation via ocamlbuild still need some work, since plugin firstorder now depends on the new plugin decl_mode git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a fairly large commit (around 140 files and 7000 lines of code impacted), it will cause some troubles for sure (I've listed the know regressions below, there is bound to be more). At this state of developpement it brings few features to the user, as the old tactics were ported with no change. Changes are on the side of the developer mostly. Here comes a list of the major changes. I will stay brief, but the code is hopefully well documented so that it is reasonably easy to infer the details from it. Feature developer-side: * Primitives for a "real" refine tactic (generating a goal for each evar). * Abstract type of tactics, goals and proofs * Tactics can act on several goals (formally all the focused goals). An interesting consequence of this is that the tactical (. ; [ . | ... ]) can be separated in two tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for this particular syntax). We can also imagine a tactic to reorder the goals. * Possibility for a tactic to pass a value to following tactics (a typical example is an intro function which tells the following tactics which name it introduced). * backtracking primitives for tactics (it is now possible to implement a tactical '+' with (a+b);c equivalent to (a;c+b;c) (itself equivalent to (a;c||b;c)). This is a valuable tool to implement tactics like "auto" without nowing of the implementation of tactics. * A notion of proof modes, which allows to dynamically change the parser for tactics. It is controlled at user level with the keywords Set Default Proof Mode (this is the proof mode which is loaded at the start of each proof) and Proof Mode (switches the proof mode of the current proof) to control them. * A new primitive Evd.fold_undefined which operates like an Evd.fold, except it only goes through the evars whose body is Evar_empty. This is a common operation throughout the code, some of the fold-and-test-if-empty occurences have been replaced by fold_undefined. For now, it is only implemented as a fold-and-test, but we expect to have some optimisations coming some day, as there can be a lot of evars in an evar_map with this new implementation (I've observed a couple of thousands), whereas there are rarely more than a dozen undefined ones. Folding being a linear operation, this might result in a significant speed-up. * The declarative mode has been moved into the plugins. This is made possible by the proof mode feature. I tried to document it so that it can serve as a tutorial for a tactic mode plugin. Features user-side: * Unfocus does not go back to the root of the proof if several Focus-s have been performed. It only goes back to the point where it was last focused. * experimental (non-documented) support of keywords BeginSubproof/EndSubproof: BeginSubproof focuses on first goal, one can unfocus only with EndSubproof, and only if the proof is completed for that goal. * experimental (non-documented) support for bullets ('+', '-' and '*') they act as hierarchical BeginSubproof/EndSubproof: First time one uses '+' (for instance) it focuses on first goal, when the subproof is completed, one can use '+' again which unfocuses and focuses on next first goal. Meanwhile, one cas use '*' (for instance) to focus more deeply. Known regressions: * The xml plugin had some functions related to proof trees. As the structure of proof changed significantly, they do not work anymore. * I do not know how to implement info or show script in this new engine. Actually I don't even know what they were suppose to actually mean in earlier versions either. I wager they would require some calm thinking before going back to work. * Declarative mode not entirely working (in particular proofs by induction need to be restored). * A bug in the inversion tactic (observed in some contributions) * A bug in Program (observed in some contributions) * Minor change in the 'old' type of tactics causing some contributions to fail. * Compilation time takes about 10-15% longer for unknown reasons (I suspect it might be linked to the fact that I don't perform any reduction at QED-s, and also to some linear operations on evar_map-s (see Evd.fold_undefined above)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: cosmetics when using ocaml + Extract Inductive to symbolsGravatar letouzey2010-04-16
| | | | | | | | | | | - When using an infix constructor such as (::), whitespaces are to be given by the user, for instance Extract Inductive list => list [ "[]" "( :: )" ]. - Remove ugly whitespaces when using the ""-for-Pair trick: Extract Inductive prod => "(*)" [ "" ]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: restore (temporarily?) a very limited form of linear letin reductionGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12943 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: less eta in calls to global functions, better optimization phaseGravatar letouzey2010-04-16
| | | | | | | | | | | | - we saturate the normalize function : as long as (kill_dummy + simpl) isn't a nop, we do it again. - generalize_case allowed on all types of theories/Init/*.v instead of only bool,sumbool,sumor. NB: this optim cannot be performed on any type, it might produce untyped code. - common_branch allowed on match with one branch: in this situation it indicates whether the match can be removed or not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12942 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: improvement of optimizations (kill_dummy, optim_fix)Gravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12940 85f007b7-540e-0410-9357-904b9bb8a0f7
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: ad-hoc identifier type with annotations for reductionsGravatar letouzey2010-04-16
| | | | | | | | | | | | | | | | * An inductive constructor Dummy instead of a constant dummy_name * The Tmp constructor indicates that the corresponding MLlam or MLletin is extraction-specific and can be reduced if possible * When inlining a glob (for instance a recursor), we tag some lambdas as reducible. In (nat_rect Fo Fs n), the head lams of Fo and Fs are treated this way, in order for the recursive call inside nat_rect to be correctly pushed as deeper as possible. * This way, we can stop allowing by default linear beta/let reduction even under binders (can be activated back via Set Extraction Flag). * Btw, fix the strange definition of non_stricts for (x y). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12938 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: less _ in Haskell (typically for False_rect), less toplevel ↵Gravatar letouzey2010-04-16
| | | | | | eta-expansions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Look for csdp in $PATH at runtime, remove -csdpdir configure optionGravatar glondu2010-04-11
| | | | | | | | | The csdp path computed by the configure script wasn't used at all, but was forcing presence of csdp at configure time whereas it is not used at all in the build process. Instead, we replace the configure-time check with a runtime check for existence of csdp in $PATH. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove unused functions run_sdpaGravatar glondu2010-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using ↵Gravatar letouzey2010-03-30
| | | | | | ide/proof git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - make links to section variables working (used qualified names for disambiguation and fixed the place in intern_var where to dump them) (wish #2277) - mapping of physical to logical paths now follows coq (see bug #2274) (incidentally, it was also incorrectly seeing foobar.v as a in directory foo) - added links for notations - added new category "other" for indexing entries not starting with latin letter (e.g. notations or non-latin identifiers which was otherwise broken) - protected non-notation strings (from String.v) from utf8 symbol interpretation - incidentally quoted parseable _ in notations to avoid confusion with placeholder in the "_ + _" form of notation - improved several "Sys_error" error messages - fixed old bug about second dot of ".." being interpreted as regular dot - removed obsolete lexer in index.mll (and renamed index.mll to index.ml) - added a test-suite file for testing various features of coqdoc Things that still do not work: - when a notation is redefined several times in the same scope, only the link to the first definition works - if chars and symbols are not separated in advance, idents that immediately follow symbols are not detected (e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}") - parentheses, curly brackets and semi-colon not linked in notations Things that can probably be improved: - all notations are indexed in the same category "other"; can we do better? - all non-latin identifiers (e.g. Greek letters) are also indexed in the same "other" category; can we do better? - globalization data for notations could be compacted (currently there is one line per each proper location covered by the notation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oops, don't use zeta by default.Gravatar msozeau2010-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix splitting evars tactics and stop dropping evar constraints whenGravatar msozeau2010-03-15
| | | | | | | | | building a new goal evar defs. Allow customization of the reduction function applied to subtac obligations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12867 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
* Consider OccurCheck a catchable exception.Gravatar msozeau2010-03-08
| | | | | | | Fix minor bug in Program wellfounded definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application des patches envoyés par F. Besson pour micromegaGravatar notin2010-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder resolution of type class and unification constraints.Gravatar msozeau2010-03-07
| | | | | | | | Fix a bug in dependent elimination when treating defined variables in the context. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
| | | | | | | | | informative exception if some constraints do not unify. All calls except one used to raise a less informative exception when the constraints weren't solved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in generalized rewriting:Gravatar msozeau2010-03-05
| | | | | | | | | | | | | | - support a new strategy: reduction using any of the allowed reduction operators. This strategy does _not_ make the proof size grow. - support rewriting under arbitrary [match with] using a folding strategy. We fold matches to applications of registered [case] combinators and let the user declare the Proper instances for them. - fix the lemma application strategy to correctly report when no progress has been made (avoids loop when repeateadly rewriting with convertible terms). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a generic tactic option builder. Use it in firstorder to set theGravatar msozeau2010-03-05
| | | | | | | | | default solver (using "Set Firstorder Solver") and for program's obligation tactic. I don't understand exactly the reason of the warning when building states/initial.coq, anyone? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12842 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration mineure dans FunctionGravatar jforest2010-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Win32 cross-compilation from debian: build of coqide.exe and other binariesGravatar letouzey2010-02-24
| | | | | | | | | | | | Details will follow. In a word, we use a gtk+ win32 bundle from gtk.org to build some (unofficial) mingw32-liblablgtk2 debian packages. Then ./configure -local && ./build win32 is enough to get all native win32 binaries and plugin cmxs from a confortable linux box. Next step: an auto-installer :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12804 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction of bug #2088Gravatar jforest2010-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix sort_dependencies for good, maintaining the initial order.Gravatar msozeau2010-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12780 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug in field_simplify_eq inGravatar barras2010-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Euclidean division for NArithGravatar letouzey2010-02-10
| | | | | | | | | There was already a Ndiv and Nmod, but hiddent in ZOdiv_def. We higlight it by putting it in a separate file, prove its specification without using Z (but for the moment can't avoid a detour via nat, though), and then instantiate general results from Natural/Abstract/NDiv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
| | | | | | | dependency order of obligations that was not backwards-compatible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
| | | | | | | | Let's avoid writing huge "Eval ... in ..." lines :-) Will be used in particular soon in NMake for defining function via Definition ... := Eval ... in ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backport fixes in Instance declarations to Program Instance.Gravatar msozeau2010-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add [Next Obligation with tactic] support (wish #1953).Gravatar msozeau2010-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12691 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2086, error message when we match on an non-inductive type.Gravatar msozeau2010-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12669 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Show Obligation TacticGravatar msozeau2010-01-14
| | | | | | | - fix bug #1952. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12668 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
| | | | | | | | Update Numbers that was implicitely using [simpl_relation] instead of the default tactic [program_simpl]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
| | | | | | | | | NB: the grammar entry is placed in vernac:command on purpose even if it should have gone into vernac:gallina_ext. Camlp4 isn't factorising rules starting by "Declare" in a correct way otherwise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Few misc. updates.Gravatar herbelin2010-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12622 85f007b7-540e-0410-9357-904b9bb8a0f7
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
| | | | | | | | | | | | | | | - to type patterns w/o losing the information of what subterm is a hole would need to remember where holes were in "understand", but "understand" needs sometimes to instantiate evars to ensure the type of an evar is not its original type but the type of its instance (what can e.g. lower a universe level); we would need here to update evars type at the same time we define them but this would need in turn to check the convertibility of the actual and expected type since otherwise type-checking constraints may disappear; - typing pattern is apparently expensive in time; is it worth to do it for the benefit of pattern-matching compilation and coercion insertion? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We renounced to distribute evars to constr and bindings and to let tactics do the merge. There are now two disciplines: - the general case is that the holes in tactic arguments are pushed to the general sigma of the goal so that tactics have no such low-level tclEVARS, Evd.merge, or check_evars to do: - what takes tclEVARS and check_evars in charge is now a new tactical of name tclWITHHOLES (this tactical has a flag to support tactics in either the "e"- mode and the non "e"- mode); - the merge of goal evars and holes is now done generically at interpretation time (in tacinterp) and as a side-effect it also anticipates the possibility to refer to evars of the goal in the arguments; - with this approach, we don't need such constr/open_constr or bindings/ebindings variants and we can get rid of all ugly inj_open-style coercions; - some tactics however needs to have the exact subset of holes known; this is the case e.g. of "rewrite !c" which morally reevaluates c at each new rewriting step; this kind of tactics still receive a specific sigma around their arguments and they have to merge evars and call tclWITHHOLES by themselves. Changes so that each specific tactics can take benefit of this generic support remain to be done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Const_omega: look for S in Init only (avoid future clash with S of Numbers)Gravatar letouzey2009-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12597 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction de la nouvelle option pour functional inductionGravatar jforest2009-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12593 85f007b7-540e-0410-9357-904b9bb8a0f7
* adding an option functional_induction_rewrite_dependent to make functional ↵Gravatar jforest2009-12-16
| | | | | | induction using not v8.2 version of subst. By default functional induction uses new version of subst git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12592 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
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
| | | | | | | | | | - made the new "subst'" the default by renaming it "subst"; - renamed old "subst" into "simple subst"; - add option for non-rewriting of dependent proofs in general_rewrite and co - kept use of dependent proofs in the "subst" call of "functional induction", in spite it introduced incompatibilities (in Compcert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵Gravatar letouzey2009-12-09
| | | | | | | | | | | | in */*/vo.itarget On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the build of coq via ocamlbuildGravatar letouzey2009-12-08
| | | | | | | | - no more plugins/interface - a few missing files in theories.itarget - a few things required Unix now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12572 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sos.ml: no more warningsGravatar letouzey2009-12-08
| | | | | | | | | apart for a few non-exhaustive patterns, there was also some unused let-in variables. Hard to check whether the apparently useless code is doing some side-effect or not... It seems not, so I've removed completely the corresponding code. Frederic, is that ok ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
| | | | | | | | | | - fixed misunderstanding of the role of nenv while simplifying code of occur_id in namegen.ml, - documented the possible incompatibilites in CHANGES - fixed output/Naming.v test, and fixed the count of misc. tests in test-suite/check. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12556 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove interface pluginGravatar glondu2009-12-02
| | | | | | It has moved to the contribs (Sophia-Antipolis/Interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 19:00:36 +0000