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

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

ltac_expr_opt: [
| OPT tactic_expr5
]

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 ".." 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_ident: [
| "." ident
]

basequalid: [
| REPLACE ident fields
| WITH ident LIST0 field_ident
| DELETE ident
]

field: [ | DELETENT ]
fields: [ | DELETENT ]

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

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

lconstr: [
| DELETE l_constr
]

type_cstr: [
| REPLACE ":" lconstr
| WITH OPT ( ":" lconstr )
| DELETE (* empty *)
]

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

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

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

binder_constr: [
| MOVETO term_let "let" name binders let_type_cstr ":=" operconstr200 "in" operconstr200
| MOVETO term_fix "let" "fix" fix_decl "in" operconstr200
| MOVETO term_cofix "let" "cofix" cofix_decl "in" operconstr200
| MOVETO term_let "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" 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
| MOVETO term_fix "fix" fix_decls
| MOVETO term_cofix "cofix" cofix_decls
]

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 ":=" operconstr200 "in" operconstr200
| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" 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 global univ_instance
| WITH global OPT univ_instance
| 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
| REPLACE "@" global univ_instance LIST0 operconstr9
| WITH "@" global OPT univ_instance LIST0 operconstr9
]

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

operconstr1: [
| REPLACE operconstr0 ".(" global LIST0 appl_arg ")"
| WITH operconstr0 ".(" global LIST0 appl_arg ")"
| MOVETO term_projection operconstr0 ".(" global LIST0 appl_arg ")"
| 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 "}"
| REPLACE "{|" record_declaration bar_cbrace
| WITH "{|" LIST0 field_def bar_cbrace
]

fix_decls: [
| DELETE fix_decl
| REPLACE fix_decl "with" LIST1 fix_decl SEP "with" "for" identref
| WITH fix_decl OPT ( LIST1 ("with" fix_decl) "for" identref )
]

cofix_decls: [
| DELETE cofix_decl
| REPLACE cofix_decl "with" LIST1 cofix_decl SEP "with" "for" identref
| WITH cofix_decl OPT ( LIST1 ( "with" cofix_decl ) "for" identref )
]

fields_def: [
| REPLACE field_def ";" fields_def
| WITH LIST1 field_def SEP ";"
| DELETE field_def
]

binders_fixannot: [
| DELETE binder binders_fixannot
| DELETE fixannot
| DELETE (* empty *)
| LIST0 binder OPT fixannot
]


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 type_cstr ":=" lconstr ")"

| DELETE "{" name "}"
| DELETE "{" name LIST1 name "}"

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

name_colon: [
| name ":"
]

typeclass_constraint: [
| EDIT ADD_OPT "!" operconstr200
| REPLACE "{" name "}" ":" [ "!" | ] operconstr200
| WITH "{" name "}" ":" OPT "!"  operconstr200
| REPLACE name_colon [ "!" | ] operconstr200
| WITH name_colon 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
]

pattern10: [
| REPLACE pattern1 LIST1 pattern1
| WITH pattern1 LIST0 pattern1
| DELETE pattern1
]

pattern0: [
| REPLACE "(" pattern200 ")"
| WITH "(" LIST1 pattern200 SEP "|" ")"
| DELETE "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
| REPLACE "{|" record_patterns bar_cbrace
| WITH "{|" LIST0 record_pattern bar_cbrace
]

DELETE: [
| record_patterns
]

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

universe_increment: [
| REPLACE "+" natural
| WITH OPT ( "+" natural )
| DELETE (* empty *)
]

evar_instance: [
| REPLACE "@{" LIST1 inst SEP ";" "}"
| WITH OPT ( "@{" LIST1 inst SEP ";" "}" )
| DELETE (* empty *)
]

univ_instance: [
| DELETE (* empty *)
]

constr: [
| REPLACE "@" global univ_instance
| WITH "@" global OPT univ_instance
]

(* todo: binders should be binders_opt *)


(* lexer stuff *)
IDENT: [
| ident
]

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

LEFTQMARK: [
| "?"
]

digit: [
| "0" ".." "9"
]

num: [
| LIST1 digit
]

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

numeral: [
| LIST1 digit OPT ("." LIST1 digit) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ]
]

int: [
| OPT "-" LIST1 digit
]

bigint: [
| DELETE NUMERAL
| num
]

first_letter: [
| [ "a" ".." "z" | "A" ".." "Z" | "_" | unicode_letter ]
]

subsequent_letter: [
| [ first_letter | digit | "'" | unicode_id_part ]
]

ident: [
| DELETE IDENT
| first_letter LIST0 subsequent_letter
]

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

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
]

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

(*
| 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
| as_return_type
| case_type
| fields_def
| universe_increment
| type_cstr
| record_pattern
| evar_instance
| fix_decls
| cofix_decls
]

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
| cofix_decl cofix_body
| constr term1_extended
| appl_arg arg
| rec_definition fix_definition
| corec_definition cofix_definition
| inst evar_binding
| univ_instance univ_annot
]


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