src/HOL/Library/Efficient_Nat.thy
changeset 34899 8674bb6f727b
parent 34893 ecdc526af73a
child 34902 780172c006e1
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:47:38 2010 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:47:39 2010 +0100
     1.3 @@ -226,7 +226,7 @@
     1.4  
     1.5  text {*
     1.6    For ML, we map @{typ nat} to target language integers, where we
     1.7 -  assert that values are always non-negative.
     1.8 +  ensure that values are always non-negative.
     1.9  *}
    1.10  
    1.11  code_type nat
    1.12 @@ -245,9 +245,9 @@
    1.13  *}
    1.14  
    1.15  text {*
    1.16 -  For Haskell we define our own @{typ nat} type.  The reason
    1.17 -  is that we have to distinguish type class instances
    1.18 -  for @{typ nat} and @{typ int}.
    1.19 +  For Haskell ans Scala we define our own @{typ nat} type.  The reason
    1.20 +  is that we have to distinguish type class instances for @{typ nat}
    1.21 +  and @{typ int}.
    1.22  *}
    1.23  
    1.24  code_include Haskell "Nat" {*
    1.25 @@ -286,8 +286,52 @@
    1.26  
    1.27  code_reserved Haskell Nat
    1.28  
    1.29 +code_include Scala "Nat" {*
    1.30 +object Nat {
    1.31 +
    1.32 +  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    1.33 +  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
    1.34 +  def apply(numeral: String): Nat = Nat(BigInt(numeral))
    1.35 +
    1.36 +}
    1.37 +
    1.38 +class Nat private(private val value: BigInt) {
    1.39 +
    1.40 +  override def hashCode(): Int = this.value.hashCode()
    1.41 +
    1.42 +  override def equals(that: Any): Boolean = that match {
    1.43 +    case that: Nat => this equals that
    1.44 +    case _ => false
    1.45 +  }
    1.46 +
    1.47 +  override def toString(): String = this.value.toString
    1.48 +
    1.49 +  def equals(that: Nat): Boolean = this.value == that.value
    1.50 +
    1.51 +  def as_BigInt: BigInt = this.value
    1.52 +
    1.53 +  def +(that: Nat): Nat = new Nat(this.value + that.value)
    1.54 +  def -(that: Nat): Nat = Nat(this.value + that.value)
    1.55 +  def *(that: Nat): Nat = new Nat(this.value * that.value)
    1.56 +
    1.57 +  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
    1.58 +    else {
    1.59 +      val (k, l) = this.value /% that.value
    1.60 +      (new Nat(k), new Nat(l))
    1.61 +    }
    1.62 +
    1.63 +  def <=(that: Nat): Boolean = this.value <= that.value
    1.64 +
    1.65 +  def <(that: Nat): Boolean = this.value < that.value
    1.66 +
    1.67 +}
    1.68 +*}
    1.69 +
    1.70 +code_reserved Scala Nat
    1.71 +
    1.72  code_type nat
    1.73    (Haskell "Nat.Nat")
    1.74 +  (Scala "Nat.Nat")
    1.75  
    1.76  code_instance nat :: eq
    1.77    (Haskell -)
    1.78 @@ -303,7 +347,9 @@
    1.79  
    1.80  setup {*
    1.81    fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    1.82 -    false true) ["SML", "OCaml", "Haskell"]
    1.83 +    false true Code_Printer.str) ["SML", "OCaml", "Haskell"]
    1.84 +  #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    1.85 +    false true (fn s => (Pretty.block o map Code_Printer.str) ["Nat.Nat", s]) "Scala"
    1.86  *}
    1.87  
    1.88  text {*
    1.89 @@ -349,10 +395,11 @@
    1.90    (SML "IntInf.max/ (/0,/ _)")
    1.91    (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
    1.92  
    1.93 -text {* For Haskell, things are slightly different again. *}
    1.94 +text {* For Haskell ans Scala, things are slightly different again. *}
    1.95  
    1.96  code_const int and nat
    1.97    (Haskell "toInteger" and "fromInteger")
    1.98 +  (Scala "!_.as'_BigInt" and "!Nat.Nat((_))")
    1.99  
   1.100  text {* Conversion from and to indices. *}
   1.101  
   1.102 @@ -360,11 +407,13 @@
   1.103    (SML "IntInf.toInt")
   1.104    (OCaml "_")
   1.105    (Haskell "fromEnum")
   1.106 +  (Scala "!_.as'_BigInt")
   1.107  
   1.108  code_const Code_Numeral.nat_of
   1.109    (SML "IntInf.fromInt")
   1.110    (OCaml "_")
   1.111    (Haskell "toEnum")
   1.112 +  (Scala "!Nat.Nat((_))")
   1.113  
   1.114  text {* Using target language arithmetic operations whenever appropriate *}
   1.115  
   1.116 @@ -372,31 +421,45 @@
   1.117    (SML "IntInf.+ ((_), (_))")
   1.118    (OCaml "Big'_int.add'_big'_int")
   1.119    (Haskell infixl 6 "+")
   1.120 +  (Scala infixl 7 "+")
   1.121 +
   1.122 +code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
   1.123 +  (Haskell infixl 6 "-")
   1.124 +  (Scala infixl 7 "-")
   1.125  
   1.126  code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
   1.127    (SML "IntInf.* ((_), (_))")
   1.128    (OCaml "Big'_int.mult'_big'_int")
   1.129    (Haskell infixl 7 "*")
   1.130 +  (Scala infixl 8 "*")
   1.131  
   1.132  code_const divmod_aux
   1.133    (SML "IntInf.divMod/ ((_),/ (_))")
   1.134    (OCaml "Big'_int.quomod'_big'_int")
   1.135    (Haskell "divMod")
   1.136 +  (Scala infixl 8 "/%")
   1.137 +
   1.138 +code_const divmod_nat
   1.139 +  (Haskell "divMod")
   1.140 +  (Scala infixl 8 "/%")
   1.141  
   1.142  code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   1.143    (SML "!((_ : IntInf.int) = _)")
   1.144    (OCaml "Big'_int.eq'_big'_int")
   1.145    (Haskell infixl 4 "==")
   1.146 +  (Scala infixl 5 "==")
   1.147  
   1.148  code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   1.149    (SML "IntInf.<= ((_), (_))")
   1.150    (OCaml "Big'_int.le'_big'_int")
   1.151    (Haskell infix 4 "<=")
   1.152 +  (Scala infixl 4 "<=")
   1.153  
   1.154  code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   1.155    (SML "IntInf.< ((_), (_))")
   1.156    (OCaml "Big'_int.lt'_big'_int")
   1.157    (Haskell infix 4 "<")
   1.158 +  (Scala infixl 4 "<")
   1.159  
   1.160  consts_code
   1.161    "0::nat"                     ("0")