[m-rev.] for pre-commit review: add nondet_member/2
Julien Fischer
jfischer at opturion.com
Sun Mar 2 13:53:17 AEDT 2025
For pre-commit review:
In particular, I am looking for opinions on the first two issues below.
1. Should the new predicate be called nondet_member/2 (as per ranges.m)
or one_member/2 (as per set_ctree234)?
2. On backtracking the (out, in) mode of set_unordlist.member/2 (and
consequently nondet_member/2) returns all of the elements in the
representation of the set including duplicates. I think we should
sort and remove duplicates here as we do for other operations on this
type of set (e.g. folds).
3. Test coverage of many of the set modules in the test suite is quite
sparse, indeed non-existent in a number of cases.
---------------------------------------------------
Add nondet_member/2 to set and list modules.
This is a synonym for the (out, in) is nondet mode of member/2, but with the
arguments in an order that is more conducive to higher-order programming.
library/diet.m:
library/fatter_sparse_bitset.m:
library/list.m:
library/one_or_more.m:
library/set.m:
library/set_bbbtree.m:
library/set_ctree234.m:
library/set_ordlist.m:
library/set_tree234.m:
library/set_unordlist.m:
library/sparse_bitset.m:
library/tree_bitset.m:
Julien.
diff --git a/library/diet.m b/library/diet.m
index fae707e..fd41483 100644
--- a/library/diet.m
+++ b/library/diet.m
@@ -94,6 +94,13 @@
%
:- pred contains(diet(T)::in, T::in) is semidet <= diet_element(T).
+ % nondet_member(Set, X):
+ %
+ % Nondeterministically produce each element in Set.
+ % Each time this call succeeds, X will be bound to an element in Set.
+ %
+:- pred nondet_member(diet(T)::in, T::out) is nondet <= diet_element(T).
+
%---------------------------------------------------------------------------%
%
% Insertions and deletions.
@@ -798,6 +805,9 @@ contains(T, Z) :-
true
).
+nondet_member(Set, Elem) :-
+ member(Elem, Set).
+
%---------------------------------------------------------------------------%
insert(Set0, Elem) = Set :-
diff --git a/library/fat_sparse_bitset.m b/library/fat_sparse_bitset.m
index 9c414bd..88f52c2 100644
--- a/library/fat_sparse_bitset.m
+++ b/library/fat_sparse_bitset.m
@@ -112,6 +112,8 @@
%
:- pred contains(fat_sparse_bitset(T)::in, T::in) is semidet <= uenum(T).
+:- pred nondet_member(fat_sparse_bitset(T)::in, T::out) is nondet <= uenum(T).
+
%---------------------------------------------------------------------------%
%
% Insertions and deletions.
@@ -685,6 +687,11 @@ contains_search_nodes(Elems, ItemOffset, ItemBitToSet) :-
contains_search_nodes(Tail, ItemOffset, ItemBitToSet)
).
+%---------------------%
+
+nondet_member(Set, Item) :-
+ member(Item, Set).
+
%---------------------------------------------------------------------------%
insert(Set0, Item) = Set :-
diff --git a/library/fatter_sparse_bitset.m b/library/fatter_sparse_bitset.m
index c7aa258..ea763da 100644
--- a/library/fatter_sparse_bitset.m
+++ b/library/fatter_sparse_bitset.m
@@ -165,6 +165,9 @@
%
:- pred contains(fatter_sparse_bitset(T)::in, T::in) is semidet <= uenum(T).
+:- pred nondet_member(fatter_sparse_bitset(T)::in, T::out) is nondet
+ <= uenum(T).
+
%---------------------------------------------------------------------------%
%
% Insertions and deletions.
@@ -767,6 +770,11 @@ contains_search_nodes(Elems, ItemOffset, ItemBitToSet) :-
contains_search_nodes(Tail, ItemOffset, ItemBitToSet)
).
+%---------------------%
+
+nondet_member(Set, Item) :-
+ member(Item, Set).
+
%---------------------------------------------------------------------------%
insert(Set0, Item) = Set :-
diff --git a/library/list.m b/library/list.m
index f1a3b26..0f7e98c 100644
--- a/library/list.m
+++ b/library/list.m
@@ -237,13 +237,22 @@
% contains(List, Elem):
%
- % Equivalent to member(Elem, List).
+ % Equivalent to member(Elem, List) in the (in, in) mode.
%
% Sometimes you need the arguments in this order, because you want to
% construct a closure with only the list.
%
:- pred contains(list(T)::in, T::in) is semidet.
+ % nondet_member(List, Elem):
+ %
+ % Equivalent to member(Elem, List) in the (out, in) mode.
+ %
+ % Sometimes you need the arguments in this order, because you want to
+ % construct a closure with only the list.
+ %
+:- pred nondet_member(list(T)::in, T::out) is nondet.
+
%---------------------------------------------------------------------------%
% index*(List, Position, Elem):
@@ -2561,6 +2570,9 @@ member_indexes0_loop(X, I, [H | T], Indexes) :-
contains(List, Elem) :-
list.member(Elem, List).
+nondet_member(List, Elem) :-
+ list.member(Elem, List).
+
%---------------------------------------------------------------------------%
index0([X | Xs], N, Elem) :-
diff --git a/library/one_or_more.m b/library/one_or_more.m
index 4e5e058..5ae837e 100644
--- a/library/one_or_more.m
+++ b/library/one_or_more.m
@@ -1,7 +1,7 @@
%---------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
-% Copyright (C) 2020-2024 The Mercury team.
+% Copyright (C) 2020-2025 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%---------------------------------------------------------------------------%
%
@@ -153,6 +153,15 @@
%
:- pred contains(one_or_more(T)::in, T::in) is semidet.
+ % nondet_member(List, Elem):
+ %
+ % Equivalent to member(Elem, List) in the (out, in) mode.
+ %
+ % Sometimes you need the arguments in this order, because you want to
+ % construct a closure with only the list.
+ %
+:- pred nondet_member(one_or_more(T)::in, T::out) is multi.
+
%---------------------------------------------------------------------------%
% index*(List, Position, Elem):
@@ -1877,6 +1886,9 @@ member_indexes0(X, one_or_more(H, T), Indexes) :-
contains(one_or_more(H, T), Elem) :-
list.member(Elem, [H | T]).
+nondet_member(OoM, Elem) :-
+ member(Elem, OoM).
+
%---------------------------------------------------------------------------%
index0(one_or_more(H, T), N, Elem) :-
diff --git a/library/set.m b/library/set.m
index b32fbdd..c5735ab 100644
--- a/library/set.m
+++ b/library/set.m
@@ -2,7 +2,7 @@
% vim: ts=4 sw=4 et ft=mercury
%---------------------------------------------------------------------------%
% Copyright (C) 1994-1997, 1999-2012 The University of Melbourne.
-% Copyright (C) 2014-2016, 2018-2024 The Mercury team.
+% Copyright (C) 2014-2016, 2018-2025 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%---------------------------------------------------------------------------%
%
@@ -81,6 +81,13 @@
%
:- pred contains(set(T)::in, T::in) is semidet.
+ % nondet_member(Set, X):
+ %
+ % Nondeterministically produce each element in Set.
+ % Each time this call succeeds, X will be bound to an element in Set.
+ %
+:- pred nondet_member(set(T)::in, T::out) is nondet.
+
%---------------------------------------------------------------------------%
%
% Insertions and deletions.
@@ -665,6 +672,9 @@ is_member(X, Set, Result) :-
contains(Set, X) :-
set_ordlist.contains(Set, X).
+nondet_member(Set, X) :-
+ set_ordlist.nondet_member(Set, X).
+
%---------------------------------------------------------------------------%
insert(S1, T) = S2 :-
diff --git a/library/set_bbbtree.m b/library/set_bbbtree.m
index 152330e..f15d37a 100644
--- a/library/set_bbbtree.m
+++ b/library/set_bbbtree.m
@@ -81,6 +81,13 @@
%
:- pred contains(set_bbbtree(T)::in, T::in) is semidet.
+ % nondet_member(Set X):
+ %
+ % Nondeterministically produce each element in Set.
+ % Each time this call succeeds, X will be bound to an element in Set.
+ %
+:- pred nondet_member(set_bbbtree(T)::in, T::out) is nondet.
+
% least(Set, X) is true iff X is smaller than all the other members of Set.
%
:- pred least(set_bbbtree(T), T).
@@ -545,6 +552,9 @@ is_member(X, Set, Result) :-
contains(Set, X) :-
member(X, Set).
+nondet_member(Set, X) :-
+ member(X, Set).
+
least(tree(V, _N, L, _R), X) :-
(
% Found least element.
diff --git a/library/set_ctree234.m b/library/set_ctree234.m
index 6ce984a..85368e7 100644
--- a/library/set_ctree234.m
+++ b/library/set_ctree234.m
@@ -92,7 +92,14 @@
%
:- pred contains(set_ctree234(T)::in, T::in) is semidet.
-%---------------------------------------------------------------------------%
+ % nondet_member(Set, X):
+ %
+ % Nondeterministically produce each element in Set.
+ % Each time this call succeeds, X will be bound to an element in Set.
+ %
+:- pred nondet_member(set_ctree234(T)::in, T::out) is nondet.
+
+%--------------------------------------------------------------------------%
%
% Insertions and deletions.
%
@@ -682,6 +689,9 @@ contains(ct(_, T), E) :-
do_contains(Tree, E) :-
do_is_member(Tree, E, yes).
+nondet_member(ct(_, T), E) :-
+ do_one_member(T, E).
+
%---------------------------------------------------------------------------%
insert(E, Tin) = Tout :-
diff --git a/library/set_ordlist.m b/library/set_ordlist.m
index 8098eaa..60da39b 100644
--- a/library/set_ordlist.m
+++ b/library/set_ordlist.m
@@ -2,7 +2,7 @@
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 1996-1997,1999-2002, 2004-2006, 2008-2012 The
University of Melbourne.
-% Copyright (C) 2014-2015, 2018-2022, 2024 The Mercury team.
+% Copyright (C) 2014-2015, 2018-2022, 2024-2025 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%---------------------------------------------------------------------------%
%
@@ -80,6 +80,13 @@
%
:- pred contains(set_ordlist(T)::in, T::in) is semidet.
+ % nondet_member(Set, X):
+ %
+ % Nondeterministically produce each element in Set.
+ % Each time this call succeeds, X will be bound to an element in Set.
+ %
+:- pred nondet_member(set_ordlist(T)::in, T::out) is nondet.
+
%---------------------------------------------------------------------------%
%
% Insertions and deletions.
@@ -646,6 +653,9 @@ is_member_loop(E, [H | T], R) :-
contains(S, E) :-
member(E, S).
+nondet_member(S, E) :-
+ member(E, S).
+
%---------------------------------------------------------------------------%
insert(!.S, T) = !:S :-
diff --git a/library/set_tree234.m b/library/set_tree234.m
index 5864fd3..c7c58fc 100644
--- a/library/set_tree234.m
+++ b/library/set_tree234.m
@@ -80,6 +80,13 @@
%
:- pred contains(set_tree234(T)::in, T::in) is semidet.
+ % nondet_member(Set, X):
+ %
+ % Nondeterministically produce each element in Set.
+ % Each time this call succeeds, X will be bound to an element in Set.
+ %
+:- pred nondet_member(set_tree234(T)::in, T::out) is nondet.
+
%---------------------------------------------------------------------------%
%
% Insertions and deletions.
@@ -792,6 +799,9 @@ is_member(T, E, R) :-
contains(T, E) :-
is_member(T, E, yes).
+nondet_member(T, E) :-
+ member(E, T).
+
%---------------------------------------------------------------------------%
insert(E, Tin) = Tout :-
diff --git a/library/set_unordlist.m b/library/set_unordlist.m
index ddb6069..f31ecac 100644
--- a/library/set_unordlist.m
+++ b/library/set_unordlist.m
@@ -2,7 +2,7 @@
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 1995-1997,1999-2002, 2004-2006, 2010-2012 The
University of Melbourne.
-% Copyright (C) 2014-2015, 2018-2019, 2021-2022, 2024 The Mercury team.
+% Copyright (C) 2014-2015, 2018-2019, 2021-2022, 2024-2025 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%---------------------------------------------------------------------------%
%
@@ -81,6 +81,13 @@
%
:- pred contains(set_unordlist(T)::in, T::in) is semidet.
+ % nondet_member(Set, X):
+ %
+ % Nondeterministically produce each element in Set.
+ % Each time this call succeeds, X will be bound to an element in Set.
+ %
+:- pred nondet_member(set_unordlist(T)::in, T::out) is nondet.
+
%---------------------------------------------------------------------------%
%
% Insertions and deletions.
@@ -475,6 +482,9 @@ is_member(E, S, R) :-
contains(S, E) :-
set_unordlist.member(E, S).
+nondet_member(S, E) :-
+ set_unordlist.member(E, S).
+
%---------------------------------------------------------------------------%
insert(!.S, T) = !:S :-
diff --git a/library/sparse_bitset.m b/library/sparse_bitset.m
index da26f0a..79d3c39 100644
--- a/library/sparse_bitset.m
+++ b/library/sparse_bitset.m
@@ -127,6 +127,8 @@
%
:- pred contains(sparse_bitset(T)::in, T::in) is semidet <= uenum(T).
+:- pred nondet_member(sparse_bitset(T)::in, T::out) is nondet <= uenum(T).
+
%---------------------------------------------------------------------------%
%
% Insertions and deletions.
@@ -685,6 +687,11 @@ contains_search_nodes([Head | Tail], ItemOffset,
ItemBitToSet) :-
contains_search_nodes(Tail, ItemOffset, ItemBitToSet)
).
+%---------------------%
+
+nondet_member(Set, Item) :-
+ member(Item, Set).
+
%---------------------------------------------------------------------------%
insert(Set0, Item) = Set :-
diff --git a/library/tree_bitset.m b/library/tree_bitset.m
index 270168c..ff2c406 100644
--- a/library/tree_bitset.m
+++ b/library/tree_bitset.m
@@ -2,7 +2,7 @@
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 2006, 2009-2012 The University of Melbourne.
-% Copyright (C) 2014-2018, 2021-2022, 2024 The Mercury team.
+% Copyright (C) 2014-2018, 2021-2022, 2024-2025 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%---------------------------------------------------------------------------%
%
@@ -108,6 +108,8 @@
%
:- pred contains(tree_bitset(T)::in, T::in) is semidet <= uenum(T).
+:- pred nondet_member(tree_bitset(T)::in, T::out) is nondet <= uenum(T).
+
%---------------------------------------------------------------------------%
%
% Insertions and deletions.
@@ -1113,6 +1115,11 @@ interiorlist_contains([Head | Tail], Index) :-
interiorlist_contains(Tail, Index)
).
+%---------------------%
+
+nondet_member(Set, Elem) :-
+ member(Elem, Set).
+
%---------------------------------------------------------------------------%
insert(Set0, Elem) = Set :-
More information about the reviews
mailing list