On 16/11/11 15:38, David Matthews wrote:
On 16/11/2011 15:17, Phil Clayton wrote:
On 16/11/11 11:17, David Matthews wrote:
On 16/11/2011 04:15, Ian Zimmerman wrote:
Phil> David, My situation is slightly unusual so perhaps it's Phil> useful/interesting to explain some background. I'm working on Phil> support for GLib/GTK in SML which involves a significant number of Phil> calls to C functions.
Last I knew, this was impossible in Poly/ML due to no callbacks from C. Has something crucial changed?
The CInterface structure has had callbacks for a long time. They're only implemented on X86 but that covers the vast majority of users. There's an example in mlsource/extra/CInterface/Examples/ForeignTest.sml.
To clarify, callbacks are available on i386 but not x86_64.
I suspect those involved with large scale theorem proving will start moving to 64 bit OSes, if not already, so one application can address more than 4GB memory, as that amount of physical memory is becoming quite common these days.
Yes, you're correct. I'd forgotten that. I seem to recall that there was a problem with floating point on X86/64 but it may be possible to provide call-backs for functions that don't use them.
The calling conventions for x86_64 appear to pass via registers not only the initial floating point arguments but also the initial int/pointer arguments: http://en.wikipedia.org/wiki/X86_calling_conventions So I suspect all arguments, not just floating point, would be an issue for callbacks on x86_64?
There is a separate issue with floats/doubles on x86_64 when calling from SML to C but that doesn't relate to callbacks. It looks like an exception is meant to be raised but isn't currently. (Perhaps the preprocessor symbol X86_64 should be HOSTARCHITECTURE_X86_64 in foreign.cpp?)
But now I have confused myself. If x86_64 calling conventions pass initial int/pointer args via registers as well as floating point args, what is it about double/float args that is problematic? (Comment foreign.cpp, line 1037.) Also, a comment (foreign.cpp, line 1041) suggests that the size of doubles is the issue but on x86_64 but pointers are also 8 bytes.
Phil