blob: 2c8cb53dc394961c7c3d442e622bd2ae595b89f7 (
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
|
(* $Id$ *)
open Coqast
open Pcoq
open Vernac
GEXTEND Gram
identarg:
[ [ id = IDENT -> <:ast< ($VAR $id) >> ] ]
;
ne_identarg_list:
[ [ l = LIST1 identarg -> l ] ]
;
ne_identarg_comma_list:
[ [ id = identarg; ","; idl = ne_identarg_comma_list -> id::idl
| id = identarg -> [id] ] ]
;
numarg:
[ [ n = Prim.number -> n
| "-"; n = Prim.number -> Num (loc, ( - Ast.num_of_ast n)) ] ]
;
ne_numarg_list:
[ [ n = numarg; l = ne_numarg_list -> n::l
| n = numarg -> [n] ] ]
;
numarg_list:
[ [ l = ne_numarg_list -> l
| -> [] ] ]
;
stringarg:
[ [ s = Prim.string -> s ] ]
;
comarg:
[ [ c = Command.command -> <:ast< (COMMAND $c) >> ] ]
;
lcomarg:
[ [ c = Command.lcommand -> <:ast< (COMMAND $c) >> ] ]
;
lvernac:
[ [ v = vernac; l = lvernac -> v::l
| -> [] ] ]
;
ne_stringarg_list:
[ [ n = stringarg; l = ne_stringarg_list -> n::l
| n = stringarg -> [n] ] ]
;
varg_ne_stringarg_list:
[ [ l = ne_stringarg_list -> <:ast< (VERNACARGLIST ($LIST $l)) >> ] ]
;
vernac:
[ [ IDENT "Pwd"; "." -> <:ast< (PWD) >>
| IDENT "Cd"; "." -> <:ast< (CD) >>
| IDENT "Cd"; dir = stringarg; "." -> <:ast< (CD $dir) >>
| "Quit"; "." -> <:ast< (QUIT) >>
| IDENT "Drop"; "." -> <:ast< (DROP) >>
| IDENT "ProtectedLoop"; "." -> <:ast< (PROTECTEDLOOP) >>
| IDENT "Print"; IDENT "All"; "." -> <:ast< (PrintAll) >>
| IDENT "Print"; "." -> <:ast< (PRINT) >>
| IDENT "Print"; IDENT "Hint"; "*"; "."
-> <:ast< (PrintHint) >>
| IDENT "Print"; IDENT "Hint"; s = identarg; "." ->
<:ast< (PrintHintId $s) >>
| IDENT "Print"; IDENT "Hint"; "." ->
<:ast< (PrintHintGoal) >>
| IDENT "Print"; IDENT "HintDb"; s = identarg ; "." ->
<:ast< (PrintHintDb $s) >>
| IDENT "Print"; IDENT "Section"; s = identarg; "." ->
<:ast< (PrintSec $s) >>
| IDENT "Print"; IDENT "States"; "." -> <:ast< (PrintStates) >>
| IDENT "Locate"; IDENT "File"; f = stringarg; "." ->
<:ast< (LocateFile $f) >>
| IDENT "Locate"; IDENT "Library"; id = identarg; "." ->
<:ast< (LocateLibrary $id) >>
| IDENT "Locate"; id = identarg; "." ->
<:ast< (Locate $id) >>
| IDENT "Print"; IDENT "LoadPath"; "." -> <:ast< (PrintPath) >>
| IDENT "AddPath"; dir = stringarg; "." -> <:ast< (ADDPATH $dir) >>
| IDENT "DelPath"; dir = stringarg; "." -> <:ast< (DELPATH $dir) >>
| IDENT "AddRecPath"; dir = stringarg; "." ->
<:ast< (RECADDPATH $dir) >>
| IDENT "Print"; IDENT "Modules"; "." -> <:ast< (PrintModules) >>
| IDENT "Print"; "Proof"; id = identarg; "." ->
<:ast< (PrintOpaqueId $id) >>
(* Pris en compte dans PrintOption ci-dessous
| IDENT "Print"; id = identarg; "." -> <:ast< (PrintId $id) >> *)
| IDENT "Search"; id = identarg; "." -> <:ast< (SEARCH $id) >>
| IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
(* TODO: rapprocher Eval et Check *)
| IDENT "Eval"; r = Tactic.red_tactic; "in"; c = comarg; "." ->
<:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c) >>
| IDENT "Eval"; g = numarg; r = Tactic.red_tactic;
"in"; c = comarg; "." ->
<:ast< (Eval (TACTIC_ARG (REDEXP $r)) $c $g) >>
| check = check_tok; c = comarg; "." -> <:ast< (Check $check $c) >>
| check = check_tok; g = numarg; c = comarg; "." ->
<:ast< (Check $check $c $g) >>
| IDENT "Print"; IDENT "ML"; IDENT "Path"; "." ->
<:ast< (PrintMLPath) >>
| IDENT "Print"; IDENT "ML"; IDENT "Modules"; "." ->
<:ast< (PrintMLModules) >>
| IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = stringarg; "." ->
<:ast< (AddMLPath $dir) >>
| IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path";
dir = stringarg; "." ->
<:ast< (RecAddMLPath $dir) >>
| IDENT "Print"; IDENT "Graph"; "." -> <:ast< (PrintGRAPH) >>
| IDENT "Print"; IDENT "Classes"; "." -> <:ast< (PrintCLASSES) >>
| IDENT "Print"; IDENT "Coercions"; "." -> <:ast< (PrintCOERCIONS) >>
| IDENT "Print"; IDENT "Path"; c = identarg; d = identarg; "." ->
<:ast< (PrintPATH $c $d) >>
(* | IDENT "Time"; "." -> <:ast< (Time) >>
| IDENT "Untime"; "." -> <:ast< (Untime) >> *)
| IDENT "Time"; v = vernac -> <:ast< (Time $v)>>
| IDENT "SearchIsos"; com = comarg; "." ->
<:ast< (Searchisos $com) >>
| "Set"; IDENT "Undo"; n = numarg; "." ->
<:ast< (SETUNDO $n) >>
| IDENT "Unset"; IDENT "Undo"; "." -> <:ast< (UNSETUNDO) >>
| "Set"; IDENT "Hyps_limit"; n = numarg; "." ->
<:ast< (SETHYPSLIMIT $n) >>
| IDENT "Unset"; IDENT "Hyps_limit"; "." ->
<:ast< (UNSETHYPSLIMIT) >>
(* Pour intervenir sur les tables de paramètres *)
| "Set"; table = identarg; field = identarg;
value = option_value; "." ->
<:ast< (SetTableField $table $field $value) >>
| "Set"; table = identarg; field = identarg; "." ->
<:ast< (SetTableField $table $field) >>
| IDENT "Unset"; table = identarg; field = identarg; "." ->
<:ast< (UnsetTableField $table $field) >>
| "Set"; table = identarg; value = option_value; "." ->
<:ast< (SetTableField $table $value) >>
| "Set"; table = identarg; "." ->
<:ast< (SetTableField $table) >>
| IDENT "Unset"; table = identarg; "." ->
<:ast< (UnsetTableField $table) >>
| IDENT "Print"; table = identarg; field = identarg; "." ->
<:ast< (PrintOption $table $field) >>
(* Le cas suivant inclut aussi le "Print id" standard *)
| IDENT "Print"; table = identarg; "." ->
<:ast< (PrintOption $table) >>
| IDENT "Add"; table = identarg; field = identarg; id = identarg; "."
-> <:ast< (AddTableField $table $field $id) >>
| IDENT "Add"; table = identarg; id = identarg; "."
-> <:ast< (AddTableField $table $id) >>
| IDENT "Test"; table = identarg; field = identarg; id = identarg; "."
-> <:ast< (MemTableField $table $field $id) >>
| IDENT "Test"; table = identarg; id = identarg; "."
-> <:ast< (MemTableField $table $id) >>
| IDENT "Remove"; table = identarg; field = identarg; id = identarg; "." ->
<:ast< (RemoveTableField $table $field $id) >>
| IDENT "Remove"; table = identarg; id = identarg; "." ->
<:ast< (RemoveTableField $table $id) >> ] ]
;
option_value:
[ [ id = identarg -> id
| n = numarg -> n
| s = stringarg -> s ] ]
;
check_tok:
[ [ IDENT "Check" -> <:ast< "CHECK" >>
| "Type" -> <:ast< "PRINTTYPE" >> ] ] (* pas dans le RefMan *)
;
END;
|
