src/Tools/Code/code_scala.ML
changeset 48072 ace701efe203
parent 48003 1d11af40b106
child 48073 1b609a7837ef
     1.1 --- a/src/Tools/Code/code_scala.ML	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Tue Jun 05 07:05:56 2012 +0200
     1.3 @@ -46,8 +46,8 @@
     1.4      fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
     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 some_thm vars fxy (IConst c) =
     1.8 -          print_app tyvars is_pat some_thm vars fxy (c, [])
     1.9 +    fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
    1.10 +          print_app tyvars is_pat some_thm vars fxy (const, [])
    1.11        | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
    1.12            (case Code_Thingol.unfold_const_app t
    1.13             of SOME app => print_app tyvars is_pat some_thm vars fxy app
    1.14 @@ -65,30 +65,30 @@
    1.15                print_term tyvars false some_thm vars' NOBR t
    1.16              ]
    1.17            end
    1.18 -      | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
    1.19 -          (case Code_Thingol.unfold_const_app t0
    1.20 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    1.21 -                then print_case tyvars some_thm vars fxy cases
    1.22 -                else print_app tyvars is_pat some_thm vars fxy c_ts
    1.23 -            | NONE => print_case tyvars some_thm vars fxy cases)
    1.24 +      | print_term tyvars is_pat some_thm vars fxy (ICase case_expr) =
    1.25 +          (case Code_Thingol.unfold_const_app (#primitive case_expr)
    1.26 +           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    1.27 +                then print_case tyvars some_thm vars fxy case_expr
    1.28 +                else print_app tyvars is_pat some_thm vars fxy app
    1.29 +            | NONE => print_case tyvars some_thm vars fxy case_expr)
    1.30      and print_app tyvars is_pat some_thm vars fxy
    1.31 -        (app as ((c, (((tys, _), (arg_tys, _)), _)), ts)) =
    1.32 +        (app as ({ name = c, typargs, dom, ... }, ts)) =
    1.33        let
    1.34          val k = length ts;
    1.35 -        val tys' = if is_pat orelse
    1.36 -          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else tys;
    1.37 +        val typargs' = if is_pat orelse
    1.38 +          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else typargs;
    1.39          val (l, print') = case const_syntax c
    1.40           of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
    1.41                (print_term tyvars is_pat some_thm vars NOBR) fxy
    1.42                  (applify "[" "]" (print_typ tyvars NOBR)
    1.43 -                  NOBR ((str o deresolve) c) tys') ts)
    1.44 +                  NOBR ((str o deresolve) c) typargs') ts)
    1.45            | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
    1.46                (print_term tyvars is_pat some_thm vars NOBR) fxy
    1.47                  (applify "[" "]" (print_typ tyvars NOBR)
    1.48 -                  NOBR (str s) tys') ts)
    1.49 +                  NOBR (str s) typargs') ts)
    1.50            | SOME (Complex_const_syntax (k, print)) =>
    1.51                (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    1.52 -                (ts ~~ take k arg_tys))
    1.53 +                (ts ~~ take k dom))
    1.54        in if k = l then print' fxy ts
    1.55        else if k < l then
    1.56          print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    1.57 @@ -100,9 +100,11 @@
    1.58        end end
    1.59      and print_bind tyvars some_thm fxy p =
    1.60        gen_print_bind (print_term tyvars true) some_thm fxy p
    1.61 -    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    1.62 +    and print_case tyvars some_thm vars fxy { clauses = [], ... } =
    1.63 +          (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"]
    1.64 +      | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
    1.65            let
    1.66 -            val (bind :: binds, body) = Code_Thingol.unfold_let (ICase cases);
    1.67 +            val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
    1.68              fun print_match_val ((pat, ty), t) vars =
    1.69                vars
    1.70                |> print_bind tyvars some_thm BR pat
    1.71 @@ -123,7 +125,7 @@
    1.72                | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
    1.73                    (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
    1.74            in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end
    1.75 -      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
    1.76 +      | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
    1.77            let
    1.78              fun print_select (pat, body) =
    1.79                let
    1.80 @@ -135,9 +137,7 @@
    1.81              |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}")
    1.82              |> single
    1.83              |> enclose "(" ")"
    1.84 -          end
    1.85 -      | print_case tyvars some_thm vars fxy ((_, []), _) =
    1.86 -          (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
    1.87 +          end;
    1.88      fun print_context tyvars vs name = applify "[" "]"
    1.89        (fn (v, sort) => (Pretty.block o map str)
    1.90          (lookup_tyvar tyvars v :: maps (fn sort => [" : ", deresolve sort]) sort))
    1.91 @@ -261,19 +261,19 @@
    1.92                :: map print_classparam_def classparams
    1.93              )
    1.94            end
    1.95 -      | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
    1.96 -            (super_instances, (classparam_instances, further_classparam_instances)))) =
    1.97 +      | print_stmt (name, Code_Thingol.Classinst
    1.98 +          { class, tyco, vs, inst_params, superinst_params, ... }) =
    1.99            let
   1.100              val tyvars = intro_tyvars vs reserved;
   1.101              val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
   1.102 -            fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) =
   1.103 +            fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) =
   1.104                let
   1.105 -                val aux_tys = Name.invent_names (snd reserved) "a" tys;
   1.106 -                val auxs = map fst aux_tys;
   1.107 +                val aux_dom = Name.invent_names (snd reserved) "a" dom;
   1.108 +                val auxs = map fst aux_dom;
   1.109                  val vars = intro_vars auxs reserved;
   1.110                  val aux_abstr = if null auxs then [] else [enum "," "(" ")"
   1.111                    (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
   1.112 -                  (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
   1.113 +                  (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
   1.114                in
   1.115                  concat ([str "val", print_method classparam, str "="]
   1.116                    @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
   1.117 @@ -283,7 +283,7 @@
   1.118              Pretty.block_enclose (concat [str "implicit def",
   1.119                constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
   1.120                str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
   1.121 -                (map print_classparam_instance (classparam_instances @ further_classparam_instances))
   1.122 +                (map print_classparam_instance (inst_params @ superinst_params))
   1.123            end;
   1.124    in print_stmt end;
   1.125