# HG changeset patch
# User bulwahn
# Date 1321536932 -3600
# Node ID 4ab21521b393eb26f282a168d86ee843712f09a3
# Parent  af3690f6bd799f17cdb63c25cf694303a3b4ac34
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition

diff -r af3690f6bd79 -r 4ab21521b393 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Nov 17 06:04:59 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Nov 17 14:35:32 2011 +0100
@@ -11,6 +11,13 @@
   val lookup_quotmaps_global: theory -> string -> quotmaps option
   val print_quotmaps: Proof.context -> unit
 
+  type abs_rep = {abs : term, rep : term}
+  val transform_abs_rep: morphism -> abs_rep -> abs_rep
+  val lookup_abs_rep: Proof.context -> string -> abs_rep option
+  val lookup_abs_rep_global: theory -> string -> abs_rep option
+  val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
+  val print_abs_rep: Proof.context -> unit
+  
   type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
   val transform_quotients: morphism -> quotients -> quotients
   val lookup_quotients: Proof.context -> string -> quotients option
@@ -86,6 +93,39 @@
     |> Pretty.writeln
   end
 
+(* info about abs/rep terms *)
+type abs_rep = {abs : term, rep : term}
+
+structure Abs_Rep = Generic_Data
+(
+  type T = abs_rep Symtab.table
+  val empty = Symtab.empty
+  val extend = I
+  fun merge data = Symtab.merge (K true) data
+)
+
+fun transform_abs_rep phi {abs, rep} = {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
+
+val lookup_abs_rep = Symtab.lookup o Abs_Rep.get o Context.Proof
+val lookup_abs_rep_global = Symtab.lookup o Abs_Rep.get o Context.Theory
+
+fun update_abs_rep str data = Abs_Rep.map (Symtab.update (str, data))
+
+fun print_abs_rep ctxt =
+  let
+    fun prt_abs_rep (s, {abs, rep}) =
+      Pretty.block (separate (Pretty.brk 2)
+       [Pretty.str "type constructor:",
+        Pretty.str s,
+        Pretty.str "abs term:",
+        Syntax.pretty_term ctxt abs,
+        Pretty.str "rep term:",
+        Syntax.pretty_term ctxt rep])
+  in
+    map prt_abs_rep (Symtab.dest (Abs_Rep.get (Context.Proof ctxt)))
+    |> Pretty.big_list "abs/rep terms:"
+    |> Pretty.writeln
+  end
 
 (* info about quotient types *)
 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
diff -r af3690f6bd79 -r 4ab21521b393 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Nov 17 06:04:59 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Nov 17 14:35:32 2011 +0100
@@ -123,14 +123,18 @@
 (* produces the rep or abs constant for a qty *)
 fun absrep_const flag ctxt qty_str =
   let
-    val qty_name = Long_Name.base_name qty_str
-    val qualifier = Long_Name.qualifier qty_str
+    (* FIXME *)
+    fun mk_dummyT (Const (c, _)) = Const (c, dummyT)
+      | mk_dummyT _ = error "Expecting abs/rep term to be a constant"     
   in
-    case flag of
-      AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
-    | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
+    case Quotient_Info.lookup_abs_rep ctxt qty_str of
+      SOME abs_rep => 
+        mk_dummyT (case flag of
+          AbsF => #abs abs_rep
+        | RepF => #rep abs_rep)
+      | NONE => error ("No abs/rep terms for " ^ quote qty_str)
   end
-
+  
 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
 fun absrep_const_chk flag ctxt qty_str =
   Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
diff -r af3690f6bd79 -r 4ab21521b393 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Nov 17 06:04:59 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Nov 17 14:35:32 2011 +0100
@@ -116,9 +116,9 @@
     val abs_name = Binding.prefix_name "abs_" qty_name
     val rep_name = Binding.prefix_name "rep_" qty_name
 
-    val ((_, (_, abs_def)), lthy2) = lthy1
+    val ((abs_t, (_, abs_def)), lthy2) = lthy1
       |> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm))
-    val ((_, (_, rep_def)), lthy3) = lthy2
+    val ((rep_t, (_, rep_def)), lthy3) = lthy2
       |> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm))
 
     (* quot_type theorem *)
@@ -137,10 +137,12 @@
     val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
 
     fun qinfo phi = Quotient_Info.transform_quotients phi quotients
+    fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
 
     val lthy4 = lthy3
       |> Local_Theory.declaration {syntax = false, pervasive = true}
-        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
+        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
+           #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
       |> (snd oo Local_Theory.note)
         ((equiv_thm_name,
           if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),