src/Pure/display.ML
changeset 19698 f48cfaacd92c
parent 19642 ea7162f84677
child 19702 2ab12e94156f
     1.1 --- a/src/Pure/display.ML	Mon May 22 22:29:15 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Mon May 22 22:29:16 2006 +0200
     1.3 @@ -172,6 +172,8 @@
     1.4      val prt_typ_no_tvars = prt_typ o Type.freeze_type;
     1.5      fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
     1.6      val prt_term_no_vars = prt_term o Logic.unvarify;
     1.7 +    fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
     1.8 +    val prt_const' = Defs.pretty_const (Sign.pp thy);
     1.9  
    1.10      fun pretty_classrel (c, []) = prt_cls c
    1.11        | pretty_classrel (c, cs) = Pretty.block
    1.12 @@ -200,20 +202,24 @@
    1.13  
    1.14      val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
    1.15  
    1.16 -    fun pretty_const (c, ty) = Pretty.block
    1.17 -      [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.18 +    fun pretty_abbrev (c, (ty, t)) = Pretty.block
    1.19 +      (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
    1.20 +
    1.21 +    fun pretty_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t];
    1.22  
    1.23 -    fun pretty_abbrev (c, (ty, t)) = Pretty.block
    1.24 -      [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty,
    1.25 -        Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t];
    1.26 +    fun pretty_reduct (lhs, rhs) = Pretty.block
    1.27 +      ([prt_const' lhs, Pretty.str "  ->", Pretty.brk 2] @ Pretty.commas (map prt_const' rhs));
    1.28  
    1.29 -    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t];
    1.30 +    fun pretty_restrict (const, name) =
    1.31 +      Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
    1.32  
    1.33 -    val {axioms, defs = _, oracles} = Theory.rep_theory thy;
    1.34 +    val {axioms, defs, oracles} = Theory.rep_theory thy;
    1.35 +    val {restricts, reducts} = Defs.dest defs;
    1.36      val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
    1.37      val {constants, constraints} = Consts.dest consts;
    1.38 -    val {classes = (class_space, class_algebra),
    1.39 -      default, types, log_types = _, witness} = Type.rep_tsig tsig;
    1.40 +    val extern_const = NameSpace.extern (#1 constants);
    1.41 +    val {classes, default, types, witness, ...} = Type.rep_tsig tsig;
    1.42 +    val (class_space, class_algebra) = classes;
    1.43      val {classes, arities} = Sorts.rep_algebra class_algebra;
    1.44  
    1.45      val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
    1.46 @@ -225,6 +231,11 @@
    1.47      val cnstrs = NameSpace.extern_table constraints;
    1.48      val axms = NameSpace.extern_table axioms;
    1.49      val oras = NameSpace.extern_table oracles;
    1.50 +
    1.51 +    val reds = reducts |> map_filter (fn (lhs, rhs) =>
    1.52 +      if null rhs then NONE
    1.53 +      else SOME (apfst extern_const lhs, map (apfst extern_const) rhs)) |> sort_wrt (#1 o #1);
    1.54 +    val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
    1.55    in
    1.56      [Pretty.strs ("names:" :: Context.names_of thy),
    1.57        Pretty.strs ("theory data:" :: Context.theory_data_of thy),
    1.58 @@ -236,10 +247,13 @@
    1.59        Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
    1.60        Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
    1.61        Pretty.big_list "type arities:" (pretty_arities arties),
    1.62 -      Pretty.big_list "logical consts:" (map pretty_const log_cnsts),
    1.63 +      Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
    1.64        Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
    1.65 -      Pretty.big_list "constraints:" (map pretty_const cnstrs),
    1.66 -      Pretty.big_list "axioms:" (map prt_axm axms),
    1.67 +      Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
    1.68 +      Pretty.big_list "axioms:" (map pretty_axm axms),
    1.69 +      Pretty.big_list "definitions:"
    1.70 +        [Pretty.big_list "open dependencies:" (map pretty_reduct reds),
    1.71 +         Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)],
    1.72        Pretty.strs ("oracles:" :: (map #1 oras))]
    1.73    end;
    1.74