Re: [isabelle] using Isabelle programmatically

On Thu, 9 Apr 2015, Viorel Preoteasa wrote:

On 04/09/2015 06:50 PM, Lars Noschinski wrote:
context = ...
T = Simplifier.rewrite context (Syntax.parse_term context "...")
result =  Syntax.string_of_term context (the right hand side term of T)
Lars has already written something about how to acquire a context.
Depending on what you do with the terms in your program, it might be a
good idea to use the YXML format to pass terms between Isabelle and your
program. There have been some discussions on that subject in the past.

This is a good point. Thank you. We will use the simplified
expressions to generate some other Isabelle file, so for this
purpose we do not need the xml format.

Generating Isabelle sources sounds a bit odd. Depending on the actual application, it might be easier to put the "programmatic" part into Isabelle itself, as a small Isabelle/ML tool that reads the input and drives the system in the intended way, then outputs the results somewhere else. But you did not explain the intention so far.


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