aboutsummaryrefslogtreecommitdiff
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-26 19:53:51 -0400
committerEmilio Jesus Gallego Arias2020-04-10 18:11:02 -0400
commit39c4f9030f3aefdb7581aa02dd4b0c0d1ef89ee5 (patch)
tree9489b19632ba418a6dd9ef047543851eb069ebd4 /kernel/safe_typing.ml
parent91171386f55a2d423d831a1ce96f9d621a5be141 (diff)
[sideeff] Don't use polymorphic equality to check for empty side-effects
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 181ec4860c..50922ffc52 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -301,6 +301,7 @@ sig
type t
val repr : t -> side_effect list
val empty : t
+ val is_empty : t -> bool
val add : side_effect -> t -> t
val concat : t -> t -> t
end =
@@ -319,6 +320,7 @@ type t = { seff : side_effect list; elts : SeffSet.t }
let repr eff = eff.seff
let empty = { seff = []; elts = SeffSet.empty }
+let is_empty { seff; elts } = List.is_empty seff && SeffSet.is_empty elts
let add x es =
if SeffSet.mem x es.elts then es
else { seff = x :: es.seff; elts = SeffSet.add x es.elts }
@@ -349,6 +351,7 @@ let push_private_constants env eff =
List.fold_left add_if_undefined env eff
let empty_private_constants = SideEffects.empty
+let is_empty_private_constants c = SideEffects.is_empty c
let concat_private = SideEffects.concat
let universes_of_private eff =