Email Gateway (Aug 22 2022 at 10:29): Email Gateway (Aug 22 2022 at 10:29):From: Lars Hupel <hupel@in.tum.de>
Dear list,
it appears that 'value' sometimes performs a (silent) fallback on other
evaluators if something goes wrong. I don't understand the precise
mechanics there, but one particular annoying instance is that when no
code equations exist for some constant, 'value (code)' will leave it
unevaluated, whereas the corresponding ML code
ML‹Code_Evaluation.dynamic_conv @{context} @{cterm foo}›
will print an error message
No code equations for foo
It took me a while of debugging to figure out why 'value' didn't
evaluate my term fully.
What's the reasoning behind this?
Cheers
Lars
Email Gateway (Aug 22 2022 at 10:29):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Lars,
value without options tries different evaluation mechanisms (code and nbe IIRC), and nbe
can handle constants without code equations - it just leaves them uninterpreted.
Therefore, no error message occurs. If you just want to use the code generator for
evaluation, you explicitly have to say so:
value [code] "expression"
Then, you also get the expected error message if code equations are missing. Similarly,
[nbe] lets you choose nbe as evaluation strategy.
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:29):From: Lars Hupel <hupel@in.tum.de>
value [code] "expression"
Thanks, that was the missing bit: I was using wrong syntax! I thought
that 'value (code)' was the way to select the evaluation strategy, but
in fact, I can write anything there ... 'value (foobar)' gets happily
accepted :-)
Cheers
Lars
Email Gateway (Aug 22 2022 at 10:29):From: "C. Diekmann" <diekmann@in.tum.de>
Why did I also use value(code) all the time? Was this in some release candidate?
find ./ -name '*.thy' | xargs grep 'value(code)' | wc -l
25
This explains a lot! Thanks!
Cornelius
Email Gateway (Aug 22 2022 at 10:30):From: Lars Hupel <hupel@in.tum.de>
I might have told you ;-)
Email Gateway (Aug 22 2022 at 10:32):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
To make it clear: ( ) denotes a print mode:
value [nbe] (iff) "(P::bool) ⟷ Q"
value [nbe] ("iff, xsymbols") "(P::bool) ⟷ Q"
value [nbe] "(P::bool) ⟷ Q"
signature.asc
Last updated: Apr 20 2024 at 01:05 UTC