improved print_theory;
authorwenzelm
Tue Jun 22 09:52:08 2004 +0200 (2004-06-22)
changeset 149962571227f3fcc
parent 14995 318e58f49e8d
child 14997 aa2aaab41566
improved print_theory;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Tue Jun 22 09:51:59 2004 +0200
     1.2 +++ b/src/Pure/display.ML	Tue Jun 22 09:52:08 2004 +0200
     1.3 @@ -181,7 +181,8 @@
     1.4      fun prt_cls c = Sign.pretty_sort sg [c];
     1.5      fun prt_sort S = Sign.pretty_sort sg S;
     1.6      fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]);
     1.7 -    fun prt_typ_no_tvars ty = Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)));
     1.8 +    fun prt_typ ty = Pretty.quote (Sign.pretty_typ sg ty);
     1.9 +    val prt_typ_no_tvars = prt_typ o #1 o Type.freeze_thaw_type;
    1.10      fun prt_term t = Pretty.quote (Sign.pretty_term sg t);
    1.11  
    1.12      fun pretty_classrel (c, []) = prt_cls c
    1.13 @@ -192,61 +193,62 @@
    1.14      fun pretty_default S = Pretty.block
    1.15        [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
    1.16  
    1.17 -    fun pretty_ty (t, n) = Pretty.block
    1.18 -      [Pretty.str t, Pretty.brk 1, Pretty.str (string_of_int n)];
    1.19 -
    1.20 -    fun pretty_witness None = Pretty.str "universal non-emptiness witness: --"
    1.21 +    fun pretty_witness None = Pretty.str "universal non-emptiness witness: -"
    1.22        | pretty_witness (Some (T, S)) = Pretty.block
    1.23            [Pretty.str "universal non-emptiness witness:", Pretty.brk 1,
    1.24              prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S];
    1.25  
    1.26 -    fun pretty_nonterminals ts = Pretty.block
    1.27 -      (Pretty.breaks (Pretty.str "syntactic types:" :: map Pretty.str ts));
    1.28 -
    1.29 -    fun pretty_abbr (t, (vs, rhs, _)) = Pretty.block
    1.30 -      [prt_typ_no_tvars (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
    1.31 -        Pretty.str " =", Pretty.brk 1, prt_typ_no_tvars rhs];
    1.32 +    val tfrees = map (fn v => TFree (v, []));
    1.33 +    fun pretty_type syn ((_, t), (Type.LogicalType n, _)) =
    1.34 +          if syn then None
    1.35 +          else Some (prt_typ (Type (t, tfrees (Term.invent_names [] "'a" n))))
    1.36 +      | pretty_type syn ((_, t), (Type.Abbreviation (vs, U, syn'), _)) =
    1.37 +          if syn <> syn' then None
    1.38 +          else Some (Pretty.block
    1.39 +            [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
    1.40 +      | pretty_type syn ((_, t), (Type.Nonterminal, _)) =
    1.41 +          if not syn then None
    1.42 +          else Some (prt_typ (Type (t, [])));
    1.43  
    1.44 -    fun pretty_arities (t, ars) = map (prt_arity t) ars;
    1.45 -
    1.46 -    fun pretty_final (c:string, tys:typ list) = Pretty.block
    1.47 -      ([Pretty.str c, Pretty.str " ::", Pretty.brk 1] @
    1.48 -         (if null tys then [Pretty.str "<all instances>"]
    1.49 -	  else Pretty.commas (map prt_typ_no_tvars tys)));
    1.50 +    val pretty_arities = flat o map (fn (t, ars) => map (prt_arity t) ars);
    1.51  
    1.52      fun pretty_const (c, (ty, _)) = Pretty.block
    1.53        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.54  
    1.55 +    fun pretty_final (c, []) = Pretty.str c
    1.56 +      | pretty_final (c, tys) = Pretty.block
    1.57 +          (Pretty.str c :: Pretty.str " ::" :: Pretty.brk 1 ::
    1.58 +             Pretty.commas (map prt_typ_no_tvars tys));
    1.59 +
    1.60      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    1.61  
    1.62  
    1.63 +    val {sign = _, const_deps = _, final_consts, axioms, oracles,
    1.64 +      parents = _, ancestors = _} = Theory.rep_theory thy;
    1.65      val {self = _, tsig, consts, path, spaces, data} = Sign.rep_sg sg;
    1.66 -    val {axioms, oracles, ...} = Theory.rep_theory thy;
    1.67 -    val spaces' = Library.sort_wrt fst spaces;
    1.68      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    1.69 -    val tdecls = Symtab.dest types |>
    1.70 -      map (fn (t, (decl, _)) => (Sign.cond_extern sg Sign.typeK t, decl));
    1.71 -    val tycons = mapfilter (fn (t, Type.LogicalType n) => Some (t, n) | _ => None) tdecls;
    1.72 -    val abbrs = mapfilter (fn (t, Type.Abbreviation u) => Some (t, u) | _ => None) tdecls;
    1.73 -    val nonterminals = mapfilter (fn (t, Type.Nonterminal) => Some t | _ => None) tdecls;
    1.74 -    val finals = Symtab.dest (#final_consts (Theory.rep_theory thy));
    1.75 +
    1.76 +    val spcs = Library.sort_wrt #1 spaces;
    1.77 +    val tdecls =
    1.78 +      map (apfst (fn t => (Sign.cond_extern sg Sign.typeK t, t))) (Symtab.dest types)
    1.79 +      |> Library.sort_wrt (#1 o #1);
    1.80      val cnsts = Sign.cond_extern_table sg Sign.constK consts;
    1.81 +    val finals = Sign.cond_extern_table sg Sign.constK final_consts;
    1.82      val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
    1.83      val oras = Sign.cond_extern_table sg Theory.oracleK oracles;
    1.84    in
    1.85      [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
    1.86        Pretty.strs ("data:" :: Sign.data_kinds data),
    1.87        Pretty.strs ["name prefix:", NameSpace.pack (if_none path ["-"])],
    1.88 -      Pretty.big_list "name spaces:" (map pretty_name_space spaces'),
    1.89 +      Pretty.big_list "name spaces:" (map pretty_name_space spcs),
    1.90        Pretty.big_list "classes:" (map pretty_classrel (Graph.dest classes)),
    1.91        pretty_default default,
    1.92        pretty_witness witness,
    1.93 -      Pretty.big_list "logical type constructors:" (map pretty_ty tycons),
    1.94 -      Pretty.big_list "type abbreviations:" (map pretty_abbr abbrs),
    1.95 -      pretty_nonterminals nonterminals,
    1.96 -      Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))),
    1.97 +      Pretty.big_list "syntactic types:" (mapfilter (pretty_type true) tdecls),
    1.98 +      Pretty.big_list "logical types:" (mapfilter (pretty_type false) tdecls),
    1.99 +      Pretty.big_list "type arities:" (pretty_arities (Symtab.dest arities)),
   1.100        Pretty.big_list "consts:" (map pretty_const cnsts),
   1.101 -      Pretty.big_list "finals:" (map pretty_final finals),
   1.102 +      Pretty.big_list "finals consts:" (map pretty_final finals),
   1.103        Pretty.big_list "axioms:" (map prt_axm axms),
   1.104        Pretty.strs ("oracles:" :: (map #1 oras))]
   1.105    end;