--- a/src/HOL/Code_Numeral.thy Thu Jan 14 15:06:38 2010 +0100
+++ b/src/HOL/Code_Numeral.thy Thu Jan 14 18:44:22 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
--- a/src/HOL/Library/Code_Integer.thy Thu Jan 14 15:06:38 2010 +0100
+++ b/src/HOL/Library/Code_Integer.thy Thu Jan 14 18:44:22 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 *}
--- a/src/HOL/Library/Efficient_Nat.thy Thu Jan 14 15:06:38 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Jan 14 18:44:22 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")
--- a/src/HOL/Product_Type.thy Thu Jan 14 15:06:38 2010 +0100
+++ b/src/HOL/Product_Type.thy Thu Jan 14 18:44:22 2010 +0100
@@ -1000,7 +1000,7 @@
(SML infix 2 "*")
(OCaml infix 2 "*")
(Haskell "!((_),/ (_))")
- (Scala "!((_),/ (_))")
+ (Scala "((_),/ (_))")
code_instance * :: eq
(Haskell -)
--- a/src/HOL/Tools/inductive_set.ML Thu Jan 14 15:06:38 2010 +0100
+++ b/src/HOL/Tools/inductive_set.ML Thu Jan 14 18:44:22 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
--- a/src/HOL/Tools/numeral.ML Thu Jan 14 15:06:38 2010 +0100
+++ b/src/HOL/Tools/numeral.ML Thu Jan 14 18:44:22 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*)
--- a/src/Pure/Isar/code.ML Thu Jan 14 15:06:38 2010 +0100
+++ b/src/Pure/Isar/code.ML Thu Jan 14 18:44:22 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;
--- a/src/Tools/Code/code_scala.ML Thu Jan 14 15:06:38 2010 +0100
+++ b/src/Tools/Code/code_scala.ML Thu Jan 14 18:44:22 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
]))