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