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

[Julien Fischer]

Hi,

On Thu, 9 Jun 2011, Guillaume Yziquel wrote:

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

It is possible to do something of the sort using the do_while/4
predicate in the standard library's solutions module.  (The basic idea
is to use the Filter argument to make calls back to the foreign language
after each solution is generated.)

...

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

Here's one way in which the above code could go into an infinite loop
when that clause is uncommented.  Consider what happens when
typeinfer/3 is called with the Props argument set to the empty bag.

(1) We call typecheck(Term, Type, Props)
(2) The first clause of typecheck/3 will fail since the call to
     bag.member/3 in search_type_annotation/3 will fail.
(3) Trying the second clause of typecheck/3, we will first call
     search_equivalent_term/3.  The first clause (the commented out one)
     will succeed (it's deterministic), and the value returend in EqTerm
     will the same as the value Term.
(4) The recursive call to typecheck/3 has the same arguments as in (1)
     ...

The same could happen with non-empty bags if the unification "Type = T" in
search_type_annotation/3 always fails.

(The above depends on the order of the disjunctions, but I don't think
the compiler has much of a reason to reoder them in this case.)

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

It infers the determinism of det for typeinfer/3 because it infers the
determinism of multi for typecheck/3.  If the solutions of a multi goal
are promised to be equivalent then it is det.

Why does it infer a determinsim of multi for typecheck/3? 
The first clause:

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

is nondet, while the second:

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

is inferred to be multi.  The overall determinism is therefore
multi, since even if the first clause fails the second cannot fail.

Rather than relying on determinism inference I would suggest that you
include determinism annotations in your predicate declarations.  The
compiler would then be able to tell you about cases where the inferred
determinism differed from your expectations.

Cheers,
Julien.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------