always annotate potentially polymorphic Haskell numerals
authorhaftmann
Thu Sep 18 18:48:54 2014 +0200 (2014-09-18)
changeset 58400d0d3c30806b4
parent 58399 c5430cf9aa87
child 58401 b8ca69d9897b
always annotate potentially polymorphic Haskell numerals
src/HOL/Code_Numeral.thy
src/HOL/Quickcheck_Narrowing.thy
src/Tools/Code/code_haskell.ML
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Sep 18 18:48:04 2014 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Sep 18 18:48:54 2014 +0200
     1.3 @@ -538,9 +538,9 @@
     1.4  
     1.5  code_printing
     1.6    constant "0::integer" \<rightharpoonup>
     1.7 -    (SML) "0"
     1.8 +    (SML) "!(0/ :/ IntInf.int)"
     1.9      and (OCaml) "Big'_int.zero'_big'_int"
    1.10 -    and (Haskell) "0"
    1.11 +    and (Haskell) "!(0/ ::/ Integer)"
    1.12      and (Scala) "BigInt(0)"
    1.13  
    1.14  setup {*
     2.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 18 18:48:04 2014 +0200
     2.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Sep 18 18:48:54 2014 +0200
     2.3 @@ -23,6 +23,20 @@
     2.4  
     2.5  code_reserved Haskell_Quickcheck Typerep
     2.6  
     2.7 +code_printing
     2.8 +  constant "0::integer" \<rightharpoonup>
     2.9 +    (Haskell_Quickcheck) "!(0/ ::/ Prelude.Int)"
    2.10 +
    2.11 +setup {*
    2.12 +  let
    2.13 +    val target = "Haskell_Quickcheck";
    2.14 +    fun print _ = Code_Haskell.print_numeral "Prelude.Int";
    2.15 +  in
    2.16 +    Numeral.add_code @{const_name Code_Numeral.Pos} I print target
    2.17 +    #> Numeral.add_code @{const_name Code_Numeral.Neg} (op ~) print target
    2.18 +  end
    2.19 +*}
    2.20 +
    2.21  
    2.22  subsubsection {* Narrowing's deep representation of types and terms *}
    2.23  
     3.1 --- a/src/Tools/Code/code_haskell.ML	Thu Sep 18 18:48:04 2014 +0200
     3.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Sep 18 18:48:54 2014 +0200
     3.3 @@ -8,6 +8,7 @@
     3.4  sig
     3.5    val language_params: string
     3.6    val target: string
     3.7 +  val print_numeral: string -> int -> string
     3.8    val setup: theory -> theory
     3.9  end;
    3.10  
    3.11 @@ -424,17 +425,17 @@
    3.12      >> (fn (module_prefix, string_classes) =>
    3.13        serialize_haskell module_prefix string_classes));
    3.14  
    3.15 +fun print_numeral typ = Library.enclose "(" (" :: " ^ typ ^ ")") o signed_string_of_int;
    3.16 +
    3.17  val literals = let
    3.18    fun char_haskell c =
    3.19      let
    3.20        val s = ML_Syntax.print_char c;
    3.21      in if s = "'" then "\\'" else s end;
    3.22 -  fun numeral_haskell k = if k >= 0 then string_of_int k
    3.23 -    else Library.enclose "(" ")" (signed_string_of_int k);
    3.24  in Literals {
    3.25    literal_char = Library.enclose "'" "'" o char_haskell,
    3.26    literal_string = quote o translate_string char_haskell,
    3.27 -  literal_numeral = numeral_haskell,
    3.28 +  literal_numeral = print_numeral "Integer",
    3.29    literal_list = enum "," "[" "]",
    3.30    infix_cons = (5, ":")
    3.31  } end;