Меркурий недет в дет

Question

Предположим, что в Меркурии вы используете предикат det и хотите вызвать предикат nondet следующим образом.Если нет решений, вы хотите Result = [];если есть один или более, вы просто хотите первый как Result = [FirstSolution].Предикат nondet может иметь бесконечное количество решений, поэтому вы не можете перечислить их все и взять первое.Самое близкое, что я пришел, - это использование do_while и просто остановка после первого решения, но do_while, по-видимому, cc_multi, и я не знаю, как привести его обратно в контекст det или даже обратно.в контекст multi, чтобы я мог применить к нему solutions.

Answer 1

Почему именно вы хотите это сделать?Если вы делаете это, чтобы оптимизировать некоторый логический код, чтобы вы выполняли меньше ненужного поиска, должен быть лучший способ.Возможно, что-то с решающими типами.

В любом случае, это технически работает:

:- module nondetindet.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
:- import_module list, string, int, bool, 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.

:- initialise(set_number/0).

:- mutable(number, int, 0, ground, [untrailed]).

:- impure pred set_number is cc_multi.
set_number :-
    do_while(even_numbers, (pred(N1::in, no::out, _::in, N1::out) is det), 0, N),
    impure set_number(N).

:- func first_number = int.
:- pragma promise_pure(first_number/0).
first_number = N :- semipure get_number(N).

main(!IO) :-
    io.format("decided on: %d\n", [i(first_number)], !IO),
    io.format("still want: %d\n", [i(first_number)], !IO).

И имеет вывод:

number tried: 1
number tried: 2
decided on: 2
still want: 2