(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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 Locus.or_var

(* clear switch {H G} *)
type ssrclear = ssrhyps

(* Discharge occ switch (combined occurrence / clear switch) *)
type ssrdocc = ssrclear option * ssrocc

(* OLD ssr terms *)
(* terms are pre constr, the kind is a parsing/printing flag to distinguish
 * between x, @x and (x). It affects automatic clear and let-in preservation. *)
(* FIXME *)
(* Cpattern is a temporary flag that becomes InParens ASAP. *)
type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind
type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr

(* NEW ssr term *)

type ast_glob_env = {
  ast_ltacvars : Id.Set.t;
  ast_extra : Genintern.Store.t;
  ast_intern_sign : Genintern.intern_variable_status;
}

(* 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 : ast_glob_env 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

type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int

(* Only [One] forces an introduction, possibly reducing the goal. *)
type anon_kind =
  | One of string option (* name hint *)
  | Drop
  | All
  | Temporary

type ssripat =
  | IPatNoop
  | IPatId of Id.t
  | IPatAnon of anon_kind (* inaccessible name *)
  | IPatDispatch of ssripatss_or_block (* (..|..) *)
  | IPatCase of ssripatss_or_block (* [..|..] *)
  | 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
  | IPatFastNondep

and ssripats = ssripat list
and ssripatss = ssripats list
and ssripatss_or_block =
  | Block of id_block
  | Regular of ssripats list
type ssrhpats = ((ssrclear option * 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 'tac ffwbinders =
  (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 = Evar.t
