Re: [isabelle] using Isabelle programmatically




On 04/10/2015 11:58 AM, Makarius wrote:
> On Fri, 10 Apr 2015, Viorel Preoteasa wrote:
>
>> Ideally I would need an API available in Python which does what I
>> need: Simplifies a term based on a specific theory. I understand now
>> that this API is available for Scala, and of course for SML, so in
>> the future I may use Scala.
>>
>> On the other hand, even if using SML, getting started with it does
>> not seem easy. I tried to find the right functions for this job
>> before posting the question to the mailing list.
>
> Do you mean SML as a language, or Isabelle/ML as a language + library?
I mean Isabelle/ML as a language + library.
>
> Getting started with Standard ML should be easy, using resources on
> the web or text books.
>
> Getting started with Isabelle/ML should be easy as well, since the
> Isabelle Prover IDE allows to explore whatever you see, down to its
> actual definition.  Tools are defined in Isabelle/ML, so the standard
> PIDE control-hover-click over Isar commands, methods, attributes etc.
> will show the relevant ML definitions.
Getting started was a bit difficult because I could not find an example
which
was self contained and small.

After asking on the mailing list, the answer by Lars, was very helpful
(ML‹Simplifier.rewrite @{context} @{cterm "rev []"}›), but it was working
within an Isabelle theory only, and not as standalone Isabelle/ML program.
The final Isabelle/ML program which does what I need is the following:

use_thy "AutoSimp";
val thy = Thy_Info.get_theory "AutoSimp";
fun term_to_string ctxt t =
  let
    val ctxt' = Config.put show_markup false ctxt;
    in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

val ctxt = Proof_Context.init_global thy;
val t = Syntax.read_term ctxt "rel (ExampleA0) (si_f) (d,so_f)";
val simp_term_a = Simplifier.rewrite ctxt (cterm_of thy t) |> Thm.rhs_of;
val simp_term_b = term_of simp_term_a;
val result = term_to_string ctxt simp_term_b;
writeln result;

It is conceptually very simple, but figuring out all these functions
was not that simple. I could do it only with the help of the answers
from the mailing list.

For example figuring out how to use Syntax.string_of_term was also
not easy. I found this way of using Syntax.string_of_term in an old message
for the mailing list. I do not understand it fully, but it seems it does
what
I need.

It is not clear to me if it is better to use this program as such or embed
as ML{*...*} into a theory file. In the end I am only interested in the
string from the variable result.

>
>
> Reading and understanding that needs some practice and some guidance,
> though. The "implementation" provides many explanations of many
> things, but it is not a quick-and-dirty HOWTO guide.
The main problem was getting started.
>
>
> Depending on what you ultimately want to achieve, some decent
> Isabelle/ML could work out easier and more robust than tinkering with
> scripting languages, processes, generated sources etc.
My use case is very simple now, and it is mainly exploratory. Using
Scala can be a good
solution, however Python is also a convenient language. Isabelle/ML can
also be a
solution, but the problem remains the same, figuring out the right
functions for
solving the problem.

Passing strings from one program to another does not seem such a big
problem,
and Python has a simple API for working with external programs.

By the way, how is the communication between Scala and Isabelle/ML done?
I assume it is also by having the Isabelle/ML process running in the
background,
and by sending and receiving strings via pipes.

Viorel




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