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
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
|
(************************************************************************)
(* 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 Pp
open Util
open Errors
open Names
open Term
open Environ
open Termops
open Evd
open Namegen
open Retyping
open Reductionops
open Evarutil
open Pretype_errors
let normalize_evar evd ev =
match kind_of_term (whd_evar evd (mkEvar ev)) with
| Evar (evk,args) -> (evk,args)
| _ -> assert false
(************************)
(* Unification results *)
(************************)
type unification_result =
| Success of evar_map
| UnifFailure of evar_map * unification_error
let is_success = function Success _ -> true | UnifFailure _ -> false
let test_success conv_algo env evd c c' rhs =
is_success (conv_algo env evd c c' rhs)
(************************)
(* Manipulating filters *)
(************************)
let extract_subfilter initial_filter refined_filter =
snd (List.filter2 (fun b1 b2 -> b1) initial_filter refined_filter)
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))
(*------------------------------------*
* Restricting existing evars *
*------------------------------------*)
let rec eq_filter l1 l2 = match l1, l2 with
| [], [] -> true
| h1 :: l1, h2 :: l2 ->
(if h1 then h2 else not h2) && eq_filter l1 l2
| _ -> false
let restrict_evar_key evd evk filter candidates =
match filter, candidates with
| None, None -> evd, evk
| _ ->
let evi = Evd.find_undefined evd evk in
let oldfilter = evar_filter evi in
begin match filter, candidates with
| Some filter, None when eq_filter oldfilter filter ->
evd, evk
| _ ->
let filter = match filter with
| None -> evar_filter evi
| Some filter -> filter in
let candidates = match candidates with
| None -> evi.evar_candidates
| Some _ -> 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 = 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
end
(* 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
let noccur_evar env evd evk c =
let rec occur_rec k c = match kind_of_term c with
| Evar (evk',args' as ev') ->
(match safe_evar_value evd ev' with
| Some c -> occur_rec k c
| None ->
if Int.equal evk evk' then raise Occur
else Array.iter (occur_rec k) args')
| Rel i when i > k ->
(match pi2 (Environ.lookup_rel (i-k) env) with
| None -> ()
| Some b -> occur_rec k (lift i b))
| _ -> iter_constr_with_binders succ occur_rec k c
in
try occur_rec 0 c; true with Occur -> false
(***************************************)
(* 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 Id.Map.find id' aliases with Not_found -> [] in
Id.Map.add id (aliases_of_id@[t]) aliases
| _ ->
Id.Map.add id [t] aliases)
| None -> aliases)
sign Id.Map.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 Id.Map.find id' var_aliases with Not_found -> [] in
Int.Map.add n (aliases_of_n@[t]) aliases
| Rel p ->
let aliases_of_n =
try Int.Map.find (p+n) aliases with Not_found -> [] in
Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
| _ ->
Int.Map.add n [lift n t] aliases)
| None -> aliases))
rels (List.length rels,Int.Map.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 Int.equal n 0 then aliases else
(var_aliases,
Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (lift n) l))
rel_aliases Int.Map.empty)
let get_alias_chain_of aliases x = match kind_of_term x with
| Rel n -> (try Int.Map.find n (snd aliases) with Not_found -> [])
| Var id -> (try Id.Map.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,Int.Map.empty) (mkVar id))
let extend_alias (_,b,_) (var_aliases,rel_aliases) =
let rel_aliases =
Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l))
rel_aliases Int.Map.empty in
let rel_aliases =
match b with
| Some t ->
(match kind_of_term t with
| Var id' ->
let aliases_of_binder =
try Id.Map.find id' var_aliases with Not_found -> [] in
Int.Map.add 1 (aliases_of_binder@[t]) rel_aliases
| Rel p ->
let aliases_of_binder =
try Int.Map.find (p+1) rel_aliases with Not_found -> [] in
Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
| _ ->
Int.Map.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 Int.Set.empty and acc2 = ref Id.Set.empty in
let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
let is_in_cache depth = function
| Rel n -> Int.Set.mem (n-depth) !cache_rel
| Var s -> Id.Set.mem s !cache_var
| _ -> false in
let put_in_cache depth = function
| Rel n -> cache_rel := Int.Set.add (n-depth) !cache_rel
| Var s -> cache_var := Id.Set.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 := Id.Set.add id !acc2
| Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
| _ -> frec (aliases,depth) c end
| Const _ | Ind _ | Construct _ ->
acc2 := List.fold_right Id.Set.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)
(********************************)
(* 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 -> Id.Set.mem id fv_ids
| Rel n -> Int.Set.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 env 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 =
let is_ev = is_unification_pattern_evar env evd (evk,args) [] t in
match is_ev with
| None -> false
| Some _ -> true
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,Id.Map.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 Id.Map.find idc all with Not_found -> [] in
if List.exists (fun (c,_,_) -> eq_constr a c) sub then
(rest,all,cstrs)
else
(rest,
Id.Map.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
cstrs)
| _ ->
(rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
| _ -> anomaly (Pp.str "Instance does not match its signature"))
sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in
(full_subst,cstr_subst)
(*------------------------------------*
* 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)
(***************)
(* Unification *)
(* 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 * Id.t * evar_projection
exception NotUnique
exception NotUniqueInType of (Id.t * 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
match l with
| _ :: _ -> assoc_up_to_alias sigma aliases y yc l
| [] ->
(* 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'
with Not_found ->
(* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
(* projectable on [y] *)
if with_evars then
let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
match idcl' with
| [c,_,id] ->
begin
let (evk,argsv as t) = destEvar c in
let evi = Evd.find sigma evk in
let subst,_ = make_projectable_subst aliases sigma evi argsv in
let l = find_projectable_vars with_evars aliases sigma y subst in
match l with
| [id',p] -> (id,ProjectEvar (t,evi,id',p))::subst'
| _ -> subst'
end
| [] -> subst'
| _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance")
else
subst' in
Id.Map.fold is_projectable subst []
(* [filter_solution] checks if one and only one possible projection exists
* among a set of solutions to a projection problem *)
let filter_solution = function
| [] -> raise Not_found
| (id,p)::_::_ -> raise NotUnique
| [id,p] -> (mkVar id, p)
let project_with_effects aliases sigma effects t subst =
let c, p =
filter_solution (find_projectable_vars false aliases sigma t subst) in
effects := p :: !effects;
c
let rec find_solution_type evarenv = function
| (id,ProjectVar)::l -> pi3 (lookup_named id evarenv)
| [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv)
| (id,ProjectEvar _)::l -> find_solution_type evarenv l
| [] -> assert false
(* In case the solution to a projection problem requires the instantiation of
* subsidiary evars, [do_projection_effects] performs them; it
* also try to instantiate the type of those subsidiary evars if their
* type is an evar too.
*
* Note: typing creates new evar problems, which induces a recursive dependency
* with [define]. To avoid a too large set of recursive functions, we
* pass [define] to [do_projection_effects] as a parameter.
*)
let rec do_projection_effects define_fun env ty evd = function
| ProjectVar -> evd
| ProjectEvar ((evk,argsv),evi,id,p) ->
let evd = Evd.define evk (mkVar id) evd in
(* TODO: simplify constraints involving evk *)
let evd = do_projection_effects define_fun env ty evd p in
let ty = whd_betadeltaiota env evd (Lazy.force ty) in
if not (isSort ty) then
(* Don't try to instantiate if a sort because if evar_concl is an
evar it may commit to a univ level which is not the right
one (however, regarding coercions, because t is obtained by
unif, we know that no coercion can be inserted) *)
let subst = make_pure_subst evi argsv in
let ty' = replace_vars subst evi.evar_concl in
let ty' = whd_evar evd ty' in
if isEvar ty' then define_fun env evd (destEvar ty') ty else evd
else
evd
(* Assuming Σ; Γ, y1..yk |- c, [invert_arg_from_subst Γ k Σ [x1:=u1..xn:=un] c]
* tries to return φ(x1..xn) such that equation φ(u1..un) = c is valid.
* The strategy is to imitate the structure of c and then to invert
* the variables of c (i.e. rels or vars of Γ) using the algorithm
* implemented by project_with_effects/find_projectable_vars.
* It returns either a unique solution or says whether 0 or more than
* 1 solutions is found.
*
* Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
* Postcondition: if φ(x1..xn) is returned then
* Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
*
* The effects correspond to evars instantiated while trying to project.
*
* [invert_arg_from_subst] is used on instances of evars. Since the
* evars are flexible, these instances are potentially erasable. This
* is why we don't investigate whether evars in the instances of evars
* are unifiable, to the contrary of [invert_definition].
*)
type projectibility_kind =
| NoUniqueProjection
| UniqueProjection of constr * evar_projection list
type projectibility_status =
| CannotInvert
| Invertible of projectibility_kind
let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
let effects = ref [] in
let rec aux k t =
let t = whd_evar evd t in
match kind_of_term t with
| Rel i when i>k0+k -> aux' k (mkRel (i-k))
| Var id -> aux' k t
| _ -> map_constr_with_binders succ aux k t
and aux' k t =
try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
with Not_found ->
match expand_alias_once aliases t with
| None -> raise Not_found
| Some c -> aux k c in
try
let c = aux 0 c_in_env_extended_with_k_binders in
Invertible (UniqueProjection (c,!effects))
with
| Not_found -> CannotInvert
| NotUnique -> Invertible NoUniqueProjection
let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
match res with
| Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c)
->
CannotInvert
| _ ->
res
exception NotEnoughInformationToInvert
let extract_unique_projections projs =
List.map (function
| Invertible (UniqueProjection (c,_)) -> c
| _ ->
(* For instance, there are evars with non-invertible arguments and *)
(* we cannot arbitrarily restrict these evars before knowing if there *)
(* will really be used; it can also be due to some argument *)
(* (typically a rel) that is not inversible and that cannot be *)
(* inverted either because it is needed for typing the conclusion *)
(* of the evar to project *)
raise NotEnoughInformationToInvert) projs
let extract_candidates sols =
try
Some
(List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols)
with Exit ->
None
let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
let evi = Evd.find_undefined evd evk in
let subst,_ = make_projectable_subst aliases evd evi argsv in
let projs =
Array.map_to_list (invert_arg fullenv evd aliases k evk subst) args' in
Array.of_list (extract_unique_projections projs)
(* Redefines an evar with a smaller context (i.e. it may depend on less
* variables) such that c becomes closed.
* Example: in "fun (x:?1) (y:list ?2[x]) => x = y :> ?3[x,y] /\ x = nil bool"
* ?3 <-- ?1 no pb: env of ?3 is larger than ?1's
* ?1 <-- list ?2 pb: ?2 may depend on x, but not ?1.
* What we do is that ?2 is defined by a new evar ?4 whose context will be
* a prefix of ?2's env, included in ?1's env.
*
* If "hyps |- ?e : T" and "filter" selects a subset hyps' of hyps then
* [do_restrict_hyps evd ?e filter] sets ?e:=?e'[hyps'] and returns ?e'
* such that "hyps' |- ?e : T"
*)
let filter_candidates evd evk filter candidates =
let evi = Evd.find_undefined evd evk in
let candidates = match candidates with
| None -> evi.evar_candidates
| Some _ -> candidates in
match candidates,filter with
| None,_ | _, None -> candidates
| Some l, Some filter ->
let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in
Some (List.filter (fun a ->
List.subset (Id.Set.elements (collect_vars a)) ids) l)
let eq_filter f1 f2 =
let eq_bool b1 b2 = if b1 then b2 else not b2 in
List.equal eq_bool f1 f2
let closure_of_filter evd evk filter =
let evi = Evd.find_undefined evd evk in
let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
let ids = List.map pi1 (evar_context evi) in
let test id b = b || Id.Set.mem id vars in
let newfilter = List.map2 test ids filter in
if eq_filter newfilter (evar_filter evi) then None else Some newfilter
let restrict_hyps evd evk filter candidates =
(* What to do with dependencies?
Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
- If y is in a non-erasable position in C(x,y) (i.e. it is not below an
occurrence of x in the hnf of C), then z should be removed too.
- If y is in a non-erasable position in T(x,y,z) then the problem is
unsolvable.
Computing whether y is erasable or not may be costly and the
interest for this early detection in practice is not obvious. We let
it for future work. In any case, thanks to the use of filters, the whole
(unrestricted) context remains consistent. *)
let candidates = filter_candidates evd evk (Some filter) candidates in
let typablefilter = closure_of_filter evd evk filter in
(typablefilter,candidates)
exception EvarSolvedWhileRestricting of evar_map * constr
let do_restrict_hyps evd (evk,args as ev) filter candidates =
let filter,candidates = match filter with
| None -> None,candidates
| Some filter -> restrict_hyps evd evk filter candidates in
match candidates,filter with
| Some [], _ -> error "Not solvable."
| Some [nc],_ ->
let evd = Evd.define evk nc evd in
raise (EvarSolvedWhileRestricting (evd,whd_evar evd (mkEvar ev)))
| None, None -> evd,ev
| _ -> restrict_applied_evar evd ev filter candidates
(* [postpone_non_unique_projection] postpones equation of the form ?e[?] = c *)
(* ?e is assumed to have no candidates *)
let postpone_non_unique_projection env evd (evk,argsv as ev) sols rhs =
let rhs = expand_vars_in_term env rhs in
let filter =
restrict_upon_filter evd evk
(* Keep only variables that occur in rhs *)
(* This is not safe: is the variable is a local def, its body *)
(* may contain references to variables that are removed, leading to *)
(* a ill-formed context. We would actually need a notion of filter *)
(* that says that the body is hidden. Note that expand_vars_in_term *)
(* expands only rels and vars aliases, not rels or vars bound to an *)
(* arbitrary complex term *)
(fun a -> not (isRel a || isVar a)
|| dependent a rhs || List.exists (fun (id,_) -> isVarId id a) sols)
(Array.to_list argsv) in
let filter = match filter with
| None -> None
| Some filter -> closure_of_filter evd evk filter in
let candidates = extract_candidates sols in
match candidates with
| None ->
(* We made an approximation by not expanding a local definition *)
let evd,ev = restrict_applied_evar evd ev filter None in
let pb = (Reduction.CONV,env,mkEvar ev,rhs) in
Evd.add_conv_pb pb evd
| Some _ ->
restrict_evar evd evk filter candidates
(* [postpone_evar_evar] postpones an equation of the form ?e1[?1] = ?e2[?2] *)
let postpone_evar_evar f env evd filter1 ev1 filter2 ev2 =
(* Leave an equation between (restrictions of) ev1 andv ev2 *)
try
let evd,ev1' = do_restrict_hyps evd ev1 filter1 None in
try
let evd,ev2' = do_restrict_hyps evd ev2 filter2 None in
add_conv_pb (Reduction.CONV,env,mkEvar ev1',mkEvar ev2') evd
with EvarSolvedWhileRestricting (evd,ev2) ->
(* ev2 solved on the fly *)
f env evd ev1' ev2
with EvarSolvedWhileRestricting (evd,ev1) ->
(* ev1 solved on the fly *)
f env evd ev2 ev1
(* [solve_evar_evar f Γ Σ ?e1[u1..un] ?e2[v1..vp]] applies an heuristic
* to solve the equation Σ; Γ ⊢ ?e1[u1..un] = ?e2[v1..vp]:
* - if there are at most one φj for each vj s.t. vj = φj(u1..un),
* we first restrict ?e2 to the subset v_k1..v_kq of the vj that are
* inversible and we set ?e1[x1..xn] := ?e2[φk1(x1..xn)..φkp(x1..xn)]
* (this is a case of pattern-unification)
* - symmetrically if there are at most one ψj for each uj s.t.
* uj = ψj(v1..vp),
* - otherwise, each position i s.t. ui does not occur in v1..vp has to
* be restricted and similarly for the vi, and we leave the equation
* as an open equation (performed by [postpone_evar])
*
* Warning: the notion of unique φj is relative to some given class
* of unification problems
*
* Note: argument f is the function used to instantiate evars.
*)
let are_canonical_instances args1 args2 env =
let n1 = Array.length args1 in
let n2 = Array.length args2 in
let rec aux n = function
| (id,_,c)::sign
when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) ->
aux (n+1) sign
| [] ->
let rec aux2 n =
Int.equal n n1 ||
(isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
in aux2 n
| _ -> false in
Int.equal n1 n2 && aux 0 (named_context env)
let filter_compatible_candidates conv_algo env evd evi args rhs c =
let c' = instantiate_evar (evar_filtered_context evi) c args in
match conv_algo env evd Reduction.CONV rhs c' with
| Success evd -> Some (c,evd)
| UnifFailure _ -> None
exception DoesNotPreserveCandidateRestriction
let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
let evi1 = Evd.find evd evk1 in
let evi2 = Evd.find evd evk2 in
let cand1 = filter_candidates evd evk1 filter1 None in
let cand2 = evi2.evar_candidates in
match cand1, cand2 with
| _, None -> cand1
| None, Some _ -> raise DoesNotPreserveCandidateRestriction
| Some l1, Some l2 ->
let args1 = Array.to_list argsv1 in
let args2 = Array.to_list argsv2 in
let l1' = List.filter (fun c1 ->
let c1' = instantiate_evar (evar_filtered_context evi1) c1 args1 in
let filter c2 =
let compatibility = filter_compatible_candidates conv_algo env evd evi2 args2 c1' c2 in
match compatibility with
| None -> false
| Some _ -> true
in
let filtered = List.filter filter l2 in
match filtered with [] -> false | _ -> true) l1 in
if Int.equal (List.length l1) (List.length l1') then None else Some l1'
exception CannotProject of bool list option
(* Assume that FV(?n[x1:=t1..xn:=tn]) belongs to some set U.
Can ?n be instantiated by a term u depending essentially on xi such that the
FV(u[x1:=t1..xn:=tn]) are in the set U?
- If ti is a variable, it has to be in U.
- If ti is a constructor, its parameters cannot be erased even if u
matches on it, so we have to discard ti if the parameters
contain variables not in U.
- If ti is rigid, we have to discard it if it contains variables in U.
Note: when restricting as part of an equation ?n[x1:=t1..xn:=tn] = ?m[...]
then, occurrences of ?m in the ti can be seen, like variables, as occurrences
of subterms to eventually discard so as to be allowed to keep ti.
*)
let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
let f,args = decompose_app_vect t in
match kind_of_term f with
| Construct (ind,_) ->
let params,_ = Array.chop (Inductiveops.inductive_nparams ind) args in
Array.for_all (is_constrainable_in k g) params
| Ind _ -> Array.for_all (is_constrainable_in k g) args
| Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
| Evar (ev',_) -> not (Int.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
| Var id -> Id.Set.mem id fv_ids
| Rel n -> n <= k || Int.Set.mem n fv_rels
| Sort _ -> true
| _ -> (* We don't try to be more clever *) true
let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
let t = expansion_of_var aliases t in
match kind_of_term t with
| Var id -> Id.Set.mem id fv_ids
| Rel n -> n <= k || Int.Set.mem n fv_rels
| _ -> is_constrainable_in k (ev,fvs) t
let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
let filter1 =
restrict_upon_filter evd evk1 (noccur_evar env evd evk2)
(Array.to_list argsv1)
in
let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
let filter2 =
restrict_upon_filter evd evk2 (noccur_evar env evd evk1)
(Array.to_list argsv2)
in
let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
evd,ev1,ev2
exception EvarSolvedOnTheFly of evar_map * constr
let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
(* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
let filter1 = restrict_upon_filter evd evk1
(has_constrainable_free_vars evd aliases k2 evk2 fvs2)
(Array.to_list argsv1) in
(* Only try pruning on variable substitutions, postpone otherwise. *)
(* Rules out non-linear instances. *)
if is_unification_pattern_pure_evar env evd ev2 (mkEvar ev1) then
try
let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in
evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1)
with
| EvarSolvedWhileRestricting (evd,ev1) ->
raise (EvarSolvedOnTheFly (evd,ev1))
| DoesNotPreserveCandidateRestriction | NotEnoughInformationToInvert ->
raise (CannotProject filter1)
else
raise (CannotProject filter1)
let solve_evar_evar_l2r f g env evd aliases ev1 (evk2,_ as ev2) =
try
let evd,body = project_evar_on_evar g env evd aliases 0 ev1 ev2 in
Evd.define evk2 body evd
with EvarSolvedOnTheFly (evd,c) ->
f env evd ev2 c
let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 as ev2) =
if are_canonical_instances args1 args2 env then
(* If instances are canonical, we solve the problem in linear time *)
let sign = evar_filtered_context (Evd.find evd evk2) in
let id_inst = Array.map (fun (id,_,_) -> mkVar id) (Array.of_list sign) in
Evd.define evk2 (mkEvar(evk1,id_inst)) evd
else
let evd,ev1,ev2 =
(* If an evar occurs in the instance of the other evar and the
use of an heuristic is forced, we restrict *)
if force then ensure_evar_independent g env evd ev1 ev2 else (evd,ev1,ev2) in
let aliases = make_alias_map env in
try solve_evar_evar_l2r f g env evd aliases ev1 ev2
with CannotProject filter1 ->
try solve_evar_evar_l2r f g env evd aliases ev2 ev1
with CannotProject filter2 ->
postpone_evar_evar f env evd filter1 ev1 filter2 ev2
type conv_fun =
env -> evar_map -> conv_pb -> constr -> constr -> unification_result
type conv_fun_bool =
env -> evar_map -> conv_pb -> constr -> constr -> bool
exception IllTypedInstance of env * types * types
let check_evar_instance evd evk1 body conv_algo =
let evi = Evd.find evd evk1 in
let evenv = evar_env evi in
(* FIXME: The body might be ill-typed when this is called from w_merge *)
let ty =
try Retyping.get_type_of evenv evd body
with e when Errors.noncritical e -> error "Ill-typed evar instance"
in
match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with
| Success evd -> evd
| UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
(* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
* definitions. We try to unify the ti with the ui pairwise. The pairs
* that don't unify are discarded (i.e. ?e is redefined so that it does not
* depend on these args). *)
let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
if Array.equal eq_constr argsv1 argsv2 then evd else
(* Filter and restrict if needed *)
let untypedfilter =
restrict_upon_filter evd evk
(fun (a1,a2) -> conv_algo env evd Reduction.CONV a1 a2)
(List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
let candidates = filter_candidates evd evk untypedfilter None in
let filter = match untypedfilter with
| None -> None
| Some filter -> closure_of_filter evd evk filter in
let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
if Int.equal (fst ev1) evk && can_drop then (* No refinement *) evd else
(* either progress, or not allowed to drop, e.g. to preserve possibly *)
(* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
(* if e can depend on x until ?y is not resolved, or, conversely, we *)
(* don't know if ?y has to be unified with ?y, until e is resolved *)
let argsv2 = restrict_instance evd evk filter argsv2 in
let ev2 = (fst ev1,argsv2) in
(* Leave a unification problem *)
Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev1,mkEvar ev2) evd
(* If the evar can be instantiated by a finite set of candidates known
in advance, we check which of them apply *)
exception NoCandidates
let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
let evi = Evd.find evd evk in
let args = Array.to_list argsv in
match evi.evar_candidates with
| None -> raise NoCandidates
| Some l ->
let l' =
List.map_filter
(filter_compatible_candidates conv_algo env evd evi args rhs) l in
match l' with
| [] -> error_cannot_unify env evd (mkEvar ev, rhs)
| [c,evd] ->
(* solve_candidates might have been called recursively in the mean *)
(* time and the evar been solved by the filtering process *)
if Evd.is_undefined evd evk then Evd.define evk c evd else evd
| l when List.length l < List.length l' ->
let candidates = List.map fst l in
restrict_evar evd evk None (Some candidates)
| l -> evd
(* We try to instantiate the evar assuming the body won't depend
* on arguments that are not Rels or Vars, or appearing several times
* (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
*
* 1) Let "env |- ?ev[hyps:=args] = rhs" be the unification problem
* 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
* where only Rel's and Var's are relevant in subst
* 3) We recur on rhs, "imitating" the term, and failing if some Rel/Var is
* not in the scope of ?ev. For instance, the problem
* "y:nat |- ?x[] = y" where "|- ?1:nat" is not satisfiable because
* ?1 would be instantiated by y which is not in the scope of ?1.
* 4) We try to "project" the term if the process of imitation fails
* and that only one projection is possible
*
* Note: we don't assume rhs in normal form, it may fail while it would
* have succeeded after some reductions.
*
* This is the work of [invert_definition Γ Σ ?ev[hyps:=args] c]
* Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
* Postcondition: if φ(x1..xn) is returned then
* Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
*)
exception NotInvertibleUsingOurAlgorithm of constr
exception NotEnoughInformationToProgress of (Id.t * evar_projection) list
exception OccurCheckIn of evar_map * constr
exception MetaOccurInBodyInternal
let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
let aliases = make_alias_map env in
let evdref = ref evd in
let progress = ref false in
let evi = Evd.find evd evk in
let subst,cstr_subst = make_projectable_subst aliases evd evi argsv in
(* Projection *)
let project_variable t =
(* Evar/Var problem: unifiable iff variable projectable from ev subst *)
try
let sols = find_projectable_vars true aliases !evdref t subst in
let c, p = match sols with
| [] -> raise Not_found
| [id,p] -> (mkVar id, p)
| (id,p)::_::_ ->
if choose then (mkVar id, p) else raise (NotUniqueInType sols)
in
let ty = lazy (Retyping.get_type_of env !evdref t) in
let evd = do_projection_effects (evar_define conv_algo) env ty !evdref p in
evdref := evd;
c
with
| Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
| NotUniqueInType sols ->
if not !progress then
raise (NotEnoughInformationToProgress sols);
(* No unique projection but still restrict to where it is possible *)
(* materializing is necessary, but is restricting useful? *)
let ty = find_solution_type (evar_filtered_env evi) sols in
let sign = evar_filtered_context evi in
let ty' = instantiate_evar sign ty (Array.to_list argsv) in
let (evd,evar,(evk',argsv' as ev')) =
materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
let ts = expansions_of_var aliases t in
let test c = isEvar c or List.mem c ts in
let filter = Array.map_to_list test argsv' in
let filter = apply_subfilter (evar_filter (Evd.find_undefined evd evk)) filter in
let filter = closure_of_filter evd evk' filter in
let candidates = extract_candidates sols in
let evd = match candidates with
| None ->
let evd, ev'' = restrict_applied_evar evd ev' filter None in
Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd
| Some _ ->
restrict_evar evd evk' filter candidates
in
evdref := evd;
evar in
let rec imitate (env',k as envk) t =
let t = whd_evar !evdref t in
match kind_of_term t with
| Rel i when i>k ->
(match pi2 (Environ.lookup_rel (i-k) env') with
| None -> project_variable (mkRel (i-k))
| Some b ->
try project_variable (mkRel (i-k))
with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i b))
| Var id ->
(match pi2 (Environ.lookup_named id env') with
| None -> project_variable t
| Some b ->
try project_variable t
with NotInvertibleUsingOurAlgorithm _ -> imitate envk b)
| Evar (evk',args' as ev') ->
if Int.equal evk evk' then raise (OccurCheckIn (evd,rhs));
(* Evar/Evar problem (but left evar is virtual) *)
let aliases = lift_aliases k aliases in
(try
let ev = (evk,Array.map (lift k) argsv) in
let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev' ev in
evdref := evd;
body
with
| EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t
| CannotProject filter' ->
assert !progress;
(* Make the virtual left evar real *)
let ty = get_type_of env' !evdref t in
let (evd,evar'',ev'') =
materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
(* materialize_evar may instantiate ev' by another evar; adjust it *)
let (evk',args' as ev') = normalize_evar evd ev' in
let evd =
(* Try to project (a restriction of) the left evar ... *)
try
let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 ev'' ev' in
Evd.define evk' body evd
with
| EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
| CannotProject filter'' ->
(* ... or postpone the problem *)
postpone_evar_evar (evar_define conv_algo) env' evd filter'' ev'' filter' ev' in
evdref := evd;
evar'')
| _ ->
progress := true;
match
let c,args = decompose_app_vect t in
match kind_of_term c with
| Construct cstr when noccur_between 1 k t ->
(* This is common case when inferring the return clause of match *)
(* (currently rudimentary: we do not treat the case of multiple *)
(* possible inversions; we do not treat overlap with a possible *)
(* alternative inversion of the subterms of the constructor, etc)*)
(match find_projectable_constructor env evd cstr k args cstr_subst with
| _::_ as l -> Some (List.map mkVar l)
| _ -> None)
| _ -> None
with
| Some l ->
let ty = get_type_of env' !evdref t in
let candidates =
try
let t =
map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
imitate envk t in
t::l
with e when Errors.noncritical e -> l in
(match candidates with
| [x] -> x
| _ ->
let (evd,evar'',ev'') =
materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
evdref := restrict_evar evd (fst ev'') None (Some candidates);
evar'')
| None ->
(* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
imitate envk t in
let rhs = whd_beta evd rhs (* heuristic *) in
let body = imitate (env,0) rhs in
(!evdref,body)
(* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
* an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
* [define] tries to find an instance lhs such that
* "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in
* context "hyps" and not referring to itself.
*)
and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
match kind_of_term rhs with
| Evar (evk2,argsv2 as ev2) ->
if Int.equal evk evk2 then
solve_refl ~can_drop:choose
(test_success conv_algo) env evd evk argsv argsv2
else
solve_evar_evar ~force:choose
(evar_define conv_algo) conv_algo env evd ev ev2
| _ ->
try solve_candidates conv_algo env evd ev rhs
with NoCandidates ->
try
let (evd',body) = invert_definition conv_algo choose env evd ev rhs in
if occur_meta body then raise MetaOccurInBodyInternal;
(* invert_definition may have instantiate some evars of rhs with evk *)
(* so we recheck acyclicity *)
if occur_evar evk body then raise (OccurCheckIn (evd',body));
(* needed only if an inferred type *)
let body = refresh_universes body in
(* Cannot strictly type instantiations since the unification algorithm
* does not unify applications from left to right.
* e.g problem f x == g y yields x==y and f==g (in that order)
* Another problem is that type variables are evars of type Type
let _ =
try
let env = evar_filtered_env evi in
let ty = evi.evar_concl in
Typing.check env evd' body ty
with e ->
msg_info
(str "Ill-typed evar instantiation: " ++ fnl() ++
pr_evar_map evd' ++ fnl() ++
str "----> " ++ int ev ++ str " := " ++
print_constr body);
raise e in*)
let evd' = check_evar_instance evd' evk body conv_algo in
Evd.define evk body evd'
with
| NotEnoughInformationToProgress sols ->
postpone_non_unique_projection env evd ev sols rhs
| NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
raise e
| OccurCheckIn (evd,rhs) ->
(* last chance: rhs actually reduces to ev *)
let c = whd_betadeltaiota env evd rhs in
match kind_of_term c with
| Evar (evk',argsv2) when Int.equal evk evk' ->
solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
env evd evk argsv argsv2
| _ ->
raise (OccurCheckIn (evd,rhs))
(* This code (i.e. solve_pb, etc.) takes a unification
* problem, and tries to solve it. If it solves it, then it removes
* all the conversion problems, and re-runs conversion on each one, in
* the hopes that the new solution will aid in solving them.
*
* The kinds of problems it knows how to solve are those in which
* the usable arguments of an existential var are all themselves
* universal variables.
* The solution to this problem is to do renaming for the Var's,
* to make them match up with the Var's which are found in the
* hyps of the existential, to do a "pop" for each Rel which is
* not an argument of the existential, and a subst1 for each which
* is, again, with the corresponding variable. This is done by
* define
*
* Thus, we take the arguments of the existential which we are about
* to assign, and zip them with the identifiers in the hypotheses.
* Then, we process all the Var's in the arguments, and sort the
* Rel's into ascending order. Then, we just march up, doing
* subst1's and pop's.
*
* NOTE: We can do this more efficiently for the relative arguments,
* by building a long substituend by hand, but this is a pain in the
* ass.
*)
let status_changed lev (pbty,_,t1,t2) =
(try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or
(try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false)
let reconsider_conv_pbs conv_algo evd =
let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
List.fold_left
(fun p (pbty,env,t1,t2) ->
match p with
| Success evd -> conv_algo env evd pbty t1 t2
| UnifFailure _ as x -> x) (Success evd)
pbs
(* Tries to solve problem t1 = t2.
* Precondition: t1 is an uninstantiated evar
* Returns an optional list of evars that were instantiated, or None
* if the problem couldn't be solved. *)
(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
try
let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
let evd =
match pbty with
| Some true when isEvar t2 ->
add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd
| Some false when isEvar t2 ->
add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
| _ ->
evar_define conv_algo ~choose env evd ev1 t2 in
reconsider_conv_pbs conv_algo evd
with
| NotInvertibleUsingOurAlgorithm t ->
UnifFailure (evd,NotClean (ev1,t))
| OccurCheckIn (evd,rhs) ->
UnifFailure (evd,OccurCheck (evk1,rhs))
| MetaOccurInBodyInternal ->
UnifFailure (evd,MetaOccurInBody evk1)
| IllTypedInstance (env,t,u) ->
UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))
|