# HG changeset patch
# User haftmann
# Date 1263490935 -3600
# Node ID 9c4d5db7c7ad830130d2f46f4b7e14ab3c5be646
# Parent  a22b09addd78c28970a19049bfa883b017997a1d# Parent  d75704c60768fdc4b0785ca4076c80348e9a3be6
merged

diff -r a22b09addd78 -r 9c4d5db7c7ad src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Jan 14 09:18:08 2010 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Jan 14 18:42:15 2010 +0100
@@ -296,8 +296,11 @@
 
 setup {*
   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
-    false false) ["SML", "Haskell", "Scala"]
-  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml"
+    false false Code_Printer.str) ["SML", "Haskell"]
+  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false true Code_Printer.str "OCaml"
+  #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
+    false false Code_Printer.str "Scala"
 *}
 
 code_reserved SML Int int
@@ -323,9 +326,10 @@
   (Scala infixl 8 "*")
 
 code_const div_mod_code_numeral
-  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
-  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
+  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+  (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   (Haskell "divMod")
+  (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))")
 
 code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
@@ -337,12 +341,12 @@
   (SML "Int.<=/ ((_),/ (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
-  (Scala infix 4 "<=")
+  (Scala infixl 4 "<=")
 
 code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "Int.</ ((_),/ (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
-  (Scala infix 4 "<")
+  (Scala infixl 4 "<")
 
 end
diff -r a22b09addd78 -r 9c4d5db7c7ad src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Thu Jan 14 09:18:08 2010 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Thu Jan 14 18:42:15 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 *}
 
diff -r a22b09addd78 -r 9c4d5db7c7ad src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 09:18:08 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Jan 14 18:42:15 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,53 @@
 
 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 as_Int: Int = 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 +348,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 +396,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 +408,13 @@
   (SML "IntInf.toInt")
   (OCaml "_")
   (Haskell "fromEnum")
+  (Scala "!_.as'_Int")
 
 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 +422,45 @@
   (SML "IntInf.+ ((_), (_))")
   (OCaml "Big'_int.add'_big'_int")
   (Haskell infixl 6 "+")
+  (Scala infixl 7 "+")
+
+code_const "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"
+  (Haskell infixl 6 "-")
+  (Scala infixl 7 "-")
 
 code_const "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> 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 \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
+  (Scala infixl 5 "==")
 
 code_const "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "IntInf.<= ((_), (_))")
   (OCaml "Big'_int.le'_big'_int")
   (Haskell infix 4 "<=")
+  (Scala infixl 4 "<=")
 
 code_const "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "IntInf.< ((_), (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
+  (Scala infixl 4 "<")
 
 consts_code
   "0::nat"                     ("0")
diff -r a22b09addd78 -r 9c4d5db7c7ad src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Jan 14 09:18:08 2010 +0100
+++ b/src/HOL/Product_Type.thy	Thu Jan 14 18:42:15 2010 +0100
@@ -1000,7 +1000,7 @@
   (SML infix 2 "*")
   (OCaml infix 2 "*")
   (Haskell "!((_),/ (_))")
-  (Scala "!((_),/ (_))")
+  (Scala "((_),/ (_))")
 
 code_instance * :: eq
   (Haskell -)
diff -r a22b09addd78 -r 9c4d5db7c7ad src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Jan 14 09:18:08 2010 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Thu Jan 14 18:42:15 2010 +0100
@@ -34,7 +34,7 @@
 val collect_mem_simproc =
   Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
-         let val (u, Ts, ps) = HOLogic.strip_psplits t
+         let val (u, _, ps) = HOLogic.strip_psplits t
          in case u of
            (c as Const ("op :", _)) $ q $ S' =>
              (case try (HOLogic.strip_ptuple ps) q of
diff -r a22b09addd78 -r 9c4d5db7c7ad src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Thu Jan 14 09:18:08 2010 +0100
+++ b/src/HOL/Tools/numeral.ML	Thu Jan 14 18:42:15 2010 +0100
@@ -8,7 +8,7 @@
 sig
   val mk_cnumeral: int -> cterm
   val mk_cnumber: ctyp -> int -> cterm
-  val add_code: string -> bool -> bool -> string -> theory -> theory
+  val add_code: string -> bool -> bool -> (string -> Pretty.T) -> string -> theory -> theory
 end;
 
 structure Numeral: NUMERAL =
@@ -56,7 +56,7 @@
 
 local open Basic_Code_Thingol in
 
-fun add_code number_of negative unbounded target thy =
+fun add_code number_of negative unbounded print target thy =
   let
     fun dest_numeral pls' min' bit0' bit1' thm =
       let
@@ -74,11 +74,12 @@
           | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
       in dest_num end;
     fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
-      (Code_Printer.str o Code_Printer.literal_numeral literals unbounded
+      (print o Code_Printer.literal_numeral literals unbounded
         o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
   in
     thy |> Code_Target.add_syntax_const target number_of
-      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
+      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min},
+        @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
   end;
 
 end; (*local*)
diff -r a22b09addd78 -r 9c4d5db7c7ad src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Thu Jan 14 09:18:08 2010 +0100
+++ b/src/Pure/Isar/code.ML	Thu Jan 14 18:42:15 2010 +0100
@@ -746,6 +746,10 @@
                           :: Pretty.str "of"
                           :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
           );
+    fun pretty_case (const, (_, (_, []))) = Pretty.str (string_of_const thy const)
+      | pretty_case (const, (_, (_, cos))) = (Pretty.block o Pretty.breaks) [
+          Pretty.str (string_of_const thy const), Pretty.str "with",
+          (Pretty.block o Pretty.commas o map (Pretty.str o string_of_const thy)) cos];
     val eqns = the_eqns exec
       |> Symtab.dest
       |> (map o apfst) (string_of_const thy)
@@ -755,18 +759,26 @@
       |> Symtab.dest
       |> map (fn (dtco, (_, (vs, cos)) :: _) =>
           (string_of_typ thy (Type (dtco, map TFree vs)), cos))
-      |> sort (string_ord o pairself fst)
+      |> sort (string_ord o pairself fst);
+    val cases = Symtab.dest ((fst o the_cases o the_exec) thy);
+    val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy);
   in
     (Pretty.writeln o Pretty.chunks) [
       Pretty.block (
-        Pretty.str "code equations:"
-        :: Pretty.fbrk
+        Pretty.str "code equations:" :: Pretty.fbrk
         :: (Pretty.fbreaks o map pretty_eqns) eqns
       ),
       Pretty.block (
-        Pretty.str "datatypes:"
-        :: Pretty.fbrk
+        Pretty.str "datatypes:" :: Pretty.fbrk
         :: (Pretty.fbreaks o map pretty_dtyp) dtyps
+      ),
+      Pretty.block (
+        Pretty.str "cases:" :: Pretty.fbrk
+        :: (Pretty.fbreaks o map pretty_case) cases
+      ),
+      Pretty.block (
+        Pretty.str "undefined:" :: Pretty.fbrk
+        :: (Pretty.commas o map (Pretty.str o string_of_const thy)) undefineds
       )
     ]
   end;
diff -r a22b09addd78 -r 9c4d5db7c7ad src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jan 14 09:18:08 2010 +0100
+++ b/src/Tools/Code/code_scala.ML	Thu Jan 14 18:42:15 2010 +0100
@@ -71,7 +71,7 @@
               (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
                 (map (print_term tyvars is_pat thm vars NOBR) ts))
           | SOME (_, print) => (false, fn ts =>
-              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take k tys_args));
+              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take l tys_args));
       in if k = l then print' ts
       else if k < l then
         print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
@@ -404,11 +404,17 @@
     let
       val s = ML_Syntax.print_char c;
     in if s = "'" then "\\'" else s end;
+  fun bigint_scala k = "(" ^ (if k <= 2147483647
+    then string_of_int k else quote (string_of_int k)) ^ ")"
 in Literals {
   literal_char = Library.enclose "'" "'" o char_scala,
   literal_string = quote o translate_string char_scala,
-  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
-    else Library.enclose "(" ")" (signed_string_of_int k),
+  literal_numeral = fn unbounded => fn k => if k >= 0 then
+      if unbounded then bigint_scala k
+      else Library.enclose "(" ")" (string_of_int k)
+    else
+      if unbounded then "(- " ^ bigint_scala (~ k) ^ ")"
+      else Library.enclose "(" ")" (signed_string_of_int k),
   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   infix_cons = (6, "::")
 } end;
@@ -424,7 +430,7 @@
   Code_Target.add_target (target, (isar_seri_scala, literals))
   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy [
-        print_typ (INFX (1, X)) ty1,
+        print_typ BR ty1 (*product type vs. tupled arguments!*),
         str "=>",
         print_typ (INFX (1, R)) ty2
       ]))