# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256060782 -7200
# Node ID 6f0d14ba096c742062998561513d9d6a0f80b354
# Parent  72d003e823491b1d8abcca5a76fc5da647ec497f
started to write code for storing data about the quotients

diff -r 72d003e82349 -r 6f0d14ba096c quotient.ML
--- a/quotient.ML	Tue Oct 20 09:37:22 2009 +0200
+++ b/quotient.ML	Tue Oct 20 19:46:22 2009 +0200
@@ -16,21 +16,74 @@
 (* data containers *)
 (*******************)
 
-(* map-functions and rel-functions *)
+(* info about map- and rel-functions *)
 type maps_info = {mapfun: string, relfun: string}
 
-local
-  structure Data = TheoryDataFun
+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 k v = MapsData.map (Symtab.update (k, v))
+
+
+
+(* info about the quotient types *)
+type quotient_info = {qtyp: typ, rtyp: typ, rel: term}
+
+structure QuotData = TheoryDataFun
+  (type T = quotient_info list
+   val empty = []
+   val copy = I
+   val extend = I
+   fun merge _ = (op @))
+
+val quotdata_lookup = QuotData.get
+fun quotdata_update (qty, rty, rel) = 
+      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls)
+
+fun print_quotdata ctxt =
+let
+  val quots = QuotData.get (Context.theory_of_proof ctxt)
+  fun prt_quot {qtyp, rtyp, rel} = Pretty.block
+      [Pretty.str ("quotient:"), 
+       Pretty.brk 2, 
+       Syntax.pretty_typ ctxt qtyp,
+       Pretty.brk 2, 
+       Syntax.pretty_typ ctxt rtyp,
+       Pretty.brk 2, 
+       Syntax.pretty_term ctxt rel]
 in
-  val maps_lookup = Symtab.lookup o Data.get
-  fun maps_update k v = Data.map (Symtab.update (k, v))
+  [Pretty.big_list "quotients:" (map prt_quot quots)]
+  |> Pretty.chunks |> Pretty.writeln
 end
 
+val _ = 
+  OuterSyntax.improper_command "print_quotients" "print quotient types of this theory" 
+    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of)))
+
+
+
+(* wrappers for define and note *)
+fun define (name, mx, rhs) lthy =
+let
+  val ((rhs, (_ , thm)), lthy') =
+     LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy
+in
+  ((rhs, thm), lthy')
+end
+
+fun note (name, thm) lthy =
+let
+  val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
+in
+  (thm', lthy')
+end
+
+
 
 (* definition of the quotient type *)
 (***********************************)
@@ -110,22 +163,6 @@
     (K typedef_quotient_thm_tac)
 end
 
-(* two wrappers for define and note *)
-fun define (name, mx, rhs) lthy =
-let
-  val ((rhs, (_ , thm)), lthy') =
-     LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy
-in
-  ((rhs, thm), lthy')
-end
-
-fun note (name, thm) lthy =
-let
-  val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
-in
-  (thm', lthy')
-end
-
 (* main function for constructing the quotient type *)
 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy =
 let
@@ -209,7 +246,7 @@
 let
   fun get_goal (rty, rel) =
   let
-    val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+      val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   in 
     (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), [])
   end
@@ -217,11 +254,7 @@
   val goals = map (get_goal o snd) quot_list
               
   fun after_qed thms lthy =
-  let
-    val thms' = flat thms
-  in
-    fold_map mk_typedef_main (quot_list ~~ thms') lthy |> snd
-  end
+    fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd
 in
   Proof.theorem_i NONE after_qed [goals] lthy
 end