src/Tools/Code/code_scala.ML
author haftmann
Thu Jan 14 17:47:39 2010 +0100 (2010-01-14)
changeset 34900 9b12b0824bfe
parent 34888 460ec1a99aa2
child 34944 970e1466028d
permissions -rw-r--r--
tuned for products vs. tupled functions
     1 (*  Author:     Florian Haftmann, TU Muenchen
     2 
     3 Serializer for Scala.
     4 *)
     5 
     6 signature CODE_SCALA =
     7 sig
     8   val setup: theory -> theory
     9 end;
    10 
    11 structure Code_Scala : CODE_SCALA =
    12 struct
    13 
    14 val target = "Scala";
    15 
    16 open Basic_Code_Thingol;
    17 open Code_Printer;
    18 
    19 infixr 5 @@;
    20 infixr 5 @|;
    21 
    22 
    23 (** Scala serializer **)
    24 
    25 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton deresolve =
    26   let
    27     val deresolve_base = Long_Name.base_name o deresolve;
    28     fun print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
    29          of NONE => applify "[" "]" fxy
    30               ((str o deresolve) tyco) (map (print_typ tyvars NOBR) tys)
    31           | SOME (i, print) => print (print_typ tyvars) fxy tys)
    32       | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
    33     fun print_typed tyvars p ty =
    34       Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
    35     fun print_var vars NONE = str "_"
    36       | print_var vars (SOME v) = (str o lookup_var vars) v
    37     fun print_term tyvars is_pat thm vars fxy (IConst c) =
    38           print_app tyvars is_pat thm vars fxy (c, [])
    39       | print_term tyvars is_pat thm vars fxy (t as (t1 `$ t2)) =
    40           (case Code_Thingol.unfold_const_app t
    41            of SOME app => print_app tyvars is_pat thm vars fxy app
    42             | _ => applify "(" ")" fxy
    43                 (print_term tyvars is_pat thm vars BR t1)
    44                 [print_term tyvars is_pat thm vars NOBR t2])
    45       | print_term tyvars is_pat thm vars fxy (IVar v) =
    46           print_var vars v
    47       | print_term tyvars is_pat thm vars fxy ((v, ty) `|=> t) =
    48           let
    49             val vars' = intro_vars (the_list v) vars;
    50           in
    51             concat [
    52               Pretty.block [str "(", print_typed tyvars (print_var vars' v) ty, str ")"],
    53               str "=>",
    54               print_term tyvars false thm vars' NOBR t
    55             ]
    56           end 
    57       | print_term tyvars is_pat thm vars fxy (ICase (cases as (_, t0))) =
    58           (case Code_Thingol.unfold_const_app t0
    59            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    60                 then print_case tyvars thm vars fxy cases
    61                 else print_app tyvars is_pat thm vars fxy c_ts
    62             | NONE => print_case tyvars thm vars fxy cases)
    63     and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
    64       let
    65         val k = length ts;
    66         val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
    67         val tys' = if is_pat orelse
    68           (is_none (syntax_const c) andalso is_singleton c) then [] else tys;
    69         val (no_syntax, print') = case syntax_const c
    70          of NONE => (true, fn ts => applify "(" ")" fxy
    71               (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
    72                 (map (print_term tyvars is_pat thm vars NOBR) ts))
    73           | SOME (_, print) => (false, fn ts =>
    74               print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take l tys_args));
    75       in if k = l then print' ts
    76       else if k < l then
    77         print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
    78       else let
    79         val (ts1, ts23) = chop l ts;
    80       in
    81         Pretty.block (print' ts1 :: map (fn t => Pretty.block
    82           [str ".apply(", print_term tyvars is_pat thm vars NOBR t, str ")"]) ts23)
    83       end end
    84     and print_bind tyvars thm fxy p = gen_print_bind (print_term tyvars true) thm fxy p
    85     and print_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
    86           let
    87             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    88             fun print_match ((pat, ty), t) vars =
    89               vars
    90               |> print_bind tyvars thm BR pat
    91               |>> (fn p => semicolon [Pretty.block [str "val", Pretty.brk 1, p,
    92                 str ":", Pretty.brk 1, print_typ tyvars NOBR ty],
    93                   str "=", print_term tyvars false thm vars NOBR t])
    94             val (ps, vars') = fold_map print_match binds vars;
    95           in
    96             brackify_block fxy
    97               (str "{")
    98               (ps @| print_term tyvars false thm vars' NOBR body)
    99               (str "}")
   100           end
   101       | print_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
   102           let
   103             fun print_select (pat, body) =
   104               let
   105                 val (p, vars') = print_bind tyvars thm NOBR pat vars;
   106               in concat [str "case", p, str "=>", print_term tyvars false thm vars' NOBR body] end;
   107           in brackify_block fxy
   108             (concat [print_term tyvars false thm vars NOBR t, str "match", str "{"])
   109             (map print_select clauses)
   110             (str "}") 
   111           end
   112       | print_case tyvars thm vars fxy ((_, []), _) =
   113           (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
   114     fun implicit_arguments tyvars vs vars =
   115       let
   116         val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
   117           [(str o deresolve) class, str "[", (str o lookup_var tyvars) v, str "]"]) sort) vs;
   118         val implicit_names = Name.invents (snd vars) "a" (length implicit_typ_ps);
   119         val vars' = intro_vars implicit_names vars;
   120         val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
   121           implicit_names implicit_typ_ps;
   122       in ((implicit_names, implicit_ps), vars') end;
   123     fun print_defhead tyvars vars p vs params tys implicits ty =
   124       concat [str "def", print_typed tyvars (applify "(implicit " ")" NOBR
   125         (applify "(" ")" NOBR
   126           (applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs))
   127             (map2 (fn param => fn ty => print_typed tyvars
   128                 ((str o lookup_var vars) param) ty)
   129               params tys)) implicits) ty, str "="]
   130     fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs
   131          of [] =>
   132               let
   133                 val (tys, ty') = Code_Thingol.unfold_fun ty;
   134                 val params = Name.invents (snd reserved) "a" (length tys);
   135                 val tyvars = intro_vars (map fst vs) reserved;
   136                 val vars = intro_vars params reserved;
   137               in
   138                 concat [print_defhead tyvars vars ((str o deresolve) name) vs params tys [] ty',
   139                   str ("error(\"" ^ name ^ "\")")]
   140               end
   141           | eqs =>
   142               let
   143                 val tycos = fold (fn ((ts, t), (thm, _)) =>
   144                   fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
   145                 val tyvars = reserved
   146                   |> intro_base_names
   147                        (is_none o syntax_tyco) deresolve tycos
   148                   |> intro_vars (map fst vs);
   149                 val simple = case eqs
   150                  of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
   151                   | _ => false;
   152                 val consts = fold Code_Thingol.add_constnames
   153                   (map (snd o fst) eqs) [];
   154                 val vars1 = reserved
   155                   |> intro_base_names
   156                        (is_none o syntax_const) deresolve consts
   157                 val ((_, implicit_ps), vars2) = implicit_arguments tyvars vs vars1;
   158                 val params = if simple then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
   159                   else aux_params vars2 (map (fst o fst) eqs);
   160                 val vars3 = intro_vars params vars2;
   161                 val (tys, ty1) = Code_Thingol.unfold_fun ty;
   162                 val (tys1, tys2) = chop (length params) tys;
   163                 val ty2 = Library.foldr
   164                   (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
   165                 fun print_tuple [p] = p
   166                   | print_tuple ps = enum "," "(" ")" ps;
   167                 fun print_rhs vars' ((_, t), (thm, _)) = print_term tyvars false thm vars' NOBR t;
   168                 fun print_clause (eq as ((ts, _), (thm, _))) =
   169                   let
   170                     val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars2;
   171                   in
   172                     concat [str "case", print_tuple (map (print_term tyvars true thm vars' NOBR) ts),
   173                       str "=>", print_rhs vars' eq]
   174                   end;
   175                 val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 implicit_ps ty2;
   176               in if simple then
   177                 concat [head, print_rhs vars3 (hd eqs)]
   178               else
   179                 Pretty.block_enclose
   180                   (concat [head, print_tuple (map (str o lookup_var vars3) params),
   181                     str "match", str "{"], str "}")
   182                   (map print_clause eqs)
   183               end)
   184       | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
   185           let
   186             val tyvars = intro_vars (map fst vs) reserved;
   187             fun print_co (co, []) =
   188                   concat [str "final", str "case", str "object", (str o deresolve_base) co,
   189                     str "extends", applify "[" "]" NOBR ((str o deresolve_base) name)
   190                       (replicate (length vs) (str "Nothing"))]
   191               | print_co (co, tys) =
   192                   let
   193                     val fields = Name.names (snd reserved) "a" tys;
   194                     val vars = intro_vars (map fst fields) reserved;
   195                     fun add_typargs p = applify "[" "]" NOBR p
   196                       (map (str o lookup_var tyvars o fst) vs);
   197                   in
   198                     concat [
   199                       applify "(" ")" NOBR
   200                         (add_typargs ((concat o map str) ["final", "case", "class", deresolve_base co]))
   201                         (map (uncurry (print_typed tyvars) o apfst str) fields),
   202                       str "extends",
   203                       add_typargs ((str o deresolve_base) name)
   204                     ]
   205                   end
   206           in
   207             Pretty.chunks (
   208               applify "[" "]" NOBR ((concat o map str) ["sealed", "class", deresolve_base name])
   209                 (map (str o prefix "+" o lookup_var tyvars o fst) vs)
   210               :: map print_co cos
   211             )
   212           end
   213       | print_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) =
   214           let
   215             val tyvars = intro_vars [v] reserved;
   216             val vs = [(v, [name])];
   217             fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_var tyvars) v];
   218             fun print_superclasses [] = NONE
   219               | print_superclasses classes = SOME (concat (str "extends"
   220                   :: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
   221             fun print_tupled_typ ([], ty) =
   222                   print_typ tyvars NOBR ty
   223               | print_tupled_typ ([ty1], ty2) =
   224                   concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
   225               | print_tupled_typ (tys, ty) =
   226                   concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
   227                     str "=>", print_typ tyvars NOBR ty];
   228             fun print_classparam_val (classparam, ty) =
   229               concat [str "val", (str o suffix "$:" o deresolve_base) classparam,
   230                 (print_tupled_typ o Code_Thingol.unfold_fun) ty]
   231             fun print_classparam_def (classparam, ty) =
   232               let
   233                 val (tys, ty) = Code_Thingol.unfold_fun ty;
   234                 val params = Name.invents (snd reserved) "a" (length tys);
   235                 val vars = intro_vars params reserved;
   236                 val (([implicit], [p_implicit]), vars') = implicit_arguments tyvars vs vars;
   237                 val head = print_defhead tyvars vars' ((str o deresolve) classparam) vs params tys [p_implicit] ty;
   238               in
   239                 concat [head, applify "(" ")" NOBR
   240                   (Pretty.block [str implicit, str ".", (str o suffix "$" o deresolve_base) classparam])
   241                   (map (str o lookup_var vars') params)]
   242               end;
   243           in
   244             Pretty.chunks (
   245               (Pretty.block_enclose
   246                 (concat ([str "trait", add_typarg ((str o deresolve_base) name)]
   247                   @ the_list (print_superclasses superclasses) @ [str "{"]), str "}")
   248                 (map print_classparam_val classparams))
   249               :: map print_classparam_def classparams
   250             )
   251           end
   252       | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
   253             (super_instances, classparam_insts))) =
   254           let
   255             val tyvars = intro_vars (map fst vs) reserved;
   256             val insttyp = tyco `%% map (ITyVar o fst) vs;
   257             val p_inst_typ = print_typ tyvars NOBR insttyp;
   258             fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs);
   259             fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"];
   260             val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved;
   261             fun print_classparam_inst ((classparam, const as (_, (_, tys))), (thm, _)) =
   262               let
   263                 val auxs = Name.invents (snd reserved) "a" (length tys);
   264                 val vars = intro_vars auxs reserved;
   265                 val args = if null auxs then [] else
   266                   [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
   267                     auxs tys), str "=>"]];
   268               in 
   269                 concat ([str "val", (str o suffix "$" o deresolve_base) classparam,
   270                   str "="] @ args @ [print_app tyvars false thm vars NOBR (const, map (IVar o SOME) auxs)])
   271               end;
   272           in
   273             Pretty.chunks [
   274               Pretty.block_enclose
   275                 (concat ([str "trait",
   276                     add_typ_params ((str o deresolve_base) name),
   277                     str "extends",
   278                     Pretty.block [(str o deresolve) class, str "[", p_inst_typ, str "]"]]
   279                     @ map (fn (_, (_, (superinst, _))) => add_typ_params (str ("with " ^ deresolve superinst)))
   280                       super_instances @| str "{"), str "}")
   281                 (map (fn p => Pretty.block [str "implicit val arg$", p]) implicit_ps
   282                   @ map print_classparam_inst classparam_insts),
   283               concat [str "implicit", str (if null vs then "val" else "def"),
   284                 applify "(implicit " ")" NOBR (applify "[" "]" NOBR
   285                   ((str o deresolve_base) name) (map (str o lookup_var tyvars o fst) vs))
   286                     implicit_ps,
   287                   str "=", str "new", applify "[" "]" NOBR ((str o deresolve_base) name)
   288                       (map (str o lookup_var tyvars o fst) vs),
   289                     Pretty.enum ";" "{ " " }" (map (str o (fn v => "val arg$" ^ v ^ " = " ^ v) o lookup_var vars)
   290                       implicit_names)]
   291             ]
   292           end;
   293   in print_stmt end;
   294 
   295 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
   296   let
   297     val the_module_name = the_default "Program" module_name;
   298     val module_alias = K (SOME the_module_name);
   299     val reserved = Name.make_context reserved;
   300     fun prepare_stmt (name, stmt) (nsps, stmts) =
   301       let
   302         val (_, base) = Code_Printer.dest_name name;
   303         val mk_name_stmt = yield_singleton Name.variants;
   304         fun add_class ((nsp_class, nsp_object), nsp_common) =
   305           let
   306             val (base', nsp_class') = mk_name_stmt base nsp_class
   307           in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
   308         fun add_object ((nsp_class, nsp_object), nsp_common) =
   309           let
   310             val (base', nsp_object') = mk_name_stmt base nsp_object
   311           in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
   312         fun add_common upper ((nsp_class, nsp_object), nsp_common) =
   313           let
   314             val (base', nsp_common') =
   315               mk_name_stmt (if upper then first_upper base else base) nsp_common
   316           in (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) end;
   317         val add_name = case stmt
   318          of Code_Thingol.Fun _ => add_object
   319           | Code_Thingol.Datatype _ => add_class
   320           | Code_Thingol.Datatypecons _ => add_common true
   321           | Code_Thingol.Class _ => add_class
   322           | Code_Thingol.Classrel _ => add_object
   323           | Code_Thingol.Classparam _ => add_object
   324           | Code_Thingol.Classinst _ => add_common false;
   325         fun add_stmt base' = case stmt
   326          of Code_Thingol.Datatypecons _ => cons (name, (base', NONE))
   327           | Code_Thingol.Classrel _ => cons (name, (base', NONE))
   328           | Code_Thingol.Classparam _ => cons (name, (base', NONE))
   329           | _ => cons (name, (base', SOME stmt));
   330       in
   331         nsps
   332         |> add_name
   333         |-> (fn base' => rpair (add_stmt base' stmts))
   334       end;
   335     val (_, sca_program) = fold prepare_stmt (AList.make (fn name => Graph.get_node program name)
   336       (Graph.strong_conn program |> flat)) (((reserved, reserved), reserved), []);
   337     fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
   338       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   339   in (deresolver, (the_module_name, sca_program)) end;
   340 
   341 fun serialize_scala raw_module_name labelled_name
   342     raw_reserved includes raw_module_alias
   343     _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program cs destination =
   344   let
   345     val stmt_names = Code_Target.stmt_names_of_destination destination;
   346     val module_name = if null stmt_names then raw_module_name else SOME "Code";
   347     val reserved = fold (insert (op =) o fst) includes raw_reserved;
   348     val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
   349       module_name reserved raw_module_alias program;
   350     val reserved = make_vars reserved;
   351     fun args_num c = case Graph.get_node program c
   352      of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty
   353       | Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts
   354       | Code_Thingol.Datatypecons (_, tyco) =>
   355           let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
   356           in (length o the o AList.lookup (op =) dtcos) c end
   357       | Code_Thingol.Classparam (_, class) =>
   358           let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
   359           in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
   360     fun is_singleton c = case Graph.get_node program c
   361      of Code_Thingol.Datatypecons (_, tyco) =>
   362           let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
   363           in (null o the o AList.lookup (op =) dtcos) c end
   364       | _ => false;
   365     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
   366       reserved args_num is_singleton deresolver;
   367     fun print_module name content =
   368       (name, Pretty.chunks [
   369         str ("object " ^ name ^ " {"),
   370         str "",
   371         content,
   372         str "",
   373         str "}"
   374       ]);
   375     fun serialize_module the_module_name sca_program =
   376       let
   377         val content = Pretty.chunks2 (map_filter
   378           (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
   379             | (_, (_, NONE)) => NONE) sca_program);
   380       in print_module the_module_name content end;
   381     fun check_destination destination =
   382       (File.check destination; destination);
   383     fun write_module destination (modlname, content) =
   384       let
   385         val filename = case modlname
   386          of "" => Path.explode "Main.scala"
   387           | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
   388                 o Long_Name.explode) modlname;
   389         val pathname = Path.append destination filename;
   390         val _ = File.mkdir (Path.dir pathname);
   391       in File.write pathname (code_of_pretty content) end
   392   in
   393     Code_Target.mk_serialization target NONE
   394       (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
   395         (write_module (check_destination file)))
   396       (rpair [] o cat_lines o map (code_of_pretty o snd))
   397       (map (uncurry print_module) includes
   398         @| serialize_module the_module_name sca_program)
   399       destination
   400   end;
   401 
   402 val literals = let
   403   fun char_scala c =
   404     let
   405       val s = ML_Syntax.print_char c;
   406     in if s = "'" then "\\'" else s end;
   407   fun bigint_scala k = "(" ^ (if k <= 2147483647
   408     then string_of_int k else quote (string_of_int k)) ^ ")"
   409 in Literals {
   410   literal_char = Library.enclose "'" "'" o char_scala,
   411   literal_string = quote o translate_string char_scala,
   412   literal_numeral = fn unbounded => fn k => if k >= 0 then
   413       if unbounded then bigint_scala k
   414       else Library.enclose "(" ")" (string_of_int k)
   415     else
   416       if unbounded then "(- " ^ bigint_scala (~ k) ^ ")"
   417       else Library.enclose "(" ")" (signed_string_of_int k),
   418   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   419   infix_cons = (6, "::")
   420 } end;
   421 
   422 
   423 (** Isar setup **)
   424 
   425 fun isar_seri_scala module_name =
   426   Code_Target.parse_args (Scan.succeed ())
   427   #> (fn () => serialize_scala module_name);
   428 
   429 val setup =
   430   Code_Target.add_target (target, (isar_seri_scala, literals))
   431   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   432       brackify_infix (1, R) fxy [
   433         print_typ BR ty1 (*product type vs. tupled arguments!*),
   434         str "=>",
   435         print_typ (INFX (1, R)) ty2
   436       ]))
   437   #> fold (Code_Target.add_reserved target) [
   438       "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
   439       "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
   440       "match", "new", "null", "object", "override", "package", "private", "protected",
   441       "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
   442       "true", "type", "val", "var", "while", "with"
   443     ]
   444   #> fold (Code_Target.add_reserved target) [
   445       "error", "apply", "List", "Nil"
   446     ];
   447 
   448 end; (*struct*)