src/HOL/Library/Code_Integer.thy
changeset 37958 9728342bcd56
parent 37947 844977c7abeb
child 37968 52fdcb76c0af
     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