blob: 0f0d70f8b3c55ba31be976e0cbc80a90019cd8f7 (
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
|
(*i camlp4deps: "parsing/grammar.cma" i*)
(* $Id$ *)
open Pcoq
open Pp
open Tactic
open Util
open Vernac
(* Proof commands *)
GEXTEND Gram
GLOBAL: command ne_constrarg_list;
destruct_location :
[ [ IDENT "Conclusion" -> <:ast< (CONCL)>>
| IDENT "Discardable"; "Hypothesis" -> <:ast< (DiscardableHYP)>>
| "Hypothesis" -> <:ast< (PreciousHYP)>> ]]
;
ne_constrarg_list:
[ [ l = LIST1 constrarg -> l ] ]
;
opt_identarg_list:
[ [ -> []
| ":"; l = LIST1 identarg -> l ] ]
;
vrec_clause:
[ [ name=identarg; it=LIST1 input_fun; ":="; body=tactic_expr ->
<:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ]
;
command:
[ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
| IDENT "Goal"; "." -> <:ast< (GOAL) >>
| "Proof"; "." -> <:ast< (GOAL) >>
| IDENT "Abort"; "." -> <:ast< (ABORT) >>
| "Qed"; "." -> <:ast< (SaveNamed) >>
| IDENT "Save"; "." -> <:ast< (SaveNamed) >>
| IDENT "Defined"; "." -> <:ast< (DefinedNamed) >>
| IDENT "Save"; IDENT "Remark"; id = identarg; "." ->
<:ast< (SaveAnonymousRmk $id) >>
| IDENT "Save"; IDENT "Theorem"; id = identarg; "." ->
<:ast< (SaveAnonymousThm $id) >>
| IDENT "Save"; id = identarg; "." -> <:ast< (SaveAnonymousThm $id) >>
| IDENT "Suspend"; "." -> <:ast< (SUSPEND) >>
| IDENT "Resume"; "." -> <:ast< (RESUME) >>
| IDENT "Resume"; id = identarg; "." -> <:ast< (RESUME $id) >>
| IDENT "Abort"; IDENT "All"; "." -> <:ast< (ABORTALL) >>
| IDENT "Abort"; id = identarg; "." -> <:ast< (ABORT $id) >>
| IDENT "Restart"; "." -> <:ast< (RESTART) >>
| "Proof"; c = constrarg; "." -> <:ast< (PROOF $c) >>
| IDENT "Undo"; "." -> <:ast< (UNDO 1) >>
| IDENT "Undo"; n = numarg; "." -> <:ast< (UNDO $n) >>
| IDENT "Show"; n = numarg; "." -> <:ast< (SHOW $n) >>
| IDENT "Show"; IDENT "Implicits"; n = numarg; "." ->
<:ast< (SHOWIMPL $n) >>
| IDENT "Focus"; "." -> <:ast< (FOCUS) >>
| IDENT "Focus"; n = numarg; "." -> <:ast< (FOCUS $n) >>
| IDENT "Unfocus"; "." -> <:ast< (UNFOCUS) >>
| IDENT "Show"; "." -> <:ast< (SHOW) >>
| IDENT "Show"; IDENT "Implicits"; "." -> <:ast< (SHOWIMPL) >>
| IDENT "Show"; IDENT "Node"; "." -> <:ast< (ShowNode) >>
| IDENT "Show"; IDENT "Script"; "." -> <:ast< (ShowScript) >>
| IDENT "Show"; IDENT "Existentials"; "." -> <:ast< (ShowEx) >>
| IDENT "Existential"; n = numarg; ":="; c = constrarg; "." ->
<:ast< (EXISTENTIAL $n $c) >>
| IDENT "Existential"; n = numarg; ":="; c1 = Constr.constr; ":";
c2 = Constr.constr; "." ->
<:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
| IDENT "Existential"; n = numarg; ":"; c2 = Constr.constr; ":=";
c1 = Constr.constr; "." ->
<:ast< (EXISTENTIAL $n (CONSTR (CAST $c1 $c2))) >>
| IDENT "Explain"; "Proof"; l = numarg_list; "." ->
<:ast< (ExplainProof ($LIST $l)) >>
| IDENT "Explain"; "Proof"; IDENT "Tree"; l = numarg_list; "." ->
<:ast< (ExplainProofTree ($LIST $l)) >>
| IDENT "Go"; n = numarg; "." -> <:ast< (Go $n) >>
| IDENT "Go"; IDENT "top"; "." -> <:ast< (Go "top") >>
| IDENT "Go"; IDENT "prev"; "." -> <:ast< (Go "prev") >>
| IDENT "Go"; IDENT "next"; "." -> <:ast< (Go "next") >>
| IDENT "Show"; "Proof"; "." -> <:ast< (ShowProof) >>
| IDENT "Guarded"; "." -> <:ast< (CheckGuard) >>
| IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >>
| IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
(* Tactic Definition *)
|IDENT "Tactic"; "Definition"; name=identarg; ":="; body=Tactic.tactic;
"." -> <:ast<(TACDEF $name (AST $body))>>
|IDENT "Tactic"; "Definition"; name=identarg; largs=LIST1 input_fun;
":="; body=Tactic.tactic; "." ->
<:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
|IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause ; "." ->
(match vc with
Coqast.Node(_,"RECCLAUSE",nme::tl) ->
<:ast<(TACDEF $nme (AST (REC $vc)))>>
|_ ->
anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">])
|IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause;
IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." ->
let nvcl=
List.fold_right
(fun e b -> match e with
Coqast.Node(_,"RECCLAUSE",nme::_) ->
nme::<:ast<(AST (REC $e))>>::b
|_ ->
anomalylabstrm "Gram.vernac" [<'sTR
"Not a correct RECCLAUSE">]) (vc::vcl) []
in
<:ast<(TACDEF ($LIST $nvcl))>>
(* Hints for Auto and EAuto *)
| IDENT "Hint"; hintname = identarg; dbname = opt_identarg_list; ":=";
IDENT "Resolve"; c = constrarg; "." ->
<:ast<(HintResolve $hintname (VERNACARGLIST ($LIST $dbname)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
IDENT "Immediate"; c = constrarg; "." ->
<:ast<(HintImmediate $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
IDENT "Unfold"; c = identarg; "." ->
<:ast<(HintUnfold $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
IDENT "Constructors"; c = identarg; "." ->
<:ast<(HintConstructors $hintname (VERNACARGLIST ($LIST $dbnames)) $c)>>
| IDENT "Hint"; hintname = identarg; dbnames = opt_identarg_list; ":=";
IDENT "Extern"; n = numarg; c = constrarg ; tac = tacarg; "." ->
<:ast<(HintExtern $hintname (VERNACARGLIST ($LIST $dbnames))
$n $c (TACTIC $tac))>>
| IDENT "Hints"; IDENT "Resolve"; l = ne_identarg_list;
dbnames = opt_identarg_list; "." ->
<:ast< (HintsResolve (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
| IDENT "Hints"; IDENT "Immediate"; l = ne_identarg_list;
dbnames = opt_identarg_list; "." ->
<:ast< (HintsImmediate (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
| IDENT "Hints"; IDENT "Unfold"; l = ne_identarg_list;
dbnames = opt_identarg_list; "." ->
<:ast< (HintsUnfold (VERNACARGLIST ($LIST $dbnames)) ($LIST $l)) >>
| IDENT "HintDestruct";
dloc = destruct_location;
na = identarg;
hyptyp = constrarg;
pri = numarg;
tac = Prim.astact; "." ->
<:ast< (HintDestruct $na (AST $dloc) $hyptyp $pri (AST $tac))>>
| n = numarg; ":"; tac = tacarg; "." ->
<:ast< (SOLVE $n (TACTIC $tac)) >>
(*This entry is not commented, only for debug*)
| IDENT "PrintConstr"; com = constrarg; "." ->
<:ast< (PrintConstr $com)>>
] ];
END
|
