Thanks, Ian for your explanation<div> </div><div><div>Now I indeed see the difference.<img src="cid:330@goomoji.gmail" style="margin-top: 0px; margin-right: 0.2ex; margin-bottom: 0px; margin-left: 0.2ex; vertical-align: middle; " goomoji="330"></div> <div> </div><div> </div><div>On Mon, May 17, 2010 at 4:20 AM, Ian MacLarty <<a href="mailto:maclarty@csse.unimelb.edu.au">maclarty@csse.unimelb.edu.au</a>> wrote:</div><div><div class="gmail_quote"> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div><div></div><div class="h5">On Sun, May 16, 2010 at 11:46 PM, Vladimir Gubarkov <<a href="mailto:xonixx@gmail.com">xonixx@gmail.com</a>> wrote: > Hi Dear sirs > > let's look at code > > > :- module tst2. > > :- interface. > > :- import_module io. > > :- pred main(io, io). > :- mode main(di, uo) is det. > > :- implementation. > > > :- import_module solutions, list, int. > > main --> > { > promise_equivalent_solutions [L] unsorted_solutions((pred(E::out) is > nondet :- > member(E, 1..20), > E mod 3 = 0 > ), L) > }, > print(L). > > > Note, that without "promise_equivalent_solutions [L]" it gives > > > $ mmc tst2 > tst2.m:008: In `main'(di, uo): > tst2.m:008: error: determinism declaration not satisfied. > tst2.m:008: Declared `det', inferred `multi'. > tst2.m:017: call to `solutions.unsorted_solutions'((pred(out) is nondet), > tst2.m:017: out) can succeed more than once. > tst2.m:017: Error: call to predicate `solutions.unsorted_solutions'/2 with > tst2.m:017: determinism `cc_multi' occurs in a context which requires all > tst2.m:017: solutions. > > > while compiling. > > I've read some documentation on cc_multi, and I seem to understand the > meaning of cc_multi. It's used when we defining predicate as being multi, > but using it in place where we nead only 1 solution (actually, anyone.. this > is determined by compiler what solution to return taking in mind > optimization concerns). What I can't understand is why should I explicitely > convert it to det with "promise_equivalent_solutions [L]". Why compiler is > not smart enough to make this automatically? </div></div>In general det is not the same as cc_multi, which is why the compiler doesn't infer them the same automatically. det means that there is exactly one solution to the procedure when it's inputs are bound. cc_multi means that there are one or more solutions, but we only want to pick one of them. Consider the following example: :- pred q is semidet. q :- p(X), X > 2. :- pred p(int::out) is multi. p(1). p(2). p(3). When you evaluate q it succeeds. Now say we changed the determinism of p to cc_multi and used promise_equivalent_solutions to cast it to det in the body of q: :- pred q is semidet. q :- promise_equivalent_solutions [X] p(X), X > 2. :- pred p(int::out) is cc_multi. p(1). p(2). p(3). Now q fails, even though the program logic (the declarative semantics) hasn't changed. By requiring you to add the promise_equivalent_solutions the compiler is forcing you to think about whether the solutions to p really are equivalent. In this case they aren't and the promise_equivalent_solutions is a bug. I hope that helps. Ian. -------------------------------------------------------------------------- mercury-users mailing list Post messages to: <a href="mailto:mercury-users@csse.unimelb.edu.au">mercury-users@csse.unimelb.edu.au</a> Administrative Queries: <a href="mailto:owner-mercury-users@csse.unimelb.edu.au">owner-mercury-users@csse.unimelb.edu.au</a> Subscriptions: <a href="mailto:mercury-users-request@csse.unimelb.edu.au">mercury-users-request@csse.unimelb.edu.au</a> -------------------------------------------------------------------------- </blockquote></div> </div></div>