Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Haskell Code Generator Problem with Tuple_isom...

Email Gateway (Aug 18 2022 at 14:24):

From: Peter Lammich <peter.lammich@uni-muenster.de>
When using records and the (string_classes) option, the Haskell code
generator generates the following code (in module Record):
[...]
data Tuple_isomorphism a b c = TupleIsomorphism (a -> (b, c)) ((b, c) -> a)
deriving (Read, Show);
[...]

This causes ghc to complain:
generated/Ta.hs:240:12:
No instances for (Read ((b, c) -> a), Read (a -> (b, c)))
arising from the 'deriving' clause of a data type declaration
at generated/Ta.hs:240:12-15
Possible fix:
add an instance declaration for
(Read ((b, c) -> a), Read (a -> (b, c)))
or use a standalone 'deriving instance' declaration instead,
so you can specify the instance context yourself
When deriving the instance for (Read (Tuple_isomorphism a b c))

generated/Ta.hs:240:18:
No instances for (Show ((b, c) -> a), Show (a -> (b, c)))
arising from the 'deriving' clause of a data type declaration
at generated/Ta.hs:240:18-21
Possible fix:
add an instance declaration for
(Show ((b, c) -> a), Show (a -> (b, c)))
or use a standalone 'deriving instance' declaration instead,
so you can specify the instance context yourself
When deriving the instance for (Show (Tuple_isomorphism a b c))

The example was taken from the code generated by
afp/Tree-Automata/Ta_impl_codegen.thy,
but the same invalid code seems to be generated when using any record
with (string-classes).

Email Gateway (Aug 18 2022 at 14:25):

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

the (string_classes) option indeed has never been used widely, and it is
a little bit crude (although after having a look at the code I must
admit that it is broken now altogether). If there is really a "proper"
use of this, I have to think about a inner-logical solution to the
problem (which is not that difficult).

If this issue is mission-critical for you now, we can discuss possible
solutions separately from the mailing list.

Cheers,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC