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 transform_qconsts: morphism -> qconsts_info -> qconsts_info |
20 val transform_qconsts: 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 *) |
22 val qconsts_update_thy: term -> qconsts_info -> theory -> theory |
22 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
23 val qconsts_update_gen: term -> qconsts_info -> Context.generic -> Context.generic |
23 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
24 val qconsts_dest: theory -> qconsts_info list |
24 val qconsts_dest: theory -> qconsts_info list |
25 val print_qconstinfo: Proof.context -> unit |
25 val print_qconstinfo: Proof.context -> unit |
26 |
26 |
27 val equiv_rules_get: Proof.context -> thm list |
27 val equiv_rules_get: Proof.context -> thm list |
28 val equiv_rules_add: attribute |
28 val equiv_rules_add: attribute |
177 |
177 |
178 |
178 |
179 (* info about quotient constants *) |
179 (* info about quotient constants *) |
180 type qconsts_info = {qconst: term, rconst: term, def: thm} |
180 type qconsts_info = {qconst: term, rconst: term, def: thm} |
181 |
181 |
|
182 (* We need to be able to lookup instances of lifted constants, |
|
183 for example given "nat fset" we need to find "'a fset"; |
|
184 but overloaded constants share the same name *) |
182 structure QConstsData = Theory_Data |
185 structure QConstsData = Theory_Data |
183 (type T = qconsts_info Termtab.table |
186 (type T = qconsts_info Symtab.table |
184 val empty = Termtab.empty |
187 val empty = Symtab.empty |
185 val extend = I |
188 val extend = I |
186 val merge = Termtab.merge (K true)) |
189 val merge = Symtab.merge (K true)) |
187 |
190 |
188 fun transform_qconsts phi {qconst, rconst, def} = |
191 fun transform_qconsts phi {qconst, rconst, def} = |
189 {qconst = Morphism.term phi qconst, |
192 {qconst = Morphism.term phi qconst, |
190 rconst = Morphism.term phi rconst, |
193 rconst = Morphism.term phi rconst, |
191 def = Morphism.thm phi def} |
194 def = Morphism.thm phi def} |
192 |
195 |
193 fun qconsts_update_thy const qcinfo = QConstsData.map (Termtab.update (const, qcinfo)) |
196 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.update (name, qcinfo)) |
194 fun qconsts_update_gen const qcinfo = Context.mapping (qconsts_update_thy const qcinfo) I |
197 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I |
195 |
198 |
196 fun qconsts_dest thy = |
199 fun qconsts_dest thy = |
197 map snd (Termtab.dest (QConstsData.get thy)) |
200 map snd (Symtab.dest (QConstsData.get thy)) |
198 |
201 |
199 (* FIXME / TODO : better implementation of the lookup datastructure *) |
202 (* FIXME / TODO : better implementation of the lookup datastructure *) |
200 (* for example symtabs to alist; or tables with string type key *) |
203 (* for example symtabs to alist; or tables with string type key *) |
201 fun qconsts_lookup thy t = |
204 fun qconsts_lookup thy t = |
202 let |
205 let |
203 val smt = Termtab.dest (QConstsData.get thy); |
206 val smt = Symtab.dest (QConstsData.get thy); |
204 val (name, qty) = dest_Const t |
207 val (name, qty) = dest_Const t |
205 fun matches (_, x) = |
208 fun matches (_, x) = |
206 let |
209 let |
207 val (name', qty') = dest_Const (#qconst x); |
210 val (name', qty') = dest_Const (#qconst x); |
208 in |
211 in |