Source file clenv.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
open Pp
open CErrors
open Util
open Names
open Nameops
open Termops
open Constr
open Context
open Namegen
open Environ
open Evd
open EConstr
open Vars
open Reduction
open Reductionops
open Tacred
open Pretype_errors
open Evarutil
open Unification
open Tactypes
open Logic
type clausenv = {
env : env;
evd : evar_map;
templval : constr freelisted;
templtyp : constr freelisted;
cache : Reductionops.meta_instance_subst;
}
let mk_clausenv env evd templval templtyp = {
env; evd; templval; templtyp; cache = create_meta_instance_subst evd;
}
let update_clenv_evd clenv evd =
mk_clausenv clenv.env evd clenv.templval clenv.templtyp
let cl_env ce = ce.env
let cl_sigma ce = ce.evd
let clenv_term clenv c = meta_instance clenv.env clenv.cache c
let clenv_meta_type clenv mv =
let ty =
try Evd.meta_ftype clenv.evd mv
with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
meta_instance clenv.env clenv.cache ty
let clenv_value clenv = meta_instance clenv.env clenv.cache clenv.templval
let clenv_type clenv = meta_instance clenv.env clenv.cache clenv.templtyp
let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
exception NotExtensibleClause
let clenv_push_prod cl =
let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
let rec clrec typ = match EConstr.kind cl.evd typ with
| Cast (t,_,_) -> clrec t
| Prod (na,t,u) ->
let mv = new_meta () in
let dep = not (noccurn (cl_sigma cl) 1 u) in
let na' = if dep then na.binder_name else Anonymous in
let e' = meta_declare mv t ~name:na' cl.evd in
let concl = if dep then subst1 (mkMeta mv) u else u in
let def = applist (cl.templval.rebus,[mkMeta mv]) in
{ templval = mk_freelisted def;
templtyp = mk_freelisted concl;
evd = e';
env = cl.env;
cache = create_meta_instance_subst e' }
| _ -> raise NotExtensibleClause
in clrec typ
(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
[lmetas] is a list of metas to be applied to a proof of [t] so that
it produces the unification pattern [ccl]; [sigma'] is [sigma]
extended with [lmetas]; if [n] is defined, it limits the size of
the list even if [ccl] is still a product; otherwise, it stops when
[ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
[ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
let clenv_environments evd bound t =
let open EConstr in
let open Vars in
let rec clrec (e,metas) n t =
match n, EConstr.kind evd t with
| (Some 0, _) -> (e, List.rev metas, t)
| (n, Cast (t,_,_)) -> clrec (e,metas) n t
| (n, Prod (na,t1,t2)) ->
let mv = new_meta () in
let dep = not (noccurn evd 1 t2) in
let na' = if dep then na.binder_name else Anonymous in
let e' = meta_declare mv t1 ~name:na' e in
clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
(if dep then (subst1 (mkMeta mv) t2) else t2)
| (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
| (n, _) -> (e, List.rev metas, t)
in
clrec (evd,[]) bound t
let mk_clenv_from_env env sigma n (c,cty) =
let evd = clear_metas sigma in
let (evd,args,concl) = clenv_environments evd n cty in
{ templval = mk_freelisted (applist (c,args));
templtyp = mk_freelisted concl;
evd = evd;
env = env;
cache = create_meta_instance_subst evd }
let mk_clenv_from_n gls n (c,cty) =
let env = Proofview.Goal.env gls in
let sigma = Tacmach.New.project gls in
mk_clenv_from_env env sigma n (c, cty)
let mk_clenv_from gls = mk_clenv_from_n gls None
let mentions clenv mv0 =
let rec menrec mv1 =
Int.equal mv0 mv1 ||
let mlist =
try match meta_opt_fvalue clenv.evd mv1 with
| Some (b,_) -> b.freemetas
| None -> Metaset.empty
with Not_found -> Metaset.empty in
Metaset.exists menrec mlist
in menrec
let error_incompatible_inst clenv mv =
let na = meta_name clenv.evd mv in
match na with
Name id ->
user_err ~hdr:"clenv_assign"
(str "An incompatible instantiation has already been found for " ++
Id.print id)
| _ ->
anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.")
let clenv_assign mv rhs clenv =
let rhs_fls = mk_freelisted rhs in
if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then
user_err Pp.(str "clenv_assign: circularity in unification");
try
if meta_defined clenv.evd mv then
if not (EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
error_incompatible_inst clenv mv
else
clenv
else
let st = (Conv,TypeNotProcessed) in
update_clenv_evd clenv (meta_assign mv (rhs_fls.rebus,st) clenv.evd)
with Not_found ->
user_err Pp.(str "clenv_assign: undefined meta")
let clenv_metas_in_type_of_meta clenv mv =
(mk_freelisted (meta_instance clenv.env clenv.cache (meta_ftype clenv.evd mv))).freemetas
let dependent_in_type_of_metas clenv mvs =
List.fold_right
(fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv mv))
mvs Metaset.empty
let dependent_closure clenv mvs =
let rec aux mvs acc =
Metaset.fold
(fun mv deps ->
let metas_of_meta_type = clenv_metas_in_type_of_meta clenv mv in
aux metas_of_meta_type (Metaset.union deps metas_of_meta_type))
mvs acc in
aux mvs mvs
let clenv_dependent_gen hyps_only ?(iter=true) clenv =
let all_undefined = undefined_metas clenv.evd in
let deps_in_concl = (mk_freelisted (clenv_type clenv)).freemetas in
let deps_in_hyps = dependent_in_type_of_metas clenv all_undefined in
let deps_in_concl =
if hyps_only && iter then dependent_closure clenv deps_in_concl
else deps_in_concl in
List.filter
(fun mv ->
if hyps_only then
Metaset.mem mv deps_in_hyps && not (Metaset.mem mv deps_in_concl)
else
Metaset.mem mv deps_in_hyps || Metaset.mem mv deps_in_concl)
all_undefined
let clenv_missing ce = clenv_dependent_gen true ce
let clenv_dependent ce = clenv_dependent_gen false ce
let meta_reducible_instance env evd b =
let fm = b.freemetas in
let fold mv accu =
let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in
match fvalue with
| None -> accu
| Some (g, (_, s)) -> Metamap.add mv (g.rebus, s) accu
in
let metas = Metaset.fold fold fm Metamap.empty in
let rec irec u =
let u = whd_betaiota env Evd.empty u in
match EConstr.kind evd u with
| Case (ci,u,pms,p,iv,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
let m = destMeta evd (strip_outer_cast evd c) in
(match
try
let g, s = Metamap.find m metas in
let is_coerce = match s with CoerceToType -> true | _ -> false in
if isConstruct evd g || not is_coerce then Some g else None
with Not_found -> None
with
| Some g -> irec (mkCase (ci,u,pms,p,iv,g,bl))
| None ->
let on_ctx (na, c) = (na, irec c) in
mkCase (ci,u,Array.map irec pms,on_ctx p,iv,c,Array.map on_ctx bl))
| App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) ->
let m = destMeta evd (strip_outer_cast evd f) in
(match
try
let g, s = Metamap.find m metas in
let is_coerce = match s with CoerceToType -> true | _ -> false in
if isLambda evd g || not is_coerce then Some g else None
with Not_found -> None
with
| Some g -> irec (mkApp (g,l))
| None -> mkApp (f,Array.map irec l))
| Meta m ->
(try let g, s = Metamap.find m metas in
let is_coerce = match s with CoerceToType -> true | _ -> false in
if not is_coerce then irec g else u
with Not_found -> u)
| Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) ->
let m = try destMeta evd c with DestKO -> destMeta evd (pi1 (destCast evd c)) in
(match
try
let g, s = Metamap.find m metas in
let is_coerce = match s with CoerceToType -> true | _ -> false in
if isConstruct evd g || not is_coerce then Some g else None
with Not_found -> None
with
| Some g -> irec (mkProj (p,g))
| None -> mkProj (p,c))
| _ -> EConstr.map evd irec u
in
if Metaset.is_empty fm then b.rebus
else irec b.rebus
let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
update_clenv_evd clenv (w_unify ~flags clenv.env clenv.evd cv_pb t1 t2)
let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
update_clenv_evd clenv (w_unify_meta_types ~flags:flags clenv.env clenv.evd)
let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd clenv.templtyp.rebus))) then
clenv_unify CUMUL ~flags (clenv_type clenv) concl
(clenv_unify_meta_types ~flags clenv)
else
clenv_unify CUMUL ~flags
(meta_reducible_instance clenv.env clenv.evd clenv.templtyp) concl clenv
let clenv_unique_resolver ?flags clenv gl =
let concl = Proofview.Goal.concl gl in
clenv_unique_resolver_gen ?flags clenv concl
let adjust_meta_source evd mv = function
| loc,Evar_kinds.VarInstance id ->
let rec match_name c l =
match EConstr.kind evd c, l with
| Lambda ({binder_name=Name id},_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id
| Lambda (_,_,c), a::l -> match_name c l
| _ -> None in
let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
if Metaset.mem mv t.freemetas then
let f,l = decompose_app evd t.rebus in
match EConstr.kind evd f with
| Meta mv'' ->
(match meta_opt_fvalue evd mv'' with
| Some (c,_) -> match_name c.rebus l
| None -> None)
| _ -> None
else None in
let id = try List.find_map f (Evd.meta_list evd) with Not_found -> id in
loc,Evar_kinds.VarInstance id
| src -> src
let clenv_pose_metas_as_evars clenv dep_mvs =
let rec fold clenv = function
| [] -> clenv
| mv::mvs ->
let ty = clenv_meta_type clenv mv in
if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
else
let src = evar_source_of_meta mv clenv.evd in
let src = adjust_meta_source clenv.evd mv src in
let evd = clenv.evd in
let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
let clenv = clenv_assign mv evar {clenv with evd=evd} in
fold clenv mvs in
fold clenv dep_mvs
let fchain_flags () =
{ (default_unify_flags ()) with
allow_K_in_toplevel_higher_order_unification = true }
let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv =
let evd = meta_merge ?with_univs nextclenv.evd clenv.evd in
let clenv' =
{ templval = clenv.templval;
templtyp = clenv.templtyp;
evd;
env = nextclenv.env;
cache = create_meta_instance_subst evd } in
let clenv'' =
clenv_unify ~flags CUMUL
(clenv_term clenv' nextclenv.templtyp)
(clenv_meta_type clenv' mv)
clenv' in
let clenv''' =
clenv_assign mv (clenv_term clenv' nextclenv.templval) clenv''
in
clenv'''
let clenv_independent clenv =
let mvs = collect_metas clenv.evd (clenv_value clenv) in
let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in
List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
let qhyp_eq h1 h2 = match h1, h2 with
| NamedHyp n1, NamedHyp n2 -> Id.equal n1 n2
| AnonHyp i1, AnonHyp i2 -> Int.equal i1 i2
| _ -> false
let check_bindings bl =
match List.duplicates qhyp_eq (List.map (fun {CAst.v=x} -> fst x) bl) with
| NamedHyp s :: _ ->
user_err
(str "The variable " ++ Id.print s ++
str " occurs more than once in binding list.");
| AnonHyp n :: _ ->
user_err
(str "The position " ++ int n ++
str " occurs more than once in binding list.")
| [] -> ()
let explain_no_such_bound_variable evd id =
let fold l (n, clb) =
let na = match clb with
| Cltyp (na, _) -> na
| Clval (na, _, _) -> na
in
if na != Anonymous then Name.get_id na :: l else l
in
let mvl = List.fold_left fold [] (Evd.meta_list evd) in
user_err ~hdr:"Evd.meta_with_name"
(str"No such bound variable " ++ Id.print id ++
(if mvl == [] then str " (no bound variables at all in the expression)."
else
(str" (possible name" ++
str (if List.length mvl == 1 then " is: " else "s are: ") ++
pr_enum Id.print mvl ++ str").")))
let meta_with_name evd id =
let na = Name id in
let fold (l1, l2 as l) (n, clb) =
let (na',def) = match clb with
| Cltyp (na, _) -> (na, false)
| Clval (na, _, _) -> (na, true)
in
if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2)
else l
in
let (mvl, mvnodef) = List.fold_left fold ([], []) (Evd.meta_list evd) in
match mvnodef, mvl with
| _,[] ->
explain_no_such_bound_variable evd id
| ([n],_|_,[n]) ->
n
| _ ->
user_err ~hdr:"Evd.meta_with_name"
(str "Binder name \"" ++ Id.print id ++
strbrk "\" occurs more than once in clause.")
let meta_of_binder clause loc mvs = function
| NamedHyp s -> meta_with_name clause.evd s
| AnonHyp n ->
try List.nth mvs (n-1)
with (Failure _|Invalid_argument _) ->
user_err (str "No such binder.")
let error_already_defined b =
match b with
| NamedHyp id ->
user_err
(str "Binder name \"" ++ Id.print id ++
str"\" already defined with incompatible value.")
| AnonHyp n ->
anomaly
(str "Position " ++ int n ++ str" already defined.")
let clenv_unify_binding_type clenv c t u =
if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd u))) then
CoerceToType, clenv, c
else
try
let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
TypeProcessed, { clenv with evd = evd }, c
with
| PretypeError (_,_,ActualTypeNotCoercible (_,_,
(NotClean _ | ConversionFailed _))) as e ->
raise e
| e when precatchable_exception e ->
TypeNotProcessed, clenv, c
let clenv_assign_binding clenv k c =
let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in
let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
update_clenv_evd clenv' (meta_assign k (c,(Conv,status)) clenv'.evd)
let clenv_match_args bl clenv =
if List.is_empty bl then
clenv
else
let mvs = clenv_independent clenv in
check_bindings bl;
List.fold_left
(fun clenv {CAst.loc;v=(b,c)} ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
if EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv
else error_already_defined b
else
clenv_assign_binding clenv k c)
clenv bl
exception NoSuchBinding
let clenv_constrain_last_binding c clenv =
let all_mvs = collect_metas clenv.evd clenv.templval.rebus in
let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in
clenv_assign_binding clenv k c
let error_not_right_number_missing_arguments n =
user_err
(strbrk "Not the right number of missing arguments (expected " ++
int n ++ str ").")
let clenv_constrain_dep_args hyps_only bl clenv =
if List.is_empty bl then
clenv
else
let occlist = clenv_dependent_gen hyps_only clenv in
if Int.equal (List.length occlist) (List.length bl) then
List.fold_left2 clenv_assign_binding clenv occlist bl
else
if hyps_only then
let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in
if Int.equal (List.length occlist') (List.length bl) then
List.fold_left2 clenv_assign_binding clenv occlist' bl
else
error_not_right_number_missing_arguments (List.length occlist)
else
error_not_right_number_missing_arguments (List.length occlist)
let clenv_cast_meta clenv =
let rec crec u =
match EConstr.kind clenv.evd u with
| App _ | Case _ -> crec_hd u
| Cast (c,_,_) when isMeta clenv.evd c -> u
| Proj (p, c) -> mkProj (p, crec_hd c)
| _ -> EConstr.map clenv.evd crec u
and crec_hd u =
match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with
| Meta mv ->
(try
let b = Typing.meta_type clenv.env clenv.evd mv in
assert (not (occur_meta clenv.evd b));
if occur_meta clenv.evd b then u
else mkCast (mkMeta mv, DEFAULTcast, b)
with Not_found -> u)
| App(f,args) -> mkApp (crec_hd f, Array.map crec args)
| Case(ci,u,pms,p,iv,c,br) ->
mkCase (ci, u, pms, p, iv, crec_hd c, br)
| Proj (p, c) -> mkProj (p, crec_hd c)
| _ -> u
in
crec
let clenv_pose_dependent_evars ?(with_evars=false) clenv =
let dep_mvs = clenv_dependent clenv in
let env, sigma = clenv.env, clenv.evd in
if not (List.is_empty dep_mvs) && not with_evars then
raise
(RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
clenv_pose_metas_as_evars clenv dep_mvs
let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
Proofview.Goal.enter begin fun gl ->
let clenv = clenv_pose_dependent_evars ~with_evars clenv in
let evd' =
if with_classes then
let evd' =
Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
~fail:(not with_evars) clenv.env clenv.evd
in
Typeclasses.make_unresolvables (fun x -> true) evd'
else clenv.evd
in
let clenv = update_clenv_evd clenv evd' in
Proofview.tclTHEN
(Proofview.Unsafe.tclEVARS (Evd.clear_metas evd'))
(refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv))))
end
open Unification
let dft = default_unify_flags
let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv =
Proofview.Goal.enter begin fun gl ->
let clenv = clenv_unique_resolver ~flags clenv gl in
clenv_refine ?with_evars ~with_classes clenv
end
let fail_quick_core_unif_flags = {
modulo_conv_on_closed_terms = Some TransparentState.full;
use_metas_eagerly_in_conv_on_closed_terms = false;
use_evars_eagerly_in_conv_on_closed_terms = false;
modulo_delta = TransparentState.empty;
modulo_delta_types = TransparentState.full;
check_applied_meta_types = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
allowed_evars = Evarsolve.AllowedEvars.all;
restrict_conv_on_strict_subterms = false;
modulo_betaiota = false;
modulo_eta = true;
}
let fail_quick_unif_flags = {
core_unify_flags = fail_quick_core_unif_flags;
merge_unify_flags = fail_quick_core_unif_flags;
subterm_unify_flags = fail_quick_core_unif_flags;
allow_K_in_toplevel_higher_order_unification = false;
resolve_evars = false
}
let unify ?(flags=fail_quick_unif_flags) m =
Proofview.Goal.enter begin fun gl ->
let env = Tacmach.New.pf_env gl in
let n = Tacmach.New.pf_concl gl in
let evd = clear_metas (Tacmach.New.project gl) in
try
let evd' = w_unify env evd CONV ~flags m n in
Proofview.Unsafe.tclEVARSADVANCE evd'
with e when CErrors.noncritical e ->
let info = Exninfo.reify () in
Proofview.tclZERO ~info e
end
let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
| ImplicitBindings largs ->
let clause = mk_clenv_from_env env sigma n (c,t) in
clenv_constrain_dep_args hyps_only largs clause
| ExplicitBindings lbind ->
let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
let clause = mk_clenv_from_env env sigma n
(c, t)
in clenv_match_args lbind clause
| NoBindings ->
mk_clenv_from_env env sigma n (c,t)
let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma
let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
let pr_clenv clenv =
h
(str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++
str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++
pr_evar_map (Some 2) clenv.env clenv.evd)
(** Evar version of mk_clenv *)
type hole = {
hole_evar : EConstr.constr;
hole_type : EConstr.types;
hole_deps : bool;
hole_name : Name.t;
}
type clause = {
cl_holes : hole list;
cl_concl : EConstr.types;
}
let make_evar_clause env sigma ?len t =
let open EConstr in
let open Vars in
let bound = match len with
| None -> -1
| Some n -> assert (0 <= n); n
in
let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
let rec clrec (sigma, holes) inst n t =
if n = 0 then (sigma, holes, t)
else match EConstr.kind sigma t with
| Cast (t, _, _) -> clrec (sigma, holes) inst n t
| Prod (na, t1, t2) ->
let inst, ctx, args, subst = match inst with
| None ->
let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in
Some (ctx, args, subst), ctx, args, subst
| Some (ctx, args, subst) -> inst, ctx, args, subst
in
let (sigma, ev) = new_pure_evar ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) in
let ev = mkEvar (ev, args) in
let dep = not (noccurn sigma 1 t2) in
let hole = {
hole_evar = ev;
hole_type = t1;
hole_deps = dep;
hole_name = na.binder_name;
} in
let t2 = if dep then subst1 ev t2 else t2 in
clrec (sigma, hole :: holes) inst (pred n) t2
| LetIn (na, b, _, t) -> clrec (sigma, holes) inst n (subst1 b t)
| _ -> (sigma, holes, t)
in
let (sigma, holes, t) = clrec (sigma, []) None bound t in
let holes = List.rev holes in
let clause = { cl_concl = t; cl_holes = holes } in
(sigma, clause)
let explain_no_such_bound_variable holes id =
let fold h accu = match h.hole_name with
| Anonymous -> accu
| Name id -> id :: accu
in
let mvl = List.fold_right fold holes [] in
let expl = match mvl with
| [] -> str " (no bound variables at all in the expression)."
| [id] -> str "(possible name is: " ++ Id.print id ++ str ")."
| _ -> str "(possible names are: " ++ pr_enum Id.print mvl ++ str ")."
in
user_err (str "No such bound variable " ++ Id.print id ++ expl)
let evar_with_name holes id =
let map h = match h.hole_name with
| Anonymous -> None
| Name id' -> if Id.equal id id' then Some h else None
in
let hole = List.map_filter map holes in
match hole with
| [] -> explain_no_such_bound_variable holes id
| [h] -> h.hole_evar
| _ ->
user_err
(str "Binder name \"" ++ Id.print id ++
str "\" occurs more than once in clause.")
let evar_of_binder holes = function
| NamedHyp s -> evar_with_name holes s
| AnonHyp n ->
try
let nondeps = List.filter (fun hole -> not hole.hole_deps) holes in
let h = List.nth nondeps (pred n) in
h.hole_evar
with e when CErrors.noncritical e ->
user_err (str "No such binder.")
let define_with_type sigma env ev c =
let open EConstr in
let t = Retyping.get_type_of env sigma ev in
let ty = Retyping.get_type_of env sigma c in
let j = Environ.make_judge c ty in
let (sigma, j, _trace) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in
let (ev, _) = destEvar sigma ev in
let sigma = Evd.define ev j.Environ.uj_val sigma in
sigma
let solve_evar_clause env sigma hyp_only clause = function
| NoBindings -> sigma
| ImplicitBindings largs ->
let open EConstr in
let fold holes h =
if h.hole_deps then
let (ev, _) = destEvar sigma h.hole_evar in
let is_dep hole = occur_evar sigma ev hole.hole_type in
let in_hyp = List.exists is_dep holes in
let in_ccl = occur_evar sigma ev clause.cl_concl in
let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in
let h = { h with hole_deps = dep } in
h :: holes
else
h :: holes
in
let holes = List.fold_left fold [] (List.rev clause.cl_holes) in
let map h = if h.hole_deps then Some h.hole_evar else None in
let evs = List.map_filter map holes in
let len = List.length evs in
if Int.equal len (List.length largs) then
let fold sigma ev arg = define_with_type sigma env ev arg in
let sigma = List.fold_left2 fold sigma evs largs in
sigma
else
error_not_right_number_missing_arguments len
| ExplicitBindings lbind ->
let () = check_bindings lbind in
let fold sigma {CAst.v=(binder, c)} =
let ev = evar_of_binder clause.cl_holes binder in
define_with_type sigma env ev c
in
let sigma = List.fold_left fold sigma lbind in
sigma