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
|
(***********************************************************************)
(* 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
type ('a,'b)sum=Left of 'a|Right of 'b
type kind_of_formula=
Arrow of constr*constr
|And of inductive*constr list
|Or of inductive*constr list
|Exists of inductive*constr*constr*constr
|Forall of constr*constr
|Atom of constr
|False
type counter = bool -> int
let newcnt ()=
let cnt=ref (-1) in
fun b->if b then incr cnt;!cnt
let constant path str ()=Coqlib.gen_constant "User" ["Init";path] str
let op2bool=function Some _->true |None->false
let id_ex=constant "Logic" "ex"
let id_sig=constant "Specif" "sig"
let id_sigT=constant "Specif" "sigT"
let id_sigS=constant "Specif" "sigS"
let id_not=constant "Logic" "not"
let is_ex t =
t=(id_ex ()) ||
t=(id_sig ()) ||
t=(id_sigT ()) ||
t=(id_sigS ())
let match_with_exist_term t=
match kind_of_term t with
App(t,v)->
if t=id_ex () && (Array.length v)=2 then
let p=v.(1) in
match kind_of_term p with
Lambda(na,a,b)->Some(t,a,b,p)
| _ ->Some(t,v.(0),mkApp(p,[|mkRel 1|]),p)
else None
| _->None
let match_with_not_term t=
match match_with_nottype t with
| None ->
(match kind_of_term t with
App (no,b) when no=id_not ()->Some (no,b.(0))
| _->None)
| o -> o
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 nhyps = nb_prod_after mip.mind_nparams in
Array.map nhyps constr_types
let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind))
exception Dependent_Inductive
(* builds the array of arrays of constructor hyps for (ind Vargs)*)
let ind_hyps ind largs=
let (mib,mip) = Global.lookup_inductive ind in
let n = mip.mind_nparams in
if n<>(List.length largs) then
raise Dependent_Inductive
else
let p=nhyps mip in
let lp=Array.length p in
let types= mip.mind_nf_lc in
let myhyps i=
let t1=Term.prod_applist types.(i) largs in
fst (Sign.decompose_prod_n_assum p.(i) t1) in
Array.init lp myhyps
let kind_of_formula cciterm =
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_exist_term cciterm with
Some (i,a,b,p)-> Exists((destInd i),a,b,p)
|_->
match match_with_nodep_ind cciterm with
None -> Atom cciterm
| 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)
let build_atoms metagen=
let rec build_rec env polarity cciterm =
match kind_of_formula cciterm with
False->[]
| Arrow (a,b)->
(build_rec env (not polarity) a)@
(build_rec env polarity b)
| And(i,l) | Or(i,l)->
(try
let v = ind_hyps i l in
Array.fold_right
(fun l accu->
List.fold_right
(fun (_,_,t) accu0->
(build_rec env polarity t)@accu0) l accu) v []
with Dependent_Inductive ->
[polarity,(substnl env 0 cciterm)])
| Forall(_,b)|Exists(_,_,b,_)->
let var=mkMeta (metagen true) in
build_rec (var::env) polarity b
| Atom t->
[polarity,(substnl env 0 cciterm)]
in build_rec []
type right_pattern =
Rand
| Ror
| Rforall
| Rexists of int*constr
| Rarrow
type right_formula =
Complex of right_pattern*((bool*constr) list)
| Atomic of constr
type left_pattern=
Lfalse
| Land of inductive
| Lor of inductive
| Lforall of int*constr
| Lexists
| LAatom of constr
| LAfalse
| LAand of inductive*constr list
| LAor of inductive*constr list
| LAforall of constr
| LAexists of inductive*constr*constr*constr
| LAarrow of constr*constr*constr
type left_formula={id:global_reference;
pat:left_pattern;
atoms:(bool*constr) list;
internal:bool}
exception Is_atom of constr
let build_left_entry nam typ internal metagen=
try
let pattern=
match kind_of_formula typ with
False -> Lfalse
| Atom a -> raise (Is_atom a)
| And(i,_) -> Land i
| Or(i,_) -> Lor i
| Exists (_,_,_,_) -> Lexists
| Forall (d,_) -> let m=1+(metagen false) in Lforall(m,d)
| Arrow (a,b) ->
(match kind_of_formula a with
False-> LAfalse
| Atom a-> LAatom a
| And(i,l)-> LAand(i,l)
| Or(i,l)-> LAor(i,l)
| Arrow(a,c)-> LAarrow(a,c,b)
| Exists(i,a,_,p)->LAexists(i,a,p,b)
| Forall(_,_)->LAforall a) in
let l=build_atoms metagen false typ in
Left {id=nam;pat=pattern;atoms=l;internal=internal}
with Is_atom a-> Right a
let build_right_entry typ metagen=
try
let pattern=
match kind_of_formula typ with
False -> raise (Is_atom typ)
| Atom a -> raise (Is_atom a)
| And(_,_) -> Rand
| Or(_,_) -> Ror
| Exists (_,d,_,_) ->
let m=1+(metagen false) in Rexists(m,d)
| Forall (_,a) -> Rforall
| Arrow (a,b) -> Rarrow in
let l=build_atoms metagen true typ in
Complex(pattern,l)
with Is_atom a-> Atomic a
|
