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
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(* $Id$ *)
open Formula
open Sequent
open Rules
open Instances
open Term
open Tacmach
open Tactics
open Tacticals
let ground_tac solver startseq gl=
let rec toptac skipped seq gl=
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
then Pp.msgnl (Proof_trees.pr_goal (sig_it gl));
tclORELSE (axiom_tac seq.gl seq)
begin
try
let (hd,seq1)=take_formula seq
and re_add s=re_add_formula_list skipped s in
let continue=toptac []
and backtrack gl=toptac (hd::skipped) seq1 gl in
match hd.pat with
Right rpat->
begin
match rpat with
Rand->
and_tac backtrack continue (re_add seq1)
| Rforall->
let backtrack1=
if !qflag then
tclFAIL 0 "reversible in 1st order mode"
else
backtrack in
forall_tac backtrack continue (re_add seq1)
| Rarrow->
arrow_tac backtrack continue (re_add seq1)
| Ror->
or_tac backtrack continue (re_add seq1)
| Rfalse->backtrack
| Rexists(i,dom,triv)->
let (lfp,seq2)=collect_quantified seq in
let backtrack2=toptac (lfp@skipped) seq2 in
if !qflag && seq.depth>0 then
quantified_tac lfp backtrack2
continue (re_add seq)
else
backtrack2 (* need special backtracking *)
end
| Left lpat->
begin
match lpat with
Lfalse->
left_false_tac hd.id
| Land ind->
left_and_tac ind backtrack
hd.id continue (re_add seq1)
| Lor ind->
left_or_tac ind backtrack
hd.id continue (re_add seq1)
| Lforall (_,_,_)->
let (lfp,seq2)=collect_quantified seq in
let backtrack2=toptac (lfp@skipped) seq2 in
if !qflag && seq.depth>0 then
quantified_tac lfp backtrack2
continue (re_add seq)
else
backtrack2 (* need special backtracking *)
| Lexists ind ->
if !qflag then
left_exists_tac ind hd.id continue (re_add seq1)
else backtrack
| LA (typ,lap)->
let la_tac=
begin
match lap with
LLatom -> backtrack
| LLand (ind,largs) | LLor(ind,largs)
| LLfalse (ind,largs)->
(ll_ind_tac ind largs backtrack
hd.id continue (re_add seq1))
| LLforall p ->
if seq.depth>0 && !qflag then
(ll_forall_tac p backtrack
hd.id continue (re_add seq1))
else backtrack
| LLexists (ind,l) ->
if !qflag then
ll_ind_tac ind l backtrack
hd.id continue (re_add seq1)
else
backtrack
| LLarrow (a,b,c) ->
(ll_arrow_tac a b c backtrack
hd.id continue (re_add seq1))
end in
ll_atom_tac typ la_tac hd.id continue (re_add seq1)
end
with Heap.EmptyHeap->solver
end gl in
wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
|
