[isabelle] Real time in generated code



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





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