evd/evarutil: safe [add_unification_pb] interface, taking EConstr's

Avoid adding the same unification problem twice, module evar instantiation.

4 files changed, 29 insertions, 1 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 82be4791f..1625f6fc8 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -514,6 +514,21 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami
   evdref := evd';
   ev
 
+(* Safe interface to unification problems *)
+type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr
+
+let eq_unification_pb evd (pbty,env,t1,t2) (pbty',env',t1',t2') =
+  pbty == pbty' && env == env' &&
+    EConstr.eq_constr evd t1 t1' &&
+    EConstr.eq_constr evd t2 t2'
+
+let add_unification_pb ?(tail=false) pb evd =
+  let conv_pbs = Evd.conv_pbs evd in
+  if not (List.exists (eq_unification_pb evd pb) conv_pbs) then
+    let (pbty,env,t1,t2) = pb in
+    Evd.add_conv_pb ~tail (pbty,env,t1,t2) evd
+  else evd
+
 (* This assumes an evar with identity instance and generalizes it over only
    the de Bruijn part of the context *)
 let generalize_evar_over_rels sigma (ev,args) =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c17f3d168..db638be9e 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -217,6 +217,14 @@ val compare_cumulative_instances : Reduction.conv_pb -> Univ.Variance.t array ->
 val compare_constructor_instances : evar_map ->
   Univ.Instance.t -> Univ.Instance.t -> evar_map
 
+(** {6 Unification problems} *)
+type unification_pb = conv_pb * env * constr * constr
+
+(** [add_unification_pb ?tail pb sigma]
+    Add a unification problem [pb] to [sigma], if not already present.
+    Put it at the end of the list if [tail] is true, by default it is false. *)
+val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map
+
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 0c9c3a29b..2226193cb 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -621,10 +621,11 @@ let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
 let add_conv_pb ?(tail=false) pb d =
-  (** MS: we have duplicates here, why? *)
   if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
   else {d with conv_pbs = pb::d.conv_pbs}
 
+let conv_pbs d = d.conv_pbs
+
 let evar_source evk d = (find d evk).evar_source
 
 let evar_ident evk evd = EvNames.ident evk evd.evar_names
diff --git a/engine/evd.mli b/engine/evd.mli
index c40e925d8..4f2ece900 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -439,7 +439,11 @@ type clbinding =
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * econstr * econstr
+
+(** The following two functions are for internal use only,
+    see [Evarutil.add_unification_pb] for a safe interface. *)
 val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map
+val conv_pbs : evar_map -> evar_constraint list
 
 val extract_changed_conv_pbs : evar_map ->
       (Evar.Set.t -> evar_constraint -> bool) ->