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
open Ltac_plugin
open Formula
open Sequent
open Rules
open Instances
open Tacmach
open Tacticals
let get_flags qflag =
let open TransparentState in
let f accu coe = match coe.Coercionops.coe_value with
| Names.GlobRef.ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst }
| _ -> accu
in
let flags = List.fold_left f TransparentState.full (Coercionops.coercions ()) in
{ Formula.reds =
CClosure.RedFlags.red_add_transparent
CClosure.all
flags; qflag }
let get_id hd = match hd.id with FormulaId id -> id
let ground_tac ~flags solver startseq =
Proofview.Goal.enter begin fun gl ->
let rec toptac skipped seq =
Proofview.Goal.enter begin fun gl ->
let () =
if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
then
Feedback.msg_debug (Printer.Debug.pr_goal gl)
in
tclORELSE (axiom_tac 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
let AnyFormula hd = hd in
match hd.pat with
RightPattern rpat->
begin
match rpat with
Rand->
and_tac ~flags backtrack continue (re_add seq1)
| Rforall->
let backtrack1=
if flags.qflag then
tclFAIL (Pp.str "reversible in 1st order mode")
else
backtrack in
forall_tac ~flags backtrack1 continue (re_add seq1)
| Rarrow->
arrow_tac ~flags backtrack continue (re_add seq1)
| Ror->
or_tac ~flags 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 flags.qflag && Sequent.has_fuel seq then
quantified_tac ~flags lfp backtrack2
continue (re_add seq)
else
backtrack2
end
| LeftPattern lpat->
begin
match lpat with
Lfalse->
left_false_tac (get_id hd)
| Land ind->
left_and_tac ~flags ind backtrack
(get_id hd) continue (re_add seq1)
| Lor ind->
left_or_tac ~flags ind backtrack
(get_id hd) continue (re_add seq1)
| Lforall (_,_,_)->
let (lfp,seq2)=collect_quantified (project gl) seq in
let backtrack2=toptac (lfp@skipped) seq2 in
if flags.qflag && Sequent.has_fuel seq then
quantified_tac ~flags lfp backtrack2
continue (re_add seq)
else
backtrack2
| Lexists ind ->
if flags.qflag then
left_exists_tac ~flags ind backtrack (get_id hd)
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 ~flags ind largs backtrack
(get_id hd) continue (re_add seq1))
| LLforall p ->
if Sequent.has_fuel seq && flags.qflag then
(ll_forall_tac ~flags p backtrack
(get_id hd) continue (re_add seq1))
else backtrack
| LLexists (ind,l) ->
if flags.qflag then
ll_ind_tac ~flags ind l backtrack
(get_id hd) continue (re_add seq1)
else
backtrack
| LLarrow (a,b,c) ->
(ll_arrow_tac ~flags a b c backtrack
(get_id hd) continue (re_add seq1))
end in
ll_atom_tac ~flags typ la_tac (get_id hd) 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 ~flags n true (toptac []) seq)
end