src/Tools/Code/code_scala.ML
changeset 37881 096c8397c989
parent 37822 cf3588177676
child 37893 0dbbc4c5a67e
     1.1 --- a/src/Tools/Code/code_scala.ML	Mon Jul 19 11:55:43 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Mon Jul 19 11:55:44 2010 +0200
     1.3 @@ -76,17 +76,20 @@
     1.4          (app as ((c, ((arg_typs, _), function_typs)), ts)) =
     1.5        let
     1.6          val k = length ts;
     1.7 -        val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
     1.8          val arg_typs' = if is_pat orelse
     1.9            (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
    1.10 -        val (no_syntax, print') = case syntax_const c
    1.11 -         of NONE => (true, fn ts => applify "(" ")"
    1.12 +        val (l, print') = case syntax_const c
    1.13 +         of NONE => (args_num c, fn ts => applify "(" ")"
    1.14                (print_term tyvars is_pat some_thm vars NOBR) fxy
    1.15                  (applify "[" "]" (print_typ tyvars NOBR)
    1.16                    NOBR ((str o deresolve) c) arg_typs') ts)
    1.17 -          | SOME (_, print) => (false, fn ts =>
    1.18 -              print (print_term tyvars is_pat some_thm) some_thm vars fxy
    1.19 -                (ts ~~ take l function_typs));
    1.20 +          | SOME (Plain_const_syntax (k, s)) => (k, fn ts => applify "(" ")"
    1.21 +              (print_term tyvars is_pat some_thm vars NOBR) fxy
    1.22 +                (applify "[" "]" (print_typ tyvars NOBR)
    1.23 +                  NOBR (str s) arg_typs') ts)
    1.24 +          | SOME (Complex_const_syntax (k, print)) =>
    1.25 +              (k, fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    1.26 +                (ts ~~ take k function_typs))
    1.27        in if k = l then print' ts
    1.28        else if k < l then
    1.29          print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    1.30 @@ -355,20 +358,22 @@
    1.31        | _ => false;
    1.32      val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
    1.33        reserved args_num is_singleton_constr deresolver;
    1.34 -    fun print_module name content =
    1.35 -      (name, Pretty.chunks [
    1.36 -        str ("object " ^ name ^ " {"),
    1.37 -        str "",
    1.38 +    fun print_module name imports content =
    1.39 +      (name, Pretty.chunks (
    1.40 +        str ("object " ^ name ^ " {")
    1.41 +        :: (if null imports then []
    1.42 +          else str "" :: map (fn name => str ("import " ^ name ^ "._")) imports)
    1.43 +        @ [str "",
    1.44          content,
    1.45          str "",
    1.46 -        str "}"
    1.47 -      ]);
    1.48 +        str "}"]
    1.49 +      ));
    1.50      fun serialize_module the_module_name sca_program =
    1.51        let
    1.52          val content = Pretty.chunks2 (map_filter
    1.53            (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
    1.54              | (_, (_, NONE)) => NONE) sca_program);
    1.55 -      in print_module the_module_name content end;
    1.56 +      in print_module the_module_name (map fst includes) content end;
    1.57      fun check_destination destination =
    1.58        (File.check destination; destination);
    1.59      fun write_module destination (modlname, content) =
    1.60 @@ -385,7 +390,7 @@
    1.61        (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
    1.62          (write_module (check_destination file)))
    1.63        (rpair [] o cat_lines o map (code_of_pretty o snd))
    1.64 -      (map (uncurry print_module) includes
    1.65 +      (map (fn (name, content) => print_module name [] content) includes
    1.66          @| serialize_module the_module_name sca_program)
    1.67        destination
    1.68    end;
    1.69 @@ -405,7 +410,7 @@
    1.70    literal_char = Library.enclose "'" "'" o char_scala,
    1.71    literal_string = quote o translate_string char_scala,
    1.72    literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
    1.73 -  literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
    1.74 +  literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
    1.75    literal_naive_numeral = fn k => if k >= 0
    1.76      then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
    1.77    literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],