tuned for products vs. tupled functions
authorhaftmann
Thu Jan 14 17:47:39 2010 +0100 (2010-01-14)
changeset 349009b12b0824bfe
parent 34899 8674bb6f727b
child 34901 0d6a2ae86525
tuned for products vs. tupled functions
src/HOL/Product_Type.thy
src/Tools/Code/code_scala.ML
     1.1 --- a/src/HOL/Product_Type.thy	Thu Jan 14 17:47:39 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Jan 14 17:47:39 2010 +0100
     1.3 @@ -1000,7 +1000,7 @@
     1.4    (SML infix 2 "*")
     1.5    (OCaml infix 2 "*")
     1.6    (Haskell "!((_),/ (_))")
     1.7 -  (Scala "!((_),/ (_))")
     1.8 +  (Scala "((_),/ (_))")
     1.9  
    1.10  code_instance * :: eq
    1.11    (Haskell -)
     2.1 --- a/src/Tools/Code/code_scala.ML	Thu Jan 14 17:47:39 2010 +0100
     2.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jan 14 17:47:39 2010 +0100
     2.3 @@ -71,7 +71,7 @@
     2.4                (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
     2.5                  (map (print_term tyvars is_pat thm vars NOBR) ts))
     2.6            | SOME (_, print) => (false, fn ts =>
     2.7 -              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take k tys_args));
     2.8 +              print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take l tys_args));
     2.9        in if k = l then print' ts
    2.10        else if k < l then
    2.11          print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
    2.12 @@ -404,11 +404,17 @@
    2.13      let
    2.14        val s = ML_Syntax.print_char c;
    2.15      in if s = "'" then "\\'" else s end;
    2.16 +  fun bigint_scala k = "(" ^ (if k <= 2147483647
    2.17 +    then string_of_int k else quote (string_of_int k)) ^ ")"
    2.18  in Literals {
    2.19    literal_char = Library.enclose "'" "'" o char_scala,
    2.20    literal_string = quote o translate_string char_scala,
    2.21 -  literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
    2.22 -    else Library.enclose "(" ")" (signed_string_of_int k),
    2.23 +  literal_numeral = fn unbounded => fn k => if k >= 0 then
    2.24 +      if unbounded then bigint_scala k
    2.25 +      else Library.enclose "(" ")" (string_of_int k)
    2.26 +    else
    2.27 +      if unbounded then "(- " ^ bigint_scala (~ k) ^ ")"
    2.28 +      else Library.enclose "(" ")" (signed_string_of_int k),
    2.29    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
    2.30    infix_cons = (6, "::")
    2.31  } end;
    2.32 @@ -424,7 +430,7 @@
    2.33    Code_Target.add_target (target, (isar_seri_scala, literals))
    2.34    #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    2.35        brackify_infix (1, R) fxy [
    2.36 -        print_typ (INFX (1, X)) ty1,
    2.37 +        print_typ BR ty1 (*product type vs. tupled arguments!*),
    2.38          str "=>",
    2.39          print_typ (INFX (1, R)) ty2
    2.40        ]))