diff options
| author | Pierre-Marie Pédrot | 2018-07-03 16:42:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-02 09:27:47 +0200 |
| commit | 67e894bc9e25e68bb89c93c930d3c9eac3f8a16d (patch) | |
| tree | d2a03c98816fc68c5d427d6448b892d47e945a45 /coqpp/coqpp_parse.mly | |
| parent | 389aa51f37fda1a7a8490d1b4042b881aba730df (diff) | |
Handling VERNAC EXTEND in coqpp.
Diffstat (limited to 'coqpp/coqpp_parse.mly')
| -rw-r--r-- | coqpp/coqpp_parse.mly | 47 |
1 files changed, 45 insertions, 2 deletions
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index bf435fd247..31f234c37f 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -63,7 +63,8 @@ let parse_user_entry s sep = %token <string> STRING %token <int> INT %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED -%token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL +%token COMMAND CLASSIFIED BY AS +%token LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA %token EOF @@ -104,7 +105,49 @@ grammar_extend: ; vernac_extend: -| VERNAC EXTEND IDENT END { VernacExt } +| VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_rules END + { VernacExt { + vernacext_name = $4; + vernacext_entry = $2; + vernacext_class = $5; + vernacext_rules = $6; + } } +; + +vernac_entry: +| COMMAND { None } +| CODE { Some $1 } +; + +vernac_classifier: +| { ClassifDefault } +| CLASSIFIED BY CODE { ClassifCode $3 } +| CLASSIFIED AS IDENT { ClassifName $3 } +; + +vernac_rules: +| vernac_rule { [$1] } +| vernac_rule vernac_rules { $1 :: $2 } +; + +vernac_rule: +| PIPE LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE + { { + vernac_toks = $3; + vernac_depr = $5; + vernac_class= $6; + vernac_body = $8; + } } +; + +rule_deprecation: +| { false } +| DEPRECATED { true } +; + +rule_classifier: +| { None } +| FUN CODE { Some $2 } ; tactic_extend: |