I'm running the Isabelle theorem prover on top of Poly/ML on a Mac OS X PowerBook G4. I would like to be able to
- Call Isabelle's ML functions directly from external processes that
have been written in C.
There's no way to publish an interface to ML. I think the only way to do this is through a socket. You can set up a socket in ML and have the C code send messages through it to ML. ML can then respond in a similar way. You'll have to convert the messages between bytes on the stream and the types your functions expect. Perhaps someone could write an RPC interface compiler of some sort.
- Call C code I've loaded into Isabelle's process space,
You can use the foreign function interface to load a shared library and call functions in it.
and have that code call back to Poly/ML functions.
Passing ML functions as arguments to C functions is currently only implemented on the i386 platform. This is a bit of a hack because of the different nature of C and ML functions and the FFI code has to compile a C function on the fly to pass to C to represent the ML function.
David