[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