From 270ceed48217797e99ec845cc5d1c599b5729bc2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Jul 2018 15:11:05 +0200
Subject: Export a wrapper simplifying the registration of vernacular commands.

---
 grammar/vernacextend.mlp | 80 +++++++++++++-----------------------------------
 1 file changed, 22 insertions(+), 58 deletions(-)

(limited to 'grammar')

diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index a2872d07f6..f344f3c573 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -66,54 +66,13 @@ let mk_ignore c pt =
   let names = List.fold_left fold <:expr< () >> names in
   <:expr< do { let _ = $names$ in $c$ } >>
 
-let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
-  match c ,cg with
-  | Some c, _ ->
-     (make_patt pt,
-      ploc_vala None,
-      make_let (mk_ignore c pt) pt)
-  | None, Some cg ->
-     (make_patt pt,
-      ploc_vala None,
-      <:expr< fun loc -> $cg$ $str:s$ >>)
-  | None, None -> prerr_endline
-      (("Vernac entry \""^s^"\" misses a classifier. "^
-         "A classifier is a function that returns an expression "^
-         "of type vernac_classification (see Vernacexpr). You can: ") ^
-       "- " ^ (
-        ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^
-          "new vernacular command does not alter the system state;"))^ "\n" ^
-       "- " ^ (
-        ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^
-          "new vernacular command alters the system state but not the "^
-          "parser nor it starts a proof or ends one;"))^ "\n" ^
-       "- " ^ (
-        ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^
-          "a global function f.  The function f will be called passing "^
-          "\""^s^"\" as the only argument;")) ^ "\n" ^
-       "- " ^ (
-        "Add a specific classifier in each clause using the syntax:"
-        ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^
-       ("Specific classifiers have precedence over global "^
-         "classifiers. Only one classifier is called.") ^ "\n");
-    (make_patt pt,
-      ploc_vala None,
-      <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>)
-
-let make_fun_clauses loc s l =
+let make_clause_classifier { r_patt = pt; r_class = c; } =
   let map c =
-    let depr = match c.r_depr with
-    | None -> false
-    | Some () -> true
-    in
-    let cl = make_fun loc [make_clause c] in
-    <:expr< ($mlexpr_of_bool depr$, $cl$)>>
+    make_fun loc [(make_patt pt,
+      ploc_vala None,
+      make_let (mk_ignore c pt) pt)]
   in
-  mlexpr_of_list map l
-
-let make_fun_classifiers loc s c l =
-  let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in
-  mlexpr_of_list (fun x -> x) cl
+  mlexpr_of_option map c
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
@@ -124,23 +83,28 @@ let make_prod_item = function
       <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
       $mlexpr_of_prod_entry_key base g$ ) ) >>
 
-let mlexpr_of_clause cl =
-  let mkexpr { r_head = a; r_patt = b; } = match a with
-  | None -> mlexpr_of_list make_prod_item b
-  | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+let mlexpr_of_clause { r_head = a; r_patt = b; } = match a with
+| None -> mlexpr_of_list make_prod_item b
+| Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+
+let make_rule r =
+  let depr = match r.r_depr with
+  | None -> false
+  | Some () -> true
   in
-  mlexpr_of_list mkexpr cl
+  let gram = mlexpr_of_clause r in
+  let cmd = make_fun loc [make_clause r] in
+  let classif = make_clause_classifier r in
+  <:expr< ($mlexpr_of_bool depr$, $cmd$, $classif$, $gram$) >>
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s in
-  let gl = mlexpr_of_clause cl in
-  let funcl = make_fun_clauses loc s cl in
-  let classl = make_fun_classifiers loc s c cl in
+  let c = mlexpr_of_option (fun x -> x) c in
+  let rules = mlexpr_of_list make_rule cl in
   declare_str_items loc
     [ <:str_item< do {
-        CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
-        CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$;
-	CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$;
+        Vernacentries.vernac_extend ?{ classifier = $c$ }
+          ~{ command = $se$ } ?{ entry = $nt$ } $rules$;
       } >> ]
 
 open Pcaml
@@ -207,7 +171,7 @@ EXTEND
     ] ]
   ;
   classifier:
-    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun loc -> $c$>> ] ]
+    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ]
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-- 
cgit v1.2.3


From b9ff36b39eb193757ce57a89afe138cd09e759d7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Jul 2018 22:57:57 +0200
Subject: Statically typecheck the VERNAC EXTEND wrapper.

This moves the typing code from the macro expansion to the extension
registering mechanism, bringing in more static safety. We also seize
the opportunity to remove dead code in the macro.
---
 grammar/q_util.mli       |   2 +
 grammar/q_util.mlp       |  14 ++++++
 grammar/tacextend.mlp    |  14 ------
 grammar/vernacextend.mlp | 123 +++++++++++------------------------------------
 4 files changed, 43 insertions(+), 110 deletions(-)

(limited to 'grammar')

diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 323a12357d..f3af318b60 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -48,3 +48,5 @@ val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.ex
 val type_of_user_symbol : user_symbol -> argument_type
 
 val parse_user_entry : string -> string -> user_symbol
+
+val mlexpr_of_symbol : user_symbol -> MLast.expr
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 0b8d7fda7a..0e2bf55d86 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -128,3 +128,17 @@ let rec parse_user_entry s sep =
     let s = match s with "hyp" -> "var" | _ -> s in
     check_separator sep;
     Uentry s
+
+let rec mlexpr_of_symbol = function
+| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
+| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
+| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
+| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
+| Uentry e ->
+  let wit = <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
+| Uentryl (e, l) ->
+  assert (e = "tactic");
+  let wit = <:expr< $lid:"wit_"^e$ >> in
+  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index cea0bed599..07a9a76139 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -15,20 +15,6 @@ open Argextend
 
 let plugin_name = <:expr< __coq_plugin_name >>
 
-let rec mlexpr_of_symbol = function
-| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >>
-| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >>
-| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >>
-| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >>
-| Uentry e ->
-  let wit = <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >>
-| Uentryl (e, l) ->
-  assert (e = "tactic");
-  let wit = <:expr< $lid:"wit_"^e$ >> in
-  <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>>
-
 let rec mlexpr_of_clause = function
 | [] -> <:expr< TyNil >>
 | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >>
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index f344f3c573..f30c96a7f5 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -14,98 +14,42 @@ open Q_util
 open Argextend
 
 type rule = {
-  r_head : string option;
-  (** The first terminal grammar token *)
   r_patt : extend_token list;
   (** The remaining tokens of the parsing rule *)
   r_class : MLast.expr option;
   (** An optional classifier for the STM *)
   r_branch : MLast.expr;
   (** The action performed by this rule. *)
-  r_depr : unit option;
+  r_depr : bool;
   (** Whether this entry is deprecated *)
 }
 
-(** Quotation difference for match clauses *)
+let rec make_patt r = function
+| [] -> r
+| ExtNonTerminal (_, Some p) :: l -> <:expr< fun $lid:p$ -> $make_patt r l$ >>
+| ExtNonTerminal (_, None) :: l -> <:expr< fun _ -> $make_patt r l$ >>
+| ExtTerminal _ :: l -> make_patt r l
 
-let default_patt loc =
-  (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)
-
-let make_fun loc cl =
-  let l = cl @ [default_patt loc] in
-  MLast.ExFun (loc, ploc_vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
-
-let rec make_patt = function
-  | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, Some p) :: l ->
-      <:patt< [ $lid:p$ :: $make_patt l$ ] >>
-  | _::l -> make_patt l
-
-let rec make_let e = function
-  | [] -> e
-  | ExtNonTerminal (g, Some p) :: l ->
-      let t = type_of_user_symbol g in
-      let loc = MLast.loc_of_expr e in
-      let e = make_let e l in
-      <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
-  | _::l -> make_let e l
-
-let make_clause { r_patt = pt; r_branch = e; } =
-  (make_patt pt,
-   ploc_vala None,
-   make_let e pt)
-
-(* To avoid warnings *)
-let mk_ignore c pt =
-  let fold accu = function
-  | ExtNonTerminal (_, Some p) -> p :: accu
-  | _ -> accu
-  in
-  let names = List.fold_left fold [] pt in
-  let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
-  let names = List.fold_left fold <:expr< () >> names in
-  <:expr< do { let _ = $names$ in $c$ } >>
-
-let make_clause_classifier { r_patt = pt; r_class = c; } =
-  let map c =
-    make_fun loc [(make_patt pt,
-      ploc_vala None,
-      make_let (mk_ignore c pt) pt)]
-  in
-  mlexpr_of_option map c
-
-let make_prod_item = function
-  | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
-  | ExtNonTerminal (g, ido) ->
-    let nt = type_of_user_symbol g in
-    let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
-    let typ = match ido with None -> None | Some _ -> Some nt in
-      <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
-      $mlexpr_of_prod_entry_key base g$ ) ) >>
-
-let mlexpr_of_clause { r_head = a; r_patt = b; } = match a with
-| None -> mlexpr_of_list make_prod_item b
-| Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+let rec mlexpr_of_clause = function
+| [] -> <:expr< Vernacentries.TyNil >>
+| ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
+| ExtNonTerminal (g, id) :: cl ->
+  let id = mlexpr_of_option mlexpr_of_string id in
+  <:expr< Vernacentries.TyNonTerminal ($id$, $mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
 
 let make_rule r =
-  let depr = match r.r_depr with
-  | None -> false
-  | Some () -> true
-  in
-  let gram = mlexpr_of_clause r in
-  let cmd = make_fun loc [make_clause r] in
-  let classif = make_clause_classifier r in
-  <:expr< ($mlexpr_of_bool depr$, $cmd$, $classif$, $gram$) >>
+  let ty = mlexpr_of_clause r.r_patt in
+  let cmd = make_patt r.r_branch r.r_patt in
+  let make_classifier c = make_patt c r.r_patt in
+  let classif = mlexpr_of_option make_classifier r.r_class in
+  <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s in
   let c = mlexpr_of_option (fun x -> x) c in
   let rules = mlexpr_of_list make_rule cl in
   declare_str_items loc
-    [ <:str_item< do {
-        Vernacentries.vernac_extend ?{ classifier = $c$ }
-          ~{ command = $se$ } ?{ entry = $nt$ } $rules$;
-      } >> ]
+  [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]
 
 open Pcaml
 
@@ -140,34 +84,21 @@ EXTEND
     ] ]
   ;
   deprecation:
-    [ [ "DEPRECATED" -> () ] ]
+    [ [ -> false | "DEPRECATED" -> true ] ]
   ;
-  (* spiwack: comment-by-guessing: it seems that the isolated string
-      (which otherwise could have been another argument) is not passed
-      to the VernacExtend interpreter function to discriminate between
-      the clauses. *)
   rule:
-    [ [ "["; s = STRING; l = LIST0 args; "]";
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let () = if s = "" then failwith "Command name is empty." in
-      let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
-      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
-      | "[" ; "-" ; l = LIST1 args ; "]" ;
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+    [ [ "["; OPT "-"; l = LIST1 args; "]";
+        d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
       let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
-      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+      { r_patt = l; r_class = c; r_branch = b; r_depr = d; }
     ] ]
   ;
+  (** The [OPT "-"] argument serves no purpose nowadays, it is left here for
+      backward compatibility. *)
   fun_rule:
-    [ [ "["; s = STRING; l = LIST0 args; "]";
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let () = if s = "" then failwith "Command name is empty." in
-      let b = <:expr< $e$ >> in
-      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
-      | "[" ; "-" ; l = LIST1 args ; "]" ;
-        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let b = <:expr< $e$ >> in
-      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
+    [ [ "["; OPT "-"; l = LIST1 args; "]";
+        d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+      { r_patt = l; r_class = c; r_branch = e; r_depr = d; }
     ] ]
   ;
   classifier:
-- 
cgit v1.2.3