aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacinterp.mli
Commit message (Collapse)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
| | | | | instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
| | | | | Left a README, just in case someone will discover the remnants of it decades from now.
* Proper interpretation function for tauto.Gravatar Pierre-Marie Pédrot2014-09-06
| | | | | | | | | Instead of passing glob tactics through the infamous globTacticIn hack and antiquotation feature of the Ltac syntax, we put them in the interpretation environment as closures. This should be used everywhere to get rid of this buggy antiquotation syntax. This fixes bug #2800.
* Adding a way to inject tactic closures in interpretation values.Gravatar Pierre-Marie Pédrot2014-09-06
|
* Add [guard] tactic.Gravatar Arnaud Spiwack2014-08-01
| | | | | | | | The [guard] tactic accepts simple tests (on integers) as argument, succeeds if the test passes and fails if the test fails. Together with [numgoal] can be used to fork on the number of goals of a tactic. The syntax is not very robust (in particular [guard n<=1] is correct but not [guard (n<=1)]). Maybe tests should be moved to the general parser to allow for more flexibility.
* The tactic interpreter now uses a new type of tactics, throughGravatar Pierre-Marie Pédrot2014-06-03
| | | | | | | | | | | the GTac module. A ['a Gtac.t] is a special case of tactic that may depend on the current goals, or not. Internally, it construct a list of results, one for each focussed goal, if the tactic is actually dependent. This allows for an interpretation of whole-goal tactic that does work, which was not the case for the previous implementation, which did to many Proofview.Goal.enter.
* Revert "Chasing the goal entering backward while interpreting tactics. This ↵Gravatar Pierre-Marie Pédrot2014-05-24
| | | | | | | | required" I tested the commit on the wrong branch... This reverts commit b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04.
* Chasing the goal entering backward while interpreting tactics. This requiredGravatar Pierre-Marie Pédrot2014-05-24
| | | | | writing a new primitive recovering the first goal under focus. It sounds a bit hackish, but it does actually work.
* Tactics declared through TACTIC EXTEND that are of the formGravatar Pierre-Marie Pédrot2014-05-20
| | | | | | | | | "foobar" constr(x1) ... constr(xn) are now defined as pure Ltac definitions, and do not add grammar nor printing rules. This partially relies on a hack consisting in retrieving the arguments in the tactic environment rather than as directly passed to the TacExtend node.
* Adding phantom types to discriminate normalized goals, and adding a way toGravatar Pierre-Marie Pédrot2014-03-19
| | | | observe non-normalized goals.
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Tacinterp: spurious enterl.Gravatar Arnaud Spiwack2014-02-27
| | | This changes the tacinterp API, but only affects (one line of) the MapleMode contrib.
* Dead code: eval_ltac_constr.Gravatar Arnaud Spiwack2014-02-27
|
* Do not use ugly Dyn features in the Quote plugin. Use instead theGravatar Pierre-Marie Pédrot2013-11-26
| | | | provided tactic environment to handle open terms.
* Tacinterp: fewer use of old-style goals.Gravatar Arnaud Spiwack2013-11-25
| | | | | | There are many functions in Tacinterp which use a goal as a proxy for the pair of an environment and an evar_map. But do not build LCF tactics with them. They don't play well with the new style of tactics. I've changed some of them to explicitely take an environment and an evar_map instead.
* Centralizing the Ltac-defining functions in Tacenv.Gravatar ppedrot2013-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made multiple-goal tactic work after all: .Gravatar aspiwack2013-11-02
| | | | | | | | Internalization was done relative to a goal. It doesn't make sense in the case of all:. When we make a tactic with all: the environment for internalization is taken to be the global environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17016 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
* 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
* Cleaning up the type of Tacinterp.extract_ltac_constr_values.Gravatar ppedrot2013-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now, idtac closures use maps instead of association list.Gravatar ppedrot2013-06-22
| | | | | | | | The semantics changed slightly so it may break some scripts, though it is very unlikely, as they would have to be quite intricated and poorly written. Indeed, the test-suite passed just fine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
| | | | | | of tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
| | | | | | | | | | | | | 1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing the various glob/subst/interp registering functions forGravatar ppedrot2013-06-18
| | | | | | extra argument types and putting them into Genarg. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16586 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now glob_sign and interp_sign only depend on structures definedGravatar ppedrot2013-06-18
| | | | | | | upto Genarg, so moved them there. This will allow defining the new genarg interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16584 85f007b7-540e-0410-9357-904b9bb8a0f7
* Exporting field f_debug (needed for Ssreflect).Gravatar ppedrot2013-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using an "extra" Store.t field in interp_sign instead of dedicatedGravatar ppedrot2013-06-14
| | | | | | record fields. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving coercion functions out of Tacinterp.Gravatar ppedrot2013-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hiding tactic value representations.Gravatar ppedrot2013-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing lists by maps in matching interpretation.Gravatar ppedrot2013-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Make ist (interp_sign) available to TACTIC EXTEND codeGravatar gareuselesinge2013-05-29
| | | | | | | In order to do so I had to move the data base of tactics to tacinterp (from tacintern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16540 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 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
* Dump references in reduction tacticsGravatar pboutill2012-08-05
| | | | | | Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
| | | | | | | | | | were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
| | | | | | | | | Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrects a (very) longstanding bug of tactics. As is were, tactic expectingGravatar aspiwack2012-04-18
| | | | | | | | | | | | | | | | constr as argument (rather than openconstr) assumed that the evar_map output by pretyping was irrelevant as the final constr didn't have any evars. However, if said constr was defined using pre-existing evars from the context, the evars may be instantiated by pretyping, hence dropping the output evar_map led to inconsistent proof terms. This fixes bug #2739 ( https://coq.inria.fr/bugs/show_bug.cgi?id=2739 ). Thanks Arthur for noticing it. Note: change still has the bug, because more serious issues interfered with my fix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15207 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicGravatar herbelin2012-03-20
| | | | | | | | | | | | tactic arguments of ltac functions). Added support for recursive entries in ARGUMENT EXTEND, for right-hand sides of ARGUMENT EXTEND raising exceptions and for right-hand sides referring to "loc". Also fixed parsing level of initial value in create_arg (raw instead of glob). Thanks to the Ssreflect plugin for revealing these problems. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15065 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
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
| | | | | | | | | | | how the names of an ltac expression are globalized - allowing the expression to be a constr and in some initial context - and when and how this ltac expression is interpreted - now expecting a pure tactic in a different context). This incidentally found a Ltac bug in Ncring_polynom! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
| | | | | | Tactics set/remember and destruct/induction take benefit of it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14499 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving implicit tactic support from Tacinterp to Pfedit and final evarGravatar herbelin2011-09-26
| | | | | | | resolution from Tacinterp to Pretyping (close to resolve_evars) so that final evar resolution can eventually be called from Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14496 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename subst_raw_with_bindings to subst_glob_with_bindings and exportGravatar msozeau2011-02-10
| | | | | | | it, properly apply substitution to setoid_rewrite arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13818 85f007b7-540e-0410-9357-904b9bb8a0f7
* One more fix for setoid_rewrite: completely reinterpret the given lemmasGravatar msozeau2011-02-09
| | | | | | | | in the current goal, generating fresh evars and metas for unification (fixes contrib ATBR). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13816 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 14:24:38 +0000