6 val maps_lookup: theory -> string -> maps_info (* raises NotFound *) |
6 val maps_lookup: theory -> string -> maps_info (* raises NotFound *) |
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 val print_mapsinfo: Proof.context -> unit |
10 |
10 |
11 type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
11 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
12 val quotdata_lookup_thy: theory -> string -> quotient_info (* raises NotFound *) |
12 val quotdata_transfer: morphism -> quotdata_info -> quotdata_info |
13 val quotdata_lookup: Proof.context -> string -> quotient_info (* raises NotFound *) |
13 val quotdata_lookup: theory -> string -> quotdata_info (* raises NotFound *) |
14 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
14 val quotdata_update_thy: string -> quotdata_info -> theory -> theory |
15 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
15 val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic |
16 val quotdata_dest: theory -> quotient_info list |
16 val quotdata_dest: theory -> quotdata_info list |
17 val print_quotinfo: Proof.context -> unit |
17 val print_quotinfo: Proof.context -> unit |
18 |
18 |
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
19 type qconsts_info = {qconst: term, rconst: term, def: thm} |
20 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
20 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
21 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
21 val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) |
58 |
58 |
59 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
59 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) |
60 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
60 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) |
61 |
61 |
62 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
62 fun maps_attribute_aux s minfo = Thm.declaration_attribute |
63 (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
63 (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) |
64 |
64 |
65 (* attribute to be used in declare statements *) |
65 (* attribute to be used in declare statements *) |
66 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
66 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = |
67 let |
67 let |
68 val thy = ProofContext.theory_of ctxt |
68 val thy = ProofContext.theory_of ctxt |
96 "relation map:", relmap])) |
96 "relation map:", relmap])) |
97 in |
97 in |
98 MapsData.get (ProofContext.theory_of ctxt) |
98 MapsData.get (ProofContext.theory_of ctxt) |
99 |> Symtab.dest |
99 |> Symtab.dest |
100 |> map (prt_map) |
100 |> map (prt_map) |
101 |> Pretty.big_list "maps:" |
101 |> Pretty.big_list "maps for type constructors:" |
102 |> Pretty.writeln |
102 |> Pretty.writeln |
103 end |
103 end |
104 |
104 |
105 |
105 |
106 (* info about quotient types *) |
106 (* info about quotient types *) |
107 type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
107 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} |
108 |
108 |
109 structure QuotData = Theory_Data |
109 structure QuotData = Theory_Data |
110 (type T = quotient_info Symtab.table |
110 (type T = quotdata_info Symtab.table |
111 val empty = Symtab.empty |
111 val empty = Symtab.empty |
112 val extend = I |
112 val extend = I |
113 val merge = Symtab.merge (K true)) |
113 val merge = Symtab.merge (K true)) |
114 |
114 |
115 fun quotdata_lookup_thy thy s = |
115 fun quotdata_transfer phi {qtyp, rtyp, equiv_rel, equiv_thm} = |
116 case Symtab.lookup (QuotData.get thy) (Sign.intern_type thy s) of |
116 {qtyp = Morphism.typ phi qtyp, |
|
117 rtyp = Morphism.typ phi rtyp, |
|
118 equiv_rel = Morphism.term phi equiv_rel, |
|
119 equiv_thm = Morphism.thm phi equiv_thm} |
|
120 |
|
121 fun quotdata_lookup thy str = |
|
122 case Symtab.lookup (QuotData.get thy) str of |
117 SOME qinfo => qinfo |
123 SOME qinfo => qinfo |
118 | NONE => raise NotFound |
124 | NONE => raise NotFound |
119 |
125 |
120 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of |
126 fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo)) |
121 |
127 fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I |
122 fun quotdata_update_thy qty_name (qty, rty, equiv_rel, equiv_thm) = |
|
123 let |
|
124 val qinfo = {qtyp = qty, rtyp = rty, equiv_rel = equiv_rel, equiv_thm = equiv_thm} |
|
125 in |
|
126 QuotData.map (Symtab.update (qty_name, qinfo)) |
|
127 end |
|
128 |
|
129 fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = |
|
130 ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm)) |
|
131 |
128 |
132 fun quotdata_dest thy = |
129 fun quotdata_dest thy = |
133 map snd (Symtab.dest (QuotData.get thy)) |
130 map snd (Symtab.dest (QuotData.get thy)) |
134 |
131 |
135 fun print_quotinfo ctxt = |
132 fun print_quotinfo ctxt = |
165 fun qconsts_transfer phi {qconst, rconst, def} = |
162 fun qconsts_transfer phi {qconst, rconst, def} = |
166 {qconst = Morphism.term phi qconst, |
163 {qconst = Morphism.term phi qconst, |
167 rconst = Morphism.term phi rconst, |
164 rconst = Morphism.term phi rconst, |
168 def = Morphism.thm phi def} |
165 def = Morphism.thm phi def} |
169 |
166 |
170 fun qconsts_update_thy id qcinfo = QConstsData.map (Symtab.update (id, qcinfo)) |
167 fun qconsts_update_thy str qcinfo = QConstsData.map (Symtab.update (str, qcinfo)) |
171 fun qconsts_update_gen id qcinfo = Context.mapping (qconsts_update_thy id qcinfo) I |
168 fun qconsts_update_gen str qcinfo = Context.mapping (qconsts_update_thy str qcinfo) I |
172 |
169 |
173 fun qconsts_dest thy = |
170 fun qconsts_dest thy = |
174 map snd (Symtab.dest (QConstsData.get thy)) |
171 map snd (Symtab.dest (QConstsData.get thy)) |
175 |
172 |
176 (* FIXME / TODO : better implementation of the lookup datastructure *) |
173 (* FIXME / TODO : better implementation of the lookup datastructure *) |