mercury

Mercury nondet in det


In Mercury, suppose you're in a det predicate, and you want to call a nondet predicate, as follows. If there are no solutions, you want Result = []; if there's one or more, you just want the first one like Result = [FirstSolution]. The nondet predicate may have an infinite number of solutions, so you can't enumerate them all and take the first one. The closest I've come is to use do_while and just stop after the first solution, but do_while is apparently cc_multi and I don't know how to coerce it back into a det context, or even back into a multi context so I can apply solutions to it.


Solution

  • While scanning through the builtin module for something else, I came across very some clear "if you want to use cc_multi in a det context" language that led me to this solution:

    :- module nondetindet3.
    :- interface.
    :- import_module io.
    :- pred main(io::di, io::uo) is det.
    :- implementation.
    :- import_module list, string, int, solutions.
    
    :- pred numbers(int::out) is multi.
    numbers(N) :-
        ( N = 1; N = 2; N = 3; N = 4 ),
        trace [io(!IO)] (io.format("number tried: %d\n", [i(N)], !IO)).
    
    :- pred even_numbers(int::out) is nondet.
    even_numbers(N) :-
        numbers(N),
        N rem 2 = 0.
    
    :- pred first_number(int::out) is semidet.
    first_number(N) :-
        promise_equivalent_solutions [N] (
            even_numbers(N)
        ).
    
    main(!IO) :-
        ( if first_number(N1) then
            io.format("decided on: %d\n", [i(N1)], !IO)
        else true),
        ( if first_number(N2) then
            io.format("still want: %d\n", [i(N2)], !IO)
        else true),
        ( if promise_equivalent_solutions [N3] (even_numbers(N3), N3 > 2) then
            io.format("now want: %d\n", [i(N3)], !IO)
        else true).
    

    I believe the meaning there is "hey, no need to keep searching for even_numbers/1 solutions, 'cause all those other solutions are going to be no better than the first one you get."

    Output:

    number tried: 1
    number tried: 2
    decided on: 2
    number tried: 1
    number tried: 2
    still want: 2
    number tried: 1
    number tried: 2
    number tried: 3
    number tried: 4
    now want: 4