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



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é

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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