haftmann@37743: (*  Title:      HOL/Tools/Quotient/quotient_info.ML
kaliszyk@35222:     Author:     Cezary Kaliszyk and Christian Urban
kaliszyk@35222: 
wenzelm@46150: Context data for the quotient package.
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@35222: signature QUOTIENT_INFO =
kaliszyk@35222: sig
kuncar@46673:   type quotmaps = {relmap: string}
wenzelm@46151:   val lookup_quotmaps: Proof.context -> string -> quotmaps option
wenzelm@46211:   val lookup_quotmaps_global: theory -> string -> quotmaps option
wenzelm@46150:   val print_quotmaps: Proof.context -> unit
kaliszyk@35222: 
bulwahn@46405:   type abs_rep = {abs : term, rep : term}
bulwahn@46405:   val transform_abs_rep: morphism -> abs_rep -> abs_rep
bulwahn@46405:   val lookup_abs_rep: Proof.context -> string -> abs_rep option
bulwahn@46405:   val lookup_abs_rep_global: theory -> string -> abs_rep option
bulwahn@46405:   val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
bulwahn@46405:   val print_abs_rep: Proof.context -> unit
bulwahn@46405:   
wenzelm@46150:   type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
wenzelm@46150:   val transform_quotients: morphism -> quotients -> quotients
wenzelm@46151:   val lookup_quotients: Proof.context -> string -> quotients option
wenzelm@46211:   val lookup_quotients_global: theory -> string -> quotients option
wenzelm@46150:   val update_quotients: string -> quotients -> Context.generic -> Context.generic
wenzelm@46150:   val dest_quotients: Proof.context -> quotients list
wenzelm@46150:   val print_quotients: Proof.context -> unit
kaliszyk@35222: 
wenzelm@46150:   type quotconsts = {qconst: term, rconst: term, def: thm}
wenzelm@46150:   val transform_quotconsts: morphism -> quotconsts -> quotconsts
wenzelm@46211:   val lookup_quotconsts_global: theory -> term -> quotconsts option
wenzelm@46150:   val update_quotconsts: string -> quotconsts -> Context.generic -> Context.generic
urbanc@46215:   val dest_quotconsts_global: theory -> quotconsts list
wenzelm@46150:   val dest_quotconsts: Proof.context -> quotconsts list
wenzelm@46150:   val print_quotconsts: Proof.context -> unit
kaliszyk@35222: 
wenzelm@46150:   val equiv_rules: Proof.context -> thm list
kaliszyk@35222:   val equiv_rules_add: attribute
wenzelm@46150:   val rsp_rules: Proof.context -> thm list
kaliszyk@35314:   val rsp_rules_add: attribute
wenzelm@46150:   val prs_rules: Proof.context -> thm list
kaliszyk@35314:   val prs_rules_add: attribute
wenzelm@46150:   val id_simps: Proof.context -> thm list
wenzelm@46150:   val quotient_rules: Proof.context -> thm list
kaliszyk@35222:   val quotient_rules_add: attribute
wenzelm@41708:   val setup: theory -> theory
kaliszyk@35222: end;
kaliszyk@35222: 
kaliszyk@35222: structure Quotient_Info: QUOTIENT_INFO =
kaliszyk@35222: struct
kaliszyk@35222: 
kaliszyk@35222: (** data containers **)
kaliszyk@35222: 
wenzelm@41720: (* FIXME just one data slot (record) per program unit *)
wenzelm@41720: 
kaliszyk@35222: (* info about map- and rel-functions for a type *)
kuncar@46673: type quotmaps = {relmap: string}
kaliszyk@35222: 
wenzelm@46151: structure Quotmaps = Generic_Data
wenzelm@39034: (
wenzelm@46150:   type T = quotmaps Symtab.table
wenzelm@39034:   val empty = Symtab.empty
wenzelm@39034:   val extend = I
wenzelm@39034:   fun merge data = Symtab.merge (K true) data
wenzelm@39034: )
kaliszyk@35222: 
wenzelm@46151: val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
wenzelm@46211: val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory
kaliszyk@35222: 
wenzelm@46152: (* FIXME export proper internal update operation!? *)
kaliszyk@35222: 
wenzelm@46152: val quotmaps_attribute_setup =
wenzelm@46152:   Attrib.setup @{binding map}
wenzelm@47823:     ((Args.type_name false --| Scan.lift (@{keyword "="})) --  (* FIXME Args.type_name true (requires "set" type) *)
kuncar@46673:       Args.const_proper true >>
kuncar@46673:       (fn (tyname, relname) =>
kuncar@46673:         let val minfo = {relmap = relname}
wenzelm@46152:         in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
wenzelm@46152:     "declaration of map information"
kaliszyk@35222: 
wenzelm@46150: fun print_quotmaps ctxt =
wenzelm@41700:   let
kuncar@46673:     fun prt_map (ty_name, {relmap}) =
wenzelm@41701:       Pretty.block (separate (Pretty.brk 2)
wenzelm@41700:         (map Pretty.str
wenzelm@41701:          ["type:", ty_name,
wenzelm@41700:           "relation map:", relmap]))
wenzelm@41700:   in
wenzelm@46151:     map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
wenzelm@41700:     |> Pretty.big_list "maps for type constructors:"
wenzelm@41700:     |> Pretty.writeln
wenzelm@41700:   end
kaliszyk@35222: 
bulwahn@46405: (* info about abs/rep terms *)
bulwahn@46405: type abs_rep = {abs : term, rep : term}
bulwahn@46405: 
bulwahn@46405: structure Abs_Rep = Generic_Data
bulwahn@46405: (
bulwahn@46405:   type T = abs_rep Symtab.table
bulwahn@46405:   val empty = Symtab.empty
bulwahn@46405:   val extend = I
bulwahn@46405:   fun merge data = Symtab.merge (K true) data
bulwahn@46405: )
bulwahn@46405: 
bulwahn@46405: fun transform_abs_rep phi {abs, rep} = {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
bulwahn@46405: 
bulwahn@46405: val lookup_abs_rep = Symtab.lookup o Abs_Rep.get o Context.Proof
bulwahn@46405: val lookup_abs_rep_global = Symtab.lookup o Abs_Rep.get o Context.Theory
bulwahn@46405: 
bulwahn@46405: fun update_abs_rep str data = Abs_Rep.map (Symtab.update (str, data))
bulwahn@46405: 
bulwahn@46405: fun print_abs_rep ctxt =
bulwahn@46405:   let
bulwahn@46405:     fun prt_abs_rep (s, {abs, rep}) =
bulwahn@46405:       Pretty.block (separate (Pretty.brk 2)
bulwahn@46405:        [Pretty.str "type constructor:",
bulwahn@46405:         Pretty.str s,
bulwahn@46405:         Pretty.str "abs term:",
bulwahn@46405:         Syntax.pretty_term ctxt abs,
bulwahn@46405:         Pretty.str "rep term:",
bulwahn@46405:         Syntax.pretty_term ctxt rep])
bulwahn@46405:   in
bulwahn@46405:     map prt_abs_rep (Symtab.dest (Abs_Rep.get (Context.Proof ctxt)))
bulwahn@46405:     |> Pretty.big_list "abs/rep terms:"
bulwahn@46405:     |> Pretty.writeln
bulwahn@46405:   end
kaliszyk@35222: 
kaliszyk@35222: (* info about quotient types *)
wenzelm@46150: type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
kaliszyk@35222: 
wenzelm@46151: structure Quotients = Generic_Data
wenzelm@39034: (
wenzelm@46150:   type T = quotients Symtab.table
wenzelm@39034:   val empty = Symtab.empty
wenzelm@39034:   val extend = I
wenzelm@39034:   fun merge data = Symtab.merge (K true) data
wenzelm@39034: )
kaliszyk@35222: 
wenzelm@46150: fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} =
kaliszyk@35222:   {qtyp = Morphism.typ phi qtyp,
kaliszyk@35222:    rtyp = Morphism.typ phi rtyp,
kaliszyk@35222:    equiv_rel = Morphism.term phi equiv_rel,
kaliszyk@35222:    equiv_thm = Morphism.thm phi equiv_thm}
kaliszyk@35222: 
wenzelm@46151: val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
wenzelm@46211: val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
kaliszyk@35222: 
wenzelm@46151: fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
kaliszyk@35222: 
wenzelm@46151: fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
wenzelm@46151:   map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
kaliszyk@35222: 
wenzelm@46150: fun print_quotients ctxt =
wenzelm@41700:   let
wenzelm@41700:     fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
wenzelm@41701:       Pretty.block (separate (Pretty.brk 2)
wenzelm@41700:        [Pretty.str "quotient type:",
wenzelm@41700:         Syntax.pretty_typ ctxt qtyp,
wenzelm@41700:         Pretty.str "raw type:",
wenzelm@41700:         Syntax.pretty_typ ctxt rtyp,
wenzelm@41700:         Pretty.str "relation:",
wenzelm@41700:         Syntax.pretty_term ctxt equiv_rel,
wenzelm@41700:         Pretty.str "equiv. thm:",
wenzelm@41700:         Syntax.pretty_term ctxt (prop_of equiv_thm)])
wenzelm@41700:   in
wenzelm@46151:     map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
wenzelm@41700:     |> Pretty.big_list "quotients:"
wenzelm@41700:     |> Pretty.writeln
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (* info about quotient constants *)
wenzelm@46150: type quotconsts = {qconst: term, rconst: term, def: thm}
kaliszyk@35222: 
wenzelm@46150: fun eq_quotconsts (x : quotconsts, y : quotconsts) = #qconst x = #qconst y
kaliszyk@35222: 
kaliszyk@35222: (* We need to be able to lookup instances of lifted constants,
kaliszyk@35222:    for example given "nat fset" we need to find "'a fset";
kaliszyk@35222:    but overloaded constants share the same name *)
wenzelm@46151: structure Quotconsts = Generic_Data
wenzelm@39034: (
wenzelm@46150:   type T = quotconsts list Symtab.table
wenzelm@39034:   val empty = Symtab.empty
wenzelm@39034:   val extend = I
wenzelm@46150:   val merge = Symtab.merge_list eq_quotconsts
wenzelm@39034: )
kaliszyk@35222: 
wenzelm@46150: fun transform_quotconsts phi {qconst, rconst, def} =
kaliszyk@35222:   {qconst = Morphism.term phi qconst,
kaliszyk@35222:    rconst = Morphism.term phi rconst,
kaliszyk@35222:    def = Morphism.thm phi def}
kaliszyk@35222: 
wenzelm@46151: fun update_quotconsts name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
kaliszyk@35222: 
wenzelm@46151: fun dest_quotconsts ctxt =
wenzelm@46151:   flat (map snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
kaliszyk@35222: 
urbanc@46215: fun dest_quotconsts_global thy =
urbanc@46215:   flat (map snd (Symtab.dest (Quotconsts.get (Context.Theory thy))))
urbanc@46215: 
urbanc@46215: 
urbanc@46215: 
wenzelm@46211: fun lookup_quotconsts_global thy t =
kaliszyk@35222:   let
kaliszyk@35222:     val (name, qty) = dest_Const t
wenzelm@46150:     fun matches (x: quotconsts) =
wenzelm@46151:       let val (name', qty') = dest_Const (#qconst x);
wenzelm@46151:       in name = name' andalso Sign.typ_instance thy (qty, qty') end
kaliszyk@35222:   in
wenzelm@46211:     (case Symtab.lookup (Quotconsts.get (Context.Theory thy)) name of
bulwahn@46145:       NONE => NONE
bulwahn@46145:     | SOME l => find_first matches l)
kaliszyk@35222:   end
kaliszyk@35222: 
wenzelm@46150: fun print_quotconsts ctxt =
wenzelm@41700:   let
wenzelm@41700:     fun prt_qconst {qconst, rconst, def} =
wenzelm@41700:       Pretty.block (separate (Pretty.brk 1)
wenzelm@41700:        [Syntax.pretty_term ctxt qconst,
wenzelm@41700:         Pretty.str ":=",
wenzelm@41700:         Syntax.pretty_term ctxt rconst,
wenzelm@41700:         Pretty.str "as",
wenzelm@41700:         Syntax.pretty_term ctxt (prop_of def)])
wenzelm@41700:   in
wenzelm@46151:     map prt_qconst (maps snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
wenzelm@41700:     |> Pretty.big_list "quotient constants:"
wenzelm@41700:     |> Pretty.writeln
wenzelm@41700:   end
kaliszyk@35222: 
kaliszyk@35222: (* equivalence relation theorems *)
wenzelm@46150: structure Equiv_Rules = Named_Thms
wenzelm@39039: (
wenzelm@46165:   val name = @{binding quot_equiv}
wenzelm@39039:   val description = "equivalence relation theorems"
wenzelm@39039: )
kaliszyk@35222: 
wenzelm@46150: val equiv_rules = Equiv_Rules.get
wenzelm@46150: val equiv_rules_add = Equiv_Rules.add
kaliszyk@35222: 
kaliszyk@35222: (* respectfulness theorems *)
wenzelm@46150: structure Rsp_Rules = Named_Thms
wenzelm@39039: (
wenzelm@46165:   val name = @{binding quot_respect}
wenzelm@39039:   val description = "respectfulness theorems"
wenzelm@39039: )
kaliszyk@35222: 
wenzelm@46150: val rsp_rules = Rsp_Rules.get
wenzelm@46150: val rsp_rules_add = Rsp_Rules.add
kaliszyk@35222: 
kaliszyk@35222: (* preservation theorems *)
wenzelm@46150: structure Prs_Rules = Named_Thms
wenzelm@39039: (
wenzelm@46165:   val name = @{binding quot_preserve}
wenzelm@39039:   val description = "preservation theorems"
wenzelm@39039: )
kaliszyk@35222: 
wenzelm@46150: val prs_rules = Prs_Rules.get
wenzelm@46150: val prs_rules_add = Prs_Rules.add
kaliszyk@35222: 
kaliszyk@35222: (* id simplification theorems *)
wenzelm@46150: structure Id_Simps = Named_Thms
wenzelm@39039: (
wenzelm@46165:   val name = @{binding id_simps}
wenzelm@39039:   val description = "identity simp rules for maps"
wenzelm@39039: )
kaliszyk@35222: 
wenzelm@46150: val id_simps = Id_Simps.get
kaliszyk@35222: 
kaliszyk@35222: (* quotient theorems *)
wenzelm@46150: structure Quotient_Rules = Named_Thms
wenzelm@39039: (
wenzelm@46165:   val name = @{binding quot_thm}
wenzelm@39039:   val description = "quotient theorems"
wenzelm@39039: )
kaliszyk@35222: 
wenzelm@46150: val quotient_rules = Quotient_Rules.get
wenzelm@46150: val quotient_rules_add = Quotient_Rules.add
kaliszyk@35222: 
kaliszyk@35222: 
wenzelm@41708: (* theory setup *)
kaliszyk@35222: 
wenzelm@41708: val setup =
wenzelm@46152:   quotmaps_attribute_setup #>
wenzelm@46150:   Equiv_Rules.setup #>
wenzelm@46150:   Rsp_Rules.setup #>
wenzelm@46150:   Prs_Rules.setup #>
wenzelm@46150:   Id_Simps.setup #>
wenzelm@46150:   Quotient_Rules.setup
kaliszyk@35222: 
kaliszyk@35222: 
wenzelm@41708: (* outer syntax commands *)
wenzelm@41708: 
wenzelm@41708: val _ =
wenzelm@41708:   Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag
wenzelm@46150:     (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
wenzelm@41708: 
wenzelm@41708: val _ =
wenzelm@41708:   Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag
wenzelm@46150:     (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
wenzelm@41708: 
wenzelm@41708: val _ =
wenzelm@41708:   Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
wenzelm@46150:     (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
kaliszyk@35222: 
wenzelm@46150: end;