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
|
(************************************************************************)
(* 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 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"
(* 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_wf_proof_type:
[ [ IDENT "proof"; t = Constr.constr ->
Scoq.ManualProof t
| IDENT "auto" -> Scoq.AutoProof
| -> Scoq.ExistentialProof
]
]
;
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"
VERNAC COMMAND EXTEND SubtacRec
[ "Recursive" "program" ident(id)
"(" ident(recid) ":" constr(rect) ")"
"using" constr(wf_relation)
subtac_wf_proof_type(wf)
":" constr(s) ":=" constr(t) ] ->
[ Interp.subtac (Some (recid, rect, wf_relation, wf)) id Environ.empty_env (s, t) ]
END
VERNAC COMMAND EXTEND Subtac
[ "Program" ident(id) ":" operconstr(s) ":=" constr(t) ] ->
[ Interp.subtac None id Environ.empty_env (s, t) ]
END
|
