1.1 --- a/src/HOL/Library/Code_Integer.thy Fri Jul 23 18:42:46 2010 +0200
1.2 +++ b/src/HOL/Library/Code_Integer.thy Sat Jul 24 18:08:41 2010 +0200
1.3 @@ -14,6 +14,142 @@
1.4 operations for abstract integer operations.
1.5 *}
1.6
1.7 +text {*
1.8 + Preliminary: alternative representation of @{typ code_numeral}
1.9 + for @{text Haskell} and @{text Scala}.
1.10 +*}
1.11 +
1.12 +code_include Haskell "Natural" {*
1.13 +newtype Natural = Natural Integer deriving (Eq, Show, Read);
1.14 +
1.15 +instance Num Natural where {
1.16 + fromInteger k = Natural (if k >= 0 then k else 0);
1.17 + Natural n + Natural m = Natural (n + m);
1.18 + Natural n - Natural m = fromInteger (n - m);
1.19 + Natural n * Natural m = Natural (n * m);
1.20 + abs n = n;
1.21 + signum _ = 1;
1.22 + negate n = error "negate Natural";
1.23 +};
1.24 +
1.25 +instance Ord Natural where {
1.26 + Natural n <= Natural m = n <= m;
1.27 + Natural n < Natural m = n < m;
1.28 +};
1.29 +
1.30 +instance Real Natural where {
1.31 + toRational (Natural n) = toRational n;
1.32 +};
1.33 +
1.34 +instance Enum Natural where {
1.35 + toEnum k = fromInteger (toEnum k);
1.36 + fromEnum (Natural n) = fromEnum n;
1.37 +};
1.38 +
1.39 +instance Integral Natural where {
1.40 + toInteger (Natural n) = n;
1.41 + divMod n m = quotRem n m;
1.42 + quotRem (Natural n) (Natural m)
1.43 + | (m == 0) = (0, Natural n)
1.44 + | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
1.45 +};
1.46 +*}
1.47 +
1.48 +code_reserved Haskell Natural
1.49 +
1.50 +code_include Scala "Natural" {*
1.51 +import scala.Math
1.52 +
1.53 +object Natural {
1.54 +
1.55 + def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
1.56 + def apply(numeral: Int): Natural = Natural(BigInt(numeral))
1.57 + def apply(numeral: String): Natural = Natural(BigInt(numeral))
1.58 +
1.59 +}
1.60 +
1.61 +class Natural private(private val value: BigInt) {
1.62 +
1.63 + override def hashCode(): Int = this.value.hashCode()
1.64 +
1.65 + override def equals(that: Any): Boolean = that match {
1.66 + case that: Natural => this equals that
1.67 + case _ => false
1.68 + }
1.69 +
1.70 + override def toString(): String = this.value.toString
1.71 +
1.72 + def equals(that: Natural): Boolean = this.value == that.value
1.73 +
1.74 + def as_BigInt: BigInt = this.value
1.75 + def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
1.76 + this.value.intValue
1.77 + else this.value.intValue
1.78 +
1.79 + def +(that: Natural): Natural = new Natural(this.value + that.value)
1.80 + def -(that: Natural): Natural = Natural(this.value - that.value)
1.81 + def *(that: Natural): Natural = new Natural(this.value * that.value)
1.82 +
1.83 + def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
1.84 + else {
1.85 + val (k, l) = this.value /% that.value
1.86 + (new Natural(k), new Natural(l))
1.87 + }
1.88 +
1.89 + def <=(that: Natural): Boolean = this.value <= that.value
1.90 +
1.91 + def <(that: Natural): Boolean = this.value < that.value
1.92 +
1.93 +}
1.94 +*}
1.95 +
1.96 +code_reserved Scala Natural
1.97 +
1.98 +code_type code_numeral
1.99 + (Haskell "Natural.Natural")
1.100 + (Scala "Natural")
1.101 +
1.102 +setup {*
1.103 + fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
1.104 + false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
1.105 +*}
1.106 +
1.107 +code_instance code_numeral :: eq
1.108 + (Haskell -)
1.109 +
1.110 +code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
1.111 + (Haskell infixl 6 "+")
1.112 + (Scala infixl 7 "+")
1.113 +
1.114 +code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
1.115 + (Haskell infixl 6 "-")
1.116 + (Scala infixl 7 "-")
1.117 +
1.118 +code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
1.119 + (Haskell infixl 7 "*")
1.120 + (Scala infixl 8 "*")
1.121 +
1.122 +code_const div_mod_code_numeral
1.123 + (Haskell "divMod")
1.124 + (Scala infixl 8 "/%")
1.125 +
1.126 +code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
1.127 + (Haskell infixl 4 "==")
1.128 + (Scala infixl 5 "==")
1.129 +
1.130 +code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
1.131 + (Haskell infix 4 "<=")
1.132 + (Scala infixl 4 "<=")
1.133 +
1.134 +code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
1.135 + (Haskell infix 4 "<")
1.136 + (Scala infixl 4 "<")
1.137 +
1.138 +text {*
1.139 + Setup for @{typ int} proper.
1.140 +*}
1.141 +
1.142 +
1.143 code_type int
1.144 (SML "IntInf.int")
1.145 (OCaml "Big'_int.big'_int")
1.146 @@ -26,8 +162,6 @@
1.147 setup {*
1.148 fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
1.149 true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
1.150 - #> Numeral.add_code @{const_name number_int_inst.number_of_int}
1.151 - true Code_Printer.literal_numeral "Scala"
1.152 *}
1.153
1.154 code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
1.155 @@ -48,72 +182,82 @@
1.156 and "!error(\"Bit0\")"
1.157 and "!error(\"Bit1\")")
1.158
1.159 -
1.160 code_const Int.pred
1.161 (SML "IntInf.- ((_), 1)")
1.162 (OCaml "Big'_int.pred'_big'_int")
1.163 (Haskell "!(_/ -/ 1)")
1.164 (Scala "!(_/ -/ 1)")
1.165 + (Eval "!(_/ -/ 1)")
1.166
1.167 code_const Int.succ
1.168 (SML "IntInf.+ ((_), 1)")
1.169 (OCaml "Big'_int.succ'_big'_int")
1.170 (Haskell "!(_/ +/ 1)")
1.171 (Scala "!(_/ +/ 1)")
1.172 + (Eval "!(_/ +/ 1)")
1.173
1.174 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
1.175 (SML "IntInf.+ ((_), (_))")
1.176 (OCaml "Big'_int.add'_big'_int")
1.177 (Haskell infixl 6 "+")
1.178 (Scala infixl 7 "+")
1.179 + (Eval infixl 8 "+")
1.180
1.181 code_const "uminus \<Colon> int \<Rightarrow> int"
1.182 (SML "IntInf.~")
1.183 (OCaml "Big'_int.minus'_big'_int")
1.184 (Haskell "negate")
1.185 (Scala "!(- _)")
1.186 + (Eval "~/ _")
1.187
1.188 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
1.189 (SML "IntInf.- ((_), (_))")
1.190 (OCaml "Big'_int.sub'_big'_int")
1.191 (Haskell infixl 6 "-")
1.192 (Scala infixl 7 "-")
1.193 + (Eval infixl 8 "-")
1.194
1.195 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
1.196 (SML "IntInf.* ((_), (_))")
1.197 (OCaml "Big'_int.mult'_big'_int")
1.198 (Haskell infixl 7 "*")
1.199 (Scala infixl 8 "*")
1.200 + (Eval infixl 9 "*")
1.201
1.202 code_const pdivmod
1.203 (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
1.204 (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
1.205 (Haskell "divMod/ (abs _)/ (abs _)")
1.206 - (Scala "!(_.abs '/% _.abs)")
1.207 + (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
1.208 + (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
1.209
1.210 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
1.211 (SML "!((_ : IntInf.int) = _)")
1.212 (OCaml "Big'_int.eq'_big'_int")
1.213 (Haskell infixl 4 "==")
1.214 (Scala infixl 5 "==")
1.215 + (Eval infixl 6 "=")
1.216
1.217 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
1.218 (SML "IntInf.<= ((_), (_))")
1.219 (OCaml "Big'_int.le'_big'_int")
1.220 (Haskell infix 4 "<=")
1.221 (Scala infixl 4 "<=")
1.222 + (Eval infixl 6 "<=")
1.223
1.224 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
1.225 (SML "IntInf.< ((_), (_))")
1.226 (OCaml "Big'_int.lt'_big'_int")
1.227 (Haskell infix 4 "<")
1.228 - (Scala infixl 4 "<=")
1.229 + (Scala infixl 4 "<")
1.230 + (Eval infixl 6 "<")
1.231
1.232 code_const Code_Numeral.int_of
1.233 (SML "IntInf.fromInt")
1.234 (OCaml "_")
1.235 - (Haskell "_")
1.236 - (Scala "!BigInt((_))")
1.237 + (Haskell "toInteger")
1.238 + (Scala "!_.as'_BigInt")
1.239 + (Eval "_")
1.240
1.241 text {* Evaluation *}
1.242