diff options
Diffstat (limited to 'plugins/ssr/ssrast.mli')
| -rw-r--r-- | plugins/ssr/ssrast.mli | 175 |
1 files changed, 175 insertions, 0 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli new file mode 100644 index 00000000..7f5f2f63 --- /dev/null +++ b/plugins/ssr/ssrast.mli @@ -0,0 +1,175 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) + +open Names +open Ltac_plugin + +(* Names of variables to be cleared (automatic check: not a section var) *) +type ssrhyp = SsrHyp of Id.t Loc.located +(* Variant of the above *) +type ssrhyp_or_id = Hyp of ssrhyp | Id of ssrhyp + +(* Variant of the above *) +type ssrhyps = ssrhyp list + +(* Direction to be used for rewriting as in -> or rewrite flag *) +type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir = L2R | R2L + +(* simpl: "/=", cut: "//", simplcut: "//=" nop: commodity placeholder *) +type ssrsimpl = Simpl of int | Cut of int | SimplCut of int * int | Nop + +(* modality for rewrite and do: ! ? *) +type ssrmmod = May | Must | Once + +(* modality with a bound for rewrite and do: !n ?n *) +type ssrmult = int * ssrmmod + +(** Occurrence switch {1 2}, all is Some(false,[]) *) +type ssrocc = (bool * int list) option + +(* index MAYBE REMOVE ONLY INTERNAL stuff between {} *) +type ssrindex = int Misctypes.or_var + +(* clear switch {H G} *) +type ssrclear = ssrhyps + +(* Discharge occ switch (combined occurrence / clear switch) *) +type ssrdocc = ssrclear option * ssrocc + +(* OLD ssr terms *) +type ssrtermkind = char (* FIXME, make algebraic *) +type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr + +(* NEW ssr term *) + +(* These terms are raw but closed with the intenalization/interpretation + * context. It is up to the tactic receiving it to decide if such contexts + * are useful or not, and eventually manipulate the term before turning it + * into a constr *) +type ast_closure_term = { + body : Constrexpr.constr_expr; + glob_env : Genintern.glob_sign option; (* for Tacintern.intern_constr *) + interp_env : Geninterp.interp_sign option; (* for Tacinterp.interp_open_constr_with_bindings *) + annotation : [ `None | `Parens | `DoubleParens | `At ]; +} + +type ssrview = ast_closure_term list + +(* TODO +type id_mod = Hat | HatTilde | Sharp + *) + +(* Only [One] forces an introduction, possibly reducing the goal. *) +type anon_iter = + | One + | Drop + | All +(* TODO + | Dependent (* fast mode *) + | UntilMark + | Temporary (* "+" *) + *) + +type ssripat = + | IPatNoop + | IPatId of (*TODO id_mod option * *) Id.t + | IPatAnon of anon_iter (* inaccessible name *) +(* TODO | IPatClearMark *) + | IPatDispatch of ssripatss (* /[..|..] *) + | IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *) + | IPatInj of ssripatss + | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir + | IPatView of ssrview (* /view *) + | IPatClear of ssrclear (* {H1 H2} *) + | IPatSimpl of ssrsimpl + | IPatAbstractVars of Id.t list + | IPatTac of unit Proofview.tactic + +and ssripats = ssripat list +and ssripatss = ssripats list +type ssrhpats = ((ssrclear * ssripats) * ssripats) * ssripats +type ssrhpats_wtransp = bool * ssrhpats + +(* tac => inpats *) +type ssrintrosarg = Tacexpr.raw_tactic_expr * ssripats + + +type ssrfwdid = Id.t +(** Binders (for fwd tactics) *) +type 'term ssrbind = + | Bvar of Name.t + | Bdecl of Name.t list * 'term + | Bdef of Name.t * 'term option * 'term + | Bstruct of Name.t + | Bcast of 'term +(* We use an intermediate structure to correctly render the binder list *) +(* abbreviations. We use a list of hints to extract the binders and *) +(* base term from a term, for the two first levels of representation of *) +(* of constr terms. *) +type ssrbindfmt = + | BFvar + | BFdecl of int (* #xs *) + | BFcast (* final cast *) + | BFdef (* has cast? *) + | BFrec of bool * bool (* has struct? * has cast? *) +type 'term ssrbindval = 'term ssrbind list * 'term + +(** Forward chaining argument *) +(* There are three kinds of forward definitions: *) +(* - Hint: type only, cast to Type, may have proof hint. *) +(* - Have: type option + value, no space before type *) +(* - Pose: binders + value, space before binders. *) +type ssrfwdkind = FwdHint of string * bool | FwdHave | FwdPose +type ssrfwdfmt = ssrfwdkind * ssrbindfmt list + +(* in *) +type ssrclseq = InGoal | InHyps + | InHypsGoal | InHypsSeqGoal | InSeqGoal | InHypsSeq | InAll | InAllHyps + +type 'tac ssrhint = bool * 'tac option list + +type 'tac fwdbinders = + bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)) + +type clause = + (ssrclear * ((ssrhyp_or_id * string) * + Ssrmatching_plugin.Ssrmatching.cpattern option) option) +type clauses = clause list * ssrclseq + +type wgen = + (ssrclear * + ((ssrhyp_or_id * string) * + Ssrmatching_plugin.Ssrmatching.cpattern option) + option) + +type 'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses +type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option) + + +open Ssrmatching_plugin +open Ssrmatching + +type 'a ssrcasearg = ssripat option * ('a * ssripats) +type 'a ssrmovearg = ssrview * 'a ssrcasearg + +type ssrdgens = { dgens : (ssrdocc * cpattern) list; + gens : (ssrdocc * cpattern) list; + clr : ssrclear } +type 'a ssragens = (ssrdocc * 'a) list list * ssrclear +type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats) + +(* OOP : these are general shortcuts *) +type gist = Tacintern.glob_sign +type ist = Tacinterp.interp_sign +type goal = Goal.goal +type 'a sigma = 'a Evd.sigma +type v82tac = Tacmach.tactic |