src/Tools/Code/code_scala.ML
changeset 35228 ac2cab4583f4
parent 34944 970e1466028d
child 36535 0195ef994077
     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;