代码之家 › 专栏 › 技术社区 › ony

汞中的ADT性质

mercury declarative logic

3

ony · 技术社区 · 15 年前

我不明白为什么水星(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 回复 | 直到 15 年前

1

2

RD1 15 年前

我对墨丘利的条件决定论规则的理解是(下面)要把它看作是确定的,你应该替换 -> 用一个 ,

汞参考手册:

If-then-else的条件不能失败,否则就是失败相当于决定论据此计算。否则,如果零件可能会失效。

2

Paul Bone 15 年前

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

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

也就是说,很少会发现这个问题,因为通常情况下条件更复杂,不允许进行这种推断,所以编译器没有足够的智能来确定正确的决定论并不重要。

3

1

ony 15 年前

好的,它可以推断出:

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