merged

--- a/Admin/jenkins/build/ci_build_benchmark.scala	Thu Jun 23 23:08:37 2016 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Thu Jun 23 23:10:19 2016 +0200
@@ -4,7 +4,7 @@
   import isabelle._
 
   def threads = 8
-  def jobs = 1
+  def jobs = 2
   def all = false
   def groups = Nil
   def exclude = Nil

--- a/Admin/jenkins/build/ci_build_makeall.scala	Thu Jun 23 23:08:37 2016 +0200
+++ b/Admin/jenkins/build/ci_build_makeall.scala	Thu Jun 23 23:10:19 2016 +0200
@@ -3,8 +3,8 @@
 
   import isabelle._
 
-  def threads = 4
-  def jobs = 2
+  def threads = 2
+  def jobs = 3
   def all = true
   def groups = Nil
   def exclude = Nil

--- a/NEWS	Thu Jun 23 23:08:37 2016 +0200
+++ b/NEWS	Thu Jun 23 23:10:19 2016 +0200
@@ -129,6 +129,10 @@
 different phases of code generation. See src/HOL/ex/Code_Timing.thy for
 examples.
 
+* Code generator: implicits in Scala (stemming from type class instances)
+are generated into companion object of corresponding type class, to resolve
+some situations where ambiguities may occur.
+
 
 *** HOL ***
 

--- a/src/HOL/Library/Code_Target_Int.thy	Thu Jun 23 23:08:37 2016 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Thu Jun 23 23:10:19 2016 +0200
@@ -95,6 +95,8 @@
   "k < l \<longleftrightarrow> (of_int k :: integer) < of_int l"
   by transfer rule
 
+declare [[code drop: "gcd :: int \<Rightarrow> _" "lcm :: int \<Rightarrow> _"]]
+
 lemma gcd_int_of_integer [code]:
   "gcd (int_of_integer x) (int_of_integer y) = int_of_integer (gcd x y)"
 by transfer rule

--- a/src/Pure/Tools/ci_profile.scala	Thu Jun 23 23:08:37 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala	Thu Jun 23 23:10:19 2016 +0200
@@ -16,16 +16,17 @@
   private def print_variable(name: String): Unit =
   {
     val value = Isabelle_System.getenv_strict(name)
-    println(s"""$name="$value"""")
+    println(name + "=" + Outer_Syntax.quote_string(value))
   }
 
   protected def hg_id(path: Path): String =
     Isabelle_System.hg("id -i", path.file).out
 
-  private def build(options: Options): Build.Results =
+  private def build(options: Options): (Build.Results, Time) =
   {
+    val start_time = Time.now()
     val progress = new Console_Progress(true)
-    progress.interrupt_handler {
+    val results = progress.interrupt_handler {
       Build.build(
         options = options,
         progress = progress,
@@ -40,6 +41,8 @@
         system_mode = true
       )
     }
+    val end_time = Time.now()
+    (results, end_time - start_time)
   }
 
   private def load_properties(): JProperties =
@@ -51,15 +54,18 @@
     props
   }
 
+  protected def print_section(title: String): Unit =
+    println(s"\n=== $title ===\n")
+
 
   override final def apply(args: List[String]): Unit =
   {
+    print_section("CONFIGURATION")
     List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS").foreach(print_variable)
     val props = load_properties()
     System.getProperties().putAll(props)
 
     val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
-    println(s"Build for Isabelle id ${hg_id(isabelle_home)}")
 
     val options =
       Options.init()
@@ -69,13 +75,20 @@
         .int.update("parallel_proofs", 2)
         .int.update("threads", threads)
 
+    print_section("BUILD")
+    println(s"Build for Isabelle id ${hg_id(isabelle_home)}")
     pre_hook(args)
 
-    val results = build(options)
+    val (results, elapsed_time) = build(options)
+
+    print_section("TIMING")
+    val total_timing =
+      (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
+        copy(elapsed = elapsed_time)
+    println(total_timing.message_resources)
 
     if (!results.ok) {
-      println()
-      println("=== FAILED SESSIONS ===")
+      print_section("FAILED SESSIONS")
 
       for (name <- results.sessions) {
         if (results.cancelled(name)) {

--- a/src/Tools/Code/code_scala.ML	Thu Jun 23 23:08:37 2016 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jun 23 23:10:19 2016 +0200
@@ -13,8 +13,6 @@
 structure Code_Scala : CODE_SCALA =
 struct
 
-val target = "Scala";
-
 open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 open Code_Printer;
@@ -29,6 +27,15 @@
 
 (** Scala serializer **)
 
+val target = "Scala";
+
+datatype scala_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list
+  | Datatype of vname list * ((string * vname list) * itype list) list
+  | Class of (vname * ((class * class) list * (string * itype) list))
+      * (string * { vs: (vname * sort) list,
+      inst_params: ((string * (const * int)) * (thm * bool)) list,
+      superinst_params: ((string * (const * int)) * (thm * bool)) list }) list;
+
 fun print_scala_stmt tyco_syntax const_syntax reserved
     args_num is_constr (deresolve, deresolve_full) =
   let
@@ -172,14 +179,14 @@
             |> single
             |> enclose "(" ")"
           end;
-    fun print_context tyvars vs sym = applify "[" "]"
+    fun print_context tyvars vs s = applify "[" "]"
       (fn (v, sort) => (Pretty.block o map str)
         (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
-          NOBR ((str o deresolve) sym) vs;
+          NOBR (str s) vs;
     fun print_defhead export tyvars vars const vs params tys ty =
       concat [str "def", constraint (applify "(" ")" (fn (param, ty) =>
         constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
-          NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
+          NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
             str "="];
     fun print_def export const (vs, ty) [] =
           let
@@ -233,9 +240,38 @@
               (map print_clause eqs)
           end;
     val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
-    fun print_stmt (Constant const, (export, Code_Thingol.Fun (((vs, ty), raw_eqs), _))) =
+    fun print_inst class (tyco, { vs, inst_params, superinst_params }) =
+      let
+        val tyvars = intro_tyvars vs reserved;
+        val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
+        fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) =
+          let
+            val aux_dom = Name.invent_names (snd reserved) "a" dom;
+            val auxs = map fst aux_dom;
+            val vars = intro_vars auxs reserved;
+            val (aux_dom1, aux_dom2) = chop dom_length aux_dom;
+            fun abstract_using [] = []
+              | abstract_using aux_dom = [enum "," "(" ")"
+                  (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+                  (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
+            val aux_abstr1 = abstract_using aux_dom1;
+            val aux_abstr2 = abstract_using aux_dom2;
+          in
+            concat ([str "val", print_method classparam, str "="]
+              @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
+                (const, map (IVar o SOME) auxs))
+          end;
+      in
+        Pretty.block_enclose (concat [str "implicit def",
+          constraint (print_context tyvars vs
+            ((Library.enclose "`" "`" o deresolve_full o Class_Instance) (tyco, class)))
+          (print_dicttyp tyvars classtyp),
+          str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
+            (map print_classparam_instance (inst_params @ superinst_params))
+      end;
+    fun print_stmt (Constant const, (export, Fun ((vs, ty), raw_eqs))) =
           print_def export const (vs, ty) (filter (snd o snd) raw_eqs)
-      | print_stmt (Type_Constructor tyco, (export, Code_Thingol.Datatype (vs, cos))) =
+      | print_stmt (Type_Constructor tyco, (export, Datatype (vs, cos))) =
           let
             val tyvars = intro_tyvars (map (rpair []) vs) reserved;
             fun print_co ((co, vs_args), tys) =
@@ -252,7 +288,7 @@
               NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
                 :: map print_co cos)
           end
-      | print_stmt (Type_Class class, (export, Code_Thingol.Class (v, (classrels, classparams)))) =
+      | print_stmt (Type_Class class, (export, Class ((v, (classrels, classparams)), insts))) =
           let
             val tyvars = intro_tyvars [(v, [class])] reserved;
             fun add_typarg s = Pretty.block
@@ -286,38 +322,24 @@
                   @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
                 (map print_classparam_val classparams))
               :: map print_classparam_def classparams
+              @| Pretty.block_enclose
+                ((concat o map str) ["object", deresolve_class class, "{"], str "}")
+                (map (print_inst class) insts)
             )
-          end
-      | print_stmt (sym, (export, Code_Thingol.Classinst
-          { class, tyco, vs, inst_params, superinst_params, ... })) =
-          let
-            val tyvars = intro_tyvars vs reserved;
-            val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
-            fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) =
-              let
-                val aux_dom = Name.invent_names (snd reserved) "a" dom;
-                val auxs = map fst aux_dom;
-                val vars = intro_vars auxs reserved;
-                val (aux_dom1, aux_dom2) = chop dom_length aux_dom;
-                fun abstract_using [] = []
-                  | abstract_using aux_dom = [enum "," "(" ")"
-                      (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
-                      (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
-                val aux_abstr1 = abstract_using aux_dom1;
-                val aux_abstr2 = abstract_using aux_dom2;
-              in
-                concat ([str "val", print_method classparam, str "="]
-                  @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
-                    (const, map (IVar o SOME) auxs))
-              end;
-          in
-            Pretty.block_enclose (concat [str "implicit def",
-              constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp),
-              str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
-                (map print_classparam_instance (inst_params @ superinst_params))
           end;
   in print_stmt end;
 
+fun pickup_instances_for_class program =
+  let
+    val tab =
+      Symtab.empty
+      |> Code_Symbol.Graph.fold
+        (fn (_, (Code_Thingol.Classinst { class, tyco, vs, inst_params, superinst_params, ... }, _)) =>
+              Symtab.map_default (class, [])
+                (cons (tyco, { vs = vs, inst_params = inst_params, superinst_params = superinst_params }))
+           | _ => I) program;
+  in Symtab.lookup_list tab end;
+
 fun scala_program_of_program ctxt module_name reserved identifiers exports program =
   let
     val variant = if Config.get ctxt case_insensitive
@@ -348,26 +370,24 @@
       | namify_stmt (Code_Thingol.Classrel _) = namify_object
       | namify_stmt (Code_Thingol.Classparam _) = namify_object
       | namify_stmt (Code_Thingol.Classinst _) = namify_common;
-    fun memorize_implicits sym =
-      let
-        fun is_classinst stmt = case stmt
-         of Code_Thingol.Classinst _ => true
-          | _ => false;
-        val implicits = filter (is_classinst o Code_Symbol.Graph.get_node program)
-          (Code_Symbol.Graph.immediate_succs program sym);
-      in union (op =) implicits end;
+    val pickup_instances = pickup_instances_for_class program;
     fun modify_stmt (_, (_, Code_Thingol.Fun (_, SOME _))) = NONE
+      | modify_stmt (_, (export, Code_Thingol.Fun (x, NONE))) = SOME (export, Fun x)
+      | modify_stmt (_, (export, Code_Thingol.Datatype x)) = SOME (export, Datatype x)
       | modify_stmt (_, (_, Code_Thingol.Datatypecons _)) = NONE
+      | modify_stmt (Type_Class class, (export, Code_Thingol.Class x)) =
+          SOME (export, Class (x, pickup_instances class))
       | modify_stmt (_, (_, Code_Thingol.Classrel _)) = NONE
       | modify_stmt (_, (_, Code_Thingol.Classparam _)) = NONE
-      | modify_stmt (_, export_stmt) = SOME export_stmt;
+      | modify_stmt (_, (_, Code_Thingol.Classinst _)) = NONE
   in
     Code_Namespace.hierarchical_program ctxt
       { module_name = module_name, reserved = reserved, identifiers = identifiers,
         empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
         namify_stmt = namify_stmt, cyclic_modules = true,
-        class_transitive = true, class_relation_public = false, empty_data = [],
-        memorize_data = memorize_implicits, modify_stmts = map modify_stmt } exports program
+        class_transitive = true, class_relation_public = false, empty_data = (),
+        memorize_data = K I, modify_stmts = map modify_stmt }
+      exports program
   end;
 
 fun serialize_scala ctxt { module_name, reserved_syms, identifiers,
@@ -398,16 +418,9 @@
       (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []);
 
     (* print modules *)
-    fun print_implicit prefix_fragments implicit =
-      let
-        val s = deresolver prefix_fragments implicit;
-      in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
-    fun print_module prefix_fragments base implicits ps = Pretty.chunks2
-      ([str ("object " ^ base ^ " {")]
-        @ (case map_filter (print_implicit prefix_fragments) implicits
-            of [] => [] | implicit_ps => (single o Pretty.block)
-            (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
-        @ ps @ [str ("} /* object " ^ base ^ " */")]);
+    fun print_module _ base _ ps = Pretty.chunks2
+      (str ("object " ^ base ^ " {")
+        :: ps @| str ("} /* object " ^ base ^ " */"));
 
     (* serialization *)
     val p = Pretty.chunks2 (map snd includes