Uniformizing the semantics of ARGUMENT EXTEND macros.

Most notably, we bring the single argument and three argument variants
closer, so that the various TYPED AS clauses may be optional. Compile-time
warnings have been added for redundant clauses.

6 files changed, 59 insertions, 57 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index adfbd8cfde..dca3e1656f 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -73,34 +73,58 @@ let make_extend loc s cl wit = match cl with
       let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in
       $lid:s$ >>
 
-let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
-  let rawtyp, rawpr, globtyp, globpr = match typ with
-    | `Uniform typ ->
-      typ, pr, typ, pr
-    | `Specialized (a, b, c, d) -> a, b, c, d
+let warning_redundant prefix s =
+  Printf.eprintf "Redundant [%sTYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" prefix s
+
+let get_type prefix s = function
+| None -> None
+| Some typ ->
+  if is_self s typ then
+    let () = warning_redundant prefix s in None
+  else Some typ
+
+let check_type prefix s = function
+| None -> ()
+| Some _ -> warning_redundant prefix s
+
+let declare_tactic_argument loc s (typ, f, g, h) cl =
+  let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with
+    | `Uniform (typ, pr) ->
+      let typ = get_type "" s typ in
+      typ, pr, typ, pr, typ, pr
+    | `Specialized (a, rpr, c, gpr, e, tpr) ->
+      (** Check that we actually need the TYPED AS arguments *)
+      let rawtyp = get_type "RAW_" s a in
+      let glbtyp = get_type "GLOB_" s c in
+      let toptyp = get_type "" s e in
+      let () = match g with None -> () | Some _ -> check_type "RAW_" s rawtyp in
+      let () = match f, h with Some _, Some _ -> check_type "GLOB_" s glbtyp | _ -> () in
+      rawtyp, rpr, glbtyp, gpr, toptyp, tpr
   in
   let glob = match g with
     | None ->
-      if is_self s rawtyp then
-        <:expr< fun ist v -> (ist, v) >>
-      else
+      begin match rawtyp with
+      | None -> <:expr< fun ist v -> (ist, v) >>
+      | Some rawtyp ->
         <:expr< fun ist v ->
           let ans = out_gen $make_globwit loc rawtyp$
           (Tacintern.intern_genarg ist
           (Genarg.in_gen $make_rawwit loc rawtyp$ v)) in
           (ist, ans) >>
+      end
     | Some f ->
       <:expr< fun ist v -> (ist, $lid:f$ ist v) >>
   in
   let interp = match f with
     | None ->
-      if is_self s globtyp then
-        <:expr< fun ist v -> Ftactic.return v >>
-      else
-	<:expr< fun ist x ->
+      begin match globtyp with
+      | None -> <:expr< fun ist v -> Ftactic.return v >>
+      | Some globtyp ->
+        <:expr< fun ist x ->
           Ftactic.bind
-	    (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x))
+            (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x))
             (fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >>
+      end
     | Some f ->
       (** Compatibility layer, TODO: remove me *)
       <:expr<
@@ -112,19 +136,20 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
       >> in
   let subst = match h with
     | None ->
-      if is_self s globtyp then
-        <:expr< fun s v -> v >>
-      else
+      begin match globtyp with
+      | None -> <:expr< fun s v -> v >>
+      | Some globtyp ->
         <:expr< fun s x ->
           out_gen $make_globwit loc globtyp$
           (Tacsubst.subst_genarg s
             (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
+      end
     | Some f -> <:expr< $lid:f$>> in
   let dyn = match typ with
-  | `Uniform typ ->
+  | None -> <:expr< None >>
+  | Some typ ->
     if is_self s typ then <:expr< None >>
     else <:expr< Some (Genarg.val_tag $make_topwit loc typ$) >>
-  | `Specialized _ -> <:expr< None >>
   in
   let se = mlexpr_of_string s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
@@ -180,22 +205,25 @@ EXTEND
         "END" ->
          declare_vernac_argument loc s pr l ] ]
   ;
+  argextend_specialized:
+  [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ];
+      "RAW_PRINTED"; "BY"; rawpr = LIDENT;
+      globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ];
+      "GLOB_PRINTED"; "BY"; globpr = LIDENT ->
+      (rawtyp, rawpr, globtyp, globpr) ] ]
+  ;
   argextend_header:
-    [ [ "TYPED"; "AS"; typ = argtype;
+    [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ];
         "PRINTED"; "BY"; pr = LIDENT;
         f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
         g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
-        h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ] ->
-        (`Uniform typ, pr, f, g, h)
-      | "PRINTED"; "BY"; pr = LIDENT;
-        f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
-        g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
         h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ];
-        "RAW_TYPED"; "AS"; rawtyp = argtype;
-        "RAW_PRINTED"; "BY"; rawpr = LIDENT;
-        "GLOB_TYPED"; "AS"; globtyp = argtype;
-        "GLOB_PRINTED"; "BY"; globpr = LIDENT ->
-        (`Specialized (rawtyp, rawpr, globtyp, globpr), pr, f, g, h) ] ]
+        special = OPT argextend_specialized ->
+        let repr = match special with
+        | None -> `Uniform (typ, pr)
+        | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr)
+        in
+        (repr, f, g, h) ] ]
   ;
   argtype:
     [ "2"
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 4d3507cbc4..fbae17bafc 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -104,16 +104,14 @@ let glob_occs ist l = l
 let subst_occs evm l = l
 
 ARGUMENT EXTEND occurrences
+  TYPED AS int list
   PRINTED BY pr_int_list_full
 
   INTERPRETED BY interp_occs
   GLOBALIZED BY glob_occs
   SUBSTITUTED BY subst_occs
 
-  RAW_TYPED AS occurrences_or_var
   RAW_PRINTED BY pr_occurrences
-
-  GLOB_TYPED AS occurrences_or_var
   GLOB_PRINTED BY pr_occurrences
 
 | [ ne_integer_list(l) ] -> [ ArgArg l ]
@@ -141,10 +139,7 @@ ARGUMENT EXTEND glob
      GLOBALIZED BY glob_glob
      SUBSTITUTED BY subst_glob
 
-     RAW_TYPED AS constr_expr
      RAW_PRINTED BY pr_gen
-
-     GLOB_TYPED AS glob_constr_and_expr
      GLOB_PRINTED BY pr_gen
   [ constr(c) ] -> [ c ]
 END
@@ -158,16 +153,14 @@ ARGUMENT EXTEND lconstr
 END
 
 ARGUMENT EXTEND lglob
+  TYPED AS glob
     PRINTED BY pr_globc
 
      INTERPRETED BY interp_glob
      GLOBALIZED BY glob_glob
      SUBSTITUTED BY subst_glob
 
-     RAW_TYPED AS constr_expr
      RAW_PRINTED BY pr_gen
-
-     GLOB_TYPED AS glob_constr_and_expr
      GLOB_PRINTED BY pr_gen
   [ lconstr(c) ] -> [ c ]
 END
@@ -207,9 +200,7 @@ ARGUMENT EXTEND hloc
     INTERPRETED BY interp_place
     GLOBALIZED BY intern_place
     SUBSTITUTED BY subst_place
-    RAW_TYPED AS loc_place
     RAW_PRINTED BY pr_loc_place
-    GLOB_TYPED AS loc_place
     GLOB_PRINTED BY pr_loc_place
   [ ] ->
     [ ConclLocation () ]
@@ -224,12 +215,6 @@ ARGUMENT EXTEND hloc
 
  END
 
-
-
-
-
-
-
 (* Julien: Mise en commun des differentes version de replace with in by *)
 
 let pr_by_arg_tac _prc _prlc prtac opt_c =
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index ba9f82fb96..0b475340e2 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -980,9 +980,7 @@ let interp_test ist gls = function
 ARGUMENT EXTEND test
   PRINTED BY pr_itest'
   INTERPRETED BY interp_test
-  RAW_TYPED AS test
   RAW_PRINTED BY pr_test'
-  GLOB_TYPED AS test
   GLOB_PRINTED BY pr_test'
 | [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ]
 END
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index bc98b7d6d4..d4fd8a1df3 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -174,7 +174,6 @@ END
 let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
 
 ARGUMENT EXTEND hints_path_atom
-  TYPED AS hints_path_atom
   PRINTED BY pr_hints_path_atom
 | [ global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ]
 | [ "*" ] -> [ Hints.PathAny ]
@@ -183,7 +182,6 @@ END
 let pr_hints_path prc prx pry c = Hints.pp_hints_path c
 
 ARGUMENT EXTEND hints_path
-  TYPED AS hints_path
   PRINTED BY pr_hints_path
 | [ "(" hints_path(p) ")"  ] -> [ p ]
 | [ "!" hints_path(p)  ] -> [ Hints.PathStar p ]
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index c4ef1f297e..395c2cd1b6 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -47,10 +47,7 @@ ARGUMENT EXTEND glob_constr_with_bindings
     GLOBALIZED BY glob_glob_constr_with_bindings
     SUBSTITUTED BY subst_glob_constr_with_bindings
 
-    RAW_TYPED AS constr_expr_with_bindings
     RAW_PRINTED BY pr_constr_expr_with_bindings
-
-    GLOB_TYPED AS glob_constr_with_bindings
     GLOB_PRINTED BY pr_glob_constr_with_bindings
 
    [ constr_with_bindings(bl) ] -> [ bl ]
@@ -76,10 +73,7 @@ ARGUMENT EXTEND rewstrategy
     GLOBALIZED BY glob_strategy
     SUBSTITUTED BY subst_strategy
 
-    RAW_TYPED AS raw_strategy
     RAW_PRINTED BY pr_raw_strategy
-
-    GLOB_TYPED AS glob_strategy
     GLOB_PRINTED BY pr_glob_strategy
 
     [ glob(c) ] -> [ StratConstr (c, true) ]
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 7bd07f6255..ca4e13e125 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -35,7 +35,6 @@ let pr_int_or_id _ _ _ = function
   | ArgId id -> pr_id id
 
 ARGUMENT EXTEND int_or_id
-  TYPED AS int_or_id
   PRINTED BY pr_int_or_id
 | [ preident(id) ] -> [ ArgId (Id.of_string id) ]
 | [ integer(i) ] -> [ ArgInt i ]