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.
Makariustheory Test
imports Pure
begin
declare [[ML_debugger]]
ML \<open>
fun (**) factorial 0 = 1
| factorial n = n * factorial (n - 1);
\<close>
text \<open>Open debugger panel, set breakpoint here: (**)\<close>
text \<open>Explore some expressions (independently via
\<^theory_text>\<open>ML_val\<close>).
This requires careful edits just before one of them, to ensure
they are evaluated again (and under debugger control).\<close>
ML_val \<open>factorial 10\<close>
ML_val \<open>factorial 100\<close>
ML_val \<open>factorial 1000\<close>
end
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
