[isabelle] No code equations for explode on String.literal



Dear all,

the code generator setup for equality on String.literal seems unsatisfactory, as the following example shows:


theory Scratch imports Main begin

definition empty :: "String.literal => bool" where "empty x = (x = STR '''')"

value [nbe] "empty (STR '''')"

declare equal_literal_def [code del] (* *** *)

value [code] "empty (STR '''')"
export_code empty in SML file -


I cannot generate code for equality tests on String.literal unless I remove the code equation equal_literal_def in line ***. However, value [nbe] requires this equation in order to fully evaluate terms like "empty (STR '''')". How can we have both [code] and [nbe] work simultaneously for equality on String.literal? I tried the following, but it the problem remains the same.

declare equal_literal_def [code del, code nbe]

Shouldn't the code generator ignore [code nbe] theorems when it checks whether there are enough code equations?

Best,
Andreas




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