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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(** Implementation of the TACTIC EXTEND macro. *)
open Q_util
open Argextend
let plugin_name = <:expr< __coq_plugin_name >>
let mlexpr_of_ident id =
(** Workaround for badly-designed generic arguments lacking a closure *)
let id = "$" ^ id in
<:expr< Names.Id.of_string_soft $str:id$ >>
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$) >>
| ExtNonTerminal(g,None) :: cl ->
<:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >>
| ExtNonTerminal(g,Some id) :: cl ->
<:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >>
let rec binders_of_clause e = function
| [] -> <:expr< fun ist -> $e$ >>
| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl
| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >>
| _ :: cl -> binders_of_clause e cl
open Pcaml
EXTEND
GLOBAL: str_item;
str_item:
[ [ "TACTIC"; "EXTEND"; s = tac_name;
level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
OPT "|"; l = LIST1 tacrule SEP "|";
"END" ->
let level = match level with Some i -> int_of_string i | None -> 0 in
let level = mlexpr_of_int level in
let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ]
;
tacrule:
[ [ "["; l = LIST1 tacargs; "]";
"->"; "["; e = Pcaml.expr; "]" ->
<:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >>
] ]
;
tacargs:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let e = parse_user_entry e "" in
ExtNonTerminal (e, Some s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let e = parse_user_entry e sep in
ExtNonTerminal (e, Some s)
| e = LIDENT ->
let e = parse_user_entry e "" in
ExtNonTerminal (e, None)
| s = STRING ->
let () = if s = "" then failwith "Empty terminal." in
ExtTerminal s
] ]
;
tac_name:
[ [ s = LIDENT -> s
| s = UIDENT -> s
] ]
;
END
|
