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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filli�tre *)
(* $Id$ *)
(*i camlp4deps: "parsing/grammar.cma" i*)
open Options
open Util
open Names
open Nameops
open Vernacentries
open Reduction
open Term
open Libnames
open Topconstr
(* We define new entries for programs, with the use of this module
* Subtac. These entries are named Subtac.<foo>
*)
module Gram = Pcoq.Gram
module Constr = Pcoq.Constr
module Tactic = Pcoq.Tactic
module Prim = Pcoq.Prim
module Subtac =
struct
let gec s = Gram.Entry.create ("Subtac."^s)
(* types *)
let subtac_wf_proof_type : Scoq.wf_proof_type Gram.Entry.e = gec "subtac_wf_proof_type"
let subtac_binders : Scoq.binders Gram.Entry.e = gec "subtac_binders"
let subtac_fixannot : Scoq.recursion_order option Gram.Entry.e = gec "subtac_fixannot"
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
(* admissible notation "(x t)"
taken from g_constrnew.ml4 *)
let test_lpar_id_coloneq =
Gram.Entry.of_parser "test_lpar_id_coloneq"
(fun strm ->
Pp.msgnl (Pp.str ("Testing lpar_id_coloneq:" ^
(snd (List.hd (Stream.npeek 1 strm)))));
match Stream.npeek 1 strm with
| [("","(")] ->
(match Stream.npeek 2 strm with
| [_; ("IDENT",s)] ->
(match Stream.npeek 3 strm with
| [_; _; ("", ":=")] ->
Stream.junk strm; Stream.junk strm; Stream.junk strm;
Pp.msgnl (Pp.str "Success");
Names.id_of_string s
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
let test_id_coloneq =
Gram.Entry.of_parser "test_id_coloneq"
(fun strm ->
Pp.msgnl (Pp.str ("Testing id_coloneq:" ^
(snd (List.hd (Stream.npeek 1 strm)))));
(match Stream.npeek 1 strm with
| [("IDENT",s)] ->
(match Stream.npeek 2 strm with
| [_; ("", ":=")] ->
Stream.junk strm; Stream.junk strm;
Pp.msgnl (Pp.str "Success");
Names.id_of_string s
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure))
end
open Subtac
open Util
GEXTEND Gram
GLOBAL: subtac_wf_proof_type subtac_binders subtac_fixannot;
subtac_wf_proof_type:
[ [ IDENT "proof"; t = Constr.constr ->
Scoq.ManualProof t
| IDENT "auto" -> Scoq.AutoProof
| -> Scoq.ExistentialProof
]
]
;
subtac_fixannot:
[ [ "{"; IDENT "struct"; id=Prim.name; "}" -> Some (Scoq.StructRec id)
| "{"; IDENT "wf"; rel= Constr.constr; id=Prim.name; "}" -> Some (Scoq.WfRec (rel, id))
| -> None ] ]
;
subtac_binders: [ [ bl = LIST0 Constr.binder_let -> bl ] ]
;
END
type wf_proof_type_argtype = (Scoq.wf_proof_type, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
let (wit_subtac_wf_proof_type : wf_proof_type_argtype),
(globwit_subtac_wf_proof_type : wf_proof_type_argtype),
(rawwit_subtac_wf_proof_type : wf_proof_type_argtype) =
Genarg.create_arg "subtac_wf_proof_type"
type subtac_binders_argtype = (Scoq.binders, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
let (wit_subtac_binders : subtac_binders_argtype),
(globwit_subtac_binders : subtac_binders_argtype),
(rawwit_subtac_binders : subtac_binders_argtype) =
Genarg.create_arg "subtac_binders"
type subtac_fixannot_argtype = (Scoq.recursion_order option, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
let (wit_subtac_fixannot : subtac_fixannot_argtype),
(globwit_subtac_fixannot : subtac_fixannot_argtype),
(rawwit_subtac_fixannot : subtac_fixannot_argtype) =
Genarg.create_arg "subtac_fixannot"
VERNAC COMMAND EXTEND SubtacRec
[ "Recursive" "program" ident(id) subtac_binders(l) subtac_fixannot(f)
":" lconstr(s) ":=" lconstr(t) ] ->
[ Interp.subtac (Some f) id l Environ.empty_env (s, t) ]
END
VERNAC COMMAND EXTEND Subtac
[ "Program" ident(id) subtac_binders(l) ":" lconstr(s) ":=" lconstr(t) ] ->
[ Interp.subtac None id l Environ.empty_env (s, t) ]
END
|
