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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Ltac_plugin
open Formula
open Sequent
open Rules
open Instances
open Constr
open Tacmach.New
open Tacticals.New
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 =
Proofview.Goal.enter begin fun gl ->
update_flags ();
let rec toptac skipped seq =
Proofview.Goal.enter begin fun gl ->
let () =
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
then
let gl = { Evd.it = Proofview.Goal.goal gl; sigma = project gl } in
Feedback.msg_debug (Printer.pr_goal gl)
in
tclORELSE (axiom_tac seq.gl seq)
begin
try
let (hd,seq1)=take_formula (project gl) seq
and re_add s=re_add_formula_list (project gl) skipped s in
let continue=toptac []
and backtrack =toptac (hd::skipped) seq1 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 (project gl) 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 (project gl) 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
end in
let n = List.length (Proofview.Goal.hyps gl) in
startseq (fun seq -> wrap n true (toptac []) seq)
end
|
