blob: 971d1e72c41ee3cb88a85115f56fc51832cc7fec (
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
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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
|
(* $Id$: *)
Declare ML Module "equality".
Grammar vernac orient_rule: ast :=
lr ["LR"] -> [ "LR" ]
|rl ["RL"] -> [ "RL" ]
with rule_list: ast list :=
single_rlt [ constrarg($com) orient_rule($ort) ] ->
[ (VERNACARGLIST $com $ort) ]
|recursive_rlt [ constrarg($com) orient_rule($ort) rule_list($tail)] ->
[ (VERNACARGLIST $com $ort) ($LIST $tail) ]
with base_list: ast list :=
single_blt [identarg($rbase) "[" rule_list($rlt) "]"] ->
[ (VERNACARGLIST $rbase ($LIST $rlt)) ]
|recursive_blt [identarg($rbase) "[" rule_list($rlt) "]"
base_list($blt)] ->
[ (VERNACARGLIST $rbase ($LIST $rlt)) ($LIST $blt) ]
with vernac: ast :=
addrule ["HintRewrite" base_list($blt) "."] ->
[ (HintRewrite ($LIST $blt)) ].
Grammar tactic list_tactics: ast list :=
single_lt [tactic($tac)] -> [$tac]
|recursive_lt [tactic($tac) "|" list_tactics($tail)] ->
[ $tac ($LIST $tail) ]
with step_largs: ast list :=
nil_step [] -> []
|solve_step ["with" "Solve"] -> [(REDEXP (SolveStep))]
|use_step ["with" "Use"] -> [(REDEXP (Use))]
|all_step ["with" "All"] -> [(REDEXP (All))]
with rest_largs: ast list :=
nil_rest [] -> []
|solve_rest ["with" "Solve"] -> [(REDEXP (SolveRest))]
|cond_rest ["with" "Cond"] -> [(REDEXP (Cond))]
with autorew_largs: ast list :=
step_arg ["Step" "=" "[" list_tactics($ltac) "]" step_largs($slargs)] ->
[(REDEXP (Step ($LIST $ltac))) ($LIST $slargs)]
|rest_arg ["Rest" "=" "[" list_tactics($ltac) "]" rest_largs($llargs)] ->
[(REDEXP (Rest ($LIST $ltac))) ($LIST $llargs)]
|depth_arg ["Depth" "=" numarg($dth)] ->
[(REDEXP (Depth $dth))]
with list_args_autorew: ast list :=
nil_laa [] -> []
|recursive_laa [autorew_largs($largs) list_args_autorew($laa)] ->
[($LIST $largs) ($LIST $laa)]
with hintbase_list: ast list :=
nil_hintbase [] -> []
| base_by_name [identarg($id) hintbase_list($tail)] ->
[ (REDEXP (ByName $id)) ($LIST $tail)]
| explicit_base ["[" hintbase($b) "]" hintbase_list($tail)] ->
[(REDEXP (Explicit ($LIST $b))) ($LIST $tail) ]
with hintbase: ast list :=
onehint_lr [ constrarg($c) "LR" ] -> [(REDEXP (LR $c))]
| onehint_rl [ constrarg($c) "RL" ] -> [(REDEXP (RL $c))]
| conshint_lr [ constrarg($c) "LR" hintbase($tail)] -> [(REDEXP (LR $c)) ($LIST $tail)]
| conshint_rl [ constrarg($c) "RL" hintbase($tail)] -> [(REDEXP (RL $c)) ($LIST $tail)]
with simple_tactic: ast :=
AutoRewrite [ "AutoRewrite" "[" hintbase_list($lbase) "]"
list_args_autorew($laa)] ->
[(AutoRewrite (REDEXP (BaseList ($LIST $lbase))) ($LIST $laa))].
Grammar tactic simple_tactic: ast :=
replace [ "Replace" constrarg($c1) "with" constrarg($c2) ] -> [(Replace $c1 $c2)]
| deqhyp [ "Simplify_eq" identarg($id) ] -> [(DEqHyp $id)]
| deqconcl [ "Simplify_eq" ] -> [(DEqConcl)]
| discr_id [ "Discriminate" identarg($id) ] -> [(DiscrHyp $id)]
| discr [ "Discriminate" ] -> [(Discr)]
| inj [ "Injection" ] -> [(Inj)]
| inj_id [ "Injection" identarg($id) ] -> [(InjHyp $id)]
| rewriteLR [ "Rewrite" "->" constrarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
| rewriteRL [ "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(RewriteRL ($LIST $cl))]
| rewrite [ "Rewrite" constrarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
| condrewriteLR [ "Conditional" tactic_expr($tac) "Rewrite" "->" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
| condrewriteRL [ "Conditional" tactic_expr($tac) "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(CondRewriteRL (TACTIC $tac) ($LIST $cl))]
| condrewrite [ "Conditional" tactic_expr($tac) "Rewrite" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
| rewrite_in [ "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ]
-> [(RewriteLRin $h ($LIST $cl))]
| rewriteRL_in [ "Rewrite" "->" constrarg_binding_list($cl) "in" identarg($h) ]
-> [(RewriteLRin $h ($LIST $cl))]
| rewriteLR_in [ "Rewrite" "<-" constrarg_binding_list($cl) "in" identarg($h) ]
-> [(RewriteRLin $h ($LIST $cl))]
| condrewriteLRin
[ "Conditional" tactic_expr($tac) "Rewrite" "->" constrarg_binding_list($cl)
"in" identarg($h) ] ->
[(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))]
| condrewriteRLin
[ "Conditional" tactic_expr($tac) "Rewrite" "<-" constrarg_binding_list($cl)
"in" identarg($h)] ->
[(CondRewriteRLin (TACTIC $tac) $h ($LIST $cl))]
| condrewritein
[ "Conditional" tactic_expr($tac) "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ]
-> [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))]
| DRewriteLR [ "Dependent" "Rewrite" "->" identarg($id) ]
-> [(SubstHypInConcl_LR $id)]
| DRewriteRL [ "Dependent" "Rewrite" "<-" identarg($id) ]
-> [(SubstHypInConcl_RL $id)]
| cutrewriteLR [ "CutRewrite" "->" constrarg($eqn) ] -> [(SubstConcl_LR $eqn)]
| cutrewriteLRin [ "CutRewrite" "->" constrarg($eqn) "in" identarg($id) ]
-> [(SubstHyp_LR $eqn $id)]
| cutrewriteRL [ "CutRewrite" "<-" constrarg($eqn) ] -> [(SubstConcl_RL $eqn)]
| cutrewriteRLin [ "CutRewrite" "<-" constrarg($eqn) "in" identarg($id) ]
-> [(SubstHyp_RL $eqn $id)].
Syntax tactic level 0:
replace [<<(Replace $c1 $c2)>>] -> ["Replace " $c1 [1 1] "with " $c2]
| deqhyp [<<(DEqHyp $id)>>] -> ["Simplify_eq " $id]
| deqconcl [<<(DEqConcl)>>] -> ["Simplify_eq"]
| discr_id [<<(DiscrHyp $id)>>] -> ["Discriminate " $id]
| discr [<<(Discr)>>] -> ["Discriminate"]
| inj [<<(Inj)>>] -> ["Injection"]
| inj_id [<<(InjHyp $id)>>] -> ["Injection " $id]
| rewritelr [<<(RewriteLR $C ($LIST $bl))>>] -> ["Rewrite " $C (WITHBINDING ($LIST $bl))]
| rewriterl [<<(RewriteRL $C ($LIST $bl))>>] -> ["Rewrite <- " $C (WITHBINDING ($LIST $bl))]
| condrewritelr [<<(CondRewriteLR (TACTIC $tac) $C ($LIST $bl))>>] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl))]
| condrewriterl [<<(CondRewriteRL (TACTIC $tac) $C ($LIST $bl))>>] -> ["Conditional " $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl))]
| rewriteLR_in [<<(RewriteLRin $h $c ($LIST $bl))>>] -> ["Rewrite " $c (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
| rewriteRL_in [<<(RewriteRLin $h $c ($LIST $bl))>>] -> ["Rewrite <- " $c (WITHBINDING ($LIST $bl)) [1 1]"in " $h]
| condrewritelrin [<<(CondRewriteLRin (TACTIC $tac) $h $C ($LIST $bl))>>] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
| condrewriterlin [<<(CondRewriteRLin (TACTIC $tac) $h $C ($LIST $bl))>>] -> ["Conditional " $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
| DRewriteLR [<<(SubstHypInConcl_LR $id)>>] -> ["Dependent Rewrite -> " $id]
| DRewriteRL [<<(SubstHypInConcl_RL $id)>>] -> ["Dependent Rewrite <- " $id]
| cutrewriteLR [<<(SubstConcl_LR $eqn)>>] -> ["CutRewrite -> " $eqn]
| cutrewriteLRin [<<(SubstHyp_LR $eqn $id)>>]
-> ["CutRewrite -> " $eqn:E [1 1]"in " $id]
| cutrewriteRL [<<(SubstConcl_RL $eqn)>>] -> ["CutRewrite <- " $eqn:E]
| cutrewriteRLin [<<(SubstHyp_RL $eqn $id)>>]
-> ["CutRewrite <- " $eqn:E [1 1]"in " $id]
|nil_consbase [<<(CONSBASE)>>] -> []
|single_consbase [<<(CONSBASE $tac)>>] -> [[1 0] $tac]
|nil_ortactic [<<(ORTACTIC)>>] -> []
|single_ortactic [<<(ORTACTIC $tac)>>] -> ["|" $tac]
|AutoRewrite [<<(AutoRewrite $id)>>] -> ["AutoRewrite " $id]
|AutoRewriteBaseList [<<(REDEXP (BaseList $ft ($LIST $tl)))>>] ->
["[" $ft (CONSBASE ($LIST $tl)) "]"]
|AutoRewriteStep [<<(REDEXP (Step $ft ($LIST $tl)))>>] ->
[[0 1] "Step=" "[" $ft (ORTACTIC ($LIST $tl)) "]"]
|AutoRewriteRest [<<(REDEXP (Rest $ft ($LIST $tl)))>>] ->
[[0 1] "Rest=" "[" $ft (ORTACTIC ($LIST $tl)) "]"]
|AutoRewriteSolveStep [<<(REDEXP (SolveStep))>>] -> ["with Solve"]
|AutoRewriteSolveRest [<<(REDEXP (SolveRest))>>] -> ["with Solve"]
|AutoRewriteUse [<<(REDEXP (Use))>>] -> ["with Use"]
|AutoRewriteAll [<<(REDEXP (All))>>] -> ["with All"]
|AutoRewriteCond [<<(REDEXP (Cond))>>] -> ["with Cond"]
|AutoRewriteDepth [<<(REDEXP (Depth $dth))>>] -> [[0 1] "Depth=" $dth]
|AutoRewriteByName [<<(REDEXP (ByName $id))>>] -> [ $id ]
|AutoRewriteExplicit [<<(REDEXP (Explicit $l))>>] -> ["[" $l "]"]
|AutoRewriteLR [<<(REDEXP (LR $c))>>] -> [ $c "LR" ]
|AutoRewriteRL [<<(REDEXP (RL $c))>>] -> [ $c "RL" ]
.
|
