(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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. *)

{

let defaultCast = Constr.DEFAULTcast
open Names
open Pp
open Pcoq
open Ltac_plugin
open Stdarg
open Tacarg
open Libnames
open Util
open Locus
open Tacexpr
open Pltac
open Ppconstr

open Namegen
open Tactypes
open Constrexpr
open Constrexpr_ops

open Proofview.Notations

open Ssrmatching_plugin.Ssrmatching

open Ssrprinters
open Ssrcommon
open Ssrequality
open Ssripats
open Libobject

(** Ssreflect load check. *)

(* To allow ssrcoq to be fully compatible with the "plain" Coq, we only *)
(* turn on its incompatible features (the new rewrite syntax, and the   *)
(* reserved identifiers) when the theory library (ssreflect.v) has      *)
(* has actually been required, or is being defined. Because this check  *)
(* needs to be done often (for each identifier lookup), we implement    *)
(* some caching, repeating the test only when the environment changes.  *)
(*   We check for protect_term because it is the first constant loaded; *)
(* ssr_have would ultimately be a better choice.                        *)
let ssr_loaded = Summary.ref ~name:"SSR:loaded" false
let is_ssr_loaded () =
  !ssr_loaded ||
  (if CLexer.is_keyword (Pcoq.get_keyword_state()) "SsrSyntax_is_Imported" then ssr_loaded:=true;
   !ssr_loaded)
let () = Pptactic.ssr_loaded_hook is_ssr_loaded

}

DECLARE PLUGIN "coq-core.plugins.ssreflect"

{

let ssrtac_name name = {
  mltac_plugin = "coq-core.plugins.ssreflect";
  mltac_tactic = "ssr" ^ name;
}

let ssrtac_entry name = {
  mltac_name = ssrtac_name name;
  mltac_index = 0;
}

let cache_tactic_notation (key, body, parule) =
  Tacenv.register_alias key body;
  Pptactic.declare_notation_tactic_pprule key parule

type tactic_grammar_obj = KerName.t * Tacenv.alias_tactic * Pptactic.pp_tactic

let inSsrGrammar : tactic_grammar_obj -> obj =
  declare_object {(default_object "SsrGrammar") with
                  load_function = (fun _ -> cache_tactic_notation);
                  cache_function = cache_tactic_notation;
                  classify_function = (fun x -> Keep)}

let path = MPfile (DirPath.make @@ List.map Id.of_string ["ssreflect"; "ssr"; "Coq"])

let register_ssrtac name f prods =
  let open Pptactic in
  Tacenv.register_ml_tactic (ssrtac_name name) [|f|];
  let map id = Reference (Locus.ArgVar (CAst.make id)) in
  let get_id = function
    | TacTerm s -> None
    | TacNonTerm (_, (_, ido)) -> ido in
  let ids = List.map_filter get_id prods in
  let tac = CAst.make (TacML (ssrtac_entry name, List.map map ids)) in
  let key = KerName.make path (Label.make ("ssrparser_" ^ name)) in
  let body = Tacenv.{ alias_args = ids; alias_body = tac; alias_deprecation = None } in
  let parule = {
    pptac_level = 0;
    pptac_prods = prods
  } in
  let obj () =
    Lib.add_leaf (inSsrGrammar (key, body, parule)) in
  Mltop.declare_cache_obj obj "coq-core.plugins.ssreflect";
  key

let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v

}

{

(* Defining grammar rules with "xx" in it automatically declares keywords too,
 * we thus save the lexer to restore it at the end of the file *)
let frozen_lexer = ref (Pcoq.get_keyword_state ()) ;;
let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () ->
    frozen_lexer := Pcoq.get_keyword_state ())

let tacltop = (LevelLe 5)

let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop

}

ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
  GLOBAL: ssrtacarg;
  ssrtacarg: TOP [[ tac = ltac_expr LEVEL "5" -> { tac } ]];
END

(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
END
GRAMMAR EXTEND Gram
  GLOBAL: ssrtac3arg;
  ssrtac3arg: TOP [[ tac = ltac_expr LEVEL "3" -> { tac } ]];
END

{

(* Lexically closed tactic for tacticals. *)
let pr_ssrtclarg env sigma _ _ prt tac = prt env sigma tacltop tac

}

ARGUMENT EXTEND ssrtclarg TYPED AS ssrtacarg
    PRINTED BY { pr_ssrtclarg env sigma }
| [ ssrtacarg(tac) ] -> { tac }
END

{

open Genarg

(** Adding a new uninterpreted generic argument type *)
let add_genarg tag pr =
  let wit = Genarg.make0 tag in
  let tag = Geninterp.Val.create tag in
  let glob ist x = (ist, x) in
  let subst _ x = x in
  let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in
  let gen_pr env sigma _ _ _ = pr env sigma in
  let () = Genintern.register_intern0 wit glob in
  let () = Gensubst.register_subst0 wit subst in
  let () = Geninterp.register_interp0 wit interp in
  let () = Geninterp.register_val0 wit (Some (Geninterp.Val.Base tag)) in
  Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr;
  wit

open Ssrast
let pr_id = Ppconstr.pr_id
let pr_name = function Name id -> pr_id id | Anonymous -> str "_"
let pr_spc () = str " "
let pr_list = prlist_with_sep

(**************************** ssrhyp **************************************)

let pr_ssrhyp _ _ _ = pr_hyp

let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp)

let intern_hyp ist (SsrHyp (loc, id) as hyp) =
  let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_hyp) CAst.(make ?loc id)) in
  if not_section_id id then hyp else
  hyp_err ?loc "Can't clear section hypothesis " id

open Pcoq.Prim

}

ARGUMENT EXTEND ssrhyp TYPED AS ssrhyprep PRINTED BY { pr_ssrhyp }
                       INTERPRETED BY { interp_hyp }
                       GLOBALIZED BY { intern_hyp }
  | [ ident(id) ] -> { SsrHyp (Loc.tag ~loc id) }
END

{

let pr_hoi = hoik pr_hyp
let pr_ssrhoi _ _ _ = pr_hoi

let wit_ssrhoirep = add_genarg "ssrhoirep" (fun env sigma -> pr_hoi)

let intern_ssrhoi ist = function
  | Hyp h -> Hyp (intern_hyp ist h)
  | Id (SsrHyp (_, id)) as hyp ->
    let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_ident) id) in
    hyp

let interp_ssrhoi ist env sigma = function
  | Hyp h -> let h' = interp_hyp ist env sigma h in Hyp h'
  | Id (SsrHyp (loc, id)) ->
    let id' = Tacinterp.interp_ident ist env sigma id in
    Id (SsrHyp (loc, id'))

}

ARGUMENT EXTEND ssrhoi_hyp TYPED AS ssrhoirep PRINTED BY { pr_ssrhoi }
                       INTERPRETED BY { interp_ssrhoi }
                       GLOBALIZED BY { intern_ssrhoi }
  | [ ident(id) ] -> { Hyp (SsrHyp(Loc.tag ~loc id)) }
END
ARGUMENT EXTEND ssrhoi_id TYPED AS ssrhoirep PRINTED BY { pr_ssrhoi }
                       INTERPRETED BY { interp_ssrhoi }
                       GLOBALIZED BY { intern_ssrhoi }
  | [ ident(id) ] -> { Id (SsrHyp(Loc.tag ~loc id)) }
END

(** Rewriting direction *)

{

let wit_ssrdir = add_genarg "ssrdir" (fun env sigma -> pr_dir)

(** Simpl switch *)

let pr_ssrsimpl _ _ _ = pr_simpl

let wit_ssrsimplrep = add_genarg "ssrsimplrep" (fun env sigma -> pr_simpl)

let test_ssrslashnum b1 b2 kwstate strm =
  match LStream.peek_nth kwstate 0 strm with
  | Tok.KEYWORD "/" ->
      (match LStream.peek_nth kwstate 1 strm with
      | Tok.NUMBER _ when b1 ->
         (match LStream.peek_nth kwstate 2 strm with
         | Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
         | Tok.KEYWORD "/" ->
             if not b2 then () else begin
               match LStream.peek_nth kwstate 3 strm with
               | Tok.NUMBER _ -> ()
               | _ -> raise Stream.Failure
             end
         | _ -> raise Stream.Failure)
      | Tok.KEYWORD "/" when not b1 ->
         (match LStream.peek_nth kwstate 2 strm with
         | Tok.KEYWORD "=" when not b2 -> ()
         | Tok.NUMBER _ when b2 ->
           (match LStream.peek_nth kwstate 3 strm with
           | Tok.KEYWORD "=" -> ()
           | _ -> raise Stream.Failure)
         | _ when not b2 -> ()
         | _ -> raise Stream.Failure)
      | Tok.KEYWORD "=" when not b1 && not b2 -> ()
      | _ -> raise Stream.Failure)
  | Tok.KEYWORD "//" when not b1 ->
         (match LStream.peek_nth kwstate 1 strm with
         | Tok.KEYWORD "=" when not b2 -> ()
         | Tok.NUMBER _ when b2 ->
           (match LStream.peek_nth kwstate 2 strm with
           | Tok.KEYWORD "=" -> ()
           | _ -> raise Stream.Failure)
         | _ when not b2 -> ()
         | _ -> raise Stream.Failure)
  | _ -> raise Stream.Failure

let test_ssrslashnum10 = test_ssrslashnum true false
let test_ssrslashnum11 = test_ssrslashnum true true
let test_ssrslashnum01 = test_ssrslashnum false true
let test_ssrslashnum00 = test_ssrslashnum false false

let negate_parser f x y =
  let rc = try Some (f x y) with Stream.Failure -> None in
  match rc with
  | None -> ()
  | Some _ -> raise Stream.Failure

let test_not_ssrslashnum =
  Pcoq.Entry.(of_parser
    "test_not_ssrslashnum" { parser_fun = negate_parser test_ssrslashnum10 })
let test_ssrslashnum00 =
  Pcoq.Entry.(of_parser "test_ssrslashnum01" { parser_fun = test_ssrslashnum00 })
let test_ssrslashnum10 =
  Pcoq.Entry.(of_parser "test_ssrslashnum10" { parser_fun = test_ssrslashnum10 })
let test_ssrslashnum11 =
  Pcoq.Entry.(of_parser "test_ssrslashnum11" { parser_fun = test_ssrslashnum11 })
let test_ssrslashnum01 =
  Pcoq.Entry.(of_parser "test_ssrslashnum01" { parser_fun = test_ssrslashnum01 })

}

ARGUMENT EXTEND ssrsimpl_ne TYPED AS ssrsimplrep PRINTED BY { pr_ssrsimpl }
| [ "//=" ] -> { SimplCut (~-1,~-1) }
| [ "/=" ] -> { Simpl ~-1 }
END

(* Pcoq.Prim. *)
GRAMMAR EXTEND Gram
  GLOBAL: ssrsimpl_ne;
  ssrsimpl_ne: TOP [
    [ test_ssrslashnum11; "/"; n = natural; "/"; m = natural; "=" -> { SimplCut(n,m) }
    | test_ssrslashnum10; "/"; n = natural; "/" -> { Cut n }
    | test_ssrslashnum10; "/"; n = natural; "=" -> { Simpl n }
    | test_ssrslashnum10; "/"; n = natural; "/=" -> { SimplCut (n,~-1) }
    | test_ssrslashnum10; "/"; n = natural; "/"; "=" -> { SimplCut (n,~-1) }
    | test_ssrslashnum01; "//"; m = natural; "=" -> { SimplCut (~-1,m) }
    | test_ssrslashnum00; "//" -> { Cut ~-1 }
    ]];

END

{

let pr_ssrclear _ _ _ = pr_clear mt

}

ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyp list PRINTED BY { pr_ssrclear }
| [ "{" ne_ssrhyp_list(clr) "}" ] -> { check_hyps_uniq [] clr; clr }
END

ARGUMENT EXTEND ssrclear TYPED AS ssrclear_ne PRINTED BY { pr_ssrclear }
| [ ssrclear_ne(clr) ] -> { clr }
| [ ] -> { [] }
END

(** Indexes *)

(* Since SSR indexes are always positive numbers, we use the 0 value *)
(* to encode an omitted index. We reuse the in or_var type, but we   *)
(* supply our own interpretation function, which checks for non      *)
(* positive values, and allows the use of constr numerals, so that   *)
(* e.g., "let n := eval compute in (1 + 3) in (do n!clear)" works.   *)

{

let pr_index = function
  | ArgVar {CAst.v=id} -> pr_id id
  | ArgArg n when n > 0 -> int n
  | _ -> mt ()
let pr_ssrindex _ _ _ = pr_index

let noindex = ArgArg 0

let check_index ?loc i =
  if i > 0 then i else CErrors.user_err ?loc (str"Index not positive")
let mk_index ?loc = function
  | ArgArg i -> ArgArg (check_index ?loc i)
  | iv -> iv

let interp_index ist env sigma idx =
  match idx with
  | ArgArg _ -> idx
  | ArgVar id ->
    let i =
      try
        let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
        begin match Tacinterp.Value.to_int v with
        | Some i -> i
        | None ->
        begin match Tacinterp.Value.to_constr v with
        | Some c ->
          let rc = Detyping.detype Detyping.Now Id.Set.empty env sigma c in
          begin match Notation.uninterp_prim_token rc ([], []) with
          | Constrexpr.Number n, _ when NumTok.Signed.is_int n ->
            int_of_string (NumTok.Signed.to_string n)
          | _ -> raise Not_found
          end
        | None -> raise Not_found
        end end
    with e when CErrors.noncritical e -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
    ArgArg (check_index ?loc:id.CAst.loc i)

open Pltac

}

ARGUMENT EXTEND ssrindex PRINTED BY { pr_ssrindex }
  INTERPRETED BY { interp_index }
END


(** Occurrence switch *)

(* The standard syntax of complemented occurrence lists involves a single *)
(* initial "-", e.g., {-1 3 5}. An initial                                *)
(* "+" may be used to indicate positive occurrences (the default). The    *)
(* "+" is optional, except if the list of occurrences starts with a       *)
(* variable or is empty (to avoid confusion with a clear switch). The     *)
(* empty positive switch "{+}" selects no occurrences, while the empty    *)
(* negative switch "{-}" selects all occurrences explicitly; this is the  *)
(* default, but "{-}" prevents the implicit clear, and can be used to     *)
(* force dependent elimination -- see ndefectelimtac below.               *)

{

let pr_ssrocc _ _ _ = pr_occ

open Pcoq.Prim

}

ARGUMENT EXTEND ssrocc TYPED AS (bool * int list) option PRINTED BY { pr_ssrocc }
| [ natural(n) natural_list(occ) ] -> {
     Some (false, List.map (check_index ~loc) (n::occ)) }
| [ "-" natural_list(occ) ]     -> { Some (true, occ) }
| [ "+" natural_list(occ) ]     -> { Some (false, occ) }
END


(* modality *)

{

let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt ()

let wit_ssrmmod = add_genarg "ssrmmod" (fun env sigma -> pr_mmod)
let ssrmmod = Pcoq.create_generic_entry2 "ssrmmod" (Genarg.rawwit wit_ssrmmod);;

}

GRAMMAR EXTEND Gram
  GLOBAL: ssrmmod;
  ssrmmod: [[ "!" -> { Must } | LEFTQMARK -> { May } | "?" -> { May } ]];
END

(** Rewrite multiplier: !n ?n *)

{

let pr_mult (n, m) =
  if n > 0 && m <> Once then int n ++ pr_mmod m else pr_mmod m

let pr_ssrmult _ _ _ = pr_mult

}

ARGUMENT EXTEND ssrmult_ne TYPED AS (int * ssrmmod) PRINTED BY { pr_ssrmult }
  | [ natural(n) ssrmmod(m) ] -> { check_index ~loc n, m }
  | [ ssrmmod(m) ]            -> { notimes, m }
END

ARGUMENT EXTEND ssrmult TYPED AS ssrmult_ne PRINTED BY { pr_ssrmult }
  | [ ssrmult_ne(m) ] -> { m }
  | [ ] -> { nomult }
END

{

(** Discharge occ switch (combined occurrence / clear switch *)

let pr_docc = function
  | None, occ -> pr_occ occ
  | Some clr, _ -> pr_clear mt clr

let pr_ssrdocc _ _ _ = pr_docc

}

ARGUMENT EXTEND ssrdocc TYPED AS (ssrclear option * ssrocc) PRINTED BY { pr_ssrdocc }
| [ "{" ssrocc(occ) "}" ] -> { mkocc occ }
| [ "{" ssrhyp_list(clr) "}" ] -> { mkclr clr }
END

{

(* Old kinds of terms *)

let input_ssrtermkind kwstate strm = match LStream.peek_nth kwstate 0 strm with
  | Tok.KEYWORD "(" -> InParens
  | Tok.KEYWORD "@" -> WithAt
  | _ -> NoFlag

let ssrtermkind = Pcoq.Entry.(of_parser "ssrtermkind" { parser_fun = input_ssrtermkind })

(* New kinds of terms *)

let input_term_annotation kwstate strm =
  match LStream.npeek kwstate 2 strm with
  | Tok.KEYWORD "(" :: Tok.KEYWORD "(" :: _ -> `DoubleParens
  | Tok.KEYWORD "(" :: _ -> `Parens
  | Tok.KEYWORD "@" :: _ -> `At
  | _ -> `None
let term_annotation =
  Pcoq.Entry.(of_parser "term_annotation" { parser_fun = input_term_annotation })

(* terms *)

(** Terms parsing. ********************************************************)

(* Because we allow wildcards in term references, we need to stage the *)
(* interpretation of terms so that it occurs at the right time during  *)
(* the execution of the tactic (e.g., so that we don't report an error *)
(* for a term that isn't actually used in the execution).              *)
(*   The term representation tracks whether the concrete initial term  *)
(* started with an opening paren, which might avoid a conflict between *)
(* the ssrreflect term syntax and Gallina notation.                    *)

(* Old terms *)
let pr_ssrterm _ _ _ = pr_term
let glob_ssrterm gs = function
  | k, (_, Some c) -> k, Tacintern.intern_constr gs c
  | ct -> ct
let subst_ssrterm s (k, c) = k, Tacsubst.subst_glob_constr_and_expr s c
let interp_ssrterm _ _ _ t = t

open Pcoq.Constr

}

ARGUMENT EXTEND ssrterm
     PRINTED BY { pr_ssrterm }
     INTERPRETED BY { interp_ssrterm }
     GLOBALIZED BY { glob_ssrterm } SUBSTITUTED BY { subst_ssrterm }
     RAW_PRINTED BY { pr_ssrterm }
     GLOB_PRINTED BY { pr_ssrterm }
END

GRAMMAR EXTEND Gram
  GLOBAL: ssrterm;
  ssrterm: TOP [[ k = ssrtermkind; c = Pcoq.Constr.constr -> { mk_term k c } ]];
END

(* New terms *)

{

let pp_ast_closure_term _ _ _ = pr_ast_closure_term

}

ARGUMENT EXTEND ast_closure_term
     PRINTED BY { pp_ast_closure_term }
     INTERPRETED BY { interp_ast_closure_term }
     GLOBALIZED BY { glob_ast_closure_term }
     SUBSTITUTED BY { subst_ast_closure_term }
     RAW_PRINTED BY { pp_ast_closure_term }
     GLOB_PRINTED BY { pp_ast_closure_term }
  | [ term_annotation(a) constr(c) ] -> { mk_ast_closure_term a c }
END
ARGUMENT EXTEND ast_closure_lterm
     PRINTED BY { pp_ast_closure_term }
     INTERPRETED BY { interp_ast_closure_term }
     GLOBALIZED BY { glob_ast_closure_term }
     SUBSTITUTED BY { subst_ast_closure_term }
     RAW_PRINTED BY { pp_ast_closure_term }
     GLOB_PRINTED BY { pp_ast_closure_term }
  | [ term_annotation(a) lconstr(c) ] -> { mk_ast_closure_term a c }
END

(* Old Views *)

{

let pr_view = pr_list mt (fun c -> str "/" ++ pr_term c)

let pr_ssrbwdview _ _ _ = pr_view

}

ARGUMENT EXTEND ssrbwdview TYPED AS ssrterm list
   PRINTED BY { pr_ssrbwdview }
END

(* Pcoq *)
GRAMMAR EXTEND Gram
  GLOBAL: ssrbwdview;
  ssrbwdview: TOP [
    [  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> { [mk_term NoFlag c] }
    |  test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrbwdview -> {
                    (mk_term NoFlag c) :: w } ]];
END

(* New Views *)

{

type ssrfwdview = ast_closure_term list

let pr_ssrfwdview _ _ _ = pr_view2

}

ARGUMENT EXTEND ssrfwdview TYPED AS ast_closure_term list
   PRINTED BY { pr_ssrfwdview }
END

(* Pcoq *)
GRAMMAR EXTEND Gram
  GLOBAL: ssrfwdview;
  ssrfwdview: TOP [
    [  test_not_ssrslashnum; "/"; c = ast_closure_term -> { [c] }
    |  test_not_ssrslashnum; "/"; c = ast_closure_term; w = ssrfwdview -> { c :: w } ]];
END

(* ipats *)

{

let remove_loc x = x.CAst.v

let ipat_of_intro_pattern p = Tactypes.(
  let rec ipat_of_intro_pattern = function
    | IntroNaming (IntroIdentifier id) -> IPatId id
    | IntroAction IntroWildcard -> IPatAnon Drop
    | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
      IPatCase (Regular(
       List.map (List.map ipat_of_intro_pattern)
         (List.map (List.map remove_loc) iorpat)))
    | IntroAction (IntroOrAndPattern (IntroAndPattern iandpat)) ->
      IPatCase
       (Regular [List.map ipat_of_intro_pattern (List.map remove_loc iandpat)])
    | IntroNaming IntroAnonymous -> IPatAnon (One None)
    | IntroAction (IntroRewrite b) -> IPatRewrite (allocc, if b then L2R else R2L)
    | IntroNaming (IntroFresh id) -> IPatAnon (One None)
    | IntroAction (IntroApplyOn _) -> (* to do *) CErrors.user_err (Pp.str "TO DO")
    | IntroAction (IntroInjection ips) ->
        IPatInj [List.map ipat_of_intro_pattern (List.map remove_loc ips)]
    | IntroForthcoming _ ->
        (* Unable to determine which kind of ipat interp_introid could
         * return [HH] *)
        assert false
  in
  ipat_of_intro_pattern p
)

let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
  | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x
  | IPatId id -> IPatId (map_id id)
  | IPatAbstractVars l -> IPatAbstractVars (List.map map_id l)
  | IPatClear clr -> IPatClear (List.map map_ssrhyp clr)
  | IPatCase (Regular iorpat) -> IPatCase (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat))
  | IPatCase (Block(hat)) -> IPatCase (Block(map_block map_id hat))
  | IPatDispatch (Regular iorpat) -> IPatDispatch (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat))
  | IPatDispatch (Block (hat)) -> IPatDispatch (Block(map_block map_id hat))
  | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)
  | IPatView v -> IPatView (List.map map_ast_closure_term v)
and map_block map_id = function
  | Prefix id -> Prefix (map_id id)
  | SuffixId id -> SuffixId (map_id id)
  | SuffixNum _ as x -> x

type ssripatrep = ssripat
let wit_ssripatrep = add_genarg "ssripatrep" (fun env sigma -> pr_ipat)

let pr_ssripat _ _ _ = pr_ipat
let pr_ssripats _ _ _ = pr_ipats
let pr_ssriorpat _ _ _ = pr_iorpat

let intern_ipat ist =
  map_ipat
    (fun id -> id)
    (intern_hyp ist)
    (glob_ast_closure_term ist)

let intern_ipats ist = List.map (intern_ipat ist)

let interp_intro_pattern = Tacinterp.interp_intro_pattern

let interp_introid ist env sigma id =
 try IntroNaming (IntroIdentifier (hyp_id (interp_hyp ist env sigma (SsrHyp (Loc.tag id)))))
 with e when CErrors.noncritical e ->
   (interp_intro_pattern ist env sigma (CAst.make @@ IntroNaming (IntroIdentifier id))).CAst.v

let get_intro_id = function
  | IntroNaming (IntroIdentifier id) -> id
  | _ -> assert false

let rec add_intro_pattern_hyps ipat hyps =
  let {CAst.loc; v=ipat} = ipat in
  match ipat with
  | IntroNaming (IntroIdentifier id) ->
    if not_section_id id then SsrHyp (loc, id) :: hyps else
    hyp_err ?loc "Can't delete section hypothesis " id
  | IntroAction IntroWildcard -> hyps
  | IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
     List.fold_right (List.fold_right add_intro_pattern_hyps) iorpat hyps
  | IntroAction (IntroOrAndPattern (IntroAndPattern iandpat)) ->
    List.fold_right add_intro_pattern_hyps iandpat hyps
  | IntroNaming IntroAnonymous -> []
  | IntroNaming (IntroFresh _) -> []
  | IntroAction (IntroRewrite _) -> hyps
  | IntroAction (IntroInjection ips) -> List.fold_right add_intro_pattern_hyps ips hyps
  | IntroAction (IntroApplyOn (c,pat)) -> add_intro_pattern_hyps pat hyps
  | IntroForthcoming _ ->
    (* As in ipat_of_intro_pattern, was unable to determine which kind
      of ipat interp_introid could return [HH] *) assert false

(* We interp the ipat using the standard ltac machinery for ids, since
 * we have no clue what a name could be bound to (maybe another ipat) *)
let interp_ipat ist env sigma =
  let ltacvar id = Id.Map.mem id ist.Tacinterp.lfun in
  let interp_block = function
    | Prefix id when ltacvar id ->
        begin match interp_introid ist env sigma id with
        | IntroNaming (IntroIdentifier id) -> Prefix id
        | _ -> Ssrcommon.errorstrm Pp.(str"Variable " ++ Id.print id ++ str" in block intro pattern should be bound to an identifier.")
        end
    | SuffixId id when ltacvar id ->
        begin match interp_introid ist env sigma id with
        | IntroNaming (IntroIdentifier id) -> SuffixId id
        | _ -> Ssrcommon.errorstrm Pp.(str"Variable " ++ Id.print id ++ str" in block intro pattern should be bound to an identifier.")
        end
    | x -> x in
  let rec interp = function
  | IPatId id when ltacvar id ->
    ipat_of_intro_pattern (interp_introid ist env sigma id)
  | IPatId _ as x -> x
  | IPatClear clr ->
    let add_hyps (SsrHyp (loc, id) as hyp) hyps =
      if not (ltacvar id) then hyp :: hyps else
      add_intro_pattern_hyps CAst.(make ?loc (interp_introid ist env sigma id)) hyps in
    let clr' = List.fold_right add_hyps clr [] in
    check_hyps_uniq [] clr';
    IPatClear clr'
  | IPatCase(Regular iorpat) ->
      IPatCase(Regular(List.map (List.map interp) iorpat))
  | IPatCase(Block(hat)) -> IPatCase(Block(interp_block hat))

  | IPatDispatch(Regular iorpat) ->
      IPatDispatch(Regular (List.map (List.map interp) iorpat))
  | IPatDispatch(Block(hat)) -> IPatDispatch(Block(interp_block hat))

  | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat)
  | IPatAbstractVars l ->
     IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist env sigma) l))
  | IPatView l -> IPatView (List.map (fun x -> interp_ast_closure_term ist
     env sigma x) l)
  | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x
    in
  interp

let interp_ipats ist env sigma l = List.map (interp_ipat ist env sigma) l

let pushIPatRewrite = function
  | pats :: orpat -> (IPatRewrite (allocc, L2R) :: pats) :: orpat
  | [] -> []

let pushIPatNoop = function
  | pats :: orpat -> (IPatNoop :: pats) :: orpat
  | [] -> []

let test_ident_no_do =
  let open Pcoq.Lookahead in
  to_entry "test_ident_no_do" begin
    lk_ident_except ["do"]
  end

}

ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print }
END


GRAMMAR EXTEND Gram
  GLOBAL: ident_no_do;
  ident_no_do: TOP [ [ test_ident_no_do; id = IDENT -> { Id.of_string id } ] ];
END

ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats }
  INTERPRETED BY { interp_ipats }
  GLOBALIZED BY { intern_ipats }
  | [ "_" ] -> { [IPatAnon Drop] }
  | [ "*" ] -> { [IPatAnon All] }
  | [ ">" ] -> { [IPatFastNondep] }
  | [ ident_no_do(id) ] -> { [IPatId id] }
  | [ "?" ] -> { [IPatAnon (One None)] }
  | [ "+" ] -> { [IPatAnon Temporary] }
  | [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] }
  | [ ssrsimpl_ne(sim) ] -> { [IPatSimpl sim] }
  | [ ssrdocc(occ) "->" ] -> { match occ with
      | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
      | None, occ -> [IPatRewrite (occ, L2R)]
      | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, L2R)] }
  | [ ssrdocc(occ) "<-" ] -> { match occ with
      | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected")
      | None, occ ->  [IPatRewrite (occ, R2L)]
      | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)] }
  | [ ssrdocc(occ) ] -> { match occ with
      | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl]
      | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") }
  | [ "->" ] -> { [IPatRewrite (allocc, L2R)] }
  | [ "<-" ] -> { [IPatRewrite (allocc, R2L)] }
  | [ "-" ] -> { [IPatNoop] }
  | [ "-/" "=" ] -> { [IPatNoop;IPatSimpl(Simpl ~-1)] }
  | [ "-/=" ] -> { [IPatNoop;IPatSimpl(Simpl ~-1)] }
  | [ "-/" "/" ] -> { [IPatNoop;IPatSimpl(Cut ~-1)] }
  | [ "-//" ] -> { [IPatNoop;IPatSimpl(Cut ~-1)] }
  | [ "-/" integer(n) "/" ] -> { [IPatNoop;IPatSimpl(Cut n)] }
  | [ "-/" "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] }
  | [ "-//" "=" ] -> { [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] }
  | [ "-//=" ] -> { [IPatNoop;IPatSimpl(SimplCut (~-1,~-1))] }
  | [ "-/" integer(n) "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (n,~-1))] }
  | [ "-/" integer(n) "/" integer (m) "=" ] ->
      { [IPatNoop;IPatSimpl(SimplCut(n,m))] }
  | [ ssrfwdview(v) ] -> { [IPatView v] }
  | [ "[" ":" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] }
  | [ "[:" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] }
END

ARGUMENT EXTEND ssripats TYPED AS ssripat PRINTED BY { pr_ssripats }
  | [ ssripat(i) ssripats(tl) ] -> { i @ tl }
  | [ ] -> { [] }
END

ARGUMENT EXTEND ssriorpat TYPED AS ssripat list PRINTED BY { pr_ssriorpat }
| [ ssripats(pats) "|" ssriorpat(orpat) ] -> { pats :: orpat }
| [ ssripats(pats) "|-" ">" ssriorpat(orpat) ] -> { pats :: pushIPatRewrite orpat }
| [ ssripats(pats) "|-" ssriorpat(orpat) ] -> { pats :: pushIPatNoop orpat }
| [ ssripats(pats) "|->" ssriorpat(orpat) ] -> { pats :: pushIPatRewrite orpat }
| [ ssripats(pats) "||" ssriorpat(orpat) ] -> { pats :: [] :: orpat }
| [ ssripats(pats) "|||" ssriorpat(orpat) ] -> { pats :: [] :: [] :: orpat }
| [ ssripats(pats) "||||" ssriorpat(orpat) ] -> { [pats; []; []; []] @ orpat }
| [ ssripats(pats) ] -> { [pats] }
END

{

let test_leftsquarebracket_equal =
  let open Pcoq.Lookahead in
  to_entry "test_leftsquarebracket_equal" begin
    lk_kw "[" >> lk_kw "=" >> check_no_space
  end

let reject_ssrhid kwstate strm =
  match LStream.peek_nth kwstate 0 strm with
  | Tok.KEYWORD "[" ->
      (match LStream.peek_nth kwstate 1 strm with
      | Tok.KEYWORD ":" -> raise Stream.Failure
      | _ -> ())
  | _ -> ()

let test_nohidden = Pcoq.Entry.(of_parser "test_ssrhid" { parser_fun = reject_ssrhid })

let rec reject_binder crossed_paren k kwstate s =
  match
    try Some (LStream.peek_nth kwstate k s)
    with Stream.Failure -> None
  with
  | Some (Tok.KEYWORD "(") when not crossed_paren -> reject_binder true (k+1) kwstate s
  | Some (Tok.IDENT _) when crossed_paren -> reject_binder true (k+1) kwstate s
  | Some (Tok.KEYWORD ":" | Tok.KEYWORD ":=") when crossed_paren ->
      raise Stream.Failure
  | Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
  | _ -> if crossed_paren then () else raise Stream.Failure

let _test_nobinder = Pcoq.Entry.(of_parser "test_nobinder" { parser_fun = reject_binder false 0 })

}

ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY { pr_ssripat }
  INTERPRETED BY { interp_ipat }
  GLOBALIZED BY { intern_ipat }

END

(* Pcoq *)
GRAMMAR EXTEND Gram
  GLOBAL: ssrcpat;
  hat: [
  [ "^"; id = ident -> { Prefix id }
  | "^"; "~"; id = ident -> { SuffixId id }
  | "^"; "~"; n = natural -> { SuffixNum n }
  | "^~"; id = ident -> { SuffixId id }
  | "^~"; n = natural -> { SuffixNum n }
  ]];
  ssrcpat: TOP [
   [ test_leftsquarebracket_equal; test_nohidden; "["; "="; iorpat = ssriorpat; "]" -> {
      IPatInj iorpat }
   | test_nohidden; "["; hat_id = hat; "]" -> {
      IPatCase (Block(hat_id)) }
   | test_nohidden; "["; iorpat = ssriorpat; "]" -> {
      IPatCase (Regular iorpat) } ]];
END

GRAMMAR EXTEND Gram
  GLOBAL: ssripat;
  ssripat: TOP [[ pat = ssrcpat -> { [pat] } ]];
END

ARGUMENT EXTEND ssripats_ne TYPED AS ssripat PRINTED BY { pr_ssripats }
  | [ ssripat(i) ssripats(tl) ] -> { i @ tl }
                                     END

(* subsets of patterns *)

{

(* TODO: review what this function does, it looks suspicious *)
let check_ssrhpats loc w_binders ipats =
  let err_loc s = CErrors.user_err ~loc s in
  let clr, ipats =
    let opt_app = function None -> fun l -> Some l
      | Some l1 -> fun l2 -> Some (l1 @ l2) in
    let rec aux clr = function
      | IPatClear cl :: tl -> aux (opt_app clr cl) tl
      | tl -> clr, tl
    in aux None ipats in
  let simpl, ipats =
    match List.rev ipats with
    | IPatSimpl _ as s :: tl -> [s], List.rev tl
    | _ -> [],  ipats in
  if simpl <> [] && not w_binders then
    err_loc (str "No s-item allowed here: " ++ pr_ipats simpl);
  let ipat, binders =
    let rec loop ipat = function
      | [] -> ipat, []
      | ( IPatId _| IPatAnon _| IPatCase _ | IPatDispatch _ | IPatRewrite _ as i) :: tl ->
        if w_binders then
          if simpl <> [] && tl <> [] then
            err_loc(str"binders XOR s-item allowed here: "++pr_ipats(tl@simpl))
          else if not (List.for_all (function IPatId _ -> true | _ -> false) tl)
          then err_loc (str "Only binders allowed here: " ++ pr_ipats tl)
          else ipat @ [i], tl
        else
          if tl = [] then  ipat @ [i], []
          else err_loc (str "No binder or s-item allowed here: " ++ pr_ipats tl)
      | hd :: tl -> loop (ipat @ [hd]) tl
    in loop [] ipats in
  ((clr, ipat), binders), simpl

let pr_clear_opt sep = function None -> mt () | Some x -> pr_clear sep x

let pr_hpats (((clr, ipat), binders), simpl) =
   pr_clear_opt mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl
let pr_ssrhpats _ _ _ = pr_hpats
let pr_ssrhpats_wtransp _ _ _ (_, x) = pr_hpats x

}

ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear option * ssripat) * ssripat) * ssripat)
PRINTED BY { pr_ssrhpats }
  | [ ssripats(i) ] -> { check_ssrhpats loc true i }
END

ARGUMENT EXTEND ssrhpats_wtransp
  TYPED AS (bool * (((ssrclear option * ssripats) * ssripats) * ssripats))
  PRINTED BY { pr_ssrhpats_wtransp }
  | [ ssripats(i) ] -> { false,check_ssrhpats loc true i }
  | [ ssripats(i) "@" ssripats(j) ] -> { true,check_ssrhpats loc true (i @ j) }
END

ARGUMENT EXTEND ssrhpats_nobs
TYPED AS (((ssrclear option * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats }
  | [ ssripats(i) ] -> { check_ssrhpats loc false i }
END

ARGUMENT EXTEND ssrrpat TYPED AS ssripatrep PRINTED BY { pr_ssripat }
  | [ "->" ] -> { IPatRewrite (allocc, L2R) }
  | [ "<-" ] -> { IPatRewrite (allocc, R2L) }
END

{

let pr_intros sep intrs =
  if intrs = [] then mt() else sep () ++ str "=>" ++ sep () ++ pr_ipats intrs
let pr_ssrintros _ _ _ = pr_intros mt

}

ARGUMENT EXTEND ssrintros_ne TYPED AS ssripat
 PRINTED BY { pr_ssrintros }
  | [ "=>" ssripats_ne(pats) ] -> { pats }
(*  TODO | [ "=>" ">" ssripats_ne(pats) ] -> { IPatFastMode :: pats }
  | [ "=>>" ssripats_ne(pats) ] -> [ IPatFastMode :: pats ] *)
END

ARGUMENT EXTEND ssrintros TYPED AS ssrintros_ne PRINTED BY { pr_ssrintros }
  | [ ssrintros_ne(intrs) ] -> { intrs }
  | [ ] -> { [] }
END

{

let pr_ssrintrosarg env sigma _ _ prt (tac, ipats) =
  prt env sigma tacltop tac ++ pr_intros spc ipats

}

ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros)
   PRINTED BY { pr_ssrintrosarg env sigma }
END

{

(** Defined identifier *)
let pr_ssrfwdid id = pr_spc () ++ pr_id id

let pr_ssrfwdidx _ _ _ = pr_ssrfwdid

}

(* We use a primitive parser for the head identifier of forward *)
(* tactis to avoid syntactic conflicts with basic Coq tactics. *)
ARGUMENT EXTEND ssrfwdid TYPED AS ident PRINTED BY { pr_ssrfwdidx }
END

{

let test_ssrfwdid =
  let open Pcoq.Lookahead in
  to_entry "test_ssrfwdid" begin
    lk_ident >> (lk_ident <+> lk_kws [":"; ":="; "("])
  end

}

GRAMMAR EXTEND Gram
  GLOBAL: ssrfwdid;
  ssrfwdid: TOP [[ test_ssrfwdid; id = Prim.ident -> { id } ]];
  END


(* by *)
(** Tactical arguments. *)

(* We have four kinds: simple tactics, [|]-bracketed lists, hints, and swaps *)
(* The latter two are used in forward-chaining tactics (have, suffice, wlog) *)
(* and subgoal reordering tacticals (; first & ; last), respectively.        *)

{

let pr_ortacs env sigma prt =
  let rec pr_rec = function
  | [None]           -> spc() ++ str "|" ++ spc()
  | None :: tacs     -> spc() ++ str "|" ++ pr_rec tacs
  | Some tac :: tacs -> spc() ++ str "| " ++ prt env sigma tacltop tac ++  pr_rec tacs
  | []                -> mt() in
  function
  | [None]           -> spc()
  | None :: tacs     -> pr_rec tacs
  | Some tac :: tacs -> prt env sigma tacltop tac ++ pr_rec tacs
  | []                -> mt()
let pr_ssrortacs env sigma _ _ = pr_ortacs env sigma

}

ARGUMENT EXTEND ssrortacs TYPED AS tactic option list PRINTED BY { pr_ssrortacs env sigma }
| [ ssrtacarg(tac) "|" ssrortacs(tacs) ] -> { Some tac :: tacs }
| [ ssrtacarg(tac) "|" ] -> { [Some tac; None] }
| [ ssrtacarg(tac) ] -> { [Some tac] }
| [ "|" ssrortacs(tacs) ] -> { None :: tacs }
| [ "|" ] -> { [None; None] }
END

{

let pr_hintarg env sigma prt = function
  | true, tacs -> hv 0 (str "[ " ++ pr_ortacs env sigma prt tacs ++ str " ]")
  | false, [Some tac] -> prt env sigma tacltop tac
  | _, _ -> mt()

let pr_ssrhintarg env sigma _ _ = pr_hintarg env sigma

}

ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma }
| [ "[" "]" ] -> { nullhint }
| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
| [ ssrtacarg(arg) ] -> { mk_hint arg }
END

(* Copy of ssrhintarg with LEVEL "3", useful for: "under ... do ..." *)
ARGUMENT EXTEND ssrhint3arg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma }
| [ "[" "]" ] -> { nullhint }
| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
| [ ssrtac3arg(arg) ] -> { mk_hint arg }
END

ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma }
| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
END

{

let pr_hint env sigma prt arg =
  if arg = nohint then mt() else spc () ++ str "by" ++ spc () ++ pr_hintarg env sigma prt arg
let pr_ssrhint env sigma _ _ = pr_hint env sigma

}

ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY { pr_ssrhint env sigma }
| [ ]                       -> { nohint }
END
(** The "in" pseudo-tactical *)

(* We can't make "in" into a general tactical because this would create a  *)
(* crippling conflict with the ltac let .. in construct. Hence, we add     *)
(* explicitly an "in" suffix to all the extended tactics for which it is   *)
(* relevant (including move, case, elim) and to the extended do tactical   *)
(* below, which yields a general-purpose "in" of the form do [...] in ...  *)

(* This tactical needs to come before the intro tactics because the latter *)
(* must take precautions in order not to interfere with the discharged     *)
(* assumptions. This is especially difficult for discharged "let"s, which  *)
(* the default simpl and unfold tactics would erase blindly.               *)

{

open Ssrmatching_plugin.G_ssrmatching

let pr_wgen = function
  | (clr, Some((id,k),None)) -> spc() ++ pr_clear mt clr ++ str k ++ pr_hoi id
  | (clr, Some((id,k),Some p)) ->
      spc() ++ pr_clear mt clr ++ str"(" ++ str k ++ pr_hoi id ++ str ":=" ++
        pr_cpattern p ++ str ")"
  | (clr, None) -> spc () ++ pr_clear mt clr
let pr_ssrwgen _ _ _ = pr_wgen

}

(* no globwith for char *)
ARGUMENT EXTEND ssrwgen
  TYPED AS (ssrclear * ((ssrhoi_hyp * string) * cpattern option) option)
  PRINTED BY { pr_ssrwgen }
| [ ssrclear_ne(clr) ] -> { clr, None }
| [ ssrhoi_hyp(hyp) ] -> { [], Some((hyp, " "), None) }
| [ "@" ssrhoi_hyp(hyp) ] -> { [], Some((hyp, "@"), None) }
| [ "(" ssrhoi_id(id) ":=" lcpattern(p) ")" ] ->
  { [], Some ((id," "),Some p) }
| [ "(" ssrhoi_id(id) ")" ] -> { [], Some ((id,"("), None) }
| [ "(@" ssrhoi_id(id) ":=" lcpattern(p) ")" ] ->
  { [], Some ((id,"@"),Some p) }
| [ "(" "@" ssrhoi_id(id) ":=" lcpattern(p) ")" ] ->
  { [], Some ((id,"@"),Some p) }
END

{

let pr_clseq = function
  | InGoal | InHyps -> mt ()
  | InSeqGoal       -> str "|- *"
  | InHypsSeqGoal   -> str " |- *"
  | InHypsGoal      -> str " *"
  | InAll           -> str "*"
  | InHypsSeq       -> str " |-"
  | InAllHyps       -> str "* |-"

let wit_ssrclseq = add_genarg "ssrclseq" (fun env sigma -> pr_clseq)
let pr_clausehyps = pr_list pr_spc pr_wgen
let pr_ssrclausehyps _ _ _ = pr_clausehyps

}

ARGUMENT EXTEND ssrclausehyps
TYPED AS ssrwgen list PRINTED BY { pr_ssrclausehyps }
| [ ssrwgen(hyp) "," ssrclausehyps(hyps) ] -> { hyp :: hyps }
| [ ssrwgen(hyp) ssrclausehyps(hyps) ] -> { hyp :: hyps }
| [ ssrwgen(hyp) ] -> { [hyp] }
END

{

(* type ssrclauses = ssrahyps * ssrclseq *)

let pr_clauses (hyps, clseq) =
  if clseq = InGoal then mt ()
  else str "in " ++ pr_clausehyps hyps ++ pr_clseq clseq
let pr_ssrclauses _ _ _ = pr_clauses

}

ARGUMENT EXTEND ssrclauses TYPED AS (ssrwgen list * ssrclseq)
    PRINTED BY { pr_ssrclauses }
  | [ "in" ssrclausehyps(hyps) "|-" "*" ] -> { hyps, InHypsSeqGoal }
  | [ "in" ssrclausehyps(hyps) "|-" ]     -> { hyps, InHypsSeq }
  | [ "in" ssrclausehyps(hyps) "*" ]      -> { hyps, InHypsGoal }
  | [ "in" ssrclausehyps(hyps) ]          -> { hyps, InHyps }
  | [ "in" "|-" "*" ]                     -> { [], InSeqGoal }
  | [ "in" "*" ]                          -> { [], InAll }
  | [ "in" "*" "|-" ]                     -> { [], InAllHyps }
  | [ ]                                   -> { [], InGoal }
END


{

(** Definition value formatting *)

(* 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.                                                      *)

let pr_binder prl = function
  | Bvar x ->
    pr_name x
  | Bdecl (xs, t) ->
    str "(" ++ pr_list pr_spc pr_name xs ++ str " : " ++ prl t ++ str ")"
  | Bdef (x, None, v) ->
    str "(" ++ pr_name x ++ str " := " ++ prl v ++ str ")"
  | Bdef (x, Some t, v) ->
    str "(" ++ pr_name x ++ str " : " ++ prl t ++
                            str " := " ++ prl v ++ str ")"
  | Bstruct x ->
    str "{struct " ++ pr_name x ++ str "}"
  | Bcast t ->
    str ": " ++ prl t

let rec format_local_binders h0 bl0 = match h0, bl0 with
  | BFvar :: h, CLocalAssum ([{CAst.v=x}], _, _,  _) :: bl ->
    Bvar x :: format_local_binders h bl
  | BFdecl _ :: h, CLocalAssum (lxs, _, _, t) :: bl ->
    Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: format_local_binders h bl
  | BFdef :: h, CLocalDef ({CAst.v=x}, _, v, oty) :: bl ->
    Bdef (x, oty, v) :: format_local_binders h bl
  | _ -> []

let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
  | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _, _)], c) } ->
    let bs, c' = format_constr_expr h c in
    Bvar x :: bs, c'
  | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, _, t)], c) } ->
    let bs, c' = format_constr_expr h c in
    Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: bs, c'
  | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
    let bs, c' = format_constr_expr h c in
    Bdef (x, oty, v) :: bs, c'
  | [BFcast], { v = CCast (c, defaultCast, t) } ->
    [Bcast t], c
  | BFrec (has_str, has_cast) :: h,
    { v = CFix ( _, [_, _, Some {CAst.v = CStructRec locn}, bl, t, c]) } ->
    let bs = format_local_binders h bl in
    let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in
    bs @ bstr @ (if has_cast then [Bcast t] else []), c
  | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, _, bl, t, c]) } ->
    format_local_binders h bl @ (if has_cast then [Bcast t] else []), c
  | _, c ->
    [], c

(** 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.        *)

let pr_fwdkind = function
  | FwdHint (s,_) -> str (s ^ " ") | _ -> str " :=" ++ spc ()
let pr_fwdfmt (fk, _ : ssrfwdfmt) = pr_fwdkind fk

let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" (fun env sigma -> pr_fwdfmt)

(* type ssrfwd = ssrfwdfmt * ssrterm *)

let mkFwdVal fk c = ((fk, []), c)
let mkssrFwdVal fk c = ((fk, []), (c,None))

let same_ist { interp_env = x } { interp_env = y } =
  match x,y with
  | None, None -> true
  | Some a, Some b -> a == b
  | _ -> false

let mkFwdCast fk ?loc ?c t =
  let c = match c with
    | None -> mkCHole loc
    | Some c -> assert (same_ist t c); c.body in
  ((fk, [BFcast]),
   { t with annotation = `None;
            body = (CAst.make ?loc @@ CCast (c, Some defaultCast, t.body)) })

let mkssrFwdCast fk loc t c = ((fk, [BFcast]), (c, Some t))

let mkFwdHint s t =
  let loc =  Constrexpr_ops.constr_loc t.body in
  mkFwdCast (FwdHint (s,false)) ?loc t
let mkFwdHintNoTC s t =
  let loc =  Constrexpr_ops.constr_loc t.body in
  mkFwdCast (FwdHint (s,true)) ?loc t

let pr_gen_fwd prval prc prlc fk (bs, c) =
  let prc s = str s ++ spc () ++ prval prc prlc c in
  match fk, bs with
  | FwdHint (s,_), [Bcast t] -> str s ++ spc () ++ prlc t
  | FwdHint (s,_), _ ->  prc (s ^ "(* typeof *)")
  | FwdHave, [Bcast t] -> str ":" ++ spc () ++ prlc t ++ prc " :="
  | _, [] -> prc " :="
  | _, _ -> spc () ++ pr_list spc (pr_binder prlc) bs ++ prc " :="

let pr_fwd_guarded prval prval' = function
| (fk, h), c ->
  pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c.body)

let pr_unguarded prc prlc = prlc

let pr_fwd = pr_fwd_guarded pr_unguarded pr_unguarded
let pr_ssrfwd _ _ _ = pr_fwd

}

ARGUMENT EXTEND ssrfwd TYPED AS (ssrfwdfmt * ast_closure_lterm) PRINTED BY { pr_ssrfwd }
  | [ ":=" ast_closure_lterm(c) ] -> { mkFwdVal FwdPose c }
  | [ ":" ast_closure_lterm (t) ":=" ast_closure_lterm(c) ] -> { mkFwdCast FwdPose ~loc t ~c }
END

(** Independent parsing for binders *)

(* The pose, pose fix, and pose cofix tactics use these internally to  *)
(* parse argument fragments.                                           *)

{

let pr_ssrbvar env sigma prc _ _ v = prc env sigma v

}

ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY { pr_ssrbvar env sigma }
| [ ident(id) ] -> { mkCVar ~loc id }
| [ "_" ] -> { mkCHole (Some loc) }
END

{

let bvar_lname = let open CAst in function
  | { v = CRef (qid, _) } when qualid_is_ident qid ->
    CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid)
  | { loc = loc } -> CAst.make ?loc Anonymous

let pr_ssrbinder env sigma prc _ _ (_, c) = prc env sigma c

}

ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinder env sigma }
 | [ ssrbvar(bv) ] ->
   { let { CAst.loc=xloc } as x = bvar_lname bv in
     (FwdPose, [BFvar]),
     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],None,Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
 | [ "(" ssrbvar(bv) ")" ] ->
   { let { CAst.loc=xloc } as x = bvar_lname bv in
     (FwdPose, [BFvar]),
     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],None,Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) }
 | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
   { let x = bvar_lname bv in
     (FwdPose, [BFdecl 1]),
     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], None, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
 | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] ->
   { let xs = List.map bvar_lname (bv :: bvs) in
     let n = List.length xs in
     (FwdPose, [BFdecl n]),
     CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, None, Default Glob_term.Explicit, t)], mkCHole (Some loc)) }
 | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
   { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) }
 | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
   { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, None, mkCHole (Some loc)) }
     END

GRAMMAR EXTEND Gram
  GLOBAL: ssrbinder;
  ssrbinder: TOP [
  [  ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> {
     (FwdPose, [BFvar]),
     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],None,Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ]
  ];
END

{

let rec binders_fmts = function
  | ((_, h), _) :: bs -> h @ binders_fmts bs
  | _ -> []

let push_binders c2 bs =
  let loc2 = constr_loc c2 in let mkloc loc1 = Loc.merge_opt loc1 loc2 in
  let open CAst in
  let rec loop ty c = function
  | (_, { loc = loc1; v = CLambdaN (b, _) } ) :: bs when ty ->
      CAst.make ?loc:(mkloc loc1) @@ CProdN (b, loop ty c bs)
  | (_, { loc = loc1; v = CLambdaN (b, _) } ) :: bs ->
      CAst.make ?loc:(mkloc loc1) @@ CLambdaN (b, loop ty c bs)
  | (_, { loc = loc1; v = CLetIn (x, v, oty, _) } ) :: bs ->
      CAst.make ?loc:(mkloc loc1) @@ CLetIn (x, v, oty, loop ty c bs)
  | [] -> c
  | _ -> anomaly "binder not a lambda nor a let in" in
  match c2 with
  | { loc; v = CCast (ct, defaultCast, cty) } ->
      CAst.make ?loc @@ (CCast (loop false ct bs, defaultCast, (loop true cty bs)))
  | ct -> loop false ct bs

let rec fix_binders = let open CAst in function
  | (_, { v = CLambdaN ([CLocalAssum(xs, _, _, t)], _) } ) :: bs ->
      CLocalAssum (xs, None, Default Glob_term.Explicit, t) :: fix_binders bs
  | (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
    CLocalDef (x, None, v, oty) :: fix_binders bs
  | _ -> []

let pr_ssrstruct _ _ _ = function
  | Some id -> str "{struct " ++ pr_id id ++ str "}"
  | None -> mt ()

}

ARGUMENT EXTEND ssrstruct TYPED AS ident option PRINTED BY { pr_ssrstruct }
| [ "{" "struct" ident(id) "}" ] -> { Some id }
| [ ] -> { None }
END

(** The "pose" tactic *)

(* The plain pose form. *)

{

let bind_fwd bs ((fk, h), c) =
 (fk,binders_fmts bs @ h), { c with body = push_binders c.body bs }

}

ARGUMENT EXTEND ssrposefwd TYPED AS ssrfwd PRINTED BY { pr_ssrfwd }
  | [ ssrbinder_list(bs) ssrfwd(fwd) ] -> { bind_fwd bs fwd }
END

(* The pose fix form. *)

{

let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd

let bvar_locid = function
  | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
    CAst.make ?loc:qid.CAst.loc (qualid_basename qid)
  | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"")

}

ARGUMENT EXTEND ssrfixfwd TYPED AS (ident * ssrfwd) PRINTED BY { pr_ssrfixfwd }
  | [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] ->
    { let { CAst.v=id } as lid = bvar_locid bv in
      let (fk, h), ac = fwd in
      let c = ac.body in
      let has_cast, t', c' = match format_constr_expr h c with
      | [Bcast t'], c' -> true, t', c'
      | _ -> false, mkCHole (constr_loc c), c in
      let lb = fix_binders bs in
      let has_struct, i =
        let rec loop = function
          | {CAst.loc=l'; v=Name id'} :: _ when Option.equal Id.equal sid (Some id') ->
            true, CAst.make ?loc:l' id'
          | [{CAst.loc=l';v=Name id'}] when sid = None ->
            false, CAst.make ?loc:l' id'
          | _ :: bn -> loop bn
          | [] -> CErrors.user_err (Pp.str "Bad structural argument") in
        loop (names_of_local_assums lb) in
      let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in
      let fix = CAst.make ~loc @@ CFix (lid, [lid, None, (Some (CAst.make (CStructRec i))), lb, t', c']) in
      id, ((fk, h'),  { ac with body = fix }) }
END


(* The pose cofix form. *)

{

let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd

}

ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY { pr_ssrcofixfwd }
  | [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] ->
    { let { CAst.v=id } as lid = bvar_locid bv in
      let (fk, h), ac = fwd in
      let c = ac.body in
      let has_cast, t', c' = match format_constr_expr h c with
      | [Bcast t'], c' -> true, t', c'
      | _ -> false, mkCHole (constr_loc c), c in
      let h' = BFrec (false, has_cast) :: binders_fmts bs in
      let cofix = CAst.make ~loc @@ CCoFix (lid, [lid, None, fix_binders bs, t', c']) in
      id, ((fk, h'), { ac with body = cofix })
    }
END

{

let pr_ssrsetfwd _ _ _ (((fk,_),(c,t)), docc) =
  let t = Option.default [] @@ Option.map (fun t -> [Bcast t]) t in
  pr_gen_fwd (fun _ _ c -> Pp.(pr_docc docc ++ pr_cpattern c))
    (fun _ -> mt()) pr_ast_closure_term fk (t, c)

}

ARGUMENT EXTEND ssrsetfwd
TYPED AS ((ssrfwdfmt * (lcpattern * ast_closure_lterm option)) * ssrdocc)
PRINTED BY { pr_ssrsetfwd }
| [ ":" ast_closure_lterm(t) ":=" "{" ssrocc(occ) "}" cpattern(c) ] ->
  { mkssrFwdCast FwdPose loc t c, mkocc occ }
| [ ":" ast_closure_lterm(t) ":=" lcpattern(c) ] ->
  { mkssrFwdCast FwdPose loc t c, nodocc }
| [ ":=" "{" ssrocc(occ) "}" cpattern(c) ] ->
  { mkssrFwdVal FwdPose c, mkocc occ }
| [ ":=" lcpattern(c) ] -> { mkssrFwdVal FwdPose c, nodocc }
END

{

let pr_ssrhavefwd env sigma _ _ prt (fwd, hint) = pr_fwd fwd ++ pr_hint env sigma prt hint

}

ARGUMENT EXTEND ssrhavefwd TYPED AS (ssrfwd * ssrhint) PRINTED BY { pr_ssrhavefwd env sigma }
| [ ":" ast_closure_lterm(t) ssrhint(hint) ] -> { mkFwdHint ":" t, hint }
| [ ":" ast_closure_lterm(t) ":=" ast_closure_lterm(c) ] -> { mkFwdCast FwdHave ~loc t ~c, nohint }
| [ ":" ast_closure_lterm(t) ":=" ] -> { mkFwdHintNoTC ":" t, nohint }
| [ ":=" ast_closure_lterm(c) ] -> { mkFwdVal FwdHave c, nohint }
END

{

let intro_id_to_binder = List.map (function
  | IPatId id ->
      let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
      (FwdPose, [BFvar]),
        CAst.make @@ CLambdaN ([CLocalAssum([x], None, Default Glob_term.Explicit, mkCHole xloc)],
          mkCHole None)
  | _ -> anomaly "non-id accepted as binder")

let binder_to_intro_id = CAst.(List.map (function
  | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_,_)],_) }
  | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_,_)],_) } ->
      List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon (One None)) ids
  | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id]
  | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)]
  | _ -> anomaly "ssrbinder is not a binder"))

let pr_ssrhavefwdwbinders env sigma _ _ prt (tr,((hpats, (fwd, hint)))) =
  pr_hpats hpats ++ pr_fwd fwd ++ pr_hint env sigma prt hint

}

ARGUMENT EXTEND ssrhavefwdwbinders
  TYPED AS (bool * (ssrhpats * (ssrfwd * ssrhint)))
  PRINTED BY { pr_ssrhavefwdwbinders env sigma }
| [ ssrhpats_wtransp(trpats) ssrbinder_list(bs) ssrhavefwd(fwd) ] ->
  { let tr, pats = trpats in
    let ((clr, pats), binders), simpl = pats in
    let allbs = intro_id_to_binder binders @ bs in
    let allbinders = binders @ List.flatten (binder_to_intro_id bs) in
    let hint = bind_fwd allbs (fst fwd), snd fwd in
    tr, ((((clr, pats), allbinders), simpl), hint) }
END

{

let pr_ssrdoarg env sigma prc _ prt (((n, m), tac), clauses) =
  pr_index n ++ pr_mmod m ++ pr_hintarg env sigma prt tac ++ pr_clauses clauses

}

ARGUMENT EXTEND ssrdoarg
  TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses)
  PRINTED BY { pr_ssrdoarg env sigma }
END

{

(* type ssrseqarg = ssrindex * (ssrtacarg * ssrtac option) *)

let pr_seqtacarg env sigma prt = function
  | (is_first, []), _ -> str (if is_first then "first" else "last")
  | tac, Some dtac ->
    hv 0 (pr_hintarg env sigma prt tac ++ spc() ++ str "|| " ++ prt env sigma tacltop dtac)
  | tac, _ -> pr_hintarg env sigma prt tac

let pr_ssrseqarg env sigma _ _ prt = function
  | ArgArg 0, tac -> pr_seqtacarg env sigma prt tac
  | i, tac -> pr_index i ++ str " " ++ pr_seqtacarg env sigma prt tac

}

(* We must parse the index separately to resolve the conflict with *)
(* an unindexed tactic.                                            *)
ARGUMENT EXTEND ssrseqarg TYPED AS (ssrindex * (ssrhintarg * tactic option))
                          PRINTED BY { pr_ssrseqarg env sigma }

END

{

let sq_brace_tacnames =
   ["first"; "solve"; "do"; "rewrite"; "have"; "suffices"; "wlog"]
   (* "by" is a keyword *)

let test_ssrseqvar =
  let open Pcoq.Lookahead in
  to_entry "test_ssrseqvar" begin
    lk_ident_except sq_brace_tacnames >> (lk_kws ["[";"first";"last"])
  end

let swaptacarg (loc, b) = (b, []), Some (CAst.make ~loc (TacId []))

let ssrorelse = Entry.make "ssrorelse"

}

GRAMMAR EXTEND Gram
  GLOBAL: ssrorelse ssrseqarg;
  ssrseqidx: [
    [ test_ssrseqvar; id = Prim.ident -> { ArgVar (CAst.make ~loc id) }
    | n = Prim.natural -> { ArgArg (check_index ~loc n) }
    ] ];
  ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]];
  ssrorelse: [[ "||"; tac = ltac_expr LEVEL "2" -> { tac } ]];
  ssrseqarg: TOP [
    [ arg = ssrswap -> { noindex, swaptacarg arg }
    | i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) }
    | i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg }
    | tac = ltac_expr LEVEL "3" -> { noindex, (mk_hint tac, None) }
    ] ];
END

{

let ltac_expr = Pltac.ltac_expr

}

(** 1. Utilities *)

(** Name generation *)

(* Since Coq now does repeated internal checks of its external lexical *)
(* rules, we now need to carve ssreflect reserved identifiers out of   *)
(* out of the user namespace. We use identifiers of the form _id_ for  *)
(* this purpose, e.g., we "anonymize" an identifier id as _id_, adding *)
(* an extra leading _ if this might clash with an internal identifier. *)
(*    We check for ssreflect identifiers in the ident grammar rule;    *)
(* when the ssreflect Module is present this is normally an error,     *)
(* but we provide a compatibility flag to reduce this to a warning.    *)

{

let { Goptions.get = ssr_reserved_ids } =
  Goptions.declare_bool_option_and_ref ~stage:Synterp ~key:["SsrIdents"] ~value:true ()

let is_ssr_reserved s =
  let n = String.length s in n > 2 && s.[0] = '_' && s.[n - 1] = '_'

let ssr_id_of_string loc s =
  if is_ssr_reserved s && is_ssr_loaded () then begin
    if ssr_reserved_ids() then
      CErrors.user_err ~loc (str ("The identifier " ^ s ^ " is reserved."))
    else if is_internal_name s then
      Feedback.msg_warning (str ("Conflict between " ^ s ^ " and ssreflect internal names."))
    else Feedback.msg_warning (str (
     "The name " ^ s ^ " fits the _xxx_ format used for anonymous variables.\n"
  ^ "Scripts with explicit references to anonymous variables are fragile."))
    end; Id.of_string s

let ssr_null_entry = Pcoq.Entry.(of_parser "ssr_null" { parser_fun = fun _ _ -> () })

}

GRAMMAR EXTEND Gram
  GLOBAL: Prim.ident;
  Prim.ident: TOP [[ s = IDENT; ssr_null_entry -> { ssr_id_of_string loc s } ]];
END

{

let perm_tag = "_perm_Hyp_"
let _ = add_internal_name (is_tagged perm_tag)

}

(* We must not anonymize context names discharged by the "in" tactical. *)

(** Tactical extensions. *)

{

  let ssrtac_expr ?loc key args =
    CAst.make ?loc (TacAlias (key, (List.map (fun x -> Tacexpr.TacGeneric (None, x)) args)))

let mk_non_term wit id =
  let open Pptactic in
  TacNonTerm (None, (Extend.Uentry (Genarg.ArgT.Any (Genarg.get_arg_tag wit)), Some id))

let tclintroskey =
  let prods =
    [ mk_non_term wit_ssrintrosarg (Names.Id.of_string "arg") ] in
  let tac = begin fun args ist -> match args with
    | [arg] ->
      let arg = cast_arg wit_ssrintrosarg arg in
      let tac, intros = arg in
      ssrevaltac ist tac <*> tclIPATssr intros
    | _ -> assert false
  end in
  register_ssrtac "tclintros" tac prods

let tclintros_expr ?loc tac ipats =
  let args = [in_gen (rawwit wit_ssrintrosarg) (tac, ipats)] in
  ssrtac_expr ?loc tclintroskey args

}

GRAMMAR EXTEND Gram
  GLOBAL: ltac_expr;
  ltac_expr: LEVEL "3" [
    [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
    ] ];
  ltac_expr: LEVEL "4" [
    [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros }
    ] ];
END


(** Bracketing tactical *)

(* The tactic pretty-printer doesn't know that some extended tactics *)
(* are actually tacticals. To prevent it from improperly removing    *)
(* parentheses we override the parsing rule for bracketed tactic     *)
(* expressions so that the pretty-print always reflects the input.   *)
(* (Removing user-specified parentheses is dubious anyway).          *)

GRAMMAR EXTEND Gram
  GLOBAL: ltac_expr;
  ssrparentacarg: [[ "("; tac = ltac_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]];
  ltac_expr: LEVEL "0" [[ arg = ssrparentacarg -> { CAst.make ~loc (TacArg CAst.(arg.v)) } ]];
END

{
type ssreqid = ssripatrep option

type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats))

}

{

(* We wipe out all the keywords generated by the grammar rules we defined. *)
(* The user is supposed to Require Import ssreflect or Require ssreflect   *)
(* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
(* consequence the extended ssreflect grammar.                             *)
let () = Mltop.add_init_function "coq-core.plugins.ssreflect" (fun () ->
      Pcoq.set_keyword_state !frozen_lexer) ;;

module Internal = struct
  let register_ssrtac = register_ssrtac
  let mk_index = mk_index
  let noindex = noindex
  let tclintros_expr = tclintros_expr
  let intern_ipat = intern_ipat
  let interp_ipat = interp_ipat
  let pr_intros = pr_intros
  let pr_view = pr_view
  let pr_mult = pr_mult
  let is_ssr_loaded = is_ssr_loaded
  let pr_hpats = pr_hpats
  let pr_fwd = pr_fwd
  let pr_hint = pr_hint
  let intro_id_to_binder = intro_id_to_binder
  let binder_to_intro_id = binder_to_intro_id
  let mkFwdHint = mkFwdHint
  let bind_fwd = bind_fwd
  let pr_wgen = pr_wgen
end

}

(* vim: set filetype=ocaml foldmethod=marker: *)