Removing the default value mechanism for generic arguments.

There was a complicated dedicated code in grammar/ to decide whether a generic argument
parsed the empty string. We now only rely on a dynamic decision. This should not affect
efficiency, as it is only made once by declaration of ML tactics.

16 files changed, 54 insertions, 160 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index be4097f137..46c68ecc3a 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -48,82 +48,6 @@ let has_extraarg l =
   in
   List.exists check l
 
-let rec is_possibly_empty = function
-| Uopt _ -> true
-| Ulist0 _ -> true
-| Ulist0sep _ -> true
-| Umodifiers _ -> true
-| Ulist1 t -> is_possibly_empty t
-| Ulist1sep (t, _) -> is_possibly_empty t
-| _ -> false
-
-let rec get_empty_entry = function
-| Uopt _ -> <:expr< None >>
-| Ulist0 _ -> <:expr< [] >>
-| Ulist0sep _ -> <:expr< [] >>
-| Umodifiers _ -> <:expr< [] >>
-| Ulist1 t -> <:expr< [$get_empty_entry t$] >>
-| Ulist1sep (t, _) -> <:expr< [$get_empty_entry t$] >>
-| _ -> assert false
-
-let statically_known_possibly_empty s (prods,_) =
-  List.for_all (function
-    | ExtNonTerminal(t, e, _) ->
-      begin match t with
-      | ExtraArgType s' ->
-        (* For ExtraArg we don't know (we'll have to test dynamically) *)
-        (* unless it is a recursive call *)
-        s <> s'
-      | _ ->
-        is_possibly_empty e
-      end
-    | ExtTerminal _ ->
-        (* This consumes a token for sure *) false)
-      prods
-
-let possibly_empty_subentries loc (prods,act) =
-  let bind_name s v e =
-    <:expr< let $lid:s$ = $v$ in $e$ >>
-  in
-  let rec aux = function
-    | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >>
-    | ExtNonTerminal(_, e, s) :: tl when is_possibly_empty e ->
-        bind_name s (get_empty_entry e) (aux tl)
-    | ExtNonTerminal(t, _, s) :: tl ->
-        let t = match t with
-        | ExtraArgType _ as t -> t
-        | _ -> assert false
-        in
-        (* We check at runtime if extraarg s parses "epsilon" *)
-        <:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit loc t$ with
-          [ None -> raise Exit
-          | Some v -> v ] in $aux tl$ >>
-    | _ -> assert false (* already filtered out *) in
-  if has_extraarg prods then
-    (* Needs a dynamic check; catch all exceptions if ever some rhs raises *)
-    (* an exception rather than returning a value; *)
-    (* declares loc because some code can refer to it; *)
-    (* ensures loc is used to avoid "unused variable" warning *)
-    (true, <:expr< try Some $aux prods$
-                   with [ Exit -> None ] >>)
-  else
-    (* Static optimisation *)
-    (false, aux prods)
-
-let make_possibly_empty_subentries loc s cl =
-  let cl = List.filter (statically_known_possibly_empty s) cl in
-  if cl = [] then
-    <:expr< None >>
-  else
-    let rec aux = function
-    | (true, e) :: l ->
-        <:expr< match $e$ with [ Some v -> Some v | None -> $aux l$ ] >>
-    | (false, e) :: _ ->
-        <:expr< Some $e$ >>
-    | [] ->
-        <:expr< None >> in
-    aux (List.map (possibly_empty_subentries loc) cl)
-
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
@@ -214,12 +138,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let wit = <:expr< $lid:"wit_"^s$ >> in
   let rawwit = <:expr< Genarg.rawwit $wit$ >> in
   let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
-  let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in
   declare_str_items loc
    [ <:str_item<
       value ($lid:"wit_"^s$) =
         let dyn = $dyn$ in
-        Genarg.make0 ?dyn $default_value$ $se$ >>;
+        Genarg.make0 ?dyn $se$ >>;
      <:str_item< Genintern.register_intern0 $wit$ $glob$ >>;
      <:str_item< Genintern.register_subst0 $wit$ $subst$ >>;
      <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>;
@@ -245,7 +168,7 @@ let declare_vernac_argument loc s pr cl =
   declare_str_items loc
    [ <:str_item<
       value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) =
-        Genarg.create_arg None $se$ >>;
+        Genarg.create_arg $se$ >>;
      <:str_item<
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
     <:str_item< do {
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index a48d683754..ead4e39692 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -20,48 +20,48 @@ let loc_of_or_by_notation f = function
   | ByNotation (loc,s,_) -> loc
 
 let wit_int_or_var =
-  Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var"
+  Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
 
 let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
-  Genarg.make0 None "intropattern"
+  Genarg.make0 "intropattern"
 
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
-  Genarg.make0 None "tactic"
+  Genarg.make0 "tactic"
 
 let wit_ident =
-  Genarg.make0 None "ident"
+  Genarg.make0 "ident"
 
 let wit_var =
-  Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) None "var"
+  Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) "var"
 
-let wit_ref = Genarg.make0 None "ref"
+let wit_ref = Genarg.make0 "ref"
 
-let wit_quant_hyp = Genarg.make0 None "quant_hyp"
+let wit_quant_hyp = Genarg.make0 "quant_hyp"
 
 let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
-  Genarg.make0 None "sort"
+  Genarg.make0 "sort"
 
 let wit_constr =
-  Genarg.make0 None "constr"
+  Genarg.make0 "constr"
 
 let wit_constr_may_eval =
-  Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval"
+  Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval"
 
-let wit_uconstr = Genarg.make0 None "uconstr"
+let wit_uconstr = Genarg.make0 "uconstr"
 
-let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "open_constr"
+let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
 
-let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings"
+let wit_constr_with_bindings = Genarg.make0 "constr_with_bindings"
 
-let wit_bindings = Genarg.make0 None "bindings"
+let wit_bindings = Genarg.make0 "bindings"
 
 let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
-  Genarg.make0 None "hyp_location_flag"
+  Genarg.make0 "hyp_location_flag"
 
-let wit_red_expr = Genarg.make0 None "redexpr"
+let wit_red_expr = Genarg.make0 "redexpr"
 
 let wit_clause_dft_concl  =
-  Genarg.make0 None "clause_dft_concl"
+  Genarg.make0 "clause_dft_concl"
 
 (** Register location *)
 
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 9c3ed94130..56b995e537 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -9,19 +9,19 @@
 open Genarg
 
 let wit_unit : unit uniform_genarg_type =
-  make0 None "unit"
+  make0 "unit"
 
 let wit_bool : bool uniform_genarg_type =
-  make0 None "bool"
+  make0 "bool"
 
 let wit_int : int uniform_genarg_type =
-  make0 None "int"
+  make0 "int"
 
 let wit_string : string uniform_genarg_type =
-  make0 None "string"
+  make0 "string"
 
 let wit_pre_ident : string uniform_genarg_type =
-  make0 None "preident"
+  make0 "preident"
 
 let () = register_name0 wit_unit "Stdarg.wit_unit"
 let () = register_name0 wit_bool "Stdarg.wit_bool"
diff --git a/lib/genarg.ml b/lib/genarg.ml
index c7273ac93e..7aada461f5 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -246,7 +246,6 @@ struct
 end
 
 type ('raw, 'glb, 'top) load = {
-  nil : 'raw option;
   dyn : 'top Val.tag;
 }
 
@@ -254,30 +253,19 @@ module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end)
 
 let arg0_map = ref LoadMap.empty
 
-let create_arg opt ?dyn name =
+let create_arg ?dyn name =
   match ArgT.name name with
   | Some _ ->
     Errors.anomaly (str "generic argument already declared: " ++ str name)
   | None ->
     let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in
-    let obj = LoadMap.Pack { nil = opt; dyn; } in
+    let obj = LoadMap.Pack { dyn; } in
     let name = ArgT.create name in
     let () = arg0_map := LoadMap.add name obj !arg0_map in
     ExtraArg name
 
 let make0 = create_arg
 
-let rec default_empty_value : type a b c. (a, b, c) genarg_type -> a option = function
-| ListArg _ -> Some []
-| OptArg _ -> Some None
-| PairArg (t1, t2) ->
-  begin match default_empty_value t1, default_empty_value t2 with
-  | Some v1, Some v2 -> Some (v1, v2)
-  | _ -> None
-  end
-| ExtraArg s ->
-  match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.nil
-
 let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
 | ListArg t -> Val.List (val_tag t)
 | OptArg t -> Val.Opt (val_tag t)
diff --git a/lib/genarg.mli b/lib/genarg.mli
index ce0536cf49..d509649f22 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -110,11 +110,11 @@ end
 type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 (** Alias for concision when the three types agree. *)
 
-val make0 : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val make0 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
 (** Create a new generic type of argument: force to associate
     unique ML types at each of the three levels. *)
 
-val create_arg : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val create_arg : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
 (** Alias for [make0]. *)
 
 (** {5 Specialized types} *)
@@ -250,8 +250,6 @@ val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
 
 (** {5 Magic used by the parser} *)
 
-val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option
-
 val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit
 (** Used by the extension to give a name to types. The string should be the
     absolute path of the argument witness, e.g.
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index cf65262c4a..52437e3867 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -853,3 +853,10 @@ let list_entry_names () =
   let ans = Hashtbl.fold add_entry (get_utable uprim) [] in
   let ans = Hashtbl.fold add_entry (get_utable uconstr) ans in
   Hashtbl.fold add_entry (get_utable utactic) ans
+
+let epsilon_value f e =
+  let r = Rule (Next (Stop, e), fun x _ -> f x) in
+  let ext = of_coq_extend_statement (None, [None, None, [r]]) in
+  let entry = G.entry_create "epsilon" in
+  let () = maybe_uncurry (Gram.extend entry) ext in
+  try Some (parse_string entry "") with _ -> None
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index b26c3044bd..7e0c89fd12 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -272,6 +272,8 @@ val symbol_of_constr_prod_entry_key : gram_assoc option ->
 
 val name_of_entry : 'a Gram.entry -> 'a Entry.t
 
+val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
+
 (** Binding general entry keys to symbols *)
 
 type 's entry_name = EntryName :
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index b62cfd6add..2d096a1081 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -87,7 +87,7 @@ let vernac_proof_instr instr =
 
 (* Only declared at raw level, because only used in vernac commands. *)
 let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
-  Genarg.make0 None "proof_instr"
+  Genarg.make0 "proof_instr"
 
 (* We create a new parser entry [proof_mode]. The Declarative proof mode
     will replace the normal parser entry for tactics with this one. *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 97b9e95e10..61ada5cc8c 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -146,7 +146,7 @@ module Tactic = Pcoq.Tactic
 type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
 
 let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
-  Genarg.create_arg None "function_rec_definition_loc"
+  Genarg.create_arg "function_rec_definition_loc"
 
 let function_rec_definition_loc =
   Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 85b9d6a08f..ae8b83b95e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -931,9 +931,9 @@ type cmp =
 type 'i test =
   | Test of cmp * 'i * 'i
 
-let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 None "cmp"
+let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp"
 let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type =
-  Genarg.make0 None "tactest"
+  Genarg.make0 "tactest"
 
 let pr_cmp = function
   | Eq -> Pp.str"="
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 6b6dc7b21a..8b012aa88e 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -184,7 +184,7 @@ END
 type binders_argtype = local_binder list
 
 let wit_binders =
- (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type)
+ (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
 
 let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders)
 
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 0cd3e09446..358f6d6468 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -18,11 +18,11 @@ open Constrarg
 exception CannotCoerceTo of string
 
 let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
-  Genarg.create_arg None "constr_context"
+  Genarg.create_arg "constr_context"
 
 (* includes idents known to be bound and references *)
 let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
-  Genarg.create_arg None "constr_under_binders"
+  Genarg.create_arg "constr_under_binders"
 
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 32f7c3c61c..36faba1137 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -109,7 +109,7 @@ type tacvalue =
   | VRec of value Id.Map.t ref * glob_tactic_expr
 
 let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
-  Genarg.create_arg None "tacvalue"
+  Genarg.create_arg "tacvalue"
 
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
 let to_tacvalue v = out_gen (topwit wit_tacvalue) v
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index d3e0b1f449..a86fdb98a9 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -55,7 +55,7 @@ type tauto_flags = {
 }
 
 let wit_tauto_flags : tauto_flags uniform_genarg_type =
-  Genarg.create_arg None "tauto_flags"
+  Genarg.create_arg "tauto_flags"
 
 let assoc_flags ist =
   let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index d620febbc1..32ccf21d2b 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -32,7 +32,7 @@ let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Spec
 type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
 
 let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
-  Genarg.create_arg None "withtac"
+  Genarg.create_arg "withtac"
 
 let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac)
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 98d1a23770..82bd5dac4c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -158,36 +158,10 @@ type ml_tactic_grammar_obj = {
 
 exception NonEmptyArgument
 
-let default_empty_value wit = match Genarg.default_empty_value wit with
-| None -> raise NonEmptyArgument
-| Some v -> v
-
-let rec empty_value : type a b c s. (a, b, c) Genarg.genarg_type -> (s, a) entry_key -> a =
-fun wit key -> match key with
-| Alist1 key ->
-  begin match wit with
-  | Genarg.ListArg wit -> [empty_value wit key]
-  | Genarg.ExtraArg _ -> default_empty_value wit
-  end
-| Alist1sep (key, _) ->
-  begin match wit with
-  | Genarg.ListArg wit -> [empty_value wit key]
-  | Genarg.ExtraArg _ -> default_empty_value wit
-  end
-| Alist0 _ -> []
-| Alist0sep (_, _) -> []
-| Amodifiers _ -> []
-| Aopt _ -> None
-| Aentry _ -> default_empty_value wit
-| Aentryl (_, _) -> default_empty_value wit
-
-| Atoken _ -> raise NonEmptyArgument
-| Aself -> raise NonEmptyArgument
-| Anext -> raise NonEmptyArgument
-
 (** ML tactic notations whose use can be restricted to an identifier are added
     as true Ltac entries. *)
 let extend_atomic_tactic name entries =
+  let open Tacexpr in
   let map_prod prods =
     let (hd, rem) = match prods with
     | GramTerminal s :: rem -> (s, rem)
@@ -197,8 +171,11 @@ let extend_atomic_tactic name entries =
     | GramTerminal s -> raise NonEmptyArgument
     | GramNonTerminal (_, typ, e) ->
       let Genarg.Rawwit wit = typ in
-      let def = Genarg.in_gen typ (empty_value wit e) in
-      Tacintern.intern_genarg Tacintern.fully_empty_glob_sign def
+      let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in
+      let default = epsilon_value inj e in
+      match default with
+      | None -> raise NonEmptyArgument
+      | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def
     in
     try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
   in
@@ -206,8 +183,7 @@ let extend_atomic_tactic name entries =
   let add_atomic i args = match args with
   | None -> ()
   | Some (id, args) ->
-    let open Tacexpr in
-    let args = List.map (fun a -> TacGeneric a) args in
+    let args = List.map (fun a -> Tacexp a) args in
     let entry = { mltac_name = name; mltac_index = i } in
     let body = TacML (Loc.ghost, entry, args) in
     Tacenv.register_ltac false false (Names.Id.of_string id) body