aboutsummaryrefslogtreecommitdiffhomepage
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
parent38b180984b09840e0b1023cc441917acc77dd438 (diff)
parent994f869496b3edd76a903cac16b13e8b6f247d63 (diff)
Merge PR #7827: [engine] safe [add_unification_pb] interface
-rw-r--r--engine/evarutil.ml15
-rw-r--r--engine/evarutil.mli8
-rw-r--r--engine/evd.ml3
-rw-r--r--engine/evd.mli4
-rw-r--r--pretyping/evarconv.ml4
5 files changed, 31 insertions, 3 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) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 88a91af88..a71ef6508 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -510,7 +510,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let tM = Stack.zip evd apprM in
miller_pfenning on_left
(fun () -> if not_only_app then (* Postpone the use of an heuristic *)
- switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
+ switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
else quick_fail i)
ev lF tM i
and consume (termF,skF as apprF) (termM,skM as apprM) i =
@@ -578,7 +578,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
i,mkEvar ev
else
i,Stack.zip evd apprF in
- switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
+ switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i))
tF tR
else
UnifFailure (evd,OccurCheck (fst ev,tR)))])