--- 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 {*
--- 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 *}
--- 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;