diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 19:53:51 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-10 18:11:02 -0400 |
| commit | 39c4f9030f3aefdb7581aa02dd4b0c0d1ef89ee5 (patch) | |
| tree | 9489b19632ba418a6dd9ef047543851eb069ebd4 /kernel/safe_typing.ml | |
| parent | 91171386f55a2d423d831a1ce96f9d621a5be141 (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.ml | 3 |
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 = |
