[mercury-users] inst of list in non-empty branch

[doug.auclair at logicaltypes.com]

Dear all, hello!

This question is a two-parter: when I have a predicate branch on
list insts, how do I tell the compiler when I am in the non-empty
list branch that the inst of the list is indeed non_empty_list?

Specifically, my pred print_kids/4 is structured thus:

print_kids(Element, [], !IO) :-
         print(Element, !IO),
         print(" has no children\n", !IO).
print_kids(Element, Kids@[_|_], !IO) :-
         format("The child element%s of ", [s(singular_plural(Kids))], !IO),
         print(Element, !IO),
         is_are(Kids, !IO),
         print(Kids, !IO),
         nl(!IO).

In the second clause, Kids can only be non-empty, and it must be that
way for func singular_plural/1 and pred is_are/3:

:- func singular_plural(list(T)) = string.
:- mode singular_plural(in(non_empty_list)) = out is det.

:- pred is_are(list(T), io.state, io.state).
:- mode is_are(in(non_empty_list), di, uo) is det.

but when I attempt to compile the above, the compiler refuses:

test_xml_kids.m:063: In clause for `print_kids(in, in, di, uo)':
test_xml_kids.m:063:   in argument 1 of call to function
test_xml_kids.m:063:   `test_xml_kids.singular_plural'/1:
test_xml_kids.m:063:   mode error: variable `Kids' has instantiatedness
test_xml_kids.m:063:   `ground',
test_xml_kids.m:063:   expected instantiatedness was `bound(list.'[|]'(ground,
test_xml_kids.m:063:   ground))'.

How do I instruct the compiler that a list in the non-empty branch is indeed
inst non_empty_list?  Shouldn't the compiler automagically 'know' this?

The second part is this:  once the compiler agrees that Kids is inst
non_empty_list, then isn't this, really, a new binary (inductive) type of:

:- type non_empty_list(T) ---> [T] ; [T|non_empty_list(T)].

or structurely, the following goal is true:

(Kids = [_] ; Kids = [_, _|_])

so that a det predicate could be composed of the following two clauses:

singular_plural([_]) = "".
singular_plural([_, _|_]) = "s".

and 

is_are([_], !IO) :- print(" is ", !IO).
is_are([_, _|_], !IO) :- print(" are ", !IO).

If this is not the proper syntax for total coverage of lists of
non_empty_list inst, what is?

Thank you for your help.

Sincerely,
Douglas M. 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
--------------------------------------------------------------------------