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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
(* $Id$ *)
open Formula
open Sequent
open Rules
open Term
open Tacmach
open Tactics
open Tacticals
open Util
let mytac ninst solver gl=
let metagen=newcnt () in
let rec toptac ninst seq gl=
match seq.gl with
Atomic t->
tclORELSE (axiom_tac t seq) (left_tac ninst seq []) gl
| Complex (pat,l)->
match pat with
Rand->and_tac seq (toptac ninst) metagen gl
| Rforall->forall_tac seq (toptac ninst) metagen gl
| Rarrow->arrow_tac seq (toptac ninst) metagen gl
| _->
if not (is_empty_left seq) && rev_left seq then
left_tac ninst seq [] gl
else
right_tac ninst seq pat l [] gl
and right_tac ninst seq pat atoms ctx gl=
let re_add s=re_add_left_list ctx s in
match pat with
Ror->
tclORELSE
(or_tac (re_add seq) (toptac ninst) metagen)
(left_tac ninst seq ctx) gl
| Rexists(i,dom)->
tclORELSE
(if ninst=0 then tclFAIL 0 "max depth" else
exists_tac i dom atoms (re_add seq) (toptac (ninst-1)) metagen)
(left_tac ninst seq ctx) gl
| _-> anomaly "unreachable place"
and left_tac ninst seq ctx gl=
if is_empty_left seq then
solver gl (* put solver here *)
else
let (hd,seq1)=take_left seq in
let re_add s=re_add_left_list ctx s in
match hd.pat with
Lfalse->left_false_tac hd.id gl
| Land ind->left_and_tac ind hd.id seq1 (toptac ninst) metagen gl
| Lor ind->left_or_tac ind hd.id seq1 (toptac ninst) metagen gl
| Lforall (i,dom)->
tclORELSE
(if ninst=0 then tclFAIL 0 "max depth" else
left_forall_tac i dom hd.atoms hd.id (re_add seq)
(toptac (ninst-1)) metagen)
(left_tac ninst seq1 (hd::ctx)) gl
| Lexists ->left_exists_tac hd.id seq1 (toptac ninst) metagen gl
| LAatom a->
let pat,atoms=
match seq1.gl with
Atomic t->assert false
| Complex (pat,atoms)->pat,atoms in
tclORELSE
(ll_atom_tac a hd.id (re_add seq1) (toptac ninst) metagen)
(right_tac ninst seq1 pat atoms (hd::ctx)) gl
| LAfalse->ll_false_tac hd.id seq1 (toptac ninst) metagen gl
| LAand (ind,largs) | LAor(ind,largs) ->
ll_ind_tac ind largs hd.id seq1 (toptac ninst) metagen gl
| LAforall p ->
tclORELSE
(if ninst=0 then tclFAIL 0 "max depth" else
ll_forall_tac p hd.id (re_add seq1)
(toptac (ninst-1)) metagen)
(left_tac ninst seq1 (hd::ctx)) gl
| LAexists (ind,a,p,_) ->
ll_ind_tac ind [a;p] hd.id seq1 (toptac ninst) metagen gl
| LAarrow (a,b,c) ->
tclORELSE
(ll_arrow_tac a b c hd.id (re_add seq1)
(toptac ninst) metagen)
(left_tac ninst seq1 (hd::ctx)) gl in
wrap (List.length (pf_hyps gl)) true empty_seq (toptac ninst) metagen gl
let default_solver=Tacinterp.interp <:tactic<Auto with *>>
let default_depth=5
TACTIC EXTEND Ground
[ "Ground" ] -> [ mytac default_depth default_solver]
| [ "Ground" integer(n)] -> [ mytac n default_solver]
| [ "Ground" tactic(t)] -> [ mytac default_depth (snd t)]
| [ "Ground" integer(n) tactic(t)] -> [ mytac n (snd t)]
END
|
