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 fun qconsts_info_eq (x : qconsts_info, y : qconsts_info) = #qconst x = #qconst y |
|
183 |
182 (* We need to be able to lookup instances of lifted constants, |
184 (* We need to be able to lookup instances of lifted constants, |
183 for example given "nat fset" we need to find "'a fset"; |
185 for example given "nat fset" we need to find "'a fset"; |
184 but overloaded constants share the same name *) |
186 but overloaded constants share the same name *) |
185 structure QConstsData = Theory_Data |
187 structure QConstsData = Theory_Data |
186 (type T = qconsts_info Symtab.table |
188 (type T = (qconsts_info list) Symtab.table |
187 val empty = Symtab.empty |
189 val empty = Symtab.empty |
188 val extend = I |
190 val extend = I |
189 val merge = Symtab.merge (K true)) |
191 val merge = Symtab.merge_list qconsts_info_eq) |
190 |
192 |
191 fun transform_qconsts phi {qconst, rconst, def} = |
193 fun transform_qconsts phi {qconst, rconst, def} = |
192 {qconst = Morphism.term phi qconst, |
194 {qconst = Morphism.term phi qconst, |
193 rconst = Morphism.term phi rconst, |
195 rconst = Morphism.term phi rconst, |
194 def = Morphism.thm phi def} |
196 def = Morphism.thm phi def} |
195 |
197 |
196 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.update (name, qcinfo)) |
198 fun qconsts_update_thy name qcinfo = QConstsData.map (Symtab.cons_list (name, qcinfo)) |
197 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I |
199 fun qconsts_update_gen name qcinfo = Context.mapping (qconsts_update_thy name qcinfo) I |
198 |
200 |
199 fun qconsts_dest thy = |
201 fun qconsts_dest thy = |
200 map snd (Symtab.dest (QConstsData.get thy)) |
202 flat (map snd (Symtab.dest (QConstsData.get thy))) |
201 |
203 |
202 (* FIXME / TODO : better implementation of the lookup datastructure *) |
|
203 (* for example symtabs to alist; or tables with string type key *) |
|
204 fun qconsts_lookup thy t = |
204 fun qconsts_lookup thy t = |
205 let |
205 let |
206 val smt = Symtab.dest (QConstsData.get thy); |
|
207 val (name, qty) = dest_Const t |
206 val (name, qty) = dest_Const t |
208 fun matches (_, x) = |
207 fun matches x = |
209 let |
208 let |
210 val (name', qty') = dest_Const (#qconst x); |
209 val (name', qty') = dest_Const (#qconst x); |
211 in |
210 in |
212 name = name' andalso Sign.typ_instance thy (qty, qty') |
211 name = name' andalso Sign.typ_instance thy (qty, qty') |
213 end |
212 end |
214 in |
213 in |
215 case (find_first matches smt) of |
214 case Symtab.lookup (QConstsData.get thy) name of |
216 SOME (_, x) => x |
215 NONE => raise NotFound |
217 | _ => raise NotFound |
216 | SOME l => |
|
217 (case (find_first matches l) of |
|
218 SOME x => x |
|
219 | NONE => raise NotFound |
|
220 ) |
218 end |
221 end |
219 |
222 |
220 fun print_qconstinfo ctxt = |
223 fun print_qconstinfo ctxt = |
221 let |
224 let |
222 fun prt_qconst {qconst, rconst, def} = |
225 fun prt_qconst {qconst, rconst, def} = |