1.1 --- a/src/Tools/Code/code_scala.ML Fri Feb 19 11:06:22 2010 +0100
1.2 +++ b/src/Tools/Code/code_scala.ML Fri Feb 19 11:06:22 2010 +0100
1.3 @@ -34,33 +34,33 @@
1.4 Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
1.5 fun print_var vars NONE = str "_"
1.6 | print_var vars (SOME v) = (str o lookup_var vars) v
1.7 - fun print_term tyvars is_pat thm vars fxy (IConst c) =
1.8 - print_app tyvars is_pat thm vars fxy (c, [])
1.9 - | print_term tyvars is_pat thm vars fxy (t as (t1 `$ t2)) =
1.10 + fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
1.11 + print_app tyvars is_pat some_thm vars fxy (c, [])
1.12 + | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
1.13 (case Code_Thingol.unfold_const_app t
1.14 - of SOME app => print_app tyvars is_pat thm vars fxy app
1.15 + of SOME app => print_app tyvars is_pat some_thm vars fxy app
1.16 | _ => applify "(" ")" fxy
1.17 - (print_term tyvars is_pat thm vars BR t1)
1.18 - [print_term tyvars is_pat thm vars NOBR t2])
1.19 - | print_term tyvars is_pat thm vars fxy (IVar v) =
1.20 + (print_term tyvars is_pat some_thm vars BR t1)
1.21 + [print_term tyvars is_pat some_thm vars NOBR t2])
1.22 + | print_term tyvars is_pat some_thm vars fxy (IVar v) =
1.23 print_var vars v
1.24 - | print_term tyvars is_pat thm vars fxy ((v, ty) `|=> t) =
1.25 + | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
1.26 let
1.27 val vars' = intro_vars (the_list v) vars;
1.28 in
1.29 concat [
1.30 Pretty.block [str "(", print_typed tyvars (print_var vars' v) ty, str ")"],
1.31 str "=>",
1.32 - print_term tyvars false thm vars' NOBR t
1.33 + print_term tyvars false some_thm vars' NOBR t
1.34 ]
1.35 end
1.36 - | print_term tyvars is_pat thm vars fxy (ICase (cases as (_, t0))) =
1.37 + | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
1.38 (case Code_Thingol.unfold_const_app t0
1.39 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
1.40 - then print_case tyvars thm vars fxy cases
1.41 - else print_app tyvars is_pat thm vars fxy c_ts
1.42 - | NONE => print_case tyvars thm vars fxy cases)
1.43 - and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
1.44 + then print_case tyvars some_thm vars fxy cases
1.45 + else print_app tyvars is_pat some_thm vars fxy c_ts
1.46 + | NONE => print_case tyvars some_thm vars fxy cases)
1.47 + and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
1.48 let
1.49 val k = length ts;
1.50 val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
1.51 @@ -69,47 +69,47 @@
1.52 val (no_syntax, print') = case syntax_const c
1.53 of NONE => (true, fn ts => applify "(" ")" fxy
1.54 (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
1.55 - (map (print_term tyvars is_pat thm vars NOBR) ts))
1.56 + (map (print_term tyvars is_pat some_thm vars NOBR) ts))
1.57 | SOME (_, print) => (false, fn ts =>
1.58 - print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take l tys_args));
1.59 + print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l tys_args));
1.60 in if k = l then print' ts
1.61 else if k < l then
1.62 - print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
1.63 + print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
1.64 else let
1.65 val (ts1, ts23) = chop l ts;
1.66 in
1.67 Pretty.block (print' ts1 :: map (fn t => Pretty.block
1.68 - [str ".apply(", print_term tyvars is_pat thm vars NOBR t, str ")"]) ts23)
1.69 + [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
1.70 end end
1.71 - and print_bind tyvars thm fxy p = gen_print_bind (print_term tyvars true) thm fxy p
1.72 - and print_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
1.73 + and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p
1.74 + and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
1.75 let
1.76 val (binds, body) = Code_Thingol.unfold_let (ICase cases);
1.77 fun print_match ((pat, ty), t) vars =
1.78 vars
1.79 - |> print_bind tyvars thm BR pat
1.80 + |> print_bind tyvars some_thm BR pat
1.81 |>> (fn p => semicolon [Pretty.block [str "val", Pretty.brk 1, p,
1.82 str ":", Pretty.brk 1, print_typ tyvars NOBR ty],
1.83 - str "=", print_term tyvars false thm vars NOBR t])
1.84 + str "=", print_term tyvars false some_thm vars NOBR t])
1.85 val (ps, vars') = fold_map print_match binds vars;
1.86 in
1.87 brackify_block fxy
1.88 (str "{")
1.89 - (ps @| print_term tyvars false thm vars' NOBR body)
1.90 + (ps @| print_term tyvars false some_thm vars' NOBR body)
1.91 (str "}")
1.92 end
1.93 - | print_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
1.94 + | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
1.95 let
1.96 fun print_select (pat, body) =
1.97 let
1.98 - val (p, vars') = print_bind tyvars thm NOBR pat vars;
1.99 - in concat [str "case", p, str "=>", print_term tyvars false thm vars' NOBR body] end;
1.100 + val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
1.101 + in concat [str "case", p, str "=>", print_term tyvars false some_thm vars' NOBR body] end;
1.102 in brackify_block fxy
1.103 - (concat [print_term tyvars false thm vars NOBR t, str "match", str "{"])
1.104 + (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
1.105 (map print_select clauses)
1.106 (str "}")
1.107 end
1.108 - | print_case tyvars thm vars fxy ((_, []), _) =
1.109 + | print_case tyvars some_thm vars fxy ((_, []), _) =
1.110 (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
1.111 fun implicit_arguments tyvars vs vars =
1.112 let
1.113 @@ -140,7 +140,7 @@
1.114 end
1.115 | eqs =>
1.116 let
1.117 - val tycos = fold (fn ((ts, t), (thm, _)) =>
1.118 + val tycos = fold (fn ((ts, t), _) =>
1.119 fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
1.120 val tyvars = reserved
1.121 |> intro_base_names
1.122 @@ -164,12 +164,12 @@
1.123 (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
1.124 fun print_tuple [p] = p
1.125 | print_tuple ps = enum "," "(" ")" ps;
1.126 - fun print_rhs vars' ((_, t), (thm, _)) = print_term tyvars false thm vars' NOBR t;
1.127 - fun print_clause (eq as ((ts, _), (thm, _))) =
1.128 + fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t;
1.129 + fun print_clause (eq as ((ts, _), (some_thm, _))) =
1.130 let
1.131 val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars2;
1.132 in
1.133 - concat [str "case", print_tuple (map (print_term tyvars true thm vars' NOBR) ts),
1.134 + concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
1.135 str "=>", print_rhs vars' eq]
1.136 end;
1.137 val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 implicit_ps ty2;
1.138 @@ -267,7 +267,7 @@
1.139 auxs tys), str "=>"]];
1.140 in
1.141 concat ([str "val", (str o suffix "$" o deresolve_base) classparam,
1.142 - str "="] @ args @ [print_app tyvars false thm vars NOBR (const, map (IVar o SOME) auxs)])
1.143 + str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
1.144 end;
1.145 in
1.146 Pretty.chunks [
1.147 @@ -352,15 +352,15 @@
1.148 of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty
1.149 | Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts
1.150 | Code_Thingol.Datatypecons (_, tyco) =>
1.151 - let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
1.152 - in (length o the o AList.lookup (op =) dtcos) c end
1.153 + let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
1.154 + in (length o the o AList.lookup (op =) constrs) c end
1.155 | Code_Thingol.Classparam (_, class) =>
1.156 let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
1.157 in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
1.158 fun is_singleton c = case Graph.get_node program c
1.159 of Code_Thingol.Datatypecons (_, tyco) =>
1.160 - let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
1.161 - in (null o the o AList.lookup (op =) dtcos) c end
1.162 + let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
1.163 + in (null o the o AList.lookup (op =) constrs) c end
1.164 | _ => false;
1.165 val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
1.166 reserved args_num is_singleton deresolver;