# HG changeset patch
# User haftmann
# Date 1411058934 -7200
# Node ID d0d3c30806b409c20e6ff280bc452d9079613d15
# Parent  c5430cf9aa8721257c1780bf9b1a6c8a3af506c5
always annotate potentially polymorphic Haskell numerals

diff -r c5430cf9aa87 -r d0d3c30806b4 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Sep 18 18:48:04 2014 +0200
+++ b/src/HOL/Code_Numeral.thy	Thu Sep 18 18:48:54 2014 +0200
@@ -538,9 +538,9 @@
 
 code_printing
   constant "0::integer" \<rightharpoonup>
-    (SML) "0"
+    (SML) "!(0/ :/ IntInf.int)"
     and (OCaml) "Big'_int.zero'_big'_int"
-    and (Haskell) "0"
+    and (Haskell) "!(0/ ::/ Integer)"
     and (Scala) "BigInt(0)"
 
 setup {*
diff -r c5430cf9aa87 -r d0d3c30806b4 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 18 18:48:04 2014 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 18 18:48:54 2014 +0200
@@ -23,6 +23,20 @@
 
 code_reserved Haskell_Quickcheck Typerep
 
+code_printing
+  constant "0::integer" \<rightharpoonup>
+    (Haskell_Quickcheck) "!(0/ ::/ Prelude.Int)"
+
+setup {*
+  let
+    val target = "Haskell_Quickcheck";
+    fun print _ = Code_Haskell.print_numeral "Prelude.Int";
+  in
+    Numeral.add_code @{const_name Code_Numeral.Pos} I print target
+    #> Numeral.add_code @{const_name Code_Numeral.Neg} (op ~) print target
+  end
+*}
+
 
 subsubsection {* Narrowing's deep representation of types and terms *}
 
diff -r c5430cf9aa87 -r d0d3c30806b4 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Sep 18 18:48:04 2014 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 18 18:48:54 2014 +0200
@@ -8,6 +8,7 @@
 sig
   val language_params: string
   val target: string
+  val print_numeral: string -> int -> string
   val setup: theory -> theory
 end;
 
@@ -424,17 +425,17 @@
     >> (fn (module_prefix, string_classes) =>
       serialize_haskell module_prefix string_classes));
 
+fun print_numeral typ = Library.enclose "(" (" :: " ^ typ ^ ")") o signed_string_of_int;
+
 val literals = let
   fun char_haskell c =
     let
       val s = ML_Syntax.print_char c;
     in if s = "'" then "\\'" else s end;
-  fun numeral_haskell k = if k >= 0 then string_of_int k
-    else Library.enclose "(" ")" (signed_string_of_int k);
 in Literals {
   literal_char = Library.enclose "'" "'" o char_haskell,
   literal_string = quote o translate_string char_haskell,
-  literal_numeral = numeral_haskell,
+  literal_numeral = print_numeral "Integer",
   literal_list = enum "," "[" "]",
   infix_cons = (5, ":")
 } end;