# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1257990880 -3600
# Node ID 77fc6f3c0343af306c58c318309cb0e7759ec3c6
# Parent  fec6301a19899e86f69f9f4f0912fe2da31dd591
changed the quotdata to be a symtab table (needs fixing)

diff -r fec6301a1989 -r 77fc6f3c0343 QuotMain.thy
--- a/QuotMain.thy	Thu Nov 12 02:18:36 2009 +0100
+++ b/QuotMain.thy	Thu Nov 12 02:54:40 2009 +0100
@@ -1032,7 +1032,9 @@
   let
     fun matches (ty1, ty2) =
       Type.raw_instance (ty1, Logic.varifyT ty2);
-    val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
+    val qty_name = fst (dest_Type qty)
+    val SOME quotdata = quotdata_lookup lthy qty_name 
+                  (* cu: Changed the lookup\<dots>not sure whether this works *)
     (* TODO: Should no longer be needed *)
     val rty = Logic.unvarifyT (#rtyp quotdata)
     val rel = #rel quotdata
diff -r fec6301a1989 -r 77fc6f3c0343 quotient.ML
--- a/quotient.ML	Thu Nov 12 02:18:36 2009 +0100
+++ b/quotient.ML	Thu Nov 12 02:54:40 2009 +0100
@@ -146,7 +146,8 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val lthy3 = quotdata_update (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
+  val lthy3 = quotdata_update (Binding.str_of qty_name) 
+                                (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
diff -r fec6301a1989 -r 77fc6f3c0343 quotient_info.ML
--- a/quotient_info.ML	Thu Nov 12 02:18:36 2009 +0100
+++ b/quotient_info.ML	Thu Nov 12 02:54:40 2009 +0100
@@ -7,10 +7,10 @@
 
   type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
   val print_quotinfo: 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
+  val quotdata_lookup_thy: theory -> string -> quotient_info option
+  val quotdata_lookup: Proof.context -> string -> quotient_info option
+  val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
+  val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
 
   type qenv = (typ * typ) list
   val mk_qenv: Proof.context -> qenv
@@ -41,7 +41,6 @@
 
 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)
 
@@ -74,19 +73,19 @@
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
 structure QuotData = Theory_Data
-  (type T = quotient_info list
-   val empty = []
+  (type T = quotient_info Symtab.table
+   val empty = Symtab.empty
    val extend = I
-   val merge = (op @)) (* FIXME: is this the correct merging function for the list? *)
+   val merge = Symtab.merge (K true)) 
 
-val quotdata_lookup_thy = QuotData.get
-val quotdata_lookup = QuotData.get o ProofContext.theory_of
+val quotdata_lookup_thy = Symtab.lookup o QuotData.get
+val quotdata_lookup = quotdata_lookup_thy 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_thy qty_name (qty, rty, rel, equiv_thm) = 
+      QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}))
 
-fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = 
-      ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt
+fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 
+      ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
 
 fun print_quotinfo ctxt =
 let
@@ -102,7 +101,8 @@
            Syntax.pretty_term ctxt (prop_of equiv_thm)])
 in
   QuotData.get (ProofContext.theory_of ctxt)
-  |> map prt_quot
+  |> Symtab.dest
+  |> map (prt_quot o snd)
   |> Pretty.big_list "quotients:" 
   |> Pretty.writeln
 end
@@ -117,7 +117,8 @@
 
 fun mk_qenv ctxt =
 let
-  val qinfo = quotdata_lookup ctxt
+  val thy = ProofContext.theory_of ctxt
+  val qinfo = (QuotData.get thy) |> Symtab.dest |> map snd
 in
   map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo
 end