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 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

  type qenv = (typ * typ) list

  val mk_qenv: Proof.context -> qenv

  val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option

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 the quotient types *)

type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}

structure QuotData = Theory_Data

  (type T = quotient_info list

   val empty = []

   val extend = I

   val merge = (op @)) (* FIXME: is this the correct merging function for the list? *)

val quotdata_lookup_thy = QuotData.get

val quotdata_lookup = QuotData.get 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 (qty, rty, rel, equiv_thm) ctxt = 

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

  |> map prt_quot

  |> Pretty.big_list "quotients:" 

  |> Pretty.writeln

end

val _ = 

  OuterSyntax.improper_command "print_quotients" "print out all quotients" 

(* environments of quotient and raw types *)

type qenv = (typ * typ) list

fun mk_qenv ctxt =

let

  val qinfo = quotdata_lookup ctxt

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'

end; (* structure *)

open Quotient_Info