1.1 --- a/NEWS	Mon Jul 23 09:26:55 2012 +0200
     1.2 +++ b/NEWS	Mon Jul 23 09:28:03 2012 +0200
     1.3 @@ -15,6 +15,9 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Code generation for Haskell: restrict unqualified imports from
     1.8 +Haskell Prelude to a small set of fundamental operations.
     1.9 +
    1.10  * Command "export_code": relative file names are interpreted
    1.11  relatively to master directory of current theory rather than
    1.12  the rather arbitrary current working directory.

     2.1 --- a/src/HOL/Code_Numeral.thy	Mon Jul 23 09:26:55 2012 +0200
     2.2 +++ b/src/HOL/Code_Numeral.thy	Mon Jul 23 09:28:03 2012 +0200
     2.3 @@ -298,7 +298,7 @@
     2.4  code_const "minus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
     2.5    (SML "Int.max/ (0 : int,/ Int.-/ ((_),/ (_)))")
     2.6    (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)")
     2.7 -  (Haskell "max/ (0 :: Integer)/ (_/ -/ _)")
     2.8 +  (Haskell "Prelude.max/ (0 :: Integer)/ (_/ -/ _)")
     2.9    (Scala "!(_/ -/ _).max(0)")
    2.10    (Eval "Integer.max/ 0/ (_/ -/ _)")
    2.11  

     3.1 --- a/src/HOL/Library/Code_Char.thy	Mon Jul 23 09:26:55 2012 +0200
     3.2 +++ b/src/HOL/Library/Code_Char.thy	Mon Jul 23 09:28:03 2012 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  code_type char
     3.5    (SML "char")
     3.6    (OCaml "char")
     3.7 -  (Haskell "Char")
     3.8 +  (Haskell "Prelude.Char")
     3.9    (Scala "Char")
    3.10  
    3.11  setup {*
    3.12 @@ -58,7 +58,4 @@
    3.13    (Haskell "_")
    3.14    (Scala "!(_.toList)")
    3.15  
    3.16 -
    3.17 -(*declare Quickcheck_Exhaustive.char.bounded_forall_char.simps [code del]*)
    3.18 -
    3.19  end

     4.1 --- a/src/HOL/Library/Code_Char_chr.thy	Mon Jul 23 09:26:55 2012 +0200
     4.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Mon Jul 23 09:28:03 2012 +0200
     4.3 @@ -25,7 +25,7 @@
     4.4  code_const int_of_char and char_of_int
     4.5    (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
     4.6    (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
     4.7 -  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)")
     4.8 +  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
     4.9    (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
    4.10  
    4.11  end

     5.1 --- a/src/HOL/Library/Code_Integer.thy	Mon Jul 23 09:26:55 2012 +0200
     5.2 +++ b/src/HOL/Library/Code_Integer.thy	Mon Jul 23 09:28:03 2012 +0200
     5.3 @@ -151,7 +151,7 @@
     5.4  code_const Code_Numeral.int_of
     5.5    (SML "IntInf.fromInt")
     5.6    (OCaml "_")
     5.7 -  (Haskell "toInteger")
     5.8 +  (Haskell "Prelude.toInteger")
     5.9    (Scala "!_.as'_BigInt")
    5.10    (Eval "_")
    5.11  

     6.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 23 09:26:55 2012 +0200
     6.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Jul 23 09:28:03 2012 +0200
     6.3 @@ -162,7 +162,7 @@
     6.4  text {* For Haskell and Scala, things are slightly different again. *}
     6.5  
     6.6  code_const int and nat
     6.7 -  (Haskell "toInteger" and "fromInteger")
     6.8 +  (Haskell "Prelude.toInteger" and "Prelude.fromInteger")
     6.9    (Scala "!_.as'_BigInt" and "Nat")
    6.10  
    6.11  text {* Alternativ implementation for @{const of_nat} *}
    6.12 @@ -189,14 +189,14 @@
    6.13  code_const Code_Numeral.of_nat
    6.14    (SML "IntInf.toInt")
    6.15    (OCaml "_")
    6.16 -  (Haskell "!(fromInteger/ ./ toInteger)")
    6.17 +  (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
    6.18    (Scala "!Natural(_.as'_BigInt)")
    6.19    (Eval "_")
    6.20  
    6.21  code_const Code_Numeral.nat_of
    6.22    (SML "IntInf.fromInt")
    6.23    (OCaml "_")
    6.24 -  (Haskell "!(fromInteger/ ./ toInteger)")
    6.25 +  (Haskell "!(Prelude.fromInteger/ ./ Prelude.toInteger)")
    6.26    (Scala "!Nat(_.as'_BigInt)")
    6.27    (Eval "_")
    6.28  

     7.1 --- a/src/Tools/Code/code_haskell.ML	Mon Jul 23 09:26:55 2012 +0200
     7.2 +++ b/src/Tools/Code/code_haskell.ML	Mon Jul 23 09:28:03 2012 +0200
     7.3 @@ -303,6 +303,27 @@
     7.4          modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
     7.5    end;
     7.6  
     7.7 +val prelude_import_operators = [
     7.8 +  "==", "/=", "<", "<=", ">=", ">", "+", "-", "*", "/", "**", ">>=", ">>", "=<<", "&&", "||", "^", "^^", ".", "$", "$!", "++", "!!"
     7.9 +];
    7.10 +
    7.11 +val prelude_import_unqualified = [
    7.12 +  "Eq",
    7.13 +  "error",
    7.14 +  "id",
    7.15 +  "return",
    7.16 +  "not",
    7.17 +  "fst", "snd",
    7.18 +  "map", "filter", "concat", "concatMap", "reverse", "zip", "null", "takeWhile", "dropWhile", "all", "any",
    7.19 +  "Integer", "negate", "abs", "divMod",
    7.20 +  "String"
    7.21 +];
    7.22 +
    7.23 +val prelude_import_unqualified_constr = [
    7.24 +  ("Bool", ["True", "False"]),
    7.25 +  ("Maybe", ["Nothing", "Just"])
    7.26 +];
    7.27 +
    7.28  fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms,
    7.29      includes, module_alias, class_syntax, tyco_syntax, const_syntax } program =
    7.30    let
    7.31 @@ -331,23 +352,28 @@
    7.32        deresolve (if string_classes then deriving_show else K false);
    7.33  
    7.34      (* print modules *)
    7.35 -    val import_includes_ps =
    7.36 -      map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes;
    7.37      fun print_module_frame module_name ps =
    7.38        (module_name, Pretty.chunks2 (
    7.39          str ("module " ^ module_name ^ " where {")
    7.40          :: ps
    7.41          @| str "}"
    7.42        ));
    7.43 +    fun print_qualified_import module_name = semicolon [str "import qualified", str module_name];
    7.44 +    val import_common_ps =
    7.45 +      enclose "import Prelude (" ");" (commas (map str
    7.46 +        (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
    7.47 +          @ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
    7.48 +      :: print_qualified_import "Prelude"
    7.49 +      :: map (print_qualified_import o fst) includes;
    7.50      fun print_module module_name (gr, imports) =
    7.51        let
    7.52 -        val deresolve = deresolver module_name
    7.53 +        val deresolve = deresolver module_name;
    7.54          fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
    7.55 -        val import_ps = import_includes_ps @ map (print_import o fst) imports;
    7.56 -        fun print_stmt' gr name = case Graph.get_node gr name
    7.57 +        val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
    7.58 +        fun print_stmt' name = case Graph.get_node gr name
    7.59           of (_, NONE) => NONE
    7.60            | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
    7.61 -        val body_ps = map_filter (print_stmt' gr) ((flat o rev o Graph.strong_conn) gr);
    7.62 +        val body_ps = map_filter print_stmt' ((flat o rev o Graph.strong_conn) gr);
    7.63        in
    7.64          print_module_frame module_name
    7.65            ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
    7.66 @@ -472,55 +498,8 @@
    7.67        "import", "default", "forall", "let", "in", "class", "qualified", "data",
    7.68        "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
    7.69      ]
    7.70 -  #> fold (Code_Target.add_reserved target) [
    7.71 -      "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
    7.72 -      "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
    7.73 -      "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
    7.74 -      "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
    7.75 -      "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
    7.76 -      "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
    7.77 -      "ExitSuccess", "False", "GT", "HeapOverflow",
    7.78 -      "IOError", "IOException", "IllegalOperation",
    7.79 -      "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
    7.80 -      "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
    7.81 -      "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
    7.82 -      "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
    7.83 -      "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
    7.84 -      "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
    7.85 -      "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
    7.86 -      "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
    7.87 -      "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
    7.88 -      "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
    7.89 -      "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
    7.90 -      "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
    7.91 -      "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
    7.92 -      "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
    7.93 -      "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
    7.94 -      "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
    7.95 -      "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
    7.96 -      "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
    7.97 -      "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
    7.98 -      "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
    7.99 -      "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
   7.100 -      "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
   7.101 -      "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
   7.102 -      "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
   7.103 -      "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
   7.104 -      "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred", 
   7.105 -      "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
   7.106 -      "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
   7.107 -      "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
   7.108 -      "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
   7.109 -      "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
   7.110 -      "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
   7.111 -      "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
   7.112 -      "sequence_", "show", "showChar", "showException", "showField", "showList",
   7.113 -      "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
   7.114 -      "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
   7.115 -      "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
   7.116 -      "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
   7.117 -      "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
   7.118 -      "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
   7.119 -    ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
   7.120 +  #> fold (Code_Target.add_reserved target) prelude_import_unqualified
   7.121 +  #> fold (Code_Target.add_reserved target o fst) prelude_import_unqualified_constr
   7.122 +  #> fold (fold (Code_Target.add_reserved target) o snd) prelude_import_unqualified_constr;
   7.123  
   7.124  end; (*struct*)