src/Tools/Code/code_scala.ML
changeset 37464 9250ad1b98e0
parent 37453 44a307746163
child 37639 5b6733e6e033
     1.1 --- a/src/Tools/Code/code_scala.ML	Fri Jun 18 15:26:04 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Fri Jun 18 15:59:51 2010 +0200
     1.3 @@ -22,7 +22,8 @@
     1.4  
     1.5  (** Scala serializer **)
     1.6  
     1.7 -fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton deresolve =
     1.8 +fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
     1.9 +    args_num is_singleton deresolve =
    1.10    let
    1.11      val deresolve_base = Long_Name.base_name o deresolve;
    1.12      val lookup_tyvar = first_upper oo lookup_var;
    1.13 @@ -61,7 +62,8 @@
    1.14                  then print_case tyvars some_thm vars fxy cases
    1.15                  else print_app tyvars is_pat some_thm vars fxy c_ts
    1.16              | NONE => print_case tyvars some_thm vars fxy cases)
    1.17 -    and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((arg_typs, _), function_typs)), ts)) =
    1.18 +    and print_app tyvars is_pat some_thm vars fxy
    1.19 +        (app as ((c, ((arg_typs, _), function_typs)), ts)) =
    1.20        let
    1.21          val k = length ts;
    1.22          val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
    1.23 @@ -69,10 +71,12 @@
    1.24            (is_none (syntax_const c) andalso is_singleton c) then [] else arg_typs;
    1.25          val (no_syntax, print') = case syntax_const c
    1.26           of NONE => (true, fn ts => applify "(" ")" fxy
    1.27 -              (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) arg_typs'))
    1.28 -                (map (print_term tyvars is_pat some_thm vars NOBR) ts))
    1.29 +              (applify "[" "]" NOBR ((str o deresolve) c)
    1.30 +                (map (print_typ tyvars NOBR) arg_typs'))
    1.31 +                  (map (print_term tyvars is_pat some_thm vars NOBR) ts))
    1.32            | SOME (_, print) => (false, fn ts =>
    1.33 -              print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l function_typs));
    1.34 +              print (print_term tyvars is_pat some_thm) some_thm vars fxy
    1.35 +                (ts ~~ take l function_typs));
    1.36        in if k = l then print' ts
    1.37        else if k < l then
    1.38          print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    1.39 @@ -82,7 +86,8 @@
    1.40          Pretty.block (print' ts1 :: map (fn t => Pretty.block
    1.41            [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
    1.42        end end
    1.43 -    and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p
    1.44 +    and print_bind tyvars some_thm fxy p =
    1.45 +      gen_print_bind (print_term tyvars true) some_thm fxy p
    1.46      and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    1.47            let
    1.48              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    1.49 @@ -103,8 +108,9 @@
    1.50            let
    1.51              fun print_select (pat, body) =
    1.52                let
    1.53 -                val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
    1.54 -              in concat [str "case", p, str "=>", print_term tyvars false some_thm vars' NOBR body] end;
    1.55 +                val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
    1.56 +                val p_body = print_term tyvars false some_thm vars' NOBR body
    1.57 +              in concat [str "case", p_pat, str "=>", p_body] end;
    1.58            in brackify_block fxy
    1.59              (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
    1.60              (map print_select clauses)
    1.61 @@ -112,25 +118,17 @@
    1.62            end
    1.63        | print_case tyvars some_thm vars fxy ((_, []), _) =
    1.64            (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
    1.65 -    fun implicit_arguments tyvars vs vars =
    1.66 -      let
    1.67 -        val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
    1.68 -          [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
    1.69 -        val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
    1.70 -          lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
    1.71 -        val vars' = intro_vars implicit_names vars;
    1.72 -        val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
    1.73 -          implicit_names implicit_typ_ps;
    1.74 -      in ((implicit_names, implicit_ps), vars') end;
    1.75      fun print_defhead tyvars vars p vs params tys implicits (*FIXME simplify*) ty =
    1.76        Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
    1.77          (applify "(" ")" NOBR
    1.78            (applify "[" "]" NOBR p (map (fn (v, sort) =>
    1.79 -              (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
    1.80 +              (str o implode)
    1.81 +                (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
    1.82              (map2 (fn param => fn ty => print_typed tyvars
    1.83                  ((str o lookup_var vars) param) ty)
    1.84                params tys)) implicits) ty, str " ="]
    1.85 -    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = (case filter (snd o snd) raw_eqs
    1.86 +    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
    1.87 +        (case filter (snd o snd) raw_eqs
    1.88           of [] =>
    1.89                let
    1.90                  val (tys, ty') = Code_Thingol.unfold_fun ty;
    1.91 @@ -157,30 +155,33 @@
    1.92                  val vars1 = reserved
    1.93                    |> intro_base_names
    1.94                         (is_none o syntax_const) deresolve consts
    1.95 -                val ((_, implicit_ps), vars2) = implicit_arguments tyvars vs vars1; (*FIXME drop*)
    1.96 -                val params = if simple then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
    1.97 -                  else aux_params vars2 (map (fst o fst) eqs);
    1.98 -                val vars3 = intro_vars params vars2;
    1.99 +                val params = if simple
   1.100 +                  then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
   1.101 +                  else aux_params vars1 (map (fst o fst) eqs);
   1.102 +                val vars2 = intro_vars params vars1;
   1.103                  val (tys, ty1) = Code_Thingol.unfold_fun ty;
   1.104                  val (tys1, tys2) = chop (length params) tys;
   1.105                  val ty2 = Library.foldr
   1.106                    (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
   1.107                  fun print_tuple [p] = p
   1.108                    | print_tuple ps = enum "," "(" ")" ps;
   1.109 -                fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t;
   1.110 +                fun print_rhs vars' ((_, t), (some_thm, _)) =
   1.111 +                  print_term tyvars false some_thm vars' NOBR t;
   1.112                  fun print_clause (eq as ((ts, _), (some_thm, _))) =
   1.113                    let
   1.114 -                    val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars2;
   1.115 +                    val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
   1.116 +                      (insert (op =)) ts []) vars1;
   1.117                    in
   1.118 -                    concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
   1.119 +                    concat [str "case",
   1.120 +                      print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
   1.121                        str "=>", print_rhs vars' eq]
   1.122                    end;
   1.123 -                val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 [] ty2;
   1.124 +                val head = print_defhead tyvars vars2 ((str o deresolve) name) vs params tys1 [] ty2;
   1.125                in if simple then
   1.126 -                concat [head, print_rhs vars3 (hd eqs)]
   1.127 +                concat [head, print_rhs vars2 (hd eqs)]
   1.128                else
   1.129                  Pretty.block_enclose
   1.130 -                  (concat [head, print_tuple (map (str o lookup_var vars3) params),
   1.131 +                  (concat [head, print_tuple (map (str o lookup_var vars2) params),
   1.132                      str "match", str "{"], str "}")
   1.133                    (map print_clause eqs)
   1.134                end)
   1.135 @@ -202,7 +203,8 @@
   1.136                    in
   1.137                      concat [
   1.138                        applify "(" ")" NOBR
   1.139 -                        (add_typargs2 ((concat o map str) ["final", "case", "class", deresolve_base co]))
   1.140 +                        (add_typargs2 ((concat o map str)
   1.141 +                          ["final", "case", "class", deresolve_base co]))
   1.142                          (map (uncurry (print_typed tyvars) o apfst str) fields),
   1.143                        str "extends",
   1.144                        add_typargs1 ((str o deresolve_base) name)
   1.145 @@ -210,7 +212,8 @@
   1.146                    end
   1.147            in
   1.148              Pretty.chunks (
   1.149 -              applify "[" "]" NOBR ((concat o map str) ["sealed", "class", deresolve_base name])
   1.150 +              applify "[" "]" NOBR ((concat o map str)
   1.151 +                  ["sealed", "class", deresolve_base name])
   1.152                  (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs)
   1.153                :: map print_co cos
   1.154              )
   1.155 @@ -222,7 +225,8 @@
   1.156              fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
   1.157              fun print_super_classes [] = NONE
   1.158                | print_super_classes classes = SOME (concat (str "extends"
   1.159 -                  :: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
   1.160 +                  :: separate (str "with")
   1.161 +                    (map (add_typarg o str o deresolve o fst) classes)));
   1.162              fun print_tupled_typ ([], ty) =
   1.163                    print_typ tyvars NOBR ty
   1.164                | print_tupled_typ ([ty1], ty2) =
   1.165 @@ -231,14 +235,17 @@
   1.166                    concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
   1.167                      str "=>", print_typ tyvars NOBR ty];
   1.168              fun print_classparam_val (classparam, ty) =
   1.169 -              concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) classparam,
   1.170 +              concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base)
   1.171 +                  classparam,
   1.172                  (print_tupled_typ o Code_Thingol.unfold_fun) ty]
   1.173              fun implicit_arguments tyvars vs vars = (*FIXME simplifiy*)
   1.174                let
   1.175                  val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
   1.176 -                  [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
   1.177 -                val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
   1.178 -                  lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
   1.179 +                  [(str o deresolve) class, str "[",
   1.180 +                    (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
   1.181 +                val implicit_names = Name.variant_list [] (maps (fn (v, sort) =>
   1.182 +                  map (fn class => lookup_tyvar tyvars v ^ "_" ^
   1.183 +                    (Long_Name.base_name o deresolve) class) sort) vs);
   1.184                  val vars' = intro_vars implicit_names vars;
   1.185                  val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
   1.186                    implicit_names implicit_typ_ps;
   1.187 @@ -253,7 +260,8 @@
   1.188                    ((map o apsnd) (K []) vs) params tys [p_implicit] ty;
   1.189                in
   1.190                  concat [head, applify "(" ")" NOBR
   1.191 -                  (Pretty.block [str implicit, str ".", (str o Library.enclose "`" "+`" o deresolve_base) classparam])
   1.192 +                  (Pretty.block [str implicit, str ".",
   1.193 +                    (str o Library.enclose "`" "+`" o deresolve_base) classparam])
   1.194                    (map (str o lookup_var vars') params)]
   1.195                end;
   1.196            in
   1.197 @@ -320,7 +328,10 @@
   1.198            let
   1.199              val (base', nsp_common') =
   1.200                mk_name_stmt (if upper then first_upper base else base) nsp_common
   1.201 -          in (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) end;
   1.202 +          in
   1.203 +            (base',
   1.204 +              ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
   1.205 +          end;
   1.206          val add_name = case stmt
   1.207           of Code_Thingol.Fun _ => add_object
   1.208            | Code_Thingol.Datatype _ => add_class
   1.209 @@ -348,7 +359,8 @@
   1.210  
   1.211  fun serialize_scala raw_module_name labelled_name
   1.212      raw_reserved includes raw_module_alias
   1.213 -    _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
   1.214 +    _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
   1.215 +    program stmt_names destination =
   1.216    let
   1.217      val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
   1.218      val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
   1.219 @@ -357,13 +369,16 @@
   1.220        module_name reserved raw_module_alias program;
   1.221      val reserved = make_vars reserved;
   1.222      fun args_num c = case Graph.get_node program c
   1.223 -     of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty
   1.224 +     of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
   1.225 +          (length o fst o Code_Thingol.unfold_fun) ty
   1.226        | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
   1.227        | Code_Thingol.Datatypecons (_, tyco) =>
   1.228            let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
   1.229            in (length o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
   1.230        | Code_Thingol.Classparam (_, class) =>
   1.231 -          let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
   1.232 +          let
   1.233 +            val Code_Thingol.Class (_, (_, (_, classparams))) =
   1.234 +              Graph.get_node program class
   1.235            in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
   1.236      fun is_singleton c = case Graph.get_node program c
   1.237       of Code_Thingol.Datatypecons (_, tyco) =>
   1.238 @@ -438,12 +453,13 @@
   1.239  
   1.240  val setup =
   1.241    Code_Target.add_target (target, (isar_seri_scala, literals))
   1.242 -  #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   1.243 -      brackify_infix (1, R) fxy (
   1.244 -        print_typ BR ty1 (*product type vs. tupled arguments!*),
   1.245 -        str "=>",
   1.246 -        print_typ (INFX (1, R)) ty2
   1.247 -      )))
   1.248 +  #> Code_Target.add_syntax_tyco target "fun"
   1.249 +     (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   1.250 +        brackify_infix (1, R) fxy (
   1.251 +          print_typ BR ty1 (*product type vs. tupled arguments!*),
   1.252 +          str "=>",
   1.253 +          print_typ (INFX (1, R)) ty2
   1.254 +        )))
   1.255    #> fold (Code_Target.add_reserved target) [
   1.256        "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
   1.257        "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",