From 3a25b967a944fe37e1ad54e54a904d90311ef381 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 09:13:44 +0200 Subject: Renaming numnotoption into number_modifier --- doc/tools/docgram/common.edit_mlg | 10 +++++----- doc/tools/docgram/fullGrammar | 6 +++--- doc/tools/docgram/orderedGrammar | 7 ++++--- 3 files changed, 12 insertions(+), 11 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index f6a684bbd7..5d0f9208fc 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Numeral" "Notation" reference reference reference ":" ident numeral_modifier -| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier -| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier -| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier +| REPLACE "Numeral" "Notation" reference reference reference ":" ident number_modifier +| WITH "Numeral" "Notation" reference reference reference ":" scope_name number_modifier +| REPLACE "Number" "Notation" reference reference reference ":" ident number_modifier +| WITH "Number" "Notation" reference reference reference ":" scope_name number_modifier | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name @@ -1358,7 +1358,7 @@ explicit_subentry: [ | DELETE "constr" (* covered by another prod *) ] -numeral_modifier: [ +number_modifier: [ | OPTINREF ] diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index c764cb6f37..914347b4cf 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,8 +686,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference reference reference ":" ident numeral_modifier -| "Numeral" "Notation" reference reference reference ":" ident numeral_modifier +| "Number" "Notation" reference reference reference ":" ident number_modifier +| "Numeral" "Notation" reference reference reference ":" ident number_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) @@ -2549,7 +2549,7 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] -numeral_modifier: [ +number_modifier: [ | | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 12a7bc684d..a972ad4719 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier +| "Number" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,6 +910,7 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -1269,7 +1270,7 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -numeral_modifier: [ +number_modifier: [ | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] -- cgit v1.2.3 From 11a8997dd8fa83537607272692a3baf10dab342a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:12:00 +0200 Subject: [numeral notation] Adding the via ... using ... option This enables numeral notations for non inductive types by pre/postprocessing them to a given proxy inductive type. For instance, this should enable the use of numeral notations for R. --- doc/tools/docgram/common.edit_mlg | 8 ++++---- doc/tools/docgram/fullGrammar | 12 ++++++++++-- doc/tools/docgram/orderedGrammar | 14 +++++++++++--- 3 files changed, 25 insertions(+), 9 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 5d0f9208fc..4d615a130a 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Numeral" "Notation" reference reference reference ":" ident number_modifier -| WITH "Numeral" "Notation" reference reference reference ":" scope_name number_modifier -| REPLACE "Number" "Notation" reference reference reference ":" ident number_modifier -| WITH "Number" "Notation" reference reference reference ":" scope_name number_modifier +| REPLACE "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| WITH "Number" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier +| REPLACE "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| WITH "Numeral" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 914347b4cf..8a0feb0e2f 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,8 +686,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference reference reference ":" ident number_modifier -| "Numeral" "Notation" reference reference reference ":" ident number_modifier +| "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) @@ -2555,6 +2555,14 @@ number_modifier: [ | "(" "abstract" "after" bignat ")" ] +number_using: [ +| reference reference +] + +number_via: [ +| "via" reference "using" "(" LIST1 number_using SEP "," ")" +] + tac2pat1: [ | Prim.qualid LIST1 tac2pat0 (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index a972ad4719..d12b3bf6cd 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier +| "Number" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier +| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,7 +910,7 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier +| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -1275,6 +1275,14 @@ number_modifier: [ | "(" "abstract" "after" bignat ")" ] +number_using: [ +| qualid qualid +] + +number_via: [ +| "via" qualid "using" "(" LIST1 number_using SEP "," ")" +] + hints_path: [ | "(" hints_path ")" | hints_path "*" -- cgit v1.2.3 From c217bbe80e18255ee3e67fa6266736529d80636d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:14:00 +0200 Subject: [numeral notation] Document the via ... using ... option --- doc/tools/docgram/common.edit_mlg | 14 ++++++-------- doc/tools/docgram/fullGrammar | 22 ++++++++++++++++------ doc/tools/docgram/orderedGrammar | 16 +++++++++------- 3 files changed, 31 insertions(+), 21 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4d615a130a..e43583de09 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1285,10 +1285,10 @@ command: [ | WITH "Declare" "Scope" scope_name (* odd that these are in command while other notation-related ones are in syntax *) -| REPLACE "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier -| WITH "Number" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier -| REPLACE "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier -| WITH "Numeral" "Notation" reference OPT number_via reference reference ":" scope_name number_modifier +| REPLACE "Number" "Notation" reference reference reference OPT number_options ":" ident +| WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name +| REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier +| WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier | REPLACE "String" "Notation" reference reference reference ":" ident | WITH "String" "Notation" reference reference reference ":" scope_name @@ -1358,10 +1358,6 @@ explicit_subentry: [ | DELETE "constr" (* covered by another prod *) ] -number_modifier: [ -| OPTINREF -] - binder_tactic: [ | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" ltac_expr5 | WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr5 @@ -2464,6 +2460,8 @@ SPLICE: [ | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) +| number_mapping +| number_options ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 8a0feb0e2f..17fc220f6c 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -686,8 +686,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" reference OPT number_via reference reference ":" ident number_modifier -| "Numeral" "Notation" reference OPT number_via reference reference ":" ident number_modifier +| "Number" "Notation" reference reference reference OPT number_options ":" ident +| "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier | "String" "Notation" reference reference reference ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) @@ -2549,18 +2549,28 @@ field_mods: [ | "(" LIST1 field_mod SEP "," ")" (* ring plugin *) ] -number_modifier: [ +deprecated_number_modifier: [ | | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] -number_using: [ -| reference reference +number_mapping: [ +| reference "=>" reference ] number_via: [ -| "via" reference "using" "(" LIST1 number_using SEP "," ")" +| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]" +] + +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_via +] + +number_options: [ +| "(" LIST1 number_modifier SEP "," ")" ] tac2pat1: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index d12b3bf6cd..3d1041e592 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,6 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier -| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,7 +908,8 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term -| "Numeral" "Notation" qualid OPT number_via qualid qualid ":" scope_name OPT number_modifier +| "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name +| "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -1270,17 +1269,20 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -number_modifier: [ +deprecated_number_modifier: [ +| | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] -number_using: [ -| qualid qualid +number_modifier: [ +| "warning" "after" bignat +| "abstract" "after" bignat +| number_via ] number_via: [ -| "via" qualid "using" "(" LIST1 number_using SEP "," ")" +| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]" ] hints_path: [ -- cgit v1.2.3 From 0520decfdc94d52a2f8658b9cf6a730e6d333f8f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:23:00 +0200 Subject: [numeral notation] Handle implicit arguments --- doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'doc/tools') diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 17fc220f6c..3a0c3a8bc7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -2557,6 +2557,7 @@ deprecated_number_modifier: [ number_mapping: [ | reference "=>" reference +| "[" reference "]" "=>" reference ] number_via: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 3d1041e592..13d8979208 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1282,7 +1282,7 @@ number_modifier: [ ] number_via: [ -| "via" qualid "mapping" "[" LIST1 ( qualid "=>" qualid ) SEP "," "]" +| "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" ] hints_path: [ -- cgit v1.2.3 From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:26:00 +0200 Subject: Merge numeral and string notation plugins --- doc/tools/docgram/doc_grammar.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index b7f1e18d2b..92bcd51528 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -538,12 +538,11 @@ let autoloaded_mlgs = [ (* in the order they are loaded by Coq *) "plugins/ltac/g_eqdecide.mlg"; "plugins/ltac/g_tactic.mlg"; "plugins/ltac/g_ltac.mlg"; - "plugins/syntax/g_string.mlg"; "plugins/btauto/g_btauto.mlg"; "plugins/rtauto/g_rtauto.mlg"; "plugins/cc/g_congruence.mlg"; "plugins/firstorder/g_ground.mlg"; - "plugins/syntax/g_numeral.mlg"; + "plugins/syntax/g_number_string.mlg"; ] -- cgit v1.2.3 From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:27:00 +0200 Subject: [string notation] Handle parameterized inductives and non inductives --- doc/tools/docgram/common.edit_mlg | 7 ++++--- doc/tools/docgram/fullGrammar | 14 +++++++++----- doc/tools/docgram/orderedGrammar | 6 +++--- 3 files changed, 16 insertions(+), 11 deletions(-) (limited to 'doc/tools') diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index e43583de09..5de1f09c53 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1289,8 +1289,8 @@ command: [ | WITH "Number" "Notation" reference reference reference OPT number_options ":" scope_name | REPLACE "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier | WITH "Numeral" "Notation" reference reference reference ":" scope_name deprecated_number_modifier -| REPLACE "String" "Notation" reference reference reference ":" ident -| WITH "String" "Notation" reference reference reference ":" scope_name +| REPLACE "String" "Notation" reference reference reference OPT string_option ":" ident +| WITH "String" "Notation" reference reference reference OPT string_option ":" scope_name | DELETE "Ltac2" ltac2_entry (* was split up *) | DELETE "Add" "Zify" "InjTyp" constr (* micromega plugin *) @@ -2460,8 +2460,9 @@ SPLICE: [ | constr_with_bindings | simple_binding | ssexpr35 (* strange in mlg, ssexpr50 is after this *) -| number_mapping +| number_string_mapping | number_options +| string_option ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 3a0c3a8bc7..826a0b6f36 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -688,7 +688,7 @@ command: [ | "Print" "Fields" (* ring plugin *) | "Number" "Notation" reference reference reference OPT number_options ":" ident | "Numeral" "Notation" reference reference reference ":" ident deprecated_number_modifier -| "String" "Notation" reference reference reference ":" ident +| "String" "Notation" reference reference reference OPT string_option ":" ident | "Ltac2" ltac2_entry (* Ltac2 plugin *) | "Ltac2" "Eval" ltac2_expr6 (* Ltac2 plugin *) | "Print" "Ltac2" reference (* Ltac2 plugin *) @@ -2555,25 +2555,29 @@ deprecated_number_modifier: [ | "(" "abstract" "after" bignat ")" ] -number_mapping: [ +number_string_mapping: [ | reference "=>" reference | "[" reference "]" "=>" reference ] -number_via: [ -| "via" reference "mapping" "[" LIST1 number_mapping SEP "," "]" +number_string_via: [ +| "via" reference "mapping" "[" LIST1 number_string_mapping SEP "," "]" ] number_modifier: [ | "warning" "after" bignat | "abstract" "after" bignat -| number_via +| number_string_via ] number_options: [ | "(" LIST1 number_modifier SEP "," ")" ] +string_option: [ +| "(" number_string_via ")" +] + tac2pat1: [ | Prim.qualid LIST1 tac2pat0 (* Ltac2 plugin *) | Prim.qualid (* Ltac2 plugin *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 13d8979208..151438bbbd 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -910,7 +910,7 @@ command: [ | "Declare" "Right" "Step" one_term | "Number" "Notation" qualid qualid qualid OPT ( "(" LIST1 number_modifier SEP "," ")" ) ":" scope_name | "Numeral" "Notation" qualid qualid qualid ":" scope_name deprecated_number_modifier -| "String" "Notation" qualid qualid qualid ":" scope_name +| "String" "Notation" qualid qualid qualid OPT ( "(" number_string_via ")" ) ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] | assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] @@ -1278,10 +1278,10 @@ deprecated_number_modifier: [ number_modifier: [ | "warning" "after" bignat | "abstract" "after" bignat -| number_via +| number_string_via ] -number_via: [ +number_string_via: [ | "via" qualid "mapping" "[" LIST1 [ qualid "=>" qualid | "[" qualid "]" "=>" qualid ] SEP "," "]" ] -- cgit v1.2.3