On Fri, 7 Dec 2007, Basile STARYNKEVITCH wrote:

Does PolyML provide facilities to generate (machine) code at runtime (on Linux/AMD64 or Linux/x86), either in a type safe way (in the spirit of MetaML or MetaOcaml) or in a more low level unsafe way (e.g. like LLVM, Libjit, GNU lightning, ....)

Poly/ML is an ``incremental compiler'' and always produces native code, even at runtime. The mechanism for this is similar to traditional EVAL in Lisp, but the code is properly compiled and type-checked (only at runtime-compilation-evaluation, though).

While this is not proper meta programming, it works very smoothly. We are using this facility on an everyday basis in the Isabelle system http://isabelle.in.tum.de/

The most basic way is to invoke PolyML.use on source files. Below is a more convenient wrapper taking strings, with optional redirection of output/error, and proper error line numbers:

fun use_text name (print, err) verbose txt = let val in_buffer = ref (SML90.explode txt); val out_buffer = ref ([]: string list); fun output () = SML90.implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));

val line_no = ref 1; fun line () = ! line_no; fun get () = (case ! in_buffer of [] => "" | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c)); fun put s = out_buffer := s :: ! out_buffer;

fun exec () = (case ! in_buffer of [] => () | _ => (PolyML.compilerEx (get, put, line, name) (); exec ())); in exec () handle exn => (err (output ()); raise exn); if verbose then print (output ()) else () end;

Examples:

use_text "test" (TextIO.print, TextIO.print) true "val a = 42";

val a = 42 : int val it = () : unit

use_text "test" (TextIO.print, TextIO.print) true "1 + true";

Error: in 'test', line 1. Can't unify Int32.int/int with bool (Overloading does not include type) Found near +( 1, true) Static errors (pass2)

Makarius