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
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
|
(***********************************************************************)
(* 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 Hipattern
open Names
open Term
open Termops
open Reductionops
open Tacmach
open Util
open Declarations
open Libnames
let qflag=ref true
let (=?) f g i1 i2 j1 j2=
let c=f i1 i2 in
if c=0 then g j1 j2 else c
let (==?) fg h i1 i2 j1 j2 k1 k2=
let c=fg i1 i2 j1 j2 in
if c=0 then h k1 k2 else c
type ('a,'b) sum = Left of 'a | Right of 'b
type counter = bool -> metavariable
exception Is_atom of constr
let meta_succ m = m+1
let rec nb_prod_after n c=
match kind_of_term c with
| Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else
1+(nb_prod_after 0 b)
| _ -> 0
let nhyps mip =
let constr_types = mip.mind_nf_lc in
let hyp = nb_prod_after mip.mind_nparams in
Array.map hyp constr_types
let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind))
(* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
let ind_hyps nevar ind largs=
let (mib,mip) = Global.lookup_inductive ind in
let n = mip.mind_nparams in
(* assert (n=(List.length largs));*)
let lp=Array.length mip.mind_consnames in
let types= mip.mind_nf_lc in
let lp=Array.length types in
let myhyps i=
let t1=Term.prod_applist types.(i) largs in
let t2=snd (Sign.decompose_prod_n_assum nevar t1) in
fst (Sign.decompose_prod_assum t2) in
Array.init lp myhyps
let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
let id_not=lazy (destConst (constant "not"))
let id_iff=lazy (destConst (constant "iff"))
let match_with_evaluable gl t=
let env=pf_env gl in
match kind_of_term t with
App (hd,b)->
(match kind_of_term hd with
Const cst->
if (*Environ.evaluable_constant cst env*)
cst=(Lazy.force id_not) ||
cst=(Lazy.force id_iff) then
Some(EvalConstRef cst,t)
else None
| _-> None)
| _-> None
type kind_of_formula=
Arrow of constr*constr
| And of inductive*constr list
| Or of inductive*constr list
| Exists of inductive*constr list
| Forall of constr*constr
| Atom of constr
| Evaluable of evaluable_global_reference*constr
| False
let rec kind_of_formula gl term =
let cciterm=whd_betaiotazeta term in
match match_with_imp_term cciterm with
Some (a,b)-> Arrow(a,(pop b))
|_->
match match_with_forall_term cciterm with
Some (_,a,b)-> Forall(a,b)
|_->
match match_with_nodep_ind cciterm with
Some (i,l)->
let ind=destInd i in
let (mib,mip) = Global.lookup_inductive ind in
if Inductiveops.mis_is_recursive (ind,mib,mip) then
Atom cciterm
else
(match Array.length mip.mind_consnames with
0->False
| 1->And(ind,l)
| _->Or(ind,l))
| _ ->
match match_with_sigma_type cciterm with
Some (i,l)-> Exists((destInd i),l)
|_->
match match_with_evaluable gl cciterm with
Some (ec,t)->Evaluable (ec,t)
| None ->Atom cciterm
type atoms = {positive:constr list;negative:constr list}
let no_atoms = (false,{positive=[];negative=[]})
let build_atoms gl metagen polarity cciterm =
let trivial =ref false
and positive=ref []
and negative=ref [] in
let pfenv=lazy (pf_env gl) in
let rec build_rec env polarity cciterm =
match kind_of_formula gl cciterm with
False->if not polarity then trivial:=true
| Arrow (a,b)->
build_rec env (not polarity) a;
build_rec env polarity b
| And(i,l) | Or(i,l)->
let v = ind_hyps 0 i l in
let g i _ (_,_,t) =
build_rec env polarity (lift i t) in
let f l =
list_fold_left_i g (1-(List.length l)) () l in
if polarity && (* we have a constant constructor *)
array_exists (function []->true|_->false) v
then trivial:=true;
Array.iter f v
| Exists(i,l)->
let var=mkMeta (metagen true) in
let v =(ind_hyps 1 i l).(0) in
let g i _ (_,_,t) =
build_rec (var::env) polarity (lift i t) in
list_fold_left_i g (2-(List.length l)) () v
| Forall(_,b)->
let var=mkMeta (metagen true) in
build_rec (var::env) polarity b
| Atom t->
let unsigned=substnl env 0 t in
if polarity then
positive:= unsigned :: !positive
else
negative:= unsigned :: !negative
| Evaluable(ec,t)->
let nt=Tacred.unfoldn [[1],ec] (Lazy.force pfenv)
(Refiner.sig_sig gl) t in
build_rec env polarity nt
in
build_rec [] polarity cciterm;
(!trivial,
{positive= !positive;
negative= !negative})
type right_pattern =
Rand
| Ror
| Rforall
| Rexists of metavariable*constr*bool
| Rarrow
| Revaluable of evaluable_global_reference
type right_formula =
Complex of right_pattern*constr*atoms
| Atomic of constr
type left_arrow_pattern=
LLatom
| LLfalse
| LLand of inductive*constr list
| LLor of inductive*constr list
| LLforall of constr
| LLexists of inductive*constr list
| LLarrow of constr*constr*constr
| LLevaluable of evaluable_global_reference
type left_pattern=
Lfalse
| Land of inductive
| Lor of inductive
| Lforall of metavariable*constr*bool
| Lexists of inductive
| Levaluable of evaluable_global_reference
| LA of constr*left_arrow_pattern
type left_formula={id:global_reference;
constr:constr;
pat:left_pattern;
atoms:atoms;
internal:bool}
let build_left_entry nam typ internal gl metagen=
try
let m=meta_succ(metagen false) in
let trivial,atoms=
if !qflag then
build_atoms gl metagen false typ
else no_atoms in
let pattern=
match kind_of_formula gl typ with
False -> Lfalse
| Atom a -> raise (Is_atom a)
| And(i,_) -> Land i
| Or(i,_) -> Lor i
| Exists (ind,_) -> Lexists ind
| Forall (d,_) ->
Lforall(m,d,trivial)
| Evaluable (egc,_) ->Levaluable egc
| Arrow (a,b) ->LA (a,
match kind_of_formula gl a with
False-> LLfalse
| Atom t-> LLatom
| And(i,l)-> LLand(i,l)
| Or(i,l)-> LLor(i,l)
| Arrow(a,c)-> LLarrow(a,c,b)
| Exists(i,l)->LLexists(i,l)
| Forall(_,_)->LLforall a
| Evaluable (egc,_)-> LLevaluable egc) in
Left {id=nam;
constr=typ;
pat=pattern;
atoms=atoms;
internal=internal}
with Is_atom a-> Right a
let build_right_entry typ gl metagen=
try
let m=meta_succ(metagen false) in
let trivial,atoms=
if !qflag then
build_atoms gl metagen true typ
else no_atoms in
let pattern=
match kind_of_formula gl typ with
False -> raise (Is_atom typ)
| Atom a -> raise (Is_atom a)
| And(_,_) -> Rand
| Or(_,_) -> Ror
| Exists (i,l) ->
let (_,_,d)=list_last (ind_hyps 0 i l).(0) in
Rexists(m,d,trivial)
| Forall (_,a) -> Rforall
| Arrow (a,b) -> Rarrow
| Evaluable (egc,_)->Revaluable egc in
Complex(pattern,typ,atoms)
with Is_atom a-> Atomic a
|
