aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-23 15:52:48 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-06-23 15:52:48 +0200
commitddd99ca6b4a23286405ec995379e4b07d42b0f78 (patch)
treee2e328b78d9fca7383973bf46014410ea08bac4f /engine
parent38b180984b09840e0b1023cc441917acc77dd438 (diff)
parent994f869496b3edd76a903cac16b13e8b6f247d63 (diff)
Merge PR #7827: [engine] safe [add_unification_pb] interface
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.ml15
-rw-r--r--engine/evarutil.mli8
-rw-r--r--engine/evd.ml3
-rw-r--r--engine/evd.mli4
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 f56f9662d..714a0b645 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 405fcc403..d166fd804 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) ->