Skip to content

Commit 36f23a0

Browse files
TragicusTragicus
committed
call tc solver when failing to unify two evars
1 parent c9c5b00 commit 36f23a0

File tree

1 file changed

+25
-53
lines changed

1 file changed

+25
-53
lines changed

‎pretyping/evarconv.ml‎

Lines changed: 25 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -729,7 +729,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
729729
in
730730
(* Checks whether two terms with the same head unify (without unfolding) *)
731731
let eq_head appr1 appr2 evd =
732-
let () = debug_unification (fun () -> Pp.(v 0 (str "compare heads" ++ cut ()))) in
733732
(* Gather the universe constraints that would make term1 and term2 equal.
734733
If these only involve unifications of flexible universes to other universes,
735734
allow this identification (first-order unification of universes). Otherwise
@@ -771,6 +770,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
771770
ise_and evd [
772771
check_univs (EConstr.eq_constr_universes env evd term1 term2);
773772
(fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] in
773+
let get_tc evd e =
774+
if not (Evd.is_typeclass_evar evd e) then raise Not_found else
775+
let tc_evars = Evd.get_typeclass_evars evd in
776+
let evd = Evd.set_typeclass_evars evd (Evar.Set.singleton e) in
777+
let evd = Typeclasses.resolve_typeclasses env evd in
778+
if not (Evd.is_defined evd e) then raise Not_found else
779+
let tc_evars = Evar.Set.union tc_evars (Evd.get_typeclass_evars evd) in
780+
let tc_evars = Evar.Set.filter (fun e -> not (Evd.is_defined evd e)) tc_evars in
781+
Evd.set_typeclass_evars evd tc_evars in
774782
let module Proj = struct
775783
type t =
776784
| None
@@ -797,24 +805,19 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
797805
(position_problem l2r pbty,ev,t2)
798806
in
799807
let consume_stack l2r (termF,skF) (termO,skO) evd =
800-
let () = debug_unification (fun () -> Pp.(v 0 (str "compare_stack" ++ cut ()))) in
801808
let switch f a b = if l2r then f a b else f b a in
802809
let not_only_app = Stack.not_purely_applicative skO in
803810
let r = (ise_stack2 not_only_app env evd (evar_conv_x flags)) in
804-
let () = debug_unification (fun () -> Pp.(v 0 (str "compared stacks" ++ cut ()))) in
805811
match switch r skF skO with
806812
| Some (l,r), Success i' when l2r && (not_only_app || List.is_empty l) ->
807-
let () = debug_unification (fun () -> Pp.(v 0 (str "l2r and not only app" ++ cut ()))) in
808813
(* E[?n]=E'[redex] reduces to either l[?n]=r[redex] with
809814
case/fix/proj in E' (why?) or ?n=r[redex] *)
810815
switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
811816
| Some (r,l), Success i' when not l2r && (not_only_app || List.is_empty l) ->
812-
let () = debug_unification (fun () -> Pp.(v 0 (str "r2l and not only app" ++ cut ()))) in
813817
(* E'[redex]=E[?n] reduces to either r[redex]=l[?n] with
814818
case/fix/proj in E' (why?) or r[redex]=?n *)
815819
switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r))
816820
| None, Success i' ->
817-
let () = debug_unification (fun () -> Pp.(v 0 (str "stacks are the same" ++ cut ()))) in
818821
switch (evar_conv_x flags env i' pbty) termF termO
819822
| _, (UnifFailure _ as x) -> x
820823
| Some _, _ -> UnifFailure (evd,NotSameArgSize) in
@@ -860,21 +863,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
860863
in
861864
(* Evar must be undefined since we have flushed evars *)
862865
let rec get_cs flags env sigma p1 appr1 appr2 =
863-
let () = debug_unification (fun () -> Pp.(v 0 (str "Search for CS on " ++ pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in
864866
let cs sigma =
865-
let () = debug_unification (fun () -> Pp.(v 0 (str "CS" ++ cut ()))) in
866867
try
867868
let s = check_conv_record env sigma p1 appr2 in
868869
conv_record flags env s
869870
with Not_found -> UnifFailure (sigma, NoCanonicalStructure) in
870871
let red sigma =
871-
let () = debug_unification (fun () -> Pp.(v 0 (str "red" ++ cut ()))) in
872872
let (term2, sk2) = appr2 in
873873
match flex_kind_of_term flags env sigma term2 sk2 with
874874
| Rigid -> UnifFailure (sigma, NoCanonicalStructure)
875875
| Flexible ev -> miller (lastUnfolded = Some false) ev appr2 appr1 sigma
876876
| MaybeFlexible vsk2' ->
877-
let () = debug_unification (fun () -> Pp.(v 0 (str "reducing subject" ++ cut ()))) in
878877
let appr2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env sigma vsk2' in
879878
get_cs flags env sigma p1 appr1 appr2 in
880879
ise_try sigma [eq_head appr1 appr2; cs; red] in
@@ -942,31 +941,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
942941
5. absorb arguments if purely applicative and postpone *)
943942
let switch f a b = if l2r then f a b else f b a in
944943
let eta evd =
945-
let () = debug_unification (fun () -> Pp.(v 0 (str "flex_rigid: eta" ++ cut ()))) in
946944
match EConstr.kind evd termR with
947945
| Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
948-
let () = debug_unification (fun () -> Pp.(v 0 (str "lambda" ++ cut ()))) in
949946
eta_lambda env evd false termR apprF
950947
| Construct u ->
951-
let () = debug_unification (fun () -> Pp.(v 0 (str "constructor" ++ cut ()))) in
952948
eta_constructor flags env evd u skR apprF
953949
| _ -> UnifFailure (evd,NotSameHead)
954950
in
955951
let tc evd =
956952
let (e, _) = EConstr.destEvar evd termF in
957-
if not (Evd.is_typeclass_evar evd e) then UnifFailure (evd, NotSameHead) else
958-
let tc_evars = Evd.get_typeclass_evars evd in
959-
let evd = Evd.set_typeclass_evars evd (Evar.Set.singleton e) in
960-
match Typeclasses.resolve_typeclasses env evd with
961-
| exception _ ->
962-
let () = debug_unification (fun () -> Pp.(v 0 (str "tc solver exploded" ++ cut ()))) in
963-
UnifFailure (evd, NotSameHead)
964-
| evd ->
965-
if not (Evd.is_defined evd e) then UnifFailure (evd, NotSameHead) else
966-
let tc_evars = Evar.Set.union tc_evars (Evd.get_typeclass_evars evd) in
967-
let tc_evars = Evar.Set.filter (fun e -> not (Evd.is_defined evd e)) tc_evars in
968-
let evd = Evd.set_typeclass_evars evd tc_evars in
969-
evar_eqappr_x flags env evd pbty keys lastUnfolded (whd_nored_state env evd apprF) apprR in
953+
try let evd = get_tc evd e in
954+
evar_eqappr_x flags env evd pbty hds lastUnfolded (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd apprF) apprR
955+
with _ -> quick_fail evd in
970956
match Stack.list_of_app_stack skF with
971957
| None ->
972958
ise_try evd [consume_stack l2r apprF apprR; eta; tc]
@@ -1055,8 +1041,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
10551041
| _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.")
10561042
in
10571043
let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
1058-
let () = debug_unification (fun () -> Pp.(v 0 (str "main loop " ++ pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut () ++ str "last reduction was " ++ str (match lastUnfolded with None -> "none" | Some true -> "RHS" | _ -> "LHS") ++ cut() ))) in
1059-
match (match (flex_kind_of_term flags env evd term1 sk1,
1044+
let () = debug_unification (fun () -> Pp.(v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in
1045+
match (flex_kind_of_term flags env evd term1 sk1,
10601046
flex_kind_of_term flags env evd term2 sk2) with
10611047
| Flexible (sp1,al1), Flexible (sp2,al2) ->
10621048
(* Notations:
@@ -1096,8 +1082,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
10961082
match consume true appr1 appr2 i with
10971083
| Success _ as x -> x
10981084
| UnifFailure _ -> quick_fail i
1085+
and f6 i =
1086+
try let evd = get_tc evd sp2 in
1087+
evar_eqappr_x flags env evd pbty hds lastUnfolded appr1 (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr2)
1088+
with _ -> try
1089+
let evd = get_tc evd sp1 in
1090+
evar_eqappr_x flags env evd pbty hds lastUnfolded (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr1) appr2
1091+
with _ -> quick_fail i
10991092
in
1100-
ise_try evd [f1; f2; f3; f4; f5]
1093+
ise_try evd [f1; f2; f3; f4; f5; f6]
11011094

11021095
| Flexible ev1, MaybeFlexible v2 ->
11031096
flex_maybeflex true ev1 appr1 appr2 v2
@@ -1128,10 +1121,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
11281121
ise_try evd [f1; f2]
11291122

11301123
| _, Lambda _ when sk2 <> [] && not (EConstr.isLambda evd term1) ->
1131-
evar_eqappr_x flags env evd pbty keys None appr1
1124+
evar_eqappr_x flags env evd pbty hds None appr1
11321125
(whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr2)
11331126
| Lambda _, _ when sk1 <> [] && not (EConstr.isLambda evd term2) ->
1134-
evar_eqappr_x flags env evd pbty keys None
1127+
evar_eqappr_x flags env evd pbty hds None
11351128
(whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd appr1)
11361129
appr2
11371130

@@ -1140,7 +1133,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
11401133
let p2 = match get_proj_case appr2 with Proj.CS _ when lastUnfolded = Some false -> Proj.None | p -> p in
11411134
(match p1, p2 with
11421135
| Proj.CS p1, Proj.CS p2 when flags.with_cs ->
1143-
let () = debug_unification (fun () -> Pp.(v 0 (str "both sides are CS" ++ cut ()))) in
11441136
ise_try evd [
11451137
(fun i -> get_cs flags env i p1 appr1 (snd hds));
11461138
(fun i -> get_cs flags env i p2 appr2 (fst hds));
@@ -1151,48 +1143,36 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
11511143
(whd_betaiota_deltazeta_for_iota_state
11521144
flags.open_ts env evd vsk2'))]
11531145
| Proj.CS p1, _ when flags.with_cs ->
1154-
let () = debug_unification (fun () -> Pp.(v 0 (str "LHS is CS" ++ cut ()))) in
11551146
ise_try evd [
11561147
(fun i ->
1157-
let () = debug_unification (fun () -> Pp.(v 0 (str "getting CS" ++ cut ()))) in
11581148
let r = get_cs flags env i p1 appr1 (snd hds) in
1159-
let () = debug_unification (fun () -> Pp.(v 0 (str (match r with UnifFailure(_, _) -> "failed to get" | _ -> "got") ++ str " CS" ++ cut ()))) in
11601149
r);
11611150
(fun i ->
1162-
let () = debug_unification (fun () -> Pp.(v 0 (str "reducing LHS" ++ cut ()))) in
11631151
evar_eqappr_x flags env evd pbty hds (Some false)
11641152
(whd_betaiota_deltazeta_for_iota_state
11651153
flags.open_ts env evd vsk1')
11661154
appr2)]
11671155
| _, Proj.CS p2 when flags.with_cs ->
1168-
let () = debug_unification (fun () -> Pp.(v 0 (str "RHS is CS" ++ cut ()))) in
11691156
ise_try evd [
11701157
(fun i ->
1171-
let () = debug_unification (fun () -> Pp.(v 0 (str "getting CS" ++ cut ()))) in
11721158
let r = get_cs flags env i p2 appr2 (fst hds) in
1173-
let () = debug_unification (fun () -> Pp.(v 0 (str (match r with UnifFailure(_, _) -> "failed to get" | _ -> "got") ++ str " CS" ++ cut ()))) in
11741159
r);
11751160
(fun i ->
1176-
let () = debug_unification (fun () -> Pp.(v 0 (str "reducing RHS" ++ cut ()))) in
11771161
evar_eqappr_x flags env evd pbty hds (Some true) appr1
11781162
(whd_betaiota_deltazeta_for_iota_state
11791163
flags.open_ts env evd vsk2'))]
11801164
| _, _ -> (match p1, p2 with
11811165
| Proj.Reducible n1, Proj.Reducible n2 ->
1182-
let () = debug_unification (fun () -> Pp.(v 0 (str "both sides are reducible" ++ cut ()))) in
11831166
let appr1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd vsk1' in
11841167
let appr2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd vsk2' in
11851168
evar_eqappr_x flags env evd pbty (if n1 = n2 then (appr1, appr2) else hds) None appr1 appr2
11861169
| Proj.Reducible n1, _ ->
1187-
let () = debug_unification (fun () -> Pp.(v 0 (str "LHS is reducible" ++ cut ()))) in
11881170
let appr1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd vsk1' in
11891171
evar_eqappr_x flags env evd pbty hds (Some false) appr1 appr2
11901172
| _, Proj.Reducible n2 ->
1191-
let () = debug_unification (fun () -> Pp.(v 0 (str "RHS is reducible" ++ cut ()))) in
11921173
let appr2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd vsk2' in
11931174
evar_eqappr_x flags env evd pbty hds (Some true) appr1 appr2
11941175
| _, _ ->
1195-
let () = debug_unification (fun () -> Pp.(v 0 (str "no proj or stuck" ++ cut ()))) in
11961176
(* We remember if the LHS is a reducible projection to decide if we unfold left first. *)
11971177
let f1 i = eq_head appr1 appr2 i
11981178
and f2 i =
@@ -1257,7 +1237,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
12571237
else
12581238
(match get_proj_case appr1 with
12591239
| Proj.CS p1 ->
1260-
let () = debug_unification (fun () -> Pp.(v 0 (str "CS with rigid RHS" ++ cut ()))) in
12611240
get_cs flags env evd p1 appr1 (snd hds)
12621241
| _ -> quick_fail i)
12631242
and f4 i =
@@ -1274,7 +1253,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
12741253
else
12751254
(match get_proj_case appr2 with
12761255
| Proj.CS p2 ->
1277-
let () = debug_unification (fun () -> Pp.(v 0 (str "CS with rigid LHS" ++ cut ()))) in
12781256
get_cs flags env evd p2 appr2 (fst hds)
12791257
| _ -> quick_fail i)
12801258
and f4 i =
@@ -1420,13 +1398,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
14201398
| Proj _, _ -> UnifFailure (evd,NotSameHead)
14211399
| (App _ | Cast _), _ -> assert false
14221400
| LetIn _, _ -> assert false
1423-
end) with
1424-
| exception e ->
1425-
let () = debug_unification (fun () -> Pp.(v 0 (str "evar_eqappr_x exploded" ++ cut ()))) in
1426-
raise e
1427-
| r ->
1428-
let () = debug_unification (fun () -> Pp.(v 0 (str "evar_eqappr_x " ++ str (match r with UnifFailure(_, _) -> "failed" | _ -> "succeeded") ++ cut ()))) in
1429-
r
1401+
end
14301402

14311403
and conv_record flags env (evd,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) =
14321404
(* Tries to unify the states

0 commit comments

Comments
 (0)