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