--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Feb 16 19:58:42 2018 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Feb 16 20:44:25 2018 +0100
@@ -9,6 +9,7 @@
type quotmaps = {relmap: string, quot_thm: thm}
val lookup_quotmaps: Proof.context -> string -> quotmaps option
val lookup_quotmaps_global: theory -> string -> quotmaps option
+ val update_quotmaps: string * quotmaps -> Context.generic -> Context.generic
val print_quotmaps: Proof.context -> unit
type abs_rep = {abs : term, rep : term}
@@ -30,10 +31,10 @@
val transform_quotconsts: morphism -> quotconsts -> quotconsts
val lookup_quotconsts_global: theory -> term -> quotconsts option
val update_quotconsts: string * quotconsts -> Context.generic -> Context.generic
+ val dest_quotconsts: Proof.context -> quotconsts list
val dest_quotconsts_global: theory -> quotconsts list
- val dest_quotconsts: Proof.context -> quotconsts list
val print_quotconsts: Proof.context -> unit
-end;
+end
structure Quotient_Info: QUOTIENT_INFO =
struct
@@ -42,20 +43,23 @@
(*info about map- and rel-functions for a type*)
type quotmaps = {relmap: string, quot_thm: thm}
+fun transform_quotmaps phi : quotmaps -> quotmaps =
+ fn {relmap, quot_thm} => {relmap = relmap, quot_thm = Morphism.thm phi quot_thm}
(*info about abs/rep terms*)
type abs_rep = {abs : term, rep : term}
-fun transform_abs_rep phi {abs, rep} : abs_rep =
- {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
+fun transform_abs_rep phi : abs_rep -> abs_rep =
+ fn {abs, rep} => {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
(*info about quotient types*)
type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
-fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} : quotients =
- {qtyp = Morphism.typ phi qtyp,
- rtyp = Morphism.typ phi rtyp,
- equiv_rel = Morphism.term phi equiv_rel,
- equiv_thm = Morphism.thm phi equiv_thm,
- quot_thm = Morphism.thm phi quot_thm}
+fun transform_quotients phi : quotients -> quotients =
+ fn {qtyp, rtyp, equiv_rel, equiv_thm, quot_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,
+ quot_thm = Morphism.thm phi quot_thm}
(*info about quotient constants*)
(*We need to be able to lookup instances of lifted constants,
@@ -63,10 +67,11 @@
but overloaded constants share the same name.*)
type quotconsts = {qconst: term, rconst: term, def: thm}
fun eq_quotconsts (x: quotconsts, y: quotconsts) = #qconst x = #qconst y
-fun transform_quotconsts phi {qconst, rconst, def} : quotconsts =
- {qconst = Morphism.term phi qconst,
- rconst = Morphism.term phi rconst,
- def = Morphism.thm phi def}
+fun transform_quotconsts phi : quotconsts -> quotconsts =
+ fn {qconst, rconst, def} =>
+ {qconst = Morphism.term phi qconst,
+ rconst = Morphism.term phi rconst,
+ def = Morphism.thm phi def}
structure Data = Generic_Data
(
@@ -99,10 +104,15 @@
(* quotmaps *)
-val lookup_quotmaps = Symtab.lookup o get_quotmaps o Context.Proof
-val lookup_quotmaps_global = Symtab.lookup o get_quotmaps o Context.Theory
+fun lookup_quotmaps_generic context name =
+ Symtab.lookup (get_quotmaps context) name
+ |> Option.map (transform_quotmaps (Morphism.transfer_morphism (Context.theory_of context)))
-(* FIXME export proper internal update operation!? *)
+val lookup_quotmaps = lookup_quotmaps_generic o Context.Proof
+val lookup_quotmaps_global = lookup_quotmaps_generic o Context.Theory
+
+val update_quotmaps =
+ map_quotmaps o Symtab.update o apsnd (transform_quotmaps Morphism.trim_context_morphism)
val _ =
Theory.setup
@@ -112,8 +122,8 @@
Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
Attrib.thm --| Scan.lift @{keyword ")"}) >>
(fn (tyname, (relmap, quot_thm)) =>
- let val minfo = {relmap = relmap, quot_thm = quot_thm}
- in Thm.declaration_attribute (K (map_quotmaps (Symtab.update (tyname, minfo)))) end))
+ Thm.declaration_attribute
+ (K (update_quotmaps (tyname, {relmap = relmap, quot_thm = quot_thm})))))
"declaration of map information")
fun print_quotmaps ctxt =
@@ -138,7 +148,8 @@
val lookup_abs_rep = Symtab.lookup o get_abs_rep o Context.Proof
val lookup_abs_rep_global = Symtab.lookup o get_abs_rep o Context.Theory
-val update_abs_rep = map_abs_rep o Symtab.update
+val update_abs_rep =
+ map_abs_rep o Symtab.update o apsnd (transform_abs_rep Morphism.trim_context_morphism)
fun print_abs_rep ctxt =
let
@@ -159,10 +170,15 @@
(* quotients *)
-val lookup_quotients = Symtab.lookup o get_quotients o Context.Proof
-val lookup_quotients_global = Symtab.lookup o get_quotients o Context.Theory
+fun lookup_quotients_generic context name =
+ Symtab.lookup (get_quotients context) name
+ |> Option.map (transform_quotients (Morphism.transfer_morphism (Context.theory_of context)))
-val update_quotients = map_quotients o Symtab.update
+val lookup_quotients = lookup_quotients_generic o Context.Proof
+val lookup_quotients_global = lookup_quotients_generic o Context.Theory
+
+val update_quotients =
+ map_quotients o Symtab.update o apsnd (transform_quotients Morphism.trim_context_morphism)
fun dest_quotients ctxt =
map snd (Symtab.dest (get_quotients (Context.Proof ctxt)))
@@ -190,24 +206,25 @@
(* quotconsts *)
-val update_quotconsts = map_quotconsts o Symtab.cons_list
+val update_quotconsts =
+ map_quotconsts o Symtab.cons_list o apsnd (transform_quotconsts Morphism.trim_context_morphism)
-fun dest_quotconsts ctxt =
- maps snd (Symtab.dest (get_quotconsts (Context.Proof ctxt)))
+fun dest_quotconsts_generic context =
+ maps #2 (Symtab.dest (get_quotconsts context))
+ |> map (transform_quotconsts (Morphism.transfer_morphism (Context.theory_of context)))
-fun dest_quotconsts_global thy =
- maps snd (Symtab.dest (get_quotconsts (Context.Theory thy)))
+val dest_quotconsts = dest_quotconsts_generic o Context.Proof
+val dest_quotconsts_global = dest_quotconsts_generic o Context.Theory
fun lookup_quotconsts_global thy t =
let
val (name, qty) = dest_Const t
- fun matches ({qconst, ...}: quotconsts) =
- let val (name', qty') = dest_Const qconst;
- in name = name' andalso Sign.typ_instance thy (qty, qty') end
in
- (case Symtab.lookup (get_quotconsts (Context.Theory thy)) name of
- NONE => NONE
- | SOME l => find_first matches l)
+ Symtab.lookup_list (get_quotconsts (Context.Theory thy)) name
+ |> find_first (fn {qconst, ...} =>
+ let val (name', qty') = dest_Const qconst
+ in name = name' andalso Sign.typ_instance thy (qty, qty') end)
+ |> Option.map (transform_quotconsts (Morphism.transfer_morphism thy))
end
fun print_quotconsts ctxt =
@@ -220,7 +237,7 @@
Pretty.str "as",
Syntax.pretty_term ctxt (Thm.prop_of def)])
in
- map prt_qconst (maps snd (Symtab.dest (get_quotconsts (Context.Proof ctxt))))
+ map prt_qconst (dest_quotconsts ctxt)
|> Pretty.big_list "quotient constants:"
|> Pretty.writeln
end
@@ -240,4 +257,4 @@
Outer_Syntax.command @{command_keyword print_quotconsts} "print quotient constants"
(Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
-end;
+end