--- a/src/Tools/Code/code_scala.ML Tue Jun 29 22:59:29 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Wed Jun 30 11:39:10 2010 +0200
@@ -23,17 +23,26 @@
(** Scala serializer **)
fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
- args_num is_singleton deresolve =
+ args_num is_singleton_constr deresolve =
let
val deresolve_base = Long_Name.base_name o deresolve;
- val lookup_tyvar = first_upper oo lookup_var;
- fun print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
- of NONE => applify "[" "]" fxy
- ((str o deresolve) tyco) (map (print_typ tyvars NOBR) tys)
+ fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
+ fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
+ fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
+ (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
+ and print_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
+ of NONE => print_tyco_expr tyvars fxy (tyco, tys)
| SOME (i, print) => print (print_typ tyvars) fxy tys)
| print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
- fun print_typed tyvars p ty =
- Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
+ fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]);
+ fun print_tupled_typ tyvars ([], ty) =
+ print_typ tyvars NOBR ty
+ | print_tupled_typ tyvars ([ty1], ty2) =
+ concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
+ | print_tupled_typ tyvars (tys, ty) =
+ concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
+ str "=>", print_typ tyvars NOBR ty];
+ fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
fun print_var vars NONE = str "_"
| print_var vars (SOME v) = (str o lookup_var vars) v
fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
@@ -41,9 +50,8 @@
| print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
(case Code_Thingol.unfold_const_app t
of SOME app => print_app tyvars is_pat some_thm vars fxy app
- | _ => applify "(" ")" fxy
- (print_term tyvars is_pat some_thm vars BR t1)
- [print_term tyvars is_pat some_thm vars NOBR t2])
+ | _ => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy
+ (print_term tyvars is_pat some_thm vars BR t1) [t2])
| print_term tyvars is_pat some_thm vars fxy (IVar v) =
print_var vars v
| print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
@@ -51,7 +59,7 @@
val vars' = intro_vars (the_list v) vars;
in
concat [
- Pretty.block [str "(", print_typed tyvars (print_var vars' v) ty, str ")"],
+ enclose "(" ")" [constraint (print_var vars' v) (print_typ tyvars NOBR ty)],
str "=>",
print_term tyvars false some_thm vars' NOBR t
]
@@ -68,12 +76,12 @@
val k = length ts;
val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
val arg_typs' = if is_pat orelse
- (is_none (syntax_const c) andalso is_singleton c) then [] else arg_typs;
+ (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
val (no_syntax, print') = case syntax_const c
- of NONE => (true, fn ts => applify "(" ")" fxy
- (applify "[" "]" NOBR ((str o deresolve) c)
- (map (print_typ tyvars NOBR) arg_typs'))
- (map (print_term tyvars is_pat some_thm vars NOBR) ts))
+ of NONE => (true, fn ts => applify "(" ")"
+ (print_term tyvars is_pat some_thm vars NOBR) fxy
+ (applify "[" "]" (print_typ tyvars NOBR)
+ NOBR ((str o deresolve) c) arg_typs') ts)
| SOME (_, print) => (false, fn ts =>
print (print_term tyvars is_pat some_thm) some_thm vars fxy
(ts ~~ take l function_typs));
@@ -94,15 +102,14 @@
fun print_match ((pat, ty), t) vars =
vars
|> print_bind tyvars some_thm BR pat
- |>> (fn p => semicolon [Pretty.block [str "val", Pretty.brk 1, p,
- str ":", Pretty.brk 1, print_typ tyvars NOBR ty],
+ |>> (fn p => concat [str "val", constraint p (print_typ tyvars NOBR ty),
str "=", print_term tyvars false some_thm vars NOBR t])
- val (ps, vars') = fold_map print_match binds vars;
- in
- brackify_block fxy
- (str "{")
- (ps @| print_term tyvars false some_thm vars' NOBR body)
- (str "}")
+ val (all_ps, vars') = fold_map print_match binds vars;
+ val (ps, p) = split_last all_ps;
+ in brackify_block fxy
+ (str "{")
+ (ps @ Pretty.block [p, str ";"] @@ print_term tyvars false some_thm vars' NOBR body)
+ (str "}")
end
| print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
let
@@ -118,156 +125,124 @@
end
| print_case tyvars some_thm vars fxy ((_, []), _) =
(brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
- fun print_defhead tyvars vars p vs params tys implicits (*FIXME simplify*) ty =
- Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
- (applify "(" ")" NOBR
- (applify "[" "]" NOBR p (map (fn (v, sort) =>
- (str o implode)
- (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
- (map2 (fn param => fn ty => print_typed tyvars
- ((str o lookup_var vars) param) ty)
- params tys)) implicits) ty, str " ="]
- fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
- (case filter (snd o snd) raw_eqs
- of [] =>
- let
- val (tys, ty') = Code_Thingol.unfold_fun ty;
- val params = Name.invents (snd reserved) "a" (length tys);
- val tyvars = intro_vars (map fst vs) reserved;
- val vars = intro_vars params reserved;
- in
- concat [print_defhead tyvars vars ((str o deresolve) name) vs params tys [] ty',
- str ("error(\"" ^ name ^ "\")")]
- end
- | eqs =>
+ fun print_context tyvars vs name = applify "[" "]"
+ (fn (v, sort) => (Pretty.block o map str)
+ (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
+ NOBR ((str o deresolve) name) vs;
+ fun print_defhead tyvars vars name vs params tys ty =
+ Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
+ constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
+ NOBR (print_context tyvars vs name) (params ~~ tys)) (print_typ tyvars NOBR ty),
+ str " ="];
+ fun print_def name (vs, ty) [] =
+ let
+ val (tys, ty') = Code_Thingol.unfold_fun ty;
+ val params = Name.invents (snd reserved) "a" (length tys);
+ val tyvars = intro_tyvars vs reserved;
+ val vars = intro_vars params reserved;
+ in
+ concat [print_defhead tyvars vars name vs params tys ty',
+ str ("error(\"" ^ name ^ "\")")]
+ end
+ | print_def name (vs, ty) eqs =
+ let
+ val tycos = fold (fn ((ts, t), _) =>
+ fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
+ val tyvars = reserved
+ |> intro_base_names
+ (is_none o syntax_tyco) deresolve tycos
+ |> intro_tyvars vs;
+ val simple = case eqs
+ of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
+ | _ => false;
+ val consts = fold Code_Thingol.add_constnames
+ (map (snd o fst) eqs) [];
+ val vars1 = reserved
+ |> intro_base_names
+ (is_none o syntax_const) deresolve consts
+ val params = if simple
+ then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
+ else aux_params vars1 (map (fst o fst) eqs);
+ val vars2 = intro_vars params vars1;
+ val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
+ fun print_tuple [p] = p
+ | print_tuple ps = enum "," "(" ")" ps;
+ fun print_rhs vars' ((_, t), (some_thm, _)) =
+ print_term tyvars false some_thm vars' NOBR t;
+ fun print_clause (eq as ((ts, _), (some_thm, _))) =
let
- val tycos = fold (fn ((ts, t), _) =>
- fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
- val tyvars = reserved
- |> intro_base_names
- (is_none o syntax_tyco) deresolve tycos
- |> intro_vars (map fst vs);
- val simple = case eqs
- of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
- | _ => false;
- val consts = fold Code_Thingol.add_constnames
- (map (snd o fst) eqs) [];
- val vars1 = reserved
- |> intro_base_names
- (is_none o syntax_const) deresolve consts
- val params = if simple
- then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
- else aux_params vars1 (map (fst o fst) eqs);
- val vars2 = intro_vars params vars1;
- val (tys, ty1) = Code_Thingol.unfold_fun ty;
- val (tys1, tys2) = chop (length params) tys;
- val ty2 = Library.foldr
- (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
- fun print_tuple [p] = p
- | print_tuple ps = enum "," "(" ")" ps;
- fun print_rhs vars' ((_, t), (some_thm, _)) =
- print_term tyvars false some_thm vars' NOBR t;
- fun print_clause (eq as ((ts, _), (some_thm, _))) =
- let
- val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
- (insert (op =)) ts []) vars1;
- in
- concat [str "case",
- print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
- str "=>", print_rhs vars' eq]
- end;
- val head = print_defhead tyvars vars2 ((str o deresolve) name) vs params tys1 [] ty2;
- in if simple then
- concat [head, print_rhs vars2 (hd eqs)]
- else
- Pretty.block_enclose
- (concat [head, print_tuple (map (str o lookup_var vars2) params),
- str "match", str "{"], str "}")
- (map print_clause eqs)
- end)
+ val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
+ (insert (op =)) ts []) vars1;
+ in
+ concat [str "case",
+ print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
+ str "=>", print_rhs vars' eq]
+ end;
+ val head = print_defhead tyvars vars2 name vs params tys' ty';
+ in if simple then
+ concat [head, print_rhs vars2 (hd eqs)]
+ else
+ Pretty.block_enclose
+ (concat [head, print_tuple (map (str o lookup_var vars2) params),
+ str "match", str "{"], str "}")
+ (map print_clause eqs)
+ end;
+ val print_method = (str o Library.enclose "`" "+`" o deresolve_base);
+ fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
+ print_def name (vs, ty) (filter (snd o snd) raw_eqs)
| print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
let
- val tyvars = intro_vars (map fst vs) reserved;
+ val tyvars = intro_tyvars vs reserved;
fun print_co ((co, _), []) =
concat [str "final", str "case", str "object", (str o deresolve_base) co,
- str "extends", applify "[" "]" NOBR ((str o deresolve_base) name)
+ str "extends", applify "[" "]" I NOBR ((str o deresolve_base) name)
(replicate (length vs) (str "Nothing"))]
| print_co ((co, vs_args), tys) =
- let
- val fields = Name.names (snd reserved) "a" tys;
- val vars = intro_vars (map fst fields) reserved;
- fun add_typargs1 p = applify "[" "]" NOBR p
- (map (str o lookup_tyvar tyvars o fst) vs); (*FIXME*)
- fun add_typargs2 p = applify "[" "]" NOBR p
- (map (str o lookup_tyvar tyvars) vs_args); (*FIXME*)
- in
- concat [
- applify "(" ")" NOBR
- (add_typargs2 ((concat o map str)
- ["final", "case", "class", deresolve_base co]))
- (map (uncurry (print_typed tyvars) o apfst str) fields),
- str "extends",
- add_typargs1 ((str o deresolve_base) name)
- ]
- end
+ concat [applify "(" ")"
+ (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
+ (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
+ ["final", "case", "class", deresolve_base co]) vs_args)
+ (Name.names (snd reserved) "a" tys),
+ str "extends",
+ applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
+ ((str o deresolve_base) name) vs
+ ];
in
- Pretty.chunks (
- applify "[" "]" NOBR ((concat o map str)
- ["sealed", "class", deresolve_base name])
- (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs)
- :: map print_co cos
- )
+ Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
+ NOBR ((concat o map str) ["sealed", "class", deresolve_base name]) vs
+ :: map print_co cos)
end
| print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
let
- val tyvars = intro_vars [v] reserved;
- val vs = [(v, [name])];
- fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
+ val tyvars = intro_tyvars [(v, [name])] reserved;
+ fun add_typarg s = Pretty.block
+ [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
fun print_super_classes [] = NONE
| print_super_classes classes = SOME (concat (str "extends"
- :: separate (str "with")
- (map (add_typarg o str o deresolve o fst) classes)));
- fun print_tupled_typ ([], ty) =
- print_typ tyvars NOBR ty
- | print_tupled_typ ([ty1], ty2) =
- concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
- | print_tupled_typ (tys, ty) =
- concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
- str "=>", print_typ tyvars NOBR ty];
+ :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
fun print_classparam_val (classparam, ty) =
- concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base)
- classparam,
- (print_tupled_typ o Code_Thingol.unfold_fun) ty]
- fun implicit_arguments tyvars vs vars = (*FIXME simplifiy*)
- let
- val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
- [(str o deresolve) class, str "[",
- (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
- val implicit_names = Name.variant_list [] (maps (fn (v, sort) =>
- map (fn class => lookup_tyvar tyvars v ^ "_" ^
- (Long_Name.base_name o deresolve) class) sort) vs);
- val vars' = intro_vars implicit_names vars;
- val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
- implicit_names implicit_typ_ps;
- in ((implicit_names, implicit_ps), vars') end;
+ concat [str "val", constraint (print_method classparam)
+ ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
fun print_classparam_def (classparam, ty) =
let
val (tys, ty) = Code_Thingol.unfold_fun ty;
- val params = Name.invents (snd reserved) "a" (length tys);
- val vars = intro_vars params reserved;
- val (([implicit], [p_implicit]), vars') = implicit_arguments tyvars vs vars;
- val head = print_defhead tyvars vars' ((str o deresolve) classparam)
- ((map o apsnd) (K []) vs) params tys [p_implicit] ty;
+ val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
+ val proto_vars = intro_vars [implicit_name] reserved;
+ val auxs = Name.invents (snd proto_vars) "a" (length tys);
+ val vars = intro_vars auxs proto_vars;
in
- concat [head, applify "(" ")" NOBR
- (Pretty.block [str implicit, str ".",
- (str o Library.enclose "`" "+`" o deresolve_base) classparam])
- (map (str o lookup_var vars') params)]
+ concat [str "def", constraint (Pretty.block [applify "(" ")"
+ (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+ (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
+ (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
+ add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
+ applify "(" ")" (str o lookup_var vars) NOBR
+ (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
end;
in
Pretty.chunks (
(Pretty.block_enclose
- (concat ([str "trait", add_typarg ((str o deresolve_base) name)]
+ (concat ([str "trait", (add_typarg o deresolve_base) name]
@ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
(map print_classparam_val classparams))
:: map print_classparam_def classparams
@@ -276,35 +251,27 @@
| print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
(super_instances, (classparam_instances, further_classparam_instances)))) =
let
- val tyvars = intro_vars (map fst vs) reserved;
- val classtyp = (class, (tyco, map fst vs));
- fun print_classtyp' (class, (tyco, vs)) = (*FIXME already exists?*)
- applify "[" "]" NOBR(*? FIXME*) ((str o deresolve) class)
- [print_typ tyvars NOBR (tyco `%% map ITyVar vs)]; (*FIXME a mess...*)
- fun print_typed' tyvars p classtyp = (*FIXME unify with existing print_typed*)
- Pretty.block [p, str ":", Pretty.brk 1, print_classtyp' classtyp];
- fun print_defhead' tyvars vars p vs params tys classtyp = (*FIXME unify with existing def_head*)
- Pretty.block [str "def ", print_typed' tyvars
- (applify "(" ")" NOBR
- (applify "[" "]" NOBR p (map (fn (v, sort) =>
- (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
- (map2 (fn param => fn ty => print_typed tyvars ((str o lookup_var vars) param) ty)
- params tys)) classtyp, str " ="];
+ val tyvars = intro_tyvars vs reserved;
+ val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
let
- val auxs = Name.invents (snd reserved) "a" (length tys);
+ val aux_tys = Name.names (snd reserved) "a" tys;
+ val auxs = map fst aux_tys;
val vars = intro_vars auxs reserved;
- val args = if null auxs then [] else
- [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
- auxs tys), str "=>"]];
+ val aux_abstr = if null auxs then [] else [enum "," "(" ")"
+ (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+ (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
in
- concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
- str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
+ concat ([str "val", print_method classparam, str "="]
+ @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
+ (const, map (IVar o SOME) auxs))
end;
- val head = print_defhead' tyvars reserved ((str o deresolve) name) vs [] [] classtyp;
- val body = [str "new", print_classtyp' classtyp,
- Pretty.enum ";" "{ " " }" (map print_classparam_instance (classparam_instances @ further_classparam_instances))];
- in concat (str "implicit" :: head :: body) end;
+ in
+ Pretty.block_enclose (concat [str "implicit def",
+ constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
+ str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
+ (map print_classparam_instance (classparam_instances @ further_classparam_instances))
+ end;
in print_stmt end;
fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
@@ -368,25 +335,24 @@
val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
module_name reserved raw_module_alias program;
val reserved = make_vars reserved;
+ fun lookup_constr tyco constr = case Graph.get_node program tyco
+ of Code_Thingol.Datatype (_, (_, constrs)) =>
+ the (AList.lookup (op = o apsnd fst) constrs constr);
+ fun classparams_of_class class = case Graph.get_node program class
+ of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
fun args_num c = case Graph.get_node program c
of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
(length o fst o Code_Thingol.unfold_fun) ty
| Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
- | Code_Thingol.Datatypecons (_, tyco) =>
- let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
- in (length o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
+ | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
| Code_Thingol.Classparam (_, class) =>
- let
- val Code_Thingol.Class (_, (_, (_, classparams))) =
- Graph.get_node program class
- in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
- fun is_singleton c = case Graph.get_node program c
- of Code_Thingol.Datatypecons (_, tyco) =>
- let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
- in (null o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
+ (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
+ (classparams_of_class class)) c;
+ fun is_singleton_constr c = case Graph.get_node program c
+ of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
| _ => false;
val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
- reserved args_num is_singleton deresolver;
+ reserved args_num is_singleton_constr deresolver;
fun print_module name content =
(name, Pretty.chunks [
str ("object " ^ name ^ " {"),
@@ -468,7 +434,7 @@
"true", "type", "val", "var", "while", "with", "yield"
]
#> fold (Code_Target.add_reserved target) [
- "error", "apply", "List", "Nil", "BigInt"
+ "apply", "error", "BigInt", "Nil", "List"
];
end; (*struct*)