(*  Title:      HOL/Tools/Quotient/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

   fun merge data = Symtab.merge (K true) data)

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

   fun merge data = Symtab.merge (K true) data)

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: qconsts_info) =

      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_quotmaps", "prints out all map functions"),

   (print_quotinfo, "print_quotients", "prints out all quotients"),

   (print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]

end; (* structure *)