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