1.1 --- a/src/HOL/Code_Numeral.thy Fri Jul 23 18:42:46 2010 +0200
1.2 +++ b/src/HOL/Code_Numeral.thy Sat Jul 24 18:08:41 2010 +0200
1.3 @@ -123,7 +123,7 @@
1.4 by (rule HOL.eq_refl)
1.5
1.6
1.7 -subsection {* Indices as datatype of ints *}
1.8 +subsection {* Code numerals as datatype of ints *}
1.9
1.10 instantiation code_numeral :: number
1.11 begin
1.12 @@ -293,67 +293,74 @@
1.13
1.14 subsection {* Code generator setup *}
1.15
1.16 -text {* Implementation of indices by bounded integers *}
1.17 +text {* Implementation of code numerals by bounded integers *}
1.18
1.19 code_type code_numeral
1.20 (SML "int")
1.21 (OCaml "Big'_int.big'_int")
1.22 (Haskell "Integer")
1.23 - (Scala "Int")
1.24 + (Scala "BigInt")
1.25
1.26 code_instance code_numeral :: eq
1.27 (Haskell -)
1.28
1.29 setup {*
1.30 - fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
1.31 - false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
1.32 + Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
1.33 + false Code_Printer.literal_naive_numeral "SML"
1.34 #> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
1.35 - false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
1.36 + false Code_Printer.literal_numeral) ["OCaml", "Haskell", "Scala"]
1.37 *}
1.38
1.39 code_reserved SML Int int
1.40 -code_reserved Scala Int
1.41 +code_reserved Eval Integer
1.42
1.43 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
1.44 (SML "Int.+/ ((_),/ (_))")
1.45 (OCaml "Big'_int.add'_big'_int")
1.46 (Haskell infixl 6 "+")
1.47 (Scala infixl 7 "+")
1.48 + (Eval infixl 8 "+")
1.49
1.50 code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
1.51 (SML "Int.max/ (_/ -/ _,/ 0 : int)")
1.52 (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
1.53 (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
1.54 (Scala "!(_/ -/ _).max(0)")
1.55 + (Eval "Integer.max/ (_/ -/ _)/ 0")
1.56
1.57 code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
1.58 (SML "Int.*/ ((_),/ (_))")
1.59 (OCaml "Big'_int.mult'_big'_int")
1.60 (Haskell infixl 7 "*")
1.61 (Scala infixl 8 "*")
1.62 + (Eval infixl 8 "*")
1.63
1.64 code_const div_mod_code_numeral
1.65 - (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
1.66 + (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))")
1.67 (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
1.68 (Haskell "divMod")
1.69 - (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))")
1.70 + (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
1.71 + (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
1.72
1.73 code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
1.74 (SML "!((_ : Int.int) = _)")
1.75 (OCaml "Big'_int.eq'_big'_int")
1.76 (Haskell infixl 4 "==")
1.77 (Scala infixl 5 "==")
1.78 + (Eval "!((_ : int) = _)")
1.79
1.80 code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
1.81 (SML "Int.<=/ ((_),/ (_))")
1.82 (OCaml "Big'_int.le'_big'_int")
1.83 (Haskell infix 4 "<=")
1.84 (Scala infixl 4 "<=")
1.85 + (Eval infixl 6 "<=")
1.86
1.87 code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
1.88 (SML "Int.</ ((_),/ (_))")
1.89 (OCaml "Big'_int.lt'_big'_int")
1.90 (Haskell infix 4 "<")
1.91 (Scala infixl 4 "<")
1.92 + (Eval infixl 6 "<")
1.93
1.94 end
2.1 --- a/src/HOL/Library/Code_Integer.thy Fri Jul 23 18:42:46 2010 +0200
2.2 +++ b/src/HOL/Library/Code_Integer.thy Sat Jul 24 18:08:41 2010 +0200
2.3 @@ -14,6 +14,142 @@
2.4 operations for abstract integer operations.
2.5 *}
2.6
2.7 +text {*
2.8 + Preliminary: alternative representation of @{typ code_numeral}
2.9 + for @{text Haskell} and @{text Scala}.
2.10 +*}
2.11 +
2.12 +code_include Haskell "Natural" {*
2.13 +newtype Natural = Natural Integer deriving (Eq, Show, Read);
2.14 +
2.15 +instance Num Natural where {
2.16 + fromInteger k = Natural (if k >= 0 then k else 0);
2.17 + Natural n + Natural m = Natural (n + m);
2.18 + Natural n - Natural m = fromInteger (n - m);
2.19 + Natural n * Natural m = Natural (n * m);
2.20 + abs n = n;
2.21 + signum _ = 1;
2.22 + negate n = error "negate Natural";
2.23 +};
2.24 +
2.25 +instance Ord Natural where {
2.26 + Natural n <= Natural m = n <= m;
2.27 + Natural n < Natural m = n < m;
2.28 +};
2.29 +
2.30 +instance Real Natural where {
2.31 + toRational (Natural n) = toRational n;
2.32 +};
2.33 +
2.34 +instance Enum Natural where {
2.35 + toEnum k = fromInteger (toEnum k);
2.36 + fromEnum (Natural n) = fromEnum n;
2.37 +};
2.38 +
2.39 +instance Integral Natural where {
2.40 + toInteger (Natural n) = n;
2.41 + divMod n m = quotRem n m;
2.42 + quotRem (Natural n) (Natural m)
2.43 + | (m == 0) = (0, Natural n)
2.44 + | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
2.45 +};
2.46 +*}
2.47 +
2.48 +code_reserved Haskell Natural
2.49 +
2.50 +code_include Scala "Natural" {*
2.51 +import scala.Math
2.52 +
2.53 +object Natural {
2.54 +
2.55 + def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
2.56 + def apply(numeral: Int): Natural = Natural(BigInt(numeral))
2.57 + def apply(numeral: String): Natural = Natural(BigInt(numeral))
2.58 +
2.59 +}
2.60 +
2.61 +class Natural private(private val value: BigInt) {
2.62 +
2.63 + override def hashCode(): Int = this.value.hashCode()
2.64 +
2.65 + override def equals(that: Any): Boolean = that match {
2.66 + case that: Natural => this equals that
2.67 + case _ => false
2.68 + }
2.69 +
2.70 + override def toString(): String = this.value.toString
2.71 +
2.72 + def equals(that: Natural): Boolean = this.value == that.value
2.73 +
2.74 + def as_BigInt: BigInt = this.value
2.75 + def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
2.76 + this.value.intValue
2.77 + else this.value.intValue
2.78 +
2.79 + def +(that: Natural): Natural = new Natural(this.value + that.value)
2.80 + def -(that: Natural): Natural = Natural(this.value - that.value)
2.81 + def *(that: Natural): Natural = new Natural(this.value * that.value)
2.82 +
2.83 + def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
2.84 + else {
2.85 + val (k, l) = this.value /% that.value
2.86 + (new Natural(k), new Natural(l))
2.87 + }
2.88 +
2.89 + def <=(that: Natural): Boolean = this.value <= that.value
2.90 +
2.91 + def <(that: Natural): Boolean = this.value < that.value
2.92 +
2.93 +}
2.94 +*}
2.95 +
2.96 +code_reserved Scala Natural
2.97 +
2.98 +code_type code_numeral
2.99 + (Haskell "Natural.Natural")
2.100 + (Scala "Natural")
2.101 +
2.102 +setup {*
2.103 + fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
2.104 + false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
2.105 +*}
2.106 +
2.107 +code_instance code_numeral :: eq
2.108 + (Haskell -)
2.109 +
2.110 +code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
2.111 + (Haskell infixl 6 "+")
2.112 + (Scala infixl 7 "+")
2.113 +
2.114 +code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
2.115 + (Haskell infixl 6 "-")
2.116 + (Scala infixl 7 "-")
2.117 +
2.118 +code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
2.119 + (Haskell infixl 7 "*")
2.120 + (Scala infixl 8 "*")
2.121 +
2.122 +code_const div_mod_code_numeral
2.123 + (Haskell "divMod")
2.124 + (Scala infixl 8 "/%")
2.125 +
2.126 +code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
2.127 + (Haskell infixl 4 "==")
2.128 + (Scala infixl 5 "==")
2.129 +
2.130 +code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
2.131 + (Haskell infix 4 "<=")
2.132 + (Scala infixl 4 "<=")
2.133 +
2.134 +code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
2.135 + (Haskell infix 4 "<")
2.136 + (Scala infixl 4 "<")
2.137 +
2.138 +text {*
2.139 + Setup for @{typ int} proper.
2.140 +*}
2.141 +
2.142 +
2.143 code_type int
2.144 (SML "IntInf.int")
2.145 (OCaml "Big'_int.big'_int")
2.146 @@ -26,8 +162,6 @@
2.147 setup {*
2.148 fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
2.149 true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
2.150 - #> Numeral.add_code @{const_name number_int_inst.number_of_int}
2.151 - true Code_Printer.literal_numeral "Scala"
2.152 *}
2.153
2.154 code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
2.155 @@ -48,72 +182,82 @@
2.156 and "!error(\"Bit0\")"
2.157 and "!error(\"Bit1\")")
2.158
2.159 -
2.160 code_const Int.pred
2.161 (SML "IntInf.- ((_), 1)")
2.162 (OCaml "Big'_int.pred'_big'_int")
2.163 (Haskell "!(_/ -/ 1)")
2.164 (Scala "!(_/ -/ 1)")
2.165 + (Eval "!(_/ -/ 1)")
2.166
2.167 code_const Int.succ
2.168 (SML "IntInf.+ ((_), 1)")
2.169 (OCaml "Big'_int.succ'_big'_int")
2.170 (Haskell "!(_/ +/ 1)")
2.171 (Scala "!(_/ +/ 1)")
2.172 + (Eval "!(_/ +/ 1)")
2.173
2.174 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
2.175 (SML "IntInf.+ ((_), (_))")
2.176 (OCaml "Big'_int.add'_big'_int")
2.177 (Haskell infixl 6 "+")
2.178 (Scala infixl 7 "+")
2.179 + (Eval infixl 8 "+")
2.180
2.181 code_const "uminus \<Colon> int \<Rightarrow> int"
2.182 (SML "IntInf.~")
2.183 (OCaml "Big'_int.minus'_big'_int")
2.184 (Haskell "negate")
2.185 (Scala "!(- _)")
2.186 + (Eval "~/ _")
2.187
2.188 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
2.189 (SML "IntInf.- ((_), (_))")
2.190 (OCaml "Big'_int.sub'_big'_int")
2.191 (Haskell infixl 6 "-")
2.192 (Scala infixl 7 "-")
2.193 + (Eval infixl 8 "-")
2.194
2.195 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
2.196 (SML "IntInf.* ((_), (_))")
2.197 (OCaml "Big'_int.mult'_big'_int")
2.198 (Haskell infixl 7 "*")
2.199 (Scala infixl 8 "*")
2.200 + (Eval infixl 9 "*")
2.201
2.202 code_const pdivmod
2.203 (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
2.204 (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
2.205 (Haskell "divMod/ (abs _)/ (abs _)")
2.206 - (Scala "!(_.abs '/% _.abs)")
2.207 + (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
2.208 + (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
2.209
2.210 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
2.211 (SML "!((_ : IntInf.int) = _)")
2.212 (OCaml "Big'_int.eq'_big'_int")
2.213 (Haskell infixl 4 "==")
2.214 (Scala infixl 5 "==")
2.215 + (Eval infixl 6 "=")
2.216
2.217 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
2.218 (SML "IntInf.<= ((_), (_))")
2.219 (OCaml "Big'_int.le'_big'_int")
2.220 (Haskell infix 4 "<=")
2.221 (Scala infixl 4 "<=")
2.222 + (Eval infixl 6 "<=")
2.223
2.224 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
2.225 (SML "IntInf.< ((_), (_))")
2.226 (OCaml "Big'_int.lt'_big'_int")
2.227 (Haskell infix 4 "<")
2.228 - (Scala infixl 4 "<=")
2.229 + (Scala infixl 4 "<")
2.230 + (Eval infixl 6 "<")
2.231
2.232 code_const Code_Numeral.int_of
2.233 (SML "IntInf.fromInt")
2.234 (OCaml "_")
2.235 - (Haskell "_")
2.236 - (Scala "!BigInt((_))")
2.237 + (Haskell "toInteger")
2.238 + (Scala "!_.as'_BigInt")
2.239 + (Eval "_")
2.240
2.241 text {* Evaluation *}
2.242
3.1 --- a/src/HOL/Library/Efficient_Nat.thy Fri Jul 23 18:42:46 2010 +0200
3.2 +++ b/src/HOL/Library/Efficient_Nat.thy Sat Jul 24 18:08:41 2010 +0200
3.3 @@ -50,19 +50,9 @@
3.4 "n * m = nat (of_nat n * of_nat m)"
3.5 unfolding of_nat_mult [symmetric] by simp
3.6
3.7 -text {* Specialized @{term "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}
3.8 - and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
3.9 -
3.10 -definition divmod_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
3.11 - [code del]: "divmod_aux = divmod_nat"
3.12 -
3.13 -lemma [code]:
3.14 - "divmod_nat n m = (if m = 0 then (0, n) else divmod_aux n m)"
3.15 - unfolding divmod_aux_def divmod_nat_div_mod by simp
3.16 -
3.17 -lemma divmod_aux_code [code]:
3.18 - "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"
3.19 - unfolding divmod_aux_def divmod_nat_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
3.20 +lemma divmod_nat_code [code]:
3.21 + "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
3.22 + by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
3.23
3.24 lemma eq_nat_code [code]:
3.25 "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
3.26 @@ -233,6 +223,7 @@
3.27 code_type nat
3.28 (SML "IntInf.int")
3.29 (OCaml "Big'_int.big'_int")
3.30 + (Eval "int")
3.31
3.32 types_code
3.33 nat ("int")
3.34 @@ -281,7 +272,9 @@
3.35 instance Integral Nat where {
3.36 toInteger (Nat n) = n;
3.37 divMod n m = quotRem n m;
3.38 - quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m;
3.39 + quotRem (Nat n) (Nat m)
3.40 + | (m == 0) = (0, Nat n)
3.41 + | otherwise = (Nat k, Nat l) where (k, l) = quotRem n m;
3.42 };
3.43 *}
3.44
3.45 @@ -353,9 +346,7 @@
3.46
3.47 setup {*
3.48 fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
3.49 - false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
3.50 - #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
3.51 - false Code_Printer.literal_positive_numeral "Scala"
3.52 + false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell", "Scala"]
3.53 *}
3.54
3.55 text {*
3.56 @@ -400,6 +391,7 @@
3.57 code_const nat
3.58 (SML "IntInf.max/ (/0,/ _)")
3.59 (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
3.60 + (Eval "Integer.max/ _/ 0")
3.61
3.62 text {* For Haskell and Scala, things are slightly different again. *}
3.63
3.64 @@ -407,19 +399,21 @@
3.65 (Haskell "toInteger" and "fromInteger")
3.66 (Scala "!_.as'_BigInt" and "Nat")
3.67
3.68 -text {* Conversion from and to indices. *}
3.69 +text {* Conversion from and to code numerals. *}
3.70
3.71 code_const Code_Numeral.of_nat
3.72 (SML "IntInf.toInt")
3.73 (OCaml "_")
3.74 - (Haskell "toInteger")
3.75 - (Scala "!_.as'_Int")
3.76 + (Haskell "!(fromInteger/ ./ toInteger)")
3.77 + (Scala "!Natural(_.as'_BigInt)")
3.78 + (Eval "_")
3.79
3.80 code_const Code_Numeral.nat_of
3.81 (SML "IntInf.fromInt")
3.82 (OCaml "_")
3.83 - (Haskell "fromInteger")
3.84 - (Scala "Nat")
3.85 + (Haskell "!(fromInteger/ ./ toInteger)")
3.86 + (Scala "!Nat(_.as'_BigInt)")
3.87 + (Eval "_")
3.88
3.89 text {* Using target language arithmetic operations whenever appropriate *}
3.90
3.91 @@ -428,6 +422,7 @@
3.92 (OCaml "Big'_int.add'_big'_int")
3.93 (Haskell infixl 6 "+")
3.94 (Scala infixl 7 "+")
3.95 + (Eval infixl 8 "+")
3.96
3.97 code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
3.98 (Haskell infixl 6 "-")
3.99 @@ -438,34 +433,35 @@
3.100 (OCaml "Big'_int.mult'_big'_int")
3.101 (Haskell infixl 7 "*")
3.102 (Scala infixl 8 "*")
3.103 + (Eval infixl 9 "*")
3.104
3.105 -code_const divmod_aux
3.106 +code_const divmod_nat
3.107 (SML "IntInf.divMod/ ((_),/ (_))")
3.108 (OCaml "Big'_int.quomod'_big'_int")
3.109 (Haskell "divMod")
3.110 (Scala infixl 8 "/%")
3.111 -
3.112 -code_const divmod_nat
3.113 - (Haskell "divMod")
3.114 - (Scala infixl 8 "/%")
3.115 + (Eval "Integer.div'_mod")
3.116
3.117 code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
3.118 (SML "!((_ : IntInf.int) = _)")
3.119 (OCaml "Big'_int.eq'_big'_int")
3.120 (Haskell infixl 4 "==")
3.121 (Scala infixl 5 "==")
3.122 + (Eval infixl 6 "=")
3.123
3.124 code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
3.125 (SML "IntInf.<= ((_), (_))")
3.126 (OCaml "Big'_int.le'_big'_int")
3.127 (Haskell infix 4 "<=")
3.128 (Scala infixl 4 "<=")
3.129 + (Eval infixl 6 "<=")
3.130
3.131 code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
3.132 (SML "IntInf.< ((_), (_))")
3.133 (OCaml "Big'_int.lt'_big'_int")
3.134 (Haskell infix 4 "<")
3.135 (Scala infixl 4 "<")
3.136 + (Eval infixl 6 "<")
3.137
3.138 consts_code
3.139 "0::nat" ("0")
4.1 --- a/src/Tools/Code/code_haskell.ML Fri Jul 23 18:42:46 2010 +0200
4.2 +++ b/src/Tools/Code/code_haskell.ML Sat Jul 24 18:08:41 2010 +0200
4.3 @@ -415,6 +415,7 @@
4.4 literal_string = quote o translate_string char_haskell,
4.5 literal_numeral = numeral_haskell,
4.6 literal_positive_numeral = numeral_haskell,
4.7 + literal_alternative_numeral = numeral_haskell,
4.8 literal_naive_numeral = numeral_haskell,
4.9 literal_list = enum "," "[" "]",
4.10 infix_cons = (5, ":")
5.1 --- a/src/Tools/Code/code_ml.ML Fri Jul 23 18:42:46 2010 +0200
5.2 +++ b/src/Tools/Code/code_ml.ML Sat Jul 24 18:08:41 2010 +0200
5.3 @@ -360,6 +360,7 @@
5.4 literal_string = quote o translate_string ML_Syntax.print_char,
5.5 literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
5.6 literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
5.7 + literal_alternative_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
5.8 literal_naive_numeral = string_of_int,
5.9 literal_list = enum "," "[" "]",
5.10 infix_cons = (7, "::")
5.11 @@ -702,6 +703,7 @@
5.12 literal_string = quote o translate_string char_ocaml,
5.13 literal_numeral = numeral_ocaml,
5.14 literal_positive_numeral = numeral_ocaml,
5.15 + literal_alternative_numeral = numeral_ocaml,
5.16 literal_naive_numeral = numeral_ocaml,
5.17 literal_list = enum ";" "[" "]",
5.18 infix_cons = (6, "::")
6.1 --- a/src/Tools/Code/code_printer.ML Fri Jul 23 18:42:46 2010 +0200
6.2 +++ b/src/Tools/Code/code_printer.ML Sat Jul 24 18:08:41 2010 +0200
6.3 @@ -39,7 +39,9 @@
6.4
6.5 type literals
6.6 val Literals: { literal_char: string -> string, literal_string: string -> string,
6.7 - literal_numeral: int -> string, literal_positive_numeral: int -> string,
6.8 + literal_numeral: int -> string,
6.9 + literal_positive_numeral: int -> string,
6.10 + literal_alternative_numeral: int -> string,
6.11 literal_naive_numeral: int -> string,
6.12 literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
6.13 -> literals
6.14 @@ -47,6 +49,7 @@
6.15 val literal_string: literals -> string -> string
6.16 val literal_numeral: literals -> int -> string
6.17 val literal_positive_numeral: literals -> int -> string
6.18 + val literal_alternative_numeral: literals -> int -> string
6.19 val literal_naive_numeral: literals -> int -> string
6.20 val literal_list: literals -> Pretty.T list -> Pretty.T
6.21 val infix_cons: literals -> int * string
6.22 @@ -171,6 +174,7 @@
6.23 literal_string: string -> string,
6.24 literal_numeral: int -> string,
6.25 literal_positive_numeral: int -> string,
6.26 + literal_alternative_numeral: int -> string,
6.27 literal_naive_numeral: int -> string,
6.28 literal_list: Pretty.T list -> Pretty.T,
6.29 infix_cons: int * string
6.30 @@ -182,6 +186,7 @@
6.31 val literal_string = #literal_string o dest_Literals;
6.32 val literal_numeral = #literal_numeral o dest_Literals;
6.33 val literal_positive_numeral = #literal_positive_numeral o dest_Literals;
6.34 +val literal_alternative_numeral = #literal_alternative_numeral o dest_Literals;
6.35 val literal_naive_numeral = #literal_naive_numeral o dest_Literals;
6.36 val literal_list = #literal_list o dest_Literals;
6.37 val infix_cons = #infix_cons o dest_Literals;
7.1 --- a/src/Tools/Code/code_scala.ML Fri Jul 23 18:42:46 2010 +0200
7.2 +++ b/src/Tools/Code/code_scala.ML Sat Jul 24 18:08:41 2010 +0200
7.3 @@ -402,7 +402,7 @@
7.4 else let val k = ord c
7.5 in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
7.6 fun numeral_scala k = if k < 0
7.7 - then if k <= 2147483647 then "- " ^ string_of_int (~ k)
7.8 + then if k > ~ 2147483647 then "- " ^ string_of_int (~ k)
7.9 else quote ("- " ^ string_of_int (~ k))
7.10 else if k <= 2147483647 then string_of_int k
7.11 else quote (string_of_int k)
7.12 @@ -411,8 +411,8 @@
7.13 literal_string = quote o translate_string char_scala,
7.14 literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
7.15 literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
7.16 - literal_naive_numeral = fn k => if k >= 0
7.17 - then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
7.18 + literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
7.19 + literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
7.20 literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
7.21 infix_cons = (6, "::")
7.22 } end;