88 |
88 |
89 fun print_mapsinfo ctxt = |
89 fun print_mapsinfo ctxt = |
90 let |
90 let |
91 fun prt_map (ty_name, {mapfun, relfun}) = |
91 fun prt_map (ty_name, {mapfun, relfun}) = |
92 Pretty.block (Library.separate (Pretty.brk 2) |
92 Pretty.block (Library.separate (Pretty.brk 2) |
93 [Pretty.str "type:", |
93 (map Pretty.str |
94 Pretty.str ty_name, |
94 ["type:", ty_name, |
95 Pretty.str "map fun:", |
95 "map fun:", mapfun, |
96 Pretty.str mapfun, |
96 "relation map:", relfun])) |
97 Pretty.str "relation map:", |
|
98 Pretty.str relfun]) |
|
99 in |
97 in |
100 MapsData.get (ProofContext.theory_of ctxt) |
98 MapsData.get (ProofContext.theory_of ctxt) |
101 |> Symtab.dest |
99 |> Symtab.dest |
102 |> map (prt_map) |
100 |> map (prt_map) |
103 |> Pretty.big_list "maps:" |
101 |> Pretty.big_list "maps:" |
104 |> Pretty.writeln |
102 |> Pretty.writeln |
105 end |
103 end |
106 |
104 |
107 val _ = |
105 |
108 OuterSyntax.improper_command "print_maps" "prints out all map functions" |
|
109 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of))) |
|
110 |
|
111 |
|
112 (* info about quotient types *) |
106 (* info about quotient types *) |
113 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
107 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
114 |
108 |
115 structure QuotData = Theory_Data |
109 structure QuotData = Theory_Data |
116 (type T = quotient_info Symtab.table |
110 (type T = quotient_info Symtab.table |
149 |> Symtab.dest |
143 |> Symtab.dest |
150 |> map (prt_quot o snd) |
144 |> map (prt_quot o snd) |
151 |> Pretty.big_list "quotients:" |
145 |> Pretty.big_list "quotients:" |
152 |> Pretty.writeln |
146 |> Pretty.writeln |
153 end |
147 end |
154 |
|
155 val _ = |
|
156 OuterSyntax.improper_command "print_quotients" "prints out all quotients" |
|
157 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
|
158 |
148 |
159 |
149 |
160 (* info about quotient constants *) |
150 (* info about quotient constants *) |
161 type qconsts_info = {qconst: term, rconst: term, def: thm} |
151 type qconsts_info = {qconst: term, rconst: term, def: thm} |
162 |
152 |
210 |> map (prt_qconst o snd) |
200 |> map (prt_qconst o snd) |
211 |> Pretty.big_list "quotient constants:" |
201 |> Pretty.big_list "quotient constants:" |
212 |> Pretty.writeln |
202 |> Pretty.writeln |
213 end |
203 end |
214 |
204 |
215 val _ = |
|
216 OuterSyntax.improper_command "print_quotconsts" "prints out all quotient constants" |
|
217 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of))) |
|
218 |
|
219 (* FIXME/TODO: check the various lemmas conform *) |
205 (* FIXME/TODO: check the various lemmas conform *) |
220 (* with the required shape *) |
206 (* with the required shape *) |
221 |
207 |
222 (* equivalence relation theorems *) |
208 (* equivalence relation theorems *) |
223 structure EquivRules = Named_Thms |
209 structure EquivRules = Named_Thms |
255 |
241 |
256 val quotient_rules_get = QuotientRules.get |
242 val quotient_rules_get = QuotientRules.get |
257 val quotient_rules_add = QuotientRules.add |
243 val quotient_rules_add = QuotientRules.add |
258 |
244 |
259 (* setup of the theorem lists *) |
245 (* setup of the theorem lists *) |
|
246 |
260 val _ = Context.>> (Context.map_theory |
247 val _ = Context.>> (Context.map_theory |
261 (EquivRules.setup #> |
248 (EquivRules.setup #> |
262 RspRules.setup #> |
249 RspRules.setup #> |
263 PrsRules.setup #> |
250 PrsRules.setup #> |
264 IdSimps.setup #> |
251 IdSimps.setup #> |
265 QuotientRules.setup)) |
252 QuotientRules.setup)) |
266 |
253 |
|
254 |
|
255 (* setup of the printing commands *) |
|
256 |
|
257 fun improper_command (pp_fn, cmd_name, descr_str) = |
|
258 OuterSyntax.improper_command cmd_name descr_str |
|
259 OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of))) |
|
260 |
|
261 val _ = map improper_command |
|
262 [(print_mapsinfo, "print_maps", "prints out all map functions"), |
|
263 (print_quotinfo, "print_quotients", "prints out all quotients"), |
|
264 (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")] |
|
265 |
|
266 |
267 end; (* structure *) |
267 end; (* structure *) |
268 |
268 |