aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* More optimisations of partial applications.Gravatar aspiwack2013-11-02
| | | | | | | | | | This time in Goal. Patch by Pierre-Marie Pédrot. Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16992 85f007b7-540e-0410-9357-904b9bb8a0f7
* Try to remove intermediate allocations when dealing with goal-specific tactics.Gravatar aspiwack2013-11-02
| | | | | | Introduces a primitive Goal.enter which allows to access the common information needed by goal-specific tactics, avoids a number of monadic binds, and some unnecessary allocations of lists. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various rewriting, mostly for speed purposes.Gravatar aspiwack2013-11-02
| | | | | | | | | - A variant of tclEVARS directly in the language of the monad - A variant of tclDISPATCHGEN (tclINDEPENDENT) hopefully faster in the case there is only one tactic to copy - A better written tclDISPATCHGEN (which may make thing actually a little slower) - A special case in tclDISPATCHGEN and tclINDEPENDENT for the case when they are 0 or 1 goals (adaptation of a patch sent by Pierre-Marie Pédrot) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16990 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimisation of partial applications in the tactic monad.Gravatar aspiwack2013-11-02
| | | | | | | | | | Explanations here: https://ocaml.janestreet.com/?q=node/30 Patch by Pierre-Marie Pédrot, with modifications from Arnaud Spiwack. Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes parsing of all: followed by a typechecking/evaluation command.Gravatar aspiwack2013-11-02
| | | | | | | | Exceptions raised during parsing are caught by the parser and result in weird parsing behaviour. Instead I added a special case in vernac_expr which always raises an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix behaviour of the refine tactic with respect to evars in types.Gravatar aspiwack2013-11-02
| | | | | | | It used not to propagate discovered constraints on the evars of the conclusion of the goal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small syntax fix to be compatible with Ocaml 3.11.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16986 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makes the Ltac debugger usable again.Gravatar aspiwack2013-11-02
| | | | | | | This is just a port of the existing design. Basing the tactics on an IO monad may allow to simplify things a bit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16985 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document "all:" and "Set Default Goal Selector".Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16984 85f007b7-540e-0410-9357-904b9bb8a0f7
* New option Default Goal Selector.Gravatar aspiwack2013-11-02
| | | | | | | Set Default Goal Selector "all" prefixes all tactics with "all:" if no selector is specified (it is overridden by 1: for instance). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
| | | | | | all:tac applies tac to all the focused subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replaced monads.ml by an essentially equivalent proofview_gen.ml generated ↵Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | | | | | | | | | | | | by extraction. The goal was to use Coq's partial evaluation capabilities to do manually some inlining that Ocaml couldn't do. It may be critical as we are defining higher order combinators in term of others and no inlining means a lot of unnecessary, short-lived closures built. With this modification we get back some (but not all) of the loss of performance introduced by threading the monadic type all over the place. I still have an estimated 15% longer compilation time for Coq. Makes use of Set Extraction Conservative Types and Set Extraction File Comment to maintain the relationship between the functions and their types. Uses an intermediate layer Proofview_monad between Proofview_gen and Proofview in order to use a hand-written mli to catch potential errors in the generated file (it uses Extract Constant a lot). A bug in the extraction of signatures forces to remove the generated proofview_gen.mli which does not have the correct types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16981 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).Gravatar aspiwack2013-11-02
| | | | | | | | They were a hack to avoid looking where exceptions were raised and not caught. Hopefully I produce a cleaner stack now, catching errors when it is needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16980 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removes Refine from the dev tools now that the module has been deleted.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16979 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean up a warning.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16978 85f007b7-540e-0410-9357-904b9bb8a0f7
* The tactic [admit] exits with the "unsafe" status.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | It is highlighted in yellow in Coqide. The unsafe status is tracked throughout the execution of tactics such that nested calls to admit are caught. Many function (mainly those building constr with tactics such as typeclass related stuff, and Function, and a few other like eauto's use of Hint Extern) drop the unsafe status. This is unfortunate, but a lot of refactoring would be in order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup of comments.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plug back the declarative mode.Gravatar aspiwack2013-11-02
| | | | | | It seems to work ok, but I'm not too confident in the long run. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small change to the IO monad interface: [val ref : 'a -> 'a ref t]Gravatar aspiwack2013-11-02
| | | | | | | | It doesn't matter much, it's simply a matter of aesthetic, so that all functions in the interface of [Monads.IO] are pure ([IO.run] being the only impure function but it's not part of the generic interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16974 85f007b7-540e-0410-9357-904b9bb8a0f7
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
| | | | | | | | | | | It now uses the same algorithm as pretyping does. This produces pretty weird goal when refining pattern matching terms. Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now. The file Zsqrt_compat.v has two temporary [Admitted] related to this issue. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16973 85f007b7-540e-0410-9357-904b9bb8a0f7
* A newly introduced variable inside a named context is no longer α-renamed.Gravatar aspiwack2013-11-02
| | | | | | | | | Instead, in case of collision, the older name is substituted for a fresh one. It should also be made inaccessible from the user, but I'll leave this for later. The goal is to guarantee that [refine (fun x => _)] introduces a binder named [x]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bases tactics on an IO monad.Gravatar aspiwack2013-11-02
| | | | | | | | | It allowed to restore the timeout tactics. It also prepares for the debugging mechanism to be restored. ['a IO.t] is just [unit -> 'a]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16970 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
| | | | | | It was a bad idea. The new API based on lists seems more sensible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uses Proofview.tclEXTEND more sparingly.Gravatar aspiwack2013-11-02
| | | | | | | It is used where failures can be caughts (tclORELSE, tclTRY, …) rather than at each tclTHEN. Hopefully avoiding making things a bit less slow. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the compilation of Coq, we can see an increase of ~20% compile time on my completely non-scientific tests. Hopefully this can be fixed. There are a lot of low hanging fruits, but this is an iso-functionality commit. With a few exceptions which were not necessary for the compilation of the theories: - The declarative mode is not yet ported - The timeout tactical is currently deactivated because it needs some subtle I/O. The framework is ready to handle it, but I haven't done it yet. - For much the same reason, the ltac debugger is unplugged. It will be more difficult, but will eventually be back. A few comments: I occasionnally used a coercion from [unit Proofview.tactic] to the old [Prooftype.tactic]. It should work smoothely, but loses any backtracking information: the coerced tactics has at most one success. - It is used in autorewrite (it shouldn't be a problem there). Autorewrite's code is fairly old and tricky - It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes as we might want to have various success in a "Hint Extern". But it would require a heavy port of eauto.ml4 - It is used in typeclass eauto, but with a little help from Matthieu, it should be easy to port the whole thing to the new tactic engine, actually simplifying the code. - It is used in fourier. I believe it to be inocuous. - It is used in firstorder and congruence. I think it's ok. Their code is somewhat intricate and I'm not sure they would be easy to actually port. - It is used heavily in Function. And honestly, I have no idea whether it can do harm or not. Updates: (11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based architecture for Ltac matching (r16533), which avoid painfully and expensively working around the exception-throwing control flow of the previous API. (11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730) rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma, rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially tclREPEAT, causing rewrites to be tried in the side-conditions of conditional rewrites as well). The new implementation makes Coq faster, but it is pretty much impossible to tell if it is significant at all. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Closure: fix an issue with r16959 spotted by MatthieuGravatar letouzey2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)Gravatar letouzey2013-10-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit should fix the contrib ProjectiveGeometry This update_delta_resolver is in fact a sequential composition (resolver1 then resolver2). The earlier version was strangely favoring the bindings coming from resolver2 over the bindings coming from (resolver1 chained with resolver2). So any inlining information stored in resolver1 could be discarded savagely. Apparently, this situation wasn't occurring in practice until recently, when I started to do lots of Mod_subst.join for improving the size of modular libobjects in the vo's. So, when combining two resolvers now : - Inline(_,None) is the weakest information, it's just a declaration that we intend to inline this kn someday if possible (i.e. when we'll have a transparent implementation for it). This kind of Inline is only relevant inside a module type. - Equiv(_) should only appear in modules (after some Include) so it should be ok if it takes precedence over any Inline(_,None) remaining in the other resolver. - Inline(_,Some _) is there after functor application (cf inline_delta_resolver) : we've done the inlining, so we don't care anymore about other Equiv(_) or Inline(_,None) informations about this kn, since we have anyway a new body for it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16965 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Kerpair.hash. Since the beginning, it dit not respect the typeGravatar ppedrot2013-10-31
| | | | | | equality, maybe impeding hashconsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
| | | | | | | | | | | This optimization was undone because the kernel type checking was not a pure functions (it was accessing the conv_oracle state imperatively). Now that the conv_oracle state is part of env, the optimization can be restored. This was the cause of the increase in memory consumption, since it was forcing to keep a copy of the system state for every proof, even the ones that are not delayed/delegated to slaves. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: scroll to the right position if there is an interp errorGravatar gareuselesinge2013-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16962 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
| | | | | | But for vm, the kernel should be functional now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Efficient filtered functions in Evd. We test that a filter is actuallyGravatar ppedrot2013-10-31
| | | | | | | | | | different from the identity before trying to compute filtered env/hyps. According to profiling, it seems that the filter operation is NEVER taken, that is, all filters that reach toplevel are dummy. There is surely something to do here... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16960 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoiding useless allocations in Closure.Gravatar ppedrot2013-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various optimizations of Evd.meta_* functions.Gravatar ppedrot2013-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16958 85f007b7-540e-0410-9357-904b9bb8a0f7
* More efficient implementation of [Evd.retract_coercible_metas].Gravatar ppedrot2013-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimization in unification: when checking that the head of a term is anGravatar ppedrot2013-10-29
| | | | | | | | | | | evar or a meta, don't reconstruct the whole term. This hopefully saves a lot of useless allocations and computing time. I may have slightly changed the heuristic though, as only evars in front of applications where recognized as such, whereas now this pass through cases and fixpoints. I am walking on thin ice, but the test-suite was OK... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16956 85f007b7-540e-0410-9357-904b9bb8a0f7
* Useless array-to-list casts in Unification.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16955 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16953 85f007b7-540e-0410-9357-904b9bb8a0f7
* [Reductionops.append_stack_app]: do not allocate a useless array.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert the two last commits. My bad, I messed up git-svn commands...Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Profile only when CAMLRUNPARAM is set.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Printing heap on every processed sentence.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16949 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sharing identity evar filters.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allocation-friendly version of [Pre_env.push_named].Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimizing universes: tail-rec, allocation friendly [compare_leq].Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16946 85f007b7-540e-0410-9357-904b9bb8a0f7
* - install evar printer for debuggingGravatar msozeau2013-10-29
| | | | | | | | - make unification try canonical structures before expansion as in evar_conv - add a fast path to evar inversion (patch from B. Ziliani). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16945 85f007b7-540e-0410-9357-904b9bb8a0f7
* Native compiler: library compilation errors are now non fatal.Gravatar mdenes2013-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar leak in "absurd" tactic.Gravatar ppedrot2013-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16943 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-07 15:01:42 +0000