4 |
4 |
5 type maps_info = {mapfun: string, relfun: string} |
5 type maps_info = {mapfun: string, relfun: string} |
6 val maps_lookup: theory -> string -> maps_info option |
6 val maps_lookup: theory -> string -> maps_info option |
7 val maps_update_thy: string -> maps_info -> theory -> theory |
7 val maps_update_thy: string -> maps_info -> theory -> theory |
8 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
8 val maps_update: string -> maps_info -> Proof.context -> Proof.context |
|
9 val print_mapsinfo: Proof.context -> unit |
9 |
10 |
10 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
11 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
11 val print_quotinfo: Proof.context -> unit |
|
12 val quotdata_lookup_thy: theory -> string -> quotient_info option |
12 val quotdata_lookup_thy: theory -> string -> quotient_info option |
13 val quotdata_lookup: Proof.context -> string -> quotient_info option |
13 val quotdata_lookup: Proof.context -> string -> quotient_info option |
14 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
14 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
15 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
15 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
16 val quotdata_dest: theory -> quotient_info list |
16 val quotdata_dest: theory -> quotient_info list |
|
17 val print_quotinfo: Proof.context -> unit |
17 |
18 |
18 type qconsts_info = {qconst: term, rconst: term, def: thm} |
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
19 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
20 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
20 val qconsts_lookup: theory -> term -> qconsts_info |
21 val qconsts_lookup: theory -> term -> qconsts_info |
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
22 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
78 Args.name --| OuterParse.$$$ ")")) |
79 Args.name --| OuterParse.$$$ ")")) |
79 |
80 |
80 val _ = Context.>> (Context.map_theory |
81 val _ = Context.>> (Context.map_theory |
81 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
82 (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) |
82 "declaration of map information")) |
83 "declaration of map information")) |
|
84 |
|
85 fun print_mapsinfo ctxt = |
|
86 let |
|
87 fun prt_map (ty_name, {mapfun, relfun}) = |
|
88 Pretty.block (Library.separate (Pretty.brk 2) |
|
89 [Pretty.str "type:", |
|
90 Pretty.str ty_name, |
|
91 Pretty.str "map fun:", |
|
92 Pretty.str mapfun, |
|
93 Pretty.str "relation map:", |
|
94 Pretty.str relfun]) |
|
95 in |
|
96 MapsData.get (ProofContext.theory_of ctxt) |
|
97 |> Symtab.dest |
|
98 |> map (prt_map) |
|
99 |> Pretty.big_list "maps:" |
|
100 |> Pretty.writeln |
|
101 end |
|
102 |
83 |
103 |
84 |
104 |
85 (* info about quotient types *) |
105 (* info about quotient types *) |
86 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
106 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} |
87 |
107 |