[m-rev.] Re: for review: default modes for higher-order func insts

[Simon Taylor]

On 11-Oct-2001, David Overton <dmo at cs.mu.OZ.AU> wrote:
> On Wed, Oct 10, 2001 at 05:08:40PM +1000, Fergus Henderson wrote:
> > On 10-Oct-2001, David Overton <dmo at cs.mu.OZ.AU> wrote:
> > > +++ tests/hard_coded/ho_func_default_inst.m
> > > @@ -17,27 +17,44 @@
> > >  	{ Map = map },
> > >  	{ F1 = Map ^ det_elem(1) },
> > >  	{ F2 = Map ^ det_elem(2) },
> > > -	io__write_string(F1(1)),
> > > +	io__write_int(F1(1)),
> > >  	io__nl,
> > >  	write_func(F2).
> > >  
> > > -:- type t == (func(int) = string).
> > > +:- type t == (func(int) = int).
> > ...
> > >  :- func map = map(int, t).
> > >  
> > > -map = (map__init ^ elem(1) := hello) ^ elem(2) := world.
> > > +map = (((map__init
> > > +		^ elem(1) := foo1)
> > > +		^ elem(2) := foo2)
> > > +		^ elem(3) := foo3)
> > > +		^ elem(4) := foo4.
> > ...
> > > +:- func foo4(int) = int.
> > > +:- mode foo4(in(one)) = out is det.
> > 
> > Surely it should be an error to insert foo4 into that map?
> > 
> > E.g. consider the following code:
> > 
> > 	main -->
> > 		{ F4 = map ^ det_elem(4) },
> > 		io__write_int(F4(42)).
> > 
> > This will end up calling foo4(42), so it ought to be a mode error.
> 
> Yes, you are right.  The reason no mode error is reported is because of
> this code in inst_match.m, which does the required check and the ignores
> the result:
> 
> inst_matches_final_3(ground(UniqA, GroundInstInfoA), bound(UniqB, ListB),
> 		MaybeType, Info, Info) :-
> 	\+ ground_inst_info_is_nonstandard_func_mode(GroundInstInfoA,
> 		Info^module_info),
> 	unique_matches_final(UniqA, UniqB),
> 	bound_inst_list_is_ground(ListB, Info^module_info),
> 	uniq_matches_bound_inst_list(UniqA, ListB, Info^module_info),
> 	(
> 		MaybeType = yes(Type),
> 		% We can only do this check if the type is known.
> 		bound_inst_list_is_complete_for_type(set__init,
> 			Info^module_info, ListB, Type)
> 	;
> 		true
> 		% XXX enabling the check for bound_inst_list_is_complete
> 		% for type makes the mode checker too conservative in
> 		% the absence of alias tracking, so we currently always
> 		% succeed, even if this check fails.
> 	).
> 
> 
> I will remove that test from the test case.

One of the major advantages of Mercury over languages like C
is that code which passes the compiler's checking passes cannot
crash unless it runs out of resources (stack or heap). The code
above can cause crashes (see the test case below). We haven't
implemented nested unique modes because the mode checker doesn't
do alias tracking. Why is this case any different?

Simon.


:- module inst_matches_final_bug.

:- interface.

:- import_module io.

:- pred main(io__state::di, io__state::uo) is det.

:- implementation.

:- inst two_to_six == bound(2;3;4;5;6).

main -->
	call_with_two_to_six(return_three).

:- func return_three = int.
:- mode return_three = out(bound(3)) is det.

return_three = return_three_2.

:- func return_three_2 = int.

return_three_2 = 1.

:- pred call_with_two_to_six(int::in(two_to_six),
		io__state::di, io__state::uo) is det.
:- pragma no_inline(call_with_two_to_six/3).

call_with_two_to_six(2) -->
	io__write_string("Got two\n").
call_with_two_to_six(3) -->
	io__write_string("Got three\n").
call_with_two_to_six(4) -->
	io__write_string("Got four\n").
call_with_two_to_six(5) -->
	io__write_string("Got five\n").
call_with_two_to_six(6) -->
	io__write_string("Got six\n").

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