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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(** WARNING: this file is deprecated; consider modifying coqpp instead. *)
(** Implementation of the TACTIC EXTEND macro. *)
open Q_util
open Argextend
let plugin_name = <:expr< __coq_plugin_name >>
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($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
| ExtNonTerminal(g,Some id) :: cl ->
<:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_string 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;
depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ];
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 depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr 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$ } ?{ deprecation =
$depr$ } $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
|
