4 Context data for the quotient package. |
4 Context data for the quotient package. |
5 *) |
5 *) |
6 |
6 |
7 signature QUOTIENT_INFO = |
7 signature QUOTIENT_INFO = |
8 sig |
8 sig |
9 type quotmaps = {relmap: string} |
9 type quotmaps = {relmap: string, quot_thm: thm} |
10 val lookup_quotmaps: Proof.context -> string -> quotmaps option |
10 val lookup_quotmaps: Proof.context -> string -> quotmaps option |
11 val lookup_quotmaps_global: theory -> string -> quotmaps option |
11 val lookup_quotmaps_global: theory -> string -> quotmaps option |
12 val print_quotmaps: Proof.context -> unit |
12 val print_quotmaps: Proof.context -> unit |
13 |
13 |
14 type abs_rep = {abs : term, rep : term} |
14 type abs_rep = {abs : term, rep : term} |
16 val lookup_abs_rep: Proof.context -> string -> abs_rep option |
16 val lookup_abs_rep: Proof.context -> string -> abs_rep option |
17 val lookup_abs_rep_global: theory -> string -> abs_rep option |
17 val lookup_abs_rep_global: theory -> string -> abs_rep option |
18 val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic |
18 val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic |
19 val print_abs_rep: Proof.context -> unit |
19 val print_abs_rep: Proof.context -> unit |
20 |
20 |
21 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
21 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm} |
22 val transform_quotients: morphism -> quotients -> quotients |
22 val transform_quotients: morphism -> quotients -> quotients |
23 val lookup_quotients: Proof.context -> string -> quotients option |
23 val lookup_quotients: Proof.context -> string -> quotients option |
24 val lookup_quotients_global: theory -> string -> quotients option |
24 val lookup_quotients_global: theory -> string -> quotients option |
25 val update_quotients: string -> quotients -> Context.generic -> Context.generic |
25 val update_quotients: string -> quotients -> Context.generic -> Context.generic |
26 val dest_quotients: Proof.context -> quotients list |
26 val dest_quotients: Proof.context -> quotients list |
52 (** data containers **) |
52 (** data containers **) |
53 |
53 |
54 (* FIXME just one data slot (record) per program unit *) |
54 (* FIXME just one data slot (record) per program unit *) |
55 |
55 |
56 (* info about map- and rel-functions for a type *) |
56 (* info about map- and rel-functions for a type *) |
57 type quotmaps = {relmap: string} |
57 type quotmaps = {relmap: string, quot_thm: thm} |
58 |
58 |
59 structure Quotmaps = Generic_Data |
59 structure Quotmaps = Generic_Data |
60 ( |
60 ( |
61 type T = quotmaps Symtab.table |
61 type T = quotmaps Symtab.table |
62 val empty = Symtab.empty |
62 val empty = Symtab.empty |
69 |
69 |
70 (* FIXME export proper internal update operation!? *) |
70 (* FIXME export proper internal update operation!? *) |
71 |
71 |
72 val quotmaps_attribute_setup = |
72 val quotmaps_attribute_setup = |
73 Attrib.setup @{binding map} |
73 Attrib.setup @{binding map} |
74 ((Args.type_name true --| Scan.lift @{keyword "="}) -- Args.const_proper true >> |
74 ((Args.type_name true --| Scan.lift @{keyword "="}) -- |
75 (fn (tyname, relname) => |
75 (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} -- |
76 let val minfo = {relmap = relname} |
76 Attrib.thm --| Scan.lift @{keyword ")"}) >> |
|
77 (fn (tyname, (relname, qthm)) => |
|
78 let val minfo = {relmap = relname, quot_thm = qthm} |
77 in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end)) |
79 in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end)) |
78 "declaration of map information" |
80 "declaration of map information" |
79 |
81 |
80 fun print_quotmaps ctxt = |
82 fun print_quotmaps ctxt = |
81 let |
83 let |
82 fun prt_map (ty_name, {relmap}) = |
84 fun prt_map (ty_name, {relmap, quot_thm}) = |
83 Pretty.block (separate (Pretty.brk 2) |
85 Pretty.block (separate (Pretty.brk 2) |
84 (map Pretty.str |
86 [Pretty.str "type:", |
85 ["type:", ty_name, |
87 Pretty.str ty_name, |
86 "relation map:", relmap])) |
88 Pretty.str "relation map:", |
|
89 Pretty.str relmap, |
|
90 Pretty.str "quot. theorem:", |
|
91 Syntax.pretty_term ctxt (prop_of quot_thm)]) |
87 in |
92 in |
88 map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt))) |
93 map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt))) |
89 |> Pretty.big_list "maps for type constructors:" |
94 |> Pretty.big_list "maps for type constructors:" |
90 |> Pretty.writeln |
95 |> Pretty.writeln |
91 end |
96 end |
123 |> Pretty.big_list "abs/rep terms:" |
128 |> Pretty.big_list "abs/rep terms:" |
124 |> Pretty.writeln |
129 |> Pretty.writeln |
125 end |
130 end |
126 |
131 |
127 (* info about quotient types *) |
132 (* info about quotient types *) |
128 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
133 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm} |
129 |
134 |
130 structure Quotients = Generic_Data |
135 structure Quotients = Generic_Data |
131 ( |
136 ( |
132 type T = quotients Symtab.table |
137 type T = quotients Symtab.table |
133 val empty = Symtab.empty |
138 val empty = Symtab.empty |
134 val extend = I |
139 val extend = I |
135 fun merge data = Symtab.merge (K true) data |
140 fun merge data = Symtab.merge (K true) data |
136 ) |
141 ) |
137 |
142 |
138 fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
143 fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} = |
139 {qtyp = Morphism.typ phi qtyp, |
144 {qtyp = Morphism.typ phi qtyp, |
140 rtyp = Morphism.typ phi rtyp, |
145 rtyp = Morphism.typ phi rtyp, |
141 equiv_rel = Morphism.term phi equiv_rel, |
146 equiv_rel = Morphism.term phi equiv_rel, |
142 equiv_thm = Morphism.thm phi equiv_thm} |
147 equiv_thm = Morphism.thm phi equiv_thm, |
|
148 quot_thm = Morphism.thm phi quot_thm} |
143 |
149 |
144 val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof |
150 val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof |
145 val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory |
151 val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory |
146 |
152 |
147 fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo)) |
153 fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo)) |
149 fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *) |
155 fun dest_quotients ctxt = (* FIXME slightly expensive way to retrieve data *) |
150 map snd (Symtab.dest (Quotients.get (Context.Proof ctxt))) |
156 map snd (Symtab.dest (Quotients.get (Context.Proof ctxt))) |
151 |
157 |
152 fun print_quotients ctxt = |
158 fun print_quotients ctxt = |
153 let |
159 let |
154 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = |
160 fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} = |
155 Pretty.block (separate (Pretty.brk 2) |
161 Pretty.block (separate (Pretty.brk 2) |
156 [Pretty.str "quotient type:", |
162 [Pretty.str "quotient type:", |
157 Syntax.pretty_typ ctxt qtyp, |
163 Syntax.pretty_typ ctxt qtyp, |
158 Pretty.str "raw type:", |
164 Pretty.str "raw type:", |
159 Syntax.pretty_typ ctxt rtyp, |
165 Syntax.pretty_typ ctxt rtyp, |
160 Pretty.str "relation:", |
166 Pretty.str "relation:", |
161 Syntax.pretty_term ctxt equiv_rel, |
167 Syntax.pretty_term ctxt equiv_rel, |
162 Pretty.str "equiv. thm:", |
168 Pretty.str "equiv. thm:", |
163 Syntax.pretty_term ctxt (prop_of equiv_thm)]) |
169 Syntax.pretty_term ctxt (prop_of equiv_thm), |
|
170 Pretty.str "quot. thm:", |
|
171 Syntax.pretty_term ctxt (prop_of quot_thm)]) |
164 in |
172 in |
165 map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt))) |
173 map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt))) |
166 |> Pretty.big_list "quotients:" |
174 |> Pretty.big_list "quotients:" |
167 |> Pretty.writeln |
175 |> Pretty.writeln |
168 end |
176 end |