On Thu, 4 Feb 2016, Artella Coding wrote:
So if I return back to "Pure" mode in the Theories tab, is there any way for me to enter (via the debugger) the factorial function only at "factorial 100;"? Right now the factorial file contains the following code :
================= fun factorial 0 = 1 | factorial n = n * factorial (n - 1);
factorial 10; factorial 100; factorial 1000; =================
and it seems that one has to recurse through (in the debugger) 10 calls of the factorial function (due to "factorial 10;") before one can step through invocations of the factorial function due to "factorial 100;". Is there any way to put a breakpoint at "factorial 100;" so that one only sees invocations of the factorial function due to "factorial 100;" and ignore the invocations of factorial due to the "factorial 10;" call?
It is better to split the "static" part (the function definition) from the "dynamic" exploration of later expressions with the debugger. This avoids edits on the same file, and thus a reset of breakpoints, and confusion which expressions are meant to be under debugger control.
For experimentation, I recommend Isabelle/ML and not official Standard ML, since it provides more possibilities that just SML_file.
Given the task sketched above, I would do it like this (see the included Test.thy).
Thus you get three running threads for each invocation of factorial.
From the size of the stack, it is somehow possible to guess which is which
evaluation. I presently don't know a way to restrict debugging individually, e.g. to interact with ML_val ?factorial 100? only. Debugging is controlled at compile time for factorial once and for all.
There is also some tension between continued editing and debugging: the latter lets the cursur jump around according to the program position; but the user might have something else in mind.
Makarius