--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/quotient_info.ML	Tue Nov 03 14:04:45 2009 +0100
@@ -0,0 +1,107 @@
+signature QUOTIENT_INFO =
+sig
+  type maps_info = {mapfun: string, relfun: string}
+  val maps_lookup: theory -> string -> maps_info option
+  val maps_update_thy: string -> maps_info -> theory -> theory    
+  val maps_update: string -> maps_info -> Proof.context -> Proof.context     
+
+  type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
+  val print_quotdata: Proof.context -> unit
+  val quotdata_lookup_thy: theory -> quotient_info list
+  val quotdata_lookup: Proof.context -> quotient_info list
+  val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory
+  val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context
+end;
+
+structure Quotient_Info: QUOTIENT_INFO =
+struct
+
+(* data containers *)
+(*******************)
+
+(* info about map- and rel-functions *)
+type maps_info = {mapfun: string, relfun: string}
+
+structure MapsData = TheoryDataFun
+  (type T = maps_info Symtab.table
+   val empty = Symtab.empty
+   val copy = I
+   val extend = I
+   fun merge _ = Symtab.merge (K true))
+
+val maps_lookup = Symtab.lookup o MapsData.get
+
+
+fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
+fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
+
+fun maps_attribute_aux s minfo = Thm.declaration_attribute 
+  (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
+
+(* attribute to be used in declare statements *)
+fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = 
+let  
+  val thy = ProofContext.theory_of ctxt
+  val tyname = Sign.intern_type thy tystr
+  val mapname = Sign.intern_const thy mapstr
+  val relname = Sign.intern_const thy relstr
+in
+  maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
+end
+
+val maps_attr_parser = 
+      Args.context -- Scan.lift
+       ((Args.name --| OuterParse.$$$ "=") -- 
+         (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- 
+           Args.name --| OuterParse.$$$ ")"))
+
+val _ = Context.>> (Context.map_theory
+         (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
+           "declaration of map information"))
+
+
+(* info about the quotient types *)
+type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
+
+structure QuotData = TheoryDataFun
+  (type T = quotient_info list
+   val empty = []
+   val copy = I
+   val extend = I
+   fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *)
+
+val quotdata_lookup_thy = QuotData.get
+val quotdata_lookup = QuotData.get o ProofContext.theory_of
+
+fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = 
+      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy
+
+fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = 
+      ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt
+
+fun print_quotdata ctxt =
+let
+  fun prt_quot {qtyp, rtyp, rel, equiv_thm} = 
+      Pretty.block (Library.separate (Pretty.brk 2)
+          [Pretty.str ("quotient type:"), 
+           Syntax.pretty_typ ctxt qtyp,
+           Pretty.str ("raw type:"), 
+           Syntax.pretty_typ ctxt rtyp,
+           Pretty.str ("relation:"), 
+           Syntax.pretty_term ctxt rel,
+           Pretty.str ("equiv. thm:"), 
+           Syntax.pretty_term ctxt (prop_of equiv_thm)])
+in
+  QuotData.get (ProofContext.theory_of ctxt)
+  |> map prt_quot
+  |> Pretty.big_list "quotients:" 
+  |> Pretty.writeln
+end
+
+val _ = 
+  OuterSyntax.improper_command "print_quotients" "print out all quotients" 
+    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of)))
+
+end; (* structure *)
+
+open Quotient_Info
\ No newline at end of file