[mercury-users] nested unique modes (was: Pred defns)

[Thomas Charles CONWAY]

Fergus Henderson, you write:
> 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.
> 

I came across this exact problem in my SGML parser (I guess parsing is
an instance of theorem proving for a particular class of languages and
proofs :-). In the end I solved it by making the grammar deterministic,
and implementing backtracking by hand in the parser combinators.

Another approach that I haven;t tried yet, which once again requires
definite aliasing to work properly, is to have two insts for a parsing
state: one in which the io__state is bound and unique, and another in
which the io__state is free. Then you can define a pair of predicates
for extracting the io__state and replacing it. The parsing state that
results from extracting the io__state has its io__state field free, and
all the other accessors had better have two modes (or possibly one
parametric mode). Then the deterministic outer scopes of the parser
can do IO and the inner scopes can be semidet/nondet. I suspect there
are some devils in the details, but it should be feasible.

Thomas
-- 
Thomas Conway    || conway at cs.mu.oz.au
AD DEUM ET VINUM || Nail here [] for new monitor.