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 + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.+ ((_), (_))")
   (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
+  (Scala infixl 7 "+")
 
 code_const "uminus \<Colon> int \<Rightarrow> int"
   (SML "IntInf.~")
   (OCaml "Big'_int.minus'_big'_int")
   (Haskell "negate")
+  (Scala "!(- _)")
 
 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.- ((_), (_))")
   (OCaml "Big'_int.sub'_big'_int")
   (Haskell infixl 6 "-")
+  (Scala infixl 7 "-")
 
 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> 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 \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
+  (Scala infixl 5 "==")
 
 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "IntInf.<= ((_), (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
+  (Scala infixl 4 "<=")
 
 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> 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 *}