[m-rev.] for review: Modify solutions module for stricter mode checking.
Peter Wang
novalazy at gmail.com
Mon Aug 18 16:06:36 AEST 2014
library/solutions.m:
Fix mode error in `solutions' predicate in the `multi' mode.
Convince the compiler with a run-time check that the solution
list will be non-empty.
Similarly for `builtin_solutions'.
---
library/solutions.m | 39 +++++++++++++++++++++++++++++++++------
1 file changed, 33 insertions(+), 6 deletions(-)
diff --git a/library/solutions.m b/library/solutions.m
index 0098702..bc5ff2f 100644
--- a/library/solutions.m
+++ b/library/solutions.m
@@ -48,7 +48,8 @@
:- pred unsorted_solutions(pred(T), list(T)).
:- mode unsorted_solutions(pred(out) is multi, out(non_empty_list))
is cc_multi.
-:- mode unsorted_solutions(pred(out) is nondet, out) is cc_multi.
+:- mode unsorted_solutions(pred(out) is nondet, out)
+ is cc_multi.
:- func aggregate(pred(T), func(T, U) = U, U) = U.
:- mode aggregate(pred(out) is multi, func(in, in) = out is det, in)
@@ -197,6 +198,7 @@
:- implementation.
:- import_module mutvar.
+:- import_module require.
%-----------------------------------------------------------------------------%
@@ -208,7 +210,8 @@
solutions(Pred, List) :-
builtin_solutions(Pred, UnsortedList),
- list.sort_and_remove_dups(UnsortedList, List).
+ list.sort_and_remove_dups(UnsortedList, List0),
+ assert_num_solutions(Pred, List0, List).
solutions(P) = S :-
solutions(P, S).
@@ -222,7 +225,9 @@ solutions_set(Pred, Set) :-
unsorted_solutions(Pred, List) :-
builtin_solutions(Pred, UnsortedList),
- cc_multi_equal(UnsortedList, List).
+ ( List = UnsortedList
+ ; List = UnsortedList
+ ).
aggregate(P, F, Acc0) = Acc :-
aggregate(P, (pred(X::in, A0::in, A::out) is det :- A = F(X, A0)),
@@ -248,11 +253,33 @@ unsorted_aggregate2(Generator, Accumulator, !Acc1, !Acc2) :-
%-----------------------------------------------------------------------------%
:- pred builtin_solutions(pred(T), list(T)).
-:- mode builtin_solutions(pred(out) is multi, out) is det. % really cc_multi
-:- mode builtin_solutions(pred(out) is nondet, out) is det. % really cc_multi
+:- mode builtin_solutions(pred(out) is multi, out(non_empty_list))
+ is det. % really cc_multi
+:- mode builtin_solutions(pred(out) is nondet, out)
+ is det. % really cc_multi
builtin_solutions(Generator, UnsortedList) :-
- builtin_aggregate(Generator, list.cons, [], UnsortedList).
+ builtin_aggregate(Generator, list.cons, [], UnsortedList0),
+ assert_num_solutions(Generator, UnsortedList0, UnsortedList).
+
+:- pred assert_num_solutions(pred(T), list(T), list(T)).
+:- mode assert_num_solutions(pred(out) is multi,
+ in, out(non_empty_list)) is det.
+:- mode assert_num_solutions(pred(out) is nondet,
+ in, out) is det.
+
+:- pragma promise_equivalent_clauses(assert_num_solutions/3).
+
+assert_num_solutions(_Pred::pred(out) is multi,
+ List0::in, List::out(non_empty_list)) :-
+ (
+ List0 = [],
+ unexpected($module, $pred, "no solutions")
+ ;
+ List0 = [_ | _],
+ List = List0
+ ).
+assert_num_solutions(_Pred::pred(out) is nondet, List::in, List::out).
%-----------------------------------------------------------------------------%
%
--
1.8.4
More information about the reviews
mailing list