[mercury-users] inst problem

[Fergus Henderson]

On 27-Jul-2001, Holger Krug <hkrug at rationalizer.com> wrote:
> Below there is code where I think mmc should infer a tighter inst than
> it actually does. I do not understand, why the tighter inst isn't
> inferred.
...
> :- type lexer_result(Token) = ok(Token)
> 			    ; eof
> 			    ; error(int).
...
> :- inst non_error_lexer_token ---> ok(ground) ; eof.
...
> :- mode process_token(in, out, in(statestack), in, 
> 		      in(non_error_lexer_token), out) is det.
...
> parse(Lex0, Lex, St, Sy, Res) :-
>     (
>         get_token(Tok, Lex0, Lex1),
> 
>         ( 
> 	    Tok = error(_)
> 	->
>             Res = error("lexer error"),
>             Lex = Lex1
> 	;
> 	    process_token(Lex1, Lex, St, Sy, Tok, Res)
>         )
>     ).
> 
> mmc claimes:
> 
> expr.m:102: In clause for `parse(in, out, in((expr:statestack)), in, out)':
> expr.m:102:   in argument 5 of call to predicate `expr:process_token/6':
> expr.m:102:   mode error: variable `Tok' has instantiatedness `ground',
> expr.m:102:   expected instantiatedness was `(expr:non_error_lexer_token)'.
> 
> Why isn't mmc able to infer, that `Tok' in the call to process_token/6
> has the inst demanded ?

The algorithm that the compiler uses for mode checking/inference does not
infer anything from failure of negated goals.  Likewise, when analyzing
if-then-else goals, it doesn't infer anything from the failure of the
condition when analyzing the "else" part.

In the general case, it would be difficult to infer anything positive
from failure of a compound goal, because the failure could have been due
to failure of any sub-goal of the compound goal.  Only in the special
case where the sub-goal consists of a single unification, with free
variables as arguments, would it be possible to make such inferences.

I suppose it might be possible to make the compiler's inference more
precise by checking for that special case.  However, it's not clear
whether this is really worth-while.  Getting mode inference to infer
maximally precise sub-types is an undecidable problem, in the general
case, so it's a matter of balancing expressiveness with complexity
of the mode inference algorithm.

In cases like this, it's pretty easy to rewrite your code in a slightly
different style that the compiler can analyze more easily -- as you
showed in your original post, you can write the code using a switch
rather than an if-then-else.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------