[mercury-users] inst decls and fixed-length lists

[doug.auclair at logicaltypes.com]

Dear all,

I know that a list of exactly N elements (let's say, 4 elements) can be statically verified by the compiler with:

:- inst four_play(T) == bound([T|bound([T|bound([T|bound([T|bound([])])])])]).

which, given that this is only four elements, isn't all that bad a declaration, but with larger lists (e.g. lists of 8 or more elements), this becomes a chore to write and to regard.  So, I attempted to compose inst declarations:

:- inst two_bits(T, End) == bound([T|bound([T|bound(End)])]).
:- inst four_gone(T, End) == two_bits(T, two_bits(T, End)).
:- inst pieces_of_eight(T) == four_gone(T, four_gone(T, [])).

... and with exactly two elements, the two_bits inst was well-behaved:

TwoPly = [red, green],
print_twosies(TwoPly)

:- pred print_twosies(list(T)::in(two_bits(T, []), io::di, io::uo) is det.
print_twosies(Colours) --> print(Colours), nl.

but trying to use the composed insts gets me compiler errors:

Fore = [purple, crimson, cyan, amber],
print_foursome(Fore)

:- pred print_foursome(list(T)::in(four_gone(T, []), io::di, io::uo) is det.
print_foursome(TrueColours) --> print(TrueColours), nl.

The compiler complains it is a list of (exactly) four elements, expecting a composed pair of two_bit insts instead.  But, to me, it looks like the composed pair of two_bits insts equate to a list of (exactly) four elements.  The same compiler errors result in my attempt to apply the inst of pieces_of_eight to a list of exactly eight elements.

What am I missing here?  How can I use composition of inst declarations to describe a list of N elements?

Sincerely,
Doug Auclair

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------