Handling VERNAC EXTEND in coqpp.

4 files changed, 164 insertions, 47 deletions

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 956a916792..6f697f5d49 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -85,12 +85,31 @@ type tactic_ext = {
   tacext_rules : tactic_rule list;
 }
 
+type classification =
+| ClassifDefault
+| ClassifCode of code
+| ClassifName of string
+
+type vernac_rule = {
+  vernac_toks : ext_token list;
+  vernac_class : code option;
+  vernac_depr : bool;
+  vernac_body : code;
+}
+
+type vernac_ext = {
+  vernacext_name : string;
+  vernacext_entry : code option;
+  vernacext_class : classification;
+  vernacext_rules : vernac_rule list;
+}
+
 type node =
 | Code of code
 | Comment of string
 | DeclarePlugin of string
 | GramExt of grammar_ext
-| VernacExt
+| VernacExt of vernac_ext
 | TacticExt of tactic_ext
 
 type t = node list
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index 81a53e887b..d809b824df 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -95,12 +95,16 @@ rule extend = parse
 | "{" { start_ocaml lexbuf; ocaml lexbuf }
 | "GRAMMAR" { GRAMMAR }
 | "VERNAC" { VERNAC }
+| "COMMAND" { COMMAND }
 | "TACTIC" { TACTIC }
 | "EXTEND" { EXTEND }
 | "END" { END }
 | "DECLARE" { DECLARE }
 | "PLUGIN" { PLUGIN }
 | "DEPRECATED" { DEPRECATED }
+| "CLASSIFIED" { CLASSIFIED }
+| "BY" { BY }
+| "AS" { AS }
 (** Camlp5 specific keywords *)
 | "GLOBAL" { GLOBAL }
 | "FIRST" { FIRST }
@@ -122,6 +126,7 @@ rule extend = parse
 | ']' { RBRACKET }
 | '|' { PIPE }
 | "->" { ARROW }
+| "=>" { FUN }
 | ',' { COMMA }
 | ':' { COLON }
 | ';' { SEMICOLON }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 42d8528a8c..602620968d 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -64,6 +64,39 @@ let string_split s =
 
 let plugin_name = "__coq_plugin_name"
 
+let print_list fmt pr l =
+  let rec prl fmt = function
+  | [] -> ()
+  | [x] -> fprintf fmt "%a" pr x
+  | x :: l -> fprintf fmt "%a;@ %a" pr x prl l
+  in
+  fprintf fmt "@[<hv>[%a]@]" prl l
+
+let rec print_binders fmt = function
+| [] -> ()
+| ExtTerminal _ :: rem -> print_binders fmt rem
+| ExtNonTerminal (_, TokNone) :: rem ->
+  fprintf fmt "_@ %a" print_binders rem
+| ExtNonTerminal (_, TokName id) :: rem ->
+  fprintf fmt "%s@ %a" id print_binders rem
+
+let rec print_symbol fmt = function
+| Ulist1 s ->
+  fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s
+| Ulist1sep (s, sep) ->
+  fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep
+| Ulist0 s ->
+  fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s
+| Ulist0sep (s, sep) ->
+  fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep
+| Uopt s ->
+  fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s
+| Uentry e ->
+  fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l
+
 module GramExt :
 sig
 
@@ -104,14 +137,6 @@ let print_local fmt ext =
 
 let print_string fmt s = fprintf fmt "\"%s\"" s
 
-let print_list fmt pr l =
-  let rec prl fmt = function
-  | [] -> ()
-  | [x] -> fprintf fmt "%a" pr x
-  | x :: l -> fprintf fmt "%a;@ %a" pr x prl l
-  in
-  fprintf fmt "@[<hv>[%a]@]" prl l
-
 let print_opt fmt pr = function
 | None -> fprintf fmt "None"
 | Some x -> fprintf fmt "Some@ (%a)" pr x
@@ -268,6 +293,61 @@ let print_ast fmt ext =
 
 end
 
+module VernacExt :
+sig
+
+val print_ast : Format.formatter -> vernac_ext -> unit
+
+end =
+struct
+
+let print_rule_classifier fmt r = match r.vernac_class with
+| None -> fprintf fmt "None"
+| Some f -> fprintf fmt "Some @[(fun %a-> %s)@]" print_binders r.vernac_toks f.code
+
+let print_body fmt r =
+  fprintf fmt "@[(fun %a~atts@ ~st@ -> %s)@]"
+    print_binders r.vernac_toks r.vernac_body.code
+
+let rec print_sig fmt = function
+| [] -> fprintf fmt "@[Vernacentries.TyNil@]"
+| ExtTerminal s :: rem ->
+  fprintf fmt "@[Vernacentries.TyTerminal (\"%s\", %a)@]" s print_sig rem
+| ExtNonTerminal (symb, _) :: rem ->
+  fprintf fmt "@[Vernacentries.TyNonTerminal (%a, %a)@]"
+    print_symbol symb print_sig rem
+
+let print_rule fmt r =
+  fprintf fmt "Vernacentries.TyML (%b, %a, %a, %a)"
+    r.vernac_depr print_sig r.vernac_toks print_body r print_rule_classifier r
+
+let print_rules fmt rules =
+  print_list fmt (fun fmt r -> fprintf fmt "(%a)" print_rule r) rules
+
+let print_classifier fmt = function
+| ClassifDefault -> fprintf fmt ""
+| ClassifName "QUERY" ->
+  fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_query)"
+| ClassifName "SIDEFF" ->
+  fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_sideeff)"
+| ClassifName s -> fatal (Printf.sprintf "Unknown classifier %s" s)
+| ClassifCode c -> fprintf fmt "~classifier:(%s)" c.code
+
+let print_entry fmt = function
+| None -> fprintf fmt "None"
+| Some e -> fprintf fmt "Some (%s)" e.code
+
+let print_ast fmt ext =
+  let pr fmt () =
+    fprintf fmt "Vernacentries.vernac_extend ~command:\"%s\" %a ?entry:%a %a"
+      ext.vernacext_name print_classifier ext.vernacext_class
+      print_entry ext.vernacext_entry print_rules ext.vernacext_rules
+  in
+  let () = fprintf fmt "let () = @[%a@]@\n" pr () in
+  ()
+
+end
+
 module TacticExt :
 sig
 
@@ -276,49 +356,19 @@ val print_ast : Format.formatter -> tactic_ext -> unit
 end =
 struct
 
-let rec print_symbol fmt = function
-| Ulist1 s ->
-  fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s
-| Ulist1sep (s, sep) ->
-  fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep
-| Ulist0 s ->
-  fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s
-| Ulist0sep (s, sep) ->
-  fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep
-| Uopt s ->
-  fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s
-| Uentry e ->
-  fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e
-| Uentryl (e, l) ->
-  assert (e = "tactic");
-  fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l
-
 let rec print_clause fmt = function
-| [] -> fprintf fmt "@[TyNil@]"
-| ExtTerminal s :: cl -> fprintf fmt "@[TyIdent (\"%s\", %a)@]" s print_clause cl
+| [] -> fprintf fmt "@[Tacentries.TyNil@]"
+| ExtTerminal s :: cl -> fprintf fmt "@[Tacentries.TyIdent (\"%s\", %a)@]" s print_clause cl
 | ExtNonTerminal (g, _) :: cl ->
-  fprintf fmt "@[TyArg (%a, %a)@]"
+  fprintf fmt "@[Tacentries.TyArg (%a, %a)@]"
     print_symbol g print_clause cl
 
-let rec print_binders fmt = function
-| [] -> fprintf fmt "ist@ "
-| ExtTerminal _ :: rem -> print_binders fmt rem
-| ExtNonTerminal (_, TokNone) :: rem ->
-  fprintf fmt "_@ %a" print_binders rem
-| ExtNonTerminal (_, TokName id) :: rem ->
-  fprintf fmt "%s@ %a" id print_binders rem
-
 let print_rule fmt r =
-  fprintf fmt "@[TyML (%a, @[fun %a -> %a@])@]"
+  fprintf fmt "@[Tacentries.TyML (%a, @[fun %aist@ -> %a@])@]"
     print_clause r.tac_toks print_binders r.tac_toks print_code r.tac_body
 
-let rec print_rules fmt = function
-| [] -> ()
-| [r] -> fprintf fmt "(%a)@\n" print_rule r
-| r :: rem -> fprintf fmt "(%a);@\n%a" print_rule r print_rules rem
-
 let print_rules fmt rules =
-  fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules
+  print_list fmt (fun fmt r -> fprintf fmt "(%a)" print_rule r) rules
 
 let print_ast fmt ext =
   let deprecation fmt =
@@ -347,7 +397,7 @@ let pr_ast fmt = function
 | Comment s -> fprintf fmt "%s@\n" s
 | DeclarePlugin name -> declare_plugin fmt name
 | GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram
-| VernacExt -> fprintf fmt "VERNACEXT@\n"
+| VernacExt vernac -> fprintf fmt "%a@\n" VernacExt.print_ast vernac
 | TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac
 
 let () =
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: