--- a/FIXME-TODO Tue Dec 22 21:44:50 2009 +0100
+++ b/FIXME-TODO Tue Dec 22 22:10:48 2009 +0100
@@ -1,8 +1,30 @@
+Highest Priority
+================
+
+- better lookup mechanism for quotient definition
+ (see fixme in quotient_term.ML)
+
+- check needs to be fixed in mk_resp_arg (quotient_term.ML),
+ see test for (_, Const _)
+
+- clever code in quotiet_tacs.ML needs to be turned into
+ boring code
+
+- comment about regularize tactic eeds to be adapted
+
+- Check all the places where we do "handle _"
+ (They make code changes very difficult: I sat 1/2
+ a day over simplification of calculate_inst before
+ I understood things; the reason was that my exceptions
+ where caught by the catch all. There is no problem
+ with throwing and handling exceptions...it just must
+ be clear who throws what ad what is thrown.)
+
Higher Priority
===============
- if the constant definition gives the wrong definition
- term, one gets a cryptic message about get_fun
+ term, one gets a cryptic message about absrep_fun
- have FSet.thy to have a simple infrastructure for
finite sets (syntax should be \<lbrace> \<rbrace>,
@@ -15,7 +37,7 @@
- user should be able to give quotient_respects and
preserves theorems in a more natural form.
-- the test in the (_, Const _) needs to be fixed
+
Lower Priority
==============
@@ -24,7 +46,7 @@
a proof of the respectfulness (in this way one
already excludes non-sensical definitions)
-- accept partial equvalence relations
+- accept partial equivalence relations
- think about what happens if things go wrong (like
theorem cannot be lifted) / proper diagnostic
@@ -46,9 +68,6 @@
- add tests for adding theorems to the various thm lists
-
-- Check all the places where we do "handle _"
-
- We shouldn't use the command 'quotient' as this shadows Larry's quotient.
Call it 'quotient_type'
--- a/Quot/quotient_info.ML Tue Dec 22 21:44:50 2009 +0100
+++ b/Quot/quotient_info.ML Tue Dec 22 22:10:48 2009 +0100
@@ -90,12 +90,10 @@
let
fun prt_map (ty_name, {mapfun, relfun}) =
Pretty.block (Library.separate (Pretty.brk 2)
- [Pretty.str "type:",
- Pretty.str ty_name,
- Pretty.str "map fun:",
- Pretty.str mapfun,
- Pretty.str "relation map:",
- Pretty.str relfun])
+ (map Pretty.str
+ ["type:", ty_name,
+ "map fun:", mapfun,
+ "relation map:", relfun]))
in
MapsData.get (ProofContext.theory_of ctxt)
|> Symtab.dest
@@ -104,11 +102,7 @@
|> Pretty.writeln
end
-val _ =
- OuterSyntax.improper_command "print_maps" "prints out all map functions"
- OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of)))
-
-
+
(* info about quotient types *)
type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
@@ -152,10 +146,6 @@
|> Pretty.writeln
end
-val _ =
- OuterSyntax.improper_command "print_quotients" "prints out all quotients"
- OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
-
(* info about quotient constants *)
type qconsts_info = {qconst: term, rconst: term, def: thm}
@@ -212,10 +202,6 @@
|> Pretty.writeln
end
-val _ =
- OuterSyntax.improper_command "print_quotconsts" "prints out all quotient constants"
- OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
-
(* FIXME/TODO: check the various lemmas conform *)
(* with the required shape *)
@@ -257,6 +243,7 @@
val quotient_rules_add = QuotientRules.add
(* setup of the theorem lists *)
+
val _ = Context.>> (Context.map_theory
(EquivRules.setup #>
RspRules.setup #>
@@ -264,5 +251,18 @@
IdSimps.setup #>
QuotientRules.setup))
+
+(* setup of the printing commands *)
+
+fun improper_command (pp_fn, cmd_name, descr_str) =
+ OuterSyntax.improper_command cmd_name descr_str
+ OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
+
+val _ = map improper_command
+ [(print_mapsinfo, "print_maps", "prints out all map functions"),
+ (print_quotinfo, "print_quotients", "prints out all quotients"),
+ (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
+
+
end; (* structure *)