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
open Formula
open Sequent
open Rules
open Instances
open Tacticals
let get_flags () =
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 = RedFlags.red_add_transparent RedFlags.all flags }
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 env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
tclORELSE (axiom_tac ~flags seq)
begin
try
let (hd, seq1) = take_formula env sigma seq
and re_add s=re_add_formula_list sigma 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=
tclFAIL (Pp.str "reversible in 1st order mode")
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 env sigma seq in
let backtrack2=toptac (lfp@skipped) seq2 in
if 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 env sigma seq in
let backtrack2=toptac (lfp@skipped) seq2 in
if Sequent.has_fuel seq then
quantified_tac ~flags lfp backtrack2
continue (re_add seq)
else
backtrack2
| Lexists ind ->
left_exists_tac ~flags ind backtrack (get_id hd)
continue (re_add seq1)
| LA 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 then
(ll_forall_tac ~flags p backtrack
(get_id hd) continue (re_add seq1))
else backtrack
| LLexists (ind,l) ->
ll_ind_tac ~flags ind l backtrack
(get_id hd) continue (re_add seq1)
| 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 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