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



Hi René,

I have moved the lexicographic orders from Containers in the AFP to the distribution (changesets 5836854ca0a8, 8c0a27b9c1bd, a2eeeb335a48) and added your code_printing declarations in 368c70ee1f46.

Andreas

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é





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