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
|
(***********************************************************************)
(* 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
let priority=function (* pure heuristics, <=0 for non reversible *)
Lfalse ->1000
| Land _ -> 90
| Lor _ -> 40
| Lforall (_,_) -> -20
| Lexists -> 60
| LAatom _ -> 0
| LAfalse -> 100
| LAand (_,_) -> 80
| LAor (_,_) -> 70
| LAforall _ -> -30
| LAexists (_,_,_,_) -> 50
| LAarrow (_,_,_) -> -10
let right_atomic=function
Atomic _->true
| Complex (_,_) ->false
let right_reversible=
function
Rarrow | Rand | Rforall->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 compare=Pervasives.compare
end
module CM=Map.Make(OrderedConstr)
module HP=Heap.Functional(OrderedFormula)
type t=
{hyps:HP.t;hatoms:global_reference CM.t;gl:right_formula}
let add_left (nam,t) seq internal metagen=
match build_left_entry nam t internal metagen with
Left f->{seq with hyps=HP.add f seq.hyps}
| Right t->{seq with hatoms=CM.add t nam seq.hatoms}
let re_add_left_list lf seq=
{seq with hyps=List.fold_right HP.add lf seq.hyps}
let change_right t seq metagen=
{seq with gl=build_right_entry t metagen}
let find_left t seq=CM.find t seq.hatoms
let atomic_right seq= right_atomic seq.gl
let rev_left seq=
try
let lpat=(HP.maximum seq.hyps).pat in
left_reversible lpat
with Heap.EmptyHeap -> false
let is_empty_left seq=
seq.hyps=HP.empty
let take_left seq=
let hd=HP.maximum seq.hyps
and hp=HP.remove seq.hyps in
hd,{seq with hyps=hp}
let take_right seq=seq.gl
let empty_seq=
{hyps=HP.empty;
hatoms=CM.empty;
gl=Atomic (mkMeta 1)}
open Auto
let create_with_auto_hints gl metagen=
let seqref=ref empty_seq 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 metagen
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
|
