1.1 --- a/src/HOL/Code_Numeral.thy Fri Jan 22 13:38:28 2010 +0100
1.2 +++ b/src/HOL/Code_Numeral.thy Fri Jan 22 13:38:28 2010 +0100
1.3 @@ -296,15 +296,14 @@
1.4
1.5 setup {*
1.6 fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
1.7 - false false Code_Printer.str) ["SML", "Haskell"]
1.8 + false Code_Printer.literal_naive_numeral) ["SML", "Haskell"]
1.9 #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
1.10 - false true Code_Printer.str "OCaml"
1.11 + false Code_Printer.literal_numeral "OCaml"
1.12 #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
1.13 - false false Code_Printer.str "Scala"
1.14 + false Code_Printer.literal_naive_numeral "Scala"
1.15 *}
1.16
1.17 code_reserved SML Int int
1.18 -code_reserved OCaml Big_int
1.19 code_reserved Scala Int
1.20
1.21 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
2.1 --- a/src/HOL/Library/Code_Integer.thy Fri Jan 22 13:38:28 2010 +0100
2.2 +++ b/src/HOL/Library/Code_Integer.thy Fri Jan 22 13:38:28 2010 +0100
2.3 @@ -25,9 +25,9 @@
2.4
2.5 setup {*
2.6 fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
2.7 - true true Code_Printer.str) ["SML", "OCaml", "Haskell", "Scala"]
2.8 + true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
2.9 #> Numeral.add_code @{const_name number_int_inst.number_of_int}
2.10 - true true (fn s => (Pretty.block o map Code_Printer.str) ["BigInt", s]) "Scala"
2.11 + true Code_Printer.literal_numeral "Scala"
2.12 *}
2.13
2.14 code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
2.15 @@ -88,7 +88,7 @@
2.16 code_const pdivmod
2.17 (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
2.18 (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
2.19 - (Haskell "divMod/ (abs _)/ (abs _))")
2.20 + (Haskell "divMod/ (abs _)/ (abs _)")
2.21 (Scala "!(_.abs '/% _.abs)")
2.22
2.23 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
2.24 @@ -113,10 +113,7 @@
2.25 (SML "IntInf.fromInt")
2.26 (OCaml "_")
2.27 (Haskell "toEnum")
2.28 - (Scala "!BigInt(_)")
2.29 -
2.30 -code_reserved SML IntInf
2.31 -code_reserved Scala BigInt
2.32 + (Scala "!BigInt((_))")
2.33
2.34 text {* Evaluation *}
2.35
3.1 --- a/src/HOL/Library/Efficient_Nat.thy Fri Jan 22 13:38:28 2010 +0100
3.2 +++ b/src/HOL/Library/Efficient_Nat.thy Fri Jan 22 13:38:28 2010 +0100
3.3 @@ -287,6 +287,8 @@
3.4 code_reserved Haskell Nat
3.5
3.6 code_include Scala "Nat" {*
3.7 +import scala.Math
3.8 +
3.9 object Nat {
3.10
3.11 def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
3.12 @@ -309,7 +311,9 @@
3.13 def equals(that: Nat): Boolean = this.value == that.value
3.14
3.15 def as_BigInt: BigInt = this.value
3.16 - def as_Int: Int = this.value
3.17 + def as_Int: Int = if (this.value >= Math.MAX_INT && this.value <= Math.MAX_INT)
3.18 + this.value.intValue
3.19 + else error("Int value too big:" + this.value.toString)
3.20
3.21 def +(that: Nat): Nat = new Nat(this.value + that.value)
3.22 def -(that: Nat): Nat = Nat(this.value + that.value)
3.23 @@ -348,9 +352,9 @@
3.24
3.25 setup {*
3.26 fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
3.27 - false true Code_Printer.str) ["SML", "OCaml", "Haskell"]
3.28 + false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
3.29 #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
3.30 - false true (fn s => (Pretty.block o map Code_Printer.str) ["Nat.Nat", s]) "Scala"
3.31 + false Code_Printer.literal_positive_numeral "Scala"
3.32 *}
3.33
3.34 text {*
4.1 --- a/src/HOL/Tools/numeral.ML Fri Jan 22 13:38:28 2010 +0100
4.2 +++ b/src/HOL/Tools/numeral.ML Fri Jan 22 13:38:28 2010 +0100
4.3 @@ -8,7 +8,7 @@
4.4 sig
4.5 val mk_cnumeral: int -> cterm
4.6 val mk_cnumber: ctyp -> int -> cterm
4.7 - val add_code: string -> bool -> bool -> (string -> Pretty.T) -> string -> theory -> theory
4.8 + val add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
4.9 end;
4.10
4.11 structure Numeral: NUMERAL =
4.12 @@ -56,7 +56,7 @@
4.13
4.14 local open Basic_Code_Thingol in
4.15
4.16 -fun add_code number_of negative unbounded print target thy =
4.17 +fun add_code number_of negative print target thy =
4.18 let
4.19 fun dest_numeral pls' min' bit0' bit1' thm =
4.20 let
4.21 @@ -74,8 +74,7 @@
4.22 | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
4.23 in dest_num end;
4.24 fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
4.25 - (print o Code_Printer.literal_numeral literals unbounded
4.26 - o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
4.27 + (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
4.28 in
4.29 thy |> Code_Target.add_syntax_const target number_of
4.30 (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
5.1 --- a/src/Tools/Code/code_haskell.ML Fri Jan 22 13:38:28 2010 +0100
5.2 +++ b/src/Tools/Code/code_haskell.ML Fri Jan 22 13:38:28 2010 +0100
5.3 @@ -401,11 +401,14 @@
5.4 let
5.5 val s = ML_Syntax.print_char c;
5.6 in if s = "'" then "\\'" else s end;
5.7 + fun numeral_haskell k = if k >= 0 then string_of_int k
5.8 + else Library.enclose "(" ")" (signed_string_of_int k);
5.9 in Literals {
5.10 literal_char = Library.enclose "'" "'" o char_haskell,
5.11 literal_string = quote o translate_string char_haskell,
5.12 - literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
5.13 - else Library.enclose "(" ")" (signed_string_of_int k),
5.14 + literal_numeral = numeral_haskell,
5.15 + literal_positive_numeral = numeral_haskell,
5.16 + literal_naive_numeral = numeral_haskell,
5.17 literal_list = enum "," "[" "]",
5.18 infix_cons = (5, ":")
5.19 } end;
6.1 --- a/src/Tools/Code/code_ml.ML Fri Jan 22 13:38:28 2010 +0100
6.2 +++ b/src/Tools/Code/code_ml.ML Fri Jan 22 13:38:28 2010 +0100
6.3 @@ -354,9 +354,9 @@
6.4 val literals_sml = Literals {
6.5 literal_char = prefix "#" o quote o ML_Syntax.print_char,
6.6 literal_string = quote o translate_string ML_Syntax.print_char,
6.7 - literal_numeral = fn unbounded => fn k =>
6.8 - if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
6.9 - else string_of_int k,
6.10 + literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
6.11 + literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
6.12 + literal_naive_numeral = string_of_int,
6.13 literal_list = enum "," "[" "]",
6.14 infix_cons = (7, "::")
6.15 };
6.16 @@ -687,18 +687,17 @@
6.17 val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
6.18 then chr i else c
6.19 in s end;
6.20 - fun bignum_ocaml k = if k <= 1073741823
6.21 - then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
6.22 - else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
6.23 + fun numeral_ocaml k = if k < 0
6.24 + then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
6.25 + else if k <= 1073741823
6.26 + then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
6.27 + else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
6.28 in Literals {
6.29 literal_char = Library.enclose "'" "'" o char_ocaml,
6.30 literal_string = quote o translate_string char_ocaml,
6.31 - literal_numeral = fn unbounded => fn k => if k >= 0 then
6.32 - if unbounded then bignum_ocaml k
6.33 - else string_of_int k
6.34 - else
6.35 - if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")"
6.36 - else (Library.enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
6.37 + literal_numeral = numeral_ocaml,
6.38 + literal_positive_numeral = numeral_ocaml,
6.39 + literal_naive_numeral = numeral_ocaml,
6.40 literal_list = enum ";" "[" "]",
6.41 infix_cons = (6, "::")
6.42 } end;
6.43 @@ -975,7 +974,7 @@
6.44 ]))
6.45 #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
6.46 #> fold (Code_Target.add_reserved target_SML)
6.47 - ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
6.48 + ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
6.49 #> fold (Code_Target.add_reserved target_OCaml) [
6.50 "and", "as", "assert", "begin", "class",
6.51 "constraint", "do", "done", "downto", "else", "end", "exception",
6.52 @@ -985,6 +984,6 @@
6.53 "sig", "struct", "then", "to", "true", "try", "type", "val",
6.54 "virtual", "when", "while", "with"
6.55 ]
6.56 - #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod"];
6.57 + #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];
6.58
6.59 end; (*struct*)
7.1 --- a/src/Tools/Code/code_printer.ML Fri Jan 22 13:38:28 2010 +0100
7.2 +++ b/src/Tools/Code/code_printer.ML Fri Jan 22 13:38:28 2010 +0100
7.3 @@ -39,12 +39,15 @@
7.4
7.5 type literals
7.6 val Literals: { literal_char: string -> string, literal_string: string -> string,
7.7 - literal_numeral: bool -> int -> string,
7.8 + literal_numeral: int -> string, literal_positive_numeral: int -> string,
7.9 + literal_naive_numeral: int -> string,
7.10 literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
7.11 -> literals
7.12 val literal_char: literals -> string -> string
7.13 val literal_string: literals -> string -> string
7.14 - val literal_numeral: literals -> bool -> int -> string
7.15 + val literal_numeral: literals -> int -> string
7.16 + val literal_positive_numeral: literals -> int -> string
7.17 + val literal_naive_numeral: literals -> int -> string
7.18 val literal_list: literals -> Pretty.T list -> Pretty.T
7.19 val infix_cons: literals -> int * string
7.20
7.21 @@ -163,7 +166,9 @@
7.22 datatype literals = Literals of {
7.23 literal_char: string -> string,
7.24 literal_string: string -> string,
7.25 - literal_numeral: bool -> int -> string,
7.26 + literal_numeral: int -> string,
7.27 + literal_positive_numeral: int -> string,
7.28 + literal_naive_numeral: int -> string,
7.29 literal_list: Pretty.T list -> Pretty.T,
7.30 infix_cons: int * string
7.31 };
7.32 @@ -173,6 +178,8 @@
7.33 val literal_char = #literal_char o dest_Literals;
7.34 val literal_string = #literal_string o dest_Literals;
7.35 val literal_numeral = #literal_numeral o dest_Literals;
7.36 +val literal_positive_numeral = #literal_positive_numeral o dest_Literals;
7.37 +val literal_naive_numeral = #literal_naive_numeral o dest_Literals;
7.38 val literal_list = #literal_list o dest_Literals;
7.39 val infix_cons = #infix_cons o dest_Literals;
7.40
8.1 --- a/src/Tools/Code/code_scala.ML Fri Jan 22 13:38:28 2010 +0100
8.2 +++ b/src/Tools/Code/code_scala.ML Fri Jan 22 13:38:28 2010 +0100
8.3 @@ -404,17 +404,18 @@
8.4 let
8.5 val s = ML_Syntax.print_char c;
8.6 in if s = "'" then "\\'" else s end;
8.7 - fun bigint_scala k = "(" ^ (if k <= 2147483647
8.8 - then string_of_int k else quote (string_of_int k)) ^ ")"
8.9 + fun numeral_scala k = if k < 0
8.10 + then if k <= 2147483647 then "- " ^ string_of_int (~ k)
8.11 + else quote ("- " ^ string_of_int (~ k))
8.12 + else if k <= 2147483647 then string_of_int k
8.13 + else quote (string_of_int k)
8.14 in Literals {
8.15 literal_char = Library.enclose "'" "'" o char_scala,
8.16 literal_string = quote o translate_string char_scala,
8.17 - literal_numeral = fn unbounded => fn k => if k >= 0 then
8.18 - if unbounded then bigint_scala k
8.19 - else Library.enclose "(" ")" (string_of_int k)
8.20 - else
8.21 - if unbounded then "(- " ^ bigint_scala (~ k) ^ ")"
8.22 - else Library.enclose "(" ")" (signed_string_of_int k),
8.23 + literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
8.24 + literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
8.25 + literal_naive_numeral = fn k => if k >= 0
8.26 + then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
8.27 literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
8.28 infix_cons = (6, "::")
8.29 } end;
8.30 @@ -442,7 +443,7 @@
8.31 "true", "type", "val", "var", "while", "with"
8.32 ]
8.33 #> fold (Code_Target.add_reserved target) [
8.34 - "error", "apply", "List", "Nil"
8.35 + "error", "apply", "List", "Nil", "BigInt"
8.36 ];
8.37
8.38 end; (*struct*)