3

Mercury（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： `load_freqs'（in、out、di、uo）内：
cpugear.m：075：エラー：決定論宣言が満たされていません。
cpugear.m：075：「det」を宣言し、「semidet」を推測しました。
cpugear.m：080： `ResStream'と`io.error（Err）'の統合が失敗する可能性があります。
cpugear.m：076：述語 `cpugear.load_freqs'/ 4の節内：
cpugear.m：076：警告：変数`CPU'はこのスコープで1回だけ発生します。
cpugear.m：078：述語 `cpugear.load_freqs'/ 4の節内：
cpugear.m：078：警告：変数`Stream'はこのスコープで1回だけ発生します。

しかし、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.
4

3 に答える 3

2

条件付きの決定論に関するMercuryの規則（以下）を読んだところ、これを決定論的と見なすには、を次のように置き換える必要があります->。,

Mercuryリファレンスマニュアルから：

if-then-elseの条件が失敗できない場合、if-then-elseは、条件と「then」部分の接続詞と同等であり、その決定論はそれに応じて計算されます。そうしないと、「then」部分または「else」部分のいずれかが失敗する可能性がある場合に、if-then-elseが失敗する可能性があります。

于 2010-07-29T16:16:53.390 に答える
2

「なぜ」は。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などになる可能性がある場合、コンパイラーは、スイッチが不完全になるため、プログラマーにスイッチを修正するように指示します。

于 2011-02-07T02:11:23.537 に答える
1

わかりました、それは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)
    ).

しかし、なぜ「if-then-else」構造がセミデットを導入するのでしょうか。

于 2010-07-30T04:45:41.137 に答える