paulson@1591: (* Title: Pure/display.ML paulson@1591: Author: Lawrence C Paulson, Cambridge University Computer Laboratory wenzelm@32089: Author: Makarius paulson@1591: wenzelm@32089: Printing of theorems, results etc. paulson@1591: *) paulson@1591: wenzelm@11883: signature BASIC_DISPLAY = wenzelm@11883: sig wenzelm@32738: val goals_limit: int Unsynchronized.ref wenzelm@32738: val show_consts: bool Unsynchronized.ref wenzelm@32738: val show_hyps: bool Unsynchronized.ref wenzelm@32738: val show_tags: bool Unsynchronized.ref wenzelm@11883: end; wenzelm@11883: paulson@1591: signature DISPLAY = wenzelm@4950: sig wenzelm@11883: include BASIC_DISPLAY wenzelm@32145: val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} -> wenzelm@32145: thm -> Pretty.T wenzelm@32090: val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T wenzelm@32090: val pretty_thm: Proof.context -> thm -> Pretty.T wenzelm@32090: val pretty_thm_global: theory -> thm -> Pretty.T wenzelm@32090: val pretty_thm_without_context: thm -> Pretty.T wenzelm@32090: val string_of_thm: Proof.context -> thm -> string wenzelm@32090: val string_of_thm_global: theory -> thm -> string wenzelm@32090: val string_of_thm_without_context: thm -> string wenzelm@32090: val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T wenzelm@32090: val pretty_thms: Proof.context -> thm list -> Pretty.T wenzelm@26928: val print_syntax: theory -> unit wenzelm@20629: val pretty_full_theory: bool -> theory -> Pretty.T list wenzelm@4950: end; paulson@1591: wenzelm@4950: structure Display: DISPLAY = paulson@1591: struct paulson@1591: wenzelm@32089: (** options **) wenzelm@32089: wenzelm@32187: val goals_limit = Goal_Display.goals_limit; wenzelm@32187: val show_consts = Goal_Display.show_consts; wenzelm@32089: wenzelm@32738: val show_hyps = Unsynchronized.ref false; (*false: print meta-hypotheses as dots*) wenzelm@32738: val show_tags = Unsynchronized.ref false; (*false: suppress tags*) wenzelm@32089: wenzelm@32089: wenzelm@11883: wenzelm@6087: (** print thm **) wenzelm@6087: wenzelm@28840: fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; wenzelm@6087: val pretty_tags = Pretty.list "[" "]" o map pretty_tag; paulson@1591: wenzelm@30723: fun display_status false _ = "" wenzelm@30723: | display_status true th = wenzelm@30723: let wenzelm@30723: val {oracle = oracle0, unfinished, failed} = Thm.status_of th; wenzelm@30723: val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps); wenzelm@30723: in wenzelm@30723: if failed then "!!" wenzelm@30723: else if oracle andalso unfinished then "!?" wenzelm@30723: else if oracle then "!" wenzelm@30723: else if unfinished then "?" wenzelm@30723: else "" wenzelm@30723: end; wenzelm@30711: wenzelm@32145: fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th = paulson@1591: let wenzelm@17447: val th = Thm.strip_shyps raw_th; wenzelm@28316: val {hyps, tpairs, prop, ...} = Thm.rep_thm th; wenzelm@6087: val xshyps = Thm.extra_shyps th; wenzelm@21646: val tags = Thm.get_tags th; wenzelm@6087: berghofe@13658: val q = if quote then Pretty.quote else I; wenzelm@32145: val prt_term = q o Syntax.pretty_term ctxt; wenzelm@6279: wenzelm@32145: val asms = map Thm.term_of (Assumption.all_assms_of ctxt); wenzelm@19300: val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps; wenzelm@30723: val status = display_status show_status th; wenzelm@28802: wenzelm@17447: val hlen = length xshyps + length hyps' + length tpairs; paulson@1591: val hsymbs = wenzelm@30711: if hlen = 0 andalso status = "" then [] wenzelm@17447: else if ! show_hyps orelse show_hyps' then paulson@1591: [Pretty.brk 2, Pretty.list "[" "]" wenzelm@32187: (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ wenzelm@32145: map (Syntax.pretty_sort ctxt) xshyps @ wenzelm@30711: (if status = "" then [] else [Pretty.str status]))] wenzelm@30711: else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")]; wenzelm@6087: val tsymbs = wenzelm@6087: if null tags orelse not (! show_tags) then [] wenzelm@6087: else [Pretty.brk 1, pretty_tags tags]; wenzelm@6279: in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; paulson@1591: wenzelm@32145: fun pretty_thm_aux ctxt show_status = wenzelm@32145: pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status}; wenzelm@6087: wenzelm@32090: fun pretty_thm ctxt = pretty_thm_aux ctxt true; wenzelm@32090: wenzelm@32145: fun pretty_thm_global thy = wenzelm@32145: pretty_thm_raw (Syntax.init_pretty_global thy) wenzelm@32145: {quote = false, show_hyps = false, show_status = true}; wenzelm@32090: wenzelm@32090: fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th; wenzelm@6087: wenzelm@32090: val string_of_thm = Pretty.string_of oo pretty_thm; wenzelm@32090: val string_of_thm_global = Pretty.string_of oo pretty_thm_global; wenzelm@32090: val string_of_thm_without_context = Pretty.string_of o pretty_thm_without_context; wenzelm@32090: paulson@1591: wenzelm@32090: (* multiple theorems *) wenzelm@32090: wenzelm@32090: fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th wenzelm@32090: | pretty_thms_aux ctxt flag ths = wenzelm@32090: Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths)); wenzelm@32090: wenzelm@32090: fun pretty_thms ctxt = pretty_thms_aux ctxt true; paulson@1591: paulson@1591: wenzelm@4250: wenzelm@4250: (** print theory **) paulson@1591: wenzelm@16437: val print_syntax = Syntax.print_syntax o Sign.syn_of; wenzelm@4498: wenzelm@4498: wenzelm@11883: (* pretty_full_theory *) wenzelm@4250: wenzelm@20629: fun pretty_full_theory verbose thy = wenzelm@4250: let wenzelm@35199: val ctxt = Syntax.init_pretty_global thy; wenzelm@24920: wenzelm@24920: fun prt_cls c = Syntax.pretty_sort ctxt [c]; wenzelm@24920: fun prt_sort S = Syntax.pretty_sort ctxt S; wenzelm@24920: fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]); wenzelm@24920: fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); wenzelm@35845: val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; wenzelm@24920: fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); wenzelm@35845: val prt_term_no_vars = prt_term o Logic.unvarify_global; wenzelm@19698: fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; wenzelm@26939: val prt_const' = Defs.pretty_const (Syntax.pp ctxt); wenzelm@4250: wenzelm@14794: fun pretty_classrel (c, []) = prt_cls c wenzelm@14794: | pretty_classrel (c, cs) = Pretty.block wenzelm@14794: (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: wenzelm@14794: Pretty.commas (map prt_cls cs)); wenzelm@4250: wenzelm@4250: fun pretty_default S = Pretty.block wenzelm@14794: [Pretty.str "default sort:", Pretty.brk 1, prt_sort S]; wenzelm@4250: wenzelm@14996: val tfrees = map (fn v => TFree (v, [])); wenzelm@33173: fun pretty_type syn (t, (Type.LogicalType n)) = skalberg@15531: if syn then NONE wenzelm@24848: else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n)))) wenzelm@33173: | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) = skalberg@15531: if syn <> syn' then NONE skalberg@15531: else SOME (Pretty.block wenzelm@14996: [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U]) wenzelm@33173: | pretty_type syn (t, Type.Nonterminal) = skalberg@15531: if not syn then NONE skalberg@15531: else SOME (prt_typ (Type (t, []))); wenzelm@4250: wenzelm@19482: val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars); skalberg@14223: wenzelm@19698: fun pretty_abbrev (c, (ty, t)) = Pretty.block wenzelm@19698: (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]); wenzelm@19698: wenzelm@19698: fun pretty_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t]; wenzelm@19365: wenzelm@19702: fun pretty_finals reds = Pretty.block wenzelm@19703: (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_const' o fst) reds)); wenzelm@19702: wenzelm@19698: fun pretty_reduct (lhs, rhs) = Pretty.block wenzelm@19702: ([prt_const' lhs, Pretty.str " ->", Pretty.brk 2] @ wenzelm@19702: Pretty.commas (map prt_const' (sort_wrt #1 rhs))); wenzelm@4250: wenzelm@19698: fun pretty_restrict (const, name) = wenzelm@19698: Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); wenzelm@8720: wenzelm@24665: val axioms = (Theory.axiom_space thy, Theory.axiom_table thy); wenzelm@24665: val defs = Theory.defs_of thy; wenzelm@19698: val {restricts, reducts} = Defs.dest defs; wenzelm@32784: val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy; wenzelm@18936: val {constants, constraints} = Consts.dest consts; wenzelm@33095: val extern_const = Name_Space.extern (#1 constants); wenzelm@26637: val {classes, default, types, ...} = Type.rep_tsig tsig; wenzelm@19698: val (class_space, class_algebra) = classes; wenzelm@36328: val classes = Sorts.classes_of class_algebra; wenzelm@36328: val arities = Sorts.arities_of class_algebra; wenzelm@14996: wenzelm@33095: val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes)); wenzelm@33095: val tdecls = Name_Space.dest_table types; wenzelm@33095: val arties = Name_Space.dest_table (Sign.type_space thy, arities); wenzelm@20629: wenzelm@33158: fun prune_const c = not verbose andalso Consts.is_concealed consts c; wenzelm@33095: val cnsts = Name_Space.extern_table (#1 constants, wenzelm@24774: Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants)))); wenzelm@24774: wenzelm@19482: val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; wenzelm@25405: val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; wenzelm@33095: val cnstrs = Name_Space.extern_table constraints; wenzelm@19698: wenzelm@33095: val axms = Name_Space.extern_table axioms; wenzelm@24774: wenzelm@24774: val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts wenzelm@24774: |> map (fn (lhs, rhs) => wenzelm@24774: (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs))) wenzelm@19702: |> sort_wrt (#1 o #1) wenzelm@19702: |> List.partition (null o #2) wenzelm@19702: ||> List.partition (Defs.plain_args o #2 o #1); wenzelm@19698: val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1); wenzelm@4250: in wenzelm@29091: [Pretty.strs ("names:" :: Context.display_names thy)] @ wenzelm@30409: [Pretty.big_list "classes:" (map pretty_classrel clsses), wenzelm@8720: pretty_default default, wenzelm@19482: Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), wenzelm@19482: Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), wenzelm@16534: Pretty.big_list "type arities:" (pretty_arities arties), wenzelm@19698: Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts), wenzelm@19365: Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), wenzelm@19698: Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), wenzelm@19698: Pretty.big_list "axioms:" (map pretty_axm axms), wenzelm@28290: Pretty.strs ("oracles:" :: Thm.extern_oracles thy), wenzelm@19698: Pretty.big_list "definitions:" wenzelm@19702: [pretty_finals reds0, wenzelm@19702: Pretty.big_list "non-overloaded:" (map pretty_reduct reds1), wenzelm@19702: Pretty.big_list "overloaded:" (map pretty_reduct reds2), wenzelm@19702: Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]] wenzelm@4250: end; wenzelm@4250: paulson@1591: end; paulson@1591: wenzelm@32089: structure Basic_Display: BASIC_DISPLAY = Display; wenzelm@32089: open Basic_Display;