How do I execute, as part of a ML{*…*} command, a string that contains ML source?

Question

From the Isabelle user list Makarius Wenzel says this:

It is also possible to pass around ML sources as strings or tokens in Isabelle/ML, and invoke the compiler on it. That is a normal benefit of incremental compilation.

I have an ML statement as a string, like this:

ML{* val source_string = "val x = 3 + 4"; *}

I want to use "val x = 3 + 4" as a ML statement in a ML{*...*} command. I can do it by calling Poly/ML externally like this:

ML{* 
fun polyp cmd = Isabelle_System.bash 
  ("perl -e 'print q(" ^ cmd ^ ");' | $ML_HOME/poly");
*}

ML{* polyp source_string; *}

That takes about 200ms. I figure it would be about 0ms if I could do it internally.

Update 140411

Makarius Wenzel may have another way to do things, but what I have below with ML_Context.eval_text is almost what I want. It's in line with what I've been experimenting with. The problem is that used_only_by_src1 is global. I can't put it in the let.

I suppose if I was using src1 in two different ML{*...*} commands, there's some short period of time in which used_only_by_src1 could be changed by the one before it was used by the other. But, I guess this is all part of learning about stateless programming.

ML{*
val src1 = "x + y" (*I would actually have a global list of sources.*)

val used_only_by_src1 = Unsynchronized.ref "";

fun two_int_arg_fun s1 s2 = let
    val s = "val x = " ^ s1 ^ "val y = " ^ s2 
             ^ "used_only_by_src1 := (Int.toString(" ^ src1 ^ "))";
    val _ = ML_Context.eval_text true Position.none s;
  in !used_only_by_src1 end;
*}

ML{*
  two_int_arg_fun;  
  two_int_arg_fun "44;" "778;"
  (*3ms*)
*}

Note 140412: Actually, I don't need to execute ML strings. I can program in ML like normal, since any ML{*...*} can access global ML functions, where I can write what I need.

The main solution I got from this is how to pass arguments to a string of Perl code, which I got here from trying to do it for ML, so thanks to davidg. Plus, ML_Context.exec and ML_Context.eval_text might come in useful somewhere, and learning enough to be able to use them is totally useful.

There is the problem of needing a local or global Unsynchronized.ref that's guaranteed to not be changed by some other code (or a non-mutable type), but surely there's a solution to that.

I didn't pursue ML_Context.exec because isar_syn.ML wasn't making any sense to me, but I've gotten as far as below, so now I'm asking, "What functions do I need that involve Context.generic -> Context.generic or Toplevel.transition -> Toplevel.transition, and what do those do for me as far as being able to get the return value of 3+4 in a ML{*...*}?"

I'm using grep with Isabelle_System.bash, and I've gotten as far as what's below, in looking for the right signatures in Isabelle/Pure. I throw in for free a grep I use to look for useful or needed functions in the Poly/ML Basis.

ML{*
Isabelle_System.bash ("grep -nr 'get_generic' $ISABELLE_HOME/src/Pure");
Isabelle_System.bash ("grep -nr 'hash' $ML_HOME/../src/Basis/*");

Config.get_generic;

(*From use at line 265 of isar_syn.ML.*)
ML_Context.exec;
ML_Context.exec (fn () => ML_Context.eval_text true Position.none "3 + 4");
  (*OUT: val it = fn: Context.generic -> Context.generic*)  

(fn (txt, pos) =>
      Toplevel.generic_theory
        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
          Local_Theory.propagate_ml_env)) ("3 + 4", Position.none);
  (*OUT: val it = fn: Toplevel.transition -> Toplevel.transition*)
*}

Answer 1

The structure ML_Context might be a good starting point to look. For instance, your expression can be executed as so:

ML {*
  ML_Context.eval_text true Position.none "val x = 3 + 4"
*}

This will internally evaluate the expression 3 + 4, and throw away the results.

Functions like ML_Context.exec will allow you to capture the results of expressions and put them into your local context; you might want to look at implementation of the ML Isar command in src/Pure/Isar/isar_syn.ML to see how such functions are used in practice.