1(* Title: Tools/Code/code_scala.ML 2 Author: Florian Haftmann, TU Muenchen 3 4Serializer for Scala. 5*) 6 7signature CODE_SCALA = 8sig 9 val target: string 10end; 11 12structure Code_Scala : CODE_SCALA = 13struct 14 15open Basic_Code_Symbol; 16open Basic_Code_Thingol; 17open Code_Printer; 18 19infixr 5 @@; 20infixr 5 @|; 21 22(** Scala serializer **) 23 24val target = "Scala"; 25 26val print_scala_string = 27 let 28 fun chr i = "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX i) 29 fun char c = if c = "'" then "\\'" 30 else if c = "\"" then "\\\"" 31 else if c = "\\" then "\\\\" 32 else 33 let 34 val i = ord c 35 in 36 if i < 32 orelse i > 126 37 then chr i 38 else if i >= 128 39 then error "non-ASCII byte in Scala string literal" 40 else c 41 end 42 in quote o translate_string char end; 43 44datatype scala_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list 45 | Datatype of vname list * ((string * vname list) * itype list) list 46 | Class of (vname * ((class * class) list * (string * itype) list)) 47 * (string * { vs: (vname * sort) list, 48 inst_params: ((string * (const * int)) * (thm * bool)) list, 49 superinst_params: ((string * (const * int)) * (thm * bool)) list }) list; 50 51fun print_scala_stmt tyco_syntax const_syntax reserved 52 args_num is_constr (deresolve, deresolve_full) = 53 let 54 val deresolve_const = deresolve o Constant; 55 val deresolve_tyco = deresolve o Type_Constructor; 56 val deresolve_class = deresolve o Type_Class; 57 fun lookup_tyvar tyvars = lookup_var tyvars o Name.enforce_case true; 58 fun intro_tyvars vs = intro_vars (map (Name.enforce_case true o fst) vs); 59 fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]" 60 (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys 61 and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco 62 of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys) 63 | SOME (_, print) => print (print_typ tyvars) fxy tys) 64 | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v; 65 fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]); 66 fun print_tupled_typ tyvars ([], ty) = 67 print_typ tyvars NOBR ty 68 | print_tupled_typ tyvars ([ty1], ty2) = 69 concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2] 70 | print_tupled_typ tyvars (tys, ty) = 71 concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys), 72 str "=>", print_typ tyvars NOBR ty]; 73 fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2]; 74 fun print_var vars NONE = str "_" 75 | print_var vars (SOME v) = (str o lookup_var vars) v; 76 fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d 77 and applify_plain_dict tyvars (Dict_Const (inst, dss)) = 78 applify_dictss tyvars ((str o deresolve o Class_Instance) inst) dss 79 | applify_plain_dict tyvars (Dict_Var { var, class, ... }) = 80 Pretty.block [str "implicitly", 81 enclose "[" "]" [Pretty.block [(str o deresolve_class) class, 82 enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]] 83 and applify_dictss tyvars p dss = 84 applify "(" ")" (applify_dict tyvars) NOBR p (flat dss) 85 fun print_term tyvars is_pat some_thm vars fxy (IConst const) = 86 print_app tyvars is_pat some_thm vars fxy (const, []) 87 | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) = 88 (case Code_Thingol.unfold_const_app t 89 of SOME app => print_app tyvars is_pat some_thm vars fxy app 90 | _ => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy 91 (print_term tyvars is_pat some_thm vars BR t1) [t2]) 92 | print_term tyvars is_pat some_thm vars fxy (IVar v) = 93 print_var vars v 94 | print_term tyvars is_pat some_thm vars fxy (t as _ `|=> _) = 95 let 96 val (vs_tys, body) = Code_Thingol.unfold_abs t; 97 val (ps, vars') = fold_map (print_abs_head tyvars) vs_tys vars; 98 in 99 brackets (ps @| print_term tyvars false some_thm vars' NOBR body) 100 end 101 | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) = 102 (case Code_Thingol.unfold_const_app (#primitive case_expr) 103 of SOME (app as ({ sym = Constant const, ... }, _)) => 104 if is_none (const_syntax const) 105 then print_case tyvars some_thm vars fxy case_expr 106 else print_app tyvars is_pat some_thm vars fxy app 107 | NONE => print_case tyvars some_thm vars fxy case_expr) 108 and print_abs_head tyvars (some_v, ty) vars = 109 let 110 val vars' = intro_vars (the_list some_v) vars; 111 in 112 (concat [ 113 enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)], 114 str "=>" 115 ], vars') 116 end 117 and print_app tyvars is_pat some_thm vars fxy 118 (app as ({ sym, typargs, dom, dicts, ... }, ts)) = 119 let 120 val k = length ts; 121 val typargs' = if is_pat then [] else typargs; 122 val syntax = case sym of 123 Constant const => const_syntax const 124 | _ => NONE; 125 val applify_dicts = 126 if is_pat orelse is_some syntax orelse is_constr sym 127 orelse Code_Thingol.unambiguous_dictss dicts 128 then fn p => K p 129 else applify_dictss tyvars; 130 val (l, print') = case syntax of 131 NONE => (args_num sym, fn fxy => fn ts => applify_dicts 132 (gen_applify (is_constr sym) "(" ")" 133 (print_term tyvars is_pat some_thm vars NOBR) fxy 134 (applify "[" "]" (print_typ tyvars NOBR) 135 NOBR ((str o deresolve) sym) typargs') ts) dicts) 136 | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts 137 (applify "(" ")" 138 (print_term tyvars is_pat some_thm vars NOBR) fxy 139 (applify "[" "]" (print_typ tyvars NOBR) 140 NOBR (str s) typargs') ts) dicts) 141 | SOME (k, Complex_printer print) => 142 (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy 143 (ts ~~ take k dom)) 144 in if k = l then print' fxy ts 145 else if k < l then 146 print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app) 147 else let 148 val (ts1, ts23) = chop l ts; 149 in 150 Pretty.block (print' BR ts1 :: map (fn t => Pretty.block 151 [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23) 152 end end 153 and print_bind tyvars some_thm fxy p = 154 gen_print_bind (print_term tyvars true) some_thm fxy p 155 and print_case tyvars some_thm vars fxy { clauses = [], ... } = 156 (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"] 157 | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) = 158 let 159 val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr); 160 fun print_match_val ((pat, ty), t) vars = 161 vars 162 |> print_bind tyvars some_thm BR pat 163 |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty), 164 str "=", print_term tyvars false some_thm vars NOBR t])); 165 fun print_match_seq t vars = 166 ((true, print_term tyvars false some_thm vars NOBR t), vars); 167 fun print_match is_first ((IVar NONE, ty), t) = 168 if Code_Thingol.is_IAbs t andalso is_first 169 then print_match_val ((IVar NONE, ty), t) 170 else print_match_seq t 171 | print_match _ ((pat, ty), t) = 172 print_match_val ((pat, ty), t); 173 val (seps_ps, vars') = 174 vars |> print_match true bind ||>> fold_map (print_match false) binds |>> uncurry cons; 175 val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)]; 176 fun insert_seps [(_, p)] = [p] 177 | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) = 178 (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps 179 in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end 180 | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } = 181 let 182 fun print_select (pat, body) = 183 let 184 val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars; 185 val p_body = print_term tyvars false some_thm vars' NOBR body 186 in concat [str "case", p_pat, str "=>", p_body] end; 187 in 188 map print_select clauses 189 |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}") 190 |> single 191 |> enclose "(" ")" 192 end; 193 fun print_context tyvars vs s = applify "[" "]" 194 (fn (v, sort) => (Pretty.block o map str) 195 (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort)) 196 NOBR (str s) vs; 197 fun print_defhead tyvars vars const vs params tys ty = 198 concat [str "def", constraint (applify "(" ")" (fn (param, ty) => 199 constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty)) 200 NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty), 201 str "="]; 202 fun print_def const (vs, ty) [] = 203 let 204 val (tys, ty') = Code_Thingol.unfold_fun ty; 205 val params = Name.invent (snd reserved) "a" (length tys); 206 val tyvars = intro_tyvars vs reserved; 207 val vars = intro_vars params reserved; 208 in 209 concat [print_defhead tyvars vars const vs params tys ty', 210 str ("sys.error(" ^ print_scala_string const ^ ")")] 211 end 212 | print_def const (vs, ty) eqs = 213 let 214 val tycos = fold (fn ((ts, t), _) => 215 fold Code_Thingol.add_tyconames (t :: ts)) eqs []; 216 val tyvars = reserved 217 |> intro_base_names 218 (is_none o tyco_syntax) deresolve_tyco tycos 219 |> intro_tyvars vs; 220 val simple = case eqs 221 of [((ts, _), _)] => forall Code_Thingol.is_IVar ts 222 | _ => false; 223 val vars1 = reserved 224 |> intro_base_names_for (is_none o const_syntax) 225 deresolve (map (snd o fst) eqs); 226 val params = if simple 227 then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs 228 else aux_params vars1 (map (fst o fst) eqs); 229 val vars2 = intro_vars params vars1; 230 val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty; 231 fun tuplify [p] = p 232 | tuplify ps = enum "," "(" ")" ps; 233 fun print_rhs vars' ((_, t), (some_thm, _)) = 234 print_term tyvars false some_thm vars' NOBR t; 235 fun print_clause (eq as ((ts, _), (some_thm, _))) = 236 let 237 val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) 238 (insert (op =)) ts []) vars1; 239 in 240 concat [str "case", 241 tuplify (map (print_term tyvars true some_thm vars' NOBR) ts), 242 str "=>", print_rhs vars' eq] 243 end; 244 val head = print_defhead tyvars vars2 const vs params tys' ty'; 245 in if simple then 246 concat [head, print_rhs vars2 (hd eqs)] 247 else 248 Pretty.block_enclose 249 (concat [head, tuplify (map (str o lookup_var vars2) params), 250 str "match", str "{"], str "}") 251 (map print_clause eqs) 252 end; 253 val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant; 254 fun print_inst class (tyco, { vs, inst_params, superinst_params }) = 255 let 256 val tyvars = intro_tyvars vs reserved; 257 val classtyp = (class, tyco `%% map (ITyVar o fst) vs); 258 fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) = 259 let 260 val aux_dom = Name.invent_names (snd reserved) "a" dom; 261 val auxs = map fst aux_dom; 262 val vars = intro_vars auxs reserved; 263 val (aux_dom1, aux_dom2) = chop dom_length aux_dom; 264 fun abstract_using [] = [] 265 | abstract_using aux_dom = [enum "," "(" ")" 266 (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux) 267 (print_typ tyvars NOBR ty)) aux_dom), str "=>"]; 268 val aux_abstr1 = abstract_using aux_dom1; 269 val aux_abstr2 = abstract_using aux_dom2; 270 in 271 concat ([str "val", print_method classparam, str "="] 272 @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR 273 (const, map (IVar o SOME) auxs)) 274 end; 275 in 276 Pretty.block_enclose (concat [str "implicit def", 277 constraint (print_context tyvars vs 278 ((Library.enclose "`" "`" o deresolve_full o Class_Instance) (tyco, class))) 279 (print_dicttyp tyvars classtyp), 280 str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}") 281 (map print_classparam_instance (inst_params @ superinst_params)) 282 end; 283 fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) = 284 print_def const (vs, ty) (filter (snd o snd) raw_eqs) 285 | print_stmt (Type_Constructor tyco, (_, Datatype (vs, cos))) = 286 let 287 val tyvars = intro_tyvars (map (rpair []) vs) reserved; 288 fun print_co ((co, vs_args), tys) = 289 concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR 290 ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args) 291 @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) 292 (Name.invent_names (snd reserved) "a" tys))), 293 str "extends", 294 applify "[" "]" (str o lookup_tyvar tyvars) NOBR 295 ((str o deresolve_tyco) tyco) vs 296 ]; 297 in 298 Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars) 299 NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs 300 :: map print_co cos) 301 end 302 | print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) = 303 let 304 val tyvars = intro_tyvars [(v, [class])] reserved; 305 fun add_typarg s = Pretty.block 306 [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"]; 307 fun print_super_classes [] = NONE 308 | print_super_classes classrels = SOME (concat (str "extends" 309 :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels))); 310 fun print_classparam_val (classparam, ty) = 311 concat [str "val", constraint (print_method classparam) 312 ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)]; 313 fun print_classparam_def (classparam, ty) = 314 let 315 val (tys, ty) = Code_Thingol.unfold_fun ty; 316 val [implicit_name] = Name.invent (snd reserved) (lookup_tyvar tyvars v) 1; 317 val proto_vars = intro_vars [implicit_name] reserved; 318 val auxs = Name.invent (snd proto_vars) "a" (length tys); 319 val vars = intro_vars auxs proto_vars; 320 in 321 concat [str "def", constraint (Pretty.block [applify "(" ")" 322 (fn (aux, ty) => constraint ((str o lookup_var vars) aux) 323 (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam)) 324 (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ", 325 add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=", 326 applify "(" ")" (str o lookup_var vars) NOBR 327 (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs] 328 end; 329 in 330 Pretty.chunks ( 331 (Pretty.block_enclose 332 (concat ([str "trait", (add_typarg o deresolve_class) class] 333 @ the_list (print_super_classes classrels) @ [str "{"]), str "}") 334 (map print_classparam_val classparams)) 335 :: map print_classparam_def classparams 336 @| Pretty.block_enclose 337 ((concat o map str) ["object", deresolve_class class, "{"], str "}") 338 (map (print_inst class) insts) 339 ) 340 end; 341 in print_stmt end; 342 343fun pickup_instances_for_class program = 344 let 345 val tab = 346 Symtab.empty 347 |> Code_Symbol.Graph.fold 348 (fn (_, (Code_Thingol.Classinst { class, tyco, vs, inst_params, superinst_params, ... }, _)) => 349 Symtab.map_default (class, []) 350 (cons (tyco, { vs = vs, inst_params = inst_params, superinst_params = superinst_params })) 351 | _ => I) program; 352 in Symtab.lookup_list tab end; 353 354fun scala_program_of_program ctxt case_insensitive module_name reserved identifiers exports program = 355 let 356 val variant = if case_insensitive 357 then Code_Namespace.variant_case_insensitive 358 else Name.variant; 359 fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) = 360 let 361 val declare = Name.declare name_fragment; 362 in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end; 363 fun namify_class base ((nsp_class, nsp_object), nsp_common) = 364 let 365 val (base', nsp_class') = variant base nsp_class 366 in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end; 367 fun namify_object base ((nsp_class, nsp_object), nsp_common) = 368 let 369 val (base', nsp_object') = variant base nsp_object 370 in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end; 371 fun namify_common base ((nsp_class, nsp_object), nsp_common) = 372 let 373 val (base', nsp_common') = variant base nsp_common 374 in 375 (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) 376 end; 377 fun namify_stmt (Code_Thingol.Fun _) = namify_object 378 | namify_stmt (Code_Thingol.Datatype _) = namify_class 379 | namify_stmt (Code_Thingol.Datatypecons _) = namify_common 380 | namify_stmt (Code_Thingol.Class _) = namify_class 381 | namify_stmt (Code_Thingol.Classrel _) = namify_object 382 | namify_stmt (Code_Thingol.Classparam _) = namify_object 383 | namify_stmt (Code_Thingol.Classinst _) = namify_common; 384 val pickup_instances = pickup_instances_for_class program; 385 fun modify_stmt (_, (_, Code_Thingol.Fun (_, SOME _))) = NONE 386 | modify_stmt (_, (export, Code_Thingol.Fun (x, NONE))) = SOME (export, Fun x) 387 | modify_stmt (_, (export, Code_Thingol.Datatype x)) = SOME (export, Datatype x) 388 | modify_stmt (_, (_, Code_Thingol.Datatypecons _)) = NONE 389 | modify_stmt (Type_Class class, (export, Code_Thingol.Class x)) = 390 SOME (export, Class (x, pickup_instances class)) 391 | modify_stmt (_, (_, Code_Thingol.Classrel _)) = NONE 392 | modify_stmt (_, (_, Code_Thingol.Classparam _)) = NONE 393 | modify_stmt (_, (_, Code_Thingol.Classinst _)) = NONE 394 in 395 Code_Namespace.hierarchical_program ctxt 396 { module_name = module_name, reserved = reserved, identifiers = identifiers, 397 empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, 398 namify_stmt = namify_stmt, cyclic_modules = true, 399 class_transitive = true, class_relation_public = false, empty_data = (), 400 memorize_data = K I, modify_stmts = map modify_stmt } 401 exports program 402 end; 403 404fun serialize_scala case_insensitive ctxt { module_name, reserved_syms, identifiers, 405 includes, class_syntax, tyco_syntax, const_syntax } exports program = 406 let 407 408 (* build program *) 409 val { deresolver, hierarchical_program = scala_program } = 410 scala_program_of_program ctxt case_insensitive module_name (Name.make_context reserved_syms) 411 identifiers exports program; 412 413 (* print statements *) 414 fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco) 415 of Code_Thingol.Datatype (_, constrs) => 416 the (AList.lookup (op = o apsnd fst) constrs constr); 417 fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Type_Class class) 418 of Code_Thingol.Class (_, (_, classparams)) => classparams; 419 fun args_num (sym as Constant const) = case Code_Symbol.Graph.get_node program sym 420 of Code_Thingol.Fun (((_, ty), []), _) => 421 (length o fst o Code_Thingol.unfold_fun) ty 422 | Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts 423 | Code_Thingol.Datatypecons tyco => length (lookup_constr tyco const) 424 | Code_Thingol.Classparam class => 425 (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) 426 (classparams_of_class class)) const; 427 fun print_stmt prefix_fragments = print_scala_stmt 428 tyco_syntax const_syntax (make_vars reserved_syms) args_num 429 (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []); 430 431 (* print modules *) 432 fun print_module _ base _ ps = Pretty.chunks2 433 (str ("object " ^ base ^ " {") 434 :: ps @| str ("} /* object " ^ base ^ " */")); 435 436 (* serialization *) 437 val p = Pretty.chunks2 (map snd includes 438 @ Code_Namespace.print_hierarchical { 439 print_module = print_module, print_stmt = print_stmt, 440 lift_markup = I } scala_program); 441 fun write width NONE = writeln o format [] width 442 | write width (SOME p) = File.write p o format [] width; 443 fun prepare syms width p = ([("", format syms width p)], try (deresolver [])); 444 in 445 Code_Target.serialization write prepare p 446 end; 447 448val serializer : Code_Target.serializer = 449 Code_Target.parse_args (Scan.optional (Args.$$$ "case_insensitive" >> K true) false 450 >> (fn case_insensitive => serialize_scala case_insensitive)); 451 452val literals = let 453 fun numeral_scala k = 454 if ~2147483647 < k andalso k <= 2147483647 455 then signed_string_of_int k 456 else quote (signed_string_of_int k) 457in Literals { 458 literal_string = print_scala_string, 459 literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")", 460 literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps], 461 infix_cons = (6, "::") 462} end; 463 464 465(** Isar setup **) 466 467val _ = Theory.setup 468 (Code_Target.add_language 469 (target, { serializer = serializer, literals = literals, 470 check = { env_var = "SCALA_HOME", 471 make_destination = fn p => Path.append p (Path.explode "ROOT.scala"), 472 make_command = fn _ => 473 "isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"}, 474 evaluation_args = Token.explode0 Keyword.empty_keywords "case_insensitive"}) 475 #> Code_Target.set_printings (Type_Constructor ("fun", 476 [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => 477 brackify_infix (1, R) fxy ( 478 print_typ BR ty1 (*product type vs. tupled arguments!*), 479 str "=>", 480 print_typ (INFX (1, R)) ty2 481 )))])) 482 #> fold (Code_Target.add_reserved target) [ 483 "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false", 484 "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy", 485 "match", "new", "null", "object", "override", "package", "private", "protected", 486 "requires", "return", "sealed", "super", "this", "throw", "trait", "try", 487 "true", "type", "val", "var", "while", "with", "yield" 488 ] 489 #> fold (Code_Target.add_reserved target) [ 490 "apply", "sys", "scala", "BigInt", "Nil", "List" 491 ]); 492 493end; (*struct*) 494