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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Constrexpr
open Vernacexpr
open Misctypes
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
open Pcoq.Vernac_
let thm_token = G_vernac.thm_token
let hint = Gram.entry_create "hint"
(* Proof commands *)
GEXTEND Gram
GLOBAL: hint command;
opt_hintbases:
[ [ -> []
| ":"; l = LIST1 [id = IDENT -> id ] -> l ] ]
;
command:
[ [ IDENT "Goal"; c = lconstr ->
VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc:!@loc Names.Anonymous), None), ProveBody ([], c))
| IDENT "Proof" -> VernacProof (None,None)
| IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
| IDENT "Proof"; c = lconstr -> VernacExactProof c
| IDENT "Abort" -> VernacAbort None
| IDENT "Abort"; IDENT "All" -> VernacAbortAll
| IDENT "Abort"; id = identref -> VernacAbort (Some id)
| IDENT "Existential"; n = natural; c = constr_body ->
VernacSolveExistential (n,c)
| IDENT "Admitted" -> VernacEndProof Admitted
| IDENT "Qed" -> VernacEndProof (Proved (Opaque,None))
| IDENT "Save"; id = identref ->
VernacEndProof (Proved (Opaque, Some id))
| IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
| IDENT "Defined"; id=identref ->
VernacEndProof (Proved (Transparent,Some id))
| IDENT "Restart" -> VernacRestart
| IDENT "Undo" -> VernacUndo 1
| IDENT "Undo"; n = natural -> VernacUndo n
| IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n
| IDENT "Focus" -> VernacFocus None
| IDENT "Focus"; n = natural -> VernacFocus (Some n)
| IDENT "Unfocus" -> VernacUnfocus
| IDENT "Unfocused" -> VernacUnfocused
| IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
| IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
| IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id))
| IDENT "Show"; IDENT "Script" -> VernacShow ShowScript
| IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials
| IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses
| IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames
| IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
| IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
| IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
| IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id)
| IDENT "Guarded" -> VernacCheckGuard
(* Hints for Auto and EAuto *)
| IDENT "Create"; IDENT "HintDb" ;
id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
VernacCreateHintDb (id, b)
| IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
VernacRemoveHints (dbnames, ids)
| IDENT "Hint"; h = hint;
dbnames = opt_hintbases ->
VernacHints (dbnames, h)
(* Declare "Resolve" explicitly so as to be able to later extend with
"Resolve ->" and "Resolve <-" *)
| IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr;
info = hint_info; dbnames = opt_hintbases ->
VernacHints (dbnames,
HintsResolve (List.map (fun x -> (info, true, x)) lc))
] ];
reference_or_constr:
[ [ r = global -> HintsReference r
| c = constr -> HintsConstr c ] ]
;
hint:
[ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info ->
HintsResolve (List.map (fun x -> (info, true, x)) lc)
| IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc
| IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
| IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
| IDENT "Mode"; l = global; m = mode -> HintsMode (l, m)
| IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
| IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc ] ]
;
constr_body:
[ [ ":="; c = lconstr -> c
| ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ]
;
mode:
[ [ l = LIST1 [ "+" -> ModeInput
| "!" -> ModeNoHeadEvar
| "-" -> ModeOutput ] -> l ] ]
;
END
|
