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
|
(************************************************************************)
(* * 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 VERNAC EXTEND macro. *)
open Q_util
open Argextend
type rule = {
r_patt : extend_token list;
(** The remaining tokens of the parsing rule *)
r_class : MLast.expr option;
(** An optional classifier for the STM *)
r_branch : MLast.expr;
(** The action performed by this rule. *)
r_depr : bool;
(** Whether this entry is deprecated *)
}
let rec make_patt r = function
| [] -> r
| ExtNonTerminal (_, Some p) :: l -> <:expr< fun $lid:p$ -> $make_patt r l$ >>
| ExtNonTerminal (_, None) :: l -> <:expr< fun _ -> $make_patt r l$ >>
| ExtTerminal _ :: l -> make_patt r l
let rec mlexpr_of_clause = function
| [] -> <:expr< Vernacentries.TyNil >>
| ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >>
| ExtNonTerminal (g, id) :: cl ->
let id = mlexpr_of_option mlexpr_of_string id in
<:expr< Vernacentries.TyNonTerminal ($id$, $mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >>
let make_rule r =
let ty = mlexpr_of_clause r.r_patt in
let cmd = make_patt r.r_branch r.r_patt in
let make_classifier c = make_patt c r.r_patt in
let classif = mlexpr_of_option make_classifier r.r_class in
<:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >>
let declare_command loc s c nt cl =
let se = mlexpr_of_string s in
let c = mlexpr_of_option (fun x -> x) c in
let rules = mlexpr_of_list make_rule cl in
declare_str_items loc
[ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ]
open Pcaml
EXTEND
GLOBAL: str_item;
str_item:
[ [ "VERNAC"; "COMMAND"; "EXTEND"; s = UIDENT; c = OPT classification;
OPT "|"; l = LIST1 rule SEP "|";
"END" ->
declare_command loc s c <:expr<None>> l
| "VERNAC"; "COMMAND"; "FUNCTIONAL"; "EXTEND"; s = UIDENT; c = OPT classification;
OPT "|"; l = LIST1 fun_rule SEP "|";
"END" ->
declare_command loc s c <:expr<None>> l
| "VERNAC"; nt = LIDENT ; "EXTEND"; s = UIDENT; c = OPT classification;
OPT "|"; l = LIST1 rule SEP "|";
"END" ->
declare_command loc s c <:expr<Some $lid:nt$>> l
| "DECLARE"; "PLUGIN"; name = STRING ->
declare_str_items loc [
<:str_item< value __coq_plugin_name = $str:name$ >>;
<:str_item< value _ = Mltop.add_known_module __coq_plugin_name >>;
]
] ]
;
classification:
[ [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >>
| "CLASSIFIED"; "AS"; "SIDEFF" ->
<:expr< fun _ -> Vernac_classifier.classify_as_sideeff >>
| "CLASSIFIED"; "AS"; "QUERY" ->
<:expr< fun _ -> Vernac_classifier.classify_as_query >>
] ]
;
deprecation:
[ [ -> false | "DEPRECATED" -> true ] ]
;
rule:
[ [ "["; OPT "-"; l = LIST1 args; "]";
d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
let b = <:expr< fun ~{atts} ~{st} -> ( let () = $e$ in st ) >> in
{ r_patt = l; r_class = c; r_branch = b; r_depr = d; }
] ]
;
(** The [OPT "-"] argument serves no purpose nowadays, it is left here for
backward compatibility. *)
fun_rule:
[ [ "["; OPT "-"; l = LIST1 args; "]";
d = deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
{ r_patt = l; r_class = c; r_branch = e; r_depr = d; }
] ]
;
classifier:
[ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< $c$>> ] ]
;
args:
[ [ 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 ->
ExtTerminal s
] ]
;
END
;;
|
