paulson@1591: (* Title: Pure/display.ML paulson@1591: ID: $Id$ paulson@1591: Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@1591: Copyright 1993 University of Cambridge paulson@1591: paulson@1591: Printing of theories, theorems, etc. paulson@1591: *) paulson@1591: paulson@1591: signature DISPLAY = paulson@1591: sig paulson@1591: val pprint_cterm : cterm -> pprint_args -> unit paulson@1591: val pprint_ctyp : ctyp -> pprint_args -> unit paulson@1591: val pprint_theory : theory -> pprint_args -> unit paulson@1591: val pprint_thm : thm -> pprint_args -> unit wenzelm@3547: val pretty_cterm : cterm -> Pretty.T paulson@1591: val pretty_thm : thm -> Pretty.T paulson@1591: val print_cterm : cterm -> unit paulson@1591: val print_ctyp : ctyp -> unit paulson@1591: val print_goals : int -> thm -> unit paulson@1591: val print_syntax : theory -> unit paulson@1591: val print_theory : theory -> unit paulson@1591: val print_thm : thm -> unit paulson@1591: val prth : thm -> thm paulson@1591: val prthq : thm Sequence.seq -> thm Sequence.seq paulson@1591: val prths : thm list -> thm list paulson@1591: val show_hyps : bool ref paulson@1591: val string_of_cterm : cterm -> string paulson@1591: val string_of_ctyp : ctyp -> string paulson@1591: val string_of_thm : thm -> string paulson@1591: end; paulson@1591: paulson@1591: paulson@1591: structure Display : DISPLAY = paulson@1591: struct paulson@1591: paulson@1591: (*If false, hypotheses are printed as dots*) paulson@1591: val show_hyps = ref true; paulson@1591: paulson@1591: fun pretty_thm th = paulson@1591: let paulson@1591: val {sign, hyps, prop, ...} = rep_thm th; paulson@1591: val xshyps = extra_shyps th; paulson@1591: val hlen = length xshyps + length hyps; paulson@1591: val hsymbs = paulson@1591: if hlen = 0 then [] paulson@1591: else if ! show_hyps then paulson@1591: [Pretty.brk 2, Pretty.list "[" "]" wenzelm@3785: (map (Sign.pretty_term sign) hyps @ wenzelm@3785: map (Sign.pretty_sort sign) xshyps)] paulson@1591: else paulson@1591: [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")]; paulson@1591: in paulson@1591: Pretty.block (Sign.pretty_term sign prop :: hsymbs) paulson@1591: end; paulson@1591: paulson@1591: val string_of_thm = Pretty.string_of o pretty_thm; paulson@1591: val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm; paulson@1591: paulson@1591: paulson@1591: (** Top-level commands for printing theorems **) paulson@1591: val print_thm = writeln o string_of_thm; paulson@1591: paulson@1591: fun prth th = (print_thm th; th); paulson@1591: paulson@1591: (*Print and return a sequence of theorems, separated by blank lines. *) paulson@1591: fun prthq thseq = paulson@1591: (Sequence.prints (fn _ => print_thm) 100000 thseq; thseq); paulson@1591: paulson@1591: (*Print and return a list of theorems, separated by blank lines. *) paulson@1591: fun prths ths = (print_list_ln print_thm ths; ths); paulson@1591: paulson@1591: paulson@1591: (* other printing commands *) paulson@1591: paulson@1591: fun pprint_ctyp cT = paulson@1591: let val {sign, T} = rep_ctyp cT in Sign.pprint_typ sign T end; paulson@1591: paulson@1591: fun string_of_ctyp cT = paulson@1591: let val {sign, T} = rep_ctyp cT in Sign.string_of_typ sign T end; paulson@1591: paulson@1591: val print_ctyp = writeln o string_of_ctyp; paulson@1591: wenzelm@3547: fun pretty_cterm ct = wenzelm@3547: let val {sign, t, ...} = rep_cterm ct in Sign.pretty_term sign t end; wenzelm@3547: paulson@1591: fun pprint_cterm ct = paulson@1591: let val {sign, t, ...} = rep_cterm ct in Sign.pprint_term sign t end; paulson@1591: paulson@1591: fun string_of_cterm ct = paulson@1591: let val {sign, t, ...} = rep_cterm ct in Sign.string_of_term sign t end; paulson@1591: paulson@1591: val print_cterm = writeln o string_of_cterm; paulson@1591: paulson@1591: paulson@1591: (* print theory *) paulson@1591: paulson@1591: val pprint_theory = Sign.pprint_sg o sign_of; paulson@1591: paulson@1591: val print_syntax = Syntax.print_syntax o syn_of; paulson@1591: wenzelm@3811: fun print_thy thy = paulson@1591: let wenzelm@3811: val {sign, new_axioms, oracles, ...} = rep_theory thy; paulson@1591: val axioms = Symtab.dest new_axioms; wenzelm@3811: val oras = map fst (Symtab.dest oracles); paulson@1591: paulson@1591: fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, paulson@1591: Pretty.quote (Sign.pretty_term sign t)]; paulson@1591: in wenzelm@3811: Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms)); wenzelm@3811: Pretty.writeln (Pretty.strs ("oracles:" :: oras)) paulson@1591: end; paulson@1591: wenzelm@3811: fun print_theory thy = (Sign.print_sg (sign_of thy); print_thy thy); paulson@1591: paulson@1591: paulson@1591: paulson@1591: (** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **) paulson@1591: paulson@1591: (* get type_env, sort_env of term *) paulson@1591: paulson@1591: local paulson@1591: open Syntax; paulson@1591: paulson@1591: fun ins_entry (x, y) [] = [(x, [y])] paulson@1591: | ins_entry (x, y) ((pair as (x', ys')) :: pairs) = paulson@2180: if x = x' then (x', y ins_string ys') :: pairs paulson@1591: else pair :: ins_entry (x, y) pairs; paulson@1591: paulson@1591: fun add_type_env (Free (x, T), env) = ins_entry (T, x) env paulson@1591: | add_type_env (Var (xi, T), env) = ins_entry (T, string_of_vname xi) env paulson@1591: | add_type_env (Abs (_, _, t), env) = add_type_env (t, env) paulson@1591: | add_type_env (t $ u, env) = add_type_env (u, add_type_env (t, env)) paulson@1591: | add_type_env (_, env) = env; paulson@1591: paulson@1591: fun add_sort_env (Type (_, Ts), env) = foldr add_sort_env (Ts, env) paulson@1591: | add_sort_env (TFree (x, S), env) = ins_entry (S, x) env paulson@1591: | add_sort_env (TVar (xi, S), env) = ins_entry (S, string_of_vname xi) env; paulson@1591: paulson@2226: fun sort l = map (apsnd sort_strings) l; paulson@1591: in paulson@1591: fun type_env t = sort (add_type_env (t, [])); paulson@1591: fun sort_env t = rev (sort (it_term_types add_sort_env (t, []))); paulson@1591: end; paulson@1591: paulson@1591: paulson@1591: (* print_goals *) paulson@1591: paulson@1591: fun print_goals maxgoals state = paulson@1591: let paulson@1591: open Syntax; paulson@1591: paulson@1591: val {sign, prop, ...} = rep_thm state; paulson@1591: paulson@1591: val pretty_term = Sign.pretty_term sign; paulson@1591: val pretty_typ = Sign.pretty_typ sign; wenzelm@3785: val pretty_sort = Sign.pretty_sort sign; paulson@1591: paulson@1591: fun pretty_vars prtf (X, vs) = Pretty.block paulson@1591: [Pretty.block (Pretty.commas (map Pretty.str vs)), paulson@1591: Pretty.str " ::", Pretty.brk 1, prtf X]; paulson@1591: paulson@1591: fun print_list _ _ [] = () paulson@1591: | print_list name prtf lst = paulson@1591: (writeln ""; Pretty.writeln (Pretty.big_list name (map prtf lst))); paulson@1591: paulson@1591: paulson@1591: fun print_goals (_, []) = () paulson@1591: | print_goals (n, A :: As) = (Pretty.writeln (Pretty.blk (0, paulson@1591: [Pretty.str (" " ^ string_of_int n ^ ". "), pretty_term A])); paulson@1591: print_goals (n + 1, As)); paulson@1591: paulson@1591: val print_ffpairs = paulson@1591: print_list "Flex-flex pairs:" (pretty_term o Logic.mk_flexpair); paulson@1591: paulson@1591: val print_types = print_list "Types:" (pretty_vars pretty_typ) o type_env; paulson@1591: val print_sorts = print_list "Sorts:" (pretty_vars pretty_sort) o sort_env; paulson@1591: paulson@1591: paulson@1591: val (tpairs, As, B) = Logic.strip_horn prop; paulson@1591: val ngoals = length As; paulson@1591: paulson@1591: val orig_no_freeTs = ! show_no_free_types; wenzelm@2992: val orig_types = ! show_types; paulson@1591: val orig_sorts = ! show_sorts; paulson@1591: paulson@1591: fun restore () = wenzelm@2992: (show_no_free_types := orig_no_freeTs; wenzelm@2992: show_types := orig_types; wenzelm@2992: show_sorts := orig_sorts); paulson@1591: in wenzelm@2992: (show_no_free_types := true; wenzelm@2992: show_types := (orig_types orelse orig_sorts); wenzelm@2992: show_sorts := false; paulson@1591: Pretty.writeln (pretty_term B); paulson@1591: if ngoals = 0 then writeln "No subgoals!" paulson@1591: else if ngoals > maxgoals then paulson@1591: (print_goals (1, take (maxgoals, As)); paulson@1591: writeln ("A total of " ^ string_of_int ngoals ^ " subgoals...")) paulson@1591: else print_goals (1, As); paulson@1591: paulson@1591: print_ffpairs tpairs; paulson@1591: paulson@1591: if orig_sorts then paulson@1591: (print_types prop; print_sorts prop) wenzelm@2992: else if orig_types then paulson@1591: print_types prop paulson@1591: else ()) paulson@1591: handle exn => (restore (); raise exn); paulson@1591: restore () paulson@1591: end; paulson@1591: paulson@1591: paulson@1591: end; paulson@1591: paulson@1591: open Display;