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
