[isabelle] Haskell Code Generator Problem with Tuple_isomorphism and (string_classes)



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).

--
  Peter







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