src/Tools/Code/code_scala.ML
changeset 37453 44a307746163
parent 37450 45073611170a
child 37464 9250ad1b98e0
equal deleted inserted replaced
37452:8f515d6aded5 37453:44a307746163
   295               end;
   295               end;
   296             val head = print_defhead' tyvars reserved ((str o deresolve) name) vs [] [] classtyp;
   296             val head = print_defhead' tyvars reserved ((str o deresolve) name) vs [] [] classtyp;
   297             val body = [str "new", print_classtyp' classtyp,
   297             val body = [str "new", print_classtyp' classtyp,
   298               Pretty.enum ";" "{ " " }" (map print_classparam_instance (classparam_instances @ further_classparam_instances))];
   298               Pretty.enum ";" "{ " " }" (map print_classparam_instance (classparam_instances @ further_classparam_instances))];
   299           in concat (str "implicit" :: head :: body) end;
   299           in concat (str "implicit" :: head :: body) end;
   300           (*let
       
   301             val tyvars = intro_vars (map fst vs) reserved;
       
   302             val insttyp = tyco `%% map (ITyVar o fst) vs;
       
   303             val p_inst_typ = print_typ tyvars NOBR insttyp;
       
   304             fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs);
       
   305             fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"];
       
   306             val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved;
       
   307             fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
       
   308               let
       
   309                 val auxs = Name.invents (snd reserved) "a" (length tys);
       
   310                 val vars = intro_vars auxs reserved;
       
   311                 val args = if null auxs then [] else
       
   312                   [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
       
   313                     auxs tys), str "=>"]];
       
   314               in 
       
   315                 concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
       
   316                   str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
       
   317               end;
       
   318           in
       
   319             Pretty.chunks [
       
   320               Pretty.block_enclose
       
   321                 (concat ([str "trait",
       
   322                     add_typ_params ((str o deresolve_base) name),
       
   323                     str "extends",
       
   324                     Pretty.block [(str o deresolve) class, str "[", p_inst_typ, str "]"]]
       
   325                     @ map (fn (_, (_, (super_instance, _))) => add_typ_params (str ("with " ^ deresolve super_instance)))
       
   326                       super_instances @| str "{"), str "}")
       
   327                 (map (fn p => Pretty.block [str "implicit val arg$", p]) implicit_ps
       
   328                   @ map print_classparam_instance classparam_instances),
       
   329               concat [str "implicit", str (if null vs then "val" else "def"),
       
   330                 applify "(implicit " ")" NOBR (applify "[" "]" NOBR
       
   331                   ((str o deresolve_base) name) (map (str o lookup_tyvar tyvars o fst) vs))
       
   332                     implicit_ps,
       
   333                   str "=", str "new", applify "[" "]" NOBR ((str o deresolve_base) name)
       
   334                       (map (str o lookup_tyvar tyvars o fst) vs),
       
   335                     Pretty.enum ";" "{ " " }" (map (str o (fn v => "val arg$" ^ v ^ " = " ^ v) o lookup_var vars)
       
   336                       implicit_names)]
       
   337             ]
       
   338           end;*)
       
   339   in print_stmt end;
   300   in print_stmt end;
   340 
   301 
   341 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
   302 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
   342   let
   303   let
   343     val the_module_name = the_default "Program" module_name;
   304     val the_module_name = the_default "Program" module_name;