Re: [isabelle] value (code) doesn't complain when no code equations exist

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.


On 03/06/15 11:42, Lars Hupel wrote:
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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.