src/Tools/Code/code_ml.ML
changeset 41100 6c0940392fb4
parent 40627 becf5d5187cc
child 41118 b290841cd3b0
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Dec 09 09:58:33 2010 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Dec 09 17:25:43 2010 +0100
     1.3 @@ -76,23 +76,20 @@
     1.4          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     1.5      fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     1.6      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
     1.7 -    fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
     1.8 -          brackify fxy ((str o deresolve) inst ::
     1.9 +    fun print_classrels fxy [] ps = brackify fxy ps
    1.10 +      | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
    1.11 +      | print_classrels fxy classrels ps =
    1.12 +          brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
    1.13 +    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
    1.14 +          print_classrels fxy classrels ((str o deresolve) inst ::
    1.15              (if is_pseudo_fun inst then [str "()"]
    1.16              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.17 -      | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
    1.18 -          let
    1.19 -            val v_p = str (if k = 1 then first_upper v ^ "_"
    1.20 -              else first_upper v ^ string_of_int (i+1) ^ "_");
    1.21 -          in case classrels
    1.22 -           of [] => v_p
    1.23 -            | [classrel] => brackets [(str o deresolve) classrel, v_p]
    1.24 -            | classrels => brackets
    1.25 -                [enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
    1.26 -          end
    1.27 +      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
    1.28 +          print_classrels fxy classrels [str (if k = 1 then first_upper v ^ "_"
    1.29 +            else first_upper v ^ string_of_int (i+1) ^ "_")]
    1.30      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.31      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.32 -      (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    1.33 +      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
    1.34      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.35            print_app is_pseudo_fun some_thm vars fxy (c, [])
    1.36        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    1.37 @@ -218,11 +215,11 @@
    1.38        | print_def is_pseudo_fun _ definer
    1.39            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
    1.40            let
    1.41 -            fun print_super_instance (_, (classrel, dss)) =
    1.42 +            fun print_super_instance (_, (classrel, x)) =
    1.43                concat [
    1.44                  (str o Long_Name.base_name o deresolve) classrel,
    1.45                  str "=",
    1.46 -                print_dict is_pseudo_fun NOBR (DictConst dss)
    1.47 +                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
    1.48                ];
    1.49              fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.50                concat [
    1.51 @@ -381,18 +378,20 @@
    1.52          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    1.53      fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
    1.54      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    1.55 -    fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
    1.56 -          brackify fxy ((str o deresolve) inst ::
    1.57 +    val print_classrels =
    1.58 +      fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
    1.59 +    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
    1.60 +          brackify BR ((str o deresolve) inst ::
    1.61              (if is_pseudo_fun inst then [str "()"]
    1.62              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.63 -      | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
    1.64 +          |> print_classrels classrels
    1.65 +      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
    1.66            str (if k = 1 then "_" ^ first_upper v
    1.67              else "_" ^ first_upper v ^ string_of_int (i+1))
    1.68 -          |> fold_rev (fn classrel => fn p =>
    1.69 -               Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
    1.70 +          |> print_classrels classrels
    1.71      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.72      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.73 -      (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    1.74 +      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
    1.75      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.76            print_app is_pseudo_fun some_thm vars fxy (c, [])
    1.77        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    1.78 @@ -553,11 +552,11 @@
    1.79        | print_def is_pseudo_fun _ definer
    1.80              (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
    1.81            let
    1.82 -            fun print_super_instance (_, (classrel, dss)) =
    1.83 +            fun print_super_instance (_, (classrel, x)) =
    1.84                concat [
    1.85                  (str o deresolve) classrel,
    1.86                  str "=",
    1.87 -                print_dict is_pseudo_fun NOBR (DictConst dss)
    1.88 +                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
    1.89                ];
    1.90              fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.91                concat [