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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4deps: "grammar/grammar.cma" i*)
(*
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filli�tre *)
open Flags
open Util
open Names
open Nameops
open Reduction
open Term
open Libnames
open Constrexpr
open Constrexpr_ops
(* We define new entries for programs, with the use of this module
* Subtac. These entries are named Subtac.<foo>
*)
module Gram = Pcoq.Gram
module Vernac = Pcoq.Vernac_
module Tactic = Pcoq.Tactic
module ObligationsGram =
struct
let gec s = Gram.entry_create s
let withtac : Tacexpr.raw_tactic_expr option Gram.entry = gec "withtac"
end
open Glob_term
open ObligationsGram
open Util
open Tok
open Pcoq
open Prim
open Constr
let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Specif.sig"))
GEXTEND Gram
GLOBAL: withtac;
withtac:
[ [ "with"; t = Tactic.tactic -> Some t
| -> None ] ]
;
Constr.closed_binder:
[[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
[LocalRawAssum ([id], default_binder_kind, typ)]
] ];
END
type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
let (wit_withtac : Genarg.tlevel withtac_argtype),
(globwit_withtac : Genarg.glevel withtac_argtype),
(rawwit_withtac : Genarg.rlevel withtac_argtype) =
Genarg.create_arg None "withtac"
open Obligations
VERNAC COMMAND EXTEND Obligations
| [ "Obligation" integer(num) "of" ident(name) ":" lconstr(t) withtac(tac) ] ->
[ obligation (num, Some name, Some t) tac ]
| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
[ obligation (num, Some name, None) tac ]
| [ "Obligation" integer(num) ":" lconstr(t) withtac(tac) ] ->
[ obligation (num, None, Some t) tac ]
| [ "Obligation" integer(num) withtac(tac) ] ->
[ obligation (num, None, None) tac ]
| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
[ next_obligation (Some name) tac ]
| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ]
END
VERNAC COMMAND EXTEND Solve_Obligation
| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
[ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ]
| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
[ try_solve_obligation num None (Some (Tacinterp.interp t)) ]
END
VERNAC COMMAND EXTEND Solve_Obligations
| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
[ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ]
| [ "Solve" "Obligations" "with" tactic(t) ] ->
[ try_solve_obligations None (Some (Tacinterp.interp t)) ]
| [ "Solve" "Obligations" ] ->
[ try_solve_obligations None None ]
END
VERNAC COMMAND EXTEND Solve_All_Obligations
| [ "Solve" "All" "Obligations" "with" tactic(t) ] ->
[ solve_all_obligations (Some (Tacinterp.interp t)) ]
| [ "Solve" "All" "Obligations" ] ->
[ solve_all_obligations None ]
END
VERNAC COMMAND EXTEND Admit_Obligations
| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ]
| [ "Admit" "Obligations" ] -> [ admit_obligations None ]
END
VERNAC COMMAND EXTEND Set_Solver
| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
set_default_tactic
(Locality.use_section_locality ())
(Tacinterp.glob_tactic t) ]
END
open Pp
VERNAC COMMAND EXTEND Show_Solver
| [ "Show" "Obligation" "Tactic" ] -> [
msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ]
END
VERNAC COMMAND EXTEND Show_Obligations
| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ]
| [ "Obligations" ] -> [ show_obligations None ]
END
VERNAC COMMAND EXTEND Show_Preterm
| [ "Preterm" "of" ident(name) ] -> [ msg_info (show_term (Some name)) ]
| [ "Preterm" ] -> [ msg_info (show_term None) ]
END
open Pp
(* Declare a printer for the content of Program tactics *)
let () =
let printer _ _ _ = function
| None -> mt ()
| Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic (Global.env ()) tac
in
(* should not happen *)
let dummy _ _ _ expr = assert false in
Pptactic.declare_extra_genarg_pprule
(rawwit_withtac, printer)
(globwit_withtac, dummy)
(wit_withtac, dummy)
|
