nested unique modes (was: Pred defns)
fjh at cs.mu.OZ.AU
Tue Apr 7 17:22:31 AEST 1998
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
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'
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
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
> %% Finalize the prover (returning IO state).
> :- pred finalize_prover(prover::instate, io__state::uo).
> finalize_prover(state(_,_,IO), IO).
finalize_prover(state(_,_,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 188.8.131.52 | -- the last words of T. S. Garp.
More information about the users