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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Formula
open Sequent
open Rules
open Instances
open Term
open Tacmach
open Tacticals
let update_flags ()=
let predref=ref Names.Cpred.empty in
let f coe=
try
let kn= fst (destConst (Classops.get_coercion_value coe)) in
predref:=Names.Cpred.add kn !predref
with DestKO -> ()
in
List.iter f (Classops.coercions ());
red_flags:=
CClosure.RedFlags.red_add_transparent
CClosure.betaiotazeta
(Names.Id.Pred.full,Names.Cpred.complement !predref)
let ground_tac solver startseq gl=
update_flags ();
let rec toptac skipped seq gl=
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
then Feedback.msg_debug (Printer.pr_goal 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 (Pp.str "reversible in 1st order mode")
else
backtrack in
forall_tac backtrack1 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 backtrack 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
let seq, gl' = startseq gl in
wrap (List.length (pf_hyps gl)) true (toptac []) seq gl'
|
