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”在此范围内仅出现一次。
cpugear.m:078：在谓词“cpugear.load_freqs”/4 的子句中：
cpugear.m:078：警告：变量“流”在此范围内仅出现一次。

但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：它甚至可以决定：

:- 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

至于“为什么”。让我们用 if-then-else 查看原始代码：

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

如果条件失败，则 else 情况下的第一个合取是 semidet 测试。编译器不知道它必须成功（这可以通过知道该条件失败来推断）。换句话说，编译器不够聪明。

也就是说，很少会发现这个问题，因为通常情况更复杂，不允许做出这种推断，所以编译器不够聪明，无法在这里确定正确的确定性并不重要。

建议尽可能使用开关进行编程（例如此示例），它可以防止当前问题并有助于确保您已经涵盖了所有可能的 ResStream 情况。例如，如果将来 io.error 被重构并且可能是 io.error_file_not_found 或 io.error_disk_full 等，编译器将指示程序员修复他们的开关，因为它现在不完整。

于 2011-02-07T02:11:23.537 回答
2

我对带有条件的确定性规则的 Mercury 规则（如下）的解读是，要将此视为确定性，您应该->将,

来自 Mercury 参考手册：

如果 if-then-else 的条件不能失败，则 if-then-else 等价于条件和“then”部分的合取，并据此计算其确定性。否则，如果“then”部分或“else”部分可能失败，则 if-then-else 可能会失败。

于 2010-07-29T16:16:53.390 回答
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”结构会引入 semidet 呢？

于 2010-07-30T04:45:41.137 回答