aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarsolve.ml11
-rw-r--r--pretyping/evd.ml21
-rw-r--r--pretyping/evd.mli13
-rw-r--r--pretyping/unification.ml8
5 files changed, 40 insertions, 21 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c436fed2c..f8e959075 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -830,7 +830,7 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) =
let choose_less_dependent_instance evk evd term args =
let evi = Evd.find_undefined evd evk in
let subst = make_pure_subst evi args in
- let subst' = List.filter (fun (id,c) -> eq_constr evd c term) subst in
+ let subst' = List.filter (fun (id,c) -> Term.eq_constr c term) subst in
match subst' with
| [] -> None
| (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
@@ -840,7 +840,7 @@ let apply_on_subterm evdref f c t =
(* By using eq_constr, we make an approximation, for instance, we *)
(* could also be interested in finding a term u convertible to t *)
(* such that c occurs in u *)
- if eq_constr !evdref c t then f k
+ if e_eq_constr evdref c t then f k
else
match kind_of_term t with
| Evar (evk,args) when Evd.is_undefined !evdref evk ->
@@ -1002,7 +1002,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let app_empty = Array.is_empty l1 && Array.is_empty l2 in
match kind_of_term term1, kind_of_term term2 with
| Evar (evk1,args1), (Rel _|Var _) when app_empty
- && List.for_all (fun a -> eq_constr evd a term2 || isEvar a)
+ && List.for_all (fun a -> Term.eq_constr a term2 || isEvar a)
(remove_instance_local_defs evd evk1 args1) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
@@ -1010,7 +1010,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
| Some evd -> Success evd
| None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
| (Rel _|Var _), Evar (evk2,args2) when app_empty
- && List.for_all (fun a -> eq_constr evd a term1 || isEvar a)
+ && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a)
(remove_instance_local_defs evd evk2 args2) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4bffe3d1f..ba877d35c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -495,7 +495,7 @@ let make_projectable_subst aliases sigma evi args =
| 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 sigma a c) sub then
+ if List.exists (fun (c,_,_) -> Term.eq_constr a c) sub then
(rest,all,cstrs)
else
(rest,
@@ -648,15 +648,15 @@ 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 sigma y c' then id
+ if Term.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 sigma yc cc -> id
- | _ -> if eq_constr sigma yc c then id else raise Not_found
+ | Some cc when Term.eq_constr yc cc -> id
+ | _ -> if Term.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
@@ -1172,7 +1172,8 @@ type conv_fun_bool =
* depend on these args). *)
let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
- if Array.equal (eq_constr evd) argsv1 argsv2 then evd else
+ let evdref = ref evd in
+ if Array.equal (e_eq_constr evdref) argsv1 argsv2 then !evdref else
(* Filter and restrict if needed *)
let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
let untypedfilter =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index bd105c728..e49ed7b45 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1333,24 +1333,35 @@ let test_conversion env d pb t u =
try conversion_gen env d pb t u; true
with _ -> false
-let eq_constr d t u =
- Term.eq_constr_univs d.universes.uctx_universes t u
+let eq_constr evd t u =
+ let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
+ if b then
+ try let evd' = add_universe_constraints evd c in evd', b
+ with Univ.UniverseInconsistency _ -> evd, false
+ else evd, b
+
+let e_eq_constr evdref t u =
+ let evd, b = eq_constr !evdref t u in
+ evdref := evd; b
+
+let eq_constr_test evd t u =
+ snd (eq_constr evd t u)
let eq_named_context_val d ctx1 ctx2 =
ctx1 == ctx2 ||
let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
- Id.equal i1 i2 && Option.equal (eq_constr d) c1 c2 && (eq_constr d) t1 t2
+ Id.equal i1 i2 && Option.equal (eq_constr_test d) c1 c2 && (eq_constr_test d) t1 t2
in List.equal eq_named_declaration c1 c2
let eq_evar_body d b1 b2 = match b1, b2 with
| Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr d t1 t2
+| Evar_defined t1, Evar_defined t2 -> eq_constr_test d t1 t2
| _ -> false
let eq_evar_info d ei1 ei2 =
ei1 == ei2 ||
- eq_constr d ei1.evar_concl ei2.evar_concl &&
+ eq_constr_test d ei1.evar_concl ei2.evar_concl &&
eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
eq_evar_body d ei1.evar_body ei2.evar_body
(** ppedrot: [eq_constr] may be a bit too permissive here *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index d0a47fe96..b284bd42c 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -515,11 +515,18 @@ val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map ->
val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
-(** This one forgets about the assignemts of universes. *)
val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
+(** This one forgets about the assignemts of universes. *)
+
+val eq_constr : evar_map -> constr -> constr -> evar_map * bool
+(** Syntactic equality up to universes, recording the associated constraints *)
+
+val e_eq_constr : evar_map ref -> constr -> constr -> bool
+(** Syntactic equality up to universes. *)
-(** Syntactic equality up to universe constraints. *)
-val eq_constr : evar_map -> constr -> constr -> bool
+val eq_constr_test : evar_map -> constr -> constr -> bool
+(** Syntactic equality up to universes, throwing away the (consistent) constraints
+ in case of success. *)
(********************************************************************
constr with holes *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7530ced7c..7b302229b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -717,11 +717,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
and reduce curenvnb pb b wt (sigma, metas, evars as substn) cM cN =
if use_full_betaiota flags && not (subterm_restriction b flags) then
let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
- if not (eq_constr sigma cM cM') then
+ if not (Term.eq_constr cM cM') then
unirec_rec curenvnb pb b wt substn cM' cN
else
let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in
- if not (eq_constr sigma cN cN') then
+ if not (Term.eq_constr cN cN') then
unirec_rec curenvnb pb b wt substn cM cN'
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1500,7 +1500,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
let return a b =
let (evd,c as a) = a () in
- if List.exists (fun (evd',c') -> eq_constr evd' c c') b then b else a :: b
+ if List.exists (fun (evd',c') -> Term.eq_constr c c') b then b else a :: b
in
let fail str _ = error str in
let bind f g a =
@@ -1577,7 +1577,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
in
if not flags.allow_K_in_toplevel_higher_order_unification &&
(* ensure we found a different instance *)
- List.exists (fun op -> eq_constr evd op cl) l
+ List.exists (fun op -> Term.eq_constr op cl) l
then error_non_linear_unification env evd hdmeta cl
else (evd',cl::l)
else if flags.allow_K_in_toplevel_higher_order_unification
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 00:52:52 +0000