11 val pp_typ: (unit -> theory) -> typ -> Pretty.T |
11 val pp_typ: (unit -> theory) -> typ -> Pretty.T |
12 val pp_term: (unit -> theory) -> term -> Pretty.T |
12 val pp_term: (unit -> theory) -> term -> Pretty.T |
13 val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T |
13 val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T |
14 val pp_cterm: (unit -> theory) -> cterm -> Pretty.T |
14 val pp_cterm: (unit -> theory) -> cterm -> Pretty.T |
15 val pretty_definitions: bool -> Proof.context -> Pretty.T |
15 val pretty_definitions: bool -> Proof.context -> Pretty.T |
16 val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list |
16 val pretty_theorems_diff: bool -> theory list -> Proof.context -> Pretty.T list |
17 val pretty_theorems: bool -> theory -> Pretty.T list |
17 val pretty_theorems: bool -> Proof.context -> Pretty.T list |
18 val pretty_full_theory: bool -> theory -> Pretty.T |
18 val pretty_theory: bool -> Proof.context -> Pretty.T |
19 val string_of_rule: Proof.context -> string -> thm -> string |
19 val string_of_rule: Proof.context -> string -> thm -> string |
20 val pretty_goal_header: thm -> Pretty.T |
20 val pretty_goal_header: thm -> Pretty.T |
21 val string_of_goal: Proof.context -> thm -> string |
21 val string_of_goal: Proof.context -> thm -> string |
22 val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T |
22 val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T |
23 val method_error: string -> Position.T -> |
23 val method_error: string -> Position.T -> |
60 |
60 |
61 (** theory content **) |
61 (** theory content **) |
62 |
62 |
63 (* theorems and theory *) |
63 (* theorems and theory *) |
64 |
64 |
65 fun pretty_theorems_diff verbose prev_thys thy = |
65 fun pretty_theorems_diff verbose prev_thys ctxt = |
66 let |
66 let |
67 val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy); |
67 val pretty_fact = Proof_Context.pretty_fact ctxt; |
68 val facts = Global_Theory.facts_of thy; |
68 val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt); |
69 val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts; |
69 val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts; |
70 val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss)); |
70 val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss)); |
71 in if null prts then [] else [Pretty.big_list "theorems:" prts] end; |
71 in if null prts then [] else [Pretty.big_list "theorems:" prts] end; |
72 |
72 |
73 fun pretty_theorems verbose thy = |
73 fun pretty_theorems verbose ctxt = |
74 pretty_theorems_diff verbose (Theory.parents_of thy) thy; |
74 pretty_theorems_diff verbose (Theory.parents_of (Proof_Context.theory_of ctxt)) ctxt; |
75 |
75 |
76 fun pretty_full_theory verbose thy = |
76 fun pretty_theory verbose ctxt = |
77 Pretty.chunks (Display.pretty_full_theory verbose thy @ pretty_theorems verbose thy); |
77 let |
|
78 val thy = Proof_Context.theory_of ctxt; |
|
79 |
|
80 fun prt_cls c = Syntax.pretty_sort ctxt [c]; |
|
81 fun prt_sort S = Syntax.pretty_sort ctxt S; |
|
82 fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]); |
|
83 fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); |
|
84 val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; |
|
85 fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); |
|
86 val prt_term_no_vars = prt_term o Logic.unvarify_global; |
|
87 fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; |
|
88 |
|
89 fun pretty_classrel (c, []) = prt_cls c |
|
90 | pretty_classrel (c, cs) = Pretty.block |
|
91 (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); |
|
92 |
|
93 fun pretty_default S = Pretty.block |
|
94 [Pretty.str "default sort:", Pretty.brk 1, prt_sort S]; |
|
95 |
|
96 val tfrees = map (fn v => TFree (v, [])); |
|
97 fun pretty_type syn (t, Type.LogicalType n) = |
|
98 if syn then NONE |
|
99 else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n)))) |
|
100 | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) = |
|
101 if syn <> syn' then NONE |
|
102 else SOME (Pretty.block |
|
103 [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U]) |
|
104 | pretty_type syn (t, Type.Nonterminal) = |
|
105 if not syn then NONE |
|
106 else SOME (prt_typ (Type (t, []))); |
|
107 |
|
108 val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars); |
|
109 |
|
110 fun pretty_abbrev (c, (ty, t)) = Pretty.block |
|
111 (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]); |
|
112 |
|
113 fun pretty_axm (a, t) = |
|
114 Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t]; |
|
115 |
|
116 val tsig = Sign.tsig_of thy; |
|
117 val consts = Sign.consts_of thy; |
|
118 val {const_space, constants, constraints} = Consts.dest consts; |
|
119 val {classes, default, types, ...} = Type.rep_tsig tsig; |
|
120 val type_space = Type.type_space tsig; |
|
121 val (class_space, class_algebra) = classes; |
|
122 val classes = Sorts.classes_of class_algebra; |
|
123 val arities = Sorts.arities_of class_algebra; |
|
124 |
|
125 val clsses = |
|
126 Name_Space.extern_entries verbose ctxt class_space |
|
127 (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)) |
|
128 |> map (apfst #1); |
|
129 val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1); |
|
130 val arties = |
|
131 Name_Space.extern_entries verbose ctxt type_space (Symtab.dest arities) |
|
132 |> map (apfst #1); |
|
133 |
|
134 val cnsts = Name_Space.markup_entries verbose ctxt const_space constants; |
|
135 val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; |
|
136 val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; |
|
137 val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints; |
|
138 |
|
139 val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy); |
|
140 in |
|
141 [Pretty.strs ("names:" :: Context.display_names thy)] @ |
|
142 [Pretty.big_list "classes:" (map pretty_classrel clsses), |
|
143 pretty_default default, |
|
144 Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), |
|
145 Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls), |
|
146 Pretty.big_list "type arities:" (pretty_arities arties), |
|
147 Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts), |
|
148 Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), |
|
149 Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), |
|
150 Pretty.big_list "axioms:" (map pretty_axm axms), |
|
151 Pretty.block |
|
152 (Pretty.breaks (Pretty.str "oracles:" :: |
|
153 map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))] @ |
|
154 pretty_theorems verbose ctxt |
|
155 end |> Pretty.chunks; |
78 |
156 |
79 |
157 |
80 (* definitions *) |
158 (* definitions *) |
81 |
159 |
82 fun pretty_definitions verbose ctxt = |
160 fun pretty_definitions verbose ctxt = |