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
(* $Id: termops.ml 12058 2009-04-08 10:54:59Z herbelin $ *)
21
(* Sorts and sort family *)
23
let print_sort = function
24
| Prop Pos -> (str "Set")
25
| Prop Null -> (str "Prop")
26
| Type u -> (str "Type(" ++ Univ.pr_uni u ++ str ")")
28
let pr_sort_family = function
29
| InSet -> (str "Set")
30
| InProp -> (str "Prop")
31
| InType -> (str "Type")
33
let pr_name = function
35
| Anonymous -> str "_"
37
let pr_sp sp = str(string_of_kn sp)
38
let pr_con sp = str(string_of_con sp)
40
let rec pr_constr c = match kind_of_term c with
41
| Rel n -> str "#"++int n
42
| Meta n -> str "Meta(" ++ int n ++ str ")"
44
| Sort s -> print_sort s
45
| Cast (c,_, t) -> hov 1
46
(str"(" ++ pr_constr c ++ cut() ++
47
str":" ++ pr_constr t ++ str")")
48
| Prod (Name(id),t,c) -> hov 1
49
(str"forall " ++ pr_id id ++ str":" ++ pr_constr t ++ str"," ++
51
| Prod (Anonymous,t,c) -> hov 0
52
(str"(" ++ pr_constr t ++ str " ->" ++ spc() ++
53
pr_constr c ++ str")")
54
| Lambda (na,t,c) -> hov 1
55
(str"fun " ++ pr_name na ++ str":" ++
56
pr_constr t ++ str" =>" ++ spc() ++ pr_constr c)
57
| LetIn (na,b,t,c) -> hov 0
58
(str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++
59
str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++
62
(str"(" ++ pr_constr c ++ spc() ++
63
prlist_with_sep spc pr_constr (Array.to_list l) ++ str")")
65
(str"Evar#" ++ int e ++ str"{" ++
66
prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
67
| Const c -> str"Cst(" ++ pr_con c ++ str")"
68
| Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")"
69
| Construct ((sp,i),j) ->
70
str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
71
| Case (ci,p,c,bl) -> v 0
72
(hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
73
pr_constr c ++ str"of") ++ cut() ++
74
prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++
76
| Fix ((t,i),(lna,tl,bl)) ->
77
let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
79
(str"fix " ++ int i ++ spc() ++ str"{" ++
80
v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
81
pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
82
cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
84
| CoFix(i,(lna,tl,bl)) ->
85
let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
87
(str"cofix " ++ int i ++ spc() ++ str"{" ++
88
v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
89
pr_name na ++ str":" ++ pr_constr ty ++
90
cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
93
let term_printer = ref (fun _ -> pr_constr)
94
let print_constr_env t = !term_printer t
95
let print_constr t = !term_printer (Global.env()) t
96
let set_print_constr f = term_printer := f
98
let pr_var_decl env (id,c,typ) =
99
let pbody = match c with
102
(* Force evaluation *)
103
let pb = print_constr_env env c in
104
(str" := " ++ pb ++ cut () ) in
105
let pt = print_constr_env env typ in
106
let ptyp = (str" : " ++ pt) in
107
(pr_id id ++ hov 0 (pbody ++ ptyp))
109
let pr_rel_decl env (na,c,typ) =
110
let pbody = match c with
113
(* Force evaluation *)
114
let pb = print_constr_env env c in
115
(str":=" ++ spc () ++ pb ++ spc ()) in
116
let ptyp = print_constr_env env typ in
118
| Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
119
| Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
121
let print_named_context env =
122
hv 0 (fold_named_context
124
pps ++ ws 2 ++ pr_var_decl env d)
127
let print_rel_context env =
128
hv 0 (fold_rel_context
129
(fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d)
136
let pidt = pr_var_decl env d in
137
(pps ++ fnl () ++ pidt))
143
let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
148
(*let current_module = ref empty_dirpath
150
let set_module m = current_module := m*)
153
let univ_gen = ref 0 in
156
Univ.make_univ (Lib.library_dp(),!univ_gen))
157
let new_Type () = mkType (new_univ ())
158
let new_Type_sort () = Type (new_univ ())
160
(* This refreshes universes in types; works only for inferred types (i.e. for
161
types of the form (x1:A1)...(xn:An)B with B a sort or an atom in
163
let refresh_universes_gen strict t =
164
let modified = ref false in
165
let rec refresh t = match kind_of_term t with
166
| Sort (Type u) when strict or u <> Univ.type0m_univ ->
167
modified := true; new_Type ()
168
| Prod (na,u,v) -> mkProd (na,u,refresh v)
170
let t' = refresh t in
171
if !modified then t' else t
173
let refresh_universes = refresh_universes_gen false
174
let refresh_universes_strict = refresh_universes_gen true
176
let new_sort_in_family = function
177
| InProp -> prop_sort
179
| InType -> Type (new_univ ())
183
(* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
184
let prod_it ~init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
186
(* lam_it b [xn:Tn;..;x1:T1] = [x1:T1]..[xn:Tn]b *)
187
let lam_it ~init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
189
(* [Rel (n+m);...;Rel(n+1)] *)
190
let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
194
if p>m then l else reln (mkRel(n+p)::l) (p+1)
198
(* Same as [rel_list] but takes a context as argument and skips let-ins *)
199
let extended_rel_list n hyps =
200
let rec reln l p = function
201
| (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
202
| (_,Some _,_) :: hyps -> reln l (p+1) hyps
207
let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
211
let push_rel_assum (x,t) env = push_rel (x,None,t) env
213
let push_rels_assum assums =
214
push_rel_context (List.map (fun (x,t) -> (x,None,t)) assums)
216
let push_named_rec_types (lna,typarray,_) env =
221
| Name id -> (id, None, lift i t)
222
| Anonymous -> anomaly "Fix declarations must be named")
225
(fun e assum -> push_named assum e) env ctxt
227
let rec lookup_rel_id id sign =
228
let rec lookrec = function
229
| (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
230
| (n, (Name id',_,t)::l) -> if id' = id then (n,t) else lookrec (n+1,l)
231
| (_, []) -> raise Not_found
235
(* Constructs either [(x:t)c] or [[x=b:t]c] *)
236
let mkProd_or_LetIn (na,body,t) c =
238
| None -> mkProd (na, t, c)
239
| Some b -> mkLetIn (na, b, t, c)
241
(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
242
let mkProd_wo_LetIn (na,body,t) c =
244
| None -> mkProd (na, t, c)
245
| Some b -> subst1 b c
247
let it_mkProd_wo_LetIn ~init =
248
List.fold_left (fun c d -> mkProd_wo_LetIn d c) init
250
let it_mkProd_or_LetIn ~init =
251
List.fold_left (fun c d -> mkProd_or_LetIn d c) init
253
let it_mkLambda_or_LetIn ~init =
254
List.fold_left (fun c d -> mkLambda_or_LetIn d c) init
256
let it_named_context_quantifier f ~init =
257
List.fold_left (fun c d -> f d c) init
259
let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
260
let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
262
let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_LetIn
266
(* strips head casts and flattens head applications *)
267
let rec strip_head_cast c = match kind_of_term c with
269
let rec collapse_rec f cl2 = match kind_of_term f with
270
| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
271
| Cast (c,_,_) -> collapse_rec c cl2
272
| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
275
| Cast (c,_,_) -> strip_head_cast c
278
(* Get the last arg of an application *)
279
let last_arg c = match kind_of_term c with
280
| App (f,cl) -> array_last cl
281
| _ -> anomaly "last_arg"
283
(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
284
subterms of [c]; it carries an extra data [l] (typically a name
285
list) which is processed by [g na] (which typically cons [na] to
286
[l]) at each binder traversal (with name [na]); it is not recursive
287
and the order with which subterms are processed is not specified *)
289
let map_constr_with_named_binders g f l c = match kind_of_term c with
290
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
292
| Cast (c,k,t) -> mkCast (f l c, k, f l t)
293
| Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c)
294
| Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
295
| LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
296
| App (c,al) -> mkApp (f l c, Array.map (f l) al)
297
| Evar (e,al) -> mkEvar (e, Array.map (f l) al)
298
| Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
299
| Fix (ln,(lna,tl,bl)) ->
300
let l' = Array.fold_left (fun l na -> g na l) l lna in
301
mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
302
| CoFix(ln,(lna,tl,bl)) ->
303
let l' = Array.fold_left (fun l na -> g na l) l lna in
304
mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
306
(* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the
307
immediate subterms of [c]; it carries an extra data [n] (typically
308
a lift index) which is processed by [g] (which typically add 1 to
309
[n]) at each binder traversal; the subterms are processed from left
310
to right according to the usual representation of the constructions
311
(this may matter if [f] does a side-effect); it is not recursive;
312
in fact, the usual representation of the constructions is at the
313
time being almost those of the ML representation (except for
316
let fold_rec_types g (lna,typarray,_) e =
317
let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
318
Array.fold_left (fun e assum -> g assum e) e ctxt
321
let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
322
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
324
| Cast (c,k,t) -> let c' = f l c in mkCast (c',k,f l t)
327
mkProd (na, t', f (g (na,None,t) l) c)
330
mkLambda (na, t', f (g (na,None,t) l) c)
331
| LetIn (na,b,t,c) ->
334
let c' = f (g (na,Some b,t) l) c in
335
mkLetIn (na, b', t', c')
336
| App (c,[||]) -> assert false
338
(*Special treatment to be able to recognize partially applied subterms*)
339
let a = al.(Array.length al - 1) in
340
let hd = f l (mkApp (c, Array.sub al 0 (Array.length al - 1))) in
341
mkApp (hd, [| f l a |])
342
| Evar (e,al) -> mkEvar (e, array_map_left (f l) al)
343
| Case (ci,p,c,bl) ->
344
(* In v8 concrete syntax, predicate is after the term to match! *)
347
mkCase (ci, p', c', array_map_left (f l) bl)
348
| Fix (ln,(lna,tl,bl as fx)) ->
349
let l' = fold_rec_types g fx l in
350
let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in
351
mkFix (ln,(lna,tl',bl'))
352
| CoFix(ln,(lna,tl,bl as fx)) ->
353
let l' = fold_rec_types g fx l in
354
let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in
355
mkCoFix (ln,(lna,tl',bl'))
358
let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
359
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
360
| Construct _) -> cstr
364
if c==c' && t==t' then cstr else mkCast (c', k, t')
367
let c' = f (g (na,None,t) l) c in
368
if t==t' && c==c' then cstr else mkProd (na, t', c')
371
let c' = f (g (na,None,t) l) c in
372
if t==t' && c==c' then cstr else mkLambda (na, t', c')
373
| LetIn (na,b,t,c) ->
376
let c' = f (g (na,Some b,t) l) c in
377
if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
380
let al' = Array.map (f l) al in
381
if c==c' && array_for_all2 (==) al al' then cstr else mkApp (c', al')
383
let al' = Array.map (f l) al in
384
if array_for_all2 (==) al al' then cstr else mkEvar (e, al')
385
| Case (ci,p,c,bl) ->
388
let bl' = Array.map (f l) bl in
389
if p==p' && c==c' && array_for_all2 (==) bl bl' then cstr else
390
mkCase (ci, p', c', bl')
391
| Fix (ln,(lna,tl,bl)) ->
392
let tl' = Array.map (f l) tl in
394
array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
395
let bl' = Array.map (f l') bl in
396
if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
398
else mkFix (ln,(lna,tl',bl'))
399
| CoFix(ln,(lna,tl,bl)) ->
400
let tl' = Array.map (f l) tl in
402
array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
403
let bl' = Array.map (f l') bl in
404
if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
406
else mkCoFix (ln,(lna,tl',bl'))
408
(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
409
subterms of [c] starting from [acc] and proceeding from left to
410
right according to the usual representation of the constructions as
411
[fold_constr] but it carries an extra data [n] (typically a lift
412
index) which is processed by [g] (which typically add 1 to [n]) at
413
each binder traversal; it is not recursive *)
415
let fold_constr_with_binders g f n acc c = match kind_of_term c with
416
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
417
| Construct _) -> acc
418
| Cast (c,_, t) -> f n (f n acc c) t
419
| Prod (_,t,c) -> f (g n) (f n acc t) c
420
| Lambda (_,t,c) -> f (g n) (f n acc t) c
421
| LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
422
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
423
| Evar (_,l) -> Array.fold_left (f n) acc l
424
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
425
| Fix (_,(lna,tl,bl)) ->
426
let n' = iterate g (Array.length tl) n in
427
let fd = array_map2 (fun t b -> (t,b)) tl bl in
428
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
429
| CoFix (_,(lna,tl,bl)) ->
430
let n' = iterate g (Array.length tl) n in
431
let fd = array_map2 (fun t b -> (t,b)) tl bl in
432
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
434
(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
435
subterms of [c]; it carries an extra data [acc] which is processed by [g] at
436
each binder traversal; it is not recursive and the order with which
437
subterms are processed is not specified *)
439
let iter_constr_with_full_binders g f l c = match kind_of_term c with
440
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
442
| Cast (c,_, t) -> f l c; f l t
443
| Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
444
| Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
445
| LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
446
| App (c,args) -> f l c; Array.iter (f l) args
447
| Evar (_,args) -> Array.iter (f l) args
448
| Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
449
| Fix (_,(lna,tl,bl)) ->
450
let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
453
| CoFix (_,(lna,tl,bl)) ->
454
let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
458
(***************************)
459
(* occurs check functions *)
460
(***************************)
465
let rec occrec c = match kind_of_term c with
466
| Meta _ -> raise Occur
467
| _ -> iter_constr occrec c
468
in try occrec c; false with Occur -> true
470
let occur_existential c =
471
let rec occrec c = match kind_of_term c with
472
| Evar _ -> raise Occur
473
| _ -> iter_constr occrec c
474
in try occrec c; false with Occur -> true
476
let occur_meta_or_existential c =
477
let rec occrec c = match kind_of_term c with
478
| Evar _ -> raise Occur
479
| Meta _ -> raise Occur
480
| _ -> iter_constr occrec c
481
in try occrec c; false with Occur -> true
483
let occur_const s c =
484
let rec occur_rec c = match kind_of_term c with
485
| Const sp when sp=s -> raise Occur
486
| _ -> iter_constr occur_rec c
488
try occur_rec c; false with Occur -> true
491
let rec occur_rec c = match kind_of_term c with
492
| Evar (sp,_) when sp=n -> raise Occur
493
| _ -> iter_constr occur_rec c
495
try occur_rec c; false with Occur -> true
497
let occur_in_global env id constr =
498
let vars = vars_of_global env constr in
499
if List.mem id vars then raise Occur
501
let occur_var env s c =
502
let rec occur_rec c =
503
occur_in_global env s c;
504
iter_constr occur_rec c
506
try occur_rec c; false with Occur -> true
508
let occur_var_in_decl env hyp (_,c,typ) =
510
| None -> occur_var env hyp typ
512
occur_var env hyp typ ||
513
occur_var env hyp body
515
(* Tests that t is a subterm of c *)
517
let eq_constr_fail c = if eq_constr t c then raise Occur
518
in let rec occur_rec c = eq_constr_fail c; iter_constr occur_rec c
519
in try occur_rec c; false with Occur -> true
521
(* returns the list of free debruijn indices in a term *)
524
let rec frec depth acc c = match kind_of_term c with
525
| Rel n -> if n >= depth then Intset.add (n-depth+1) acc else acc
526
| _ -> fold_constr_with_binders succ frec depth acc c
528
frec 1 Intset.empty m
530
(* collects all metavar occurences, in left-to-right order, preserving
531
* repetitions and all. *)
533
let collect_metas c =
534
let rec collrec acc c =
535
match kind_of_term c with
536
| Meta mv -> list_add_set mv acc
537
| _ -> fold_constr collrec acc c
539
List.rev (collrec [] c)
541
(* (dependent M N) is true iff M is eq_term with a subterm of N
542
M is appropriately lifted through abstractions of N *)
546
if eq_constr m t then
549
match kind_of_term m, kind_of_term t with
550
| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
551
deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
552
Array.iter (deprec m)
554
(Array.length lm) ((Array.length lt) - (Array.length lm)))
555
| _ -> iter_constr_with_binders (lift 1) deprec m t
557
try deprec m t; false with Occur -> true
559
let pop t = lift (-1) t
561
(***************************)
562
(* bindings functions *)
563
(***************************)
565
type metamap = (metavariable * constr) list
567
let rec subst_meta bl c =
568
match kind_of_term c with
569
| Meta i -> (try List.assoc i bl with Not_found -> c)
570
| _ -> map_constr (subst_meta bl) c
572
(* First utilities for avoiding telescope computation for subst_term *)
574
let prefix_application eq_fun (k,c) (t : constr) =
575
let c' = collapse_appl c and t' = collapse_appl t in
576
match kind_of_term c', kind_of_term t' with
577
| App (f1,cl1), App (f2,cl2) ->
578
let l1 = Array.length cl1
579
and l2 = Array.length cl2 in
581
&& eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
582
Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
587
let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
588
let c' = collapse_appl c and t' = collapse_appl t in
589
match kind_of_term c', kind_of_term t' with
590
| App (f1,cl1), App (f2,cl2) ->
591
let l1 = Array.length cl1
592
and l2 = Array.length cl2 in
594
&& eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
595
Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1)))
600
(* Recognizing occurrences of a given (closed) subterm in a term for Pattern :
601
[subst_term c t] substitutes [(Rel 1)] for all occurrences of (closed)
602
term [c] in a term [t] *)
603
(*i Bizarre : si on cherche un sous terme clos, pourquoi le lifter ? i*)
605
let subst_term_gen eq_fun c t =
606
let rec substrec (k,c as kc) t =
607
match prefix_application eq_fun kc t with
610
if eq_fun c t then mkRel k
612
map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
616
(* Recognizing occurrences of a given (closed) subterm in a term :
617
[replace_term c1 c2 t] substitutes [c2] for all occurrences of (closed)
618
term [c1] in a term [t] *)
619
(*i Meme remarque : a priori [c] n'est pas forcement clos i*)
621
let replace_term_gen eq_fun c by_c in_t =
622
let rec substrec (k,c as kc) t =
623
match my_prefix_application eq_fun kc by_c t with
626
(if eq_fun c t then (lift k by_c) else
627
map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c))
632
let subst_term = subst_term_gen eq_constr
634
let replace_term = replace_term_gen eq_constr
636
(* Substitute only at a list of locations or excluding a list of
637
locations; in the occurrences list (b,l), b=true means no
638
occurrence except the ones in l and b=false, means all occurrences
639
except the ones in l *)
641
type occurrences = bool * int list
642
let all_occurrences = (false,[])
643
let no_occurrences_in_set = (true,[])
645
let error_invalid_occurrence l =
646
let l = list_uniquize (List.sort Pervasives.compare l) in
648
(str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++
649
prlist_with_sep spc int l ++ str ".")
651
let subst_term_occ_gen (nowhere_except_in,locs) occ c t =
652
let maxocc = List.fold_right max locs 0 in
654
assert (List.for_all (fun x -> x >= 0) locs);
655
let rec substrec (k,c as kc) t =
656
if nowhere_except_in & !pos > maxocc then t
658
if eq_constr c t then
660
if nowhere_except_in then
661
if List.mem !pos locs then (mkRel k) else t
663
if List.mem !pos locs then t else (mkRel k)
666
map_constr_with_binders_left_to_right
667
(fun d (k,c) -> (k+1,lift 1 c))
670
let t' = substrec (1,c) t in
673
let subst_term_occ (nowhere_except_in,locs as plocs) c t =
674
if locs = [] then if nowhere_except_in then t else subst_term c t
676
let (nbocc,t') = subst_term_occ_gen plocs 1 c t in
677
let rest = List.filter (fun o -> o >= nbocc) locs in
678
if rest <> [] then error_invalid_occurrence rest;
681
type hyp_location_flag = (* To distinguish body and type of local defs *)
686
let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,typ as d) =
687
match bodyopt,hloc with
688
| None, InHypValueOnly -> errorlabstrm "" (pr_id id ++ str " has no value")
689
| None, _ -> (id,None,subst_term_occ plocs c typ)
690
| Some body, InHypTypeOnly -> (id,Some body,subst_term_occ plocs c typ)
691
| Some body, InHypValueOnly -> (id,Some (subst_term_occ plocs c body),typ)
692
| Some body, InHyp ->
694
if nowhere_except_in then d
695
else (id,Some (subst_term c body),subst_term c typ)
697
let (nbocc,body') = subst_term_occ_gen plocs 1 c body in
698
let (nbocc',t') = subst_term_occ_gen plocs nbocc c typ in
699
let rest = List.filter (fun o -> o >= nbocc') locs in
700
if rest <> [] then error_invalid_occurrence rest;
703
(* First character of a constr *)
705
let lowercase_first_char id =
706
lowercase_first_char_utf8 (string_of_id id)
708
let vars_of_env env =
710
Sign.fold_named_context (fun (id,_,_) s -> Idset.add id s)
711
(named_context env) ~init:Idset.empty in
712
Sign.fold_rel_context
713
(fun (na,_,_) s -> match na with Name id -> Idset.add id s | _ -> s)
714
(rel_context env) ~init:s
716
let add_vname vars = function
717
Name id -> Idset.add id vars
720
let id_of_global = Nametab.id_of_global
722
let sort_hdchar = function
728
match kind_of_term c with
729
| Prod (_,_,c) -> hdrec (k+1) c
730
| Lambda (_,_,c) -> hdrec (k+1) c
731
| LetIn (_,_,_,c) -> hdrec (k+1) c
732
| Cast (c,_,_) -> hdrec k c
733
| App (f,l) -> hdrec k f
735
lowercase_first_char (id_of_label (con_label kn))
736
| Ind ((kn,i) as x) ->
738
lowercase_first_char (id_of_label (label kn))
740
lowercase_first_char (id_of_global (IndRef x))
741
| Construct ((sp,i) as x) ->
742
lowercase_first_char (id_of_global (ConstructRef x))
743
| Var id -> lowercase_first_char id
744
| Sort s -> sort_hdchar s
746
(if n<=k then "p" (* the initial term is flexible product/function *)
748
try match Environ.lookup_rel (n-k) env with
749
| (Name id,_,_) -> lowercase_first_char id
750
| (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
751
with Not_found -> "y")
752
| Fix ((_,i),(lna,_,_)) ->
753
let id = match lna.(i) with Name id -> id | _ -> assert false in
754
lowercase_first_char id
755
| CoFix (i,(lna,_,_)) ->
756
let id = match lna.(i) with Name id -> id | _ -> assert false in
757
lowercase_first_char id
758
| Meta _|Evar _|Case (_, _, _, _) -> "y"
762
let id_of_name_using_hdchar env a = function
763
| Anonymous -> id_of_string (hdchar env a)
766
let named_hd env a = function
767
| Anonymous -> Name (id_of_string (hdchar env a))
770
let mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b)
771
let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
773
let lambda_name = mkLambda_name
774
let prod_name = mkProd_name
776
let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b)
777
let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b)
779
let name_assumption env (na,c,t) =
781
| None -> (named_hd env t na, None, t)
782
| Some body -> (named_hd env body na, c, t)
784
let name_context env hyps =
788
let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
789
(env,[]) (List.rev hyps))
791
let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
792
let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
794
let it_mkProd_or_LetIn_name env b hyps =
795
it_mkProd_or_LetIn b (name_context env hyps)
796
let it_mkLambda_or_LetIn_name env b hyps =
797
it_mkLambda_or_LetIn b (name_context env hyps)
799
(*************************)
800
(* Names environments *)
801
(*************************)
802
type names_context = name list
803
let add_name n nl = n::nl
804
let lookup_name_of_rel p names =
805
try List.nth names (p-1)
806
with Invalid_argument _ | Failure _ -> raise Not_found
807
let rec lookup_rel_of_name id names =
808
let rec lookrec n = function
809
| Anonymous :: l -> lookrec (n+1) l
810
| (Name id') :: l -> if id' = id then n else lookrec (n+1) l
811
| [] -> raise Not_found
814
let empty_names_context = []
816
let ids_of_rel_context sign =
817
Sign.fold_rel_context
818
(fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
821
let ids_of_named_context sign =
822
Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
824
let ids_of_context env =
825
(ids_of_rel_context (rel_context env))
826
@ (ids_of_named_context (named_context env))
829
let names_of_rel_context env =
830
List.map (fun (na,_,_) -> na) (rel_context env)
832
(**** Globality of identifiers *)
834
let rec is_imported_modpath = function
838
let is_imported_ref = function
841
| ConstructRef ((kn,_),_) ->
842
let (mp,_,_) = repr_kn kn in is_imported_modpath mp
844
let (mp,_,_) = repr_con kn in is_imported_modpath mp
848
let ref = locate (make_short_qualid id) in
849
not (is_imported_ref ref)
853
let is_constructor id =
855
match locate (make_short_qualid id) with
856
| ConstructRef _ as ref -> not (is_imported_ref ref)
861
let is_section_variable id =
862
try let _ = Global.lookup_named id in true
863
with Not_found -> false
865
let next_global_ident_from allow_secvar id avoid =
866
let rec next_rec id =
867
let id = next_ident_away_from id avoid in
868
if (allow_secvar && is_section_variable id) || not (is_global id) then
871
next_rec (lift_ident id)
875
let next_global_ident_away allow_secvar id avoid =
876
let id = next_ident_away id avoid in
877
if (allow_secvar && is_section_variable id) || not (is_global id) then
880
next_global_ident_from allow_secvar (lift_ident id) avoid
883
match kind_of_term c with
884
| Const _ | Ind _ | Construct _ | Var _ -> true
887
let has_polymorphic_type c =
888
match (Global.lookup_constant c).Declarations.const_type with
889
| Declarations.PolymorphicArity _ -> true
892
(* nouvelle version de renommage des variables (DEC 98) *)
893
(* This is the algorithm to display distinct bound variables
895
- R�gle 1 : un nom non anonyme, m�me non affich�, contribue � la liste
897
- R�gle 2 : c'est la d�pendance qui d�cide si on affiche ou pas
900
si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors
901
il est affich� (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
902
mais f et f0 contribue � la liste des variables � �viter (en supposant
903
que les noms f et f0 ne sont pas d�j� pris)
904
Int�r�t : noms homog�nes dans un but avant et apr�s Intro
907
type used_idents = identifier list
909
let occur_rel p env id =
910
try lookup_name_of_rel p env = Name id
911
with Not_found -> false (* Unbound indice : may happen in debug *)
913
let occur_id nenv id0 c =
914
let rec occur n c = match kind_of_term c with
915
| Var id when id=id0 -> raise Occur
916
| Const kn when id_of_global (ConstRef kn) = id0 -> raise Occur
918
when id_of_global (IndRef ind_sp) = id0 ->
921
when id_of_global (ConstructRef cstr_sp) = id0 ->
923
| Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur
924
| _ -> iter_constr_with_binders succ occur n c
928
| Not_found -> false (* Case when a global is not in the env *)
930
type avoid_flags = bool option
932
let next_name_not_occuring avoid_flags name l env_names t =
934
if List.mem id l or occur_id env_names id t or
935
(* Further restrictions ? *)
936
match avoid_flags with None -> false | Some not_only_cstr ->
937
(if not_only_cstr then
938
(* To be consistent with the intro mechanism *)
939
is_global id & not (is_section_variable id)
941
(* To avoid constructors in pattern-matchings *)
943
then next (lift_ident id)
949
(* Normally, an anonymous name is not dependent and will not be *)
950
(* taken into account by the function concrete_name; just in case *)
951
(* invent a valid name *)
952
next (id_of_string "H")
954
let base_sort_cmp pb s0 s1 =
956
| (Prop c1, Prop c2) -> c1 = Null or c2 = Pos (* Prop <= Set *)
957
| (Prop c1, Type u) -> pb = Reduction.CUMUL
958
| (Type u1, Type u2) -> true
961
(* eq_constr extended with universe erasure *)
962
let rec constr_cmp cv_pb t1 t2 =
963
(match kind_of_term t1, kind_of_term t2 with
964
Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
966
|| compare_constr (constr_cmp cv_pb) t1 t2
968
let eq_constr = constr_cmp Reduction.CONV
970
(* On reduit une serie d'eta-redex de tete ou rien du tout *)
971
(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
972
(* Remplace 2 versions pr�c�dentes bugg�es *)
974
let rec eta_reduce_head c =
975
match kind_of_term c with
976
| Lambda (_,c1,c') ->
977
(match kind_of_term (eta_reduce_head c') with
979
let lastn = (Array.length cl) - 1 in
980
if lastn < 1 then anomaly "application without arguments"
982
(match kind_of_term cl.(lastn) with
986
else mkApp (f, Array.sub cl 0 lastn)
996
(* alpha-eta conversion : ignore print names and casts *)
999
let t1 = eta_reduce_head (strip_head_cast t1)
1000
and t2 = eta_reduce_head (strip_head_cast t2) in
1001
t1=t2 or compare_constr aux t1 t2
1005
(* iterator on rel context *)
1006
let process_rel_context f env =
1007
let sign = named_context_val env in
1008
let rels = rel_context env in
1009
let env0 = reset_with_named_context sign env in
1010
Sign.fold_rel_context f rels ~init:env0
1012
let assums_of_rel_context sign =
1013
Sign.fold_rel_context
1017
| None -> (na, t)::l)
1020
let fold_map_rel_context f env sign =
1021
let rec aux env acc = function
1023
aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
1027
aux env [] (List.rev sign)
1029
let map_rel_context_with_binders f sign =
1030
let rec aux k = function
1031
| d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
1034
aux (rel_context_length sign) sign
1036
let substl_rel_context l =
1037
map_rel_context_with_binders (fun k -> substnl l (k-1))
1039
let lift_rel_context n =
1040
map_rel_context_with_binders (liftn n)
1042
let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init
1044
let rec mem_named_context id = function
1045
| (id',_,_) :: _ when id=id' -> true
1046
| _ :: sign -> mem_named_context id sign
1049
let make_all_name_different env =
1050
let avoid = ref (ids_of_named_context (named_context env)) in
1052
(fun (na,c,t) newenv ->
1053
let id = next_name_away na !avoid in
1054
avoid := id::!avoid;
1055
push_rel (Name id,c,t) newenv)
1058
let global_vars env ids = Idset.elements (global_vars_set env ids)
1060
let global_vars_set_of_decl env = function
1061
| (_,None,t) -> global_vars_set env t
1063
Idset.union (global_vars_set env t)
1064
(global_vars_set env c)
1066
let dependency_closure env sign hyps =
1067
if Idset.is_empty hyps then [] else
1069
Sign.fold_named_context_reverse
1070
(fun (hs,hl) (x,_,_ as d) ->
1071
if Idset.mem x hs then
1072
(Idset.union (global_vars_set_of_decl env d) (Idset.remove x hs),
1079
let default_x = id_of_string "x"
1081
let rec next_name_away_in_cases_pattern id avoid =
1082
let id = match id with Name id -> id | Anonymous -> default_x in
1084
if List.mem id avoid or is_constructor id then next (lift_ident id)
1088
(* Remark: Anonymous var may be dependent in Evar's contexts *)
1089
let concrete_name avoid_flags l env_names n c =
1090
if n = Anonymous & noccurn 1 c then
1093
let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
1094
let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
1095
(idopt, fresh_id::l)
1097
let concrete_let_name avoid_flags l env_names n c =
1098
let fresh_id = next_name_not_occuring avoid_flags n l env_names c in
1099
(Name fresh_id, fresh_id::l)
1101
let rec rename_bound_var env avoid c =
1102
let env_names = names_of_rel_context env in
1103
let rec rename avoid c =
1104
match kind_of_term c with
1105
| Prod (na,c1,c2) ->
1106
let na',avoid' = concrete_name None avoid env_names na c2 in
1107
mkProd (na', c1, rename avoid' c2)
1108
| LetIn (na,c1,t,c2) ->
1109
let na',avoid' = concrete_let_name None avoid env_names na c2 in
1110
mkLetIn (na',c1,t, rename avoid' c2)
1111
| Cast (c,k,t) -> mkCast (rename avoid c, k,t)
1116
(* Combinators on judgments *)
1118
let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
1119
let on_judgment_value f j = { j with uj_val = f j.uj_val }
1120
let on_judgment_type f j = { j with uj_type = f j.uj_type }
1122
(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
1124
let context_chop k ctx =
1125
let rec chop_aux acc = function
1126
| (0, l2) -> (List.rev acc, l2)
1127
| (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
1128
| (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
1129
| (_, []) -> anomaly "context_chop"
1130
in chop_aux [] (k,ctx)
added
removed
pretyping/termops.ml
