Merge the ssr plugin.

1 files changed, 149 insertions, 0 deletions

diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
new file mode 100644
index 000000000..69202ae2d
--- /dev/null
+++ b/plugins/ssr/ssrast.mli
@@ -0,0 +1,149 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* 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
+
+(* FIXME, make algebraic *)
+type ssrtermkind = char
+
+type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr
+
+type ssrview = ssrterm 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 *)
+(* TODO | 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 ssrterm list (* /view *)
+  | IPatClear of ssrclear (* {H1 H2} *)
+  | IPatSimpl of ssrsimpl
+  | IPatNewHidden of identifier list
+(* | IPatVarsForAbstract of Id.t list *)
+
+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
+  | Bdecl of name list * 'term
+  | Bdef of name * 'term option * 'term
+  | Bstruct of name
+  | 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 * ssrterm) * '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)
+
+(* OOP : these are general shortcuts *)
+type gist = Tacintern.glob_sign
+type ist = Tacinterp.interp_sign
+type goal = Proof_type.goal 
+type 'a sigma = 'a Evd.sigma
+type v82tac = Proof_type.tactic