/
evarutil.ml
2040 lines (1823 loc) · 77.5 KB
/
evarutil.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
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Errors
open Util
open Pp
open Names
open Term
open Termops
open Namegen
open Pre_env
open Environ
open Evd
open Reductionops
open Pretype_errors
open Retyping
(****************************************************)
(* Expanding/testing/exposing existential variables *)
(****************************************************)
(* flush_and_check_evars fails if an existential is undefined *)
exception Uninstantiated_evar of existential_key
let rec flush_and_check_evars sigma c =
match kind_of_term c with
| Evar (evk,_ as ev) ->
(match existential_opt_value sigma ev with
| None -> raise (Uninstantiated_evar evk)
| Some c -> flush_and_check_evars sigma c)
| _ -> map_constr (flush_and_check_evars sigma) c
let nf_evar = Pretype_errors.nf_evar
let j_nf_evar = Pretype_errors.j_nf_evar
let jl_nf_evar = Pretype_errors.jl_nf_evar
let jv_nf_evar = Pretype_errors.jv_nf_evar
let tj_nf_evar = Pretype_errors.tj_nf_evar
let nf_named_context_evar sigma ctx =
Sign.map_named_context (Reductionops.nf_evar sigma) ctx
let nf_rel_context_evar sigma ctx =
Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
let nf_env_evar sigma env =
let nc' = nf_named_context_evar sigma (Environ.named_context env) in
let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
let nf_evar_info evc info =
{ info with
evar_concl = Reductionops.nf_evar evc info.evar_concl;
evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
evar_body = match info.evar_body with
| Evar_empty -> Evar_empty
| Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) }
let nf_evars evm =
Evd.fold
(fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
evm Evd.empty
let nf_evars_undefined evm =
Evd.fold_undefined
(fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
evm (defined_evars evm)
let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd
(*-------------------*)
(* Auxiliary functions for the conversion algorithms modulo evars
*)
let has_undefined_evars_or_sorts evd t =
let rec has_ev t =
match kind_of_term t with
| Evar (ev,args) ->
(match evar_body (Evd.find evd ev) with
| Evar_defined c ->
has_ev c; Array.iter has_ev args
| Evar_empty ->
raise NotInstantiatedEvar)
| Sort s when is_sort_variable evd s -> raise Not_found
| _ -> iter_constr has_ev t in
try let _ = has_ev t in false
with (Not_found | NotInstantiatedEvar) -> true
let is_ground_term evd t =
not (has_undefined_evars_or_sorts evd t)
let is_ground_env evd env =
let is_ground_decl = function
(_,Some b,_) -> is_ground_term evd b
| _ -> true in
List.for_all is_ground_decl (rel_context env) &&
List.for_all is_ground_decl (named_context env)
(* Memoization is safe since evar_map and environ are applicative
structures *)
let memo f =
let m = ref None in
fun x y -> match !m with
| Some (x', y', r) when x == x' && y == y' -> r
| _ -> let r = f x y in m := Some (x, y, r); r
let is_ground_env = memo is_ground_env
(* Return the head evar if any *)
exception NoHeadEvar
let head_evar =
let rec hrec c = match kind_of_term c with
| Evar (evk,_) -> evk
| Case (_,_,c,_) -> hrec c
| App (c,_) -> hrec c
| Cast (c,_,_) -> hrec c
| _ -> raise NoHeadEvar
in
hrec
(* Expand head evar if any (currently consider only applications but I
guess it should consider Case too) *)
let whd_head_evar_stack sigma c =
let rec whrec (c, l as s) =
match kind_of_term c with
| Evar (evk,args as ev) when Evd.is_defined sigma evk
-> whrec (existential_value sigma ev, l)
| Cast (c,_,_) -> whrec (c, l)
| App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
| _ -> s
in
whrec (c, [])
let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
let noccur_evar evd evk c =
let rec occur_rec c = match kind_of_term c with
| Evar (evk',_ as ev') ->
(match safe_evar_value evd ev' with
| Some c -> occur_rec c
| None -> if evk = evk' then raise Occur)
| _ -> iter_constr occur_rec c
in
try occur_rec c; true with Occur -> false
let normalize_evar evd ev =
match kind_of_term (whd_evar evd (mkEvar ev)) with
| Evar (evk,args) -> (evk,args)
| _ -> assert false
(**********************)
(* Creating new metas *)
(**********************)
(* Generator of metavariables *)
let new_meta =
let meta_ctr = ref 0 in
Summary.declare_summary "meta counter"
{ Summary.freeze_function = (fun () -> !meta_ctr);
Summary.unfreeze_function = (fun n -> meta_ctr := n);
Summary.init_function = (fun () -> meta_ctr := 0) };
fun () -> incr meta_ctr; !meta_ctr
let mk_new_meta () = mkMeta(new_meta())
let collect_evars emap c =
let rec collrec acc c =
match kind_of_term c with
| Evar (evk,_) ->
if Evd.is_undefined emap evk then evk::acc
else (* No recursion on the evar instantiation *) acc
| _ ->
fold_constr collrec acc c in
List.uniquize (collrec [] c)
let push_dependent_evars sigma emap =
Evd.fold_undefined (fun ev {evar_concl = ccl} (sigma',emap') ->
List.fold_left
(fun (sigma',emap') ev ->
(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
(sigma',emap') (collect_evars emap' ccl))
emap (sigma,emap)
let push_duplicated_evars sigma emap c =
let rec collrec (one,(sigma,emap) as acc) c =
match kind_of_term c with
| Evar (evk,_) when not (Evd.mem sigma evk) ->
if List.mem evk one then
let sigma' = Evd.add sigma evk (Evd.find emap evk) in
let emap' = Evd.remove emap evk in
(one,(sigma',emap'))
else
(evk::one,(sigma,emap))
| _ ->
fold_constr collrec acc c
in
snd (collrec ([],(sigma,emap)) c)
(* replaces a mapping of existentials into a mapping of metas.
Problem if an evar appears in the type of another one (pops anomaly) *)
let evars_to_metas sigma (emap, c) =
let emap = nf_evar_map_undefined emap in
let sigma',emap' = push_dependent_evars sigma emap in
let sigma',emap' = push_duplicated_evars sigma' emap' c in
(* if an evar has been instantiated in [emap] (as part of typing [c])
then it is instantiated in [sigma]. *)
let repair_evars sigma emap =
fold_undefined begin fun ev _ sigma' ->
try
let info = find emap ev in
match evar_body info with
| Evar_empty -> sigma'
| Evar_defined body -> define ev body sigma'
with Not_found -> sigma'
end sigma sigma
in
let sigma' = repair_evars sigma' emap in
let change_exist evar =
let ty = nf_betaiota emap (existential_type emap evar) in
let n = new_meta() in
mkCast (mkMeta n, DEFAULTcast, ty) in
let rec replace c =
match kind_of_term c with
| Evar (evk,_ as ev) when Evd.mem emap' evk -> change_exist ev
| _ -> map_constr replace c in
(sigma', replace c)
(* The list of non-instantiated existential declarations (order is important) *)
let non_instantiated sigma =
let listev = Evd.undefined_list sigma in
List.map (fun (ev,evi) -> (ev,nf_evar_info sigma evi)) listev
(************************)
(* Manipulating filters *)
(************************)
let apply_subfilter filter subfilter =
fst (List.fold_right (fun oldb (l,filter) ->
if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
filter ([], List.rev subfilter))
let extract_subfilter initial_filter refined_filter =
snd (List.filter2 (fun b1 b2 -> b1) (initial_filter,refined_filter))
(**********************)
(* Creating new evars *)
(**********************)
(* Generator of existential names *)
let new_untyped_evar =
let evar_ctr = ref 0 in
Summary.declare_summary "evar counter"
{ Summary.freeze_function = (fun () -> !evar_ctr);
Summary.unfreeze_function = (fun n -> evar_ctr := n);
Summary.init_function = (fun () -> evar_ctr := 0) };
fun () -> incr evar_ctr; existential_of_int !evar_ctr
(*------------------------------------*
* functional operations on evar sets *
*------------------------------------*)
(* [push_rel_context_to_named_context] builds the defining context and the
* initial instance of an evar. If the evar is to be used in context
*
* Gamma = a1 ... an xp ... x1
* \- named part -/ \- de Bruijn part -/
*
* then the x1...xp are turned into variables so that the evar is declared in
* context
*
* a1 ... an xp ... x1
* \----------- named part ------------/
*
* but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)"
* so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed
* in context Gamma.
*
* Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first)
* Remark 2: If some of the ai or xj are definitions, we keep them in the
* instance. This is necessary so that no unfolding of local definitions
* happens when inferring implicit arguments (consider e.g. the problem
* "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which
* produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want
* the hole to be instantiated by x', not by x (which would have been
* the case in [invert_definition] if x' had disappeared from the instance).
* Note that at any time, if, in some context env, the instance of
* declaration x:A is t and the instance of definition x':=phi(x) is u, then
* we have the property that u and phi(t) are convertible in env.
*)
let push_rel_context_to_named_context env typ =
(* compute the instances relative to the named context and rel_context *)
let ids = List.map pi1 (named_context env) in
let inst_vars = List.map mkVar ids in
let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
(* move the rel context to a named context and extend the named instance *)
(* with vars of the rel context *)
(* We do keep the instances corresponding to local definition (see above) *)
let (subst, _, env) =
Sign.fold_rel_context
(fun (na,c,t) (subst, avoid, env) ->
let id = next_name_away na avoid in
let d = (id,Option.map (substl subst) c,substl subst t) in
(mkVar id :: subst, id::avoid, push_named d env))
(rel_context env) ~init:([], ids, env) in
(named_context_val env, substl subst typ, inst_rels@inst_vars, subst)
(*------------------------------------*
* Entry points to define new evars *
*------------------------------------*)
let default_source = (Loc.ghost,Evar_kinds.InternalHole)
let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
let newevk = new_untyped_evar() in
let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in
(evd,newevk)
let new_evar_instance sign evd typ ?src ?filter ?candidates instance =
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates typ in
(evd,mkEvar (newevk,Array.of_list instance))
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
let new_evar evd env ?src ?filter ?candidates typ =
let sign,typ',instance,subst = push_rel_context_to_named_context env typ in
let candidates = Option.map (List.map (substl subst)) candidates in
let instance =
match filter with
| None -> instance
| Some filter -> List.filter_with filter instance in
new_evar_instance sign evd typ' ?src ?filter ?candidates instance
let new_type_evar ?src ?filter evd env =
let evd', s = new_sort_variable evd in
new_evar evd' env ?src ?filter (mkSort s)
(* The same using side-effect *)
let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates ty =
let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
evdref := evd';
ev
(*------------------------------------*
* Restricting existing evars *
*------------------------------------*)
let restrict_evar_key evd evk filter candidates =
if filter = None && candidates = None then
evd,evk
else
let evi = Evd.find_undefined evd evk in
let oldfilter = evar_filter evi in
if filter = Some oldfilter && candidates = None then
evd,evk
else
let filter =
match filter with
| None -> evar_filter evi
| Some filter -> filter in
let candidates =
match candidates with None -> evi.evar_candidates | _ -> candidates in
let ccl = evi.evar_concl in
let sign = evar_hyps evi in
let src = evi.evar_source in
let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
let ctxt = snd (List.filter2 (fun b c -> b) (filter,evar_context evi)) in
let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
(* Restrict an applied evar and returns its restriction in the same context *)
let restrict_applied_evar evd (evk,argsv) filter candidates =
let evd,newevk = restrict_evar_key evd evk filter candidates in
let newargsv = match filter with
| None -> (* optim *) argsv
| Some filter ->
let evi = Evd.find evd evk in
let subfilter = extract_subfilter (evar_filter evi) filter in
Array.filter_with subfilter argsv in
evd,(newevk,newargsv)
(* Restrict an evar in the current evar_map *)
let restrict_evar evd evk filter candidates =
fst (restrict_evar_key evd evk filter candidates)
(* Restrict an evar in the current evar_map *)
let restrict_instance evd evk filter argsv =
match filter with None -> argsv | Some filter ->
let evi = Evd.find evd evk in
Array.filter_with (extract_subfilter (evar_filter evi) filter) argsv
(* This assumes an evar with identity instance and generalizes it over only
the De Bruijn part of the context *)
let generalize_evar_over_rels sigma (ev,args) =
let evi = Evd.find sigma ev in
let sign = named_context_of_val evi.evar_hyps in
List.fold_left2
(fun (c,inst as x) a d ->
if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
(evi.evar_concl,[]) (Array.to_list args) sign
(***************************************)
(* Managing chains of local definitons *)
(***************************************)
(* Expand rels and vars that are bound to other rels or vars so that
dependencies in variables are canonically associated to the most ancient
variable in its family of aliased variables *)
let compute_var_aliases sign =
List.fold_right (fun (id,b,c) aliases ->
match b with
| Some t ->
(match kind_of_term t with
| Var id' ->
let aliases_of_id =
try Idmap.find id' aliases with Not_found -> [] in
Idmap.add id (aliases_of_id@[t]) aliases
| _ ->
Idmap.add id [t] aliases)
| None -> aliases)
sign Idmap.empty
let compute_rel_aliases var_aliases rels =
snd (List.fold_right (fun (_,b,t) (n,aliases) ->
(n-1,
match b with
| Some t ->
(match kind_of_term t with
| Var id' ->
let aliases_of_n =
try Idmap.find id' var_aliases with Not_found -> [] in
Intmap.add n (aliases_of_n@[t]) aliases
| Rel p ->
let aliases_of_n =
try Intmap.find (p+n) aliases with Not_found -> [] in
Intmap.add n (aliases_of_n@[mkRel (p+n)]) aliases
| _ ->
Intmap.add n [lift n t] aliases)
| None -> aliases))
rels (List.length rels,Intmap.empty))
let make_alias_map env =
(* We compute the chain of aliases for each var and rel *)
let var_aliases = compute_var_aliases (named_context env) in
let rel_aliases = compute_rel_aliases var_aliases (rel_context env) in
(var_aliases,rel_aliases)
let lift_aliases n (var_aliases,rel_aliases as aliases) =
if n = 0 then aliases else
(var_aliases,
Intmap.fold (fun p l -> Intmap.add (p+n) (List.map (lift n) l))
rel_aliases Intmap.empty)
let get_alias_chain_of aliases x = match kind_of_term x with
| Rel n -> (try Intmap.find n (snd aliases) with Not_found -> [])
| Var id -> (try Idmap.find id (fst aliases) with Not_found -> [])
| _ -> []
let normalize_alias_opt aliases x =
match get_alias_chain_of aliases x with
| [] -> None
| a::_ when isRel a or isVar a -> Some a
| [_] -> None
| _::a::_ -> Some a
let normalize_alias aliases x =
match normalize_alias_opt aliases x with
| Some a -> a
| None -> x
let normalize_alias_var var_aliases id =
destVar (normalize_alias (var_aliases,Intmap.empty) (mkVar id))
let extend_alias (_,b,_) (var_aliases,rel_aliases) =
let rel_aliases =
Intmap.fold (fun n l -> Intmap.add (n+1) (List.map (lift 1) l))
rel_aliases Intmap.empty in
let rel_aliases =
match b with
| Some t ->
(match kind_of_term t with
| Var id' ->
let aliases_of_binder =
try Idmap.find id' var_aliases with Not_found -> [] in
Intmap.add 1 (aliases_of_binder@[t]) rel_aliases
| Rel p ->
let aliases_of_binder =
try Intmap.find (p+1) rel_aliases with Not_found -> [] in
Intmap.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
| _ ->
Intmap.add 1 [lift 1 t] rel_aliases)
| None -> rel_aliases in
(var_aliases, rel_aliases)
let expand_alias_once aliases x =
match get_alias_chain_of aliases x with
| [] -> None
| l -> Some (List.last l)
let expansions_of_var aliases x =
match get_alias_chain_of aliases x with
| [] -> [x]
| a::_ as l when isRel a || isVar a -> x :: List.rev l
| _::l -> x :: List.rev l
let expansion_of_var aliases x =
match get_alias_chain_of aliases x with
| [] -> x
| a::_ -> a
let rec expand_vars_in_term_using aliases t = match kind_of_term t with
| Rel _ | Var _ ->
normalize_alias aliases t
| _ ->
map_constr_with_full_binders
extend_alias expand_vars_in_term_using aliases t
let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
let free_vars_and_rels_up_alias_expansion aliases c =
let acc1 = ref Intset.empty and acc2 = ref Idset.empty in
let cache_rel = ref Intset.empty and cache_var = ref Idset.empty in
let is_in_cache depth = function
| Rel n -> Intset.mem (n-depth) !cache_rel
| Var s -> Idset.mem s !cache_var
| _ -> false in
let put_in_cache depth = function
| Rel n -> cache_rel := Intset.add (n-depth) !cache_rel
| Var s -> cache_var := Idset.add s !cache_var
| _ -> () in
let rec frec (aliases,depth) c =
match kind_of_term c with
| Rel _ | Var _ as ck ->
if is_in_cache depth ck then () else begin
put_in_cache depth ck;
let c = expansion_of_var aliases c in
match kind_of_term c with
| Var id -> acc2 := Idset.add id !acc2
| Rel n -> if n >= depth+1 then acc1 := Intset.add (n-depth) !acc1
| _ -> frec (aliases,depth) c end
| Const _ | Ind _ | Construct _ ->
acc2 := List.fold_right Idset.add (vars_of_global (Global.env()) c) !acc2
| _ ->
iter_constr_with_full_binders
(fun d (aliases,depth) -> (extend_alias d aliases,depth+1))
frec (aliases,depth) c
in
frec (aliases,0) c;
(!acc1,!acc2)
(************************************)
(* Removing a dependency in an evar *)
(************************************)
type clear_dependency_error =
| OccurHypInSimpleClause of identifier option
| EvarTypingBreak of existential
exception ClearDependencyError of identifier * clear_dependency_error
open Store.Field
let cleared = Store.field ()
let rec check_and_clear_in_constr evdref err ids c =
(* returns a new constr where all the evars have been 'cleaned'
(ie the hypotheses ids have been removed from the contexts of
evars) *)
let check id' =
if List.mem id' ids then
raise (ClearDependencyError (id',err))
in
match kind_of_term c with
| Var id' ->
check id'; c
| ( Const _ | Ind _ | Construct _ ) ->
let vars = Environ.vars_of_global (Global.env()) c in
List.iter check vars; c
| Evar (evk,l as ev) ->
if Evd.is_defined !evdref evk then
(* If evk is already defined we replace it by its definition *)
let nc = whd_evar !evdref c in
(check_and_clear_in_constr evdref err ids nc)
else
(* We check for dependencies to elements of ids in the
evar_info corresponding to e and in the instance of
arguments. Concurrently, we build a new evar
corresponding to e where hypotheses of ids have been
removed *)
let evi = Evd.find_undefined !evdref evk in
let ctxt = Evd.evar_filtered_context evi in
let (nhyps,nargs,rids) =
List.fold_right2
(fun (rid,ob,c as h) a (hy,ar,ri) ->
(* Check if some id to clear occurs in the instance
a of rid in ev and remember the dependency *)
match
List.filter (fun id -> List.mem id ids) (Idset.elements (collect_vars a))
with
| id :: _ -> (hy,ar,(rid,id)::ri)
| _ ->
(* Check if some rid to clear in the context of ev
has dependencies in another hyp of the context of ev
and transitively remember the dependency *)
match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
| (_,id') :: _ -> (hy,ar,(rid,id')::ri)
| _ ->
(* No dependency at all, we can keep this ev's context hyp *)
(h::hy,a::ar,ri))
ctxt (Array.to_list l) ([],[],[]) in
(* Check if some rid to clear in the context of ev has dependencies
in the type of ev and adjust the source of the dependency *)
let nconcl =
try check_and_clear_in_constr evdref (EvarTypingBreak ev)
(List.map fst rids) (evar_concl evi)
with ClearDependencyError (rid,err) ->
raise (ClearDependencyError (List.assoc rid rids,err)) in
if rids = [] then c else begin
let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
evdref := Evd.define evk ev' !evdref;
let (evk',_) = destEvar ev' in
(* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
let evi = Evd.find !evdref evk in
let extra = evi.evar_extra in
let extra' = cleared.set true extra in
let evi' = { evi with evar_extra = extra' } in
evdref := Evd.add !evdref evk evi' ;
(* spiwack: /hacking session *)
mkEvar(evk', Array.of_list nargs)
end
| _ -> map_constr (check_and_clear_in_constr evdref err ids) c
let clear_hyps_in_evi evdref hyps concl ids =
(* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
hypothesis does not depend on a element of ids, and erases ids in
the contexts of the evars occuring in evi *)
let nconcl =
check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
let nhyps =
let check_context (id,ob,c) =
let err = OccurHypInSimpleClause (Some id) in
(id, Option.map (check_and_clear_in_constr evdref err ids) ob,
check_and_clear_in_constr evdref err ids c)
in
let check_value vk =
match !vk with
| VKnone -> vk
| VKvalue (v,d) ->
if (List.for_all (fun e -> not (Idset.mem e d)) ids) then
(* v does depend on any of ids, it's ok *)
vk
else
(* v depends on one of the cleared hyps: we forget the computed value *)
ref VKnone
in
remove_hyps ids check_context check_value hyps
in
(nhyps,nconcl)
(********************************)
(* Managing pattern-unification *)
(********************************)
let rec expand_and_check_vars aliases = function
| [] -> []
| a::l when isRel a or isVar a ->
let a = expansion_of_var aliases a in
if isRel a or isVar a then a :: expand_and_check_vars aliases l
else raise Exit
| _ ->
raise Exit
module Constrhash = Hashtbl.Make
(struct type t = constr
let equal = eq_constr
let hash = hash_constr
end)
let constr_list_distinct l =
let visited = Constrhash.create 23 in
let rec loop = function
| h::t ->
if Constrhash.mem visited h then false
else (Constrhash.add visited h h; loop t)
| [] -> true
in loop l
let get_actual_deps aliases l t =
if occur_meta_or_existential t then
(* Probably no restrictions on allowed vars in presence of evars *)
l
else
(* Probably strong restrictions coming from t being evar-closed *)
let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
List.filter (fun c ->
match kind_of_term c with
| Var id -> Idset.mem id fv_ids
| Rel n -> Intset.mem n fv_rels
| _ -> assert false) l
let remove_instance_local_defs evd evk args =
let evi = Evd.find evd evk in
let rec aux = function
| (_,Some _,_)::sign, a::args -> aux (sign,args)
| (_,None,_)::sign, a::args -> a::aux (sign,args)
| [], [] -> []
| _ -> assert false in
aux (evar_filtered_context evi, args)
(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
let find_unification_pattern_args env l t =
if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
let aliases = make_alias_map env in
match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
| Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x
| _ -> None
else
None
let is_unification_pattern_meta env nb m l t =
(* Variables from context and rels > nb are implicitly all there *)
(* so we need to be a rel <= nb *)
if List.for_all (fun x -> isRel x && destRel x <= nb) l then
match find_unification_pattern_args env l t with
| Some _ as x when not (dependent (mkMeta m) t) -> x
| _ -> None
else
None
let is_unification_pattern_evar env evd (evk,args) l t =
if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar evd evk t then
let args = remove_instance_local_defs evd evk (Array.to_list args) in
let n = List.length args in
match find_unification_pattern_args env (args @ l) t with
| Some l -> Some (List.skipn n l)
| _ -> None
else
None
let is_unification_pattern_pure_evar env evd (evk,args) t =
is_unification_pattern_evar env evd (evk,args) [] t <> None
let is_unification_pattern (env,nb) evd f l t =
match kind_of_term f with
| Meta m -> is_unification_pattern_meta env nb m l t
| Evar ev -> is_unification_pattern_evar env evd ev l t
| _ -> None
(* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
(pattern unification). It is assumed that l is made of rel's that
are distinct and not bound to aliases. *)
(* It is also assumed that c does not contain metas because metas
*implicitly* depend on Vars but lambda abstraction will not reflect this
dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
let solve_pattern_eqn env l c =
let c' = List.fold_right (fun a c ->
let c' = subst_term (lift 1 a) (lift 1 c) in
match kind_of_term a with
(* Rem: if [a] links to a let-in, do as if it were an assumption *)
| Rel n ->
let d = map_rel_declaration (lift n) (lookup_rel n env) in
mkLambda_or_LetIn d c'
| Var id ->
let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
| _ -> assert false)
l c in
(* Warning: we may miss some opportunity to eta-reduce more since c'
is not in normal form *)
whd_eta c'
(*****************************************)
(* Refining/solving unification problems *)
(*****************************************)
(* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
* [make_projectable_subst ev args] builds the substitution [Gamma:=args].
* If a variable and an alias of it are bound to the same instance, we skip
* the alias (we just use eq_constr -- instead of conv --, since anyway,
* only instances that are variables -- or evars -- are later considered;
* morever, we can bet that similar instances came at some time from
* the very same substitution. The removal of aliased duplicates is
* useful to ensure the uniqueness of a projection.
*)
let make_projectable_subst aliases sigma evi args =
let sign = evar_filtered_context evi in
let evar_aliases = compute_var_aliases sign in
let (_,full_subst,cstr_subst) =
List.fold_right
(fun (id,b,c) (args,all,cstrs) ->
match b,args with
| None, a::rest ->
let a = whd_evar sigma a in
let cstrs =
let a',args = decompose_app_vect a in
match kind_of_term a' with
| Construct cstr ->
let l = try Constrmap.find cstr cstrs with Not_found -> [] in
Constrmap.add cstr ((args,id)::l) cstrs
| _ -> cstrs in
(rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
| Some c, a::rest ->
let a = whd_evar sigma a in
(match kind_of_term c with
| Var id' ->
let idc = normalize_alias_var evar_aliases id' in
let sub = try Idmap.find idc all with Not_found -> [] in
if List.exists (fun (c,_,_) -> eq_constr a c) sub then
(rest,all,cstrs)
else
(rest,
Idmap.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
cstrs)
| _ ->
(rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
| _ -> anomaly "Instance does not match its signature")
sign (Array.rev_to_list args,Idmap.empty,Constrmap.empty) in
(full_subst,cstr_subst)
let make_pure_subst evi args =
snd (List.fold_right
(fun (id,b,c) (args,l) ->
match args with
| a::rest -> (rest, (id,a)::l)
| _ -> anomaly "Instance does not match its signature")
(evar_filtered_context evi) (Array.rev_to_list args,[]))
(*------------------------------------*
* operations on the evar constraints *
*------------------------------------*)
(* We have a unification problem Σ; Γ |- ?e[u1..uq] = t : s where ?e is not yet
* declared in Σ but yet known to be declarable in some context x1:T1..xq:Tq.
* [define_evar_from_virtual_equation ... Γ Σ t (x1:T1..xq:Tq) .. (u1..uq) (x1..xq)]
* declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds.
*)
let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env =
let ty_t_in_env = Retyping.get_type_of env evd t_in_env in
let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in
let t_in_env = whd_evar evd t_in_env in
let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
let ids = List.map pi1 (named_context_of_val sign) in
let inst_in_sign = List.map mkVar (List.filter_with filter ids) in
let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
(evd,whd_evar evd evar_in_sign)
(* We have x1..xq |- ?e1 : τ and had to solve something like
* Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
* ?e2[v1..vn], hence flexible. We had to go through k binders and now
* virtually have x1..xq, y1'..yk' | ?e1' : τ' and the equation
* Γ, y1..yk |- ?e1'[u1..uq y1..yk] = c.
* [materialize_evar Γ evd k (?e1[u1..uq]) τ'] extends Σ with the declaration
* of ?e1' and returns both its instance ?e1'[x1..xq y1..yk] in an extension
* of the context of e1 so that e1 can be instantiated by
* (...\y1' ... \yk' ... ?e1'[x1..xq y1'..yk']),
* and the instance ?e1'[u1..uq y1..yk] so that the remaining equation
* ?e1'[u1..uq y1..yk] = c can be registered
*
* Note that, because invert_definition does not check types, we need to
* guess the types of y1'..yn' by inverting the types of y1..yn along the
* substitution u1..uq.
*)
let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
let evi1 = Evd.find_undefined evd evk1 in
let env1,rel_sign = env_rel_context_chop k env in
let sign1 = evar_hyps evi1 in
let filter1 = evar_filter evi1 in
let ids1 = List.map pi1 (named_context_of_val sign1) in
let inst_in_sign = List.map mkVar (List.filter_with filter1 ids1) in
let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
let id = next_name_away na avoid in
let evd,t_in_sign =
define_evar_from_virtual_equation define_fun env evd t_in_env
sign filter inst_in_env in
let evd,b_in_sign = match b with
| None -> evd,None
| Some b ->
let evd,b = define_evar_from_virtual_equation define_fun env evd b
sign filter inst_in_env in
evd,Some b in
(push_named_context_val (id,b_in_sign,t_in_sign) sign,true::filter,
(mkRel 1)::(List.map (lift 1) inst_in_env),
(mkRel 1)::(List.map (lift 1) inst_in_sign),
push_rel d env,evd,id::avoid))
rel_sign
(sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
in
let evd,ev2ty_in_sign =
define_evar_from_virtual_equation define_fun env evd ty_in_env
sign2 filter2 inst2_in_env in
let evd,ev2_in_sign =
new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
(evd, ev2_in_sign, ev2_in_env)
let restrict_upon_filter evd evk p args =
let newfilter = List.map p args in
if List.for_all (fun id -> id) newfilter then
None
else
let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
Some (apply_subfilter oldfullfilter newfilter)
(* Inverting constructors in instances (common when inferring type of match) *)
let find_projectable_constructor env evd cstr k args cstr_subst =
try
let l = Constrmap.find cstr cstr_subst in
let args = Array.map (lift (-k)) args in
let l =
List.filter (fun (args',id) ->
(* is_conv is maybe too strong (and source of useless computation) *)
(* (at least expansion of aliases is needed) *)
Array.for_all2 (is_conv env evd) args args') l in
List.map snd l
with Not_found ->
[]
(* [find_projectable_vars env sigma y subst] finds all vars of [subst]
* that project on [y]. It is able to find solutions to the following
* two kinds of problems:
*
* - ?n[...;x:=y;...] = y
* - ?n[...;x:=?m[args];...] = y with ?m[args] = y recursively solvable
*
* (see test-suite/success/Fixpoint.v for an example of application of
* the second kind of problem).
*
* The seek for [y] is up to variable aliasing. In case of solutions that
* differ only up to aliasing, the binding that requires the less
* steps of alias reduction is kept. At the end, only one solution up
* to aliasing is kept.
*
* [find_projectable_vars] also unifies against evars that themselves mention
* [y] and recursively.
*
* In short, the following situations give the following solutions:
*
* problem evar ctxt soluce remark
* z1; z2:=z1 |- ?ev[z1;z2] = z1 y1:A; y2:=y1 y1 \ thanks to defs kept in
* z1; z2:=z1 |- ?ev[z1;z2] = z2 y1:A; y2:=y1 y2 / subst and preferring =
* z1; z2:=z1 |- ?ev[z1] = z2 y1:A y1 thanks to expand_var
* z1; z2:=z1 |- ?ev[z2] = z1 y1:A y1 thanks to expand_var
* z3 |- ?ev[z3;z3] = z3 y1:A; y2:=y1 y2 see make_projectable_subst
*
* Remark: [find_projectable_vars] assumes that identical instances of
* variables in the same set of aliased variables are already removed (see
* [make_projectable_subst])
*)
type evar_projection =
| ProjectVar
| ProjectEvar of existential * evar_info * identifier * evar_projection
exception NotUnique
exception NotUniqueInType of (identifier * evar_projection) list
let rec assoc_up_to_alias sigma aliases y yc = function
| [] -> raise Not_found
| (c,cc,id)::l ->
let c' = whd_evar sigma c in
if eq_constr y c' then id
else
if l <> [] then assoc_up_to_alias sigma aliases y yc l
else
(* Last chance, we reason up to alias conversion *)
match (if c == c' then cc else normalize_alias_opt aliases c') with
| Some cc when eq_constr yc cc -> id
| _ -> if eq_constr yc c then id else raise Not_found
let rec find_projectable_vars with_evars aliases sigma y subst =
let yc = normalize_alias aliases y in
let is_projectable idc idcl subst' =
(* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
try
let id = assoc_up_to_alias sigma aliases y yc idcl in
(id,ProjectVar)::subst'