Make most of TACTIC EXTEND macros runtime calls.

Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic
and its parsing rule. Instead, we make it generate a typed AST that is
passed to the parser and a generic tactic execution routine.

PMP has written a small parser that can generate the same typed ASTs
without relying on camlp5, which is overkill for such simple macros.

8 files changed, 246 insertions, 104 deletions

diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index b3bcc9984..2251a6620 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -15,6 +15,7 @@
 (************************************************************************)
 
 open Eqdecide
+open Stdarg
 
 DECLARE PLUGIN "ltac_plugin"
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 4665ff9ed..2c7ebb745 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -16,6 +16,7 @@ open Misctypes
 open Genarg
 open Stdarg
 open Geninterp
+open Pp
 
 exception CannotCoerceTo of string
 
@@ -94,6 +95,38 @@ let to_option v = prj Val.typ_opt v
 
 let to_pair v = prj Val.typ_pair v
 
+let cast_error wit v =
+  let pr_v = Pptactic.pr_value Pptactic.ltop v in
+  let Val.Dyn (tag, _) = v in
+  let tag = Val.pr tag in
+  CErrors.user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
+    ++ str " while type " ++ Val.pr wit ++ str " was expected.")
+
+let unbox wit v ans = match ans with
+| None -> cast_error wit v
+| Some x -> x
+
+let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
+| Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v))
+| Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v))
+| Val.Pair (tag1, tag2) ->
+  let (x, y) = unbox Val.typ_pair v (to_pair v) in
+  (prj tag1 x, prj tag2 y)
+| Val.Base t ->
+  let Val.Dyn (t', x) = v in
+  match Val.eq t t' with
+  | None -> cast_error t v
+  | Some Refl -> x
+let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with
+| ExtraArg _ -> Geninterp.val_tag (topwit wit)
+| ListArg t -> Val.List (tag_of_arg t)
+| OptArg t -> Val.Opt (tag_of_arg t)
+| PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)
+
+let val_cast arg v = prj (tag_of_arg arg) v
+
+let cast (Topwit wit) v = val_cast wit v
+
 end
 
 let is_variable env id =
@@ -334,3 +367,46 @@ let coerce_to_int_or_var_list v =
   | Some l ->
     let map n = ArgArg (coerce_to_int n) in
     List.map map l
+
+(** Abstract application, to print ltac functions *)
+type appl =
+  | UnnamedAppl (** For generic applications: nothing is printed *)
+  | GlbAppl of (Names.KerName.t * Val.t list) list
+       (** For calls to global constants, some may alias other. *)
+
+(* Values for interpretation *)
+type tacvalue =
+  | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+      Name.t list * Tacexpr.glob_tactic_expr
+  | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
+
+let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
+  let wit = Genarg.create_arg "tacvalue" in
+  let () = register_val0 wit None in
+  let () = Genprint.register_val_print0 (base_val_typ wit)
+             (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in
+  wit
+
+let pr_argument_type arg =
+  let Val.Dyn (tag, _) = arg in
+  Val.pr tag
+
+(** TODO: unify printing of generic Ltac values in case of coercion failure. *)
+
+(* Displays a value *)
+let pr_value env v =
+  let pr_with_env pr =
+    match env with
+    | Some (env,sigma) -> pr env sigma
+    | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
+  let open Genprint in
+  match generic_val_print v with
+  | TopPrinterBasic pr -> pr ()
+  | TopPrinterNeedsContext pr -> pr_with_env pr
+  | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
+     pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
+
+let error_ltac_variable ?loc id env v s =
+   CErrors.user_err ?loc  (str "Ltac variable " ++ Id.print id ++
+   strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
+   strbrk "which cannot be coerced to " ++ str s ++ str".")
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index ce05d70e8..1fa5e3c07 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -42,6 +42,7 @@ sig
   val to_list : t -> t list option
   val to_option : t -> t option option
   val to_pair : t -> (t * t) option
+  val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
 end
 
 (** {5 Coercion functions} *)
@@ -92,3 +93,21 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list
 val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type
 
 val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type
+
+val error_ltac_variable : ?loc:Loc.t -> Id.t ->
+  (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a
+
+(** Abstract application, to print ltac functions *)
+type appl =
+  | UnnamedAppl (** For generic applications: nothing is printed *)
+  | GlbAppl of (Names.KerName.t * Val.t list) list
+       (** For calls to global constants, some may alias other. *)
+
+type tacvalue =
+  | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+      Name.t list * Tacexpr.glob_tactic_expr
+  | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
+
+val wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type
+
+val pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 42f2abd73..566fc2873 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -554,3 +554,138 @@ let () =
     AnyEntry Pltac.tactic_arg;
   ] in
   register_grammars_by_name "tactic" entries
+
+type _ ty_sig =
+| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
+| TyIdent : string * 'r ty_sig -> 'r ty_sig
+| TyArg :
+  (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+| TyAnonArg :
+  ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+
+type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
+
+let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.any user_symbol = fun tu ->
+  match tu with
+  | TUlist1 l -> Ulist1(untype_user_symbol l)
+  | TUlist1sep(l,s) -> Ulist1sep(untype_user_symbol l, s)
+  | TUlist0 l -> Ulist0(untype_user_symbol l)
+  | TUlist0sep(l,s) -> Ulist0sep(untype_user_symbol l, s)
+  | TUopt(o) -> Uopt(untype_user_symbol o)
+  | TUentry a -> Uentry (Genarg.ArgT.Any a)
+  | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i)
+
+let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list =
+  fun sign -> match sign with
+  | TyNil -> []
+  | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig'
+  | TyArg ((loc,(a,id)),sig') ->
+    TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
+  | TyAnonArg ((loc,a),sig') ->
+    TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig'
+
+let clause_of_ty_ml = function
+  | TyML (t,_) -> clause_of_sign t
+
+let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
+  | TUentry a -> ExtraArg a
+  | TUentryl (a,l) -> ExtraArg a
+  | TUopt(o) -> OptArg (prj o)
+  | TUlist1 l -> ListArg (prj l)
+  | TUlist1sep (l,_) -> ListArg (prj l)
+  | TUlist0 l -> ListArg (prj l)
+  | TUlist0sep (l,_) -> ListArg (prj l)
+
+let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
+  fun sign tac ->
+    match sign with
+    | TyNil ->
+      begin fun vals ist -> match vals with
+      | [] -> tac ist
+      | _ :: _ -> assert false
+      end
+    | TyIdent (s, sig') -> eval_sign sig' tac
+    | TyArg ((_loc,(a,id)), sig') ->
+      let f = eval_sign sig' in
+      begin fun tac vals ist -> match vals with
+      | [] -> assert false
+      | v :: vals ->
+        let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+        f (tac v') vals ist
+      end tac
+    | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac
+
+let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function
+  | TyML (t,tac) -> eval_sign t tac
+
+let is_constr_entry = function
+| TUentry a -> Option.has_some @@ genarg_type_eq (ExtraArg a) Stdarg.wit_constr
+| _ -> false
+
+let rec only_constr : type a. a ty_sig -> bool = function
+| TyNil -> true
+| TyIdent(_,_) -> false
+| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false
+| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false
+
+let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function
+| TyNil -> []
+| TyIdent (_,s) -> mk_sign_vars s
+| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s
+| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s
+
+let dummy_id = Id.of_string "_"
+
+let lift_constr_tac_to_ml_tac vars tac =
+  let tac _ ist = Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Tacmach.New.project gl in
+    let map = function
+    | Anonymous -> None
+    | Name id ->
+      let c = Id.Map.find id ist.Geninterp.lfun in
+      try Some (Taccoerce.Value.of_constr @@ Taccoerce.coerce_to_closed_constr env c)
+      with Taccoerce.CannotCoerceTo ty ->
+        Taccoerce.error_ltac_variable dummy_id (Some (env,sigma)) c ty
+    in
+    let args = List.map_filter map vars in
+    tac args ist
+  end in
+  tac
+
+let tactic_extend plugin_name tacname ~level sign =
+  let open Tacexpr in
+  let ml_tactic_name =
+    { mltac_tactic = tacname;
+      mltac_plugin = plugin_name }
+  in
+  match sign with
+  | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s ->
+  (** The extension is only made of a name followed by constr entries: we do not
+      add any grammar nor printing rule and add it as a true Ltac definition. *)
+    (*
+    let patt = make_patt rem in
+    let vars = List.map make_var rem in
+    let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in
+       *)
+    let vars = mk_sign_vars s in
+    let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in
+    let tac = match s with
+    | TyNil -> eval ml_tac
+    (** Special handling of tactics without arguments: such tactics do not do
+        a Proofview.Goal.nf_enter to compute their arguments. It matters for some
+        whole-prof tactics like [shelve_unifiable]. *)
+    | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac)
+    in
+  (** Arguments are not passed directly to the ML tactic in the TacML node,
+      the ML tactic retrieves its arguments in the [ist] environment instead.
+      This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
+    let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
+    let id = Names.Id.of_string name in
+    let obj () = Tacenv.register_ltac true false id body in
+    let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
+    Mltop.declare_cache_obj obj plugin_name
+  | _ ->
+  let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+  Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
+  Mltop.declare_cache_obj obj plugin_name
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 02e2f0f60..3f804ee8d 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -67,3 +67,15 @@ val print_ltacs : unit -> unit
 
 val print_located_tactic : Libnames.reference -> unit
 (** Display the absolute name of a tactic. *)
+
+type _ ty_sig =
+| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
+| TyIdent : string * 'r ty_sig -> 'r ty_sig
+| TyArg :
+  (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+| TyAnonArg :
+  ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+
+type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
+
+val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index cd9d9bac2..991afe9c6 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -79,9 +79,6 @@ let out_gen wit v =
 
 let val_tag wit = val_tag (topwit wit)
 
-let base_val_typ wit =
-  match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.")
-
 let pr_argument_type arg =
   let Val.Dyn (tag, _) = arg in
   Val.pr tag
@@ -93,11 +90,6 @@ let safe_msgnl s =
 
 type value = Val.t
 
-(** Abstract application, to print ltac functions *)
-type appl =
-  | UnnamedAppl (** For generic applications: nothing is printed *)
-  | GlbAppl of (Names.KerName.t * Val.t list) list
-       (** For calls to global constants, some may alias other. *)
 let push_appl appl args =
   match appl with
   | UnnamedAppl -> UnnamedAppl
@@ -121,19 +113,6 @@ let combine_appl appl1 appl2 =
   | UnnamedAppl,a | a,UnnamedAppl -> a
   | GlbAppl l1 , GlbAppl l2 -> GlbAppl (l2@l1)
 
-(* Values for interpretation *)
-type tacvalue =
-  | VFun of appl*ltac_trace * value Id.Map.t *
-      Name.t list * glob_tactic_expr
-  | VRec of value Id.Map.t ref * glob_tactic_expr
-
-let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
-  let wit = Genarg.create_arg "tacvalue" in
-  let () = register_val0 wit None in
-  let () = Genprint.register_val_print0 (base_val_typ wit)
-             (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in
-  wit
-
 let of_tacvalue v = in_gen (topwit wit_tacvalue) v
 let to_tacvalue v = out_gen (topwit wit_tacvalue) v
 
@@ -169,39 +148,6 @@ module Value = struct
     let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
     of_tacvalue closure
 
-  let cast_error wit v =
-    let pr_v = Pptactic.pr_value Pptactic.ltop v in
-    let Val.Dyn (tag, _) = v in
-    let tag = Val.pr tag in
-    user_err  (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
-      ++ str " while type " ++ Val.pr wit ++ str " was expected.")
-
-  let unbox wit v ans = match ans with
-  | None -> cast_error wit v
-  | Some x -> x
-
-  let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with
-  | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v))
-  | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v))
-  | Val.Pair (tag1, tag2) ->
-    let (x, y) = unbox Val.typ_pair v (to_pair v) in
-    (prj tag1 x, prj tag2 y)
-  | Val.Base t ->
-    let Val.Dyn (t', x) = v in
-    match Val.eq t t' with
-    | None -> cast_error t v
-    | Some Refl -> x
-
-  let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with
-  | ExtraArg _ -> val_tag wit
-  | ListArg t -> Val.List (tag_of_arg t)
-  | OptArg t -> Val.Opt (tag_of_arg t)
-  | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2)
-
-  let val_cast arg v = prj (tag_of_arg arg) v
-
-  let cast (Topwit wit) v = val_cast wit v
-
 end
 
 let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
@@ -233,21 +179,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with
 | None -> DebugOff
 | Some level -> level
 
-(** TODO: unify printing of generic Ltac values in case of coercion failure. *)
-
-(* Displays a value *)
-let pr_value env v =
-  let pr_with_env pr =
-    match env with
-    | Some (env,sigma) -> pr env sigma
-    | None -> str "a value of type" ++ spc () ++ pr_argument_type v in
-  let open Genprint in
-  match generic_val_print v with
-  | TopPrinterBasic pr -> pr ()
-  | TopPrinterNeedsContext pr -> pr_with_env pr
-  | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } ->
-     pr_with_env (fun env sigma -> printer env sigma default_already_surrounded)
-
 let pr_closure env ist body =
   let pp_body = Pptactic.pr_glob_tactic env body in
   let pr_sep () = fnl () in
@@ -360,15 +291,11 @@ let debugging_exception_step ist signal_anomaly e pp =
   debugging_step ist (fun () ->
     pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
 
-let error_ltac_variable ?loc id env v s =
-   user_err ?loc  (str "Ltac variable " ++ Id.print id ++
-   strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
-   strbrk "which cannot be coerced to " ++ str s ++ str".")
-
 (* Raise Not_found if not in interpretation sign *)
 let try_interp_ltac_var coerce ist env {loc;v=id} =
   let v = Id.Map.find id ist.lfun in
-  try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s
+  try coerce v with CannotCoerceTo s ->
+    Taccoerce.error_ltac_variable ?loc id env v s
 
 let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
@@ -2090,27 +2017,6 @@ let _ =
   in
   Pretyping.register_constr_interp0 wit_tactic eval
 
-(** Used in tactic extension **)
-
-let dummy_id = Id.of_string "_"
-
-let lift_constr_tac_to_ml_tac vars tac =
-  let tac _ ist = Proofview.Goal.enter begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let sigma = project gl in
-    let map = function
-    | Anonymous -> None
-    | Name id ->
-      let c = Id.Map.find id ist.lfun in
-      try Some (coerce_to_closed_constr env c)
-      with CannotCoerceTo ty ->
-        error_ltac_variable dummy_id (Some (env,sigma)) c ty
-    in
-    let args = List.map_filter map vars in
-    tac args ist
-  end in
-  tac
-
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
 
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 3f3b8e555..bd44bdbea 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -133,13 +133,5 @@ val interp_int : interp_sign -> lident -> int
 
 val interp_int_or_var : interp_sign -> int or_var -> int
 
-val error_ltac_variable : ?loc:Loc.t -> Id.t ->
-  (Environ.env * Evd.evar_map) option -> value -> string -> 'a
-
-(** Transforms a constr-expecting tactic into a tactic finding its arguments in
-    the Ltac environment according to the given names. *)
-val lift_constr_tac_to_ml_tac : Name.t list ->
-  (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic
-
 val default_ist : unit -> Geninterp.interp_sign
 (** Empty ist with debug set on the current value. *)
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index c8112eaa9..4ac49adb9 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Ltac_plugin
+open Stdarg
 
 DECLARE PLUGIN "nsatz_plugin"