Re: [isabelle-dev] [isabelle] Code_String: linorder in String.literal
Hi Andreas René, 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? It would be the canonical solution: provide a supremum for two elements in a lattice. I don't claim that it is very beautiful. 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)? Difficult. This is one of the typical problems when the syntactic shape of generated things differ from their counterparts in the logic. String.literal has always been intended as a technical device for code generation rather than a full-flown first citizen. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Lexical orders on Lists [was: Code_String: linorder in String.literal]
Just a remark on http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on lexicographic orderings in List.thy is now numerous enough but still self-contained to justify a separate theory Lexorder.thy. I would also suggest that the predicate version should be done using locales rather than the canonical type class. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Code_String: linorder in String.literal
Hi Florian, 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? It would be the canonical solution: provide a supremum for two elements in a lattice. I don't claim that it is very beautiful. I have removed the declaration that supresses the class instance for String from List_lexord because of point b below and documented the problem (17d76426c7da). If necessary, users can issue the declaration on their own, but then it is their responsibility. 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)? String.literal has always been intended as a technical device for code generation rather than a full-flown first citizen. Yes, but that's why we should care particularly about code generation and better make sure that the existing functions on String.literal are executable. Users are writing increasingly complex programs in Isabelle and they want to interface with other code and libraries, and String.literal is one of the basic types for exchanging data. Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Lexical orders on Lists [was: Code_String: linorder in String.literal]
Hi Florian,
Just a remark on
http://isabelle.in.tum.de/repos/isabelle/rev/8c0a27b9c1bd: the matter on
lexicographic orderings in List.thy is now numerous enough but still
self-contained to justify a separate theory Lexorder.thy.
I agree that a separate theory would be nice. But before doing so, we should also try to
consolidate what's there already. The current state in List.thy is as follows (8c0a27b9c1bd):
1. lexord :: ('a * 'a) set = ('a list * 'a list) set
a set version of the irreflexive lexicographic order, the parameter corresponds
to
equality of elements is determined by op =.
2. lexordp ::('a = 'a = bool) = 'a list = 'a list = bool
the predicate version of lexord, apparently used only for code generation
3. ord_class.lexordp :: 'a list = 'a list = bool
a predicate version of the irreflexive lexicographic order
equality of elements x and y is determined by ~ (x y) ~ (y x)
4. ord_class.lexordp_eq :: 'a list = 'a list = bool
a predicate version of the reflexive lexicographic order,
equality of elements x and y is determined by ~ (x y) ~ (y x)
5. lexn defines the length-lexicographic order where only lists of the same
length are comparable (listed here only for completeness).
3 and 4 also yield parametrized versions ord.lexordp and ord.lexordp_eq where the
parameter corresponds to op .
While definitions 1 to 4 yield the same when the order on the elements is linear, they
differ in the details when they are not. I think that none of 1 to 4 is optimal, because:
(i) 1 and 2 explicitly use HOL equality which need not be related to the ordering that is
passed in (e.g. in a quasi-order) -- they also make the functions dependent on the
equality type class for code generation, which is a problem for AFP/Containers.
(ii) For non-linear quasi-orders, 3 and 4 do not work well, because they consider all
unrelated elements as equal, even if they belong to different equivalence classes of the
quasi-order.
If I could start from scratch, I would define a predicate version like 4, but with
equality of x and y determined by x = y y = x. Then, however, the order parameter
would change from irreflexive to reflexive. I do not know how much breaks if we attempt
such a change.
I would also
suggest that the predicate version should be done using locales rather
than the canonical type class.
Using the canoncial type class has the advantage that I can write
lexordp_eq [1,2] [1,3]
and obtain the order on the elements implicitly. With a locale, it is more complicated to
achieve the same effect.
Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] isatest on isabelle-release
Important note: isatest is presently testing https://bitbucket.org/isabelle_project/isabelle-release again. There have been a bit too many posthoc changes for Isabelle2013-1 to trust blindly that the usual collection of isatest platforms still work. The final Isabelle2013-2 release will probably happen in 1 week. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2013-2 release
On 21.11.2013, at 10:56 pm, Makarius makar...@sketis.net wrote: Did anybody test WWW_Find? Have just confirmed that WWW_Find works fine with Isabelle2013-2-RC2 Cheers, Gerwin The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
