102 fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); |
102 fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); |
103 val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; |
103 val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; |
104 fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); |
104 fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); |
105 val prt_term_no_vars = prt_term o Logic.unvarify_global; |
105 val prt_term_no_vars = prt_term o Logic.unvarify_global; |
106 fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; |
106 fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; |
107 val prt_item = Defs.pretty_item ctxt; |
|
108 fun sort_item_by f = sort (Defs.item_ord o apply2 f); |
|
109 |
107 |
110 fun pretty_classrel (c, []) = prt_cls c |
108 fun pretty_classrel (c, []) = prt_cls c |
111 | pretty_classrel (c, cs) = Pretty.block |
109 | pretty_classrel (c, cs) = Pretty.block |
112 (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); |
110 (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs)); |
113 |
111 |
132 (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]); |
130 (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]); |
133 |
131 |
134 fun pretty_axm (a, t) = |
132 fun pretty_axm (a, t) = |
135 Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t]; |
133 Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t]; |
136 |
134 |
137 fun pretty_finals reds = Pretty.block |
|
138 (Pretty.str "final:" :: Pretty.brk 1 :: Pretty.commas (map (prt_item o fst) reds)); |
|
139 |
|
140 fun pretty_reduct (lhs, rhs) = Pretty.block |
|
141 ([prt_item lhs, Pretty.str " ->", Pretty.brk 2] @ |
|
142 Pretty.commas (map prt_item (sort_item_by #1 rhs))); |
|
143 |
|
144 fun pretty_restrict (const, name) = |
|
145 Pretty.block ([prt_item const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]); |
|
146 |
|
147 val defs = Theory.defs_of thy; |
|
148 val {restricts, reducts} = Defs.dest defs; |
|
149 val tsig = Sign.tsig_of thy; |
135 val tsig = Sign.tsig_of thy; |
150 val consts = Sign.consts_of thy; |
136 val consts = Sign.consts_of thy; |
151 val {const_space, constants, constraints} = Consts.dest consts; |
137 val {const_space, constants, constraints} = Consts.dest consts; |
152 val {classes, default, types, ...} = Type.rep_tsig tsig; |
138 val {classes, default, types, ...} = Type.rep_tsig tsig; |
153 val type_space = Type.type_space tsig; |
139 val type_space = Type.type_space tsig; |
154 val (class_space, class_algebra) = classes; |
140 val (class_space, class_algebra) = classes; |
155 val classes = Sorts.classes_of class_algebra; |
141 val classes = Sorts.classes_of class_algebra; |
156 val arities = Sorts.arities_of class_algebra; |
142 val arities = Sorts.arities_of class_algebra; |
157 |
|
158 val item_space = fn Defs.Constant => const_space | Defs.Type => type_space; |
|
159 fun extern_item (k, c) = (k, Name_Space.extern ctxt (item_space k) c); |
|
160 fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c; |
|
161 |
143 |
162 val clsses = |
144 val clsses = |
163 Name_Space.extern_entries verbose ctxt class_space |
145 Name_Space.extern_entries verbose ctxt class_space |
164 (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)) |
146 (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)) |
165 |> map (apfst #1); |
147 |> map (apfst #1); |
172 val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; |
154 val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts; |
173 val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; |
155 val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts; |
174 val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints; |
156 val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints; |
175 |
157 |
176 val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy); |
158 val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy); |
177 |
|
178 val (reds0, (reds1, reds2)) = filter_out (prune_item o fst o fst) reducts |
|
179 |> map (fn (lhs, rhs) => |
|
180 (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs))) |
|
181 |> sort_item_by (#1 o #1) |
|
182 |> List.partition (null o #2) |
|
183 ||> List.partition (Defs.plain_args o #2 o #1); |
|
184 val rests = restricts |> map (apfst (apfst extern_item)) |> sort_item_by (#1 o #1); |
|
185 in |
159 in |
186 [Pretty.strs ("names:" :: Context.display_names thy)] @ |
160 [Pretty.strs ("names:" :: Context.display_names thy)] @ |
187 [Pretty.big_list "classes:" (map pretty_classrel clsses), |
161 [Pretty.big_list "classes:" (map pretty_classrel clsses), |
188 pretty_default default, |
162 pretty_default default, |
189 Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), |
163 Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls), |
193 Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), |
167 Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs), |
194 Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), |
168 Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs), |
195 Pretty.big_list "axioms:" (map pretty_axm axms), |
169 Pretty.big_list "axioms:" (map pretty_axm axms), |
196 Pretty.block |
170 Pretty.block |
197 (Pretty.breaks (Pretty.str "oracles:" :: |
171 (Pretty.breaks (Pretty.str "oracles:" :: |
198 map Pretty.mark_str (Thm.extern_oracles verbose ctxt))), |
172 map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))] |
199 Pretty.big_list "definitions:" |
|
200 [pretty_finals reds0, |
|
201 Pretty.big_list "non-overloaded:" (map pretty_reduct reds1), |
|
202 Pretty.big_list "overloaded:" (map pretty_reduct reds2), |
|
203 Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]] |
|
204 end; |
173 end; |
205 |
174 |
206 end; |
175 end; |
207 |
176 |
208 structure Basic_Display: BASIC_DISPLAY = Display; |
177 structure Basic_Display: BASIC_DISPLAY = Display; |