Printing & string functions moved to display.ML
authorpaulson
Thu Mar 21 11:05:34 1996 +0100 (1996-03-21)
changeset 15964a09f4698813
parent 1595 b9984b1dbc4c
child 1597 54ece585bf62
Printing & string functions moved to display.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Thu Mar 21 11:04:36 1996 +0100
     1.2 +++ b/src/Pure/drule.ML	Thu Mar 21 11:05:34 1996 +0100
     1.3 @@ -37,21 +37,6 @@
     1.4    val implies_intr_list	: cterm list -> thm -> thm
     1.5    val MRL		: thm list list * thm list -> thm list
     1.6    val MRS		: thm list * thm -> thm
     1.7 -  val pprint_cterm	: cterm -> pprint_args -> unit
     1.8 -  val pprint_ctyp	: ctyp -> pprint_args -> unit
     1.9 -  val pprint_theory	: theory -> pprint_args -> unit
    1.10 -  val pprint_thm	: thm -> pprint_args -> unit
    1.11 -  val pretty_thm	: thm -> Pretty.T
    1.12 -  val print_cterm	: cterm -> unit
    1.13 -  val print_ctyp	: ctyp -> unit
    1.14 -  val print_goals	: int -> thm -> unit
    1.15 -  val print_goals_ref	: (int -> thm -> unit) ref
    1.16 -  val print_syntax	: theory -> unit
    1.17 -  val print_theory	: theory -> unit
    1.18 -  val print_thm		: thm -> unit
    1.19 -  val prth		: thm -> thm
    1.20 -  val prthq		: thm Sequence.seq -> thm Sequence.seq
    1.21 -  val prths		: thm list -> thm list
    1.22    val read_instantiate	: (string*string)list -> thm -> thm
    1.23    val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    1.24    val read_insts	:
    1.25 @@ -69,12 +54,8 @@
    1.26    val RSN		: thm * (int * thm) -> thm
    1.27    val RL		: thm list * thm list -> thm list
    1.28    val RLN		: thm list * (int * thm list) -> thm list
    1.29 -  val show_hyps		: bool ref
    1.30    val size_of_thm	: thm -> int
    1.31    val standard		: thm -> thm
    1.32 -  val string_of_cterm	: cterm -> string
    1.33 -  val string_of_ctyp	: ctyp -> string
    1.34 -  val string_of_thm	: thm -> string
    1.35    val symmetric_thm	: thm
    1.36    val thin_rl		: thm
    1.37    val transitive_thm	: thm
    1.38 @@ -274,179 +255,6 @@
    1.39  end;
    1.40  
    1.41  
    1.42 -
    1.43 -(*** Printing of theories, theorems, etc. ***)
    1.44 -
    1.45 -(*If false, hypotheses are printed as dots*)
    1.46 -val show_hyps = ref true;
    1.47 -
    1.48 -fun pretty_thm th =
    1.49 -  let
    1.50 -    val {sign, hyps, prop, ...} = rep_thm th;
    1.51 -    val xshyps = extra_shyps th;
    1.52 -    val hlen = length xshyps + length hyps;
    1.53 -    val hsymbs =
    1.54 -      if hlen = 0 then []
    1.55 -      else if ! show_hyps then
    1.56 -        [Pretty.brk 2, Pretty.list "[" "]"
    1.57 -          (map (Sign.pretty_term sign) hyps @ map Sign.pretty_sort xshyps)]
    1.58 -      else
    1.59 -        [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")];
    1.60 -  in
    1.61 -    Pretty.block (Sign.pretty_term sign prop :: hsymbs)
    1.62 -  end;
    1.63 -
    1.64 -val string_of_thm = Pretty.string_of o pretty_thm;
    1.65 -val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
    1.66 -
    1.67 -
    1.68 -(** Top-level commands for printing theorems **)
    1.69 -val print_thm = writeln o string_of_thm;
    1.70 -
    1.71 -fun prth th = (print_thm th; th);
    1.72 -
    1.73 -(*Print and return a sequence of theorems, separated by blank lines. *)
    1.74 -fun prthq thseq =
    1.75 -  (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq);
    1.76 -
    1.77 -(*Print and return a list of theorems, separated by blank lines. *)
    1.78 -fun prths ths = (print_list_ln print_thm ths; ths);
    1.79 -
    1.80 -
    1.81 -(* other printing commands *)
    1.82 -
    1.83 -fun pprint_ctyp cT =
    1.84 -  let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end;
    1.85 -
    1.86 -fun string_of_ctyp cT =
    1.87 -  let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end;
    1.88 -
    1.89 -val print_ctyp = writeln o string_of_ctyp;
    1.90 -
    1.91 -fun pprint_cterm ct =
    1.92 -  let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end;
    1.93 -
    1.94 -fun string_of_cterm ct =
    1.95 -  let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end;
    1.96 -
    1.97 -val print_cterm = writeln o string_of_cterm;
    1.98 -
    1.99 -
   1.100 -(* print theory *)
   1.101 -
   1.102 -val pprint_theory = Sign.pprint_sg o sign_of;
   1.103 -
   1.104 -val print_syntax = Syntax.print_syntax o syn_of;
   1.105 -
   1.106 -fun print_axioms thy =
   1.107 -  let
   1.108 -    val {sign, new_axioms, ...} = rep_theory thy;
   1.109 -    val axioms = Symtab.dest new_axioms;
   1.110 -
   1.111 -    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
   1.112 -      Pretty.quote (Sign.pretty_term sign t)];
   1.113 -  in
   1.114 -    Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms))
   1.115 -  end;
   1.116 -
   1.117 -fun print_theory thy = (Sign.print_sg (sign_of thy); print_axioms thy);
   1.118 -
   1.119 -
   1.120 -
   1.121 -(** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **)
   1.122 -
   1.123 -(* get type_env, sort_env of term *)
   1.124 -
   1.125 -local
   1.126 -  open Syntax;
   1.127 -
   1.128 -  fun ins_entry (x, y) [] = [(x, [y])]
   1.129 -    | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
   1.130 -        if x = x' then (x', y ins ys') :: pairs
   1.131 -        else pair :: ins_entry (x, y) pairs;
   1.132 -
   1.133 -  fun add_type_env (Free (x, T), env) = ins_entry (T, x) env
   1.134 -    | add_type_env (Var (xi, T), env) = ins_entry (T, string_of_vname xi) env
   1.135 -    | add_type_env (Abs (_, _, t), env) = add_type_env (t, env)
   1.136 -    | add_type_env (t $ u, env) = add_type_env (u, add_type_env (t, env))
   1.137 -    | add_type_env (_, env) = env;
   1.138 -
   1.139 -  fun add_sort_env (Type (_, Ts), env) = foldr add_sort_env (Ts, env)
   1.140 -    | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env
   1.141 -    | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env;
   1.142 -
   1.143 -  val sort = map (apsnd sort_strings);
   1.144 -in
   1.145 -  fun type_env t = sort (add_type_env (t, []));
   1.146 -  fun sort_env t = rev (sort (it_term_types add_sort_env (t, [])));
   1.147 -end;
   1.148 -
   1.149 -
   1.150 -(* print_goals *)
   1.151 -
   1.152 -fun print_goals maxgoals state =
   1.153 -  let
   1.154 -    open Syntax;
   1.155 -
   1.156 -    val {sign, prop, ...} = rep_thm state;
   1.157 -
   1.158 -    val pretty_term = Sign.pretty_term sign;
   1.159 -    val pretty_typ = Sign.pretty_typ sign;
   1.160 -    val pretty_sort = Sign.pretty_sort;
   1.161 -
   1.162 -    fun pretty_vars prtf (X, vs) = Pretty.block
   1.163 -      [Pretty.block (Pretty.commas (map Pretty.str vs)),
   1.164 -        Pretty.str " ::", Pretty.brk 1, prtf X];
   1.165 -
   1.166 -    fun print_list _ _ [] = ()
   1.167 -      | print_list name prtf lst =
   1.168 -          (writeln ""; Pretty.writeln (Pretty.big_list name (map prtf lst)));
   1.169 -
   1.170 -
   1.171 -    fun print_goals (_, []) = ()
   1.172 -      | print_goals (n, A :: As) = (Pretty.writeln (Pretty.blk (0,
   1.173 -          [Pretty.str (" " ^ string_of_int n ^ ". "), pretty_term A]));
   1.174 -            print_goals (n + 1, As));
   1.175 -
   1.176 -    val print_ffpairs =
   1.177 -      print_list "Flex-flex pairs:" (pretty_term o Logic.mk_flexpair);
   1.178 -
   1.179 -    val print_types = print_list "Types:" (pretty_vars pretty_typ) o type_env;
   1.180 -    val print_sorts = print_list "Sorts:" (pretty_vars pretty_sort) o sort_env;
   1.181 -
   1.182 -
   1.183 -    val (tpairs, As, B) = Logic.strip_horn prop;
   1.184 -    val ngoals = length As;
   1.185 -
   1.186 -    val orig_no_freeTs = ! show_no_free_types;
   1.187 -    val orig_sorts = ! show_sorts;
   1.188 -
   1.189 -    fun restore () =
   1.190 -      (show_no_free_types := orig_no_freeTs; show_sorts := orig_sorts);
   1.191 -  in
   1.192 -    (show_no_free_types := true; show_sorts := false;
   1.193 -      Pretty.writeln (pretty_term B);
   1.194 -      if ngoals = 0 then writeln "No subgoals!"
   1.195 -      else if ngoals > maxgoals then
   1.196 -        (print_goals (1, take (maxgoals, As));
   1.197 -          writeln ("A total of " ^ string_of_int ngoals ^ " subgoals..."))
   1.198 -      else print_goals (1, As);
   1.199 -
   1.200 -      print_ffpairs tpairs;
   1.201 -
   1.202 -      if orig_sorts then
   1.203 -        (print_types prop; print_sorts prop)
   1.204 -      else if ! show_types then
   1.205 -        print_types prop
   1.206 -      else ())
   1.207 -    handle exn => (restore (); raise exn);
   1.208 -    restore ()
   1.209 -  end;
   1.210 -
   1.211 -
   1.212 -(*"hook" for user interfaces: allows print_goals to be replaced*)
   1.213 -val print_goals_ref = ref print_goals;
   1.214 -
   1.215  (*** Find the type (sort) associated with a (T)Var or (T)Free in a term
   1.216       Used for establishing default types (of variables) and sorts (of
   1.217       type variables) when reading another term.