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

[Guillaume Yziquel]

Le Thursday 09 Jun 2011 à 14:37:53 (+1000), Mark Brown a écrit :
> Hi,

Hi.

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

Well, as I'm doing incremental typechecking, for now, it's simpler to
just dump propositions into a bag without concern for duplicates.
Suboptimal in the long run, but practical in the short run. Lists would
be fine I guess, but I also need to train myself with more involved
datastructures as I'll be using that in the long run.

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

OK. I think I got this one...

On the same topic, I believe that the C interface to gprolog allows you
to run successively a query, hereby exhausting the answers that gprolog
finds for you. That's quite nice. I see that there's the solutions
predicate, but it finds everything in one go, and thus doesn't allow you
to interleave the execution of calling code and mercury code as gprolog
allows you to do. That would be really a nice feature to have to be able
to integrate that with Lwt monadic green threads in OCaml. No simple way
to do that?

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

Yes. I'm doing that now.

> In any case, sets and lists can be searched easily without such promises.

Well, I'm now doing almost fine with the following code. Almost fine
because if I uncomment the two '%', I get the following error message:

	./test.native

	Mercury runtime: memory zone nondetstack#0 overflowed
	This may have been caused by a stack overflow, due to unbounded
	recursion.
	make[1]: *** [test] Erreur 1

Here's the code:

	:- type prop --->
	        term_definition(term, term)     ;
	        term_typed(term, typ)           .

	:- func no_props = bag(prop).
	        no_props = bag.init.
	:- pragma foreign_export("C", no_props = out, "no_props").

	:- func define_term(term, term, bag(prop)) = bag(prop).
	        define_term(Term1, Term2, Props) =
			bag.insert(Props, term_definition(Term1, Term2)).
	:- pragma foreign_export("C", define_term(in, in, in) = out, "define_term").

	:- func type_term(term, typ, bag(prop)) = bag(prop).
	        type_term(Term, Type, Props) = bag.insert(Props, term_typed(Term, Type)).
	:- pragma foreign_export("C", type_term(in, in, in) = out, "type_term").

	:- pred search_type_annotation(term::in, typ::out, bag(prop)::in).
	        search_type_annotation(Term, Type, Props) :-
	                bag.member(Prop, Props, Remaining),
	                (       if      Prop = term_typed(Term, T)
	                        then    Type = T
	                        else    search_type_annotation(Term, Type, Remaining)
	                ).

	:- pred search_equivalent_term(term::in, term::out, bag(prop)::in).

	%       search_equivalent_term(Term, EqTerm, _) :-
	%                       Term = EqTerm.

	        search_equivalent_term(Term, EqTerm, Props) :-
	                bag.member(Prop, Props, Remaining),
	                (       if      Prop = term_definition(Term, Eq)
	                        then    EqTerm = Eq
	                        else    search_equivalent_term(Term, EqTerm, Remaining)
	                ).

	:- pred typecheck(term::in, typ::out, bag(prop)::in).

	        typecheck(Term, Type, Props) :-
	                search_type_annotation(Term, Type, Props).

	        typecheck(Term, Type, Props) :-
	                (       search_equivalent_term(Term, EqTerm, Props),
	                        typecheck(EqTerm, Type, Props)
	                ).

	:- pred typeinfer(term::in, typ::out, bag(prop)::in).
	:- pragma foreign_export("C", typeinfer(in, out, in), "typeinfer").
	        typeinfer(Term, Type, Props) :-
	                promise_equivalent_solutions [Type]
	                typecheck(Term, Type, Props).

I do not really understand where the unbounded recursion comes from.
When commented, the fact that the search exhausts the bag gives some
kind of termination argument. But I do not see why the uncommented code
loops indefinitely...

Another thing I do not understand is why the Mercury compiler infers the
determinism category of det for typeinfer. As far as I can see, with
promise_equivalent_solutions, it should be semidet as I do not see a
guarantee that the search will yield a solution.

Thank you all for helping me getting started with Mercury.

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