src/HOL/Library/Efficient_Nat.thy
changeset 34944 970e1466028d
parent 34902 780172c006e1
child 35625 9c818cab0dd0
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Jan 22 13:38:28 2010 +0100
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jan 22 13:38:28 2010 +0100
     1.3 @@ -287,6 +287,8 @@
     1.4  code_reserved Haskell Nat
     1.5  
     1.6  code_include Scala "Nat" {*
     1.7 +import scala.Math
     1.8 +
     1.9  object Nat {
    1.10  
    1.11    def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    1.12 @@ -309,7 +311,9 @@
    1.13    def equals(that: Nat): Boolean = this.value == that.value
    1.14  
    1.15    def as_BigInt: BigInt = this.value
    1.16 -  def as_Int: Int = this.value
    1.17 +  def as_Int: Int = if (this.value >= Math.MAX_INT && this.value <= Math.MAX_INT)
    1.18 +      this.value.intValue
    1.19 +    else error("Int value too big:" + this.value.toString)
    1.20  
    1.21    def +(that: Nat): Nat = new Nat(this.value + that.value)
    1.22    def -(that: Nat): Nat = Nat(this.value + that.value)
    1.23 @@ -348,9 +352,9 @@
    1.24  
    1.25  setup {*
    1.26    fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    1.27 -    false true Code_Printer.str) ["SML", "OCaml", "Haskell"]
    1.28 +    false Code_Printer.literal_positive_numeral) ["SML", "OCaml", "Haskell"]
    1.29    #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    1.30 -    false true (fn s => (Pretty.block o map Code_Printer.str) ["Nat.Nat", s]) "Scala"
    1.31 +    false Code_Printer.literal_positive_numeral "Scala"
    1.32  *}
    1.33  
    1.34  text {*