Re: [isabelle] Code_String: linorder in String.literal



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

Any opinions?

Andreas




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