Email Gateway (Aug 22 2022 at 13:17): Email Gateway (Aug 22 2022 at 13:17):From: Manuel Eberl <eberlm@in.tum.de>
I think this was discussed on the mailing list a few years ago, but I
don't recall the exact details and I cannot seem to find the emails.
When using the ‘value’ command, natural numbers are printed in ‘Suc’
notation. I for one find that very inconvenient. One way to get the
system to print natural numbers as numerals is to include
Code_Target_Numeral (this works for the [code], [nbe], and [simp]
evaluators). It also makes evaluation much more efficient.
However, one does not always want to include Code_Target_Numeral
whenever one experiments with ‘value’. I just realised that the
following [code_post] rules allow nice printing of natural numbers
(although computation is still done Peano-style behind the curtain):
lemma eval_Suc_nat [code_post]:
"Suc 0 = 1"
"Suc 1 = 2"
"Suc (numeral n) = numeral (Num.inc n)"
unfolding One_nat_def numeral_inc by simp_all
declare Num.inc.simps [code_post]
However, for some reason, this does not seem to work for the [simp] and
[nbe] evaluators.
Does anyone apart from me think that something like this should be done?
Is there a way that also works for [simp] and [nbe]?
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 13:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Manuel.
I just realised that the
following [code_post] rules allow nice printing of natural numbers
(although computation is still done Peano-style behind the curtain):lemma eval_Suc_nat [code_post]:
"Suc 0 = 1"
"Suc 1 = 2"
"Suc (numeral n) = numeral (Num.inc n)"
unfolding One_nat_def numeral_inc by simp_alldeclare Num.inc.simps [code_post]
However, for some reason, this does not seem to work for the [simp] and
[nbe] evaluators.
What are the failing examples? The following works:
value [code] "Suc 42"
value [nbe] "Suc 42"
value [simp] "Suc 42"
Does anyone apart from me think that something like this should be done?
I think the only reason why nobody has ever attempted this so far is
that the old signed numerals did not allow such a simple post processing.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 13:35):From: Manuel Eberl <eberlm@in.tum.de>
What are the failing examples? The following works:
value [code] "Suc 42"
value [nbe] "Suc 42"
value [simp] "Suc 42"
Odd. I could have sworn this did not work when I tested. But it works
now, so even better.
I think the only reason why nobody has ever attempted this so far is
that the old signed numerals did not allow such a simple post processing.
Good. Then I suppose I'll add something like this soon. I am also
planning to add some code_post rules to print multisets as "{#1,2,3#}"
instead of "mset [1,2,3]".
Last updated: Nov 21 2024 at 12:39 UTC