Email Gateway (Aug 19 2022 at 13:18): Email Gateway (Aug 19 2022 at 13:18):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 13:34):From: marco caminati <marco.caminati@yahoo.it>
Hi,
I am using Isabelle/HOL to produce executable Scala code from suitable specifications.
I can get some code returning the value of some function upon a given argument.
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.
In general, how do you exploit machine's clock at runtime?
Googling, I found references to timeap/timeit and to Time.now ().
Questions:
1) Would any of these approaches be useful for the problem stated above?
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?
Best,
Marco
Email Gateway (Aug 19 2022 at 13:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Marco,
as you produce Scala code, I assume that you want to have those time events in Scala.
However, Isabelle's code generator generates only a subset of what you can do in Scala,
namely the purely functional programming part. With some extension like Imperative_HOL,
you get a bit further. But for asynchronous time events, you need concurrency, and AFAIK
there's nothing like that in Isabelle at the moment. Do you want to reason about these
time events? If not, then all this is just a matter of wrapping up the generated Scala
code -- you definitely don't want to do all this in Isabelle. That is, you should write in
Scala your time trigger that evaluates the function you are interested in and outputs the
results. If you want to reason about these timing events in Isabelle, then you first have
to model all this in HOL (not easy) and adapt the code generator such that maps your model
to the Scala primitives (difficult to get really right).
Hope this helps,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC
