Source file constr_matching.ml
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
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
open Pp
open CErrors
open Util
open Names
open Constr
open Context
open Termops
open EConstr
open Vars
open Pattern
open Patternops
open Context.Rel.Declaration
open Ltac_pretype
let error_instantiate_pattern id l =
let is = match l with
| [_] -> "is"
| _ -> "are"
in
user_err (str "Cannot substitute the term bound to " ++ Id.print id
++ strbrk " in pattern because the term refers to " ++ pr_enum Id.print l
++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
type instantiated_pattern = constr_pattern
let instantiate_pattern env sigma lvar c =
let open EConstr in
let open Vars in
let rec aux vars = function
| PVar id as x ->
(try
let ctx,c = Id.Map.find id lvar in
try
let inst =
List.map
(fun id -> mkRel (List.index Name.equal (Name id) vars))
ctx
in
let c = substl inst c in
pattern_of_constr env sigma c
with Not_found ->
let vars =
List.map_filter (function Name id -> Some id | _ -> None) vars in
error_instantiate_pattern id (List.subtract Id.equal ctx vars)
with Not_found ->
x)
| c ->
map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
if Id.Map.is_empty lvar then c else aux [] c
type binding_bound_vars = Id.Set.t
type bound_ident_map = Id.t Id.Map.t
exception PatternMatchingFailure
let warn_meta_collision =
CWarnings.create ~name:"meta-collision" ~category:"ltac"
(fun name ->
strbrk "Collision between bound variable " ++ Id.print name ++
strbrk " and a metavariable of same name.")
let constrain sigma n (ids, m) ((names,seen as names_seen), terms as subst) =
let open EConstr in
try
let (ids', m') = Id.Map.find n terms in
if List.equal Id.equal ids ids' && eq_constr sigma m m' then subst
else raise PatternMatchingFailure
with Not_found ->
let () = if Id.Map.mem n names then warn_meta_collision n in
(names_seen, Id.Map.add n (ids, m) terms)
let add_binders na1 na2 binding_vars ((names,seen), terms as subst) =
match na1, na2.binder_name with
| Name id1, Name id2 when Id.Set.mem id1 binding_vars ->
if Id.Map.mem id1 names then
let () = Glob_ops.warn_variable_collision id1 in
subst
else
let id2 = Namegen.next_ident_away id2 seen in
let names = Id.Map.add id1 id2 names in
let seen = Id.Set.add id2 seen in
let () = if Id.Map.mem id1 terms then
warn_meta_collision id1 in
((names,seen), terms)
| _ -> subst
let rec build_lambda sigma vars ctx m = match vars with
| [] ->
if Vars.closed0 sigma m then m else raise PatternMatchingFailure
| n :: vars ->
let pre, suf = List.chop (pred n) ctx in
let (na, t, suf) = match suf with
| [] -> assert false
| (_, id, t) :: suf ->
(map_annot Name.mk_name id, t, suf)
in
let is_nondep t clear = match clear with
| [] -> true
| _ ->
let rels = free_rels sigma t in
let check i b = b || not (Int.Set.mem i rels) in
List.for_all_i check 1 clear
in
let fold (_, _, t) clear = is_nondep t clear :: clear in
let clear = List.fold_right fold pre [false] in
let clear = List.drop_last clear in
let () = if not (is_nondep m clear) then raise PatternMatchingFailure in
let fold (k, accu) keep =
if keep then
let k = succ k in
(k, Some k :: accu)
else (k, None :: accu)
in
let keep, shift = List.fold_left fold (0, []) clear in
let shift = List.rev shift in
let map = function
| None -> mkProp
| Some i -> mkRel (i + 1)
in
let subst =
List.map map shift @
mkRel 1 ::
List.mapi (fun i _ -> mkRel (i + keep + 2)) suf
in
let map i (na, id, c) =
let i = succ i in
let subst = List.skipn i subst in
let subst = List.map (fun c -> Vars.lift (- i) c) subst in
(na, id, substl subst c)
in
let pre = List.mapi map pre in
let pre = List.filter_with clear pre in
let m = substl subst m in
let map i =
if i > n then i - n + keep
else match List.nth shift (i - 1) with
| None ->
raise PatternMatchingFailure
| Some k -> k
in
let vars = List.map map vars in
let m = mkLambda (na, Vars.lift keep t, m) in
build_lambda sigma vars (pre @ suf) m
let rec k accu frels ctx = match ctx with
| [] -> accu
| (na, _, _) :: ctx ->
if Int.Set.mem k frels then
begin match na with
| Name id ->
let () = if Id.Set.mem id accu then raise PatternMatchingFailure in
extract_bound_aux (k + 1) (Id.Set.add id accu) frels ctx
| Anonymous -> raise PatternMatchingFailure
end
else extract_bound_aux (k + 1) accu frels ctx
let frels ctx =
extract_bound_aux 1 Id.Set.empty frels ctx
let dummy_constr = EConstr.mkProp
let make_renaming ids = function
| (Name id, _, _) ->
begin
try EConstr.mkRel (List.index Id.equal id ids)
with Not_found -> dummy_constr
end
| _ -> dummy_constr
let push_binder na1 na2 t ctx =
let id2 = map_annot (function
| Name id2 -> id2
| Anonymous ->
let avoid = Id.Set.of_list (List.map (fun (_,id,_) -> id.binder_name) ctx) in
Namegen.next_ident_away Namegen.default_non_dependent_ident avoid) na2
in
(na1, id2, t) :: ctx
let rec match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env' subst t1 t2 b1 b2 =
match t1, EConstr.kind sigma t2, b1, EConstr.kind sigma b2 with
| PProd(na1,c1,t1'), Prod(na2,c2,t2'), PLambda (_,c1',b1'), Lambda (na2',c2',b2') ->
let ctx = push_binder na1 na2 c2 ctx in
let ctx' = push_binder na1 na2' c2' ctx' in
let env = EConstr.push_rel (LocalAssum (na2,c2)) env in
let subst = sorec ctx env subst c1 c2 in
let subst = sorec ctx env subst c1' c2' in
let subst = add_binders na1 na2 binding_vars subst in
match_under_common_fix_binders sorec sigma binding_vars
ctx ctx' env env' subst t1' t2' b1' b2'
| PLetIn(na1,c1,u1,t1), LetIn(na2,c2,u2,t2), PLetIn(_,c1',u1',b1), LetIn(na2',c2',u2',b2) ->
let ctx = push_binder na1 na2 u2 ctx in
let ctx' = push_binder na1 na2' u2' ctx' in
let env = EConstr.push_rel (LocalDef (na2,c2,t2)) env in
let subst = sorec ctx env subst c1 c2 in
let subst = sorec ctx env subst c1' c2' in
let subst = Option.fold_left (fun subst u1 -> sorec ctx env subst u1 u2) subst u1 in
let subst = Option.fold_left (fun subst u1' -> sorec ctx env subst u1' u2') subst u1' in
let subst = add_binders na1 na2 binding_vars subst in
match_under_common_fix_binders sorec sigma binding_vars
ctx ctx' env env' subst t1 t2 b1 b2
| _ ->
sorec ctx' env' (sorec ctx env subst t1 t2) b1 b2
let merge_binding sigma allow_bound_rels ctx n cT subst =
let c = match ctx with
| [] ->
([], cT)
| _ ->
let frels = free_rels sigma cT in
if allow_bound_rels then
let vars = extract_bound_vars frels ctx in
let ordered_vars = Id.Set.elements vars in
let rename binding = make_renaming ordered_vars binding in
let renaming = List.map rename ctx in
(ordered_vars, Vars.substl renaming cT)
else
let depth = List.length ctx in
let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in
if depth < min_elt then
([], Vars.lift (- depth) cT)
else raise PatternMatchingFailure
in
constrain sigma n c subst
let matches_core env sigma allow_bound_rels
(binding_vars,pat) c =
let open EConstr in
let convref ref c =
let open GlobRef in
match ref, EConstr.kind sigma c with
| VarRef id, Var id' -> Names.Id.equal id id'
| ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c'
| IndRef i, Ind (i', _) -> Names.Ind.CanOrd.equal i i'
| ConstructRef c, Construct (c',u) -> Names.Construct.CanOrd.equal c c'
| _, _ -> false
in
let rec sorec ctx env subst p t =
let cT = strip_outer_cast sigma t in
match p, EConstr.kind sigma cT with
| PSoApp (n,args),m ->
let fold (ans, seen) = function
| PRel n ->
let () = if Int.Set.mem n seen then user_err (str "Non linear second-order pattern") in
(n :: ans, Int.Set.add n seen)
| _ -> user_err (str "Only bound indices allowed in second order pattern matching.")
in
let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in
let frels = free_rels sigma cT in
if Int.Set.subset frels relset then
constrain sigma n ([], build_lambda sigma relargs ctx cT) subst
else
raise PatternMatchingFailure
| PMeta (Some n), m -> merge_binding sigma allow_bound_rels ctx n cT subst
| PMeta None, m -> subst
| PRef (GlobRef.VarRef v1), Var v2 when Id.equal v1 v2 -> subst
| PVar v1, Var v2 when Id.equal v1 v2 -> subst
| PRef ref, _ when convref ref cT -> subst
| PRel n1, Rel n2 when Int.equal n1 n2 -> subst
| PSort ps, Sort s ->
if Sorts.family_equal ps (Sorts.family (ESorts.kind sigma s))
then subst else raise PatternMatchingFailure
| PApp (p, [||]), _ -> sorec ctx env subst p t
| PApp (PApp (h, a1), a2), _ ->
sorec ctx env subst (PApp(h,Array.append a1 a2)) t
| PApp (PMeta meta,args1), App (c2,args2) ->
(let diff = Array.length args2 - Array.length args1 in
if diff >= 0 then
let args21, args22 = Array.chop diff args2 in
let c = mkApp(c2,args21) in
let subst =
match meta with
| None -> subst
| Some n -> merge_binding sigma allow_bound_rels ctx n c subst in
Array.fold_left2 (sorec ctx env) subst args1 args22
else
match EConstr.kind sigma c2 with
| Proj (pr, c) ->
(try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
| _ -> raise PatternMatchingFailure)
| PApp (c1,arg1), App (c2,arg2) ->
(match c1, EConstr.kind sigma c2 with
| PRef (GlobRef.ConstRef r), Proj (pr,c)
when not (Environ.QConstant.equal env r (Projection.constant pr)) ->
raise PatternMatchingFailure
| PProj (pr1,c1), Proj (pr,c) ->
if Environ.QProjection.equal env pr1 pr then
try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2
with Invalid_argument _ -> raise PatternMatchingFailure
else raise PatternMatchingFailure
| _, Proj (pr,c) ->
(try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
| _, _ ->
try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2
with Invalid_argument _ -> raise PatternMatchingFailure)
| PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2)
when not (Environ.QConstant.equal env c1 (Projection.constant pr)) ->
raise PatternMatchingFailure
| PApp (c, args), Proj (pr, c2) ->
(try let term = Retyping.expand_projection env sigma pr c2 [] in
sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
| PProj (p1,c1), Proj (p2,c2) when Environ.QProjection.equal env p1 p2 ->
sorec ctx env subst c1 c2
| PProd (na1,c1,d1), Prod(na2,c2,d2) ->
sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) ->
sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2
| PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) ->
sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PIf (a1,b1,b1'), Case (ci, u2, pms2, p2, iv, a2, ([|b2;b2'|] as br2)) ->
let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci, u2, pms2, p2, iv, a2, br2) in
let ctx_b2,b2 = br2.(0) in
let ctx_b2',b2' = br2.(1) in
let n = Context.Rel.length ctx_b2 in
let n' = Context.Rel.length ctx_b2' in
if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then
let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = push_binder Anonymous na t l in
let ctx_br = List.fold_left f ctx ctx_b2 in
let ctx_br' = List.fold_left f ctx ctx_b2' in
let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
sorec ctx_br' (push_rel_context ctx_b2' env)
(sorec ctx_br (push_rel_context ctx_b2 env)
(sorec ctx env subst a1 a2) b1 b2) b1' b2'
else
raise PatternMatchingFailure
| PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) ->
let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
let n2 = Array.length br2 in
let () = match ci1.cip_ind with
| None -> ()
| Some ind1 ->
if not (Ind.CanOrd.equal ind1 ci2.ci_ind) then raise PatternMatchingFailure
in
let () =
if not ci1.cip_extensible && not (Int.equal (List.length br1) n2)
then raise PatternMatchingFailure
in
let sorec_under_ctx subst (n, c1) (decls, c2) =
let env = push_rel_context decls env in
let rec fold (ctx, subst) nas decls = match nas, decls with
| [], _ ->
(ctx, subst)
| na1 :: nas, d :: decls ->
let na2 = Context.Rel.Declaration.get_annot d in
let t = Context.Rel.Declaration.get_type d in
let ctx = push_binder na1 na2 t ctx in
let subst = add_binders na1 na2 binding_vars subst in
fold (ctx, subst) nas decls
| _, [] ->
assert false
in
let ctx, subst = fold (ctx, subst) (Array.to_list n) (List.rev decls) in
sorec ctx env subst c1 c2
in
let chk_branch subst (j,n,c) =
assert (j < n2);
sorec_under_ctx subst (n, c) br2.(j)
in
let subst = sorec ctx env subst a1 a2 in
let subst = match p1 with
| None -> subst
| Some p1 -> sorec_under_ctx subst p1 p2
in
List.fold_left chk_branch subst br1
| PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2))
when Array.equal Int.equal ln1 ln2 && i1 = i2 ->
let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
| PCoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(lna2,tl2,bl2))
when i1 = i2 ->
let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
| PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
List.fold_left2 (sorec ctx env) subst args1 args2
| PInt i1, Int i2 when Uint63.equal i1 i2 -> subst
| PFloat f1, Float f2 when Float64.equal f1 f2 -> subst
| PArray(pt,pdef,pty), Array(_u,t,def,ty)
when Array.length pt = Array.length t ->
sorec ctx env (sorec ctx env (Array.fold_left2 (sorec ctx env) subst pt t) pdef def) pty ty
| (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
| PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _
| PFix _ | PCoFix _| PEvar _ | PInt _ | PFloat _ | PArray _), _ -> raise PatternMatchingFailure
in
sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c
let matches_core_closed env sigma pat c =
let names, subst = matches_core env sigma false pat c in
(fst names, Id.Map.map snd subst)
let extended_matches env sigma pat c =
let (names,_), subst = matches_core env sigma true pat c in
names, subst
let matches env sigma pat c =
snd (matches_core_closed env sigma (Id.Set.empty,pat) c)
type context = constr Lazy.t
let special_meta = (-1)
let empty_context = Lazy.from_val (mkMeta special_meta)
let repr_context c = Lazy.force c
let instantiate_context ctxt c =
let ctxt = EConstr.Unsafe.to_constr (Lazy.force ctxt) in
let c = EConstr.Unsafe.to_constr c in
EConstr.of_constr (subst_meta [special_meta, c] ctxt)
type matching_result =
{ m_sub : bound_ident_map * patvar_map;
m_ctx : context; }
let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )
let isPMeta = function PMeta _ -> true | _ -> false
let matches_head env sigma pat c =
let open EConstr in
let head =
match pat, EConstr.kind sigma c with
| PApp (c1,arg1), App (c2,arg2) ->
if isPMeta c1 then c else
let n1 = Array.length arg1 in
if n1 < Array.length arg2 then mkApp (c2,Array.sub arg2 0 n1) else c
| c1, App (c2,arg2) when not (isPMeta c1) -> c2
| _ -> c in
matches env sigma pat head
let authorized_occ env sigma closed pat c mk_ctx =
try
let subst = matches_core_closed env sigma pat c in
if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
then (fun next -> next ())
else (fun next -> mkresult subst (lazy (mk_ctx (mkMeta special_meta))) next)
with PatternMatchingFailure -> (fun next -> next ())
let subargs env v = Array.map_to_list (fun c -> (env, c)) v
let sub_match ?(closed=true) env sigma pat c =
let open EConstr in
let rec aux env c mk_ctx next =
let here = authorized_occ env sigma closed pat c mk_ctx in
let next () = match EConstr.kind sigma c with
| Cast (c1,k,c2) ->
let next_mk_ctx = function
| [c1] -> mk_ctx (mkCast (c1, k, c2))
| _ -> assert false
in
try_aux [env, c1] next_mk_ctx next
| Lambda (x,c1,c2) ->
let next_mk_ctx = function
| [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
| _ -> assert false
in
let env' = EConstr.push_rel (LocalAssum (x,c1)) env in
try_aux [(env, c1); (env', c2)] next_mk_ctx next
| Prod (x,c1,c2) ->
let next_mk_ctx = function
| [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
| _ -> assert false
in
let env' = EConstr.push_rel (LocalAssum (x,c1)) env in
try_aux [(env, c1); (env', c2)] next_mk_ctx next
| LetIn (x,c1,t,c2) ->
let next_mk_ctx = function
| [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
| _ -> assert false
in
let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in
try_aux [(env, c1); (env', c2)] next_mk_ctx next
| App (c1,lc) ->
let lc1 = Array.sub lc 0 (Array.length lc - 1) in
let app = mkApp (c1,lc1) in
let mk_ctx = function
| [app';c] -> mk_ctx (mkApp (app',[|c|]))
| _ -> assert false in
try_aux [(env, app); (env, Array.last lc)] mk_ctx next
| Case (ci,u,pms,hd0,iv,c1,lc0) ->
let (mib, mip) = Inductive.lookup_mind_specif env ci.ci_ind in
let (_, hd, _, _, br) = expand_case env sigma (ci, u, pms, hd0, iv, c1, lc0) in
let hd =
let (ctx, hd) = decompose_lam_assum sigma hd in
(push_rel_context ctx env, hd)
in
let map i br =
let decls = mip.Declarations.mind_consnrealdecls.(i) in
let (ctx, c) = decompose_lam_n_decls sigma decls br in
(push_rel_context ctx env, c)
in
let lc = Array.to_list (Array.mapi map br) in
let next_mk_ctx = function
| c1 :: rem ->
let pms, rem = List.chop (Array.length pms) rem in
let pms = Array.of_list pms in
let hd, lc = match rem with [] -> assert false | x :: l -> (x, l) in
let hd = (fst hd0, hd) in
let map_br (nas, _) br = (nas, br) in
mk_ctx (mkCase (ci,u,pms,hd,iv,c1,Array.map2 map_br lc0 (Array.of_list lc)))
| _ -> assert false
in
let sub = (env, c1) :: Array.fold_right (fun c accu -> (env, c) :: accu) pms (hd :: lc) in
try_aux sub next_mk_ctx next
| Fix (indx,(names,types,bodies as recdefs)) ->
let nb_fix = Array.length types in
let next_mk_ctx le =
let (ntypes,nbodies) = CList.chop nb_fix le in
mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
let env' = push_rec_types recdefs env in
let sub = subargs env types @ subargs env' bodies in
try_aux sub next_mk_ctx next
| CoFix (i,(names,types,bodies as recdefs)) ->
let nb_fix = Array.length types in
let next_mk_ctx le =
let (ntypes,nbodies) = CList.chop nb_fix le in
mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
let env' = push_rec_types recdefs env in
let sub = subargs env types @ subargs env' bodies in
try_aux sub next_mk_ctx next
| Proj (p,c') ->
begin match Retyping.expand_projection env sigma p c' [] with
| term -> aux env term mk_ctx next
| exception Retyping.RetypeError _ -> next ()
end
| Array(u, t, def, ty) ->
let next_mk_ctx = function
| def :: ty :: l -> mk_ctx (mkArray(u, Array.of_list l, def, ty))
| _ -> assert false
in
let sub = (env,def) :: (env,ty) :: subargs env t in
try_aux sub next_mk_ctx next
| Construct _|Ind _|Evar _|Const _|Rel _|Meta _|Var _|Sort _|Int _|Float _ ->
next ()
in
here next
and try_aux lc mk_ctx next =
let rec try_sub_match_rec lacc lc =
match lc with
| [] -> next ()
| (env, c) :: tl ->
let mk_ctx ce = mk_ctx (List.rev_append lacc (ce :: List.map snd tl)) in
let next () = try_sub_match_rec (c :: lacc) tl in
aux env c mk_ctx next
in
try_sub_match_rec [] lc in
let lempty () = IStream.Nil in
let result () = aux env c (fun x -> x) lempty in
IStream.thunk result
let match_subterm env sigma pat c = sub_match env sigma pat c
let is_matching env sigma pat c =
try let _ = matches env sigma pat c in true
with PatternMatchingFailure -> false
let is_matching_head env sigma pat c =
try let _ = matches_head env sigma pat c in true
with PatternMatchingFailure -> false
let is_matching_appsubterm ?(closed=true) env sigma pat c =
let pat = (Id.Set.empty,pat) in
let results = sub_match ~closed env sigma pat c in
not (IStream.is_empty results)