signature QUOTIENT_INFO =
sig
  type maps_info = {mapfun: string, relfun: string}
  val maps_lookup: theory -> string -> maps_info option
  val maps_update_thy: string -> maps_info -> theory -> theory    
  val maps_update: string -> maps_info -> Proof.context -> Proof.context     

  type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
  val print_quotinfo: Proof.context -> unit
  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

  (*FIXME: obsolete *)
  type qenv = (typ * typ) list
  val mk_qenv: Proof.context -> qenv
  val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option

  type qconsts_info = {qconst: term, rconst: term}
  val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
  val qconsts_lookup: theory -> string -> qconsts_info option
  val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic 
  val print_qconstinfo: Proof.context -> unit
end;

structure Quotient_Info: QUOTIENT_INFO =
struct


(* data containers *)
(*******************)

(* info about map- and rel-functions *)
type maps_info = {mapfun: string, relfun: string}

structure MapsData = Theory_Data
  (type T = maps_info Symtab.table
   val empty = Symtab.empty
   val extend = I
   val merge = Symtab.merge (K true))

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)

fun maps_attribute_aux s minfo = Thm.declaration_attribute 
  (fn thm => 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
in
  maps_attribute_aux tyname {mapfun = mapname, relfun = 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"))


(* info about quotient types *)
type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}

structure QuotData = Theory_Data
  (type T = quotient_info Symtab.table
   val empty = Symtab.empty
   val extend = I
   val merge = Symtab.merge (K true)) 

fun quotdata_lookup_thy thy str = 
    Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str)

val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of

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_name (qty, rty, rel, equiv_thm) = 
      ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))

fun print_quotinfo ctxt =
let
  fun prt_quot {qtyp, rtyp, 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 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

val _ = 
  OuterSyntax.improper_command "print_quotients" "print out all quotients" 
    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))


(* FIXME: obsolete: environments for quotient and raw types *)
type qenv = (typ * typ) list

fun mk_qenv ctxt =
let
  val thy = ProofContext.theory_of ctxt
  val qinfo = (QuotData.get thy) |> Symtab.dest |> map snd
in
  map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) qinfo
end

fun lookup_qenv _ [] _ = NONE
  | lookup_qenv eq ((qty, rty)::xs) qty' =
      if eq (qty', qty) then SOME (qty, rty)
      else lookup_qenv eq xs qty'

(* information about quotient constants *)
type qconsts_info = {qconst: term, rconst: term}

structure QConstsData = Theory_Data
  (type T = qconsts_info Symtab.table
   val empty = Symtab.empty
   val extend = I
   val merge = Symtab.merge (K true))

fun qconsts_transfer phi {qconst, rconst} =
    {qconst = Morphism.term phi qconst,
     rconst = Morphism.term phi rconst}

val qconsts_lookup = Symtab.lookup o QConstsData.get

fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I

fun print_qconstinfo ctxt =
let
  fun prt_qconst {qconst, rconst} = 
      Pretty.block (separate (Pretty.brk 1)
          [Syntax.pretty_term ctxt qconst,
           Pretty.str ":=",
           Syntax.pretty_term ctxt rconst])
in
  QConstsData.get (ProofContext.theory_of ctxt)
  |> Symtab.dest
  |> map (prt_qconst o snd)
  |> Pretty.big_list "quotient constants:" 
  |> Pretty.writeln
end

val _ = 
  OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))

end; (* structure *)

open Quotient_Info