1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*)
11
(* $Id: hipattern.ml4 11739 2009-01-02 19:33:19Z herbelin $ *)
31
(* I implemented the following functions which test whether a term t
32
is an inductive but non-recursive type, a general conjuction, a
33
general disjunction, or a type with no constructors.
35
They are more general than matching with or_term, and_term, etc,
36
since they do not depend on the name of the type. Hence, they
37
also work on ad-hoc disjunctions introduced by the user.
39
-- Eduardo (6/8/97). *)
41
type 'a matching_function = constr -> 'a option
43
type testing_function = constr -> bool
45
let mkmeta n = Nameops.make_ident "X" (Some n)
51
let op2bool = function Some _ -> true | None -> false
53
let match_with_non_recursive_type t =
54
match kind_of_term t with
56
let (hdapp,args) = decompose_app t in
57
(match kind_of_term hdapp with
59
if not (Global.lookup_mind (fst ind)).mind_finite then
66
let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
68
(* Test dependencies *)
70
let rec has_nodep_prod_after n c =
71
match kind_of_term c with
73
( n>0 || not (dependent (mkRel 1) b))
74
&& (has_nodep_prod_after (n-1) b)
77
let has_nodep_prod = has_nodep_prod_after 0
79
(* A general conjunctive type is a non-recursive with-no-indices inductive
80
type with only one constructor and no dependencies between argument;
81
it is strict if it has the form
82
"Inductive I A1 ... An := C (_:A1) ... (_:An)" *)
84
(* style: None = record; Some false = conjunction; Some true = strict conj *)
86
let match_with_one_constructor style t =
87
let (hdapp,args) = decompose_app t in
88
match kind_of_term hdapp with
90
let (mib,mip) = Global.lookup_inductive ind in
91
if (Array.length mip.mind_consnames = 1)
92
&& (not (mis_is_recursive (ind,mib,mip)))
93
&& (mip.mind_nrealargs = 0)
95
if style = Some true (* strict conjunction *) then
97
fst (decompose_prod_assum (snd
98
(decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in
101
(fun (_,b,c) -> b=None && c = mkRel mib.mind_nparams) ctx
106
let ctyp = prod_applist mip.mind_nf_lc.(0) args in
107
let cargs = List.map pi3 (fst (decompose_prod_assum ctyp)) in
108
if style <> Some false || has_nodep_prod ctyp then
109
(* Record or non strict conjunction *)
110
Some (hdapp,List.rev cargs)
117
let match_with_conjunction ?(strict=false) t =
118
match_with_one_constructor (Some strict) t
120
let match_with_record t =
121
match_with_one_constructor None t
123
let is_conjunction ?(strict=false) t =
124
op2bool (match_with_conjunction ~strict t)
127
op2bool (match_with_record t)
130
(* A general disjunction type is a non-recursive with-no-indices inductive
131
type with of which all constructors have a single argument;
132
it is strict if it has the form
133
"Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
135
let test_strict_disjunction n lc =
136
array_for_all_i (fun i c ->
137
match fst (decompose_prod_assum (snd (decompose_prod_n_assum n c))) with
138
| [_,None,c] -> c = mkRel (n - i)
141
let match_with_disjunction ?(strict=false) t =
142
let (hdapp,args) = decompose_app t in
143
match kind_of_term hdapp with
145
let car = mis_constr_nargs ind in
146
let (mib,mip) = Global.lookup_inductive ind in
147
if array_for_all (fun ar -> ar = 1) car &&
148
not (mis_is_recursive (ind,mib,mip))
151
if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
157
Array.map (fun ar -> pi2 (destProd (prod_applist ar args)))
159
Some (hdapp,Array.to_list cargs)
164
let is_disjunction ?(strict=false) t =
165
op2bool (match_with_disjunction ~strict t)
167
(* An empty type is an inductive type, possible with indices, that has no
170
let match_with_empty_type t =
171
let (hdapp,args) = decompose_app t in
172
match (kind_of_term hdapp) with
174
let (mib,mip) = Global.lookup_inductive ind in
175
let nconstr = Array.length mip.mind_consnames in
176
if nconstr = 0 then Some hdapp else None
179
let is_empty_type t = op2bool (match_with_empty_type t)
181
(* This filters inductive types with one constructor with no arguments;
182
Parameters and indices are allowed *)
184
let match_with_unit_or_eq_type t =
185
let (hdapp,args) = decompose_app t in
186
match (kind_of_term hdapp) with
188
let (mib,mip) = Global.lookup_inductive ind in
189
let constr_types = mip.mind_nf_lc in
190
let nconstr = Array.length mip.mind_consnames in
191
let zero_args c = nb_prod c = mib.mind_nparams in
192
if nconstr = 1 && zero_args constr_types.(0) then
198
let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t)
200
(* A unit type is an inductive type with no indices but possibly
201
(useless) parameters, and that has no constructors *)
204
match match_with_conjunction t with
205
| Some (_,t) when List.length t = 0 -> true
208
(* Checks if a given term is an application of an
209
inductive binary relation R, so that R has only one constructor
210
establishing its reflexivity. *)
212
let coq_refl_rel1_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ]
213
let coq_refl_rel2_pattern = PATTERN [ forall x:_, _ x x ]
214
let coq_refl_reljm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ]
216
let match_with_equation t =
217
let (hdapp,args) = decompose_app t in
218
match (kind_of_term hdapp) with
220
let (mib,mip) = Global.lookup_inductive ind in
221
let constr_types = mip.mind_nf_lc in
222
let nconstr = Array.length mip.mind_consnames in
224
(is_matching coq_refl_rel1_pattern constr_types.(0) ||
225
is_matching coq_refl_rel2_pattern constr_types.(0) ||
226
is_matching coq_refl_reljm_pattern constr_types.(0))
233
let is_equation t = op2bool (match_with_equation t)
235
let match_with_equality_type t =
236
let (hdapp,args) = decompose_app t in
237
match (kind_of_term hdapp) with
238
| Ind ind when args <> [] ->
239
let (mib,mip) = Global.lookup_inductive ind in
240
let nconstr = Array.length mip.mind_consnames in
241
if nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0
248
let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
250
let match_arrow_pattern t =
251
match matches coq_arrow_pattern t with
252
| [(m1,arg);(m2,mind)] -> assert (m1=meta1 & m2=meta2); (arg, mind)
253
| _ -> anomaly "Incorrect pattern matching"
255
let match_with_nottype t =
257
let (arg,mind) = match_arrow_pattern t in
258
if is_empty_type mind then Some (mind,arg) else None
259
with PatternMatchingFailure -> None
261
let is_nottype t = op2bool (match_with_nottype t)
263
let match_with_forall_term c=
264
match kind_of_term c with
265
| Prod (nam,a,b) -> Some (nam,a,b)
268
let is_forall_term c = op2bool (match_with_forall_term c)
270
let match_with_imp_term c=
271
match kind_of_term c with
272
| Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b)
275
let is_imp_term c = op2bool (match_with_imp_term c)
277
let match_with_nodep_ind t =
278
let (hdapp,args) = decompose_app t in
279
match (kind_of_term hdapp) with
281
let (mib,mip) = Global.lookup_inductive ind in
282
if Array.length (mib.mind_packets)>1 then None else
283
let nodep_constr = has_nodep_prod_after mib.mind_nparams in
284
if array_for_all nodep_constr mip.mind_nf_lc then
286
if mip.mind_nrealargs=0 then args else
287
fst (list_chop mib.mind_nparams args) in
288
Some (hdapp,params,mip.mind_nrealargs)
293
let is_nodep_ind t=op2bool (match_with_nodep_ind t)
295
let match_with_sigma_type t=
296
let (hdapp,args) = decompose_app t in
297
match (kind_of_term hdapp) with
299
let (mib,mip) = Global.lookup_inductive ind in
300
if (Array.length (mib.mind_packets)=1) &&
301
(mip.mind_nrealargs=0) &&
302
(Array.length mip.mind_consnames=1) &&
303
has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then
304
(*allowing only 1 existential*)
310
let is_sigma_type t=op2bool (match_with_sigma_type t)
312
(***** Destructing patterns bound to some theory *)
314
let rec first_match matcher = function
315
| [] -> raise PatternMatchingFailure
316
| (pat,build_set)::l ->
317
try (build_set (),matcher pat)
318
with PatternMatchingFailure -> first_match matcher l
322
(* Patterns "(eq ?1 ?2 ?3)" and "(identity ?1 ?2 ?3)" *)
323
let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ]
324
let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
325
let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
327
let match_eq eqn eq_pat =
328
match matches (Lazy.force eq_pat) eqn with
329
| [(m1,t);(m2,x);(m3,y)] ->
330
assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
332
| _ -> anomaly "match_eq: an eq pattern should match 3 terms"
335
[coq_eq_pattern, build_coq_eq_data;
336
coq_identity_pattern, build_coq_identity_data]
338
let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *)
339
first_match (match_eq eqn) equalities
344
let match_eq_nf gls eqn eq_pat =
345
match pf_matches gls (Lazy.force eq_pat) eqn with
346
| [(m1,t);(m2,x);(m3,y)] ->
347
assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
348
(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
349
| _ -> anomaly "match_eq: an eq pattern should match 3 terms"
351
let dest_nf_eq gls eqn =
353
snd (first_match (match_eq_nf gls eqn) equalities)
354
with PatternMatchingFailure ->
355
error "Not an equality."
359
(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
360
let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
361
let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
363
let match_sigma ex ex_pat =
364
match matches (Lazy.force ex_pat) ex with
365
| [(m1,a);(m2,p);(m3,car);(m4,cdr)] ->
366
assert (m1=meta1 & m2=meta2 & m3=meta3 & m4=meta4);
369
anomaly "match_sigma: a successful sigma pattern should match 4 terms"
371
let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
372
first_match (match_sigma ex)
373
[coq_existT_pattern, build_sigma_type]
375
(* Pattern "(sig ?1 ?2)" *)
376
let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
379
match matches (Lazy.force coq_sig_pattern) t with
380
| [(_,a); (_,p)] -> (a,p)
381
| _ -> anomaly "Unexpected pattern"
383
let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t
385
(*** Decidable equalities *)
387
(* The expected form of the goal for the tactic Decide Equality *)
389
(* Pattern "{<?1>x=y}+{~(<?1>x=y)}" *)
390
(* i.e. "(sumbool (eq ?1 x y) ~(eq ?1 x y))" *)
392
let coq_eqdec_inf_pattern =
393
lazy PATTERN [ { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } ]
395
let coq_eqdec_inf_rev_pattern =
396
lazy PATTERN [ { ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 } ]
398
let coq_eqdec_pattern =
399
lazy PATTERN [ %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) ]
401
let coq_eqdec_rev_pattern =
402
lazy PATTERN [ %coq_or_ref (~ ?X2 = ?X3 :> ?X1) (?X2 = ?X3 :> ?X1) ]
404
let op_or = coq_or_ref
405
let op_sum = coq_sumbool_ref
408
let eqonleft,op,subst =
409
try true,op_sum,matches (Lazy.force coq_eqdec_inf_pattern) t
410
with PatternMatchingFailure ->
411
try false,op_sum,matches (Lazy.force coq_eqdec_inf_rev_pattern) t
412
with PatternMatchingFailure ->
413
try true,op_or,matches (Lazy.force coq_eqdec_pattern) t
414
with PatternMatchingFailure ->
415
false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in
417
| [(_,typ);(_,c1);(_,c2)] ->
418
eqonleft, Libnames.constr_of_global (Lazy.force op), c1, c2, typ
419
| _ -> anomaly "Unexpected pattern"
421
(* Patterns "~ ?" and "? -> False" *)
422
let coq_not_pattern = lazy PATTERN [ ~ _ ]
423
let coq_imp_False_pattern = lazy PATTERN [ _ -> %coq_False_ref ]
425
let is_matching_not t = is_matching (Lazy.force coq_not_pattern) t
426
let is_matching_imp_False t = is_matching (Lazy.force coq_imp_False_pattern) t
428
(* Remark: patterns that have references to the standard library must
429
be evaluated lazily (i.e. at the time they are used, not a the time
added
removed
tactics/hipattern.ml4
