added Scala setup
authorhaftmann
Thu Jan 14 17:47:39 2010 +0100 (2010-01-14)
changeset 348998674bb6f727b
parent 34898 62d70417f8ce
child 34900 9b12b0824bfe
added Scala setup
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Efficient_Nat.thy
     1.1 --- a/src/HOL/Library/Code_Integer.thy	Thu Jan 14 17:47:38 2010 +0100
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Thu Jan 14 17:47:39 2010 +0100
     1.3 @@ -18,13 +18,16 @@
     1.4    (SML "IntInf.int")
     1.5    (OCaml "Big'_int.big'_int")
     1.6    (Haskell "Integer")
     1.7 +  (Scala "BigInt")
     1.8  
     1.9  code_instance int :: eq
    1.10    (Haskell -)
    1.11  
    1.12  setup {*
    1.13    fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
    1.14 -    true true) ["SML", "OCaml", "Haskell"]
    1.15 +    true true Code_Printer.str) ["SML", "OCaml", "Haskell", "Scala"]
    1.16 +  #> Numeral.add_code @{const_name number_int_inst.number_of_int}
    1.17 +    true true (fn s => (Pretty.block o map Code_Printer.str) ["BigInt", s]) "Scala"
    1.18  *}
    1.19  
    1.20  code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
    1.21 @@ -40,63 +43,80 @@
    1.22       and "error/ \"Min\""
    1.23       and "error/ \"Bit0\""
    1.24       and "error/ \"Bit1\"")
    1.25 +  (Scala "!error(\"Pls\")"
    1.26 +     and "!error(\"Min\")"
    1.27 +     and "!error(\"Bit0\")"
    1.28 +     and "!error(\"Bit1\")")
    1.29 +
    1.30  
    1.31  code_const Int.pred
    1.32    (SML "IntInf.- ((_), 1)")
    1.33    (OCaml "Big'_int.pred'_big'_int")
    1.34    (Haskell "!(_/ -/ 1)")
    1.35 +  (Scala "!(_/ -/ 1)")
    1.36  
    1.37  code_const Int.succ
    1.38    (SML "IntInf.+ ((_), 1)")
    1.39    (OCaml "Big'_int.succ'_big'_int")
    1.40    (Haskell "!(_/ +/ 1)")
    1.41 +  (Scala "!(_/ +/ 1)")
    1.42  
    1.43  code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    1.44    (SML "IntInf.+ ((_), (_))")
    1.45    (OCaml "Big'_int.add'_big'_int")
    1.46    (Haskell infixl 6 "+")
    1.47 +  (Scala infixl 7 "+")
    1.48  
    1.49  code_const "uminus \<Colon> int \<Rightarrow> int"
    1.50    (SML "IntInf.~")
    1.51    (OCaml "Big'_int.minus'_big'_int")
    1.52    (Haskell "negate")
    1.53 +  (Scala "!(- _)")
    1.54  
    1.55  code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    1.56    (SML "IntInf.- ((_), (_))")
    1.57    (OCaml "Big'_int.sub'_big'_int")
    1.58    (Haskell infixl 6 "-")
    1.59 +  (Scala infixl 7 "-")
    1.60  
    1.61  code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    1.62    (SML "IntInf.* ((_), (_))")
    1.63    (OCaml "Big'_int.mult'_big'_int")
    1.64    (Haskell infixl 7 "*")
    1.65 +  (Scala infixl 8 "*")
    1.66  
    1.67  code_const pdivmod
    1.68 -  (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))")
    1.69 -  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
    1.70 -  (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))")
    1.71 +  (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
    1.72 +  (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
    1.73 +  (Haskell "divMod/ (abs _)/ (abs _))")
    1.74 +  (Scala "!(_.abs '/% _.abs)")
    1.75  
    1.76  code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.77    (SML "!((_ : IntInf.int) = _)")
    1.78    (OCaml "Big'_int.eq'_big'_int")
    1.79    (Haskell infixl 4 "==")
    1.80 +  (Scala infixl 5 "==")
    1.81  
    1.82  code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.83    (SML "IntInf.<= ((_), (_))")
    1.84    (OCaml "Big'_int.le'_big'_int")
    1.85    (Haskell infix 4 "<=")
    1.86 +  (Scala infixl 4 "<=")
    1.87  
    1.88  code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.89    (SML "IntInf.< ((_), (_))")
    1.90    (OCaml "Big'_int.lt'_big'_int")
    1.91    (Haskell infix 4 "<")
    1.92 +  (Scala infixl 4 "<=")
    1.93  
    1.94  code_const Code_Numeral.int_of
    1.95    (SML "IntInf.fromInt")
    1.96    (OCaml "_")
    1.97    (Haskell "toEnum")
    1.98 +  (Scala "!BigInt(_)")
    1.99  
   1.100  code_reserved SML IntInf
   1.101 +code_reserved Scala BigInt
   1.102  
   1.103  text {* Evaluation *}
   1.104  
     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:47:38 2010 +0100
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 17:47:39 2010 +0100
     2.3 @@ -226,7 +226,7 @@
     2.4  
     2.5  text {*
     2.6    For ML, we map @{typ nat} to target language integers, where we
     2.7 -  assert that values are always non-negative.
     2.8 +  ensure that values are always non-negative.
     2.9  *}
    2.10  
    2.11  code_type nat
    2.12 @@ -245,9 +245,9 @@
    2.13  *}
    2.14  
    2.15  text {*
    2.16 -  For Haskell we define our own @{typ nat} type.  The reason
    2.17 -  is that we have to distinguish type class instances
    2.18 -  for @{typ nat} and @{typ int}.
    2.19 +  For Haskell ans Scala we define our own @{typ nat} type.  The reason
    2.20 +  is that we have to distinguish type class instances for @{typ nat}
    2.21 +  and @{typ int}.
    2.22  *}
    2.23  
    2.24  code_include Haskell "Nat" {*
    2.25 @@ -286,8 +286,52 @@
    2.26  
    2.27  code_reserved Haskell Nat
    2.28  
    2.29 +code_include Scala "Nat" {*
    2.30 +object Nat {
    2.31 +
    2.32 +  def apply(numeral: BigInt): Nat = new Nat(numeral max 0)
    2.33 +  def apply(numeral: Int): Nat = Nat(BigInt(numeral))
    2.34 +  def apply(numeral: String): Nat = Nat(BigInt(numeral))
    2.35 +
    2.36 +}
    2.37 +
    2.38 +class Nat private(private val value: BigInt) {
    2.39 +
    2.40 +  override def hashCode(): Int = this.value.hashCode()
    2.41 +
    2.42 +  override def equals(that: Any): Boolean = that match {
    2.43 +    case that: Nat => this equals that
    2.44 +    case _ => false
    2.45 +  }
    2.46 +
    2.47 +  override def toString(): String = this.value.toString
    2.48 +
    2.49 +  def equals(that: Nat): Boolean = this.value == that.value
    2.50 +
    2.51 +  def as_BigInt: BigInt = this.value
    2.52 +
    2.53 +  def +(that: Nat): Nat = new Nat(this.value + that.value)
    2.54 +  def -(that: Nat): Nat = Nat(this.value + that.value)
    2.55 +  def *(that: Nat): Nat = new Nat(this.value * that.value)
    2.56 +
    2.57 +  def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
    2.58 +    else {
    2.59 +      val (k, l) = this.value /% that.value
    2.60 +      (new Nat(k), new Nat(l))
    2.61 +    }
    2.62 +
    2.63 +  def <=(that: Nat): Boolean = this.value <= that.value
    2.64 +
    2.65 +  def <(that: Nat): Boolean = this.value < that.value
    2.66 +
    2.67 +}
    2.68 +*}
    2.69 +
    2.70 +code_reserved Scala Nat
    2.71 +
    2.72  code_type nat
    2.73    (Haskell "Nat.Nat")
    2.74 +  (Scala "Nat.Nat")
    2.75  
    2.76  code_instance nat :: eq
    2.77    (Haskell -)
    2.78 @@ -303,7 +347,9 @@
    2.79  
    2.80  setup {*
    2.81    fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    2.82 -    false true) ["SML", "OCaml", "Haskell"]
    2.83 +    false true Code_Printer.str) ["SML", "OCaml", "Haskell"]
    2.84 +  #> Numeral.add_code @{const_name number_nat_inst.number_of_nat}
    2.85 +    false true (fn s => (Pretty.block o map Code_Printer.str) ["Nat.Nat", s]) "Scala"
    2.86  *}
    2.87  
    2.88  text {*
    2.89 @@ -349,10 +395,11 @@
    2.90    (SML "IntInf.max/ (/0,/ _)")
    2.91    (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
    2.92  
    2.93 -text {* For Haskell, things are slightly different again. *}
    2.94 +text {* For Haskell ans Scala, things are slightly different again. *}
    2.95  
    2.96  code_const int and nat
    2.97    (Haskell "toInteger" and "fromInteger")
    2.98 +  (Scala "!_.as'_BigInt" and "!Nat.Nat((_))")
    2.99  
   2.100  text {* Conversion from and to indices. *}
   2.101  
   2.102 @@ -360,11 +407,13 @@
   2.103    (SML "IntInf.toInt")
   2.104    (OCaml "_")
   2.105    (Haskell "fromEnum")
   2.106 +  (Scala "!_.as'_BigInt")
   2.107  
   2.108  code_const Code_Numeral.nat_of
   2.109    (SML "IntInf.fromInt")
   2.110    (OCaml "_")
   2.111    (Haskell "toEnum")
   2.112 +  (Scala "!Nat.Nat((_))")
   2.113  
   2.114  text {* Using target language arithmetic operations whenever appropriate *}
   2.115  
   2.116 @@ -372,31 +421,45 @@
   2.117    (SML "IntInf.+ ((_), (_))")
   2.118    (OCaml "Big'_int.add'_big'_int")
   2.119    (Haskell infixl 6 "+")
   2.120 +  (Scala infixl 7 "+")
   2.121 +
   2.122 +code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
   2.123 +  (Haskell infixl 6 "-")
   2.124 +  (Scala infixl 7 "-")
   2.125  
   2.126  code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
   2.127    (SML "IntInf.* ((_), (_))")
   2.128    (OCaml "Big'_int.mult'_big'_int")
   2.129    (Haskell infixl 7 "*")
   2.130 +  (Scala infixl 8 "*")
   2.131  
   2.132  code_const divmod_aux
   2.133    (SML "IntInf.divMod/ ((_),/ (_))")
   2.134    (OCaml "Big'_int.quomod'_big'_int")
   2.135    (Haskell "divMod")
   2.136 +  (Scala infixl 8 "/%")
   2.137 +
   2.138 +code_const divmod_nat
   2.139 +  (Haskell "divMod")
   2.140 +  (Scala infixl 8 "/%")
   2.141  
   2.142  code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   2.143    (SML "!((_ : IntInf.int) = _)")
   2.144    (OCaml "Big'_int.eq'_big'_int")
   2.145    (Haskell infixl 4 "==")
   2.146 +  (Scala infixl 5 "==")
   2.147  
   2.148  code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   2.149    (SML "IntInf.<= ((_), (_))")
   2.150    (OCaml "Big'_int.le'_big'_int")
   2.151    (Haskell infix 4 "<=")
   2.152 +  (Scala infixl 4 "<=")
   2.153  
   2.154  code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   2.155    (SML "IntInf.< ((_), (_))")
   2.156    (OCaml "Big'_int.lt'_big'_int")
   2.157    (Haskell infix 4 "<")
   2.158 +  (Scala infixl 4 "<")
   2.159  
   2.160  consts_code
   2.161    "0::nat"                     ("0")