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

DECLARE PLUGIN "ltac2_plugin"

{

open Pp
open Util
open Names
open Pcoq
open Attributes
open Constrexpr
open Tac2expr
open Tac2qexpr
open Ltac_plugin

let lk_ident_or_anti =
  Pcoq.Lookahead.(lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space))

(* lookahead for (x:=t), (?x:=t) and (1:=t) *)
let test_lpar_idnum_coloneq =
  let open Pcoq.Lookahead in
  to_entry "test_lpar_idnum_coloneq" begin
    lk_kw "(" >> (lk_ident_or_anti <+> lk_nat) >> lk_kw ":="
  end

(* lookahead for (x:t), (?x:t) *)
let test_lpar_id_colon =
  let open Pcoq.Lookahead in
  to_entry "test_lpar_id_colon" begin
    lk_kw "(" >> lk_ident_or_anti >> lk_kw ":"
  end

(* Hack to recognize "(x := t)" and "($x := t)" *)
let test_lpar_id_coloneq =
  let open Pcoq.Lookahead in
  to_entry "test_lpar_id_coloneq" begin
    lk_kw "(" >> lk_ident_or_anti >> lk_kw ":="
  end

(* Hack to recognize "(x)" *)
let test_lpar_id_rpar =
  let open Pcoq.Lookahead in
  to_entry "test_lpar_id_rpar" begin
    lk_kw "(" >> lk_ident >> lk_kw ")"
  end

let test_ampersand_ident =
  let open Pcoq.Lookahead in
  to_entry "test_ampersand_ident" begin
    lk_kw "&" >> lk_ident >> check_no_space
  end

let test_dollar_ident =
  let open Pcoq.Lookahead in
  to_entry "test_dollar_ident" begin
    lk_kw "$" >> lk_ident >> check_no_space
  end

let test_ltac1_env =
  let open Pcoq.Lookahead in
  to_entry "test_ltac1_env" begin
    lk_ident_list >> lk_kw "|-"
  end

let ltac2_expr = Tac2entries.Pltac.ltac2_expr
let _ltac2_expr = ltac2_expr
let ltac2_type = Entry.create "ltac2_type"
let tac2def_val = Entry.create "tac2def_val"
let tac2def_typ = Entry.create "tac2def_typ"
let tac2def_ext = Entry.create "tac2def_ext"
let tac2def_syn = Entry.create "tac2def_syn"
let tac2def_mut = Entry.create "tac2def_mut"
let tac2mode = Entry.create "ltac2_command"

let ltac_expr = Pltac.ltac_expr
let tac2expr_in_env = Tac2entries.Pltac.tac2expr_in_env

let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)
let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c
let inj_pattern loc c = inj_wit Tac2quote.wit_pattern loc c
let inj_reference loc c = inj_wit Tac2quote.wit_reference loc c
let inj_ltac1 loc e = inj_wit Tac2quote.wit_ltac1 loc e
let inj_ltac1val loc e = inj_wit Tac2quote.wit_ltac1val loc e

let pattern_of_qualid qid =
  if Tac2env.is_constructor qid then CAst.make ?loc:qid.CAst.loc @@ CPatRef (RelId qid, [])
  else
    let open Libnames in
    if qualid_is_ident qid then CAst.make ?loc:qid.CAst.loc @@ CPatVar (Name (qualid_basename qid))
    else
      CErrors.user_err ?loc:qid.CAst.loc (Pp.str "Syntax error")

let opt_fun ?loc args ty e =
  let e = match ty with
  | None -> e
  | Some ty -> CAst.make ?loc:e.CAst.loc (CTacCnv (e, ty))
  in
  match args with
  | [] -> e
  | _ :: _ -> CAst.make ?loc (CTacFun (args, e))

}

GRAMMAR EXTEND Gram
  GLOBAL: ltac2_expr ltac2_type tac2def_val tac2def_typ tac2def_ext tac2def_syn
          tac2def_mut tac2expr_in_env;
  tac2pat:
    [ "1" LEFTA
      [ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> {
        if Tac2env.is_constructor qid then
          CAst.make ~loc @@ CPatRef (RelId qid, pl)
        else
          CErrors.user_err ~loc (Pp.str "Syntax error") }
      | qid = Prim.qualid -> { pattern_of_qualid qid }
      | "["; "]" -> { CAst.make ~loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_nil), []) }
      | p1 = tac2pat; "::"; p2 = tac2pat ->
        { CAst.make ~loc @@ CPatRef (AbsKn (Other Tac2core.Core.c_cons), [p1; p2])}
      ]
    | "0"
      [ "_" -> { CAst.make ~loc @@ CPatVar Anonymous }
      | "()" -> { CAst.make ~loc @@ CPatRef (AbsKn (Tuple 0), []) }
      | qid = Prim.qualid -> { pattern_of_qualid qid }
      | "("; p = atomic_tac2pat; ")" -> { p }
    ] ]
  ;
  atomic_tac2pat:
    [ [ ->
        { CAst.make ~loc @@ CPatRef (AbsKn (Tuple 0), []) }
      | p = tac2pat; ":"; t = ltac2_type ->
        { CAst.make ~loc @@ CPatCnv (p, t) }
      | p = tac2pat; ","; pl = LIST0 tac2pat SEP "," ->
        { let pl = p :: pl in
          CAst.make ~loc @@ CPatRef (AbsKn (Tuple (List.length pl)), pl) }
      | p = tac2pat -> { p }
    ] ]
  ;
  ltac2_expr:
    [ "6" RIGHTA
        [ e1 = SELF; ";"; e2 = SELF -> { CAst.make ~loc @@ CTacSeq (e1, e2) } ]
    | "5"
      [ "fun"; it = LIST1 input_fun; ty = type_cast; "=>"; body = ltac2_expr LEVEL "6" ->
        { opt_fun ~loc it ty body }
      | "let"; isrec = rec_flag;
          lc = LIST1 let_clause SEP "with"; "in";
          e = ltac2_expr LEVEL "6" ->
        { CAst.make ~loc @@ CTacLet (isrec, lc, e) }
      | "match"; e = ltac2_expr LEVEL "5"; "with"; bl = branches; "end" ->
        { CAst.make ~loc @@ CTacCse (e, bl) }
      | "if"; e = ltac2_expr LEVEL "5"; "then"; e1 = ltac2_expr LEVEL "5"; "else"; e2 = ltac2_expr LEVEL "5" ->
        { CAst.make ~loc @@ CTacIft (e, e1, e2) }
      ]
    | "4" LEFTA [ ]
    | "3" [ e0 = SELF; ","; el = LIST1 NEXT SEP "," ->
        { let el = e0 :: el in
          CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) } ]
    | "2" RIGHTA
      [ e1 = ltac2_expr; "::"; e2 = ltac2_expr ->
        { CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2]) }
      ]
    | "1" LEFTA
      [ e = ltac2_expr; el = LIST1 ltac2_expr LEVEL "0" ->
        { CAst.make ~loc @@ CTacApp (e, el) }
      | e = SELF; ".("; qid = Prim.qualid; ")" ->
        { CAst.make ~loc @@ CTacPrj (e, RelId qid) }
      | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = ltac2_expr LEVEL "5" ->
        { CAst.make ~loc @@ CTacSet (e, RelId qid, r) } ]
    | "0"
      [ "("; a = SELF; ")" -> { a }
      | "("; a = SELF; ":"; t = ltac2_type; ")" ->
        { CAst.make ~loc @@ CTacCnv (a, t) }
      | "()" ->
        { CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) }
      | "("; ")" ->
        { CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) }
      | "["; a = LIST0 ltac2_expr LEVEL "5" SEP ";"; "]" ->
        { Tac2quote.of_list ~loc (fun x -> x) a }
      | "{"; a = tac2rec_fieldexprs; "}" ->
        { CAst.make ~loc @@ CTacRec a }
      | a = tactic_atom -> { a } ]
    ]
  ;
  branches:
  [ [ -> { [] }
    | "|"; bl = LIST1 branch SEP "|" -> { bl }
    | bl = LIST1 branch SEP "|" -> { bl } ]
  ]
  ;
  branch:
  [ [ pat = tac2pat LEVEL "1"; "=>"; e = ltac2_expr LEVEL "6" -> { (pat, e) } ] ]
  ;
  rec_flag:
    [ [ IDENT "rec" -> { true }
      | -> { false } ] ]
  ;
  mut_flag:
    [ [ IDENT "mutable" -> { true }
      | -> { false } ] ]
  ;
  ltac2_typevar:
    [ [ "'"; id = Prim.ident -> { id } ] ]
  ;
  tactic_atom:
    [ [ n = Prim.integer -> { CAst.make ~loc @@ CTacAtm (AtmInt n) }
      | s = Prim.string -> { CAst.make ~loc @@ CTacAtm (AtmStr s) }
      | qid = Prim.qualid ->
      { if Tac2env.is_constructor qid then
          CAst.make ~loc @@ CTacCst (RelId qid)
        else
          CAst.make ~loc @@ CTacRef (RelId qid) }
      | "@"; id = Prim.ident -> { Tac2quote.of_ident (CAst.make ~loc id) }
      | "&"; id = lident -> { Tac2quote.of_hyp ~loc id }
      | "'"; c = Constr.constr -> { inj_open_constr loc c }
      | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_constr c }
      | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_open_constr c }
      | IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c }
      | IDENT "pat"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c }
      | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c }
      | IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid }
      | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid }
    ] ]
  ;
  ltac1_expr_in_env:
    [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac_expr -> { ids, e }
      | e = ltac_expr -> { [], e }
    ] ]
  ;
  tac2expr_in_env :
    [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac2_expr ->
      { let check { CAst.v = id; CAst.loc = loc } =
          if Tac2env.is_constructor (Libnames.qualid_of_ident ?loc id) then
            CErrors.user_err ?loc Pp.(str "Invalid bound Ltac2 identifier " ++ Id.print id)
        in
        let () = List.iter check ids in
        (ids, e)
      }
      | tac = ltac2_expr -> { [], tac }
    ] ]
  ;
  type_cast:
    [ [ -> { None }
      | ":"; ty = ltac2_type -> { Some ty }
    ] ]
  ;
  let_clause:
    [ [ binder = let_binder; ty = type_cast; ":="; te = ltac2_expr ->
      { let (pat, fn) = binder in
        let te = opt_fun ~loc fn ty te in
        (pat, te) }
    ] ]
  ;
  let_binder:
    [ [ pats = LIST1 input_fun ->
      { match pats with
        | [{CAst.v=CPatVar _} as pat] -> (pat, [])
        | ({CAst.v=CPatVar (Name id)} as pat) :: args -> (pat, args)
        | [pat] -> (pat, [])
        | _ -> CErrors.user_err ~loc (str "Invalid pattern") }
    ] ]
  ;
  ltac2_type:
    [ "5" RIGHTA
      [ t1 = ltac2_type; "->"; t2 = ltac2_type -> { CAst.make ~loc @@ CTypArrow (t1, t2) } ]
    | "2"
      [ t = ltac2_type; "*"; tl = LIST1 ltac2_type LEVEL "1" SEP "*" ->
      { let tl = t :: tl in
        CAst.make ~loc @@ CTypRef (AbsKn (Tuple (List.length tl)), tl) } ]
    | "1" LEFTA
      [ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ]
    | "0"
      [ "(";  p = LIST1 ltac2_type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid ->
        { match p, qid with
          | [t], None -> t
          | _, None -> CErrors.user_err ~loc (Pp.str "Syntax error")
          | ts, Some qid -> CAst.make ~loc @@ CTypRef (RelId qid, p)
        }
      | id = ltac2_typevar -> { CAst.make ~loc @@ CTypVar (Name id) }
      | "_" -> { CAst.make ~loc @@ CTypVar Anonymous }
      | qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) }
      ]
    ];
  locident:
    [ [ id = Prim.ident -> { CAst.make ~loc id } ] ]
  ;
  binder:
    [ [ "_" -> { CAst.make ~loc Anonymous }
      | l = Prim.ident -> { CAst.make ~loc (Name l) } ] ]
  ;
  input_fun:
    [ [ b = tac2pat LEVEL "0" -> { b } ] ]
  ;
  tac2def_body:
    [ [ name = binder; it = LIST0 input_fun; ty = type_cast; ":="; e = ltac2_expr ->
      { (name, opt_fun ~loc it ty e) }
    ] ]
  ;
  tac2def_val:
    [ [ mut = mut_flag; isrec = rec_flag; l = LIST1 tac2def_body SEP "with" ->
        { StrVal (mut, isrec, l) }
    ] ]
  ;
  tac2def_mut:
    [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = ltac2_expr -> { StrMut (qid, old, e) } ] ]
  ;
  tac2typ_knd:
    [ [ t = ltac2_type -> { CTydDef (Some t) }
      | "["; ".."; "]" -> { CTydOpn }
      | "["; t = tac2alg_constructors; "]" -> { CTydAlg t }
      | "{"; t = tac2rec_fields; "}"-> { CTydRec t } ] ]
  ;
  tac2alg_constructors:
    [ [ "|"; cs = LIST1 tac2alg_constructor SEP "|" -> { cs }
      | cs = LIST0 tac2alg_constructor SEP "|" -> { cs } ] ]
  ;
  tac2alg_constructor:
    [ [ c = Prim.ident -> { (c, []) }
      | c = Prim.ident; "("; args = LIST0 ltac2_type SEP ","; ")"-> { (c, args) } ] ]
  ;
  tac2rec_fields:
    [ [ f = tac2rec_field; ";"; l = tac2rec_fields -> { f :: l }
      | f = tac2rec_field; ";" -> { [f] }
      | f = tac2rec_field -> { [f] }
      | -> { [] } ] ]
  ;
  tac2rec_field:
    [ [ mut = mut_flag; id = Prim.ident; ":"; t = ltac2_type -> { (id, mut, t) } ] ]
  ;
  tac2rec_fieldexprs:
    [ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> { f :: l }
      | f = tac2rec_fieldexpr; ";" -> { [f] }
      | f = tac2rec_fieldexpr-> { [f] }
      | -> { [] } ] ]
  ;
  tac2rec_fieldexpr:
    [ [ qid = Prim.qualid; ":="; e = ltac2_expr LEVEL "1" -> { RelId qid, e } ] ]
  ;
  tac2typ_prm:
    [ [ -> { [] }
      | id = ltac2_typevar -> { [CAst.make ~loc id] }
      | "("; ids = LIST1 [ id = ltac2_typevar -> { CAst.make ~loc id } ] SEP "," ;")" -> { ids }
    ] ]
  ;
  tac2typ_def:
    [ [ prm = tac2typ_prm; id = Prim.qualid; b = tac2type_body -> { let (r, e) = b in (id, r, (prm, e)) } ] ]
  ;
  tac2type_body:
    [ [ -> { false, CTydDef None }
      | ":="; e = tac2typ_knd -> { false, e }
      | "::="; e = tac2typ_knd -> { true, e }
    ] ]
  ;
  tac2def_typ:
    [ [ "Type"; isrec = rec_flag; l = LIST1 tac2typ_def SEP "with" ->
        { StrTyp (isrec, l) }
    ] ]
  ;
  tac2def_ext:
    [ [ "@"; IDENT "external"; id = locident; ":"; t = ltac2_type LEVEL "5"; ":=";
        plugin = Prim.string; name = Prim.string ->
      { let ml = { mltac_plugin = plugin; mltac_tactic = name } in
        StrPrm (id, t, ml) }
    ] ]
  ;
  syn_node:
    [ [ "_" -> { CAst.make ~loc None }
      | id = Prim.ident -> { CAst.make ~loc (Some id) }
    ] ]
  ;
  ltac2_scope:
    [ [ s = Prim.string -> { SexprStr (CAst.make ~loc s) }
      | n = Prim.integer -> { SexprInt (CAst.make ~loc n) }
      | id = syn_node -> { SexprRec (loc, id, []) }
      | id = syn_node; "("; tok = LIST1 ltac2_scope SEP "," ; ")" ->
        { SexprRec (loc, id, tok) }
    ] ]
  ;
  syn_level:
    [ [ -> { None }
      | ":"; n = Prim.natural -> { Some n }
    ] ]
  ;
  tac2def_syn:
    [ [ "Notation"; toks = LIST1 ltac2_scope; n = syn_level; ":=";
        e = ltac2_expr ->
        { StrSyn (toks, n, e) }
    ] ]
  ;
  lident:
    [ [ id = Prim.ident -> { CAst.make ~loc id } ] ]
  ;
  globref:
    [ [ "&"; id = Prim.ident -> { CAst.make ~loc (QHypothesis id) }
      | qid = Prim.qualid -> { CAst.make ~loc @@ QReference qid }
    ] ]
  ;
END

(* Quotation scopes used by notations *)

{

open Tac2entries.Pltac

let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))

}

GRAMMAR EXTEND Gram
  GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
          q_conversion q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
          q_destruction_arg q_reference q_with_bindings q_constr_matching
          q_goal_matching q_hintdb q_move_location q_pose q_assert;
  anti:
    [ [ "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) } ] ]
  ;
  ident_or_anti:
    [ [ id = lident -> { QExpr id }
      | "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) }
    ] ]
  ;
  lident:
    [ [ id = Prim.ident -> { CAst.make ~loc id } ] ]
  ;
  lnatural:
    [ [ n = Prim.natural -> { CAst.make ~loc n } ] ]
  ;
  q_ident:
    [ [ id = ident_or_anti -> { id } ] ]
  ;
  qhyp:
    [ [ x = anti -> { x }
      | n = lnatural -> { QExpr (CAst.make ~loc @@ QAnonHyp n) }
      | id = lident -> { QExpr (CAst.make ~loc @@ QNamedHyp id) }
    ] ]
  ;
  simple_binding:
    [ [ "("; h = qhyp; ":="; c = Constr.lconstr; ")" ->
        { CAst.make ~loc (h, c) }
    ] ]
  ;
  bindings:
    [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
        { CAst.make ~loc @@ QExplicitBindings bl }
      | bl = LIST1 Constr.constr ->
        { CAst.make ~loc @@ QImplicitBindings bl }
    ] ]
  ;
  q_bindings:
    [ [ bl = bindings -> { bl } ] ]
  ;
  q_with_bindings:
    [ [ bl = with_bindings -> { bl } ] ]
  ;
  intropatterns:
    [ [ l = LIST0 nonsimple_intropattern -> { CAst.make ~loc l } ] ]
  ;
(*   ne_intropatterns: *)
(*     [ [ l = LIST1 nonsimple_intropattern -> l ]] *)
(*   ; *)
  or_and_intropattern:
    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { CAst.make ~loc @@ QIntroOrPattern tc }
      | "()" -> { CAst.make ~loc @@ QIntroAndPattern (CAst.make ~loc []) }
      | "("; si = simple_intropattern; ")" -> { CAst.make ~loc @@ QIntroAndPattern (CAst.make ~loc [si]) }
      | "("; si = simple_intropattern; ",";
             tc = LIST1 simple_intropattern SEP "," ; ")" ->
             { CAst.make ~loc @@ QIntroAndPattern (CAst.make ~loc (si::tc)) }
      | "("; si = simple_intropattern; "&";
             tc = LIST1 simple_intropattern SEP "&" ; ")" ->
          (* (A & B & C) is translated into (A,(B,C)) *)
        { let rec pairify = function
            | ([]|[_]|[_;_]) as l -> CAst.make ~loc l
            | t::q ->
              let q =
                CAst.make ~loc @@
                  QIntroAction (CAst.make ~loc @@
                    QIntroOrAndPattern (CAst.make ~loc @@
                      QIntroAndPattern (pairify q)))
              in
              CAst.make ~loc [t; q]
          in CAst.make ~loc @@ QIntroAndPattern (pairify (si::tc)) } ] ]
  ;
  equality_intropattern:
    [ [ "->" -> { CAst.make ~loc @@ QIntroRewrite true }
      | "<-" -> { CAst.make ~loc @@ QIntroRewrite false }
      | "[="; tc = intropatterns; "]" -> { CAst.make ~loc @@ QIntroInjection tc } ] ]
  ;
  naming_intropattern:
    [ [ LEFTQMARK; id = lident ->
        { CAst.make ~loc @@ QIntroFresh (QExpr id) }
      | "?$"; id = lident ->
        { CAst.make ~loc @@ QIntroFresh (QAnti id) }
      | "?" ->
        { CAst.make ~loc @@ QIntroAnonymous }
      | id = ident_or_anti ->
        { CAst.make ~loc @@ QIntroIdentifier id }
    ] ]
  ;
  nonsimple_intropattern:
    [ [ l = simple_intropattern -> { l }
      | "*"  -> { CAst.make ~loc @@ QIntroForthcoming true }
      | "**" -> { CAst.make ~loc @@ QIntroForthcoming false } ] ]
  ;
  simple_intropattern:
    [ [ pat = simple_intropattern_closed ->
(*         l = LIST0 ["%"; c = term LEVEL "0" -> c] -> *)
        (** TODO: handle %pat *)
        { pat }
    ] ]
  ;
  simple_intropattern_closed:
    [ [ pat = or_and_intropattern ->
        { CAst.make ~loc @@ QIntroAction (CAst.make ~loc @@ QIntroOrAndPattern pat) }
      | pat = equality_intropattern ->
        { CAst.make ~loc @@ QIntroAction pat }
      | "_" ->
        { CAst.make ~loc @@ QIntroAction (CAst.make ~loc @@ QIntroWildcard) }
      | pat = naming_intropattern ->
        { CAst.make ~loc @@ QIntroNaming pat }
    ] ]
  ;
  q_intropatterns:
    [ [ ipat = intropatterns -> { ipat } ] ]
  ;
  q_intropattern:
    [ [ ipat = simple_intropattern -> { ipat } ] ]
  ;
  nat_or_anti:
    [ [ n = lnatural -> { QExpr n }
      | "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) }
    ] ]
  ;
  eqn_ipat:
    [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some pat }
      | -> { None }
    ] ]
  ;
  with_bindings:
    [ [ "with"; bl = bindings -> { bl } | -> { CAst.make ~loc @@ QNoBindings } ] ]
  ;
  constr_with_bindings:
    [ [ c = Constr.constr; l = with_bindings -> { CAst.make ~loc @@ (c, l) } ] ]
  ;
  destruction_arg:
    [ [ n = lnatural -> { CAst.make ~loc @@ QElimOnAnonHyp n }
      | id = lident -> { CAst.make ~loc @@ QElimOnIdent id }
      | c = constr_with_bindings -> { CAst.make ~loc @@ QElimOnConstr c }
    ] ]
  ;
  q_destruction_arg:
    [ [ arg = destruction_arg -> { arg } ] ]
  ;
  as_or_and_ipat:
    [ [ "as"; ipat = or_and_intropattern -> { Some ipat }
      | -> { None }
    ] ]
  ;
  occs_nums:
    [ [ nl = LIST1 nat_or_anti -> { CAst.make ~loc @@ QOnlyOccurrences nl }
      | "-"; n = nat_or_anti; nl = LIST0 nat_or_anti ->
        { CAst.make ~loc @@ QAllOccurrencesBut (n::nl) }
    ] ]
  ;
  occs:
    [ [ "at"; occs = occs_nums -> { occs } | -> { CAst.make ~loc QAllOccurrences } ] ]
  ;
  hypident:
    [ [ id = ident_or_anti ->
        { id,Locus.InHyp }
      | "("; IDENT "type"; IDENT "of"; id = ident_or_anti; ")" ->
        { id,Locus.InHypTypeOnly }
      | "("; IDENT "value"; IDENT "of"; id = ident_or_anti; ")" ->
        { id,Locus.InHypValueOnly }
    ] ]
  ;
  hypident_occ:
    [ [ h=hypident; occs=occs -> { let (id,l) = h in ((occs,id),l) } ] ]
  ;
  in_clause:
    [ [ "*"; occs=occs ->
        { { q_onhyps = None; q_concl_occs = occs } }
      | "*"; "|-"; occs = concl_occ ->
        { { q_onhyps = None; q_concl_occs = occs } }
      | hl = LIST0 hypident_occ SEP ","; "|-"; occs = concl_occ ->
        { { q_onhyps = Some hl; q_concl_occs = occs } }
      | hl = LIST0 hypident_occ SEP "," ->
        { { q_onhyps = Some hl; q_concl_occs = CAst.make ~loc QNoOccurrences } }
    ] ]
  ;
  clause:
    [ [ "in"; cl = in_clause -> { CAst.make ~loc @@ cl }
      | "at"; occs = occs_nums ->
        { CAst.make ~loc @@ { q_onhyps = Some []; q_concl_occs = occs } }
    ] ]
  ;
  q_clause:
    [ [ cl = clause -> { cl } ] ]
  ;
  concl_occ:
    [ [ "*"; occs = occs -> { occs }
      | -> { CAst.make ~loc QNoOccurrences }
    ] ]
  ;
  induction_clause:
    [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
        cl = OPT clause ->
      { CAst.make ~loc @@ {
          indcl_arg = c;
          indcl_eqn = eq;
          indcl_as = pat;
          indcl_in = cl;
        } }
    ] ]
  ;
  q_induction_clause:
    [ [ cl = induction_clause -> { cl } ] ]
  ;
  conversion:
    [ [ c = Constr.constr ->
        { CAst.make ~loc @@ QConvert c }
      | c1 = Constr.constr; "with"; c2 = Constr.constr ->
        { CAst.make ~loc @@ QConvertWith (c1, c2) }
    ] ]
  ;
  q_conversion:
    [ [ c = conversion -> { c } ] ]
  ;
  ltac2_orient:
    [ [ "->" -> { CAst.make ~loc (Some true) }
      | "<-" -> { CAst.make ~loc (Some false) }
      | -> { CAst.make ~loc None }
    ]]
  ;
  rewriter:
    [ [ "!"; c = constr_with_bindings ->
        { (CAst.make ~loc @@ QRepeatPlus,c) }
      | [ "?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings ->
        { (CAst.make ~loc @@ QRepeatStar,c) }
      | n = lnatural; "!"; c = constr_with_bindings ->
        { (CAst.make ~loc @@ QPrecisely n,c) }
      |	n = lnatural; ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings ->
        { (CAst.make ~loc @@ QUpTo n,c) }
      | n = lnatural; c = constr_with_bindings ->
        { (CAst.make ~loc @@ QPrecisely n,c) }
      | c = constr_with_bindings ->
        { (CAst.make ~loc @@ QPrecisely (CAst.make 1), c) }
      ] ]
  ;
  oriented_rewriter:
    [ [ b = ltac2_orient; r = rewriter ->
      { let (m, c) = r in
        CAst.make ~loc @@ {
        rew_orient = b;
        rew_repeat = m;
        rew_equatn = c;
      } }
    ] ]
  ;
  q_rewriting:
    [ [ r = oriented_rewriter -> { r } ] ]
  ;
  tactic_then_last:
    [ [ "|"; lta = LIST0 (OPT ltac2_expr LEVEL "6") SEP "|" -> { lta }
      | -> { [] }
    ] ]
  ;
  for_each_goal:
    [ [ ta = ltac2_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (Some ta :: first, last) }
      | ta = ltac2_expr; ".."; l = tactic_then_last -> { ([], Some (Some ta, l)) }
      | ".."; l = tactic_then_last -> { ([], Some (None, l)) }
      | ta = ltac2_expr -> { ([Some ta], None) }
      | "|"; tg = for_each_goal -> { let (first,last) = tg in (None :: first, last) }
      | -> { ([None], None) }
    ] ]
  ;
  q_dispatch:
    [ [ d = for_each_goal -> { CAst.make ~loc d } ] ]
  ;
  q_occurrences:
    [ [ occs = occs -> { occs } ] ]
  ;
  ltac2_red_flag:
    [ [ IDENT "beta" -> { CAst.make ~loc @@ QBeta }
      | IDENT "iota" -> { CAst.make ~loc @@ QIota }
      | IDENT "match" -> { CAst.make ~loc @@ QMatch }
      | IDENT "fix" -> { CAst.make ~loc @@ QFix }
      | IDENT "cofix" -> { CAst.make ~loc @@ QCofix }
      | IDENT "zeta" -> { CAst.make ~loc @@ QZeta }
      | IDENT "delta"; d = delta_flag -> { d }
    ] ]
  ;
  refglobal:
    [ [ "&"; id = Prim.ident -> { QExpr (CAst.make ~loc @@ QHypothesis id) }
      | qid = Prim.qualid -> { QExpr (CAst.make ~loc @@ QReference qid) }
      | "$"; id = Prim.ident -> { QAnti (CAst.make ~loc id) }
    ] ]
  ;
  q_reference:
    [ [ r = refglobal -> { r } ] ]
  ;
  refglobals:
    [ [ gl = LIST1 refglobal -> { CAst.make ~loc gl } ] ]
  ;
  delta_flag:
    [ [ "-"; "["; idl = refglobals; "]" -> { CAst.make ~loc @@ QDeltaBut idl }
      | "["; idl = refglobals; "]" -> { CAst.make ~loc @@ QConst idl }
      | -> { CAst.make ~loc @@ QDeltaBut (CAst.make ~loc []) }
    ] ]
  ;
  strategy_flag:
    [ [ s = LIST1 ltac2_red_flag -> { CAst.make ~loc s }
      | d = delta_flag ->
      { CAst.make ~loc
          [CAst.make ~loc QBeta; CAst.make ~loc QIota; CAst.make ~loc QZeta; d] }
    ] ]
  ;
  q_strategy_flag:
    [ [ flag = strategy_flag -> { flag } ] ]
  ;
  hintdb:
    [ [ "*" -> { CAst.make ~loc @@ QHintAll }
      | l = LIST1 ident_or_anti -> { CAst.make ~loc @@ QHintDbs l }
    ] ]
  ;
  q_hintdb:
    [ [ db = hintdb -> { db } ] ]
  ;
  match_pattern:
    [ [ IDENT "context";  id = OPT Prim.ident;
          "["; pat = Constr.cpattern; "]" -> { CAst.make ~loc @@ QConstrMatchContext (id, pat) }
      | pat = Constr.cpattern -> { CAst.make ~loc @@ QConstrMatchPattern pat } ] ]
  ;
  match_rule:
    [ [ mp = match_pattern; "=>"; tac = ltac2_expr ->
        { CAst.make ~loc @@ (mp, tac) }
    ] ]
  ;
  match_list:
    [ [ mrl = LIST1 match_rule SEP "|" -> { CAst.make ~loc @@ mrl }
      | "|"; mrl = LIST1 match_rule SEP "|" -> { CAst.make ~loc @@ mrl } ] ]
  ;
  q_constr_matching:
    [ [ m = match_list -> { m } ] ]
  ;
  gmatch_hyp_pattern:
    [ [ na = Prim.name; ":"; pat = match_pattern -> { (na, pat) } ] ]
  ;
  gmatch_pattern:
    [ [ "["; hl = LIST0 gmatch_hyp_pattern SEP ","; "|-"; p = match_pattern; "]" ->
        { CAst.make ~loc @@ {
          q_goal_match_concl = p;
          q_goal_match_hyps = hl;
        } }
    ] ]
  ;
  gmatch_rule:
    [ [ mp = gmatch_pattern; "=>"; tac = ltac2_expr ->
        { CAst.make ~loc @@ (mp, tac) }
    ] ]
  ;
  goal_match_list:
    [ [ mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl }
      | "|"; mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl } ] ]
  ;
  q_goal_matching:
    [ [ m = goal_match_list -> { m } ] ]
  ;
  move_location:
    [ [ "at"; IDENT "top" -> { CAst.make ~loc @@ QMoveFirst }
      | "at"; IDENT "bottom" -> { CAst.make ~loc @@ QMoveLast }
      | IDENT "after"; id = ident_or_anti -> { CAst.make ~loc @@ QMoveAfter id }
      | IDENT "before"; id = ident_or_anti -> { CAst.make ~loc @@ QMoveBefore id }
    ] ]
  ;
  q_move_location:
    [ [ mv = move_location -> { mv } ] ]
  ;
  as_name:
    [ [ -> { None }
      | "as"; id = ident_or_anti -> { Some id }
    ] ]
  ;
  pose:
    [ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
        { CAst.make ~loc (Some id, c) }
      | c = Constr.constr; na = as_name -> { CAst.make ~loc (na, c) }
    ] ]
  ;
  q_pose:
    [ [ p = pose -> { p } ] ]
  ;
  as_ipat:
    [ [ "as"; ipat = simple_intropattern -> { Some ipat }
      | -> { None }
    ] ]
  ;
  by_tactic:
    [ [ "by"; tac = ltac2_expr -> { Some tac }
      | -> { None }
    ] ]
  ;
  assertion:
    [ [ test_lpar_id_coloneq; "("; id = ident_or_anti; ":="; c = Constr.lconstr; ")" ->
        { CAst.make ~loc (QAssertValue (id, c)) }
      | test_lpar_id_colon; "("; id = ident_or_anti; ":"; c = Constr.lconstr; ")"; tac = by_tactic ->
      { let ipat = CAst.make ~loc @@ QIntroNaming (CAst.make ~loc @@ QIntroIdentifier id) in
        CAst.make ~loc (QAssertType (Some ipat, c, tac)) }
      | c = Constr.constr; ipat = as_ipat; tac = by_tactic ->
        { CAst.make ~loc (QAssertType (ipat, c, tac)) }
    ] ]
  ;
  q_assert:
    [ [ a = assertion -> { a } ] ]
  ;
END

(** Extension of constr syntax *)

(*
GRAMMAR EXTEND Gram
  Pcoq.Constr.term: LEVEL "0"
    [ [ IDENT "ltac2"; ":"; "("; tac = ltac2_expr; ")" ->
      { let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
        CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
      | test_ampersand_ident; "&"; id = Prim.ident ->
      { let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in
        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
        CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
      | test_dollar_ident; "$"; id = Prim.ident ->
      { let id = Loc.tag ~loc id in
        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
        CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
    ] ]
  ;
END
*)
{

let () =

let open Tok in
let (++) r s = Pcoq.Rule.next r s in
let rules = [
  Pcoq.(
    Production.make
      (Rule.stop ++ Symbol.nterm test_dollar_ident ++ Symbol.token (PKEYWORD "$") ++ Symbol.nterm Prim.ident)
    begin fun id _ _ loc ->
      let id = Loc.tag ~loc id in
      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
      CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
    end
  );

  Pcoq.(
    Production.make
      (Rule.stop ++ Symbol.nterm test_ampersand_ident ++ Symbol.token (PKEYWORD "&") ++ Symbol.nterm Prim.ident)
    begin fun id _ _ loc ->
      let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in
      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
      CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
    end
  );

  Pcoq.(
    Production.make
      (Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++
       Symbol.token (PKEYWORD "(") ++ Symbol.nterm ltac2_expr ++ Symbol.token (PKEYWORD ")"))
    begin fun _ tac _ _ _ loc ->
      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
      CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
    end
  )
] in

Hook.set Tac2entries.register_constr_quotations begin fun () ->
  Pcoq.grammar_extend Pcoq.Constr.term {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
end

}

{

let pr_ltac2entry _ = mt () (* FIXME *)
let pr_ltac2expr _ = mt () (* FIXME *)

}

VERNAC ARGUMENT EXTEND ltac2_entry
PRINTED BY { pr_ltac2entry }
| [ tac2def_val(v) ] -> { v }
| [ tac2def_typ(t) ] -> { t }
| [ tac2def_ext(e) ] -> { e }
| [ tac2def_syn(e) ] -> { e }
| [ tac2def_mut(e) ] -> { e }
END

VERNAC ARGUMENT EXTEND ltac2_expr
PRINTED BY { pr_ltac2expr }
| [ _ltac2_expr(e) ] -> { e }
END

{

let classify_ltac2 = function
| StrSyn _ -> Vernacextend.(VtSideff ([], VtNow))
| StrMut _ | StrVal _ | StrPrm _  | StrTyp _ -> Vernacextend.classify_as_sideeff

}

VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
| #[ deprecation = deprecation; local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
  Tac2entries.register_struct ?deprecation ?local e
  }
| ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> {
  fun ~pstate -> Tac2entries.perform_eval ~pstate e
  }
END

{

let _ = Pvernac.register_proof_mode "Ltac2" tac2mode

open G_ltac
open Vernacextend

}

VERNAC { tac2mode } EXTEND VernacLtac2
| ![proof] [ ltac2_expr(t) ltac_use_default(with_end_tac) ] =>
    { classify_as_proofstep } -> {
(*     let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
  fun ~pstate -> Tac2entries.call ~pstate ~with_end_tac t }
END

GRAMMAR EXTEND Gram
  GLOBAL: tac2mode;
  tac2mode:
    [ [ tac = G_vernac.query_command -> { tac None } ] ];
END

{

open Stdarg

}

VERNAC COMMAND EXTEND Ltac2Print CLASSIFIED AS SIDEFF
| [ "Print" "Ltac2" reference(tac) ] -> { Tac2entries.print_ltac tac }
END