[mercury-users] Pred defns

[Ray Nickson]

>>>>> "Fergus" == Fergus Henderson <fjh at cs.mu.OZ.AU> writes:

Fergus> One way to do that sort of thing would be to provide an
Fergus> extensible type called say 'gvar'/1, with some way for the
Fergus> user to declare new constants of this type (or of instances of
Fergus> this type, e.g.  `gvar(int)', `gvar(float)', etc.) in
Fergus> different modules; then the io__state could contain a global
Fergus> store of the values of these global variables.

This is the first approach mentioned in this discussion that has
really appealed to me.  It's simple and elegant, and the only
``magic'' is in the standard DCG notation.

It's so simple in fact, that I tried to emulate something similar a
while ago.  (Code extracts below.)

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.

Initialize and finalize operations converted io__state to prover and
back, so the main/2 line looked tidy.

I actually wanted some of the non-IO parts of this state to be
backtrackable, but as a compromise I was willing to restrict it to be
determinate.

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.

Anyway, this was a couple of months ago, and I've forgotten some of
the details of the difficulties I had (didn't keep enough notes).  I
enclose part of one of my (unsuccessful) attempts, to give an idea of
the flavour I was hoping for.  I've suppressed some detail that I
think is irrelevant.  This attempt looks like one that was supposed
to be backtrackable.

Ray


:- 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)).

%% The last two arguments of proof_start and proof_step (in use, typically the
%% implicit DCG args) record the state of the prover (including the proof in
%% progress).

%% proof_start takes a term to prove and yields a name for the root node.

:- pred proof_start(proofterm::in, nodename::out,
                    prover::instate, prover::outstate)
   is det.

:- implementation.

%% The prover state comprises the mapping from node names to nodes, the next
%% free node number, and the I/O streams.
:- type prover
   ---> state(map(nodename,proofnode), int, io__state).

proof_start(Term, Node) -->
    new_node(unproved(Term), Node).

%%%%%%%%%%%%%%%%%%%%%%%%
%%%% The proof state ADT.
%%%%%%%%%%%%%%%%%%%%%%%%

%% Initialize the prover from initial IO state.
:- pred initialize_prover(io__state::di, prover::outstate)
   is det.
initialize_prover(IO, state(EmptyMap, 0, IO)) :-
    init(EmptyMap).

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

%% Create a brand new node with given proof.
:- pred new_node(proofnode::in, nodename::out,
                 prover::instate, prover::outstate)
   is det.

new_node(Proof, Node, state(Map0,Num0,IO), State) :-
    Num is Num0 + 1,
    Node = name(Num0),
    map__set(Map0, Node, Proof, Map),
    State = state(Map,Num,IO).

%%%%%%%%%%%%%%%%%%%
%%%% A sample proof.
%%%%%%%%%%%%%%%%%%%

main -->
    initialize_prover,
    sample_proof,
    finalize_prover.

:- pred sample_proof(prover::instate, prover::outstate)
   is det.