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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Vernacexpr
open Errors
open Pp
let string_of_in_script b = if b then " (inside script)" else ""
let string_of_vernac_type = function
| VtUnknown -> "Unknown"
| VtStartProof _ -> "StartProof"
| VtSideff _ -> "Sideff"
| VtQed VtKeep -> "Qed(keep)"
| VtQed VtKeepAsAxiom -> "Qed(admitted)"
| VtQed VtDrop -> "Qed(drop)"
| VtProofStep false -> "ProofStep"
| VtProofStep true -> "ProofStep (parallel)"
| VtProofMode s -> "ProofMode " ^ s
| VtQuery (b,(id,route)) ->
"Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
" route " ^ string_of_int route
| VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
"Stm " ^ string_of_in_script b
| VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
| VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
let string_of_vernac_when = function
| VtLater -> "Later"
| VtNow -> "Now"
let string_of_vernac_classification (t,w) =
string_of_vernac_type t ^ " " ^ string_of_vernac_when w
let classifiers = ref []
let declare_vernac_classifier
(s : Vernacexpr.extend_name)
(f : Genarg.raw_generic_argument list -> unit -> vernac_classification)
=
classifiers := !classifiers @ [s,f]
let elide_part_of_script_and_now (a, _) =
match a with
| VtQuery (_,id) -> VtQuery (false,id), VtNow
| VtStm (x, _) -> VtStm (x, false), VtNow
| x -> x, VtNow
let make_polymorphic (a, b as x) =
match a with
| VtStartProof (x, _, ids) ->
VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
| _ -> x
let undo_classifier = ref (fun _ -> assert false)
let set_undo_classifier f = undo_classifier := f
let rec classify_vernac e =
let rec static_classifier e = match e with
(* PG compatibility *)
| VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
| VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
(* Univ poly compatibility: we run it now, so that we can just
* look at Flags in stm.ml. Would be nicer to have the stm
* look at the entire dag to detect this option. *)
| VernacSetOption (["Universe"; "Polymorphism"],_)
| VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
(* Stm *)
| VernacStm Finish -> VtStm (VtFinish, true), VtNow
| VernacStm Wait -> VtStm (VtWait, true), VtNow
| VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
| VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow
| VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow
| VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x)
| VernacStm (PGLast x) -> fst (classify_vernac x), VtNow
(* Nested vernac exprs *)
| VernacProgram e -> classify_vernac e
| VernacLocal (_,e) -> classify_vernac e
| VernacPolymorphic (b, e) ->
if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
make_polymorphic (classify_vernac e)
else classify_vernac e
| VernacTimeout (_,e) -> classify_vernac e
| VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
| VtStm _ | VtProofMode _ ), _ as x -> x
| VtQed _, _ -> VtProofStep false, VtNow
| (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
(* Qed *)
| VernacAbort _ -> VtQed VtDrop, VtLater
| VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
| VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
(* Query *)
| VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
| VernacCheckMayEval _ ->
VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
(* ProofStep *)
| VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
| VernacProof _
| VernacBullet _
| VernacFocus _ | VernacUnfocus
| VernacSubproof _ | VernacEndSubproof
| VernacSolve _
| VernacCheckGuard
| VernacUnfocused
| VernacSolveExistential _ -> VtProofStep false, VtLater
(* Options changing parser *)
| VernacUnsetOption (["Default";"Proof";"Using"])
| VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
(* StartProof *)
| VernacDefinition (
(Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) ->
VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
| VernacDefinition (_,((_,i),_),ProveBody _) ->
VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
| VernacStartTheoremProof (_,l,_) ->
let ids =
CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
| VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
| VernacFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
| VernacCoFixpoint (_,l) ->
let ids, open_proof =
List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
id::l, b || p = None) ([],false) l in
if open_proof
then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
else VtSideff ids, VtLater
(* Sideff: apply to all open branches. usually run on master only *)
| VernacAssumption (_,_,l) ->
let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
VtSideff ids, VtLater
| VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
| VernacInductive (_,_,l) ->
let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with
| Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
| RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
CList.map_filter (function
| ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n
| _ -> None) l) l in
VtSideff (List.flatten ids), VtLater
| VernacScheme l ->
let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in
VtSideff ids, VtLater
| VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater
| VernacBeginSection (_,id) -> VtSideff [id], VtLater
| VernacUniverse _ | VernacConstraint _
| VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
| VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
| VernacChdir _
| VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
| VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _
| VernacReserve _
| VernacGeneralizable _
| VernacSetOpacity _ | VernacSetStrategy _
| VernacUnsetOption _ | VernacSetOption _
| VernacAddOption _ | VernacRemoveOption _
| VernacMemOption _ | VernacPrintOption _
| VernacGlobalCheck _
| VernacDeclareReduction _
| VernacDeclareClass _ | VernacDeclareInstances _
| VernacRegister _
| VernacNameSectionHypSet _
| VernacComments _ -> VtSideff [], VtLater
| VernacDeclareTacticDefinition (_,l) ->
let open Libnames in
VtSideff (List.map (function
| (Ident (_,r),_,_) -> r
| (Qualid (_,q),_,_) -> snd(repr_qualid q)) l), VtLater
(* Who knows *)
| VernacLoad _ -> VtSideff [], VtNow
(* (Local) Notations have to disappear *)
| VernacEndSegment _ -> VtSideff [], VtNow
(* Modules with parameters have to be executed: can import notations *)
| VernacDeclareModule (exp,(_,id),bl,_)
| VernacDefineModule (exp,(_,id),bl,_,_) ->
VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
| VernacDeclareModuleType ((_,id),bl,_,_) ->
VtSideff [id], if bl = [] then VtLater else VtNow
(* These commands alter the parser *)
| VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
| VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
| VernacSyntaxExtension _
| VernacSyntacticDefinition _
| VernacTacticNotation _
| VernacRequire _ | VernacImport _ | VernacInclude _
| VernacDeclareMLModule _
| VernacContext _ (* TASSI: unsure *)
| VernacProofMode _
(* These are ambiguous *)
| VernacInstance _ -> VtUnknown, VtNow
(* Stm will install a new classifier to handle these *)
| VernacBack _ | VernacAbortAll
| VernacUndoTo _ | VernacUndo _
| VernacResetName _ | VernacResetInitial
| VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
(* What are these? *)
| VernacNop
| VernacToplevelControl _
| VernacRestoreState _
| VernacWriteState _ -> VtUnknown, VtNow
| VernacError _ -> assert false
(* Plugins should classify their commands *)
| VernacExtend (s,l) ->
try List.assoc s !classifiers l ()
with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
and classify_vernac_list = function
(* spiwack: It would be better to define a monoid on classifiers.
So that the classifier of the list would be the composition of
the classifier of the individual commands. Currently: special
case for singleton lists.*)
| [_,c] -> static_classifier c
| l -> VtUnknown,VtNow
in
let res = static_classifier e in
if Flags.is_universe_polymorphism () then
make_polymorphic res
else res
let classify_as_query =
VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
let classify_as_sideeff = VtSideff [], VtLater
let classify_as_proofstep = VtProofStep false, VtLater
|
