*To*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Subject*: Re: [isabelle] using Isabelle programmatically*From*: Makarius <makarius at sketis.net>*Date*: Fri, 10 Apr 2015 14:18:18 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5527AFC7.5060801@aalto.fi>*References*: <55267367.9010402@aalto.fi> <alpine.LNX.2.00.1504092210370.39858@lxbroy10.informatik.tu-muenchen.de> <55278BEE.70108@aalto.fi> <alpine.LNX.2.00.1504101049230.46946@lxbroy10.informatik.tu-muenchen.de> <5527AFC7.5060801@aalto.fi>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 10 Apr 2015, Viorel Preoteasa wrote:

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 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.

support in the editor.

Scala can be a good solution, however Python is also a convenientlanguage. Isabelle/ML can also be a solution, but the problem remainsthe same, figuring out the right functions for solving the problem.

Passing strings from one program to another does not seem such a bigproblem, 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 thebackground, and by sending and receiving strings via pipes.

Makarius

**References**:**[isabelle] using Isabelle programmatically***From:*Viorel Preoteasa

**Re: [isabelle] using Isabelle programmatically***From:*Makarius

**Re: [isabelle] using Isabelle programmatically***From:*Viorel Preoteasa

**Re: [isabelle] using Isabelle programmatically***From:*Makarius

**Re: [isabelle] using Isabelle programmatically***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] using Isabelle programmatically
- Next by Date: [isabelle] Unknown Isabelle tool: env
- Previous by Thread: Re: [isabelle] using Isabelle programmatically
- Next by Thread: [isabelle] Last Call for Papers, PxTP 2015
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list