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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
|
(***********************************************************************)
(* 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 Term
open Util
open Formula
open Tacmach
open Names
open Libnames
open Pp
let newcnt ()=
let cnt=ref (-1) in
fun b->if b then incr cnt;!cnt
let priority = function (* pure heuristics, <=0 for non reversible *)
Lfalse ->1000
| Land _ -> 90
| Lor _ -> 40
| Lforall (_,_) -> -30 (* must stay at lowest priority *)
| Lexists -> 60
| Levaluable _ -> 100
| LA(_,lap) ->
match lap with
LLatom -> 0
| LLfalse -> 100
| LLand (_,_) -> 80
| LLor (_,_) -> 70
| LLforall _ -> -20
| LLexists (_,_,_,_) -> 50
| LLarrow (_,_,_) -> -10
| LLevaluable _ -> 100
let right_reversible=
function
Rarrow | Rand | Rforall | Revaluable _ ->true
| _ ->false
let left_reversible lpat=(priority lpat)>0
module OrderedFormula=
struct
type t=left_formula
let compare e1 e2=
(priority e1.pat) - (priority e2.pat)
end
module OrderedConstr=
struct
type t=constr
let rec compare c1 c2=
match (kind_of_term c1,kind_of_term c2) with
(Prod(_,a1,b1),Prod(_,a2,b2))
| (Lambda(_,a1,b1),Lambda(_,a2,b2)) ->
(compare a1 a2) +- (compare b1 b2)
| (LetIn(_,a1,b1,aa1),LetIn(_,a2,b2,aa2)) ->
((compare a1 a2) +- (compare b1 b2)) +- (compare aa1 aa2)
| _-> Pervasives.compare c1 c2
end
module Hitem=
struct
type t=(global_reference * constr option)
let compare (id1,co1) (id2,co2)=
(Pervasives.compare id1 id2) +-
(match co1,co2 with
Some c1,Some c2 -> OrderedConstr.compare c1 c2
| _->Pervasives.compare co1 co2)
end
module CM=Map.Make(OrderedConstr)
module History=Set.Make(Hitem)
let cm_add typ nam cm=
try
let l=CM.find typ cm in CM.add typ (nam::l) cm
with
Not_found->CM.add typ [nam] cm
let cm_remove typ nam cm=
try
let l=CM.find typ cm in
let l0=List.filter (fun id->id<>nam) l in
match l0 with
[]->CM.remove typ cm
| _ ->CM.add typ l0 cm
with Not_found ->cm
module HP=Heap.Functional(OrderedFormula)
type t=
{redexes:HP.t;
context:(global_reference list) CM.t;
latoms:constr list;
gl:right_formula;
cnt:counter;
history:History.t;
depth:int}
let deepen seq={seq with depth=seq.depth-1}
let record id topt seq={seq with history=History.add (id,topt) seq.history}
let lookup id topt seq=History.mem (id,topt) seq.history
let add_left (nam,t) seq internal gl=
match build_left_entry nam t internal gl seq.cnt with
Left f->{seq with
redexes=HP.add f seq.redexes;
context=cm_add f.constr nam seq.context}
| Right t->{seq with
context=cm_add t nam seq.context;
latoms=t::seq.latoms}
let re_add_left_list lf seq=
{seq with
redexes=List.fold_right HP.add lf seq.redexes;
context=List.fold_right
(fun f cm->cm_add f.constr f.id cm) lf seq.context}
let change_right t seq gl=
{seq with gl=build_right_entry t gl seq.cnt}
let find_left t seq=List.hd (CM.find t seq.context)
let rev_left seq=
try
let lpat=(HP.maximum seq.redexes).pat in
left_reversible lpat
with Heap.EmptyHeap -> false
let is_empty_left seq=
seq.redexes=HP.empty
let take_left seq=
let hd=HP.maximum seq.redexes
and hp=HP.remove seq.redexes in
hd,{seq with
redexes=hp;
context=cm_remove hd.constr hd.id seq.context}
let take_right seq=seq.gl
let empty_seq depth=
{redexes=HP.empty;
context=CM.empty;
latoms=[];
gl=Atomic (mkMeta 1);
cnt=newcnt ();
history=History.empty;
depth=depth}
let create_with_ref_list l depth gl=
let f gr seq=
let c=constr_of_reference gr in
let typ=(pf_type_of gl c) in
add_left (gr,typ) seq false gl in
List.fold_right f l (empty_seq depth)
open Auto
let create_with_auto_hints depth gl=
let seqref=ref (empty_seq depth) in
let f p_a_t =
match p_a_t.code with
Res_pf (c,_) | Give_exact c
| Res_pf_THEN_trivial_fail (c,_) ->
(try
let gr=reference_of_constr c in
let typ=(pf_type_of gl c) in
seqref:=add_left (gr,typ) !seqref false gl
with Not_found->())
| _-> () in
let g _ l=List.iter f l in
let h str hdb=Hint_db.iter g hdb in
Util.Stringmap.iter h (!searchtable);
!seqref
let print_cmap map=
let print_entry c l s=
let xc=Constrextern.extern_constr false (Global.env ()) c in
str "| " ++
Util.prlist (Ppconstr.pr_global Idset.empty) l ++
str " : " ++
Ppconstr.pr_constr xc ++
cut () ++
s in
msgnl (v 0
(str "-----" ++
cut () ++
CM.fold print_entry map (mt ()) ++
str "-----"))
|
