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
Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Hi all, recently I thought about something which is slightly related to giving sort constraints for datatypes (but also raised a completely unrelated question). Let me just give my idea: Currently I am working on a formalization of Kruskal's Tree Theorem (but I am still far from finished ;)) which shows that when a set A is well-quasi-ordered (wqo), then the set of finite trees over A is wqo. Since the strict part of any wqo is well-founded, they can be employed in termination analysis. Moreover, every datatype represents (somehow) a set of finite trees. So if the type parameters of a datatype are restricted to wqo, we have that values of this datatype are wqo. (I guess, also here, as Tobias suggested, you can first use an unconstrained datatype and later on add the constraints by hand; but I was thinking about something like "deriving" in Haskell, where we automatically obtain an instance.) Now to the unrelated question this raised (maybe "the transfer guys" could comment): What would be the best way to prove something about "finite trees" (like Kruskal's Tree Theorem) and then obtain this result for other finite trees (like every datatype) "for free". Before I heard about the transfer machinery I thought of axiomatizing what it means to be a finite tree in a locale and do the proof inside this locale (but this seems a bit cumbersome). Is there any chance that having a proof for, lets say datatype 'a tree = Empty | Node 'a "'a tree list" to obtain the same result "for free" for any other datatype (as long as this proof only depends on the property "being a finite tree"). If this all would work out, maybe wqo could be incorporated (in addition to the existing measures) into Isabelle's termination checker (at least something similar to primrec is conceivable, where we check for tree-embedding of arguments). As I said, this is just a recent idea (which may contain several flaws). cheers chris On 05/09/2012 01:43 AM, Tobias Nipkow wrote: Am 08/05/2012 14:44, schrieb Makarius: So apart from the observation that the foundational kernel does not require sort constraints (apart from HOL.type of course), were there any reasons against them? They are not allowed in Haskell anymore, so why do we allow them (and complicate the code generation for Haskell in the future)? That was the starting point. That the kernel does not require sort constraints is not the point. Even if it did, you would still not need sort constraints in datatypes because their construction does not involve any sorts. You could always (I think) define an unconstrained datatype, even if its intended usage is in a constrained setting. I now see that there are certain extra-logical uses and accept that some people just like to explicitly constrain the usage of a datatype. Now that the machinery works smoothly, I would not suggest to remove it. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ 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.
On Tue, 8 May 2012, Tobias Nipkow wrote: Am 08/05/2012 14:44, schrieb Makarius: So apart from the observation that the foundational kernel does not require sort constraints (apart from HOL.type of course), were there any reasons against them? They are not allowed in Haskell anymore, so why do we allow them (and complicate the code generation for Haskell in the future)? That was the starting point. The expert(s) on code generation should comment on that, most notably Florian. When he made his first round on the renewed codegenerator, we changed a few things at the bottom of the logic to get sort constraints out of the way. As a consequence, primitive consts and corresponding definitional axioms have become free from sort constraints, but the results are presented to the user with constraints as expected. Makarius ___ 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.
On Tue, 8 May 2012, Makarius wrote: I did not find these ancient mails in my folders from the mid-1990-ies on the spot. At last, I've found my mail folders before the year 1996. On 29-Sep-1994 someone was pointing out that "latest" Gofer and Haskell would now support type class constraints in datatypes, observing this as a current trend in functional programming, and demanding that Isabelle/HOL would have to follow :-) This was long before I got myself involved in the datatype package, and we added the support for sort constraints in Stefan's version for other reasons than following other languges trends. I can tell further stories about the domain variant by David von Oheimb, but maybe I should stop the history session here. Makarius ___ 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.
Am 08/05/2012 14:44, schrieb Makarius: > So apart from the observation that the foundational kernel does not require > sort > constraints (apart from HOL.type of course), were there any reasons against > them? They are not allowed in Haskell anymore, so why do we allow them (and complicate the code generation for Haskell in the future)? That was the starting point. That the kernel does not require sort constraints is not the point. Even if it did, you would still not need sort constraints in datatypes because their construction does not involve any sorts. You could always (I think) define an unconstrained datatype, even if its intended usage is in a constrained setting. I now see that there are certain extra-logical uses and accept that some people just like to explicitly constrain the usage of a datatype. Now that the machinery works smoothly, I would not suggest to remove it. Tobias ___ 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.
Am 08/05/2012 13:49, schrieb Peter Lammich: > datatype a'::heap linked_list = nil | node 'a "'a linked_list ref" Actually, I think this does not do what you hope it does, hence the magic is still in there. But Lukas showed me a related defn: datatype 'a ref = Ref nat where 'a is a phantom type but for extra-logical reasons you want to restrict 'a to some type class. Extra-logical reasons can be quite compelling ;-) I'm convinced. Tobias ___ 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.
On Tue, 8 May 2012, Tobias Nipkow wrote: I mean the datatype definition facility. Over the years this lead to occasional confusion of end-users, who wanted to restrict their datatype constructors on purpose. (I can dig up an email by Elsa Gunter from the late 1990-ies, if you want.) Kudos to the experts, but my question was *why* the type constraints are supported for dataypes. What is the use case? I did not find these ancient mails in my folders from the mid-1990-ies on the spot. In a private mail to Stefan Berghofer from April 1998, I mention the problem of passing sort constraints cleanly through datatype definitions casually, as something that is already known to be supported (based on earlier discussions with users of the earlier datatype package). Anyway, without any special expertise in software archeology, a quick survey of the reachable applications of Isabelle2012 reveals this: (line 16 of "~~/src/HOL/HOLCF/Up.thy") datatype 'a u = Ibottom | Iup 'a -- "'a::cpo per default" (line 428 of "~~/src/HOL/Nitpick_Examples/Manual_Nits.thy") datatype 'a aa_tree = \ | N "'a\linorder" nat "'a aa_tree" "'a aa_tree" There are several more of the latter kind in AFP, e.g. Collections and Binomial-Heaps. I did not run the full AFP. This low frequency of usage is what I also remember over the years. More frequent issues happen when packages are built in top of other packages that attempt to disregard the standard treatment of sort constraints in Isabelle. It is also why I did the renovations last winter, because I had to explain some users in Fall historical peculiarities of HOL datatypes that were not really necessary. One also needs to understand that the foundational part of the package is the smaller one. There are many add-ons, including a general datatype interpretation mechanism, where users can define and prove further things on top of the datatypes. This complexity is the deeper reason why the datatype package is still only half localized. So apart from the observation that the foundational kernel does not require sort constraints (apart from HOL.type of course), were there any reasons against them? Makarius ___ 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.
On 05/08/2012 01:49 PM, Peter Lammich wrote:
On Di, 2012-05-08 at 12:55 +0200, Tobias Nipkow wrote:
Am 08/05/2012 12:41, schrieb Makarius:
On Tue, 8 May 2012, Tobias Nipkow wrote:
I mean the datatype definition facility.
Over the years this lead to occasional confusion of end-users, who wanted to
restrict their datatype constructors on purpose. (I can dig up an email by
Elsa Gunter from the late 1990-ies, if you want.)
It is precisely such a convincing example I am looking for. It seems to me
that such constraints restrict the types artificially: the type makes sense
without it. What is gained by the constraint?
Foundationally nothing, which is why constraints are not present in most of the
raw definitional primitives, at the bottom of the logic.
There is a difference of the foundation vs. the user context, though. (As usual
"user" means other packages or end-users connected to the surface syntax of such
packages.) The Isabelle experts in the background have spent countless years to
make all this work most of the time, such that it is rarely visible now where
things actually happen, and how.
Kudos to the experts, but my question was *why* the type constraints are
supported for dataypes. What is the use case?
One use case arises in imperative HOL, where you want to declare
datatypes that can be stored on the heap, and thus, they only make sense
if constrained to ::heap - sort. E.g.
datatype a'::heap linked_list = nil | node 'a "'a linked_list ref"
Currently, Imperative/HOL does some ML-magic after the datatype
declarations here, which certainly looks much cleaner when just adding a
sort constraint.
The mentioned ML-magic achieves two things:
First, you want to restrict 'a to be constrained to heap in the phantom
type:
datatype ('a :: heap) ref = Ref nat
Second, when defining linked lists, the restriction has to be dropped
locally,
as "valid" (user-space) type definition would require to prove the
datatype "'a node" being of sort heap interleaved with its definition in:
datatype 'a node = Empty | Node 'a "('a node) ref"
Maybe with new developments can this be achieved written in a more
"user-friendly" way, although understanding one line of ML is the least
problem in the overall confusion of this subject.
It is actually more surprising that sort constraints are imposed
(however only for convience, and not because of foundational reasons)
and can be dropped if one wishes at any point.
Lukas
Peter
Tobias
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
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.
On Di, 2012-05-08 at 12:55 +0200, Tobias Nipkow wrote: > Am 08/05/2012 12:41, schrieb Makarius: > > On Tue, 8 May 2012, Tobias Nipkow wrote: > > > >> I mean the datatype definition facility. > >> > >>> Over the years this lead to occasional confusion of end-users, who wanted > >>> to > >>> restrict their datatype constructors on purpose. (I can dig up an email > >>> by > >>> Elsa Gunter from the late 1990-ies, if you want.) > >> > >> It is precisely such a convincing example I am looking for. It seems to me > >> that such constraints restrict the types artificially: the type makes sense > >> without it. What is gained by the constraint? > > > > Foundationally nothing, which is why constraints are not present in most of > > the > > raw definitional primitives, at the bottom of the logic. > > > > There is a difference of the foundation vs. the user context, though. (As > > usual > > "user" means other packages or end-users connected to the surface syntax of > > such > > packages.) The Isabelle experts in the background have spent countless > > years to > > make all this work most of the time, such that it is rarely visible now > > where > > things actually happen, and how. > > Kudos to the experts, but my question was *why* the type constraints are > supported for dataypes. What is the use case? One use case arises in imperative HOL, where you want to declare datatypes that can be stored on the heap, and thus, they only make sense if constrained to ::heap - sort. E.g. datatype a'::heap linked_list = nil | node 'a "'a linked_list ref" Currently, Imperative/HOL does some ML-magic after the datatype declarations here, which certainly looks much cleaner when just adding a sort constraint. Peter > > Tobias > > > > > Makarius > > ___ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ 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.
Am 08/05/2012 12:41, schrieb Makarius: > On Tue, 8 May 2012, Tobias Nipkow wrote: > >> I mean the datatype definition facility. >> >>> Over the years this lead to occasional confusion of end-users, who wanted to >>> restrict their datatype constructors on purpose. (I can dig up an email by >>> Elsa Gunter from the late 1990-ies, if you want.) >> >> It is precisely such a convincing example I am looking for. It seems to me >> that such constraints restrict the types artificially: the type makes sense >> without it. What is gained by the constraint? > > Foundationally nothing, which is why constraints are not present in most of > the > raw definitional primitives, at the bottom of the logic. > > There is a difference of the foundation vs. the user context, though. (As > usual > "user" means other packages or end-users connected to the surface syntax of > such > packages.) The Isabelle experts in the background have spent countless years > to > make all this work most of the time, such that it is rarely visible now where > things actually happen, and how. Kudos to the experts, but my question was *why* the type constraints are supported for dataypes. What is the use case? Tobias > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ 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.
On Tue, 8 May 2012, Tobias Nipkow wrote: I mean the datatype definition facility. Over the years this lead to occasional confusion of end-users, who wanted to restrict their datatype constructors on purpose. (I can dig up an email by Elsa Gunter from the late 1990-ies, if you want.) It is precisely such a convincing example I am looking for. It seems to me that such constraints restrict the types artificially: the type makes sense without it. What is gained by the constraint? Foundationally nothing, which is why constraints are not present in most of the raw definitional primitives, at the bottom of the logic. There is a difference of the foundation vs. the user context, though. (As usual "user" means other packages or end-users connected to the surface syntax of such packages.) The Isabelle experts in the background have spent countless years to make all this work most of the time, such that it is rarely visible now where things actually happen, and how. Makarius ___ 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.
Am 08/05/2012 12:01, schrieb Makarius:
> On Tue, 8 May 2012, Tobias Nipkow wrote:
>
>> This is an interesting issue. I would like to know if we need class
>> constraints for datatype parameters in the first place. I thought we had
>> agreed at some point (not on this list) to get rid of them, but we never did.
>> Maybe there are situations where you need them? The only one that comes to my
>> mind is the following: you define some type "('a::C) t" by a typedef and then
>> make it into a datatype by hand (via rep_datatype). Now you can use it inside
>> a datatype definition. Do we have a (conceivable) example of this situation?
>
> Are you speaking about the actual definitional package, or its adjoined
> code-generator?
>
I mean the datatype definition facility.
> In ancient times, the datatype package did not treat sort constraints at all.
> It was not required for the logical foundations of the construction, and it
> was
> not yet clear how to write such packages properly. I.e. all the now standard
> ways of processing input, type-checking it, passing around parameters etc.
> were
> not yet established.
>
> Over the years this lead to occasional confusion of end-users, who wanted to
> restrict their datatype constructors on purpose. (I can dig up an email by
> Elsa
> Gunter from the late 1990-ies, if you want.)
It is precisely such a convincing example I am looking for. It seems to me that
such constraints restrict the types artificially: the type makes sense without
it. What is gained by the constraint?
Tobias
> There was additional confusion in packages built on top of datatype, because
> of
> incompatibilities of the way its input is specified. We have spent many years
> to reform all this, to keep the datatype package up-to-date. I've made the
> last
> reforms in the Christmas vacation 2011/2012, so that the NEWS for Isabelle2012
> can now say:
>
> * Datatype: type parameters allow explicit sort constraints.
>
> This is only a trivial consequence of straightening, clarifying, simplifying
> all
> the internal layers of these packages.
>
>
> Of course, the code generator can ignore sort constraints on its own, without
> affecting any of the specification packages.
>
>
> Makarius
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
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.
On Tue, 8 May 2012, Tobias Nipkow wrote:
This is an interesting issue. I would like to know if we need class
constraints for datatype parameters in the first place. I thought we had
agreed at some point (not on this list) to get rid of them, but we never
did. Maybe there are situations where you need them? The only one that
comes to my mind is the following: you define some type "('a::C) t" by a
typedef and then make it into a datatype by hand (via rep_datatype). Now
you can use it inside a datatype definition. Do we have a (conceivable)
example of this situation?
Are you speaking about the actual definitional package, or its adjoined
code-generator?
In ancient times, the datatype package did not treat sort constraints at
all. It was not required for the logical foundations of the construction,
and it was not yet clear how to write such packages properly. I.e. all
the now standard ways of processing input, type-checking it, passing
around parameters etc. were not yet established.
Over the years this lead to occasional confusion of end-users, who wanted
to restrict their datatype constructors on purpose. (I can dig up an
email by Elsa Gunter from the late 1990-ies, if you want.)
There was additional confusion in packages built on top of datatype,
because of incompatibilities of the way its input is specified. We have
spent many years to reform all this, to keep the datatype package
up-to-date. I've made the last reforms in the Christmas vacation
2011/2012, so that the NEWS for Isabelle2012 can now say:
* Datatype: type parameters allow explicit sort constraints.
This is only a trivial consequence of straightening, clarifying,
simplifying all the internal layers of these packages.
Of course, the code generator can ignore sort constraints on its own,
without affecting any of the specification packages.
Makarius
___
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.
This is an interesting issue. I would like to know if we need class constraints
for datatype parameters in the first place. I thought we had agreed at some
point (not on this list) to get rid of them, but we never did. Maybe there are
situations where you need them? The only one that comes to my mind is the
following: you define some type "('a::C) t" by a typedef and then make it into a
datatype by hand (via rep_datatype). Now you can use it inside a datatype
definition. Do we have a (conceivable) example of this situation?
Tobias
Am 07/05/2012 16:02, schrieb Bertram Felgenhauer:
> Dear Isabelle developers,
>
> 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)
>
> Best regards,
>
> Bertram
>
>
>
> This body part will be downloaded on demand.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Dear Isabelle developers, 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) Best regards, Bertram # HG changeset patch # User felgenhauer # Date 1336397766 -7200 # Node ID 1a976d546b94ca265a26f6d916a7f54979c0c547 # Parent 29212a4bb866adc5f8f94a85602acb8dbcd65f81 do not generate contexts for datatype declarations in generated Haskell code (see http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts) diff -r 29212a4bb866 -r 1a976d546b94 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Fri May 04 17:12:37 2012 +0200 +++ b/src/Tools/Code/code_haskell.ML Mon May 07 15:36:06 2012 +0200 @@ -57,7 +57,7 @@ | SOME (_, print) => print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; fun print_typdecl tyvars (vs, tycoexpr) = - Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); + print_tyco_expr tyvars NOBR tycoexpr; fun print_typscheme tyvars (vs, ty) = Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty); fun print_term tyvars some_thm vars fxy (IConst c) = ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
