aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacentries.ml
blob: fada7424c33cfcfc43047a736ffb664c2dcda35c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open CErrors
open Util
open Names
open Libobject
open Genarg
open Extend
open Pcoq
open Egramml
open Vernacexpr
open Libnames
open Nameops

type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
| TacTerm of string
| TacNonTerm of ('a * Names.Id.t option) Loc.located

type raw_argument = string * string option
type argument = Genarg.ArgT.any Extend.user_symbol

(**********************************************************************)
(* Interpret entry names of the form "ne_constr_list" as entry keys   *)

let coincide s pat off =
  let len = String.length pat in
  let break = ref true in
  let i = ref 0 in
  while !break && !i < len do
    let c = Char.code s.[off + !i] in
    let d = Char.code pat.[!i] in
    break := Int.equal c d;
    incr i
  done;
  !break

let atactic n =
  if n = 5 then Aentry Pltac.binder_tactic
  else Aentryl (Pltac.tactic_expr, n)

type entry_name = EntryName :
  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name

(** Quite ad-hoc *)
let get_tacentry n m =
  let check_lvl n =
    Int.equal m n
    && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
    && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
  in
  if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself)
  else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
  else EntryName (rawwit Tacarg.wit_tactic, atactic n)

let get_separator = function
| None -> user_err Pp.(str "Missing separator.")
| Some sep -> sep

let check_separator ?loc = function
| None -> ()
| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.")

let rec parse_user_entry ?loc s sep =
  let l = String.length s in
  if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
    let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in
    check_separator ?loc sep;
    Ulist1 entry
  else if l > 12 && coincide s "ne_" 0 &&
                   coincide s "_list_sep" (l-9) then
    let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in
    Ulist1sep (entry, get_separator sep)
  else if l > 5 && coincide s "_list" (l-5) then
    let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in
    check_separator ?loc sep;
    Ulist0 entry
  else if l > 9 && coincide s "_list_sep" (l-9) then
    let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in
    Ulist0sep (entry, get_separator sep)
  else if l > 4 && coincide s "_opt" (l-4) then
    let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in
    check_separator ?loc sep;
    Uopt entry
  else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
    let n = Char.code s.[6] - 48 in
    check_separator ?loc sep;
    Uentryl ("tactic", n)
  else
    let _ = check_separator ?loc sep in
    Uentry s

let interp_entry_name interp symb =
  let rec eval = function
  | Ulist1 e -> Ulist1 (eval e)
  | Ulist1sep (e, sep) -> Ulist1sep (eval e, sep)
  | Ulist0 e -> Ulist0 (eval e)
  | Ulist0sep (e, sep) -> Ulist0sep (eval e, sep)
  | Uopt e -> Uopt (eval e)
  | Uentry s -> Uentry (interp s None)
  | Uentryl (s, n) -> Uentryl (interp s (Some n), n)
  in
  eval symb

(**********************************************************************)
(** Grammar declaration for Tactic Notation (Coq level)               *)

let get_tactic_entry n =
  if Int.equal n 0 then
    Pltac.simple_tactic, None
  else if Int.equal n 5 then
    Pltac.binder_tactic, None
  else if 1<=n && n<5 then
    Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
  else
    user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))

(**********************************************************************)
(** State of the grammar extensions                                   *)

type tactic_grammar = {
  tacgram_level : int;
  tacgram_prods : Pptactic.grammar_terminals;
}

(* Declaration of the tactic grammar rule *)

let head_is_ident tg = match tg.tacgram_prods with
| TacTerm _ :: _ -> true
| _ -> false

let rec prod_item_of_symbol lev = function
| Extend.Ulist1 s ->
  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
  EntryName (Rawwit (ListArg typ), Alist1 e)
| Extend.Ulist0 s ->
  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
  EntryName (Rawwit (ListArg typ), Alist0 e)
| Extend.Ulist1sep (s, sep) ->
  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
  EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep)))
| Extend.Ulist0sep (s, sep) ->
  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
  EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep)))
| Extend.Uopt s ->
  let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
  EntryName (Rawwit (OptArg typ), Aopt e)
| Extend.Uentry arg ->
  let ArgT.Any tag = arg in
  let wit = ExtraArg tag in
  EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit))
| Extend.Uentryl (s, n) ->
  let ArgT.Any tag = s in
  assert (coincide (ArgT.repr tag) "tactic" 0);
  get_tacentry n lev

(** Tactic grammar extensions *)

let add_tactic_entry (kn, ml, tg) state =
  let open Tacexpr in
  let entry, pos = get_tactic_entry tg.tacgram_level in
  let mkact loc l =
    let map arg =
      (** HACK to handle especially the tactic(...) entry *)
      let wit = Genarg.rawwit Tacarg.wit_tactic in
      if Genarg.has_type arg wit && not ml then
        Tacexp (Genarg.out_gen wit arg)
      else
        TacGeneric arg
    in
    let l = List.map map l in
    (TacAlias (Loc.tag ~loc (kn,l)):raw_tactic_expr)
  in
  let () =
    if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
      user_err Pp.(str "Notation for simple tactic must start with an identifier.")
  in
  let map = function
  | TacTerm s -> GramTerminal s
  | TacNonTerm (loc, (s, ido)) ->
    let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
    GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e))
  in
  let prods = List.map map tg.tacgram_prods in
  let rules = make_rule mkact prods in
  let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in
  ([r], state)

let tactic_grammar =
  create_grammar_command "TacticGrammar" add_tactic_entry

let extend_tactic_grammar kn ml ntn = extend_grammar_command tactic_grammar (kn, ml, ntn)

(**********************************************************************)
(* Tactic Notation                                                    *)

let entry_names = ref String.Map.empty

let register_tactic_notation_entry name entry =
  let entry = match entry with
  | ExtraArg arg -> ArgT.Any arg
  | _ -> assert false
  in
  entry_names := String.Map.add name entry !entry_names

let interp_prod_item = function
  | TacTerm s -> TacTerm s
  | TacNonTerm (loc, ((nt, sep), ido)) ->
    let symbol = parse_user_entry ?loc nt sep in
    let interp s = function
    | None ->
      if String.Map.mem s !entry_names then String.Map.find s !entry_names
      else begin match ArgT.name s with
      | None -> user_err Pp.(str ("Unknown entry "^s^"."))
      | Some arg -> arg
      end
    | Some n ->
      (** FIXME: do better someday *)
      assert (String.equal s "tactic");
      begin match Tacarg.wit_tactic with
      | ExtraArg tag -> ArgT.Any tag
      end
    in
    let symbol = interp_entry_name interp symbol in
    TacNonTerm (loc, (symbol, ido))

let make_fresh_key =
  let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
  fun prods ->
    let cur = incr id; !id in
    let map = function
    | TacTerm s -> s
    | TacNonTerm _ -> "#"
    in
    let prods = String.concat "_" (List.map map prods) in
    (** We embed the hash of the kernel name in the label so that the identifier
        should be mostly unique. This ensures that including two modules
        together won't confuse the corresponding labels. *)
    let hash = (cur lxor (ModPath.hash (Lib.current_mp ()))) land 0x7FFFFFFF in
    let lbl = Id.of_string_soft (Printf.sprintf "%s_%08X" prods hash) in
    Lib.make_kn lbl

type tactic_grammar_obj = {
  tacobj_key : KerName.t;
  tacobj_local : locality_flag;
  tacobj_tacgram : tactic_grammar;
  tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
  tacobj_forml : bool;
}

let pprule pa = {
  Pptactic.pptac_level = pa.tacgram_level;
  pptac_prods = pa.tacgram_prods;
}

let check_key key =
  if Tacenv.check_alias key then
    user_err Pp.(str "Conflicting tactic notations keys. This can happen when including \
    twice the same module.")

let cache_tactic_notation (_, tobj) =
  let key = tobj.tacobj_key in
  let () = check_key key in
  Tacenv.register_alias key tobj.tacobj_body;
  extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram;
  Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram)

let open_tactic_notation i (_, tobj) =
  let key = tobj.tacobj_key in
  if Int.equal i 1 && not tobj.tacobj_local then
    extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram

let load_tactic_notation i (_, tobj) =
  let key = tobj.tacobj_key in
  let () = check_key key in
  (** Only add the printing and interpretation rules. *)
  Tacenv.register_alias key tobj.tacobj_body;
  Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram);
  if Int.equal i 1 && not tobj.tacobj_local then
    extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram

let subst_tactic_notation (subst, tobj) =
  let (ids, body) = tobj.tacobj_body in
  { tobj with
    tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
    tacobj_body = (ids, Tacsubst.subst_tactic subst body);
  }

let classify_tactic_notation tacobj = Substitute tacobj

let inTacticGrammar : tactic_grammar_obj -> obj =
  declare_object {(default_object "TacticGrammar") with
       open_function = open_tactic_notation;
       load_function = load_tactic_notation;
       cache_function = cache_tactic_notation;
       subst_function = subst_tactic_notation;
       classify_function = classify_tactic_notation}

let cons_production_parameter = function
| TacTerm _ -> None
| TacNonTerm (_, (_, ido)) -> ido

let add_glob_tactic_notation local ~level prods forml ids tac =
  let parule = {
    tacgram_level = level;
    tacgram_prods = prods;
  } in
  let tacobj = {
    tacobj_key = make_fresh_key prods;
    tacobj_local = local;
    tacobj_tacgram = parule;
    tacobj_body = (ids, tac);
    tacobj_forml = forml;
  } in
  Lib.add_anonymous_leaf (inTacticGrammar tacobj)

let add_tactic_notation local n prods e =
  let ids = List.map_filter cons_production_parameter prods in
  let prods = List.map interp_prod_item prods in
  let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
  add_glob_tactic_notation local ~level:n prods false ids tac

(**********************************************************************)
(* ML Tactic entries                                                  *)

exception 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
    | TacTerm s :: rem -> (s, rem)
    | _ -> assert false (** Not handled by the ML extension syntax *)
    in
    let empty_value = function
    | TacTerm s -> raise NonEmptyArgument
    | TacNonTerm (_, (symb, _)) ->
      let EntryName (typ, e) = prod_item_of_symbol 0 symb in
      let Genarg.Rawwit wit = typ in
      let inj x = TacArg (Loc.tag @@ 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
  let entries = List.map map_prod entries in
  let add_atomic i args = match args with
  | None -> ()
  | Some (id, args) ->
    let args = List.map (fun a -> Tacexp a) args in
    let entry = { mltac_name = name; mltac_index = i } in
    let body = TacML (Loc.tag (entry, args)) in
    Tacenv.register_ltac false false (Names.Id.of_string id) body
  in
  List.iteri add_atomic entries

let add_ml_tactic_notation name ~level prods =
  let len = List.length prods in
  let iter i prods =
    let open Tacexpr in
    let get_id = function
    | TacTerm s -> None
    | TacNonTerm (_, (_, ido)) -> ido
    in
    let ids = List.map_filter get_id prods in
    let entry = { mltac_name = name; mltac_index = len - i - 1 } in
    let map id = Reference (Locus.ArgVar (CAst.make id)) in
    let tac = TacML (Loc.tag (entry, List.map map ids)) in
    add_glob_tactic_notation false ~level prods true ids tac
  in
  List.iteri iter (List.rev prods);
  (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
  tactic_expr level 0) *)
  if Int.equal level 0 then extend_atomic_tactic name prods

(**********************************************************************)
(** Ltac quotations                                                   *)

let ltac_quotations = ref String.Set.empty

let create_ltac_quotation name cast (e, l) =
  let () =
    if String.Set.mem name !ltac_quotations then
      failwith ("Ltac quotation " ^ name ^ " already registered")
  in
  let () = ltac_quotations := String.Set.add name !ltac_quotations in
  let entry = match l with
  | None -> Aentry e
  | Some l -> Aentryl (e, l)
  in
(*   let level = Some "1" in *)
  let level = None in
  let assoc = None in
  let rule =
    Next (Next (Next (Next (Next (Stop,
      Atoken (CLexer.terminal name)),
      Atoken (CLexer.terminal ":")),
      Atoken (CLexer.terminal "(")),
      entry),
      Atoken (CLexer.terminal ")"))
  in
  let action _ v _ _ _ loc = cast (Some loc, v) in
  let gram = (level, assoc, [Rule (rule, action)]) in
  Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])

(** Command *)


type tacdef_kind =
  | NewTac of Id.t
  | UpdateTac of Tacexpr.ltac_constant

let is_defined_tac kn =
  try ignore (Tacenv.interp_ltac kn); true with Not_found -> false

let warn_unusable_identifier =
  CWarnings.create ~name:"unusable-identifier" ~category:"parsing"
      (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++
        strbrk "may be unusable because of a conflict with a notation.")

let register_ltac local tacl =
  let map tactic_body =
    match tactic_body with
    | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
        let kn = Lib.make_kn id in
        let id_pp = Id.print id in
        let () = if is_defined_tac kn then
          CErrors.user_err ?loc
            (str "There is already an Ltac named " ++ id_pp ++ str".")
        in
        let is_shadowed =
          try
            match Pcoq.parse_string Pltac.tactic (Id.to_string id) with
            | Tacexpr.TacArg _ -> false
            | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *)
          with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *)
        in
        let () = if is_shadowed then warn_unusable_identifier id in
        NewTac id, body
    | Tacexpr.TacticRedefinition (ident, body) ->
        let kn =
          try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v
          with Not_found ->
            CErrors.user_err ?loc:ident.CAst.loc
                       (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
        in
        UpdateTac kn, body
  in
  let rfun = List.map map tacl in
  let recvars =
    let fold accu (op, _) = match op with
    | UpdateTac _ -> accu
    | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu
    in
    List.fold_left fold [] rfun
  in
  let ist = Tacintern.make_empty_glob_sign () in
  let map (name, body) =
    let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in
    (name, body)
  in
  let defs () =
    (** Register locally the tactic to handle recursivity. This function affects
        the whole environment, so that we transactify it afterwards. *)
    let iter_rec (sp, kn) = Tacenv.push_tactic (Nametab.Until 1) sp kn in
    let () = List.iter iter_rec recvars in
    List.map map rfun
  in
  (* STATE XXX: Review what is going on here. Why does this needs
     protection? Why is not the STM level protection enough? Fishy *)
  let defs = States.with_state_protection defs () in
  let iter (def, tac) = match def with
  | NewTac id ->
    Tacenv.register_ltac false local id tac;
    Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
  | UpdateTac kn ->
    Tacenv.redefine_ltac local kn tac;
    let name = Tacenv.shortest_qualid_of_tactic kn in
    Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
  in
  List.iter iter defs

(** Queries *)

let print_ltacs () =
  let entries = KNmap.bindings (Tacenv.ltac_entries ()) in
  let sort (kn1, _) (kn2, _) = KerName.compare kn1 kn2 in
  let entries = List.sort sort entries in
  let map (kn, entry) =
    let qid =
      try Some (Tacenv.shortest_qualid_of_tactic kn)
      with Not_found -> None
    in
    match qid with
    | None -> None
    | Some qid -> Some (qid, entry.Tacenv.tac_body)
  in
  let entries = List.map_filter map entries in
  let pr_entry (qid, body) =
    let (l, t) = match body with
    | Tacexpr.TacFun (l, t) -> (l, t)
    | _ -> ([], body)
    in
    let pr_ltac_fun_arg n = spc () ++ Name.print n in
    hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
  in
  Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)

let locatable_ltac = "Ltac"

let () =
  let open Prettyp in
  let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in
  let locate_all = Tacenv.locate_extended_all_tactic in
  let shortest_qualid = Tacenv.shortest_qualid_of_tactic in
  let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
  let print kn =
    let qid = qualid_of_path (Tacenv.path_of_tactic kn) in
    Tacintern.print_ltac qid
  in
  let about = name in
  register_locatable locatable_ltac {
    locate;
    locate_all;
    shortest_qualid;
    name;
    print;
    about;
  }

let print_located_tactic qid =
  Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)

(** Grammar *)

let () =
  let entries = [
    AnyEntry Pltac.tactic_expr;
    AnyEntry Pltac.binder_tactic;
    AnyEntry Pltac.simple_tactic;
    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