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
266
267
268
269
270
271
272
273
274
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Hipattern
open Names
open Constr
open EConstr
open Vars
open Termops
open Util
open Declarations
open Globnames
module RelDecl = Context.Rel.Declaration
let qflag=ref true
let red_flags=ref CClosure.betaiotazeta
let (=?) f g i1 i2 j1 j2=
let c=f i1 i2 in
if Int.equal 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 Int.equal 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 Constr.kind c with
| Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else
1+(nb_prod_after 0 b)
| _ -> 0
let construct_nhyps env ind =
let nparams = (fst (Global.lookup_inductive (fst ind))).mind_nparams in
let constr_types = Inductiveops.arities_of_constructors env ind in
let hyp = nb_prod_after nparams in
Array.map hyp constr_types
(* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
let ind_hyps env sigma nevar ind largs =
let types= Inductiveops.arities_of_constructors env ind in
let myhyps t =
let t = EConstr.of_constr t in
let nparam_decls = Context.Rel.length (fst (Global.lookup_inductive (fst ind))).mind_params_ctxt in
let t1=Termops.prod_applist_assum sigma nparam_decls t largs in
let t2=snd (decompose_prod_n_assum sigma nevar t1) in
fst (decompose_prod_assum sigma t2) in
Array.map myhyps types
let special_nf env sigma t =
Reductionops.clos_norm_flags !red_flags env sigma t
let special_whd env sigma t =
Reductionops.clos_whd_flags !red_flags env sigma t
type kind_of_formula=
Arrow of constr*constr
| False of pinductive*constr list
| And of pinductive*constr list*bool
| Or of pinductive*constr list*bool
| Exists of pinductive*constr list
| Forall of constr*constr
| Atom of constr
let pop t = Vars.lift (-1) t
let kind_of_formula env sigma term =
let normalize = special_nf env sigma in
let cciterm = special_whd env sigma term in
match match_with_imp_term sigma cciterm with
Some (a,b)-> Arrow (a, pop b)
|_->
match match_with_forall_term sigma cciterm with
Some (_,a,b)-> Forall (a, b)
|_->
match match_with_nodep_ind sigma cciterm with
Some (i,l,n)->
let ind,u=EConstr.destInd sigma i in
let u = EConstr.EInstance.kind sigma u in
let (mib,mip) = Global.lookup_inductive ind in
let nconstr=Array.length mip.mind_consnames in
if Int.equal nconstr 0 then
False((ind,u),l)
else
let has_realargs=(n>0) in
let is_trivial=
let is_constant c =
Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in
Array.exists is_constant mip.mind_nf_lc in
if Inductiveops.mis_is_recursive (ind,mib,mip) ||
(has_realargs && not is_trivial)
then
Atom cciterm
else
if Int.equal nconstr 1 then
And((ind,u),l,is_trivial)
else
Or((ind,u),l,is_trivial)
| _ ->
match match_with_sigma_type sigma cciterm with
Some (i,l)->
let (ind, u) = EConstr.destInd sigma i in
let u = EConstr.EInstance.kind sigma u in
Exists((ind, u), l)
|_-> Atom (normalize cciterm)
type atoms = {positive:constr list;negative:constr list}
type side = Hyp | Concl | Hint
let no_atoms = (false,{positive=[];negative=[]})
let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *)
let build_atoms env sigma metagen side cciterm =
let trivial =ref false
and positive=ref []
and negative=ref [] in
let normalize=special_nf env sigma in
let rec build_rec subst polarity cciterm=
match kind_of_formula env sigma cciterm with
False(_,_)->if not polarity then trivial:=true
| Arrow (a,b)->
build_rec subst (not polarity) a;
build_rec subst polarity b
| And(i,l,b) | Or(i,l,b)->
if b then
begin
let unsigned=normalize (substnl subst 0 cciterm) in
if polarity then
positive:= unsigned :: !positive
else
negative:= unsigned :: !negative
end;
let v = ind_hyps env sigma 0 i l in
let g i _ decl =
build_rec subst polarity (lift i (RelDecl.get_type decl)) 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 env sigma 1 i l).(0) in
let g i _ decl =
build_rec (var::subst) polarity (lift i (RelDecl.get_type decl)) in
List.fold_left_i g (2-(List.length l)) () v
| Forall(_,b)->
let var=mkMeta (metagen true) in
build_rec (var::subst) polarity b
| Atom t->
let unsigned=substnl subst 0 t in
if not (isMeta sigma unsigned) then (* discarding wildcard atoms *)
if polarity then
positive:= unsigned :: !positive
else
negative:= unsigned :: !negative in
begin
match side with
Concl -> build_rec [] true cciterm
| Hyp -> build_rec [] false cciterm
| Hint ->
let rels,head=decompose_prod sigma cciterm in
let subst=List.rev_map (fun _->mkMeta (metagen true)) rels in
build_rec subst false head;trivial:=false (* special for hints *)
end;
(!trivial,
{positive= !positive;
negative= !negative})
type right_pattern =
Rarrow
| Rand
| Ror
| Rfalse
| Rforall
| Rexists of metavariable*constr*bool
type left_arrow_pattern=
LLatom
| LLfalse of pinductive*constr list
| LLand of pinductive*constr list
| LLor of pinductive*constr list
| LLforall of constr
| LLexists of pinductive*constr list
| LLarrow of constr*constr*constr
type left_pattern=
Lfalse
| Land of pinductive
| Lor of pinductive
| Lforall of metavariable*constr*bool
| Lexists of pinductive
| LA of constr*left_arrow_pattern
type t={id:global_reference;
constr:constr;
pat:(left_pattern,right_pattern) sum;
atoms:atoms}
let build_formula env sigma side nam typ metagen=
let normalize = special_nf env sigma in
try
let m=meta_succ(metagen false) in
let trivial,atoms=
if !qflag then
build_atoms env sigma metagen side typ
else no_atoms in
let pattern=
match side with
Concl ->
let pat=
match kind_of_formula env sigma typ with
False(_,_) -> Rfalse
| Atom a -> raise (Is_atom a)
| And(_,_,_) -> Rand
| Or(_,_,_) -> Ror
| Exists (i,l) ->
let d = RelDecl.get_type (List.last (ind_hyps env sigma 0 i l).(0)) in
Rexists(m,d,trivial)
| Forall (_,a) -> Rforall
| Arrow (a,b) -> Rarrow in
Right pat
| _ ->
let pat=
match kind_of_formula env sigma typ with
False(i,_) -> Lfalse
| Atom a -> raise (Is_atom a)
| And(i,_,b) ->
if b then
let nftyp=normalize typ in raise (Is_atom nftyp)
else Land i
| Or(i,_,b) ->
if b then
let nftyp=normalize typ in raise (Is_atom nftyp)
else Lor i
| Exists (ind,_) -> Lexists ind
| Forall (d,_) ->
Lforall(m,d,trivial)
| Arrow (a,b) ->
let nfa=normalize a in
LA (nfa,
match kind_of_formula env sigma a with
False(i,l)-> LLfalse(i,l)
| 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) in
Left pat
in
Left {id=nam;
constr=normalize typ;
pat=pattern;
atoms=atoms}
with Is_atom a-> Right a (* already in nf *)
|
