diff options
Diffstat (limited to 'doc/tools/docgram')
| -rw-r--r-- | doc/tools/docgram/README.md | 17 | ||||
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 345 | ||||
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 103 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 30 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 639 | ||||
| -rw-r--r-- | doc/tools/docgram/productionlist.edit_mlg | 16 |
6 files changed, 733 insertions, 417 deletions
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md index 182532e413..fc6d0ace0d 100644 --- a/doc/tools/docgram/README.md +++ b/doc/tools/docgram/README.md @@ -176,9 +176,13 @@ that appear in the specified production: production **without** `<grammar_symbol>`. If found, both productions are replaced with single production with `OPT <grammar_symbol>` - The current version handles a single USE_NT or ADD_OPT per EDIT. + The current version handles a single USE_NT or ADD_OPT per EDIT. These symbols + may appear in the middle of the production given in the EDIT. -* `REPLACE` - (2 sequential productions) - removes `<oldprod>` and +`INSERTALL <symbols>` - inserts <symbols> at the beginning of every production in +<edited_nt>. + +`REPLACE` - (2 sequential productions) - removes `<oldprod>` and inserts `<newprod>` in its place. ``` @@ -186,7 +190,14 @@ that appear in the specified production: | WITH <newprod> ``` -* `PRINT` <nonterminal> - prints the nonterminal definition at that point in +`MOVETO <destination> <production>` - moves the production to `<destination>` and, + if needed, creates a new production <edited_nt> -> <destination>. + +`OPTINREF` - verifies that <edited_nt> has an empty production. If so, it removes +the empty production and replaces all references to <edited_nt> throughout the +grammar with `OPT <edited_nt>` + +`PRINT` <nonterminal> - prints the nonterminal definition at that point in applying the edits. Most useful when the edits get a bit complicated to follow. * (any other nonterminal name) - adds a new production (and possibly a new nonterminal) diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 9c1827f5b7..3524d77380 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -39,7 +39,7 @@ RENAME: [ | Prim.natural natural *) | Vernac.rec_definition rec_definition - +(* todo: hmm, rename adds 1 prodn to closed_binder?? *) | Constr.closed_binder closed_binder ] @@ -162,11 +162,6 @@ lconstr: [ | DELETE l_constr ] -type_cstr: [ -| REPLACE ":" lconstr -| WITH OPT ( ":" lconstr ) -| DELETE (* empty *) -] let_type_cstr: [ | DELETE OPT [ ":" lconstr ] @@ -210,8 +205,6 @@ term_let: [ 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 "]" @@ -237,8 +230,6 @@ 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: [ @@ -285,13 +276,6 @@ binders_fixannot: [ | LIST0 binder OPT fixannot ] - -of_type_with_opt_coercion: [ -| DELETE ":>" ">" -| DELETE ":" ">" ">" -| DELETE ":" ">" -] - binder: [ | DELETE name ] @@ -306,11 +290,15 @@ open_binders: [ | DELETE closed_binder binders ] +type: [ +| operconstr200 +] + closed_binder: [ | name | REPLACE "(" name LIST1 name ":" lconstr ")" -| WITH "(" LIST1 name ":" lconstr ")" +| WITH "(" LIST1 name ":" type ")" | DELETE "(" name ":" lconstr ")" | DELETE "(" name ":=" lconstr ")" @@ -324,6 +312,16 @@ closed_binder: [ | REPLACE "{" name LIST1 name ":" lconstr "}" | WITH "{" LIST1 name type_cstr "}" | DELETE "{" name ":" lconstr "}" + +| DELETE "[" name "]" +| DELETE "[" name LIST1 name "]" + +| REPLACE "[" name LIST1 name ":" lconstr "]" +| WITH "[" LIST1 name type_cstr "]" +| DELETE "[" name ":" lconstr "]" + +| REPLACE "(" Prim.name ":" lconstr "|" lconstr ")" +| WITH "(" Prim.name ":" type "|" lconstr ")" ] name_colon: [ @@ -377,28 +375,151 @@ eqn: [ ] universe_increment: [ -| REPLACE "+" natural -| WITH OPT ( "+" natural ) -| DELETE (* empty *) +| OPTINREF ] evar_instance: [ -| REPLACE "@{" LIST1 inst SEP ";" "}" -| WITH OPT ( "@{" LIST1 inst SEP ";" "}" ) +| OPTINREF +] + +gallina: [ +| REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ] +| WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ] +| DELETE assumptions_token inline assum_list +| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) +| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition ) +| "Variant" inductive_definition LIST0 ( "with" inductive_definition ) +| [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition ) +| "Class" inductive_definition LIST0 ( "with" inductive_definition ) +| REPLACE "Fixpoint" LIST1 rec_definition SEP "with" +| WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) +| REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with" +| WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) +| REPLACE "CoFixpoint" LIST1 corec_definition SEP "with" +| WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) +| REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with" +| WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) +| REPLACE "Scheme" LIST1 scheme SEP "with" +| WITH "Scheme" scheme LIST0 ( "with" scheme ) +] + +DELETE: [ +| private_token +| cumulativity_token +] + +opt_coercion: [ +| OPTINREF +] + +opt_constructors_or_fields: [ +| OPTINREF +] + +SPLICE: [ +| opt_coercion +| opt_constructors_or_fields +] + +constructor_list_or_record_decl: [ +| OPTINREF +] + +record_fields: [ +| REPLACE record_field ";" record_fields +| WITH LIST1 record_field SEP ";" +| DELETE record_field | DELETE (* empty *) ] +decl_notation: [ +| REPLACE "where" LIST1 one_decl_notation SEP decl_sep +| WITH "where" one_decl_notation LIST0 ( decl_sep one_decl_notation ) +] + +assumptions_token: [ +| DELETENT +] + +inline: [ +| REPLACE "Inline" "(" natural ")" +| WITH "Inline" OPT ( "(" natural ")" ) +| DELETE "Inline" +| OPTINREF +] + univ_instance: [ -| DELETE (* empty *) +| OPTINREF +] + +univ_decl: [ +| REPLACE "@{" LIST0 identref [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | bar_cbrace ] ] +| WITH "@{" LIST0 identref OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" +] + +of_type_with_opt_coercion: [ +| DELETENT +] + +of_type_with_opt_coercion: [ +| [ ":" | ":>" | ":>>" ] type +] + +attribute_value: [ +| OPTINREF +] + +def_body: [ +| DELETE binders ":=" reduce lconstr +| REPLACE binders ":" lconstr ":=" reduce lconstr +| WITH LIST0 binder OPT (":" type) ":=" reduce lconstr +| REPLACE binders ":" lconstr +| WITH LIST0 binder ":" type +] + +reduce: [ +| OPTINREF +] + +occs: [ +| OPTINREF +] + +delta_flag: [ +| REPLACE "-" "[" LIST1 smart_global "]" +| WITH OPT "-" "[" LIST1 smart_global "]" +| DELETE "[" LIST1 smart_global "]" +| OPTINREF +] + +strategy_flag: [ +| REPLACE OPT delta_flag +| WITH delta_flag +| (* empty *) +| OPTINREF ] -constr: [ -| REPLACE "@" global univ_instance -| WITH "@" global OPT univ_instance +export_token: [ +| OPTINREF ] -(* todo: binders should be binders_opt *) +functor_app_annot: [ +| OPTINREF +] + +is_module_expr: [ +| OPTINREF +] +is_module_type: [ +| OPTINREF +] + +gallina_ext: [ +| REPLACE "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| WITH "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +] (* lexer stuff *) IDENT: [ @@ -478,6 +599,8 @@ 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" +| REPLACE failkw [ int_or_var | ] LIST0 message_token +| WITH failkw OPT int_or_var LIST0 message_token ] DELETE: [ @@ -544,12 +667,146 @@ bar_cbrace: [ | WITH "|}" ] +printable: [ +| REPLACE [ "Sorted" | ] "Universes" OPT printunivs_subgraph OPT ne_string +| WITH OPT "Sorted" "Universes" OPT printunivs_subgraph OPT ne_string +| INSERTALL "Print" +] + +command: [ +| REPLACE "Print" printable +| WITH printable +| "SubClass" ident_decl def_body +| REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with" +| WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body ) +| REPLACE "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) +| WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc ) (* funind plugin *) +| REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) +| WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg ) (* funind plugin *) + +] + +only_parsing: [ +| OPTINREF +] + +syntax: [ +| REPLACE "Infix" ne_lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| WITH "Infix" ne_lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ] +| REPLACE "Notation" lstring ":=" constr [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" IDENT ] +| WITH "Notation" lstring ":=" constr OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" IDENT ] +| REPLACE "Reserved" "Infix" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] +| WITH "Reserved" "Infix" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] +| REPLACE "Reserved" "Notation" ne_lstring [ "(" LIST1 syntax_modifier SEP "," ")" | ] +| WITH "Reserved" "Notation" ne_lstring OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] +] + +numnotoption: [ +| OPTINREF +] + +binder_tactic: [ +| REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 +| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5 +] + +tactic_then_gen: [ +| OPTINREF +] + +record_binder_body: [ +| REPLACE binders of_type_with_opt_coercion lconstr +| WITH binders of_type_with_opt_coercion +| REPLACE binders of_type_with_opt_coercion lconstr ":=" lconstr +| WITH binders of_type_with_opt_coercion ":=" lconstr +] + +simple_assum_coe: [ +| REPLACE LIST1 ident_decl of_type_with_opt_coercion lconstr +| WITH LIST1 ident_decl of_type_with_opt_coercion +] + +constructor_type: [ +| REPLACE binders [ of_type_with_opt_coercion lconstr | ] +| WITH binders OPT of_type_with_opt_coercion +] + (* todo: is this really correct? Search for "Pvernac.register_proof_mode" *) (* consider tactic_command vs tac2mode *) vernac_aux: [ | tactic_mode "." ] +def_token: [ +| DELETE "SubClass" (* document separately from Definition and Example *) +] + +assumption_token: [ +| REPLACE "Axiom" +| WITH [ "Axiom" | "Axioms" ] +| REPLACE "Conjecture" +| WITH [ "Conjecture" | "Conjectures" ] +| REPLACE "Hypothesis" +| WITH [ "Hypothesis" | "Hypotheses" ] +| REPLACE "Parameter" +| WITH [ "Parameter" | "Parameters" ] +| REPLACE "Variable" +| WITH [ "Variable" | "Variables" ] +] + +legacy_attrs: [ +| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" +] + +all_attrs: [ +| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs +] + +vernacular: [ +| LIST0 ( OPT all_attrs [ command | tactic ] "." ) +] + +rec_definition: [ +| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation +| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation +] + +corec_definition: [ +| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation +| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation +] + +type_cstr: [ +| REPLACE ":" lconstr +| WITH ":" type +| OPTINREF +] + +decl_notation: [ +| OPTINREF +] + +inductive_definition: [ +| REPLACE OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation +| WITH OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation +] + +constructor_list_or_record_decl: [ +| DELETE "|" LIST1 constructor SEP "|" +| REPLACE identref constructor_type "|" LIST1 constructor SEP "|" +| WITH OPT "|" LIST1 constructor SEP "|" +| DELETE identref constructor_type +| REPLACE identref "{" record_fields "}" +| WITH OPT identref "{" record_fields "}" +| DELETE "{" record_fields "}" +] + +record_binder: [ +| REPLACE name record_binder_body +| WITH name OPT record_binder_body +| DELETE name +] + SPLICE: [ | noedit_mode | command_entry @@ -642,8 +899,6 @@ SPLICE: [ | tactic | uconstr | impl_ident_head -| argument_spec -| at_level | branches | check_module_type | decorated_vernac @@ -666,7 +921,27 @@ SPLICE: [ | evar_instance | fix_decls | cofix_decls -] +| assum_list +| assum_coe +| inline +| occs +| univ_name_list +| ltac_info +| field_mods +| ltac_production_sep +| ltac_tactic_level +| printunivs_subgraph +| ring_mods +| scope_delimiter +| eliminator (* todo: splice or not? *) +| quoted_attributes (* todo: splice or not? *) +| printable +| only_parsing +| def_token +| record_fields +| constructor_type +| record_binder +] (* end SPLICE *) RENAME: [ | clause clause_dft_concl @@ -711,6 +986,14 @@ RENAME: [ | corec_definition cofix_definition | inst evar_binding | univ_instance univ_annot +| simple_assum_coe assumpt +| of_type_with_opt_coercion of_type +| decl_notation decl_notations +| one_decl_notation decl_notation +| attribute attr +| attribute_value attr_value +| constructor_list_or_record_decl constructors_or_record +| record_binder_body field_body ] diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index b50c427742..5fcb56f5f2 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -693,6 +693,58 @@ let create_edit_map g op edits = let remove_Sedit2 p = List.filter (fun sym -> match sym with | Sedit2 _ -> false | _ -> true) p +(* don't deal with Sedit, Sedit2 yet (ever?) *) +let rec pmatch fullprod fullpat repl = + let map_prod prod = List.concat (List.map (fun s -> pmatch [s] fullpat repl) prod) in + let pmatch_wrap sym = + let r = pmatch [sym] fullpat repl in + match r with + | a :: b :: tl -> Sparen r + | [a] -> a + | x -> error "pmatch: should not happen"; Sterm "??" + in + + let symmatch_r s = + let res = match s with + | Slist1 sym -> Slist1 (pmatch_wrap sym) + | Slist1sep (sym, sep) -> Slist1sep (pmatch_wrap sym, sep) + | Slist0 sym -> Slist0 (pmatch_wrap sym) + | Slist0sep (sym, sep) -> Slist0sep (pmatch_wrap sym, sep) + | Sopt sym -> Sopt (pmatch_wrap sym) + | Sparen prod -> Sparen (map_prod prod) + | Sprod prods -> Sprod (List.map map_prod prods) + | sym -> sym + in +(* Printf.printf "symmatch of %s gives %s\n" (prod_to_str [s]) (prod_to_str [res]);*) + res + in + + let rec pmatch_r prod pat match_start start_res res = +(* Printf.printf "pmatch_r: prod = %s; pat = %s; res = %s\n" (prod_to_str prod) (prod_to_str pat) (prod_to_str res);*) + match prod, pat with + | _, [] -> + let new_res = (List.rev repl) @ res in + pmatch_r prod fullpat prod new_res new_res (* subst and continue *) + | [], _ -> (List.rev ((List.rev match_start) @ res)) (* leftover partial match *) + | hdprod :: tlprod, hdpat :: tlpat -> + if hdprod = hdpat then + pmatch_r tlprod tlpat match_start start_res res + else + (* match from the next starting position *) + match match_start with + | hd :: tl -> + let new_res = (symmatch_r hd) :: start_res in + pmatch_r tl fullpat tl new_res new_res + | [] -> List.rev res (* done *) + in + pmatch_r fullprod fullpat fullprod [] [] + +(* global replace of production substrings, rhs only *) +let global_repl g pat repl = + List.iter (fun nt -> + g_update_prods g nt (List.map (fun prod -> pmatch prod pat repl) (NTMap.find nt !g.map)) + ) !g.order + (* edit a production: rename nonterminals, drop nonterminals, substitute nonterminals *) let rec edit_prod g top edit_map prod = let edit_nt edit_map sym0 nt = @@ -1112,8 +1164,15 @@ let apply_edit_file g edits = with Not_found -> prods) in aux tl prods' add_nt + | (Snterm "OPTINREF" :: _) :: tl -> + if not (List.mem [] prods) then + error "OPTINREF but no empty production for %s\n" nt; + global_repl g [(Snterm nt)] [(Sopt (Snterm nt))]; + aux tl (remove_prod [] prods nt) add_nt + | (Snterm "INSERTALL" :: syms) :: tl -> + aux tl (List.map (fun p -> syms @ p) prods) add_nt | (Snterm "PRINT" :: _) :: tl -> - pr_prods nt (NTMap.find nt !g.map); + pr_prods nt prods; aux tl prods add_nt | (Snterm "EDIT" :: oprod) :: tl -> aux tl (edit_single_prod g oprod prods nt) add_nt @@ -1593,6 +1652,7 @@ type seen = { nts: (string * int) NTMap.t; tacs: (string * int) NTMap.t; cmds: (string * int) NTMap.t; + cmdvs: (string * int) NTMap.t; } let process_rst g file args seen tac_prods cmd_prods = @@ -1640,9 +1700,9 @@ let process_rst g file args seen tac_prods cmd_prods = let start_index = index_of start !g.order in let end_index = index_of end_ !g.order in if start_index = None then - error "%s line %d: '%s' is undefined\n" file !linenum start; + error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum start; if end_index = None then - error "%s line %d: '%s' is undefined\n" file !linenum end_; + error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum end_; if start_index <> None && end_index <> None then check_range_consistency g start end_; match start_index, end_index with @@ -1697,12 +1757,17 @@ let process_rst g file args seen tac_prods cmd_prods = seen := { !seen with tacs = (NTMap.add rhs (file, !linenum) !seen.tacs)}; fprintf new_rst "%s\n" line | "cmd::" when args.check_cmds -> +(* if not (StringSet.mem rhs cmd_prods) then warn "%s line %d: Unknown command: '%s'\n" file !linenum rhs; if NTMap.mem rhs !seen.cmds then warn "%s line %d: Repeated command: '%s'\n" file !linenum rhs; +*) seen := { !seen with cmds = (NTMap.add rhs (file, !linenum) !seen.cmds)}; fprintf new_rst "%s\n" line + | "cmdv::" when args.check_cmds -> + seen := { !seen with cmdvs = (NTMap.add rhs (file, !linenum) !seen.cmdvs)}; + fprintf new_rst "%s\n" line | "insertprodn" -> process_insertprodn line rhs | _ -> fprintf new_rst "%s\n" line @@ -1818,15 +1883,43 @@ let process_grammar args = list, StringSet.of_list list in let tac_list, tac_prods = plist "simple_tactic" in let cmd_list, cmd_prods = plist "command" in - let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty } in + let seen = ref { nts=NTMap.empty; tacs=NTMap.empty; cmds=NTMap.empty; cmdvs=NTMap.empty } in List.iter (fun file -> process_rst g file args seen tac_prods cmd_prods) args.rst_files; report_omitted_prods !g.order !seen.nts "Nonterminal" ""; let out = open_out (dir "updated_rsts") in close_out out; +(* if args.check_tacs then report_omitted_prods tac_list !seen.tacs "Tactic" "\n "; if args.check_cmds then - report_omitted_prods cmd_list !seen.cmds "Command" "\n " + report_omitted_prods cmd_list !seen.cmds "Command" "\n "; +*) + + let rstCmds = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings !seen.cmds)) in + let rstCmdvs = StringSet.of_list (List.map (fun b -> let c, _ = b in c) (NTMap.bindings !seen.cmdvs)) in + let command_nts = ["command"; "gallina"; "gallina_ext"; "query_command"; "syntax"] in + (* TODO: need to handle tactic_mode (overlaps with query_command) and subprf *) + let gramCmds = List.fold_left (fun set nt -> + StringSet.union set (StringSet.of_list (List.map (fun p -> String.trim (prod_to_prodn p)) (NTMap.find nt !prodn_gram.map))) + ) StringSet.empty command_nts in + + let allCmds = StringSet.union rstCmdvs (StringSet.union rstCmds gramCmds) in + let out = open_out_bin (dir "prodnCommands") in + StringSet.iter (fun c -> + let rsts = StringSet.mem c rstCmds in + let gram = StringSet.mem c gramCmds in + let pfx = match rsts, gram with + | true, false -> "+" + | false, true -> "-" + | false, false -> "?" + | _, _ -> " " + in + let var = if StringSet.mem c rstCmdvs then "v" else " " in + fprintf out "%s%s %s\n" pfx var c) + allCmds; + close_out out; + Printf.printf "# cmds in rsts, gram, total = %d %d %d\n" (StringSet.cardinal gramCmds) + (StringSet.cardinal rstCmds) (StringSet.cardinal allCmds); end; (* generate output for prodn: simple_tactic, command, also for Ltac?? *) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index e12589bb89..529d81e424 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -322,8 +322,13 @@ closed_binder: [ | "{" name LIST1 name ":" lconstr "}" | "{" name ":" lconstr "}" | "{" name LIST1 name "}" +| "[" name "]" +| "[" name LIST1 name ":" lconstr "]" +| "[" name ":" lconstr "]" +| "[" name LIST1 name "]" | "`(" LIST1 typeclass_constraint SEP "," ")" | "`{" LIST1 typeclass_constraint SEP "," "}" +| "`[" LIST1 typeclass_constraint SEP "," "]" | "'" pattern0 ] @@ -643,6 +648,7 @@ command: [ | "Show" "Ltac" "Profile" | "Show" "Ltac" "Profile" "CutOff" int | "Show" "Ltac" "Profile" string +| "Show" "Lia" "Profile" (* micromega plugin *) | "Add" "InjTyp" constr (* micromega plugin *) | "Add" "BinOp" constr (* micromega plugin *) | "Add" "UnOp" constr (* micromega plugin *) @@ -937,12 +943,12 @@ opt_constructors_or_fields: [ ] inductive_definition: [ -| opt_coercion ident_decl binders OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation +| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation ] constructor_list_or_record_decl: [ | "|" LIST1 constructor SEP "|" -| identref constructor_type "|" LIST0 constructor SEP "|" +| identref constructor_type "|" LIST1 constructor SEP "|" | identref constructor_type | identref "{" record_fields "}" | "{" record_fields "}" @@ -1270,7 +1276,7 @@ printable: [ | "Instances" smart_global | "Coercions" | "Coercion" "Paths" class_rawexpr class_rawexpr -| "Canonical" "Projections" +| "Canonical" "Projections" LIST0 smart_global | "Typing" "Flags" | "Tables" | "Options" @@ -1400,8 +1406,7 @@ syntax_modifier: [ | "only" "parsing" | "format" STRING OPT STRING | IDENT; "," LIST1 IDENT SEP "," "at" level -| IDENT; "at" level -| IDENT; "at" level constr_as_binder_kind +| IDENT; "at" level OPT constr_as_binder_kind | IDENT constr_as_binder_kind | IDENT syntax_extension_type ] @@ -1412,17 +1417,18 @@ syntax_extension_type: [ | "bigint" | "binder" | "constr" -| "constr" OPT at_level OPT constr_as_binder_kind +| "constr" at_level_opt OPT constr_as_binder_kind | "pattern" | "pattern" "at" "level" natural | "strict" "pattern" | "strict" "pattern" "at" "level" natural | "closed" "binder" -| "custom" IDENT OPT at_level OPT constr_as_binder_kind +| "custom" IDENT at_level_opt OPT constr_as_binder_kind ] -at_level: [ +at_level_opt: [ | "at" level +| ] constr_as_binder_kind: [ @@ -1719,7 +1725,6 @@ simple_tactic: [ | "restart_timer" OPT string | "finish_timing" OPT string | "finish_timing" "(" string ")" OPT string -| "myred" (* micromega plugin *) | "psatz_Z" int_or_var tactic (* micromega plugin *) | "psatz_Z" tactic (* micromega plugin *) | "xlia" tactic (* micromega plugin *) @@ -1735,13 +1740,12 @@ simple_tactic: [ | "psatz_R" tactic (* micromega plugin *) | "psatz_Q" int_or_var tactic (* micromega plugin *) | "psatz_Q" tactic (* micromega plugin *) -| "iter_specs" tactic (* micromega plugin *) +| "zify_iter_specs" tactic (* micromega plugin *) | "zify_op" (* micromega plugin *) -| "saturate" (* micromega plugin *) +| "zify_saturate" (* micromega plugin *) +| "zify_iter_let" tactic (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) | "omega" (* omega plugin *) -| "omega" "with" LIST1 ident (* omega plugin *) -| "omega" "with" "*" (* omega plugin *) | "rtauto" | "protect_fv" string "in" ident (* setoid_ring plugin *) | "protect_fv" string (* setoid_ring plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 63e0ca129c..908e3ccd51 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -29,7 +29,7 @@ vernac_control: [ | "Redirect" string vernac_control | "Timeout" num vernac_control | "Fail" vernac_control -| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) vernac +| LIST0 ( "#[" LIST0 attr SEP "," "]" ) vernac ] term: [ @@ -102,50 +102,24 @@ dangling_pattern_extension_rule: [ | "@" "?" ident LIST1 ident ] -record_fields: [ -| record_field ";" record_fields -| record_field -| -] - -record_field: [ -| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) record_binder OPT [ "|" num ] decl_notation -] - -decl_notation: [ -| "where" LIST1 one_decl_notation SEP "and" -| -] - -one_decl_notation: [ -| string ":=" term1_extended OPT [ ":" ident ] +assumption_token: [ +| [ "Axiom" | "Axioms" ] +| [ "Conjecture" | "Conjectures" ] +| [ "Parameter" | "Parameters" ] +| [ "Hypothesis" | "Hypotheses" ] +| [ "Variable" | "Variables" ] ] -record_binder: [ -| name -| name record_binder_body +assumpt: [ +| LIST1 ident_decl of_type ] -record_binder_body: [ -| LIST0 binder of_type_with_opt_coercion term -| LIST0 binder of_type_with_opt_coercion term ":=" term -| LIST0 binder ":=" term -] - -of_type_with_opt_coercion: [ -| ":>>" -| ":>" -| ":" +ident_decl: [ +| ident OPT univ_decl ] -attribute: [ -| ident attribute_value -] - -attribute_value: [ -| "=" string -| "(" LIST0 attribute SEP "," ")" -| +of_type: [ +| [ ":" | ":>" | ":>>" ] type ] qualid: [ @@ -156,6 +130,10 @@ field_ident: [ | "." ident ] +type: [ +| term +] + numeral: [ | LIST1 digit OPT ( "." LIST1 digit ) OPT [ [ "e" | "E" ] OPT [ "+" | "-" ] LIST1 digit ] ] @@ -184,6 +162,27 @@ subsequent_letter: [ | [ first_letter | digit | "'" | unicode_id_part ] ] +vernacular: [ +| LIST0 ( OPT all_attrs [ command | ltac_expr ] "." ) +] + +all_attrs: [ +| LIST0 ( "#[" LIST0 attr SEP "," "]" ) OPT legacy_attrs +] + +attr: [ +| ident OPT attr_value +] + +attr_value: [ +| "=" string +| "(" LIST0 attr SEP "," ")" +] + +legacy_attrs: [ +| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" +] + sort: [ | "Set" | "Prop" @@ -208,6 +207,10 @@ universe_name: [ | "Prop" ] +univ_annot: [ +| "@{" LIST0 universe_level "}" +] + universe_level: [ | "Set" | "Prop" @@ -216,8 +219,12 @@ universe_level: [ | qualid ] -univ_annot: [ -| "@{" LIST0 universe_level "}" +univ_decl: [ +| "@{" LIST0 ident OPT "+" OPT [ "|" LIST0 univ_constraint SEP "," OPT "+" ] "}" +] + +univ_constraint: [ +| universe_name [ "<" | "=" | "<=" ] universe_name ] term_fix: [ @@ -226,7 +233,7 @@ term_fix: [ ] fix_body: [ -| ident LIST0 binder OPT fixannot OPT ( ":" term ) ":=" term +| ident LIST0 binder OPT fixannot OPT ( ":" type ) ":=" term ] fixannot: [ @@ -246,12 +253,12 @@ term_cofix: [ ] cofix_body: [ -| ident LIST0 binder OPT ( ":" term ) ":=" term +| ident LIST0 binder OPT ( ":" type ) ":=" term ] term_let: [ -| "let" name OPT ( ":" term ) ":=" term "in" term -| "let" name LIST1 binder OPT ( ":" term ) ":=" term "in" term +| "let" name OPT ( ":" type ) ":=" term "in" term +| "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term | "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term | "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term | "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term @@ -269,13 +276,15 @@ name: [ binder: [ | name -| "(" LIST1 name ":" term ")" -| "(" name OPT ( ":" term ) ":=" term ")" -| "{" LIST1 name OPT ( ":" term ) "}" +| "(" LIST1 name ":" type ")" +| "(" name OPT ( ":" type ) ":=" term ")" +| "(" name ":" type "|" term ")" +| "{" LIST1 name OPT ( ":" type ) "}" +| "[" LIST1 name OPT ( ":" type ) "]" | "`(" LIST1 typeclass_constraint SEP "," ")" | "`{" LIST1 typeclass_constraint SEP "," "}" +| "`[" LIST1 typeclass_constraint SEP "," "]" | "'" pattern0 -| "(" name ":" term "|" term ")" ] typeclass_constraint: [ @@ -359,17 +368,20 @@ subprf: [ ] gallina: [ -| thm_token ident_decl LIST0 binder ":" term LIST0 [ "with" ident_decl LIST0 binder ":" term ] -| assumption_token inline assum_list -| assumptions_token inline assum_list -| def_token ident_decl def_body +| thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] +| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] +| [ "Definition" | "Example" ] ident_decl def_body | "Let" ident def_body -| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" -| "Fixpoint" LIST1 fix_definition SEP "with" -| "Let" "Fixpoint" LIST1 fix_definition SEP "with" -| "CoFixpoint" LIST1 cofix_definition SEP "with" -| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with" -| "Scheme" LIST1 scheme SEP "with" +| "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) +| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition ) +| "Variant" inductive_definition LIST0 ( "with" inductive_definition ) +| [ "Record" | "Structure" ] inductive_definition LIST0 ( "with" inductive_definition ) +| "Class" inductive_definition LIST0 ( "with" inductive_definition ) +| "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) +| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) +| "Scheme" scheme LIST0 ( "with" scheme ) | "Combined" "Scheme" ident "from" LIST1 ident SEP "," | "Register" qualid "as" qualid | "Register" "Inline" qualid @@ -380,7 +392,15 @@ gallina: [ ] fix_definition: [ -| ident_decl LIST0 binder OPT fixannot OPT ( ":" term ) OPT [ ":=" term ] decl_notation +| ident_decl LIST0 binder OPT fixannot OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations +] + +decl_notations: [ +| "where" decl_notation LIST0 ( "and" decl_notation ) +] + +decl_notation: [ +| string ":=" term1_extended OPT [ ":" ident ] ] register_token: [ @@ -444,80 +464,23 @@ thm_token: [ | "Property" ] -def_token: [ -| "Definition" -| "Example" -| "SubClass" -] - -assumption_token: [ -| "Hypothesis" -| "Variable" -| "Axiom" -| "Parameter" -| "Conjecture" -] - -assumptions_token: [ -| "Hypotheses" -| "Variables" -| "Axioms" -| "Parameters" -| "Conjectures" -] - -inline: [ -| "Inline" "(" num ")" -| "Inline" -| -] - -univ_constraint: [ -| universe_name [ "<" | "=" | "<=" ] universe_name -] - -ident_decl: [ -| ident OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) -] - -finite_token: [ -| "Inductive" -| "CoInductive" -| "Variant" -| "Record" -| "Structure" -| "Class" -] - -cumulativity_token: [ -| "Cumulative" -| "NonCumulative" -] - -private_token: [ -| "Private" -| -] - def_body: [ -| LIST0 binder ":=" reduce term -| LIST0 binder ":" term ":=" reduce term -| LIST0 binder ":" term +| LIST0 binder OPT ( ":" type ) ":=" OPT reduce term +| LIST0 binder ":" type ] reduce: [ | "Eval" red_expr "in" -| ] red_expr: [ | "red" | "hnf" -| "simpl" delta_flag OPT ref_or_pattern_occ -| "cbv" strategy_flag -| "cbn" strategy_flag -| "lazy" strategy_flag -| "compute" delta_flag +| "simpl" OPT delta_flag OPT ref_or_pattern_occ +| "cbv" OPT strategy_flag +| "cbn" OPT strategy_flag +| "lazy" OPT strategy_flag +| "compute" OPT delta_flag | "vm_compute" OPT ref_or_pattern_occ | "native_compute" OPT ref_or_pattern_occ | "unfold" LIST1 unfold_occ SEP "," @@ -526,6 +489,19 @@ red_expr: [ | ident ] +delta_flag: [ +| OPT "-" "[" LIST1 smart_global "]" +] + +smart_global: [ +| qualid +| by_notation +] + +by_notation: [ +| string OPT [ "%" ident ] +] + strategy_flag: [ | LIST1 red_flags | delta_flag @@ -538,70 +514,71 @@ red_flags: [ | "fix" | "cofix" | "zeta" -| "delta" delta_flag +| "delta" OPT delta_flag ] -delta_flag: [ -| "-" "[" LIST1 smart_global "]" -| "[" LIST1 smart_global "]" -| +ref_or_pattern_occ: [ +| smart_global OPT ( "at" occs_nums ) +| term1_extended OPT ( "at" occs_nums ) ] -ref_or_pattern_occ: [ -| smart_global occs -| term1_extended occs +occs_nums: [ +| LIST1 num_or_var +| "-" num_or_var LIST0 int_or_var ] -unfold_occ: [ -| smart_global occs +num_or_var: [ +| num +| ident ] -opt_constructors_or_fields: [ -| ":=" constructor_list_or_record_decl -| +int_or_var: [ +| int +| ident ] -inductive_definition: [ -| opt_coercion ident_decl LIST0 binder OPT [ ":" term ] opt_constructors_or_fields decl_notation +unfold_occ: [ +| smart_global OPT ( "at" occs_nums ) ] -opt_coercion: [ -| ">" -| +pattern_occ: [ +| term1_extended OPT ( "at" occs_nums ) ] -constructor_list_or_record_decl: [ -| "|" LIST1 constructor SEP "|" -| ident constructor_type "|" LIST0 constructor SEP "|" -| ident constructor_type -| ident "{" record_fields "}" -| "{" record_fields "}" -| +finite_token: [ +| "Inductive" +| "CoInductive" +| "Variant" +| "Record" +| "Structure" +| "Class" ] -assum_list: [ -| LIST1 assum_coe -| simple_assum_coe +inductive_definition: [ +| OPT ">" ident_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] OPT ( ":=" OPT constructors_or_record ) OPT decl_notations ] -assum_coe: [ -| "(" simple_assum_coe ")" +constructors_or_record: [ +| OPT "|" LIST1 constructor SEP "|" +| OPT ident "{" LIST1 record_field SEP ";" "}" ] -simple_assum_coe: [ -| LIST1 ident_decl of_type_with_opt_coercion term +constructor: [ +| ident LIST0 binder OPT of_type ] -constructor_type: [ -| LIST0 binder [ of_type_with_opt_coercion term | ] +record_field: [ +| LIST0 ( "#[" LIST0 attr SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations ] -constructor: [ -| ident constructor_type +field_body: [ +| LIST0 binder of_type +| LIST0 binder of_type ":=" term +| LIST0 binder ":=" term ] cofix_definition: [ -| ident_decl LIST0 binder OPT ( ":" term ) OPT [ ":=" term ] decl_notation +| ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations ] scheme: [ @@ -624,25 +601,16 @@ sort_family: [ | "Type" ] -smart_global: [ -| qualid -| by_notation -] - -by_notation: [ -| string OPT [ "%" ident ] -] - gallina_ext: [ -| "Module" export_token ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) of_module_type is_module_expr -| "Module" "Type" ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) LIST0 ( "<:" module_type_inl ) is_module_type -| "Declare" "Module" export_token ident LIST0 ( "(" export_token LIST1 ident ":" module_type_inl ")" ) ":" module_type_inl +| "Module" OPT export_token ident LIST0 module_binder of_module_type OPT is_module_expr +| "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT is_module_type +| "Declare" "Module" OPT export_token ident LIST0 module_binder ":" module_type_inl | "Section" ident | "Chapter" ident | "End" ident | "Collection" ident ":=" section_subset_expr -| "Require" export_token LIST1 qualid -| "From" qualid "Require" export_token LIST1 qualid +| "Require" OPT export_token LIST1 qualid +| "From" qualid "Require" OPT export_token LIST1 qualid | "Import" LIST1 qualid | "Export" LIST1 qualid | "Include" module_type_inl LIST0 ( "<+" module_expr_inl ) @@ -650,9 +618,9 @@ gallina_ext: [ | "Transparent" LIST1 smart_global | "Opaque" LIST1 smart_global | "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ] -| "Canonical" OPT "Structure" qualid OPT [ OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) def_body ] +| "Canonical" OPT "Structure" qualid OPT [ OPT univ_decl def_body ] | "Canonical" OPT "Structure" by_notation -| "Coercion" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) def_body +| "Coercion" qualid OPT univ_decl def_body | "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr | "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr | "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr @@ -661,7 +629,7 @@ gallina_ext: [ | "Existing" "Instance" qualid hint_info | "Existing" "Instances" LIST1 qualid OPT [ "|" num ] | "Existing" "Class" qualid -| "Arguments" smart_global LIST0 argument_spec_block OPT [ "," LIST1 [ LIST0 more_implicits_block ] SEP "," ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] | "Implicit" "Type" reserv_list | "Implicit" "Types" reserv_list | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ] @@ -689,43 +657,41 @@ hint_info: [ export_token: [ | "Import" | "Export" -| ] -of_module_type: [ -| ":" module_type_inl -| LIST0 ( "<:" module_type_inl ) +module_binder: [ +| "(" OPT export_token LIST1 ident ":" module_type_inl ")" ] -is_module_type: [ -| ":=" module_type_inl LIST0 ( "<+" module_type_inl ) -| +module_type_inl: [ +| "!" module_type +| module_type OPT functor_app_annot ] -is_module_expr: [ -| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl ) -| +module_type: [ +| qualid +| "(" module_type ")" +| module_type module_expr_atom +| module_type "with" with_declaration +] + +with_declaration: [ +| "Definition" qualid OPT univ_decl ":=" term +| "Module" qualid ":=" qualid ] functor_app_annot: [ | "[" "inline" "at" "level" num "]" | "[" "no" "inline" "]" -| -] - -module_expr_inl: [ -| "!" module_expr -| module_expr functor_app_annot ] -module_type_inl: [ -| "!" module_type -| module_type functor_app_annot +of_module_type: [ +| ":" module_type_inl +| LIST0 ( "<:" module_type_inl ) ] -module_expr: [ -| module_expr_atom -| module_expr module_expr_atom +is_module_type: [ +| ":=" module_type_inl LIST0 ( "<+" module_type_inl ) ] module_expr_atom: [ @@ -733,25 +699,31 @@ module_expr_atom: [ | "(" module_expr ")" ] -module_type: [ -| qualid -| "(" module_type ")" -| module_type module_expr_atom -| module_type "with" with_declaration +module_expr: [ +| module_expr_atom +| module_expr module_expr_atom ] -with_declaration: [ -| "Definition" qualid OPT ( "@{" LIST0 ident [ "+" | ] [ "|" LIST0 univ_constraint SEP "," [ "+" | ] "}" | [ "}" | "|}" ] ] ) ":=" term -| "Module" qualid ":=" qualid +is_module_expr: [ +| ":=" module_expr_inl LIST0 ( "<+" module_expr_inl ) +] + +module_expr_inl: [ +| "!" module_expr +| module_expr OPT functor_app_annot ] argument_spec_block: [ -| OPT "!" name OPT ( "%" ident ) +| argument_spec | "/" | "&" -| "(" LIST1 ( OPT "!" name OPT ( "%" ident ) ) ")" OPT ( "%" ident ) -| "[" LIST1 ( OPT "!" name OPT ( "%" ident ) ) "]" OPT ( "%" ident ) -| "{" LIST1 ( OPT "!" name OPT ( "%" ident ) ) "}" OPT ( "%" ident ) +| "(" LIST1 argument_spec ")" OPT ( "%" ident ) +| "[" LIST1 argument_spec "]" OPT ( "%" ident ) +| "{" LIST1 argument_spec "}" OPT ( "%" ident ) +] + +argument_spec: [ +| OPT "!" name OPT ( "%" ident ) ] more_implicits_block: [ @@ -760,6 +732,20 @@ more_implicits_block: [ | "{" LIST1 name "}" ] +arguments_modifier: [ +| "simpl" "nomatch" +| "simpl" "never" +| "default" "implicits" +| "clear" "bidirectionality" "hint" +| "clear" "implicits" +| "clear" "scopes" +| "clear" "scopes" "and" "implicits" +| "clear" "implicits" "and" "scopes" +| "rename" +| "assert" +| "extra" "scopes" +] + strategy_level: [ | "expand" | "opaque" @@ -785,20 +771,6 @@ simple_reserv: [ | LIST1 ident ":" term ] -arguments_modifier: [ -| "simpl" "nomatch" -| "simpl" "never" -| "default" "implicits" -| "clear" "implicits" -| "clear" "scopes" -| "clear" "bidirectionality" "hint" -| "rename" -| "assert" -| "extra" "scopes" -| "clear" "scopes" "and" "implicits" -| "clear" "implicits" "and" "scopes" -] - command: [ | "Goal" term | "Declare" "Scope" ident @@ -812,7 +784,43 @@ command: [ | "Add" "Rec" "LoadPath" string as_dirpath | "Remove" "LoadPath" string | "Type" term -| "Print" printable +| "Print" "Term" smart_global OPT ( "@{" LIST0 name "}" ) +| "Print" "All" +| "Print" "Section" qualid +| "Print" "Grammar" ident +| "Print" "Custom" "Grammar" ident +| "Print" "LoadPath" OPT dirpath +| "Print" "Modules" +| "Print" "Libraries" +| "Print" "ML" "Path" +| "Print" "ML" "Modules" +| "Print" "Debug" "GC" +| "Print" "Graph" +| "Print" "Classes" +| "Print" "TypeClasses" +| "Print" "Instances" smart_global +| "Print" "Coercions" +| "Print" "Coercion" "Paths" class_rawexpr class_rawexpr +| "Print" "Canonical" "Projections" LIST0 smart_global +| "Print" "Typing" "Flags" +| "Print" "Tables" +| "Print" "Options" +| "Print" "Hint" +| "Print" "Hint" smart_global +| "Print" "Hint" "*" +| "Print" "HintDb" ident +| "Print" "Scopes" +| "Print" "Scope" ident +| "Print" "Visibility" OPT ident +| "Print" "Implicit" smart_global +| "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string +| "Print" "Assumptions" smart_global +| "Print" "Opaque" "Dependencies" smart_global +| "Print" "Transparent" "Dependencies" smart_global +| "Print" "All" "Dependencies" smart_global +| "Print" "Strategy" smart_global +| "Print" "Strategies" +| "Print" "Registered" | "Print" smart_global OPT ( "@{" LIST0 name "}" ) | "Print" "Module" "Type" qualid | "Print" "Module" qualid @@ -931,6 +939,7 @@ command: [ | "Show" "Ltac" "Profile" | "Show" "Ltac" "Profile" "CutOff" int | "Show" "Ltac" "Profile" string +| "Show" "Lia" "Profile" (* micromega plugin *) | "Add" "InjTyp" term1_extended (* micromega plugin *) | "Add" "BinOp" term1_extended (* micromega plugin *) | "Add" "UnOp" term1_extended (* micromega plugin *) @@ -959,12 +968,12 @@ command: [ | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid | "Locate" "Ltac" qualid -| "Ltac" LIST1 tacdef_body SEP "with" +| "Ltac" tacdef_body LIST0 ( "with" tacdef_body ) | "Print" "Ltac" "Signatures" | "Set" "Firstorder" "Solver" ltac_expr | "Print" "Firstorder" "Solver" -| "Function" LIST1 fix_definition SEP "with" (* funind plugin *) -| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) +| "Function" fix_definition LIST0 ( "with" fix_definition ) +| "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg ) | "Extraction" qualid (* extraction plugin *) | "Recursive" "Extraction" LIST1 qualid (* extraction plugin *) | "Extraction" string LIST1 qualid (* extraction plugin *) @@ -1002,8 +1011,9 @@ command: [ | "Print" "Rings" (* setoid_ring plugin *) | "Add" "Field" ident ":" term1_extended OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) | "Print" "Fields" (* setoid_ring plugin *) -| "Numeral" "Notation" qualid qualid qualid ":" ident numnotoption +| "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption | "String" "Notation" qualid qualid qualid ":" ident +| "SubClass" ident_decl def_body ] orient: [ @@ -1043,46 +1053,6 @@ starredidentref: [ | "Type" "*" ] -printable: [ -| "Term" smart_global OPT ( "@{" LIST0 name "}" ) -| "All" -| "Section" qualid -| "Grammar" ident -| "Custom" "Grammar" ident -| "LoadPath" OPT dirpath -| "Modules" -| "Libraries" -| "ML" "Path" -| "ML" "Modules" -| "Debug" "GC" -| "Graph" -| "Classes" -| "TypeClasses" -| "Instances" smart_global -| "Coercions" -| "Coercion" "Paths" class_rawexpr class_rawexpr -| "Canonical" "Projections" -| "Typing" "Flags" -| "Tables" -| "Options" -| "Hint" -| "Hint" smart_global -| "Hint" "*" -| "HintDb" ident -| "Scopes" -| "Scope" ident -| "Visibility" OPT ident -| "Implicit" smart_global -| [ "Sorted" | ] "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string -| "Assumptions" smart_global -| "Opaque" "Dependencies" smart_global -| "Transparent" "Dependencies" smart_global -| "All" "Dependencies" smart_global -| "Strategy" smart_global -| "Strategies" -| "Registered" -] - dirpath: [ | ident | dirpath field_ident @@ -1160,7 +1130,6 @@ ltac_production_item: [ ] numnotoption: [ -| | "(" "warning" "after" num ")" | "(" "abstract" "after" num ")" ] @@ -1288,17 +1257,12 @@ syntax: [ | "Delimit" "Scope" ident "with" ident | "Undelimit" "Scope" ident | "Bind" "Scope" ident "with" LIST1 class_rawexpr -| "Infix" string ":=" term1_extended [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" ident ] -| "Notation" ident LIST0 ident ":=" term1_extended only_parsing -| "Notation" string ":=" term1_extended [ "(" LIST1 syntax_modifier SEP "," ")" | ] OPT [ ":" ident ] +| "Infix" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] +| "Notation" ident LIST0 ident ":=" term1_extended OPT ( "(" "only" "parsing" ")" ) +| "Notation" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] | "Format" "Notation" string string string -| "Reserved" "Infix" string [ "(" LIST1 syntax_modifier SEP "," ")" | ] -| "Reserved" "Notation" string [ "(" LIST1 syntax_modifier SEP "," ")" | ] -] - -only_parsing: [ -| "(" "only" "parsing" ")" -| +| "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] +| "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] ] level: [ @@ -1317,31 +1281,35 @@ syntax_modifier: [ | "only" "parsing" | "format" string OPT string | ident "," LIST1 ident SEP "," "at" level -| ident "at" level -| ident "at" level constr_as_binder_kind +| ident "at" level OPT constr_as_binder_kind | ident constr_as_binder_kind | ident syntax_extension_type ] +constr_as_binder_kind: [ +| "as" "ident" +| "as" "pattern" +| "as" "strict" "pattern" +] + syntax_extension_type: [ | "ident" | "global" | "bigint" | "binder" | "constr" -| "constr" OPT ( "at" level ) OPT constr_as_binder_kind +| "constr" at_level_opt OPT constr_as_binder_kind | "pattern" | "pattern" "at" "level" num | "strict" "pattern" | "strict" "pattern" "at" "level" num | "closed" "binder" -| "custom" ident OPT ( "at" level ) OPT constr_as_binder_kind +| "custom" ident at_level_opt OPT constr_as_binder_kind ] -constr_as_binder_kind: [ -| "as" "ident" -| "as" "pattern" -| "as" "strict" "pattern" +at_level_opt: [ +| "at" level +| ] simple_tactic: [ @@ -1591,7 +1559,7 @@ simple_tactic: [ | "eenough" term1_extended as_ipat by_tactic | "generalize" term1_extended | "generalize" term1_extended LIST1 term1_extended -| "generalize" term1_extended occs as_name LIST0 [ "," pattern_occ as_name ] +| "generalize" term1_extended OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ] | "induction" induction_clause_list | "einduction" induction_clause_list | "destruct" induction_clause_list @@ -1605,11 +1573,11 @@ simple_tactic: [ | "inversion" quantified_hypothesis "using" term1_extended in_hyp_list | "red" clause_dft_concl | "hnf" clause_dft_concl -| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl -| "cbv" strategy_flag clause_dft_concl -| "cbn" strategy_flag clause_dft_concl -| "lazy" strategy_flag clause_dft_concl -| "compute" delta_flag clause_dft_concl +| "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl +| "cbv" OPT strategy_flag clause_dft_concl +| "cbn" OPT strategy_flag clause_dft_concl +| "lazy" OPT strategy_flag clause_dft_concl +| "compute" OPT delta_flag clause_dft_concl | "vm_compute" OPT ref_or_pattern_occ clause_dft_concl | "native_compute" OPT ref_or_pattern_occ clause_dft_concl | "unfold" LIST1 unfold_occ SEP "," clause_dft_concl @@ -1631,7 +1599,6 @@ simple_tactic: [ | "functional" "inversion" quantified_hypothesis OPT qualid (* funind plugin *) | "functional" "induction" LIST1 term1_extended fun_ind_using with_names (* funind plugin *) | "soft" "functional" "induction" LIST1 term1_extended fun_ind_using with_names (* funind plugin *) -| "myred" (* micromega plugin *) | "psatz_Z" int_or_var ltac_expr (* micromega plugin *) | "psatz_Z" ltac_expr (* micromega plugin *) | "xlia" ltac_expr (* micromega plugin *) @@ -1647,24 +1614,18 @@ simple_tactic: [ | "psatz_R" ltac_expr (* micromega plugin *) | "psatz_Q" int_or_var ltac_expr (* micromega plugin *) | "psatz_Q" ltac_expr (* micromega plugin *) -| "iter_specs" ltac_expr (* micromega plugin *) +| "zify_iter_specs" ltac_expr (* micromega plugin *) | "zify_op" (* micromega plugin *) -| "saturate" (* micromega plugin *) +| "zify_saturate" (* micromega plugin *) +| "zify_iter_let" ltac_expr (* micromega plugin *) | "nsatz_compute" term1_extended (* nsatz plugin *) | "omega" (* omega plugin *) -| "omega" "with" LIST1 ident (* omega plugin *) -| "omega" "with" "*" (* omega plugin *) | "protect_fv" string "in" ident (* setoid_ring plugin *) | "protect_fv" string (* setoid_ring plugin *) | "ring_lookup" ltac_expr0 "[" LIST0 term1_extended "]" LIST1 term1_extended (* setoid_ring plugin *) | "field_lookup" ltac_expr "[" LIST0 term1_extended "]" LIST1 term1_extended (* setoid_ring plugin *) ] -int_or_var: [ -| int -| ident -] - hloc: [ | | "in" "|-" "*" @@ -1686,17 +1647,12 @@ by_arg_tac: [ in_clause: [ | in_clause -| "*" occs +| "*" OPT ( "at" occs_nums ) | "*" "|-" concl_occ | LIST0 hypident_occ SEP "," "|-" concl_occ | LIST0 hypident_occ SEP "," ] -occs: [ -| "at" occs_nums -| -] - as_ipat: [ | "as" simple_intropattern | @@ -1809,10 +1765,6 @@ bindings: [ | LIST1 term1_extended ] -pattern_occ: [ -| term1_extended occs -] - comparison: [ | "=" | "<" @@ -1838,12 +1790,12 @@ hypident: [ ] hypident_occ: [ -| hypident occs +| hypident OPT ( "at" occs_nums ) ] clause_dft_concl: [ | "in" in_clause -| occs +| OPT ( "at" occs_nums ) | ] @@ -1858,18 +1810,8 @@ opt_clause: [ | ] -occs_nums: [ -| LIST1 num_or_var -| "-" num_or_var LIST0 int_or_var -] - -num_or_var: [ -| num -| ident -] - concl_occ: [ -| "*" occs +| "*" OPT ( "at" occs_nums ) | ] @@ -1987,7 +1929,7 @@ ltac_expr: [ binder_tactic: [ | "fun" LIST1 fun_var "=>" ltac_expr -| "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr +| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr | "info" ltac_expr ] @@ -2005,16 +1947,15 @@ let_clause: [ ltac_expr4: [ | ltac_expr3 ";" binder_tactic | ltac_expr3 ";" ltac_expr3 -| ltac_expr3 ";" "[" multi_goal_tactics "]" -| ltac_expr3 ";" "[" ">" multi_goal_tactics "]" +| ltac_expr3 ";" "[" OPT multi_goal_tactics "]" | ltac_expr3 +| ltac_expr3 ";" "[" ">" OPT multi_goal_tactics "]" ] multi_goal_tactics: [ | OPT ltac_expr "|" multi_goal_tactics | ltac_expr_opt ".." OPT "|" ltac_expr_opt_list_or | ltac_expr -| ] ltac_expr_opt: [ @@ -2044,6 +1985,20 @@ ltac_expr3: [ | ltac_expr2 ] +only_selector: [ +| "only" selector ":" +] + +selector: [ +| LIST1 range_selector SEP "," +| "[" ident "]" +] + +range_selector: [ +| num "-" num +| num +] + ltac_expr2: [ | ltac_expr1 "+" binder_tactic | ltac_expr1 "+" ltac_expr2 @@ -2058,7 +2013,7 @@ ltac_expr1: [ | "first" "[" LIST0 ltac_expr SEP "|" "]" | "solve" "[" LIST0 ltac_expr SEP "|" "]" | "idtac" LIST0 message_token -| failkw [ int_or_var | ] LIST0 message_token +| failkw OPT int_or_var LIST0 message_token | ltac_match_goal | simple_tactic | tactic_arg @@ -2099,7 +2054,7 @@ tactic_arg_compat: [ ltac_expr0: [ | "(" ltac_expr ")" -| "[>" multi_goal_tactics "]" +| "[>" OPT multi_goal_tactics "]" | tactic_atom ] @@ -2115,20 +2070,6 @@ toplevel_selector: [ | "!" ":" ] -only_selector: [ -| "only" selector ":" -] - -selector: [ -| LIST1 range_selector SEP "," -| "[" ident "]" -] - -range_selector: [ -| num "-" num -| num -] - ltac_match_term: [ | match_key ltac_expr "with" OPT "|" LIST1 match_rule SEP "|" "end" ] diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg index 8170b71e7a..93eb38d1a0 100644 --- a/doc/tools/docgram/productionlist.edit_mlg +++ b/doc/tools/docgram/productionlist.edit_mlg @@ -12,19 +12,3 @@ (* Contents used to generate productionlists in doc *) DOC_GRAMMAR - -(* this is here because they're inside _opt generated by EXPAND *) -SPLICE: [ -| ltac_info -| eliminator -| field_mods -| ltac_production_sep -| ltac_tactic_level -| module_binder -| printunivs_subgraph -| quoted_attributes -| ring_mods -| scope_delimiter -| univ_decl -| univ_name_list -] |