[mercury-users] C Interface (was Circular lists)

[Thomas Charles CONWAY]

Richard A. O'Keefe, you write:
> The Quintus interface, with *NO* access to Prolog data structures or control
> from C, was entirely adequate to do I/O, networking, IPC, &c.  I believe a
> lower level access *to C structures* was provided to Prolog about the time
> I left.  Peter Schachte can comment on this, because he implemented it.
> But Prolog access to C data structures is not the same as C access to
> Prolog data structures.

The Mercury interface to C does not provide access to Mercury
data structures. Any C code that manipulates Mercury data structures
does so relying on knowledge of the current implementation, and
is considered unsafe. It would be nice if we could detect if
the C code does manipulate Mercury data structures, but I think
that this is not something that we can without too many false
hits, or too many false misses.

> What I'm getting at is really incredibly simple:  a subset of the interface
> that can be used to pass some subset of *C* data structures between Mercury
> and C, where an amazingly simple tool can say "yes, you have used no
> interface features outside that subset".
> 
> You can do _all_ of I/O, networking, IPC, and graphics with an interface
> subset like that.

Agreed. The Tcl/Tk and OpenGL interfaces don't manipulate Mercury
data structures. The only "dangerous" thing that happens (memory
management/GC issues aside) is that we store a closure in a global
variable and get it back later.

> You might be surprised at just how checkable (new) C code can be.
> 
> 	Perhaps we have different ideas on what is checkable from such a tool,
> 	and how large that checkable set needs to be before it is useful.
> 
> Exactly.  The Mercury team seem to have jumped to the conclusion that I meant
> some kind of universal theorem prover that could just about write the programs
> for you, whereas I want something much more modest:  a list of safe interface
> features and a tool that checks that only those features are used.

I guess once we had a C parser, we could check for dereferencing or
casting of Mercury terms, however even something like this would be
a large amount of work to produce. The trick is the "once we had a
C parser"...

Thomas
-- 
ZZ:wq!
^X^C
Thomas Conway               				      conway at cs.mu.oz.au
AD DEUM ET VINUM	  			      Every sword has two edges.