Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 11:15):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,

the following works:

Lemma "***" should be part of the default setup, I will look after it.

Cheers,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 11:21):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Last updated: Apr 16 2024 at 16:19 UTC