Dear all,
I wanted to write this already a long time ago (prompted by an Isabelle
course I gave) but somehow forgot about it. Now I had a look at my
slides again and was reminded.
1) The first thing is rather subjective, but maybe you could comment on
it. I think the simplifier trace would be less surprising for newbies
and slightly easier to read if
- names of rewrite rules would be printed in their original form.
Consider, e.g., the trace resulting from
lemma "Suc 0 + 0 = 0"
using [[simp_trace]]
apply simp
where we have (among others)
[1]Applying instance of rewrite rule "Nat.nat.distinct_2":
Suc ?nat'2 = 0 ≡ False
Why not use the "real" name "Nat.nat.distinct(2)" in the trace (Okay,
the rule was "preprocessed" by the simplifier, but still, as far as I
can tell the printed name does not exist)?
- in the "[1]Rewriting:" messages, we actually just see the redex and
the contractum, but not the context of a rewrite step. Why not show the
whole terms? (One reason against this is the high redundancy and
potentially huge size of such traces, but on the other hand, they are
traces and only generated when requested.)
2) Some questions concerning the trace:
- When I explicitly use a single rule by "unfolding rule-name", why is
there more in the trace than just the application of this rule?
- Why does "apply (simp only: rule)" and "unfolding rule" behave
differently? E.g., on the term "Suc 0 = 0" with rule
"Nat.nat.distinct(2)" the former results in "False", whereas the latter
does nothing. Is it important that those two commands behave differently?
3) Furthermore, in my course I recommend students (which know about term
rewriting before) to have a look at the simplifier trace whenever the
simplifier does something unexpected or does not terminate. However, for
the latter use-case (i.e., finding cause of nontermination) I do not
even know how to do it myself in jedit. As soon as I write, e.g., "apply
simp" the simplifier starts to loop, if I don't delete the command it
continues looping (and thus the whole system becomes highly unresponsive
very soon), if I delete the command, the trace is gone too. Is there any
way (or workaround), such that I can generate (part of) the trace of a
(potentially) looping reduction. Maybe giving a timeout to "apply simp"
(but I don't know whether or how this is possible) does work?
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
