[mercury-users] Testing with dependent lists?

[doug.auclair at logicaltypes.com]

Dear all,

I'm testing the behavior of a 'switch' I've built as a mercury module.
The switch is on for some preconditions and off for others (and 
is programmable), so I store the on/off answers in an even-length
list (I cribbed some code from Zoltan that defines such an inst).  The
test is as follows:

-----

:- inst even_len_list(I) ---> []; [I|bound([I|even_len_list(I)])].
:- mode even_len_list_in(I) == even_len_list(I) >> even_len_list(I).

:- pred for_each_switch(list(switch), list(float), list(float),
	                list(float), list(float),
			io, io).
:- mode for_each_switch(in, in, in, even_len_list_in(ground),
	                even_len_list_in(ground), di, uo) is det.
for_each_switch([], _, _, _, _) --> [].
for_each_switch([_|_], _, _, [], _) -->
	{ error("Answers depend on switches") }.
for_each_switch([_|_], _, _, _, []) -->
	{ error("Expectations depend on switches") }.
for_each_switch([N|Ns], OnPres, OffPres, [A1, A2|Rest1], [E1, E2|REst2]) -->
	print("For switch " ++ string(N) ++ ":\n\t"),
	print_test_result(OnPres, A1, E1),
	print_test_result(OffPres, A2, E2),
	for_each_switch(Ns, OnPres, OffPres, Rest1, REst2).
-----

... and mmc generates the following error:

-----
test_neuron.m:039: In `for_each_switch'(in, in, in,
test_neuron.m:039:   in($typed_inst((list.list(float)),
test_neuron.m:039:   test_switch.even_len_list(ground))),
test_neuron.m:039:   in($typed_inst((list.list(float)),
test_neuron.m:039:   test_switch.even_len_list(ground))), di, uo):
test_neuron.m:039:   error: determinism declaration not satisfied.
test_neuron.m:039:   Declared `det', inferred `semidet'.
test_neuron.m:044:   In argument 5 of clause head:
test_neuron.m:044:   unification of `HeadVar__5' and `list.[]' can fail.
test_neuron.m:046:   In argument 5 of clause head:
test_neuron.m:046:   unification of `HeadVar__5' and `list.[E1 | V_44]' can
test_neuron.m:046:   fail.
test_neuron.m:047: In clause for `for_each_switch(in, in, in,
test_neuron.m:047:   test_switch.even_len_list_in(ground),
test_neuron.m:047:   test_switch.even_len_list_in(ground), di, uo)':
test_neuron.m:047:   in argument 2 of call to predicate `io.print'/3:
test_neuron.m:047:   mode error: variable `DCG_0' has instantiatedness
test_neuron.m:047:   `mostly_unique',
test_neuron.m:047:   expected instantiatedness was `unique'.
-----

The wording of the first error is especially puzzling -- I may fail to bind
to EITHER the empty or non-empty list when I am a list?  Why? and, why
does only the second even-length list cause the error, but not the first?
The second error follows from the first, so solving the first error should
solve the second.

The pred is called with statically constructed even-length lists:
-----
	  for_each_switch([Sw1, Sw2, Sw3], OnPreconditions, OffPres,
			  [A11, A12, A21, A22, A31, A32],
			  [1.0, 0.0, 0.0, 0.0, 1.0, 1.0]).
-----
... so the list-structure is available at compile-time, which means the
inst requirement should be satisfied.

More generally (after the even-length list issue is cleared up), is there
a way to inform the compiler of dependency between two list instances,
like a functional dependency of some kind?  What I'm after is to be able
to tell the compiler:

If list A is not empty then list B is not empty.

So that I don't need the middle two clauses at all, I could just annotate
the predicate type with something like:

:- pred foo(A, B, C) <= (not_empty(A) -> (not_empty(B), not_empty(C))

or

:- pred foo(A, B, C) <= (not_emtpy(A) -> not_empty(B), not_empty(A) -> not_empty(C))

Does Mercury have a mechanism to do this?  If so, what is it?

Sincerely,
Doug Auclair

--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------