Mercury ADT Properties

I wander why Mercury (10.04) cannot determine the determinism of the following fragment:

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

He complains:

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.

But io.resthey have only io.ok/1and io.error/1.
And the following code fragment compiles well:

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

(. ) , , , -> ,

Mercury:

if-then-else , if-then-else "", . if-then-else , "", "else", .

+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 .., , .

+2

Well, he can infer det for:

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

But why does the if-then-else construct introduce semidet?

+1
source

Source: https://habr.com/ru/post/1757082/


All Articles