Re: [isabelle] Real time in generated code



On Tue, 21 Jan 2014, marco caminati wrote:

However, I would also like this code to be triggered by time events at runtime. For example, I would like the code to output its values every second. A simple way I had in mind was to add an argument to the specification of my function representing time, and then to plug a time counter into that argument, but I'm digressing.

Andreas Lochbihler has already given some hints that this is probably just a question how to wrap the Isabelle-generated Scala code into something that lies outside the image of your original Isabelle/HOL specifications.

So it is mostly about some timer or thread programming on the JVM, using Scala to access regular Java APIs.


Googling, I found references to timeap/timeit and to Time.now ().

timeap/timeit are from Isabele/ML.

Time.now is from Standard ML and it is OK to use in Isabelle/ML as well (this is not always the case for such SML basis library things).


2) I am only familiar with Isar, but I understand that to use these
   approaches I should embed ML code in it, right?  In this case, is
   there a good primer to descend from the Isar layer to the underlying
   ML layer?

Step 0 is to get the basic mental model about Isabelle right, including some elementary terminology. Isabelle is a framework of many different languages: Isabelle/Pure, Isabelle/HOL, Isabelle/ML, Isabelle/Scala, ... Isabelle/XYZ according to your own imaginations if you like.

Some of these languages are intertwined, and embeded into each other in certain ways, but it does not make sense to speak of "layers" or to "descend" -- especially not for the special pair Isabelle/Isar versus Isabelle/ML.

The canonical picture to keep in mind is http://en.wikipedia.org/wiki/File:Yin_and_Yang.svg -- sometimes this one also helps: http://en.wikipedia.org/wiki/File:Klein_bottle.svg


You can learn more about Isabelle/ML in the "implementation" manual that is included in Isabelle, e.g. Documentation panel in Isabelle/jEdit. There is also a tiny example at the bottom of the same panel: src/HOL/ex/ML.thy. It includes some bits of HOL -> ML code generation, but not Scala.


That is an interesting pastime, but it is probably irrelevant to your problem.


	Makarius





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