[isabelle-dev] [isabelle] Code_String: linorder in String.literal

[Florian Haftmann]

Hi Andreas & René,

> a) Char_ord and List_lexord are not tied together, i.e., a user could
> import List_lexord, but not Char_ord, define his own version of order on
> String.literal and the generated Haskell code compiles, but it is
> unsound (even without any further adaptations by the user). One could
> solve this by moving the directive from commit 5 to a new theory
> Char_ord_List_lexord that imports both Char_ord and List_lexord -- but
> is this sensible?

It would be the canonical solution: provide a supremum for two elements
in a lattice.  I don't claim that it is very beautiful.

> b) If both Code_Char and List_lexord are imported, but class instances
> for ord are only required for String.literal and not for lists, the code
> generator produces no instantiation at all, i.e., the generated code
> does not compile. Is there any possibility to tell the code generator
> that if a program needs an instance for String.literal, then it also
> needs one for 'a list (but only for Haskell, because we don't want to
> force users to have any ordering on list)?

Difficult.  This is one of the typical problems when the syntactic shape
of generated things differ from their counterparts in the logic.

String.literal has always been intended as a technical device for code
generation rather than a full-flown first citizen.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de