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
|
(***********************************************************************)
(* 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 *)
(***********************************************************************)
(*i $Id$ i*)
open Util
open Formula
open Sequent
open Tacmach
open Term
open Termops
open Reductionops
exception UFAIL of constr*constr
let unif t1 t2= (* Martelli-Montanari style *)
let bige=Queue.create ()
and sigma=ref [] in
let bind i t=
sigma:=(i,t)::
(List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in
let rec head_reduce t=
(* forbids non-sigma-normal meta in head position*)
match kind_of_term t with
Meta i->
(try
head_reduce (List.assoc i !sigma)
with Not_found->t)
| _->t in
Queue.add (t1,t2) bige;
try while true do
let t1,t2=Queue.take bige in
let nt1=head_reduce (whd_betaiotazeta t1)
and nt2=head_reduce (whd_betaiotazeta t2) in
match (kind_of_term nt1),(kind_of_term nt2) with
Meta i,Meta j->
if i<>j then
if i<j then bind j nt1
else bind i nt2
| Meta i,_ ->
let t=subst_meta !sigma nt2 in
if Intset.is_empty (free_rels t) &&
not (occur_term (mkMeta i) t) then
bind i t else raise (UFAIL(nt1,nt2))
| _,Meta i ->
let t=subst_meta !sigma nt1 in
if Intset.is_empty (free_rels t) &&
not (occur_term (mkMeta i) t) then
bind i t else raise (UFAIL(nt1,nt2))
| Cast(_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
| _,Cast(_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
| (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
| Case (_,pa,ca,va),Case (_,pb,cb,vb)->
Queue.add (pa,pb) bige;
Queue.add (ca,cb) bige;
let l=Array.length va in
if l<>(Array.length vb) then
raise (UFAIL (nt1,nt2))
else
for i=0 to l-1 do
Queue.add (va.(i),vb.(i)) bige
done
| App(ha,va),App(hb,vb)->
Queue.add (ha,hb) bige;
let l=Array.length va in
if l<>(Array.length vb) then
raise (UFAIL (nt1,nt2))
else
for i=0 to l-1 do
Queue.add (va.(i),vb.(i)) bige
done
| _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2))
done;
assert false
(* this place is unreachable but needed for the sake of typing *)
with Queue.Empty-> !sigma
(* collect tries finds ground instantiations for Meta i*)
let is_ground t=(Clenv.collect_metas t)=[]
let collect i l=
try
let t=List.assoc i l in
if is_ground t then Some t else None
with Not_found->None
let value i=
let tref=mkMeta i in
let rec vaux term=
if term=tref then 1 else
let f v t=max v (vaux t) in
let vrec=fold_constr f 0 term in
if vrec=0 then 0 else succ vrec in vaux
let is_head_meta t=match kind_of_term t with Meta _->true | _ ->false
let unif_atoms_for_meta i (b1,t1) (b2,t2)=
if b1=b2 || is_head_meta t1 || is_head_meta t2 then None else
try
match collect i (unif t1 t2) with
None->None
| Some t->Some ((max (value i t1) (value i t2)),t)
with UFAIL(_,_) ->None
module OrderedConstr=
struct
type t=int*constr
let compare (n1,t1) (n2,t2)=
(n2 - n1) +- (Pervasives.compare t1 t2)
(* we want a decreasing total order *)
end
module CS=Set.Make(OrderedConstr)
let match_atom_list i atom l=
let f atom2 accu=
match unif_atoms_for_meta i atom atom2 with
None-> accu
| Some t-> CS.add t accu in
List.fold_right f l CS.empty
let match_lists i l1 l2=
let f atom accu=
CS.union (match_atom_list i atom l2) accu in
List.fold_right f l1 CS.empty
let find_instances i l seq=
let match_hyp f accu=
CS.union
(if f.internal then
match_lists i l f.atoms
else
CS.empty)
accu in
let match_atom t accu=
CS.union (match_atom_list i (false,t) l) accu in
let s1=
match seq.gl with
Atomic t->(match_atom_list i (true,t) l)
| Complex(_,_,l1)->(match_lists i l l1) in
let s2=List.fold_right match_atom seq.latoms s1 in
let s3=HP.fold match_hyp seq.redexes s2 in
List.map snd (CS.elements s3)
|
