signature QUOTIENT_INFO =

sig

  exception NotFound

  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

  val quotdata_dest: theory -> quotient_info list

  type qconsts_info = {qconst: term, rconst: term, def: thm}

  val qconsts_transfer: morphism -> qconsts_info -> qconsts_info

  val qconsts_lookup: theory -> term -> qconsts_info

  val qconsts_update_thy: string -> qconsts_info -> theory -> theory

  val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic

  val qconsts_dest: theory -> 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 prs_rules_get: Proof.context -> thm list  

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

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 quotdata_dest thy =

    map snd (Symtab.dest (QuotData.get thy))

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

(* info about quotient constants *)

type qconsts_info = {qconst: term, rconst: term, def: thm}

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, def} =

    {qconst = Morphism.term phi qconst,

     rconst = Morphism.term phi rconst,

     def = Morphism.thm phi def}

fun qconsts_update_thy id qcinfo = QConstsData.map (Symtab.update (id, qcinfo))

fun qconsts_update_gen id qcinfo = Context.mapping (qconsts_update_thy id qcinfo) I

fun qconsts_dest thy =

  map snd (Symtab.dest (QConstsData.get thy))

fun qconsts_lookup thy t =

  let

    val smt = Symtab.dest (QConstsData.get thy);

    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 (find_first matches smt) of

      SOME (_, x) => x

    | _ => raise NotFound

  end

(* We don't print the definition *)

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

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

(* FIXME/TODO: check the various lemmas conform *)

(* with the required shape                      *)

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

(* preservation theorems *)

structure PrsRules = Named_Thms

  (val name = "quot_preserve"

   val description = "Respectfulness theorems.")

val prs_rules_get = PrsRules.get

(* respectfulness 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))

end; (* structure *)

open Quotient_Info