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

[Andreas Lochbihler]

Hi Florian,

>> 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.
I have removed the declaration that supresses the class instance for String from 
List_lexord because of point b below and documented the problem (17d76426c7da). If 
necessary, users can issue the declaration on their own, but then it is their responsibility.

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

> String.literal has always been intended as a technical device for code
> generation rather than a full-flown first citizen.
Yes, but that's why we should care particularly about code generation and better make sure 
that the existing functions on String.literal are executable. Users are writing 
increasingly complex programs in Isabelle and they want to interface with other code and 
libraries, and String.literal is one of the basic types for exchanging data.

Andreas