nested unique modes (was: Pred defns)

[Fergus Henderson]

On 07-Apr-1998, Ray Nickson <nickson at MCS.VUW.AC.NZ> wrote:
> I wanted to include io__states in a structure that also included state
> peculiar to my application (a theorem prover ADT).  This ``prover''
> state would then be threaded using ordinary DCGs, with wrappers around
> the IO operations to get at the io__state, and accessors for my
> private state.
...
> Even with this simplification, I wasn't able to make the compiler
> happy: I couldn't get things determinate enough to satisfy the
> appropriate di/uo constraints for IO.  Maybe I could have done it if
> I'd tried harder, but I ran out of time.  Maybe the eagerly-awaited
> support for partially-instantiated modes is required: I don't
> understand well enough to say.

Putting the io__state inside some other structure requires nested
unique modes, and for that we need support for definite aliasing in the
mode system.

As a work-around, however, it is possible to convince the current compiler
that things are unique using calls to unsafe_promise_unique/2 (that's the
name in the latest development release; in some previous releases
it had the highly misleading name copy/2).

If you want an example of how to do it, the module `typecheck.m' in the
`compiler' subdirectory uses exactly this technique for its `typecheck_info'
data structure.

Note that the typechecker is deterministic; if you code is not, then
there may be some additional problems.

> :- pred main(io__state::di, io__state::uo) is det.
> 
> :- type prover.
> 
> :- mode instate ::
>    bound(state(ground,ground,unique)) -> bound(state(ground,ground,dead)).
> :- mode outstate ::
>    free -> bound(state(ground,ground,unique)).

That would need to be

  :- mode instate ::
     unique(state(ground,ground,unique)) -> bound(state(ground,ground,dead)).
  %  ^^^^^^
  :- mode outstate ::
     free -> unique(state(ground,ground,unique)).
  %          ^^^^^^

Note that the top-level structure must be unique if any component of it
is to be unique, because the components are reachable from the top-level
structure.

However, as noted above this won't work yet.
The work-around is to use

	:- mode instate :: in.	 % XXX this is a work-around
	:- mode outstate :: out. % XXX this is a work-around

and then to call unsafe_promise_unique in the appropriate places
where you extract the io__state.  For example your finalize_prover/2
predicate

> %% Finalize the prover (returning IO state).
> :- pred finalize_prover(prover::instate, io__state::uo).
> finalize_prover(state(_,_,IO), IO).

would become

  finalize_prover(state(_,_,IO), UniqIO) :-
	unsafe_promise_unique(IO, UniqIO).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.