Re: [isabelle] accessing ML definitions in isabelle_process



On Tue, 28 Apr 2015, Viorel Preoteasa wrote:

 I was talking about batch mode already. You could e.g. put all your tool
 setup in a static .thy (or .thy that loads a .ML via ML_file).  It could
 refer to some environment variables to get dynamic input from somewhere
 else, e.g. another tmp file.
If I do this, and for example I define a value in a theory file:

theory TestML imports Main
begin
ML{*
val newline = writeln ""
*}
end

Now in isabelle_process I do:

use_thy "TestML"

The basic question is how do I access the value newline in the isabelle_process?

If I try just newline it is not recognized. Is this value available under some scope?

The value is part of the theory context of TextML. You can access it in a theory that imports it, for example.

All of Isabelle/ML happens within some theory context. The standard commands for that are 'ML' and 'ML_file' -- they are computationally complete wrt. the ML language. You can do whatever you want with it, including arbitrary I/O with the outside world.


Of course, you can define variants of the above 'ML' commands for your own purposes. With some more efforts it is also possible to define variants of use_thy + embedded Isabelle/ML in the raw ML toplevel environment, to bypass files altogether -- it depends on the application what is really required.


Here is an example to play with Isabelle/ML runtime-compilation-evaluation in Isabelle2015-RC:


theory Scratch
imports Main
begin

ML ‹fun ML ctxt source = ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags source›

ML ‹ML @{context} ‹writeln @{const_name True}››

end


Here is the same for the raw ML toplevel of isabelle_process:

fun ML ctxt source = ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags source;

ML (Proof_Context.init_global (Thy_Info.get_theory "Main")) (Input.string "writeln @{const_name True}");


This works to some extent, but not all aspects of the normal Isabelle/Isar/ML environment is imitated here (like proper handling of interrrupts and exceptions).


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.