--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Quot/quotient_info.ML	Thu Feb 25 07:57:17 2010 +0100
@@ -0,0 +1,293 @@
+(*  Title:      quotient_info.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Data slots for the quotient package.
+
+*)
+
+
+signature QUOTIENT_INFO =
+sig
+  exception NotFound
+
+  type maps_info = {mapfun: string, relmap: string}
+  val maps_defined: theory -> string -> bool
+  val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
+  val maps_update_thy: string -> maps_info -> theory -> theory
+  val maps_update: string -> maps_info -> Proof.context -> Proof.context
+  val print_mapsinfo: Proof.context -> unit
+
+  type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+  val transform_quotdata: morphism -> quotdata_info -> quotdata_info
+  val quotdata_lookup_raw: theory -> string -> quotdata_info option
+  val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
+  val quotdata_update_thy: string -> quotdata_info -> theory -> theory
+  val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
+  val quotdata_dest: Proof.context -> quotdata_info list
+  val print_quotinfo: Proof.context -> unit
+
+  type qconsts_info = {qconst: term, rconst: term, def: thm}
+  val transform_qconsts: morphism -> qconsts_info -> qconsts_info
+  val qconsts_lookup: theory -> term -> qconsts_info     (* raises NotFound *)
+  val qconsts_update_thy: string -> qconsts_info -> theory -> theory
+  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic
+  val qconsts_dest: Proof.context -> qconsts_info list
+  val print_qconstinfo: Proof.context -> unit
+
+  val equiv_rules_get: Proof.context -> thm list
+  val equiv_rules_add: attribute
+  val rsp_rules_get: Proof.context -> thm list
+  val rsp_rules_add: attribute
+  val prs_rules_get: Proof.context -> thm list
+  val prs_rules_add: attribute
+  val id_simps_get: Proof.context -> thm list
+  val quotient_rules_get: Proof.context -> thm list
+  val quotient_rules_add: attribute
+end;
+
+
+structure Quotient_Info: QUOTIENT_INFO =
+struct
+
+exception NotFound
+
+
+(** data containers **)
+
+(* info about map- and rel-functions for a type *)
+type maps_info = {mapfun: string, relmap: string}
+
+structure MapsData = Theory_Data
+  (type T = maps_info Symtab.table
+   val empty = Symtab.empty
+   val extend = I
+   val merge = Symtab.merge (K true))
+
+fun maps_defined thy s =
+  Symtab.defined (MapsData.get thy) s
+
+fun maps_lookup thy s =
+  case (Symtab.lookup (MapsData.get thy) s) of
+    SOME map_fun => map_fun
+  | NONE => raise NotFound
+
+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 _ => 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
+
+  fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
+  val _ = List.app sanity_check [mapname, relname]
+in
+  maps_attribute_aux tyname {mapfun = mapname, relmap = 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"))
+
+fun print_mapsinfo ctxt =
+let
+  fun prt_map (ty_name, {mapfun, relmap}) =
+    Pretty.block (Library.separate (Pretty.brk 2)
+      (map Pretty.str
+        ["type:", ty_name,
+        "map:", mapfun,
+        "relation map:", relmap]))
+in
+  MapsData.get (ProofContext.theory_of ctxt)
+  |> Symtab.dest
+  |> map (prt_map)
+  |> Pretty.big_list "maps for type constructors:"
+  |> Pretty.writeln
+end
+
+
+(* info about quotient types *)
+type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+
+structure QuotData = Theory_Data
+  (type T = quotdata_info Symtab.table
+   val empty = Symtab.empty
+   val extend = I
+   val merge = Symtab.merge (K true))
+
+fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
+  {qtyp = Morphism.typ phi qtyp,
+   rtyp = Morphism.typ phi rtyp,
+   equiv_rel = Morphism.term phi equiv_rel,
+   equiv_thm = Morphism.thm phi equiv_thm}
+
+fun quotdata_lookup_raw thy str = Symtab.lookup (QuotData.get thy) str
+
+fun quotdata_lookup thy str =
+  case Symtab.lookup (QuotData.get thy) str of
+    SOME qinfo => qinfo
+  | NONE => raise NotFound
+
+fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
+fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
+
+fun quotdata_dest lthy =
+  map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
+
+fun print_quotinfo ctxt =
+let
+  fun prt_quot {qtyp, rtyp, equiv_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 equiv_rel,
+      Pretty.str "equiv. thm:",
+      Syntax.pretty_term ctxt (prop_of equiv_thm)])
+in
+  QuotData.get (ProofContext.theory_of ctxt)
+  |> Symtab.dest
+  |> map (prt_quot o snd)
+  |> Pretty.big_list "quotients:"
+  |> Pretty.writeln
+end
+
+
+(* 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 list) Symtab.table
+   val empty = Symtab.empty
+   val extend = I
+   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.cons_list (name, qcinfo))
+fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I
+
+fun qconsts_dest lthy =
+  flat (map snd (Symtab.dest (QConstsData.get (ProofContext.theory_of lthy))))
+
+fun qconsts_lookup thy t =
+  let
+    val (name, qty) = dest_Const t
+    fun matches x =
+      let
+        val (name', qty') = dest_Const (#qconst x);
+      in
+        name = name' andalso Sign.typ_instance thy (qty, qty')
+      end
+  in
+    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 =
+let
+  fun prt_qconst {qconst, rconst, def} =
+    Pretty.block (separate (Pretty.brk 1)
+     [Syntax.pretty_term ctxt qconst,
+      Pretty.str ":=",
+      Syntax.pretty_term ctxt rconst,
+      Pretty.str "as",
+      Syntax.pretty_term ctxt (prop_of def)])
+in
+  QConstsData.get (ProofContext.theory_of ctxt)
+  |> Symtab.dest
+  |> map snd
+  |> flat
+  |> map prt_qconst
+  |> Pretty.big_list "quotient constants:"
+  |> Pretty.writeln
+end
+
+(* equivalence relation theorems *)
+structure EquivRules = Named_Thms
+  (val name = "quot_equiv"
+   val description = "Equivalence relation theorems.")
+
+val equiv_rules_get = EquivRules.get
+val equiv_rules_add = EquivRules.add
+
+(* respectfulness theorems *)
+structure RspRules = Named_Thms
+  (val name = "quot_respect"
+   val description = "Respectfulness theorems.")
+
+val rsp_rules_get = RspRules.get
+val rsp_rules_add = RspRules.add
+
+(* preservation theorems *)
+structure PrsRules = Named_Thms
+  (val name = "quot_preserve"
+   val description = "Preservation theorems.")
+
+val prs_rules_get = PrsRules.get
+val prs_rules_add = PrsRules.add
+
+(* id simplification theorems *)
+structure IdSimps = Named_Thms
+  (val name = "id_simps"
+   val description = "Identity simp rules for maps.")
+
+val id_simps_get = IdSimps.get
+
+(* quotient theorems *)
+structure QuotientRules = Named_Thms
+  (val name = "quot_thm"
+   val description = "Quotient theorems.")
+
+val quotient_rules_get = QuotientRules.get
+val quotient_rules_add = QuotientRules.add
+
+(* setup of the theorem lists *)
+
+val _ = Context.>> (Context.map_theory
+  (EquivRules.setup #>
+   RspRules.setup #>
+   PrsRules.setup #>
+   IdSimps.setup #>
+   QuotientRules.setup))
+
+(* setup of the printing commands *)
+
+fun improper_command (pp_fn, cmd_name, descr_str) =
+  OuterSyntax.improper_command cmd_name descr_str
+    OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
+
+val _ = map improper_command
+  [(print_mapsinfo, "print_maps", "prints out all map functions"),
+   (print_quotinfo, "print_quotients", "prints out all quotients"),
+   (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]
+
+
+end; (* structure *)
+