# HG changeset patch # User haftmann # Date 1263487659 -3600 # Node ID 8674bb6f727b203812f2fecf4d18bb1f9ca8eb01 # Parent 62d70417f8ce16b3a2f3813a0b54e42121a6b20a added Scala setup diff -r 62d70417f8ce -r 8674bb6f727b src/HOL/Library/Code_Integer.thy --- a/src/HOL/Library/Code_Integer.thy Thu Jan 14 17:47:38 2010 +0100 +++ b/src/HOL/Library/Code_Integer.thy Thu Jan 14 17:47:39 2010 +0100 @@ -18,13 +18,16 @@ (SML "IntInf.int") (OCaml "Big'_int.big'_int") (Haskell "Integer") + (Scala "BigInt") code_instance int :: eq (Haskell -) setup {* fold (Numeral.add_code @{const_name number_int_inst.number_of_int} - true true) ["SML", "OCaml", "Haskell"] + true true Code_Printer.str) ["SML", "OCaml", "Haskell", "Scala"] + #> Numeral.add_code @{const_name number_int_inst.number_of_int} + true true (fn s => (Pretty.block o map Code_Printer.str) ["BigInt", s]) "Scala" *} code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1" @@ -40,63 +43,80 @@ and "error/ \"Min\"" and "error/ \"Bit0\"" and "error/ \"Bit1\"") + (Scala "!error(\"Pls\")" + and "!error(\"Min\")" + and "!error(\"Bit0\")" + and "!error(\"Bit1\")") + code_const Int.pred (SML "IntInf.- ((_), 1)") (OCaml "Big'_int.pred'_big'_int") (Haskell "!(_/ -/ 1)") + (Scala "!(_/ -/ 1)") code_const Int.succ (SML "IntInf.+ ((_), 1)") (OCaml "Big'_int.succ'_big'_int") (Haskell "!(_/ +/ 1)") + (Scala "!(_/ +/ 1)") code_const "op + \ int \ int \ int" (SML "IntInf.+ ((_), (_))") (OCaml "Big'_int.add'_big'_int") (Haskell infixl 6 "+") + (Scala infixl 7 "+") code_const "uminus \ int \ int" (SML "IntInf.~") (OCaml "Big'_int.minus'_big'_int") (Haskell "negate") + (Scala "!(- _)") code_const "op - \ int \ int \ int" (SML "IntInf.- ((_), (_))") (OCaml "Big'_int.sub'_big'_int") (Haskell infixl 6 "-") + (Scala infixl 7 "-") code_const "op * \ int \ int \ int" (SML "IntInf.* ((_), (_))") (OCaml "Big'_int.mult'_big'_int") (Haskell infixl 7 "*") + (Scala infixl 8 "*") code_const pdivmod - (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))") - (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))") - (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))") + (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)") + (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)") + (Haskell "divMod/ (abs _)/ (abs _))") + (Scala "!(_.abs '/% _.abs)") code_const "eq_class.eq \ int \ int \ bool" (SML "!((_ : IntInf.int) = _)") (OCaml "Big'_int.eq'_big'_int") (Haskell infixl 4 "==") + (Scala infixl 5 "==") code_const "op \ \ int \ int \ bool" (SML "IntInf.<= ((_), (_))") (OCaml "Big'_int.le'_big'_int") (Haskell infix 4 "<=") + (Scala infixl 4 "<=") code_const "op < \ int \ int \ bool" (SML "IntInf.< ((_), (_))") (OCaml "Big'_int.lt'_big'_int") (Haskell infix 4 "<") + (Scala infixl 4 "<=") code_const Code_Numeral.int_of (SML "IntInf.fromInt") (OCaml "_") (Haskell "toEnum") + (Scala "!BigInt(_)") code_reserved SML IntInf +code_reserved Scala BigInt text {* Evaluation *} diff -r 62d70417f8ce -r 8674bb6f727b src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Thu Jan 14 17:47:38 2010 +0100 +++ b/src/HOL/Library/Efficient_Nat.thy Thu Jan 14 17:47:39 2010 +0100 @@ -226,7 +226,7 @@ text {* For ML, we map @{typ nat} to target language integers, where we - assert that values are always non-negative. + ensure that values are always non-negative. *} code_type nat @@ -245,9 +245,9 @@ *} text {* - For Haskell we define our own @{typ nat} type. The reason - is that we have to distinguish type class instances - for @{typ nat} and @{typ int}. + For Haskell ans Scala we define our own @{typ nat} type. The reason + is that we have to distinguish type class instances for @{typ nat} + and @{typ int}. *} code_include Haskell "Nat" {* @@ -286,8 +286,52 @@ code_reserved Haskell Nat +code_include Scala "Nat" {* +object Nat { + + def apply(numeral: BigInt): Nat = new Nat(numeral max 0) + def apply(numeral: Int): Nat = Nat(BigInt(numeral)) + def apply(numeral: String): Nat = Nat(BigInt(numeral)) + +} + +class Nat private(private val value: BigInt) { + + override def hashCode(): Int = this.value.hashCode() + + override def equals(that: Any): Boolean = that match { + case that: Nat => this equals that + case _ => false + } + + override def toString(): String = this.value.toString + + def equals(that: Nat): Boolean = this.value == that.value + + def as_BigInt: BigInt = this.value + + def +(that: Nat): Nat = new Nat(this.value + that.value) + def -(that: Nat): Nat = Nat(this.value + that.value) + def *(that: Nat): Nat = new Nat(this.value * that.value) + + def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this) + else { + val (k, l) = this.value /% that.value + (new Nat(k), new Nat(l)) + } + + def <=(that: Nat): Boolean = this.value <= that.value + + def <(that: Nat): Boolean = this.value < that.value + +} +*} + +code_reserved Scala Nat + code_type nat (Haskell "Nat.Nat") + (Scala "Nat.Nat") code_instance nat :: eq (Haskell -) @@ -303,7 +347,9 @@ setup {* fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat} - false true) ["SML", "OCaml", "Haskell"] + false true Code_Printer.str) ["SML", "OCaml", "Haskell"] + #> Numeral.add_code @{const_name number_nat_inst.number_of_nat} + false true (fn s => (Pretty.block o map Code_Printer.str) ["Nat.Nat", s]) "Scala" *} text {* @@ -349,10 +395,11 @@ (SML "IntInf.max/ (/0,/ _)") (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int") -text {* For Haskell, things are slightly different again. *} +text {* For Haskell ans Scala, things are slightly different again. *} code_const int and nat (Haskell "toInteger" and "fromInteger") + (Scala "!_.as'_BigInt" and "!Nat.Nat((_))") text {* Conversion from and to indices. *} @@ -360,11 +407,13 @@ (SML "IntInf.toInt") (OCaml "_") (Haskell "fromEnum") + (Scala "!_.as'_BigInt") code_const Code_Numeral.nat_of (SML "IntInf.fromInt") (OCaml "_") (Haskell "toEnum") + (Scala "!Nat.Nat((_))") text {* Using target language arithmetic operations whenever appropriate *} @@ -372,31 +421,45 @@ (SML "IntInf.+ ((_), (_))") (OCaml "Big'_int.add'_big'_int") (Haskell infixl 6 "+") + (Scala infixl 7 "+") + +code_const "op - \ nat \ nat \ nat" + (Haskell infixl 6 "-") + (Scala infixl 7 "-") code_const "op * \ nat \ nat \ nat" (SML "IntInf.* ((_), (_))") (OCaml "Big'_int.mult'_big'_int") (Haskell infixl 7 "*") + (Scala infixl 8 "*") code_const divmod_aux (SML "IntInf.divMod/ ((_),/ (_))") (OCaml "Big'_int.quomod'_big'_int") (Haskell "divMod") + (Scala infixl 8 "/%") + +code_const divmod_nat + (Haskell "divMod") + (Scala infixl 8 "/%") code_const "eq_class.eq \ nat \ nat \ bool" (SML "!((_ : IntInf.int) = _)") (OCaml "Big'_int.eq'_big'_int") (Haskell infixl 4 "==") + (Scala infixl 5 "==") code_const "op \ \ nat \ nat \ bool" (SML "IntInf.<= ((_), (_))") (OCaml "Big'_int.le'_big'_int") (Haskell infix 4 "<=") + (Scala infixl 4 "<=") code_const "op < \ nat \ nat \ bool" (SML "IntInf.< ((_), (_))") (OCaml "Big'_int.lt'_big'_int") (Haskell infix 4 "<") + (Scala infixl 4 "<") consts_code "0::nat" ("0")