# HG changeset patch
# User haftmann
# Date 1441570492 -7200
# Node ID 8e736ce4c6f46c25d97691108de047509c6f25a4
# Parent  774752af4a1ff3de5a9708a0adfad2cbd77ff662
unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup

diff -r 774752af4a1f -r 8e736ce4c6f4 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Sun Sep 06 22:14:52 2015 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Sun Sep 06 22:14:52 2015 +0200
@@ -55,4 +55,10 @@
 where
   "check_list = (if funny_list = funny_list' then () else undefined)"
 
+text \<open>Explicit check in @{text Scala} for correct bracketing of abstractions\<close>
+
+definition funny_funs :: "(bool \<Rightarrow> bool) list \<Rightarrow> (bool \<Rightarrow> bool) list"
+where
+  "funny_funs fs = (\<lambda>x. x \<or> True) # (\<lambda>x. x \<or> False) # fs"
+
 end
diff -r 774752af4a1f -r 8e736ce4c6f4 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sun Sep 06 22:14:52 2015 +0200
+++ b/src/Tools/Code/code_scala.ML	Sun Sep 06 22:14:52 2015 +0200
@@ -63,15 +63,13 @@
                 (print_term tyvars is_pat some_thm vars BR t1) [t2])
       | print_term tyvars is_pat some_thm vars fxy (IVar v) =
           print_var vars v
-      | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
+      | print_term tyvars is_pat some_thm vars fxy (t as _ `|=> _) =
           let
-            val vars' = intro_vars (the_list v) vars;
+            val (vs_tys, body) = Code_Thingol.unfold_abs t;
+            val (ps, vars') = fold_map (print_abs_head tyvars) vs_tys vars;
+            val vars' = intro_vars (map_filter fst vs_tys) vars;
           in
-            concat [
-              enclose "(" ")" [constraint (print_var vars' v) (print_typ tyvars NOBR ty)],
-              str "=>",
-              print_term tyvars false some_thm vars' NOBR t
-            ]
+            brackets (ps @| print_term tyvars false some_thm vars' NOBR body)
           end
       | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)
@@ -80,6 +78,15 @@
                 then print_case tyvars some_thm vars fxy case_expr
                 else print_app tyvars is_pat some_thm vars fxy app
             | NONE => print_case tyvars some_thm vars fxy case_expr)
+    and print_abs_head tyvars (some_v, ty) vars =
+           let
+             val vars' = intro_vars (the_list some_v) vars;
+           in
+             (concat [
+               enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)],
+               str "=>"
+             ], vars')
+           end
     and print_app tyvars is_pat some_thm vars fxy
         (app as ({ sym, typargs, dom, ... }, ts)) =
       let