ADT недвижимость в Mercury - PullRequest
Новая
       44

ADT недвижимость в Mercury

3 голосов
/ 29 июля 2010

Я странствую, почему Меркурий (10.04) не может определить детерминизм следующего фрагмента: 

:- pred load_freqs(int::in, io.res(list(float))::out, io::di, io::uo) is det.
load_freqs(CPU, ResFreqs, !IO):-
    open_input(cpu_fn(CPU, "available_frequencies"), ResStream, !IO),
    (ResStream = io.ok(Stream) ->
        ResFreqs = io.ok([])
    ;ResStream = io.error(Err),
        ResFreqs = io.error(Err)
    ).

Он жалуется: 

cpugear.m:075: In `load_freqs'(in, out, di, uo):
cpugear.m:075:   error: determinism declaration not satisfied.
cpugear.m:075:   Declared `det', inferred `semidet'.
cpugear.m:080:   Unification of `ResStream' and `io.error(Err)' can fail.
cpugear.m:076: In clause for predicate `cpugear.load_freqs'/4:
cpugear.m:076:   warning: variable `CPU' occurs only once in this scope.
cpugear.m:078: In clause for predicate `cpugear.load_freqs'/4:
cpugear.m:078:   warning: variable `Stream' occurs only once in this scope.

Но io.res имеют только io.ok/1 иio.error/1.
И следующий фрагмент кода хорошо компилируется: 

:- pred read_freqs(io.res(io.input_stream)::in, io.res(list(float))::out, io::di, io::uo) is det.
read_freqs(io.ok(Stream), io.ok([]), IO, IO).
read_freqs(io.error(Err), io.error(Err), IO, IO).

Обновление # 1 : он может решить det даже для: 

:- pred read_freqs(bool::in, io.res(io.input_stream)::in, io.res(list(float))::out, io::di, io::uo) is det.
read_freqs(no, ResStream, io.ok([]), IO, IO):- ResStream = io.ok(_).
read_freqs(F, io.ok(_), io.ok([]), IO, IO):- F = yes.
read_freqs(yes, io.error(Err), io.error(Err), IO, IO).
read_freqs(F, ResStream, io.error(Err), IO, IO):- ResStream = io.error(Err), F = no.

Ответы [ 3 ]

2 голосов
/ 07 февраля 2011

Что касается «почему».давайте посмотрим на исходный код с помощью if-then-else: 

(ResStream = io.ok(Stream) ->
    ResFreqs = io.ok([])
;ResStream = io.error(Err),
    ResFreqs = io.error(Err)
).

Если условие не выполнено, то первый конъюнкт в случае else является полуотдельным тестом.Компилятор не знает, что он должен быть успешным (что можно сделать из знания, что это условие не выполнено).Другими словами, компилятор не достаточно умен.

Тем не менее, найти эту проблему очень редко, потому что обычно условие более сложное и не позволяет сделать этот вывод, так что это не такважно, чтобы компилятор не был достаточно умен для определения правильного детерминизма.

Рекомендуется программировать с использованием переключателей, когда это возможно (например, в этом примере), это предотвращает текущую проблему и помогает гарантировать, что вы рассмотреливсе возможные случаи ResStream.Например, если в будущем io.error был повторно учтен и мог быть io.error_file_not_found или io.error_disk_full и т. Д., Компилятор дал бы указание программисту исправить их переключатель, поскольку теперь он будет неполным.

2 голосов
/ 29 июля 2010

Мое чтение правил Меркурия для детерминизма с условными обозначениями (ниже) заключается в том, что для того, чтобы это считалось детерминированным, следует заменить -> на ,

Из справочного руководства Mercury:

Если условие if-then-else не может потерпеть неудачу, если-то-еще эквивалентно соединению состояние и «тогда» часть, и ее детерминизм рассчитывается соответственно. В противном случае, if-then-else может потерпеть неудачу, если часть «тогда» или «еще» часть может потерпеть неудачу.

1 голос
/ 30 июля 2010

Хорошо, это может выводить det для: 

:- pred load_freqs(int::in, io.res(list(float))::out, io::di, io::uo) is det.
load_freqs(CPU, ResFreqs, !IO):-
    open_input(cpu_fn(0, "available_frequencies"), ResStream, !IO),
    (ResStream = io.ok(Stream),
        ResFreqs = io.ok([])
    ;ResStream = io.error(Err),
        ResFreqs = io.error(Err)
    ).

Но почему конструкция "если-то-еще" вводит полудет?

...