Re: [isabelle-dev] Nominal and FinFuns from the AFP
Precisely. Larry On 13 May 2012, at 09:44, Florian Haftmann wrote: > 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). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Locale interpretation with mixins
Hi Clemens, > What is called mixin in the implementation is a transfer principle that > is applied in addition to the interpretation morphism. Currently users > can only give equations, which yield rewrite morphisms, and > consequently, the term 'mixin' appears nowhere in the documentation. On > the other hand, the locale core 'knows' nothing about the equations. > For it, their are just general transfer principles. thanks for reminding me of that. So, an interpretation is a composition of two morphisms phi and sigma, where * phi is the instantiation morphism and * sigma is a mixin morphism Sigma in an abstract sense is generic, and, I guess, also the implementation does not make any further assumptions on it. It is exposed by two user interfaces: * the »where« clause of interpretation * the class target I deem the discussion about Tools/interpretation_with_defs.ML is mostly about user interface issues rather than generic mixin morphisms. > a) This is intentional. Mathematics is full of examples where a concept > can be defined differently (more easily) in a situation that is more > concrete. I agree. > I might have to tweak inheritance of rewrite morphisms in the > future, though, and that's why the documentation is relatively vague. Underspecification is a powerful defense shield ;-). > b) I don't yet see how one could reliably predict which equations should > be unfolded. This might be more obvious in the class package. For > interpretation, we don't even know whether a rewrite morphism is related > to a definition. I think the problem is that we would need sigma^-1 for this since we have to apply it to a subgoal rather than a plain theorem. As long as sigma does only rewriting, this is no fundamental problem. 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] 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
[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] 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
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Hi Bertram, > the Haskell code generator of Isabelle currently emits contexts for > data and newtype generates, e.g. (from CeTA): > > newtype (Linorder a) => Rbt a b = Rbt (Rbta a b); > > The sole effect of such contexts is that the programmer must provide > a (Linorder a) context wherever Rbt a b is used, which is fairly uselss. > In the next version of the Haskell language definition (whenever that > will be), this feature will be removed. > > http://www.haskell.org/pipermail/haskell-prime/2011-January/003335.html > http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts > > Ghc currently requires a flag (-XDatatypeContexts) to compile code > using datatype contexts. In the latest release (7.4.1), this option > emits a warning: > > Warning: -XDatatypeContexts is deprecated: It was widely considered a > misfeature, and has been removed from the Haskell language. > > I propose, therefore, to omit these contexts in code generated by > Isabelle. This can safely wait until after the release, of course. > (patch attached) thanks for pointing that out. Indeed, the incorporation of contexts (in Haskell speak, in Isabelle we denote this rather as sort constraints) for datatype constructors into the code generator is a relict of the early days of the code generator when I approached this story (necessarily) in a rather naive way. Since there was never a urgent pain to remove this »feature« it remained as it is. In the next months (i.e. before the release *after* Isabelle-2012) I will take care of this clean it up. 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
