diff options
Diffstat (limited to 'coqpp')
| -rw-r--r-- | coqpp/coqpp_ast.mli | 1 | ||||
| -rw-r--r-- | coqpp/coqpp_lex.mll | 1 | ||||
| -rw-r--r-- | coqpp/coqpp_main.ml | 13 | ||||
| -rw-r--r-- | coqpp/coqpp_parse.mly | 21 |
4 files changed, 28 insertions, 8 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 8e10ec49ce..81109887ba 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -103,6 +103,7 @@ type classification = type vernac_rule = { vernac_atts : (string * string) list option; + vernac_state: string option; vernac_toks : ext_token list; vernac_class : code option; vernac_depr : bool; diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index c38755943a..81ba8ad98c 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -130,6 +130,7 @@ rule extend = parse | space { extend lexbuf } | '\"' { string lexbuf } | '\n' { newline lexbuf; extend lexbuf } +| "![" { BANGBRACKET } | "#[" { HASHBRACKET } | '[' { LBRACKET } | ']' { RBRACKET } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index d33eef135f..90158c3aa3 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -347,9 +347,18 @@ let print_atts_right fmt = function let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in fprintf fmt "(Attributes.parse %s%a atts)" nota aux atts +let print_body_wrapper fmt r = + match r.vernac_state with + | Some "proof" -> + fprintf fmt "let proof = (%a) ~pstate:st.Vernacstate.proof in { st with Vernacstate.proof }" print_code r.vernac_body + | None -> + fprintf fmt "let () = %a in st" print_code r.vernac_body + | Some x -> + fatal ("unsupported state specifier: " ^ x) + let print_body_fun fmt r = - fprintf fmt "let coqpp_body %a%a ~st = let () = %a in st in " - print_binders r.vernac_toks print_atts_left r.vernac_atts print_code r.vernac_body + fprintf fmt "let coqpp_body %a%a ~st = @[%a@] in " + print_binders r.vernac_toks print_atts_left r.vernac_atts print_body_wrapper r let print_body fmt r = fprintf fmt "@[(%afun %a~atts@ ~st@ -> coqpp_body %a%a ~st)@]" diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index abe52ab46b..43ba990f6a 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -65,7 +65,7 @@ let parse_user_entry s sep = %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT %token RAW_PRINTED GLOB_PRINTED %token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS -%token HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR +%token BANGBRACKET HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA %token EOF @@ -209,13 +209,14 @@ vernac_rules: ; vernac_rule: -| PIPE vernac_attributes_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE +| PIPE vernac_attributes_opt vernac_state_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE { { vernac_atts = $2; - vernac_toks = $4; - vernac_depr = $6; - vernac_class= $7; - vernac_body = $9; + vernac_state= $3; + vernac_toks = $5; + vernac_depr = $7; + vernac_class= $8; + vernac_body = $10; } } ; @@ -235,6 +236,14 @@ vernac_attribute: | qualid_or_ident { ($1, $1) } ; +vernac_state_opt: +| { None } +| BANGBRACKET vernac_state RBRACKET { Some $2 } +; + +vernac_state: +| qualid_or_ident { $1 } + rule_deprecation: | { false } | DEPRECATED { true } |