[mercury-users] number of args for bag.init exported to C

[Mark Brown]

Hi,

On 08-Jun-2011, Guillaume Yziquel <guillaume.yziquel at gmx.ch> wrote:
> Le Wednesday 08 Jun 2011 à 11:43:50 (+1000), Paul Bone a écrit :
> > On Tue, Jun 07, 2011 at 04:38:49PM +0200, Guillaume Yziquel wrote:
> >
> > :- pred bag_of_ints_init(bag(int)::out) is det.
> > :- pragma foreign_export("C", bag_of_ints_init(out), "no_props").
> > 
> > bag_of_ints_init(Bag) :-
> >     bag.init(Bag).
> > 
> > Hope this helps.
> 
> Yes, it does. I'm now having two problems with the following code:
> 
> 	:- type prop --->
> 		term_definition(term, term)	;
> 		term_typed(term, typ)		.
> 
> 	:- pred typecheck(term::in, typ::out, bag(prop)::in) is semidet.
> 	:- pragma foreign_export("C", typecheck(in, out, in), "typecheck").
> 		typecheck(Term, Type, Props) :-
> 			promise_equivalent_solutions [Prop, RemainingProps]
> 			bag.member(Prop, Props, RemainingProps),
> 			promise_equivalent_solutions [Type]
> 			(	Prop = term_typed(Term, Type)
> 			;	typecheck(Term, Type, RemainingProps)
> 			).
> 
> Essentially, this looks up into the bag of props for a proposition that
> refers to an explicit type annotation in my custom language.
> 
> So, first of all, I'd like to know if there is a more idiomatic way to
> find an element in a bag on which to do unification. And if a bag is the
> right data structure for that goal.

No, it probably isn't.  The main feature of bags is that they con contain
duplicates, which wouldn't be meaningful for your application.  You may
try set(prop) or even just list(prop) would be a good choice.

> 
> Secondly, I'm using promise_equivalent_solutions to be able to force the
> determinism category of typecheck to semidet in order to export it to C.
> I'm under the impression that I'm using this in a suboptimal manner (if
> it's not outright wrong).

You're right, it's outright wrong.  ;-)

The first promise just covers the call to member, and effectively says
that any one Prop is equivalent to another.  In consequence, Mercury only
tries the first prop in the following goal, and doesn't consider the others.

The idiomatic way to search a bag would have the second promise scoped over
the entire body of typecheck/3.  This promises that, although the bag
contains different props, there is at most one `typ' for each term.  Once
the type has been found Mercury won't search any further.

In any case, sets and lists can be searched easily without such promises.
For sets, use set.remove_least, and for lists just deconstruct.  You will
need to write the final disjunction as an if-then-else, though:

    ( if Prop = term_typed(Term, Type0) then
        Type = Type0
    else
        typecheck(Type, Type, RemainingProps)
    ).

Unlike the disjunction, Mercury can prove that this if-then-else succeeds
at most once, and hence that the `semidet' determinism is correct.

Cheers,
Mark.

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