[mercury-users] Pred defns
Ray Nickson
nickson at MCS.VUW.AC.NZ
Tue Apr 7 05:59:07 AEST 1998
>>>>> "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.
More information about the users
mailing list