Re: [isabelle] Running ML in a theory context from the command line



On 24/05/18 11:17, Lars Hupel wrote:
> 
> I am trying to figure out if this can also be done from the command
> line, as an Isabelle tool. There's already precedent, e.g. the various
> "tptp" tools from Jasmin.
> 
> In "tptp_sledgehammer", for example, a theory file is constructed that
> imports some root theory and contains an ML snippet. It is then called
> via "isabelle process". This of course works, but I was wondering
> whether there's a more direct way, e.g. with "isabelle process -e". But
> I'm not sure what the correct incantation is to make it evaluate the ML
> snippet in the context of a theory, so that the "Open_Theory" structure
> is available.

The following is derived from the definition of 'ML_command':

  fun eval_in_theory thy s =
    ML_Context.eval_source_in (SOME (Proof_Context.init_global thy))
      ML_Compiler.flags (Input.string s);


Here is a complete example (with the included Scratch.thy):

  isabelle process -l Pure -T "~/Scratch" -e "fun eval_in_theory thy s =
ML_Context.eval_source_in (SOME (Proof_Context.init_global thy))
ML_Compiler.flags (Input.string s)" -e 'eval_in_theory
(Thy_Info.get_theory "Draft.Scratch") "test (serial_string ())"'


Maybe I should provide a function line eval_in_theory already in Pure.
Are there further important applications?


	Makarius
theory Scratch
  imports Pure
begin

ML \<open>fun test s = writeln ("This is a test: " ^ s)\<close>

end


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