blob: cb075aa79fcc7efe07de8713853e6945a1515c1d (
plain)
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
|
(****************************************************************************)
(* The Calculus of Inductive Constructions *)
(* *)
(* Projet Coq *)
(* *)
(* INRIA LRI-CNRS ENS-CNRS *)
(* Rocquencourt Orsay Lyon *)
(* *)
(* Coq V6.3 *)
(* July 1st 1999 *)
(* *)
(****************************************************************************)
(* Prolog.v *)
(****************************************************************************)
Grammar tactic simple_tactic: ast :=
eapply [ "EApply" constrarg_binding_list($cl) ]
-> [(EApplyWithBindings ($LIST $cl))]
| eexact [ "EExact" constrarg($c) ] -> [(EExact $c)]
| prolog [ "Prolog" "[" constrarg_list($l) "]" numarg($n) ]
-> [(Prolog $n ($LIST $l))]
| instantiate [ "Instantiate" numarg($n) constrarg($c) ]
-> [(Instantiate $n $c)]
| normevars [ "NormEvars" ] -> [(NormEvars)]
| etrivial [ "ETrivial" ] -> [(ETrivial)]
| eauto [ "EAuto" eautoarg($np) ]
-> [(EAuto ($LIST $np))]
| eauto_with [ "EAuto" eautoarg($np) "with" ne_identarg_list($lid) ]
-> [(EAuto ($LIST $np) ($LIST $lid))]
| eauto_with_star [ "EAuto" eautoarg($np) "with" "*" ]
-> [(EAuto ($LIST $np) "*")]
| eautod [ "EAutod" eautoarg($np) ]
-> [(EAuto "debug" ($LIST $np))]
| eautod_with [ "EAutod" eautoarg($np) "with" ne_identarg_list($lid) ]
-> [(EAuto "debug" ($LIST $np) ($LIST $lid))]
| eautod_with_star [ "EAutod" eautoarg($np) "with" "*" ]
-> [(EAuto "debug" ($LIST $np) "*")]
with eautoarg : List :=
| eautoarg_mt [ ] -> [ ]
| eautoarg_n [ numarg($n) ] -> [ $n ]
| eautoarg_np [ numarg($n) numarg($p) ] -> [ $n $p ]
.
Syntax tactic level 0:
eauto_with [<<(EAuto ($LIST $lid))>>] ->
[ "EAuto" [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
| eauto [<<(EAuto)>>] -> ["EAuto"]
| eauto_n_with [<<(EAuto ($NUM $n) ($LIST $lid))>>] ->
[ "EAuto " $n [1 0] "with " [<hov 0> (LISTSPC ($LIST $lid))] ]
| eauto_n [<<(EAuto ($NUM $n))>>] -> ["EAuto " $n]
| eauto_with_star [<<(EAuto "*")>>] ->
[ "EAuto with *" ]
| eauto_n_with_star [<<(EAuto ($NUM $n) "*")>>] ->
[ "EAuto " $n " with *" ]
| etrivial [<<(ETrivial)>>] -> ["ETrivial"]
| eexact [<<(EExact $c)>>] -> ["EExact " $c]
| eapply [<<(EApplyWithBindings $c ($LIST $bl))>>]
-> ["EApply " $c (WITHBINDING ($LIST $bl))]
| prolog [<<(Prolog ($NUM $n) ($LIST $l))>>]
-> [ [<hov 0> "Prolog" [1 2] "[" [<hov 0> (LISTSPC ($LIST $l)) ] "]"
[1 2] $n] ]
| instantiate [<<(Instantiate ($NUM $n) $c)>>] -> ["Instantiate " $n [1 2] $c]
| normevars [<<(NormEvars)>>] -> ["NormEvars"].
(* $Id$ *)
|
