# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263459989 -3600
# Node ID ce5f78f0eac5d2715a59a759def6ba9ad793f41f
# Parent  09d5b7f0e55da818e85a42144d09c08a9e1a50a5
Finished organising an efficient datastructure for qconst_info.

diff -r 09d5b7f0e55d -r ce5f78f0eac5 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Jan 14 08:02:20 2010 +0100
+++ b/Quot/QuotMain.thy	Thu Jan 14 10:06:29 2010 +0100
@@ -95,6 +95,7 @@
 section {* ML setup *}
 
 (* Auxiliary data for the quotient package *)
+
 use "quotient_info.ML"
 
 declare [[map "fun" = (fun_map, fun_rel)]]
diff -r 09d5b7f0e55d -r ce5f78f0eac5 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Thu Jan 14 08:02:20 2010 +0100
+++ b/Quot/quotient_def.ML	Thu Jan 14 10:06:29 2010 +0100
@@ -51,8 +51,9 @@
 
   (* data storage *)
   fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
+  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
   val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
+                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
 in
   ((trm, thm), lthy'')
 end
diff -r 09d5b7f0e55d -r ce5f78f0eac5 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Jan 14 08:02:20 2010 +0100
+++ b/Quot/quotient_info.ML	Thu Jan 14 10:06:29 2010 +0100
@@ -179,42 +179,45 @@
 (* info about quotient constants *)
 type qconsts_info = {qconst: term, rconst: term, def: thm}
 
+fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y
+
 (* We need to be able to lookup instances of lifted constants,
    for example given "nat fset" we need to find "'a fset";
    but overloaded constants share the same name *)
 structure QConstsData = Theory_Data
-  (type T = qconsts_info Symtab.table
+  (type T = (qconsts_info list) Symtab.table
    val empty = Symtab.empty
    val extend = I
-   val merge = Symtab.merge (K true))
+   val merge = Symtab.merge_list qconsts_info_eq)
 
 fun transform_qconsts phi {qconst, rconst, def} =
     {qconst = Morphism.term phi qconst,
      rconst = Morphism.term phi rconst,
      def = Morphism.thm phi def}
 
-fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.update (name, qcinfo))
+fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo))
 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I
 
 fun qconsts_dest thy =
-  map snd (Symtab.dest (QConstsData.get thy))
+  flat (map snd (Symtab.dest (QConstsData.get thy)))
 
-(* FIXME / TODO : better implementation of the lookup datastructure *)
-(* for example symtabs to alist; or tables with string type key     *) 
 fun qconsts_lookup thy t =
   let
-    val smt = Symtab.dest (QConstsData.get thy);
     val (name, qty) = dest_Const t
-    fun matches (_, x) =
+    fun matches x =
       let
         val (name', qty') = dest_Const (#qconst x);
       in
         name = name' andalso Sign.typ_instance thy (qty, qty')
       end
   in
-    case (find_first matches smt) of
-      SOME (_, x) => x
-    | _ => raise NotFound
+    case Symtab.lookup (QConstsData.get thy) name of
+      NONE => raise NotFound
+    | SOME l =>
+      (case (find_first matches l) of
+        SOME x => x
+      | NONE => raise NotFound
+      )
   end
 
 fun print_qconstinfo ctxt =
@@ -229,7 +232,9 @@
 in
   QConstsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
-  |> map (prt_qconst o snd)
+  |> map snd
+  |> flat
+  |> map prt_qconst
   |> Pretty.big_list "quotient constants:" 
   |> Pretty.writeln
 end