Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Hi Bertram, just a curious question: in which context are you using the Isabelle code generator? CU, 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
[isabelle-dev] Sort constraints [was: Tweak Haskell output for future Haskell compatibility.]
Hi all,
just a synopsis of the whole matter of sort constraints for constants.
a) Sort constraints for code generation. Concerning sort constraints
and datatype constructors, everything has been said already in this
thread. Generally, for code generation sort constraints *have*
operational relevance. This is a fundamental difference to the logic
itself where there is no notion of execution.
b) Sort constraints have *no* logical relevance. Indeed, given a
definition foo :: 'a::s where
foo ['a::s] = rhs
is internally stored as
foo [?'a::{}] == rhs
which is the »most correct« form of a definition because only then it is
definitional: foo [?'a::{}] can be unfolded for arbitrary instances of
?'a . Note that foo_def carries a sort constraint for 'a; this is an
example how a specification by definition may be more special than the
underlying primitive definition, and is not restricted to sort
constraints, e.g. as in:
definition foo :: 'a::s where
P == foo ['a::s] = rhs
c) Sort constraints as syntactic device. Here the parser is instructed
to enfore sort constraints on constants.
Hope this helps,
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] Nominal and FinFuns from the AFP
Hi all, In the short term, we could move the FinFun theory into the HOL library of the development version after Isabelle 2012 and the AFP 2012 has been released, if we agree that this moves this contribution in the right direction. some remarks on my behalf: a) Ideally, tools and library theories span a product space: tools should provide configuration means such that theories »not forseen by the author« can be integrated into its scope, typically by a series of declarations. AFP library theories are a nice case study for this – if the AFP infrastructure would not allow for such organization (dependencies etc.), it does not fullfil its promise. b) In the particular case of FinFun, more and more tools seem to regard this as so fundamental (or fundamentally helpful) that incorporation into the distribution could indeed be the answer. Nevertheless, I would like to see explicit statements on this. For the moment, we have a claim for Nominal. I want to add that I would like to see a type for executable mappings in the distribution, and FinFuns seems to be the most reasonable candidate. More claims? c) I strongly object to clutter the HOL syntax even more than now by incorporating just another fancy syntax. I would prefer the lattice solution (delete syntax immediately after use and provide a library theory to optionally include it later), or maybe it is also possible to use context blocks for this (another nice case study). d) In personal conversation Alex and I discussed whether it would be preferable to swap FinFun.thy into HOL-Main and Map.thy into HOL-Library, but I don't recall the arguments in particular. 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
