src/Pure/display.ML
author wenzelm
Sun Sep 17 22:23:48 2000 +0200 (2000-09-17)
changeset 10010 f6ccb6df9cb9
parent 9500 e21a76142269
child 10737 c130eb1e863f
permissions -rw-r--r--
added print_thm(s)_sg;
     1 (*  Title:      Pure/display.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Printing of theories, theorems, etc.
     7 *)
     8 
     9 signature DISPLAY =
    10 sig
    11   val show_hyps		: bool ref
    12   val show_tags		: bool ref
    13   val pretty_thm_no_quote: thm -> Pretty.T
    14   val pretty_thm	: thm -> Pretty.T
    15   val pretty_thms	: thm list -> Pretty.T
    16   val pretty_thm_sg     : Sign.sg -> thm -> Pretty.T
    17   val pretty_thms_sg    : Sign.sg -> thm list -> Pretty.T
    18   val string_of_thm	: thm -> string
    19   val pprint_thm	: thm -> pprint_args -> unit
    20   val print_thm		: thm -> unit
    21   val print_thms	: thm list -> unit
    22   val prth		: thm -> thm
    23   val prthq		: thm Seq.seq -> thm Seq.seq
    24   val prths		: thm list -> thm list
    25   val pretty_ctyp	: ctyp -> Pretty.T
    26   val pprint_ctyp	: ctyp -> pprint_args -> unit
    27   val string_of_ctyp	: ctyp -> string
    28   val print_ctyp	: ctyp -> unit
    29   val pretty_cterm	: cterm -> Pretty.T
    30   val pprint_cterm	: cterm -> pprint_args -> unit
    31   val string_of_cterm	: cterm -> string
    32   val print_cterm	: cterm -> unit
    33   val pretty_theory	: theory -> Pretty.T
    34   val pprint_theory	: theory -> pprint_args -> unit
    35   val print_syntax	: theory -> unit
    36   val pretty_full_theory: theory -> Pretty.T list
    37   val pretty_name_space : string * NameSpace.T -> Pretty.T
    38   val show_consts	: bool ref
    39 end;
    40 
    41 structure Display: DISPLAY =
    42 struct
    43 
    44 (** print thm **)
    45 
    46 val show_hyps = ref true;	(*false: print meta-hypotheses as dots*)
    47 val show_tags = ref false;	(*false: suppress tags*)
    48 
    49 local
    50 
    51 fun pretty_tag (name, args) = Pretty.strs (name :: map quote args);
    52 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    53 
    54 fun pretty_thm_aux quote th =
    55   let
    56     val {sign, hyps, prop, der = (ora, _), ...} = rep_thm th;
    57     val xshyps = Thm.extra_shyps th;
    58     val (_, tags) = Thm.get_name_tags th;
    59 
    60     val prt_term = (if quote then Pretty.quote else I) o Sign.pretty_term sign;
    61 
    62     val hlen = length xshyps + length hyps;
    63     val hsymbs =
    64       if hlen = 0 andalso not ora then []
    65       else if ! show_hyps then
    66         [Pretty.brk 2, Pretty.list "[" "]"
    67           (map prt_term hyps @ map (Sign.pretty_sort sign) xshyps @
    68             (if ora then [Pretty.str "!"] else []))]
    69       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    70         (if ora then "!" else "") ^ "]")];
    71     val tsymbs =
    72       if null tags orelse not (! show_tags) then []
    73       else [Pretty.brk 1, pretty_tags tags];
    74   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    75 
    76 in
    77 
    78 val pretty_thm = pretty_thm_aux true;
    79 val pretty_thm_no_quote = pretty_thm_aux false;
    80 
    81 end;
    82 
    83 
    84 val string_of_thm = Pretty.string_of o pretty_thm;
    85 val pprint_thm = Pretty.pprint o pretty_thm;
    86 
    87 fun pretty_thms [th] = pretty_thm th
    88   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    89 
    90 val pretty_thm_sg = pretty_thm oo Thm.transfer_sg;
    91 val pretty_thms_sg = pretty_thms oo (map o Thm.transfer_sg);
    92 
    93 
    94 (* top-level commands for printing theorems *)
    95 
    96 val print_thm = Pretty.writeln o pretty_thm;
    97 val print_thms = Pretty.writeln o pretty_thms;
    98 
    99 fun prth th = (print_thm th; th);
   100 
   101 (*Print and return a sequence of theorems, separated by blank lines. *)
   102 fun prthq thseq =
   103   (Seq.print (fn _ => print_thm) 100000 thseq; thseq);
   104 
   105 (*Print and return a list of theorems, separated by blank lines. *)
   106 fun prths ths = (seq (fn th => (print_thm th; writeln "")) ths; ths);
   107 
   108 
   109 (* other printing commands *)
   110 
   111 fun pretty_ctyp cT =
   112   let val {sign, T} = rep_ctyp cT in Sign.pretty_typ sign T end;
   113 
   114 fun pprint_ctyp cT =
   115   let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end;
   116 
   117 fun string_of_ctyp cT =
   118   let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end;
   119 
   120 val print_ctyp = writeln o string_of_ctyp;
   121 
   122 fun pretty_cterm ct =
   123   let val {sign, t, ...} = rep_cterm ct in Sign.pretty_term sign t end;
   124 
   125 fun pprint_cterm ct =
   126   let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end;
   127 
   128 fun string_of_cterm ct =
   129   let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end;
   130 
   131 val print_cterm = writeln o string_of_cterm;
   132 
   133 
   134 
   135 (** print theory **)
   136 
   137 val pretty_theory = Sign.pretty_sg o Theory.sign_of;
   138 val pprint_theory = Sign.pprint_sg o Theory.sign_of;
   139 
   140 val print_syntax = Syntax.print_syntax o Theory.syn_of;
   141 
   142 
   143 (* pretty_name_space  *)
   144 
   145 fun pretty_name_space (kind, space) =
   146   let
   147     fun prt_entry (name, accs) = Pretty.block
   148       (Pretty.str (quote name ^ " =") :: Pretty.brk 1 ::
   149         Pretty.commas (map (Pretty.str o quote) accs));
   150   in
   151     Pretty.fbreaks (Pretty.str (kind ^ ":") :: map prt_entry (NameSpace.dest space))
   152     |> Pretty.block
   153   end;
   154 
   155 
   156 
   157 (* print theory *)
   158 
   159 fun pretty_full_theory thy =
   160   let
   161     val sg = Theory.sign_of thy;
   162 
   163     fun prt_cls c = Sign.pretty_sort sg [c];
   164     fun prt_sort S = Sign.pretty_sort sg S;
   165     fun prt_arity t (c, Ss) = Sign.pretty_arity sg (t, Ss, [c]);
   166     fun prt_typ ty = Pretty.quote (Sign.pretty_typ sg ty);
   167     fun prt_term t = Pretty.quote (Sign.pretty_term sg t);
   168 
   169     fun pretty_classes cs = Pretty.block
   170       (Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs));
   171 
   172     fun pretty_classrel (c, cs) = Pretty.block
   173       (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 ::
   174         Pretty.commas (map prt_cls cs));
   175 
   176     fun pretty_default S = Pretty.block
   177       [Pretty.str "default:", Pretty.brk 1, prt_sort S];
   178 
   179     fun pretty_ty (t, n) = Pretty.block
   180       [Pretty.str t, Pretty.brk 1, Pretty.str (string_of_int n)];
   181 
   182     fun pretty_log_types ts = Pretty.block
   183       (Pretty.breaks (Pretty.str "logical types:" :: map Pretty.str ts));
   184 
   185     fun pretty_witness None = Pretty.str "universal non-emptiness witness: --"
   186       | pretty_witness (Some (T, S)) = Pretty.block
   187           [Pretty.str "universal non-emptiness witness:", Pretty.brk 1, prt_typ T,
   188             Pretty.brk 1, prt_sort S];
   189 
   190     fun pretty_abbr (t, (vs, rhs)) = Pretty.block
   191       [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
   192         Pretty.str " =", Pretty.brk 1, prt_typ rhs];
   193 
   194     fun pretty_arities (t, ars) = map (prt_arity t) ars;
   195 
   196     fun pretty_const (c, ty) = Pretty.block
   197       [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
   198 
   199     fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
   200 
   201 
   202     val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
   203     val {axioms, oracles, ...} = Theory.rep_theory thy;
   204     val spaces' = Library.sort_wrt fst spaces;
   205     val {classes, classrel, default, tycons = type_tab, log_types, univ_witness, abbrs, arities} =
   206       Type.rep_tsig tsig;
   207     val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
   208     val consts = Sign.cond_extern_table sg Sign.constK const_tab;
   209     val axms = Sign.cond_extern_table sg Theory.axiomK axioms;
   210     val oras = Sign.cond_extern_table sg Theory.oracleK oracles;
   211   in
   212     [Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
   213       Pretty.strs ("data:" :: Sign.data_kinds data),
   214       Pretty.strs ["name prefix:", NameSpace.pack path],
   215       Pretty.big_list "name spaces:" (map pretty_name_space spaces'),
   216       pretty_classes classes,
   217       Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)),
   218       pretty_default default,
   219       pretty_log_types log_types,
   220       pretty_witness univ_witness,
   221       Pretty.big_list "type constructors:" (map pretty_ty tycons),
   222       Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)),
   223       Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))),
   224       Pretty.big_list "consts:" (map pretty_const consts),
   225       Pretty.big_list "axioms:" (map prt_axm axms),
   226       Pretty.strs ("oracles:" :: (map #1 oras))]
   227   end;
   228 
   229 
   230 (*show consts with types in proof state output?*)
   231 val show_consts = ref false;
   232 
   233 
   234 end;
   235 
   236 open Display;