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.

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,

# HG changeset patch
# User felgenhauer
# Date 1336397766 -7200
# Node ID 1a976d546b94ca265a26f6d916a7f54979c0c547
# Parent  29212a4bb866adc5f8f94a85602acb8dbcd65f81
do not generate contexts for datatype declarations in generated Haskell code

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

Reply via email to