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

[Andreas Lochbihler]

Hi René and Florian (and other experts in code generation),

I move this thread from users to dev because it is now getting into detailed discussions 
and commit ids.

I've moved my setup for String.literal from Containers to the distribution and pushed the 
changes to testboard), but I realised that this is not going to work for Haskell. Even 
René's simpler theory file does not produce valid Haskell code. The problem is that 
String.literal is mapped to Haskell's type String, but String is a type synonym for 
[Char]. Therefore, the Haskell compiler rejects the instantiation

   instance Orderings.Ord String where ...

because String = [Char] is not a type constructor. Such instantiations are only generated 
when we apply a polymorphic operation which depends on ord is applied to String.literal. 
For example:

   definition compare where "compare = op <"
   definition foo where "foo = compare (STR ''a'') (STR ''b'')
   export_code foo in Haskell

Overall, we have the following cases to consider when a user invokes export_code and 
String.literal is an instance of linorder.

1. 'a list is an instance of linorder using the lexicographic order as in List_lexord.
This case is simple, we could solve it by declaring to the code generator not to produce 
an instantiation for String.literal.

   code_printing class_instance String.literal :: linorder => (Haskell) -

2. 'a list is an instance of order with some order other than the lexicographic order 
(e.g., as in Library/Prefix_Order). Then, I see no way to solve the problem, because
the two terms

   compare (STR ''a'') (STR ''b'')
   compare ''a'' ''b''

produce exactly the same Haskell code, but they should evaluate differently. In 
particular, the code_printing directive from point 1 would be unsound.

3. 'a list is not an instance of ord. Then, it would be safe to produce a linorder 
instantiation for 'a list, but I doubt that the code generator provides such a facility.


Despite case 2, I am still not convinced that linorder on String.literal should require 
the lexicographic order on 'a list in the logic. So far, I have done the following:

1. Add a predicate version for a lexicographic order on lists
   (http://isabelle.in.tum.de/testboard/Isabelle/rev/8c0a27b9c1bd)

2. Setup lifting for String.literal
   (http://isabelle.in.tum.de/testboard/Isabelle/rev/a2d1522cdd54)

3. String.literal instantiates linorder in Library/Char_ord.
   (http://isabelle.in.tum.de/testboard/Isabelle/rev/a2eeeb335a48)

4. Library/Code_Char sets up the code_printing for less/less_eq on String.literal.
   (http://isabelle.in.tum.de/testboard/Isabelle/rev/368c70ee1f46)

5. Library/List_lexord issues the class_instance directive from case 1.
   (http://isabelle.in.tum.de/testboard/Isabelle/rev/4af7c82463d3)

Unfortunately, I am not completely happy with the setup for Haskell, because

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?

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

c) If List_lexord is not imported, but the type class instance for String.literal is 
required, the generated Haskell code does not compile.

Do you have any ideas or opinions on that?

Best,
Andreas


PS: Similar problems already occur for the size instance of String.linorder in 
Isabelle2013-1, so linorder is not the only problematic case.


On 19/11/13 17:32, René Neumann wrote:
> Am 19.11.2013 17:10, schrieb Andreas Lochbihler:
>> Hi René,
>>
>>> I needed linorder on String.literal, hence I came up with the theory as
>>> in the attachment. It explicitly uses lexord, and only later lifts it to
>>> op <, to explicitly show what the order is and not rely on 'magic' from
>>> the (lin)ord(er) class.
>> Your detour via lexord does not buy you anything, because your theory
>> depends on List_lexord and therefore imposes the lexicographic order on
>> lists. Unfortunately, we have two competing order instantiation for
>> lists in Isabelle (lexicographic order and prefix order). I think that
>> it is sensible to pick lexicographic orders for String.literal, but this
>> choice should restrict the choice for list (and string as the type
>> synonym for char list). In the current version, your theory forces the
>> lexicographic order on list, too.
>>
>>> It also defines op < and op <= using the target language operators (save
>>> Scala, for I don't know it) for performance reasons.
>> For Scala and the symbolic evaluation mechanisms (simp, nbe), your
>> detour via lexord cause non-termination or no code at all. Therefore,
>> you should definitely have appropriate code equations for these cases.
>>
>>> Would this be useful for inclusion in HOL/Library?
>> In general yes, but I suggest that the above issues are addressed first.
>>
>>> I also noted, that there is something similiar (minus code-printing) in
>>> AFP/Containers, but I can't tell if this is the same.
>> Yes, AFP/Containers/Lexicographic_Order is basically the same (if you
>> ignore the stuff on list fusion). It differs from your theory in the
>> following:
>>
>> 1. It avoids the dependency on List_lexord and therefore does not
>> constrain the order for list.
>> 2. It has code equations that work for all target languages and symbolic
>> evaluation.
>> 3. There are no code_printing translations.
>>
>> Hence, it might be sensible to combine your code_printing translations
>> with my definitions and add this to HOL/Library. I don't know whether it
>> is sensible to have a separate theory, I suggest that all this could go
>> into Code_Char (just like implode is also already part of Code_Char).
>
> Adding code_printing to your theory seems like the best solution for me.
> Because in trying to fix your (very plausible) remarks, I would need to
> re-develop (or copy) parts of your theory, which seems useless to me.
>
> Btw: Using "<" and "<=" in Scala directly is working too *just checked*.
>
> - René
>