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

{

open Pp
open Util
open Names
open Glob_term
open Vernacexpr
open Constrexpr
open Constrexpr_ops
open Extend
open Decls
open Declaremods

module C = Constr

open Pcoq
open Pcoq.Prim
open Pcoq.Constr
open Pcoq.Module
open Pvernac.Vernac_
open Attributes

(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)

let query_command = Entry.make "query_command"

let search_query = Entry.make "search_query"
let search_queries = Entry.make "search_queries"

let subprf = Entry.make "subprf"
let subprf_with_selector = Entry.make "subprf_with_selector"

let quoted_attributes = Entry.make "quoted_attributes"
let attribute_list = Entry.make "attribute_list"
let coercion_class = Entry.make "coercion_class"
let thm_token = Entry.make "thm_token"
let def_token = Entry.make "def_token"
let assumption_token = Entry.make "assumption_token"
let def_body = Entry.make "def_body"
let notation_declaration = Entry.make "notation_declaration"
let decl_notations = Entry.make "decl_notations"
let record_field = Entry.make "record_field"
let of_type = Entry.make "of_type"
let of_type_inst = Entry.make "of_type_inst"
let section_subset_expr = Entry.make "section_subset_expr"
let scope_delimiter = Entry.make "scope_delimiter"
let syntax_modifiers = Entry.make "syntax_modifiers"
let goal_selector = Entry.make "goal_selector"
let toplevel_selector = Entry.make "toplevel_selector"

let make_bullet s =
  let open Proof_bullet in
  let n = String.length s in
  match s.[0] with
  | '-' -> Dash n
  | '+' -> Plus n
  | '*' -> Star n
  | _ -> assert false

(* For now we just keep the top-level location of the whole
   vernacular, that is to say, including attributes and control flags;
   this is not very convenient for advanced clients tho, so in the
   future it'd be cool to actually locate the attributes and control
   flags individually too. *)
let add_control_flag ~loc ~flag { CAst.v = cmd } =
  CAst.make ~loc { cmd with control = flag :: cmd.control }

let test_hash_ident =
  let open Pcoq.Lookahead in
  to_entry "test_hash_ident" begin
    lk_kw "#" >> lk_ident >> check_no_space
  end

let test_id_colon =
  let open Pcoq.Lookahead in
  to_entry "test_id_colon" begin
    lk_ident >> lk_kw ":"
  end

let warn_chdir_pwd = CWarnings.create ~name:"change-dir-pwd-deprecated" ~category:Deprecation.Version.v8_20
    (fun () -> strbrk "Command \"Cd\" as a synonym of \"Pwd\" is deprecated." ++ spc () ++
               strbrk "Use \"Pwd\" instead.")

}

GRAMMAR EXTEND Gram
  GLOBAL: vernac_control quoted_attributes attribute_list gallina_ext noedit_mode subprf subprf_with_selector;
  vernac_control: FIRST
    [ [ IDENT "Time"; c = vernac_control ->
        { add_control_flag ~loc ~flag:ControlTime c }
      | IDENT "Instructions"; c = vernac_control ->
        { add_control_flag ~loc ~flag:ControlInstructions c }
      | IDENT "Redirect"; s = ne_string; c = vernac_control ->
        { add_control_flag ~loc ~flag:(ControlRedirect s) c }
      | IDENT "Timeout"; n = natural; c = vernac_control ->
        { add_control_flag ~loc ~flag:(ControlTimeout n) c }
      | IDENT "Fail"; c = vernac_control ->
        { add_control_flag ~loc ~flag:ControlFail c }
      | IDENT "Succeed"; c = vernac_control ->
        { add_control_flag ~loc ~flag:ControlSucceed c }
      | v = decorated_vernac ->
        { let (attrs, expr) = v in CAst.make ~loc { control = []; attrs; expr = expr } } ]
    ]
  ;
  decorated_vernac:
    [ [ a = quoted_attributes ; fv = vernac ->
        { let (f, v) = fv in (List.append a f, v) } ] ]
  ;
  quoted_attributes:
    [ [ l = LIST0 [ "#[" ; a = attribute_list ; "]" -> { a } ] -> { List.flatten l } ]
    ]
  ;
  attribute_list:
    [ [ a = LIST1 attribute SEP "," -> { a } ]
    ]
  ;
  attribute:
    [ [ k = ident ; v = attr_value -> { CAst.make ~loc (Names.Id.to_string k, v) }
      (* Required because "ident" is declared a keyword when loading Ltac. *)
      | IDENT "using" ; v = attr_value -> { CAst.make ~loc ("using", v) } ]
    ]
  ;
  attr_value:
    [ [ "=" ; v = string -> { VernacFlagLeaf (FlagString v) }
      | "=" ; v = IDENT -> { VernacFlagLeaf (FlagIdent v) }
      | "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
      | -> { VernacFlagEmpty } ]
    ]
  ;
  legacy_attr:
    [ [ IDENT "Local" ->
        { CAst.make ~loc ("local", VernacFlagEmpty) }
      | IDENT "Global" ->
        { CAst.make ~loc ("global", VernacFlagEmpty) }
      | IDENT "Polymorphic" ->
        { Attributes.vernac_polymorphic_flag (Some loc) }
      | IDENT "Monomorphic" ->
        { Attributes.vernac_monomorphic_flag (Some loc) }
      | IDENT "Cumulative" ->
        { CAst.make ~loc ("universes", VernacFlagList [CAst.make ~loc ("cumulative", VernacFlagEmpty)]) }
      | IDENT "NonCumulative" ->
        { CAst.make ~loc ("universes", VernacFlagList [CAst.make ~loc ("cumulative", VernacFlagLeaf (FlagIdent "no"))]) }
      | IDENT "Private" ->
        { CAst.make ~loc ("private", VernacFlagList [CAst.make ~loc ("matching", VernacFlagEmpty)]) }
      | IDENT "Program" ->
        { CAst.make ~loc ("program", VernacFlagEmpty) }
      ] ]
  ;
  vernac:
    [ [ attrs = LIST0 legacy_attr; v = vernac_aux -> { (attrs, v) } ] ]
  ;
  vernac_aux:
    (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
    (* "." is still in the stream and discard_to_dot works correctly         *)
    [ [ g = gallina; "." -> { VernacSynPure g }
      | g = gallina_ext; "." -> { g }
      | c = command; "." -> { c }
      | c = syntax; "." -> { c }
    ] ]
  ;
  vernac_aux: LAST
    [ [ prfcom = command_entry -> { prfcom } ] ]
  ;

  noedit_mode: [ [ c = query_command -> { VernacSynPure (c None) } ] ]
  ;

  subprf:
  [ [ s = BULLET -> { VernacBullet (make_bullet s) }
    | "}" -> { VernacEndSubproof }
    ] ]
  ;
  subprf_with_selector:
  [ [ "{" -> { fun g -> VernacSubproof g }
    (* query_command needs to be here to factor with VernacSubproof *)
    | c = query_command -> { c }
    ] ]
  ;

END

{

let warn_plural_command =
  CWarnings.create ~name:"plural-command" ~category:CWarnings.CoreCategories.pedantic ~default:CWarnings.Disabled
         (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd))

let test_plural_form loc kwd = function
  | [(_,([_],_))] ->
     warn_plural_command ~loc kwd
  | _ -> ()

let test_plural_form_types loc kwd = function
  | [([_],_)] ->
     warn_plural_command ~loc kwd
  | _ -> ()

let test_plural_form_rules loc kwd = function
  | [_] ->
     warn_plural_command ~loc kwd
  | _ -> ()

let lname_of_lident : lident -> lname =
  CAst.map (fun s -> Name s)

let name_of_ident_decl : ident_decl -> name_decl =
  on_fst lname_of_lident

let test_variance_ident =
  let open Pcoq.Lookahead in
  to_entry "test_variance_ident" begin
    lk_kws ["=";"+";"*"] >> lk_ident
  end

let test_univ_decl =
  let open Pcoq.Lookahead in
  to_entry "test_univ_decl" (lk_ident_list >> lk_kw "|" >> lk_ident_list >> (lk_kw "+" <+> lk_empty) >> (lk_kw "|" <+> lk_kw "|}"))

let test_cumul_univ_decl =
  let open Pcoq.Lookahead in
  let lk_list_variance_ident = lk_list (lk_kw "+" <+> lk_kw "*" <+> lk_kw "=" <+> lk_ident) in
  to_entry "test_cumul_univ_decl" (lk_ident_list >> lk_kw "|" >> lk_list_variance_ident >> (lk_kw "+" <+> lk_empty) >> (lk_kw "|" <+> lk_kw "|}"))


}

(* Gallina declarations *)
GRAMMAR EXTEND Gram
  GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type of_type_inst
    record_field notation_declaration decl_notations fix_definition ident_decl univ_decl inductive_or_record_definition;

  gallina:
      (* Definition, Theorem, Variable, Axiom, ... *)
    [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr;
        l = LIST0
          [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr ->
          { (id,(bl,c)) } ] ->
          { VernacStartTheoremProof (thm, (id,(bl,c))::l) }
      | stre = assumption_token; nl = inline; bl = assum_list ->
          { VernacAssumption (stre, nl, bl) }
      | tk = assumptions_token; nl = inline; bl = assum_list ->
          { let (kwd,stre) = tk in
            test_plural_form loc kwd bl;
            VernacAssumption (stre, nl, bl) }
      | d = def_token; id = ident_decl; b = def_body ->
          { VernacDefinition (d, name_of_ident_decl id, b) }
      | IDENT "Symbol"; bl = assum_list ->
          { VernacSymbol bl }
      | IDENT "Symbols"; bl = assum_list ->
          { test_plural_form loc "Symbols" bl;
            VernacSymbol bl }
      | IDENT "Let"; id = ident_decl; b = def_body ->
          { VernacDefinition ((DoDischarge, Let), name_of_ident_decl id, b) }
      (* Gallina inductive declarations *)
      | f = finite_token; ind = inductive_or_record_definition ->
          { VernacInductive (f, [ind]) }
      | f = inductive_token; indl = LIST1 inductive_or_record_definition SEP "with" ->
          { VernacInductive (f, indl) }
      | "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
          { VernacFixpoint (NoDischarge, recs) }
      | IDENT "Let"; "Fixpoint"; recs = LIST1 fix_definition SEP "with" ->
          { VernacFixpoint (DoDischarge, recs) }
      | "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
          { VernacCoFixpoint (NoDischarge, corecs) }
      | IDENT "Let"; "CoFixpoint"; corecs = LIST1 cofix_definition SEP "with" ->
          { VernacCoFixpoint (DoDischarge, corecs) }
      | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
      | IDENT "Scheme"; IDENT "Equality"; IDENT "for" ; id = smart_global ->
          { VernacSchemeEquality (SchemeEquality,id) }
      | IDENT "Scheme"; IDENT "Boolean"; IDENT "Equality"; IDENT "for" ; id = smart_global ->
          { VernacSchemeEquality (SchemeBooleanEquality,id) }
      | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
              l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
      | IDENT "Register"; g = global; "as"; quid = qualid ->
          { VernacRegister(g, RegisterCoqlib quid) }
      | IDENT "Register"; IDENT "Scheme"; g = global; "as"; qid = qualid; IDENT "for"; g' = global ->
        { VernacRegister(g, RegisterScheme {inductive = g'; scheme_kind = qid}) }
      | IDENT "Register"; IDENT "Inline"; g = global ->
          { VernacRegister(g, RegisterInline) }
      | IDENT "Primitive"; id = ident_decl; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token ->
          { VernacPrimitive(id, r, typopt) }
      | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
      | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
      | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
      | IDENT "Rewrite"; IDENT "Rule"; id = identref; ":="; OPT"|"; rules = LIST1 rewrite_rule SEP "|" ->
          { VernacAddRewRule (id, rules) }
      | IDENT "Rewrite"; IDENT "Rules"; id = identref; ":="; OPT"|"; rules = LIST1 rewrite_rule SEP "|" ->
          { test_plural_form_rules loc "Rewrite Rules" rules;
            VernacAddRewRule (id, rules) }
  ] ]
  ;
  register_token:
    [ [ test_hash_ident; "#"; r = IDENT -> { CPrimitives.parse_op_or_type ~loc r } ] ]
  ;
  thm_token:
    [ [ "Theorem" -> { Theorem }
      | IDENT "Lemma" -> { Lemma }
      | IDENT "Fact" -> { Fact }
      | IDENT "Remark" -> { Remark }
      | IDENT "Corollary" -> { Corollary }
      | IDENT "Proposition" -> { Proposition }
      | IDENT "Property" -> { Property } ] ]
  ;
  def_token:
    [ [ "Definition" -> { (NoDischarge,Definition) }
      | IDENT "Example" -> { (NoDischarge,Example) }
      | IDENT "SubClass" -> { (NoDischarge,SubClass) } ] ]
  ;
  assumption_token:
    [ [ "Hypothesis" -> { (DoDischarge, Logical) }
      | "Variable" -> { (DoDischarge, Definitional) }
      | "Axiom" -> { (NoDischarge, Logical) }
      | "Parameter" -> { (NoDischarge, Definitional) }
      | IDENT "Conjecture" -> { (NoDischarge, Conjectural) } ] ]
  ;
  assumptions_token:
    [ [ IDENT "Hypotheses" -> { ("Hypotheses", (DoDischarge, Logical)) }
      | IDENT "Variables" -> { ("Variables", (DoDischarge, Definitional)) }
      | IDENT "Axioms" -> { ("Axioms", (NoDischarge, Logical)) }
      | IDENT "Parameters" -> { ("Parameters", (NoDischarge, Definitional)) }
      | IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ]
  ;
  inline:
    [ [ IDENT "Inline"; "("; i = natural; ")" -> { InlineAt i }
      | IDENT "Inline" -> { DefaultInline }
      | -> { NoInline } ] ]
  ;
  univ_constraint:
    [ [ l = universe_name; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ];
        r = universe_name -> { (l, ord, r) } ] ]
  ;
  univ_decl_constraints:
    [ [ "|"; l' = LIST0 univ_constraint SEP ",";
        ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) }
      | ext = [ "}" -> { true } | bar_cbrace -> { false } ] -> { ([], ext) } ] ]
  ;
  univ_decl:
    [ [ "@{" ; test_univ_decl; l0 = LIST0 identref; "|";  l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
         cs = univ_decl_constraints
         ->
         { let open UState in
         { univdecl_qualities = l0;
           univdecl_extensible_qualities = false;
           univdecl_instance = l;
           univdecl_extensible_instance = ext;
           univdecl_constraints = fst cs;
           univdecl_extensible_constraints = snd cs } }
    | "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
         cs = univ_decl_constraints
         ->
         { let open UState in
         { univdecl_qualities = [];
           univdecl_extensible_qualities = false;
           univdecl_instance = l;
           univdecl_extensible_instance = ext;
           univdecl_constraints = fst cs;
           univdecl_extensible_constraints = snd cs } }
    ] ]
  ;
  variance:
    [ [ "+" -> { UVars.Variance.Covariant }
      | "=" -> { UVars.Variance.Invariant }
      | "*" -> { UVars.Variance.Irrelevant }
    ] ]
  ;
  variance_identref:
    [ [ id = identref -> { (id, None) }
      | test_variance_ident; v = variance; id = identref -> { (id, Some v) }
        (* We need this test to help the parser avoid the conflict
           between "+" before ident (covariance) and trailing "+" (extra univs allowed) *)
    ] ]
  ;
  cumul_univ_decl:
    [ [ "@{" ; test_cumul_univ_decl; l0 = LIST0 identref; "|";
        l = LIST0 variance_identref; ext = [ "+" -> { true } | -> { false } ];
         cs = univ_decl_constraints
         ->
         { let open UState in
         { univdecl_qualities = l0;
           univdecl_extensible_qualities = false;
           univdecl_instance = l;
           univdecl_extensible_instance = ext;
           univdecl_constraints = fst cs;
           univdecl_extensible_constraints = snd cs } }

       | "@{" ; l = LIST0 variance_identref; ext = [ "+" -> { true } | -> { false } ];
         cs = univ_decl_constraints
         ->
         { let open UState in
         { univdecl_qualities = [];
           univdecl_extensible_qualities = false;
           univdecl_instance = l;
           univdecl_extensible_instance = ext;
           univdecl_constraints = fst cs;
           univdecl_extensible_constraints = snd cs } }
    ] ]
  ;
  ident_decl:
    [ [ i = identref; l = OPT univ_decl -> { (i, l) }
  ] ]
  ;
  cumul_ident_decl:
    [ [ i = identref; l = OPT cumul_univ_decl -> { (i, l) }
  ] ]
  ;
  inductive_token:
    [ [ IDENT "Inductive" -> { Inductive_kw }
      | IDENT "CoInductive" -> { CoInductive } ] ]
  ;
  finite_token:
    [ [ IDENT "Variant" -> { Variant }
      | IDENT "Record" -> { Record }
      | IDENT "Structure" -> { Structure }
      | IDENT "Class" -> { Class true } ] ]
  ;
  (* Simple definitions *)
  def_body:
    [ [ bl = binders; ":="; red = reduce; c = lconstr ->
        { match c.CAst.v with
          | CCast(c, Some C.DEFAULTcast, t) -> DefineBody (bl, red, c, Some t)
          | _ -> DefineBody (bl, red, c, None) }
    | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
        { DefineBody (bl, red, c, Some t) }
    | bl = binders; ":"; t = lconstr ->
        { ProveBody (bl, t) } ] ]
  ;
  reduce:
    [ [ IDENT "Eval"; r = red_expr; "in" -> { Some r }
      | -> { None } ] ]
  ;
  notation_declaration:
    [ [ ntn = lstring; ":="; c = constr;
        modl = syntax_modifiers;
        scopt = OPT [ ":"; sc = IDENT -> { sc } ] ->
      { { ntn_decl_string = ntn; ntn_decl_interp = c;
          ntn_decl_scope = scopt;
          ntn_decl_modifiers = modl;
      } } ] ]
  ;
  decl_sep:
    [ [ IDENT "and" -> { () } ] ]
  ;
  decl_notations:
    [ [ "where"; l = LIST1 notation_declaration SEP decl_sep -> { l }
    | -> { [] } ] ]
  ;
  (* Inductives and records *)
  opt_constructors_or_fields:
    [ [ ":="; lc = constructors_or_record -> { lc }
      | ":=" -> { Constructors [] }
      | -> { RecordDecl (None, [], None) } ] ]
  ;
  inductive_or_record_definition:
    [ [ oc = opt_coercion; id = cumul_ident_decl; indpar = binders;
        extrapar = OPT [ "|"; p = binders -> { p } ];
        c = OPT [ ":"; c = lconstr -> { c } ];
        lc=opt_constructors_or_fields; ntn = decl_notations ->
           { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
  ;
  constructors_or_record:
    [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
      | attr = quoted_attributes ; id = identref ; c = constructor_type;
        "|"; l = LIST1 constructor SEP "|" ->
          { Constructors ((c attr id)::l) }
      | attr = quoted_attributes ; id = identref ; c = constructor_type ->
          { Constructors [ c attr id ] }
      | attr = quoted_attributes ;
        cstr = identref; "{"; fs = record_fields; "}"; id = default_inhabitant_ident ->
          { let () = unsupported_attributes attr in
            RecordDecl (Some cstr,fs,id) }
      | "{";fs = record_fields; "}"; id = default_inhabitant_ident -> { RecordDecl (None,fs,id) } ] ]
  ;
  default_inhabitant_ident:
    [ [ "as"; id = identref -> { Some id }
      | -> { None } ] ]
  ;
(*
  csort:
    [ [ s = sort -> CSort (loc,s) ] ]
  ;
*)
  opt_coercion:
    [ [ ">" -> { AddCoercion }
      |  -> { NoCoercion } ] ]
  ;
  (* (co)-fixpoints *)
  fix_definition:
    [ [ id_decl = ident_decl;
        bl = binders_fixannot;
        rtype = type_cstr;
        body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notations ->
          { let binders, rec_order = bl in
            {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
          } ] ]
  ;
  cofix_definition:
    [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
        body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notations ->
        { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
        } ]]
  ;
  (* Rewrite Rules *)
  rw_pattern:
    [ [ p = lconstr -> { p } ] ];
  rewrite_rule:
    [ [ u = OPT [ u = univ_decl; "|-" -> { u }];
        lhs = rw_pattern; "=>" ; rhs = lconstr ->
        { (u, lhs, rhs)
        } ] ]
  ;
  (* Inductive schemes *)
  scheme:
    [ [ kind = scheme_kind -> { (None,kind) }
      | id = identref; ":="; kind = scheme_kind -> { (Some id,kind) } ] ]
  ;
  scheme_kind:
    [ [sch_type = scheme_type; "for"; sch_qualid = smart_global; IDENT "Sort"; sch_sort = sort_family
      -> { {sch_type; sch_qualid; sch_sort} }
    ] ]
  ;
  scheme_type:
    [ [ IDENT "Induction" -> { SchemeInduction }
      | IDENT "Minimality" -> { SchemeMinimality }
      | IDENT "Elimination" -> { SchemeElimination }
      | IDENT "Case" -> { SchemeCase }
    ] ]
  ;
  (* Various Binders *)
(*
  (* ... without coercions *)
  binder_nodef:
    [ [ b = binder_let ->
      (match b with
          CLocalAssum(l,ty) -> (l,ty)
        | CLocalDef _ ->
            user_err ~loc
              (Pp.str"defined binder not allowed here.")) ] ]
  ;
*)
  (* ... with coercions *)
  record_field:
  [ [ rfu_attrs = quoted_attributes ;
      bd = record_binder; rfu_priority = OPT [ "|"; n = natural -> { n } ];
      rfu_notation = decl_notations -> {
      let (rfu_coercion, rfu_instance), rf_decl = bd in
      rf_decl,
      { rfu_attrs ; rfu_coercion ; rfu_instance ; rfu_priority ;
        rfu_notation } } ] ]
  ;
  record_fields:
    [ [ f = record_field; ";"; fs = record_fields -> { f :: fs }
      | f = record_field -> { [f] }
      | -> { [] }
    ] ]
  ;
  field_body:
    [ [ l = binders; oc = of_type_inst;
         t = lconstr -> { fun id -> (oc,AssumExpr (id,l,t)) }
      | l = binders; oc = of_type_inst;
         t = lconstr; ":="; b = lconstr -> { fun id ->
           (oc,DefExpr (id,l,b,Some t)) }
      | l = binders; ":="; b = lconstr -> { fun id ->
        (* Why are we dropping cast info here? *)
         match b.CAst.v with
         | CCast(b', _, t) ->
             ((NoCoercion,NoInstance),DefExpr(id,l,b',Some t))
         | _ ->
             ((NoCoercion,NoInstance),DefExpr(id,l,b,None)) } ] ]
  ;
  record_binder:
    [ [ id = name -> { ((NoCoercion,NoInstance),AssumExpr(id, [], CAst.make ~loc @@ CHole (None))) }
      | id = name; f = field_body -> { f id } ] ]
  ;
  assum_list:
    [ [ bl = LIST1 assum_coe -> { bl } | b = assumpt -> { [b] } ] ]
  ;
  assum_coe:
    [ [ "("; a = assumpt; ")" -> { a } ] ]
  ;
  assumpt:
    [ [ idl = LIST1 ident_decl; oc = of_type; c = lconstr ->
        { (oc,(idl,c)) } ] ]
  ;

  constructor_type:
    [[ l = binders;
      t= [ coe = of_type_inst; c = lconstr ->
                    { fun l attr id -> ((attr, fst coe, snd coe),(id,mkProdCN ~loc l c)) }
            |  ->
                 { fun l attr id -> ((attr,NoCoercion,NoInstance),(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None)))) } ]
         -> { t l }
     ]]
;

  constructor:
    [ [ attr = quoted_attributes ;
        id = identref; c=constructor_type -> { c attr id } ] ]
  ;
  of_type:
    [ [   ":>" -> { AddCoercion }
        | ":"; ">" -> { AddCoercion }
        | ":" -> { NoCoercion } ] ]
  ;
  of_type_inst:
    [ [   ":>" -> { (AddCoercion, BackInstanceWarning) (* replace with NoInstance at end of deprecation phase *) }
        | ":"; ">" -> { (AddCoercion, BackInstanceWarning) (* replace with NoInstance at end of deprecation phase *) }
        | "::" -> { (NoCoercion, BackInstance) }
        | "::>" -> { (AddCoercion, BackInstance) }
        | ":" -> { (NoCoercion, NoInstance) } ] ]
  ;
END

{

let test_only_starredidentrefs =
  let open Pcoq.Lookahead in
  to_entry "test_only_starredidentrefs" begin
    lk_list (lk_ident <+> lk_kws ["Type"; "*"]) >> (lk_kws [".";")"])
  end

let starredidentreflist_to_expr l =
  match l with
  | [] -> SsEmpty
  | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x

let warn_deprecated_include_type =
  CWarnings.create ~name:"deprecated-include-type" ~category:Deprecation.Version.v8_3
         (fun () -> strbrk "Include Type is deprecated; use Include instead")

let warn_deprecated_as_ident_kind =
  CWarnings.create ~name:"deprecated-as-ident-kind" ~category:Deprecation.Version.v8_14
         (fun () -> strbrk "grammar kind \"as ident\" no longer accepts \"_\"; use \"as name\" instead to accept \"_\", too, or silence the warning if you actually intended to accept only identifiers.")

}

(* Modules and Sections *)
GRAMMAR EXTEND Gram
  GLOBAL: gallina_ext module_expr module_type section_subset_expr;

  gallina_ext:
    [ [ (* Interactive module declaration *)
        IDENT "Module"; export = export_token; id = identref;
        bl = LIST0 module_binder; sign = of_module_type;
        body = is_module_expr ->
          { VernacSynterp (VernacDefineModule (export, id, bl, sign, body)) }
      | IDENT "Module"; "Type"; id = identref;
        bl = LIST0 module_binder; sign = check_module_types;
        body = is_module_type ->
          { VernacSynterp (VernacDeclareModuleType (id, bl, sign, body)) }
      | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
        bl = LIST0 module_binder; ":"; mty = module_type_inl ->
          { VernacSynterp (VernacDeclareModule (export, id, bl, mty)) }
      (* Section beginning *)
      | IDENT "Section"; id = identref -> { VernacSynterp (VernacBeginSection id) }

      (* This end a Section a Module or a Module Type *)
      | IDENT "End"; id = identref -> { VernacSynterp (VernacEndSegment id) }

      (* Naming a set of section hyps *)
      | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr ->
          { VernacSynPure (VernacNameSectionHypSet (id, expr)) }

      (* Requiring an external file *)
      | IDENT "From" ; ns = global ;
        IDENT "Extra"; IDENT "Dependency"; f = ne_string ;
        id = OPT [ "as"; id = IDENT -> { id } ] ->
          { VernacSynterp (VernacExtraDependency (ns, f, Option.map Id.of_string id)) }

      (* Requiring an already compiled module *)
      | IDENT "Require"; export = export_token; qidl = LIST1 filtered_import ->
          { VernacSynterp (VernacRequire (None, export, qidl)) }
      | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token
        ; qidl = LIST1 filtered_import ->
        { VernacSynterp (VernacRequire (Some ns, export, qidl)) }
      | IDENT "Import"; cats = OPT import_categories; qidl = LIST1 filtered_import ->
        { VernacSynterp (VernacImport ((Import,cats),qidl)) }
      | IDENT "Export"; cats = OPT import_categories; qidl = LIST1 filtered_import ->
        { VernacSynterp (VernacImport ((Export,cats),qidl)) }
      | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_type ->
          { VernacSynterp (VernacInclude(e::l)) }
      | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
         { warn_deprecated_include_type ~loc ();
        VernacSynterp (VernacInclude(e::l)) } ] ]
  ;
  import_categories:
  [ [ negative = OPT "-"; "("; cats = LIST1 qualid SEP ","; ")" ->
      { let cats = List.map (fun cat -> CAst.make ?loc:cat.CAst.loc (Libnames.string_of_qualid cat)) cats in
        { negative=Option.has_some negative; import_cats = cats } }
  ] ]
  ;
  filtered_import:
    [ [ m = global -> { (m, ImportAll) }
      | m = global; "("; ns = LIST1 one_import_filter_name SEP ","; ")" -> { (m, ImportNames ns) } ] ]
  ;
  one_import_filter_name:
    [ [ n = global; etc = OPT [ "("; ".."; ")" -> { () } ] -> { n, Option.has_some etc } ] ]
  ;
  export_token:
    [ [ IDENT "Import"; cats = OPT import_categories -> { Some (Import,cats) }
      | IDENT "Export"; cats = OPT import_categories -> { Some (Export,cats) }
      |  -> { None } ] ]
  ;
  ext_module_type:
    [ [ "<+"; mty = module_type_inl -> { mty } ] ]
  ;
  ext_module_expr:
    [ [ "<+"; mexpr = module_expr_inl -> { mexpr } ] ]
  ;
  check_module_type:
    [ [ "<:"; mty = module_type_inl -> { mty } ] ]
  ;
  check_module_types:
    [ [ mtys = LIST0 check_module_type -> { mtys } ] ]
  ;
  of_module_type:
    [ [ ":"; mty = module_type_inl -> { Enforce mty }
      | mtys = check_module_types -> { Check mtys } ] ]
  ;
  is_module_type:
    [ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> { (mty::l) }
      | -> { [] } ] ]
  ;
  is_module_expr:
    [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> { (mexpr::l) }
      | -> { [] } ] ]
  ;
  functor_app_annot:
    [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = natural; "]" ->
        { InlineAt i }
      | "["; IDENT "no"; IDENT "inline"; "]" -> { NoInline }
      | -> { DefaultInline }
      ] ]
  ;
  module_expr_inl:
    [ [ "!"; me = module_expr -> { (me,NoInline) }
      | me = module_expr; a = functor_app_annot -> { (me,a) } ] ]
  ;
  module_type_inl:
    [ [ "!"; me = module_type -> { (me,NoInline) }
      | me = module_type; a = functor_app_annot -> { (me,a) } ] ]
  ;
  (* Module binder  *)
  module_binder:
    [ [ "("; export = export_token; idl = LIST1 identref; ":";
         mty = module_type_inl; ")" -> { (export,idl,mty) } ] ]
  ;
  (* Module expressions *)
  module_expr:
    [ [ me = module_expr_atom -> { CAst.make ~loc @@ CMident me }
      | me1 = module_expr; me2 = module_expr_atom -> { CAst.make ~loc @@ CMapply (me1,me2) }
      ] ]
  ;
  module_expr_atom:
    [ [ qid = qualid -> { qid } | "("; me = module_expr_atom; ")" -> { me } ] ]
  ;
  with_declaration:
    [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr ->
          { CWith_Definition (fqid,udecl,c) }
      | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid ->
          { CWith_Module (fqid,qid) }
      ] ]
  ;
  module_type:
    [ [ qid = qualid -> { CAst.make ~loc @@ CMident qid }
      | "("; mt = module_type; ")" -> { mt }
      | mty = module_type; me = module_expr_atom ->
          { CAst.make ~loc @@ CMapply (mty,me) }
      | mty = module_type; "with"; decl = with_declaration ->
          { CAst.make ~loc @@ CMwith (mty,decl) }
      ] ]
  ;
  (* Proof using *)
  section_subset_expr:
    [ [ test_only_starredidentrefs; l = LIST0 starredidentref ->
          { starredidentreflist_to_expr l }
      | e = ssexpr -> { e } ]]
  ;
  starredidentref:
    [ [ i = identref -> { SsSingl i }
      | i = identref; "*" -> { SsFwdClose(SsSingl i) }
      | "Type" -> { SsType }
      | "Type"; "*" -> { SsFwdClose SsType } ]]
  ;
  ssexpr:
    [ "35"
      [ "-"; e = ssexpr -> { SsCompl e } ]
    | "50"
      [ e1 = ssexpr; "-"; e2 = ssexpr-> { SsSubstr(e1,e2) }
      | e1 = ssexpr; "+"; e2 = ssexpr-> { SsUnion(e1,e2) } ]
    | "0"
      [ i = starredidentref -> { i }
      | "()" -> { SsEmpty }
      | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"->
          { starredidentreflist_to_expr l }
      | "("; test_only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" ->
          { SsFwdClose(starredidentreflist_to_expr l) }
      | "("; e = ssexpr; ")"-> { e }
      | "("; e = ssexpr; ")"; "*" -> { SsFwdClose e } ] ]
  ;
END

(* Extensions: implicits, coercions, etc. *)
GRAMMAR EXTEND Gram
  GLOBAL: gallina_ext hint_info scope_delimiter;

  gallina_ext: TOP
    [ [ (* Transparent and Opaque *)
        IDENT "Transparent"; o = OPT [ "!" -> {()} ]; l = LIST1 smart_global ->
          { VernacSynPure (VernacSetOpacity ((Conv_oracle.transparent, l), o <> None)) }
      | IDENT "Opaque"; o = OPT [ "!" -> {()} ]; l = LIST1 smart_global ->
          { VernacSynPure (VernacSetOpacity ((Conv_oracle.Opaque, l), o <> None)) }
      | IDENT "Strategy"; l =
          LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> { (v,q) } ] ->
            { VernacSynPure (VernacSetStrategy l) }
      (* Canonical structure *)
      | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] ->
          { match ud with
           | None ->
             VernacSynPure (VernacCanonical CAst.(make ?loc:qid.CAst.loc @@ AN qid))
           | Some (u,d) ->
             let s = coerce_reference_to_id qid in
             VernacSynPure (VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d)) }
      | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; ntn = by_notation ->
          { VernacSynPure (VernacCanonical CAst.(make ~loc @@ ByNotation ntn)) }

      (* Coercions *)
      | IDENT "Coercion"; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { u, d } ] ->
          { match ud with Some (u, d) -> let s = coerce_reference_to_id qid in
          VernacSynPure (VernacDefinition ((NoDischarge,Coercion),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d))
          | None -> VernacSynPure (VernacCoercion (CAst.make ~loc @@ AN qid, None)) }
      | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
         s = coercion_class; ">->"; t = coercion_class ->
           { VernacSynPure (VernacIdentityCoercion (f, s, t)) }
      | IDENT "Coercion"; qid = global; ":"; s = coercion_class; ">->";
         t = coercion_class ->
          { VernacSynPure (VernacCoercion (CAst.make ~loc @@ AN qid, Some(s, t))) }
      | IDENT "Coercion"; ntn = by_notation; ":"; s = coercion_class; ">->";
         t = coercion_class ->
          { VernacSynPure (VernacCoercion (CAst.make ~loc @@ ByNotation ntn, Some (s, t))) }

      | IDENT "Context"; c = LIST1 binder ->
          { VernacSynPure (VernacContext (List.flatten c)) }

      | IDENT "Instance"; namesup = instance_name; ":";
         t = term LEVEL "200";
         info = hint_info ;
         props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
             ":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
           { VernacSynPure (VernacInstance (fst namesup,snd namesup,t,props,info)) }

      | IDENT "Existing"; IDENT "Instance"; id = global;
          info = hint_info ->
          { VernacSynPure (VernacExistingInstance [id, info]) }

      | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
        pri = OPT [ "|"; i = natural -> { i } ] ->
         { let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in
         let insts = List.map (fun i -> (i, info)) ids in
          VernacSynPure (VernacExistingInstance insts) }

      | IDENT "Existing"; IDENT "Class"; is = global -> { VernacSynPure (VernacExistingClass is) }

      (* Arguments *)
      | IDENT "Arguments"; qid = smart_global;
        args = LIST0 arg_specs;
        more_implicits = OPT
          [ ","; impl = LIST1
            [ impl = LIST0 implicits_alt -> { List.flatten impl } ]
            SEP "," -> { impl }
          ];
        mods = OPT [ ":"; l = LIST1 args_modifier SEP "," -> { l } ] ->
         { let mods = match mods with None -> [] | Some l -> List.flatten l in
         let more_implicits = Option.default [] more_implicits in
         VernacSynPure (VernacArguments (qid, List.flatten args, more_implicits, mods)) }

      | IDENT "Implicit"; "Type"; bl = reserv_list ->
           { VernacSynPure (VernacReserve bl) }

      | IDENT "Implicit"; IDENT "Types"; bl = reserv_list ->
          { test_plural_form_types loc "Implicit Types" bl;
           VernacSynPure (VernacReserve bl) }

      | IDENT "Generalizable";
           gen = [IDENT "All"; IDENT "Variables" -> { Some [] }
             | IDENT "No"; IDENT "Variables" -> { None }
             | ["Variable" -> { () } | IDENT "Variables" -> { () } ];
                  idl = LIST1 identref -> { Some idl } ] ->
             { VernacSynPure (VernacGeneralizable gen) } ] ]
  ;
  args_modifier:
    [ [ IDENT "simpl"; IDENT "nomatch" -> { [`ReductionDontExposeCase] }
      | IDENT "simpl"; IDENT "never" -> { [`ReductionNeverUnfold] }
      | IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] }
      | IDENT "clear"; IDENT "implicits" -> { [`ClearImplicits] }
      | IDENT "clear"; IDENT "scopes" -> { [`ClearScopes] }
      | IDENT "clear"; IDENT "bidirectionality"; IDENT "hint" -> { [`ClearBidiHint] }
      | IDENT "rename" -> { [`Rename] }
      | IDENT "assert" -> { [`Assert] }
      | IDENT "extra"; IDENT "scopes" -> { [`ExtraScopes] }
      | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
          { [`ClearImplicits; `ClearScopes] }
      | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
          { [`ClearImplicits; `ClearScopes] }
      ] ]
  ;
  scope_delimiter:
    [ [ "%"; key = IDENT -> { DelimUnboundedScope, key }
      | "%_"; key = IDENT -> { DelimOnlyTmpScope, key } ] ]
  ;
  argument_spec: [
       [ b = OPT "!"; id = name ; s = LIST0 scope_delimiter ->
       { id.CAst.v, not (Option.is_empty b), List.map (fun x -> CAst.make ~loc x) s }
    ]
  ];
  (* List of arguments implicit status, scope, modifiers *)
  arg_specs: [
    [ item = argument_spec ->
      { let name, recarg_like, notation_scope = item in
      [RealArg { name=name; recarg_like=recarg_like;
             notation_scope=notation_scope;
             implicit_status = Explicit}] }
    | "/" -> { [VolatileArg] }
    | "&" -> { [BidiArg] }
    | "("; items = LIST1 argument_spec; ")"; scl = LIST0 scope_delimiter ->
       { let scl = List.map (CAst.make ~loc) scl in
       List.map (fun (name,recarg_like,notation_scope) ->
           RealArg { name=name; recarg_like=recarg_like;
                 notation_scope = notation_scope @ scl;
                 implicit_status = Explicit}) items }
    | "["; items = LIST1 argument_spec; "]"; scl = LIST0 scope_delimiter ->
       { let scl = List.map (CAst.make ~loc) scl in
       List.map (fun (name,recarg_like,notation_scope) ->
           RealArg { name=name; recarg_like=recarg_like;
                 notation_scope = notation_scope @ scl;
                 implicit_status = NonMaxImplicit}) items }
    | "{"; items = LIST1 argument_spec; "}"; scl = LIST0 scope_delimiter ->
       { let scl = List.map (CAst.make ~loc) scl in
       List.map (fun (name,recarg_like,notation_scope) ->
           RealArg { name=name; recarg_like=recarg_like;
                 notation_scope = notation_scope @ scl;
                 implicit_status = MaxImplicit}) items }
    ]
  ];
  (* Same as [arg_specs], but with only implicit status and names *)
  implicits_alt: [
    [ name = name -> { [(name.CAst.v, Explicit)] }
    | "["; items = LIST1 name; "]" ->
       { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items }
    | "{"; items = LIST1 name; "}" ->
       { List.map (fun name -> (name.CAst.v, MaxImplicit)) items }
    ]
  ];
  instance_name:
    [ [ name = ident_decl; bl = binders ->
          { (CAst.map (fun id -> Name id) (fst name), snd name), bl }
      | -> { ((CAst.make ~loc Anonymous), None), []  } ] ]
  ;
  hint_info:
    [ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
         { { Typeclasses.hint_priority = i; hint_pattern = pat } }
      | -> { { Typeclasses.hint_priority = None; hint_pattern = None } } ] ]
  ;
  reserv_list:
    [ [ bl = LIST1 reserv_tuple -> { bl } | b = simple_reserv -> { [b] } ] ]
  ;
  reserv_tuple:
    [ [ "("; a = simple_reserv; ")" -> { a } ] ]
  ;
  simple_reserv:
    [ [ idl = LIST1 identref; ":"; c = lconstr -> { (idl,c) } ] ]
  ;

END

{

(* Hack to parse "[ id" without dropping [ *)
let test_bracket_ident =
  let open Pcoq.Lookahead in
  to_entry "test_bracket_ident" begin
    lk_kw "[" >> lk_ident
  end

}

GRAMMAR EXTEND Gram
  GLOBAL: toplevel_selector goal_selector;
  range_selector:
    [ [ n = natural ; "-" ; m = natural -> { (n, m) }
      | n = natural -> { (n, n) } ] ]
  ;
  (* We unfold a range selectors list once so that we can make a special case
   * for a unique SelectNth selector. *)
  range_selector_or_nth:
    [ [ n = natural ; "-" ; m = natural;
        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
        { Goal_select.SelectList ((n, m) :: Option.default [] l) }
      | n = natural;
        l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] ->
        { let open Goal_select in
          Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ]
  ;
  goal_selector:
  [ [ l = range_selector_or_nth -> { l }
    | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ]
  ;
  toplevel_selector:
    [ [ sel = goal_selector; ":" -> { sel }
    |   "!"; ":" -> { Goal_select.SelectAlreadyFocused }
    |   IDENT "all"; ":" -> { Goal_select.SelectAll } ] ]
  ;
END

GRAMMAR EXTEND Gram
  GLOBAL: command query_command coercion_class gallina_ext search_query search_queries;

  gallina_ext: TOP
    [ [ IDENT "Export"; "Set"; table = setting_name; v = option_setting ->
        { VernacSynterp (VernacSetOption (true, table, v)) }
      | IDENT "Export"; IDENT "Unset"; table = setting_name ->
          { VernacSynterp (VernacSetOption (true, table, OptionUnset)) }
    ] ];

  command:
    [ [ IDENT "Comments"; l = LIST0 comment -> { VernacSynPure (VernacComments l) }

      | IDENT "Attributes"; attr = attribute_list ->
        { VernacSynPure (VernacAttributes attr) }

      (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
      | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
         t = term LEVEL "200";
         info = hint_info ->
           { VernacSynPure (VernacDeclareInstance (id, bl, t, info)) }

      (* Should be in syntax, but camlp5 would not factorize *)
      | IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
          { VernacSynPure (VernacDeclareScope sc) }

      (* System directory *)
      | IDENT "Pwd" -> { VernacSynterp (VernacChdir None) }
      | IDENT "Cd" -> { warn_chdir_pwd (); VernacSynterp (VernacChdir None) }
      | IDENT "Cd"; dir = ne_string -> { VernacSynterp (VernacChdir (Some dir)) }

      | IDENT "Load"; verbosely = [ IDENT "Verbose" -> { true } | -> { false } ];
        s = [ s = ne_string -> { s } | s = IDENT -> { s } ] ->
          { VernacSynterp (VernacLoad (verbosely, s)) }
      | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
          { VernacSynterp (VernacDeclareMLModule l) }

      | IDENT "Locate"; l = locatable -> { VernacSynPure (VernacLocate l) }

      (* Type-Checking *)
      | "Type"; c = lconstr -> { VernacSynPure (VernacGlobalCheck c) }

      (* Printing (careful factorization of entries) *)
      | IDENT "Print"; p = printable -> { VernacSynPure (VernacPrint p) }
      | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> { VernacSynPure (VernacPrint (PrintName (qid,l))) }
      | IDENT "Print"; IDENT "Module"; "Type"; qid = global ->
          { VernacSynPure (VernacPrint (PrintModuleType qid)) }
      | IDENT "Print"; IDENT "Module"; qid = global ->
          { VernacSynPure (VernacPrint (PrintModule qid)) }
      | IDENT "Print"; IDENT "Namespace" ; ns = dirpath ->
          { VernacSynPure (VernacPrint (PrintNamespace ns)) }
      | IDENT "Inspect"; n = natural -> { VernacSynPure (VernacPrint (PrintInspect n)) }

      (* For acting on parameter tables *)
      | "Set"; table = setting_name; v = option_setting ->
          { VernacSynterp (VernacSetOption (false, table, v)) }
      | IDENT "Unset"; table = setting_name ->
          { VernacSynterp (VernacSetOption (false, table, OptionUnset)) }

      | IDENT "Print"; IDENT "Table"; table = setting_name ->
          { VernacSynPure (VernacPrintOption table) }

      | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 table_value
        -> { VernacSynPure (VernacAddOption ([table;field], v)) }
      (* A global value below will be hidden by a field above! *)
      (* In fact, we give priority to secondary tables *)
      (* No syntax for tertiary tables due to conflict *)
      (* (but they are unused anyway) *)
      | IDENT "Add"; table = IDENT; v = LIST1 table_value ->
          { VernacSynPure (VernacAddOption ([table], v)) }

      | IDENT "Test"; table = setting_name; "for"; v = LIST1 table_value
        -> { VernacSynPure (VernacMemOption (table, v)) }
      | IDENT "Test"; table = setting_name ->
          { VernacSynPure (VernacPrintOption table) }

      | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 table_value
        -> { VernacSynPure (VernacRemoveOption ([table;field], v)) }
      | IDENT "Remove"; table = IDENT; v = LIST1 table_value ->
          { VernacSynPure (VernacRemoveOption ([table], v)) } ]]
  ;
  query_command:
    [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." ->
          { fun g -> VernacCheckMayEval (Some r, g, c) }
      | IDENT "Compute"; c = lconstr; "." ->
          { fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) }
      | IDENT "Check"; c = lconstr; "." ->
         { fun g -> VernacCheckMayEval (None, g, c) }
      (* Searching the environment *)
      | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." ->
         { fun g -> VernacPrint (PrintAbout (qid,l,g)) }
      | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
          { fun g -> VernacSearch (SearchPattern c,g, l) }
      | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
          { fun g -> VernacSearch (SearchRewrite c,g, l) }
      | IDENT "Search"; s = search_query; l = search_queries; "." ->
          { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) }
      ] ]
  ;
  printable:
    [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> { PrintName (qid,l) }
      | IDENT "All" -> { PrintFullContext }
      | IDENT "Section"; s = global -> { PrintSectionContext s }
      | IDENT "Grammar"; ents = LIST0 IDENT ->
          (* This should be in "syntax" section but is here for factorization*)
          { PrintGrammar ents }
      | IDENT "Custom"; IDENT "Grammar"; ent = IDENT ->
          (* Should also be in "syntax" section *)
          { PrintCustomGrammar ent }
      | IDENT "Keywords" ->
          { PrintKeywords }
      | IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir }
      | IDENT "Libraries" -> { PrintLibraries }

      | IDENT "Notation"; ntn = string ->
        { PrintNotation (Constrexpr.InConstrEntry, ntn) }
      | IDENT "Notation"; ntn = string; IDENT "in"; IDENT "custom"; ent = IDENT ->
        { PrintNotation (Constrexpr.InCustomEntry ent, ntn) }

      | IDENT "ML"; IDENT "Path" -> { PrintMLLoadPath }
      | IDENT "ML"; IDENT "Modules" -> { PrintMLModules }
      | IDENT "Debug"; IDENT "GC" -> { PrintDebugGC }
      | IDENT "Graph" -> { PrintGraph }
      | IDENT "Classes" -> {  PrintClasses }
      | IDENT "Typeclasses" -> { PrintTypeclasses }
      | IDENT "Instances"; qid = smart_global -> { PrintInstances qid }
      | IDENT "Coercions" -> { PrintCoercions }
      | IDENT "Coercion"; IDENT "Paths"; s = coercion_class; t = coercion_class ->
          { PrintCoercionPaths (s,t) }
      | IDENT "Canonical"; IDENT "Projections"; qids = LIST0 smart_global ->
          { PrintCanonicalConversions qids }
      | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags }
      | IDENT "Tables" -> { PrintTables }
      | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) }
      | IDENT "Hint" -> { PrintHintGoal }
      | IDENT "Hint"; qid = smart_global -> { PrintHint qid }
      | IDENT "Hint"; "*" -> { PrintHintDb }
      | IDENT "HintDb"; s = IDENT -> { PrintHintDbName s }
      | IDENT "Scopes" -> { PrintScopes }
      | IDENT "Scope"; s = IDENT -> { PrintScope s }
      | IDENT "Visibility"; s = OPT IDENT -> { PrintVisibility s }
      | IDENT "Implicit"; qid = smart_global -> { PrintImplicit qid }
      | b = [ IDENT "Sorted" -> { true } | -> { false } ]; IDENT "Universes";
        g = OPT printunivs_subgraph; fopt = OPT ne_string ->
        { PrintUniverses (b, g, fopt) }
      | IDENT "Assumptions"; qid = smart_global -> { PrintAssumptions (false, false, qid) }
      | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, false, qid) }
      | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) }
      | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, true, qid) }
      | IDENT "Strategy"; qid = smart_global -> { PrintStrategy (Some qid) }
      | IDENT "Strategies" -> { PrintStrategy None }
      | IDENT "Registered" -> { PrintRegistered }
      | IDENT "Registered"; IDENT "Schemes" -> { PrintRegisteredSchemes }
    ] ]
  ;
  printunivs_subgraph:
    [ [ IDENT "Subgraph"; "("; l = LIST0 reference; ")" -> { l } ] ]
  ;
  coercion_class:
    [ [ IDENT "Funclass" -> { FunClass }
      | IDENT "Sortclass" -> { SortClass }
      | qid = smart_global -> { RefClass qid } ] ]
  ;
  locatable:
    [ [ qid = smart_global -> { LocateAny qid }
      | IDENT "Term"; qid = smart_global -> { LocateTerm qid }
      | IDENT "File"; f = ne_string -> { LocateFile f }
      | IDENT "Library"; qid = global -> { LocateLibrary qid }
      | IDENT "Module"; qid = global -> { LocateModule qid } ] ]
  ;
  option_setting:
    [ [ -> { OptionSetTrue }
      | n  = integer   -> { OptionSetInt n }
      | s  = STRING    -> { OptionSetString s } ] ]
  ;
  table_value:
    [ [ id = global   -> { Goptions.QualidRefValue id }
      | s  = STRING   -> { Goptions.StringRefValue s } ] ]
  ;
  setting_name:
    [ [ fl = LIST1 [ x = IDENT -> { x } ] -> { fl } ]]
  ;
  ne_in_or_out_modules:
    [ [ IDENT "inside"; l = LIST1 global -> { SearchInside l }
      | "in"; l = LIST1 global -> { SearchInside l }
      | IDENT "outside"; l = LIST1 global -> { SearchOutside l } ] ]
  ;
  in_or_out_modules:
    [ [ m = ne_in_or_out_modules -> { m }
      | -> { SearchOutside [] } ] ]
  ;
  comment:
    [ [ c = constr -> { CommentConstr c }
      | s = STRING -> { CommentString s }
      | n = natural -> { CommentInt n } ] ]
  ;
  positive_search_mark:
    [ [ "-" -> { false } | -> { true } ] ]
  ;
  search_query:
    [ [ b = positive_search_mark; s = search_item -> { (b, SearchLiteral s) }
      | b = positive_search_mark; "["; l = LIST1 (LIST1 search_query) SEP "|"; "]" -> { (b, SearchDisjConj l) }
      ] ]
  ;
  search_item:
    [ [ test_id_colon; where = search_where; ":"; s = ne_string; sc = OPT scope_delimiter ->
            { SearchString (where,s,sc) }
      | IDENT "is"; ":"; kl = logical_kind ->
            { SearchKind kl }
      | s = ne_string; sc = OPT scope_delimiter ->
            { SearchString ((Anywhere,false),s,sc) }
      | test_id_colon; where = search_where; ":"; p = constr_pattern ->
            { SearchSubPattern (where,p) }
      | p = constr_pattern ->
            { SearchSubPattern ((Anywhere,false),p) }
      ] ]
  ;
  logical_kind:
    [ [ k = thm_token -> { IsProof k }
      | k = assumption_token -> { IsAssumption (snd k) }
      | k = IDENT "Context" -> { IsAssumption Context }
      | k = extended_def_token -> { IsDefinition k }
      | IDENT "Primitive" -> { IsPrimitive }
      | IDENT "Symbol" -> { IsSymbol } ] ]
  ;
  extended_def_token:
    [ [ k = def_token -> { snd k }
      | IDENT "Coercion" -> { Coercion }
      | IDENT "Fixpoint" -> { Fixpoint }
      | IDENT "CoFixpoint" -> { CoFixpoint }
      | IDENT "Instance" -> { Instance }
      | IDENT "Scheme" -> { Scheme }
      | IDENT "Canonical" -> { CanonicalStructure }
      | IDENT "Field" -> { StructureComponent }
      | IDENT "Method" -> { Method } ] ]
  ;
  search_where:
    [ [ IDENT "head" -> { Anywhere, true }
      | IDENT "hyp" -> { InHyp, false }
      | IDENT "concl" -> { InConcl, false }
      | IDENT "headhyp" -> { InHyp, true }
      | IDENT "headconcl" -> { InConcl, true } ] ]
  ;
  search_queries:
    [ [ m = ne_in_or_out_modules -> { ([],m) }
      | s = search_query; l = search_queries ->
        { let (sl,m) = l in (s::sl,m) }
      | -> { ([],SearchOutside []) }
      ] ]
  ;
  univ_name_list:
    [ [  "@{" ; l = LIST0 name; "}" -> { [],l } ] ]
  ;
END

GRAMMAR EXTEND Gram
  GLOBAL: command;

  command: TOP
    [ [
(* Resetting *)
        IDENT "Reset"; IDENT "Initial" -> { VernacSynPure (VernacResetInitial) }
      | IDENT "Reset"; id = identref -> { VernacSynPure (VernacResetName id) }
      | IDENT "Back" -> { VernacSynPure (VernacBack 1) }
      | IDENT "Back"; n = natural -> { VernacSynPure (VernacBack n) }

(* Tactic Debugger *)
      |	IDENT "Debug"; IDENT "On" ->
          { VernacSynterp (VernacSetOption (false, ["Ltac";"Debug"], OptionSetTrue)) }

      |	IDENT "Debug"; IDENT "Off" ->
          { VernacSynterp (VernacSetOption (false, ["Ltac";"Debug"], OptionUnset)) }

(* registration of a custom reduction *)

      | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":=";
         r = red_expr ->
           { VernacSynPure (VernacDeclareReduction (s,r)) }

(* factorized here, though relevant for syntax extensions *)

      | IDENT "Declare"; IDENT "Custom"; IDENT "Entry"; s = IDENT ->
           { VernacSynterp (VernacDeclareCustomEntry s) }

 ] ];
    END

(* Grammar extensions *)

GRAMMAR EXTEND Gram
  GLOBAL: syntax syntax_modifiers;

  syntax:
   [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT ->
         { VernacSynPure (VernacOpenCloseScope (true,sc)) }

     | IDENT "Close"; IDENT "Scope"; sc = IDENT ->
         { VernacSynPure (VernacOpenCloseScope (false,sc)) }

     | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
         { VernacSynPure(VernacDelimiters (sc, Some key)) }
     | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT ->
         { VernacSynPure(VernacDelimiters (sc, None)) }

     | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
       refl = LIST1 coercion_class -> { VernacSynPure (VernacBindScope (sc,refl)) }

     | IDENT "Infix"; ntn_decl = notation_declaration ->
         { VernacSynterp (VernacNotation (true,ntn_decl)) }
     | IDENT "Notation"; id = identref; idl = LIST0 ident;
         ":="; c = constr; modl = syntax_modifiers ->
           { VernacSynPure (VernacSyntacticDefinition (id,(idl,c), modl)) }
     | IDENT "Notation"; ntn_decl = notation_declaration ->
           { VernacSynterp (VernacNotation (false,ntn_decl)) }

     | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = syntax_modifiers ->
           { VernacSynterp (VernacReservedNotation (true,(s,l))) }
     | IDENT "Reserved"; IDENT "Notation"; s = ne_lstring; l = syntax_modifiers ->
           { VernacSynterp (VernacReservedNotation (false,(s,l))) }

     | on = enable_enable_disable; IDENT "Notation";
       rule = enable_notation_rule; interp = enable_notation_interpretation;
       flags = enable_notation_flags; scope = opt_scope ->
           { VernacSynPure (VernacEnableNotation (on, rule, interp, flags, scope)) }

     (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order
        to factorize with other "Print"-based or "Declare"-based vernac entries *)
  ] ]
  ;
  enable_enable_disable:
    [ [ IDENT "Enable" -> { true }
      | IDENT "Disable" -> { false } ] ]
  ;
  enable_notation_rule:
    [ [ s = ne_string -> { Some (Inl s) }
      | qid = global; idl = LIST0 ident -> { Some (Inr (idl,qid)) }
      | -> { None } ] ]
  ;
  enable_notation_interpretation:
    [ [ ":="; c = constr -> { Some c }
      | -> { None } ] ]
  ;
  enable_notation_flags:
    [ [ "("; l = LIST1 enable_notation_flag SEP ","; ")" -> { l }
      | -> { [] } ] ]
  ;
  enable_notation_flag:
    [ [ IDENT "all" -> { EnableNotationAll }
      | IDENT "only"; IDENT "parsing" -> { EnableNotationOnly Notationextern.OnlyParsing }
      | IDENT "only"; IDENT "printing" -> { EnableNotationOnly Notationextern.OnlyPrinting }
      | "in"; IDENT "custom"; x = identref -> { EnableNotationEntry CAst.(make ?loc:x.loc (InCustomEntry (Id.to_string x.v))) }
      | "in"; IDENT "constr" -> { EnableNotationEntry (CAst.make ~loc InConstrEntry) } ] ]
  ;
  opt_scope:
    [ [ ":"; sc = IDENT -> { Some (NotationInScope sc) }
      | ":"; IDENT "no"; IDENT "scope" -> { Some LastLonelyNotation }
      | -> { None } ] ]
  ;
  level:
    [ [ IDENT "level"; n = natural -> { NumLevel n }
      | IDENT "next"; IDENT "level" -> { NextLevel } ] ]
  ;
  syntax_modifier:
    [ [ "at"; IDENT "level"; n = natural -> { SetLevel n }
      | "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) }
      | "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural ->
         { SetCustomEntry (x,Some n) }
      | IDENT "left"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.LeftA }
      | IDENT "right"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.RightA }
      | IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA }
      | IDENT "only"; IDENT "printing" -> { SetOnlyPrinting }
      | IDENT "only"; IDENT "parsing" -> { SetOnlyParsing }
      | IDENT "format"; s = lstring -> { SetFormat (TextFormat s) }
      | x = IDENT; ","; l = LIST1 IDENT SEP ","; v =
          [ "at"; lev = level -> { fun x l -> SetItemLevel (x::l,None,lev) }
          | "in"; IDENT "scope"; k = IDENT -> { fun x l -> SetItemScope(x::l,k) } ] -> { v x l }
      | x = IDENT; "at"; lev = level; b = OPT binder_interp ->
        { SetItemLevel ([x],b,lev) }
      | x = IDENT; "in"; IDENT "scope"; k = IDENT -> { SetItemScope([x],k) }
      | x = IDENT; b = binder_interp -> { SetItemLevel ([x],Some b,DefaultLevel) }
      | x = IDENT; typ = explicit_subentry -> { SetEntryType (x,typ) }
    ] ]
  ;
  syntax_modifiers:
    [ [ "("; l = LIST1 [ s = syntax_modifier -> { CAst.make ~loc s } ] SEP ","; ")" -> { l }
      | -> { [] }
    ] ]
  ;
  explicit_subentry:
    [ [ IDENT "ident" -> { ETIdent }
      | IDENT "name" -> { ETName }
      | IDENT "global" -> { ETGlobal }
      | IDENT "bigint" -> { ETBigint }
      | IDENT "binder" -> { ETBinder true }
      | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
      | IDENT "constr"; n = at_level_opt; b = OPT binder_interp -> { ETConstr (InConstrEntry,b,n) }
      | IDENT "pattern" -> { ETPattern (false,None) }
      | IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (false,Some n) }
      | IDENT "strict"; IDENT "pattern" -> { ETPattern (true,None) }
      | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> { ETPattern (true,Some n) }
      | IDENT "closed"; IDENT "binder" -> { ETBinder false }
      | IDENT "custom"; x = IDENT; n = at_level_opt; b = OPT binder_interp ->
           { ETConstr (InCustomEntry x,b,n) }
    ] ]
  ;
  at_level_opt:
    [ [ "at"; n = level -> { n }
      | -> { DefaultLevel } ] ]
  ;
  binder_interp:
    [ [ "as"; IDENT "ident" -> { warn_deprecated_as_ident_kind (); Notation_term.AsIdent }
      | "as"; IDENT "name" -> { Notation_term.AsName }
      | "as"; IDENT "pattern" -> { Notation_term.AsAnyPattern }
      | "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ]
  ;
END