[m-rev.] for review: constrained polymorphic insts

[Fergus Henderson]

The main problem I can see is that it doesn't handle uniqueness correctly.

On 21-Feb-2002, David Overton <dmo at cs.mu.OZ.AU> wrote:
> Index: compiler/inst_match.m
...
> +:- pred inst_matches_final(inst, inst, module_info).
> +:- mode inst_matches_final(in, in, in) is semidet.
> +
>  :- pred inst_matches_final(inst, inst, type, module_info).
>  :- mode inst_matches_final(in, in, in, in) is semidet.

The difference between these two predicates should be documented.

(Also, the meaning of the inst_var_sub parameters in inst_matches_initial
should be documented.)

> +++ compiler/inst.m	21 Feb 2002 05:35:08 -0000
> +				% A constrained_inst_var is an inst variable
> +				% that is constrained to match_final the
> +				% specified inst.
> +	;		constrained_inst_var(inst_var, inst)
...
> inst_match.m:
> @@ -1036,6 +1067,8 @@
>  inst_is_clobbered(_, bound(mostly_clobbered, _)).
>  inst_is_clobbered(_, inst_var(_)) :-
>          error("internal error: uninstantiated inst parameter").
> +inst_is_clobbered(ModuleInfo, constrained_inst_var(_, Inst)) :-
> +	inst_is_clobbered(ModuleInfo, Inst).

This is not safe.

We know that constrained_inst_var(V, Inst) matches_final Inst.
But this does not imply that constrained_inst_var(V, Inst) is
clobbered iff Inst is clobbered.

In particular, V might be `unique', which matches_final `clobbered',
but V is not clobbered.

inst_is_clobbered is used by get_var_lives,
which is used to initialize the live_vars set in the mode_info.
An argument whose final inst is `V =< clobbered' will get
excluded from the live_vars set, even though it might still
be referred to be the caller.

E.g. consider this example:

	:- mode q(di, uo).
	q(X, Z) :-
		alias(X, Y),
		destroy(X),
		Z = Y.

	:- mode alias(I =< clobbered) >> (I =< clobbered),
			free >> (I =< clobbered)).
	alias(A, A).
	% i.e. alias(HeadVar__1, HeadVar__2) :- HeadVar__1 = A, HeadVar__2 = A.

	:- mode destroy(di).
	:- pragma c_code(destroy(X::di), "...").

In the call to `alias', X has initial inst `unique', which matches_final
`clobbered', so the inst parameter `I' will get bound to `unique'.

But in the body of `alias', the unification of
`HeadVar__2' with `A' will be permitted, because
both variables will be considered dead at that point.

So this example is mode-correct, but leads to the `uo' mode argument
of q/2 being clobbered.

> @@ -1242,6 +1294,9 @@
>  inst_is_not_partly_unique_2(_, inst_var(_), _, _) :-
>          error("internal error: uninstantiated inst parameter").
>  inst_is_not_partly_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
> +	Inst = constrained_inst_var(_, Inst2),
> +	inst_is_not_partly_unique_2(ModuleInfo, Inst2, Expansions0, Expansions).

There's a similar problem here.

> @@ -1285,6 +1340,9 @@
>  inst_is_not_fully_unique_2(_, inst_var(_), _, _) :-
>          error("internal error: uninstantiated inst parameter").
>  inst_is_not_fully_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
> +	Inst = constrained_inst_var(_, Inst2),
> +	inst_is_not_fully_unique_2(ModuleInfo, Inst2, Expansions0, Expansions).

And here.

> @@ -511,8 +476,20 @@
>  abstractly_unify_inst_functor(Live, InstA, ConsId, ArgInsts, ArgLives,
>  		Real, ModuleInfo0, Inst, Det, ModuleInfo) :-
>  	inst_expand(ModuleInfo0, InstA, InstA2),
> -	abstractly_unify_inst_functor_2(Live, InstA2, ConsId, ArgInsts,
> -			ArgLives, Real, ModuleInfo0, Inst, Det, ModuleInfo).
> +	( InstA2 = constrained_inst_var(InstVar, InstA3) ->
> +		abstractly_unify_inst_functor(Live, InstA3, ConsId, ArgInsts,
> +			ArgLives, Real, ModuleInfo0, Inst0, Det, ModuleInfo),
> +		(
> +			\+ inst_matches_final(Inst0, InstA3, ModuleInfo)
> +		->
> +			Inst = Inst0
> +		;
> +			Inst = constrained_inst_var(InstVar, Inst0)
> +		)
> +	;
> +		abstractly_unify_inst_functor_2(Live, InstA2, ConsId, ArgInsts,
> +			ArgLives, Real, ModuleInfo0, Inst, Det, ModuleInfo)
> +	).

Some comments here would help.

The if-then-else would probably be clearer if the `then' and the `else'
parts were swapped.

The line `Inst = Inst0' throws away information; the compiler knows that
Inst is at least as ground as InstVar, and is a subtype of InstVar,
but these facts are not recorded in the inst returned.
Is this going to cause trouble?
Maybe there should be an XXX comment there.

> +:- pred abstractly_unify_constrained_inst_var(is_live, inst_var, inst, inst,
> +		unify_is_real, module_info, inst, determinism, module_info).
> +:- mode abstractly_unify_constrained_inst_var(in, in, in, in, in, in, out,
> +		out, out) is semidet.
> +
> +abstractly_unify_constrained_inst_var(IsLive, InstVar, InstConstraint, InstB,
> +		UnifyIsReal, ModuleInfo0, Inst, Det, ModuleInfo) :-
> +	abstractly_unify_inst(IsLive, InstConstraint, InstB, UnifyIsReal,
> +		ModuleInfo0, Inst0, Det, ModuleInfo),
> +	( 
> +		Inst0 = constrained_inst_var(InstVar, _)
> +	->
> +		% Avoid adding the same constrained_inst_var twice.
> +		Inst = Inst0
> +	;
> +		\+ inst_matches_final(Inst0, InstConstraint, ModuleInfo)
> +	->
> +		% The inst has become too instantiated so the
> +		% constrained_inst_var must be removed.
> +		Inst = Inst0
> +	;
> +		% We can keep the constrained_inst_var.
> +		Inst = constrained_inst_var(InstVar, Inst0)
> +	).

This seems a bit assymetrical.
I'm concerned that the results may be different depending on
whether unifications are written as `X = Y' or `Y = X'.

> +make_shared_inst(constrained_inst_var(InstVar, Inst0), ModuleInfo0, Inst,
> +		ModuleInfo) :-
> +	make_shared_inst(Inst0, ModuleInfo0, Inst1, ModuleInfo),
> +	(
> +		\+ inst_matches_final(Inst1, Inst0, ModuleInfo)
> +	->
> +		Inst = Inst1
> +	;
> +		Inst = constrained_inst_var(InstVar, Inst1)
> +	).

make_shared_inst on `X =< clobbered' will give `X =< clobbered',
which is wrong in the case where the inst parameter X happens to be `unique'.

> +make_mostly_uniq_inst(constrained_inst_var(InstVar, Inst0), ModuleInfo0, Inst,
> +		ModuleInfo) :-
> +	make_mostly_uniq_inst(Inst0, ModuleInfo0, Inst1, ModuleInfo),
> +	(
> +		\+ inst_matches_final(Inst1, Inst0, ModuleInfo)
> +	->
> +		Inst = Inst1
> +	;
> +		Inst = constrained_inst_var(InstVar, Inst1)
> +	).

Likewise.

> @@ -1359,6 +1383,34 @@
>  :- pred inst_merge_3(inst, inst, maybe(type), module_info, inst, module_info).
>  :- mode inst_merge_3(in, in, in, in, out, out) is semidet.
>  
> +inst_merge_3(InstA, InstB, MaybeType, ModuleInfo0, Inst, ModuleInfo) :-
> +	( InstA = constrained_inst_var(InstVarA, InstA1) ->
> +		( InstB = constrained_inst_var(InstVarB, InstB1) ->
> +			( InstVarA = InstVarB ->
> +				inst_merge(InstA1, InstB1, MaybeType,
> +					ModuleInfo0, Inst0, ModuleInfo),
> +				Inst = constrained_inst_var(InstVarA, Inst0)
> +				% We can keep the constrained_inst_var here
> +				% since Inst0 = InstA1 `lub` InstB1 and the
> +				% original constraint on InstVarA, InstC,
> +				% must have been such that
> +				% InstA1 `lub` InstB1 =< InstC
> +			;
> +				inst_merge(InstA1, InstB1, MaybeType,
> +					ModuleInfo0, Inst, ModuleInfo)
> +			)

The call to inst_merge is the same in both branches of this if-then-else,
so it should be hoisted out:

			inst_merge(InstA1, InstB1, MaybeType,
				ModuleInfo0, Inst0, ModuleInfo),
			( InstVarA = InstVarB ->
				% We can keep the constrained_inst_var here
				% since Inst0 = InstA1 `lub` InstB1 and the
				% original constraint on InstVarA, InstC,
				% must have been such that
				% InstA1 `lub` InstB1 =< InstC
				Inst = constrained_inst_var(InstVarA, Inst0)
			;
				Inst = Inst0
			)


> @@ -1548,6 +1595,10 @@
>  merge_inst_uniq(not_reached, Uniq, _, Expansions, Expansions, Uniq).
>  merge_inst_uniq(inst_var(_), _, _, Expansions, Expansions, _) :-
>  	error("merge_inst_uniq: unexpected inst_var").
> +merge_inst_uniq(constrained_inst_var(_InstVar, Inst0), UniqB, ModuleInfo,
> +		Expansions0, Expansions, Uniq) :-
> +	merge_inst_uniq(Inst0, UniqB, ModuleInfo, Expansions0, Expansions,
> +		Uniq).

This might be wrong too.

> +++ compiler/mercury_to_mercury.m	20 Feb 2002 04:58:22 -0000
> +mercury_format_inst(constrained_inst_var(Var, Inst), VarSet) -->
> +	mercury_format_var(Var, VarSet, no),
> +	add_string(" =< "),
> +	mercury_format_inst(Inst, VarSet).

You need to output parentheses around that.

> +inst_apply_substitution(constrained_inst_var(Var, Inst0), Subst, Result) :-
> +	(
> +		map__search(Subst, Var, Replacement)
> +	->
> +		Result = Replacement
> +		% XXX Should probably have a sanity check here that
> +		% Replacement =< Inst0
> +	;
> +		Result = constrained_inst_var(Var, Inst0)
> +	).

Don't you need to apply substitutions recursively to Inst0?

E.g. what if you have an inst `X =< (Y =< ground)'?

> Index: compiler/prog_io.m
...
> +inst_var_constraints_are_consistent_in_inst(constrained_inst_var(V, Inst)) -->
> +	( Inst0 =^ map__elem(V) ->
> +		% Check that the inst_var constraint is consistent with the
> +		% previous constraint on this inst_var.
> +		{ Inst = Inst0 }
> +	;
> +		^ map__elem(V) := Inst
> +	),

Please s/V/InstVar/g

(In connection with `map', my first guess at what `V' stands for
is "value", not "variable".)

Otherwise that looks fine.

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