(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \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)         *)
(************************************************************************)

(* Defines additional productions and edits for use in documentation.  Not compiled into Coq *)

DOC_GRAMMAR

(* renames to eliminate qualified names
   put other renames at the end *)
RENAME: [
  (* map missing names for rhs *)
| Constr.constr term
| Constr.constr_pattern constr_pattern
| Constr.global global
| Constr.lconstr lconstr
| Constr.lconstr_pattern lconstr_pattern
| G_vernac.query_command query_command
| G_vernac.section_subset_expr section_subset_expr
| Pltac.tactic tactic
| Pltac.tactic_expr tactic_expr5
| Prim.ident ident
| Prim.reference reference
| Pvernac.Vernac_.main_entry vernac_control
| Tactic.tactic tactic

  (* SSR *)
(*
| G_vernac.def_body def_body
| Pcoq.Constr.constr term
| Prim.by_notation by_notation
| Prim.identref ident
| Prim.natural natural
*)
| Vernac.rec_definition rec_definition

| Constr.closed_binder closed_binder
]

(* written in OCaml *)
impl_ident_head: [
| "{" ident
]

lpar_id_coloneq: [
| "(" ident; ":="
]

(* lookahead symbols *)
DELETE: [
| check_for_coloneq
| local_test_lpar_id_colon
| lookup_at_as_comma
| only_starredidentrefs
| test_bracket_ident
| test_lpar_id_colon
| test_lpar_id_coloneq  (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *)
| test_lpar_id_rpar
| test_lpar_idnum_coloneq
| test_nospace_pipe_closedcurly
| test_show_goal

  (* SSR *)
(* | ssr_null_entry *)
(*
| ssrtermkind  (* todo: rename as "test..." *)
| term_annotation  (* todo: rename as "test..." *)
| test_idcomma
| test_nohidden
| test_not_ssrslashnum
| test_ssr_rw_syntax
| test_ssreqid
| test_ssrfwdid
| test_ssrseqvar
| test_ssrslashnum00
| test_ssrslashnum01
| test_ssrslashnum10
| test_ssrslashnum11
| test_ident_no_do
| ssrdoarg  (* todo: this and the next one should be removed from the grammar? *)
| ssrseqdir
*)

(* unused *)
| constr_comma_sequence'
| auto_using'
| constr_may_eval
]

(* ssrintrosarg: [ | DELETENT ] *)

(* additional nts to be spliced *)

hyp: [
| var
]

empty: [
|
]

or_opt: [
| "|"
| empty
]

ltac_expr_opt: [
| tactic_expr5
| empty
]

ltac_expr_opt_list_or: [
| ltac_expr_opt_list_or "|" ltac_expr_opt
| ltac_expr_opt
]

tactic_then_gen: [
| EDIT ADD_OPT tactic_expr5 "|" tactic_then_gen
| EDIT ADD_OPT tactic_expr5 ".." tactic_then_last
| REPLACE OPT tactic_expr5 ".." tactic_then_last
| WITH ltac_expr_opt ".." or_opt ltac_expr_opt_list_or
]

ltac_expr_opt_list_or: [
| ltac_expr_opt_list_or "|" OPT tactic_expr5
| OPT tactic_expr5
]

reference: [ | DELETENT ]

reference: [
| qualid
]

fullyqualid: [ | DELETENT ]

fullyqualid: [
| qualid
]


field: [ | DELETENT ]

field: [
| "." ident
]

basequalid: [
| REPLACE ident fields
| WITH qualid field
]

fields: [ | DELETENT ]

dirpath: [
| REPLACE ident LIST0 field
| WITH ident
| dirpath field
]

binders: [
| DELETE Pcoq.Constr.binders  (* todo: not sure why there are 2 "binders:" *)
]

lconstr: [
| DELETE l_constr
]

let_type_cstr: [
| DELETE OPT [ ":" lconstr ]
| rec_type_cstr
]

as_name_opt: [
| "as" name
| empty
]

(* rename here because we want to use "return_type" for something else *)
RENAME: [
| return_type as_return_type_opt
]

as_return_type_opt: [
| REPLACE OPT [ OPT [ "as" name ] case_type ]
| WITH as_name_opt case_type
| empty
]

case_item: [
| REPLACE operconstr100 OPT [ "as" name ] OPT [ "in" pattern200 ]
| WITH operconstr100 as_name_opt OPT [ "in" pattern200 ]
]

as_dirpath: [
| DELETE OPT [ "as" dirpath ]
| "as" dirpath
| empty
]

binder_constr: [
| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
| MOVETO term_let "let" single_fix "in" operconstr200
| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
| MOVETO term_let "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
| MOVETO term_let "let" "'" pattern200 "in" pattern200 ":=" operconstr200 case_type "in" operconstr200
]

term_let: [
| REPLACE "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
| WITH "let" name let_type_cstr ":=" operconstr200 "in" operconstr200
| "let" name LIST1 binder let_type_cstr ":=" operconstr200 "in" operconstr200
(* Don't need to document that "( )" is equivalent to "()" *)
| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
| WITH "let" [ "(" LIST1 name SEP "," ")" | "()" ] as_return_type_opt ":=" operconstr200 "in" operconstr200
| REPLACE "let" "'" pattern200 ":=" operconstr200 "in" operconstr200
| WITH  "let" "'" pattern200 ":=" operconstr200 OPT case_type "in" operconstr200
| DELETE "let" "'" pattern200 ":=" operconstr200 case_type "in" operconstr200
]

atomic_constr: [
(* @Zimmi48: "string" used only for notations, but keep to be consistent with patterns *)
(* | DELETE string *)
| REPLACE "?" "[" ident "]"
| WITH "?[" ident "]"
| MOVETO term_evar "?[" ident "]"
| REPLACE "?" "[" pattern_ident "]"
| WITH "?[" pattern_ident "]"
| MOVETO term_evar "?[" pattern_ident "]"
| MOVETO term_evar pattern_ident evar_instance
]

tactic_expr0: [
| REPLACE "[" ">" tactic_then_gen "]"
| WITH "[>" tactic_then_gen "]"
]

operconstr100: [
| MOVETO term_cast operconstr99 "<:" operconstr200
| MOVETO term_cast operconstr99 "<<:" operconstr200
| MOVETO term_cast operconstr99 ":" operconstr200
| MOVETO term_cast operconstr99 ":>"
]

operconstr10: [
(* fixme: add in as a prodn somewhere *)
| MOVETO dangling_pattern_extension_rule "@" pattern_identref LIST1 identref
| DELETE dangling_pattern_extension_rule
]

operconstr9: [
(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
| DELETE ".." operconstr0 ".."
]

arg_list: [
| arg_list appl_arg
| appl_arg
]

arg_list_opt: [
| arg_list
| empty
]

operconstr1: [
| REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
| WITH operconstr0 ".(" global arg_list_opt ")"
| MOVETO term_projection operconstr0 ".(" global arg_list_opt ")"
| MOVETO term_projection operconstr0 ".(" "@" global LIST0 ( operconstr9 ) ")"
]

operconstr0: [
(* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
| DELETE "{" binder_constr "}"
]

single_fix: [
| DELETE fix_kw fix_decl
| "fix" fix_decl
| "cofix" fix_decl
]

fix_kw: [ | DELETENT ]

binders_fixannot: [
(*
| REPLACE impl_name_head impl_ident_tail binders_fixannot
| WITH impl_name_head impl_ident_tail "}" binders_fixannot
*)
(* Omit this complex detail.  See https://github.com/coq/coq/pull/10614#discussion_r344118146 *)
| DELETE impl_name_head impl_ident_tail binders_fixannot

| DELETE fixannot
| DELETE binder binders_fixannot
| DELETE (* empty *)

| LIST0 binder OPT fixannot
]

impl_ident_tail: [
| DELETENT
(*
| REPLACE "}"
| WITH empty
| REPLACE LIST1 name ":" lconstr "}"
| WITH LIST1 name ":" lconstr
| REPLACE LIST1 name "}"
| WITH LIST1 name
| REPLACE ":" lconstr "}"
| WITH ":" lconstr
*)
]

of_type_with_opt_coercion: [
| DELETE ":>" ">"
| DELETE ":" ">" ">"
| DELETE ":" ">"
]

binder: [
| DELETE name
]

open_binders: [
| REPLACE name LIST0 name ":" lconstr
| WITH LIST1 name ":" lconstr
(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
| DELETE name ".." name
| REPLACE name LIST0 name binders
| WITH LIST1 binder
| DELETE closed_binder binders
]

closed_binder: [
| name

| REPLACE "(" name LIST1 name ":" lconstr ")"
| WITH "(" LIST1 name ":" lconstr ")"
| DELETE "(" name ":" lconstr ")"

| DELETE "(" name ":=" lconstr ")"
| REPLACE "(" name ":" lconstr ":=" lconstr ")"
| WITH "(" name rec_type_cstr ":=" lconstr ")"

| DELETE "{" name LIST1 name "}"

| REPLACE "{" name LIST1 name ":" lconstr "}"
| WITH "{" LIST1 name rec_type_cstr "}"
| DELETE "{" name ":" lconstr  "}"
]

typeclass_constraint: [
| EDIT ADD_OPT "!" operconstr200
]

(* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*)
Prim.name: [
| REPLACE "_"
| WITH name
]

oriented_rewriter: [
| REPLACE orient_rw rewriter
| WITH orient rewriter
]

DELETE: [
| orient_rw
]

pattern1_list: [
| pattern1_list pattern1
| pattern1
]

pattern1_list_opt: [
| pattern1_list
| empty
]

pattern10: [
| REPLACE pattern1 LIST1 pattern1
| WITH LIST1 pattern1
| REPLACE "@" reference LIST0 pattern1
| WITH "@" reference pattern1_list_opt
]

pattern0: [
| REPLACE "(" pattern200 ")"
| WITH "(" LIST1 pattern200 SEP "|" ")"
| DELETE "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
]

patterns_comma: [
| patterns_comma "," pattern100
| pattern100
]

patterns_comma_list_or: [
| patterns_comma_list_or "|" patterns_comma
| patterns_comma
]

eqn: [
| REPLACE LIST1 mult_pattern SEP "|" "=>" lconstr
| WITH patterns_comma_list_or "=>" lconstr
]

record_patterns: [
| REPLACE record_pattern ";" record_patterns
| WITH record_patterns ";" record_pattern
]

(* todo: binders should be binders_opt *)


(* lexer stuff *)
bigint: [
| DELETE NUMERAL
| num
]

ident: [
| DELETENT
]

IDENT: [
| ident
]

integer: [ | DELETENT ]
RENAME: [
| integer int (* todo: review uses in .mlg files, some should be "natural" *)
]

LEFTQMARK: [
| "?"
]

natural: [ | DELETENT ]
natural: [
| num  (* todo: or should it be "nat"? *)
]

NUMERAL: [
| numeral
]

(* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *)

string: [ | DELETENT ]
STRING: [
| string
]


(* todo: is "bigint" useful?? *)
(* todo: "check_int" in g_prim.mlg should be "check_num" *)

  (* added productions *)

name_colon: [
| name ":"
]

command_entry: [
| noedit_mode
]

tactic_expr1: [
| EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
| MOVETO ltac_match_goal match_key OPT "reverse" "goal" "with" match_context_list "end"
| MOVETO ltac_match_term match_key tactic_expr5 "with" match_list "end"
]

DELETE: [
| tactic_then_locality
]

tactic_expr4: [
| REPLACE tactic_expr3 ";" tactic_then_gen "]"
| WITH tactic_expr3 ";" "[" tactic_then_gen "]"
| tactic_expr3 ";" "[" ">" tactic_then_gen "]"
]

match_context_list: [
| EDIT ADD_OPT "|" LIST1 match_context_rule SEP "|"
]

match_hyps: [
| REPLACE name ":=" "[" match_pattern "]" ":" match_pattern
| WITH name ":=" OPT ("[" match_pattern "]" ":") match_pattern
| DELETE name ":=" match_pattern
]

match_list: [
| EDIT ADD_OPT "|" LIST1 match_rule SEP "|"
]

match_rule: [
| REPLACE match_pattern "=>" tactic_expr5
| WITH [ match_pattern | "_" ] "=>" tactic_expr5
| DELETE "_" "=>" tactic_expr5
]


selector_body: [
| REPLACE range_selector_or_nth  (* depends on whether range_selector_or_nth is deleted first *)
| WITH LIST1 range_selector SEP ","
]

range_selector_or_nth: [ | DELETENT ]

simple_tactic: [
| DELETE "intros"
| REPLACE "intros" ne_intropatterns
| WITH "intros" intropatterns
| DELETE "eintros"
| REPLACE "eintros" ne_intropatterns
| WITH "eintros" intropatterns
]

intropatterns: [
| DELETE LIST0 intropattern
| intropatterns intropattern
| empty
]

(* todo: don't use DELETENT for this *)
ne_intropatterns: [ | DELETENT ]


or_and_intropattern: [
| DELETE "()"
| DELETE "(" simple_intropattern ")"
| REPLACE "(" simple_intropattern "," LIST1 simple_intropattern SEP "," ")"
|   WITH  "(" LIST0 simple_intropattern SEP "," ")"
| EDIT "[" USE_NT intropattern_or LIST1 intropatterns SEP "|" "]"
]

bar_cbrace: [
| REPLACE "|" "}"
| WITH "|}"
]

(* todo: is this really correct? Search for "Pvernac.register_proof_mode" *)
(* consider tactic_command vs tac2mode *)
vernac_aux: [
| tactic_mode "."
]

SPLICE: [
| noedit_mode
| command_entry
| bigint
| match_list
| match_context_list
| IDENT
| LEFTQMARK
| natural
| NUMERAL
| STRING
| hyp
| var
| identref
| pattern_ident
| constr_eval  (* splices as multiple prods *)
| tactic_then_last  (* todo: dependency on c.edit_mlg edit?? really useful? *)
| Prim.name
| ltac_selector
| Constr.ident
| attribute_list
| operconstr99
| operconstr90
| operconstr9
| operconstr8
| pattern200
| pattern99
| pattern90
| ne_lstring
| ne_string
| lstring
| basequalid
| fullyqualid
| global
| reference
| bar_cbrace
| lconstr
| impl_name_head

(*
| ast_closure_term
| ast_closure_lterm
| ident_no_do
| ssrterm
| ssrtacarg
| ssrtac3arg
| ssrtclarg
| ssrhyp
| ssrhoi_hyp
| ssrhoi_id
| ssrindex
| ssrhpats
| ssrhpats_nobs
| ssrfwdid
| ssrmovearg
| ssrcasearg
| ssrrwargs
| ssrviewposspc
| ssrpatternarg
| ssr_elsepat
| ssr_mpat
| ssrunlockargs
| ssrcofixfwd
| ssrfixfwd
| ssrhavefwdwbinders
| ssripats_ne
| ssrparentacarg
| ssrposefwd
*)

| preident
| lpar_id_coloneq
| binders
| casted_constr
| check_module_types
| constr_pattern
| decl_sep
| function_rec_definition_loc (* loses funind annotation *)
| glob
| glob_constr_with_bindings
| id_or_meta
| lconstr_pattern
| lglob
| ltac_tacdef_body
| mode
| mult_pattern
| open_constr
| option_table
| record_declaration
| register_type_token
| tactic
| uconstr
| impl_ident_head
| argument_spec
| at_level
| branches
| check_module_type
| decorated_vernac
| ext_module_expr
| ext_module_type
| pattern_identref
| test
| binder_constr
| atomic_constr
| let_type_cstr
| name_colon
| closed_binder
| binders_fixannot
]

RENAME: [
| clause clause_dft_concl
| in_clause' in_clause

| tactic3 ltac_expr3  (* todo: can't figure out how this gets mapped by coqpp *)
| tactic1 ltac_expr1  (* todo: can't figure out how this gets mapped by coqpp *)
| tactic0 ltac_expr0  (* todo: can't figure out how this gets mapped by coqpp *)
| tactic_expr5 ltac_expr
| tactic_expr4 ltac_expr4
| tactic_expr3 ltac_expr3
| tactic_expr2 ltac_expr2
| tactic_expr1 ltac_expr1
| tactic_expr0 ltac_expr0

(* | nonsimple_intropattern intropattern (* ltac2 *) *)
| intropatterns intropattern_list_opt

| operconstr200 term   (* historical name *)
| operconstr100 term100
| operconstr10 term10
| operconstr1 term1
| operconstr0 term0
| pattern100 pattern
| match_constr term_match
(*| impl_ident_tail impl_ident*)
| ssexpr35 ssexpr (* strange in mlg, ssexpr50 is after this *)

| tactic_then_gen multi_goal_tactics
| selector only_selector
| selector_body selector
| input_fun fun_var
| match_hyps match_hyp

| BULLET bullet
| nat_or_var num_or_var
| fix_decl fix_body
| instance universe_annot_opt
| rec_type_cstr colon_term_opt
| fix_constr term_fix
| constr term1_extended
| case_type return_type
| appl_arg arg
| record_patterns record_patterns_opt
| universe_increment universe_increment_opt
| rec_definition fix_definition
| corec_definition cofix_definition
| record_field_instance field_def
| record_fields_instance fields_def
| evar_instance evar_bindings_opt
| inst evar_binding
]


(* todo: ssrreflect*.rst ref to fix_body is incorrect *)