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: string -> qconsts_info -> theory -> theory |
22 val qconsts_update_thy: term -> qconsts_info -> theory -> theory |
23 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
23 val qconsts_update_gen: term -> 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 |
180 |
180 |
181 (* info about quotient constants *) |
181 (* info about quotient constants *) |
182 type qconsts_info = {qconst: term, rconst: term, def: thm} |
182 type qconsts_info = {qconst: term, rconst: term, def: thm} |
183 |
183 |
184 structure QConstsData = Theory_Data |
184 structure QConstsData = Theory_Data |
185 (type T = qconsts_info Symtab.table |
185 (type T = qconsts_info Termtab.table |
186 val empty = Symtab.empty |
186 val empty = Termtab.empty |
187 val extend = I |
187 val extend = I |
188 val merge = Symtab.merge (K true)) |
188 val merge = Termtab.merge (K true)) |
189 |
189 |
190 fun transform_qconsts phi {qconst, rconst, def} = |
190 fun transform_qconsts phi {qconst, rconst, def} = |
191 {qconst = Morphism.term phi qconst, |
191 {qconst = Morphism.term phi qconst, |
192 rconst = Morphism.term phi rconst, |
192 rconst = Morphism.term phi rconst, |
193 def = Morphism.thm phi def} |
193 def = Morphism.thm phi def} |
194 |
194 |
195 fun qconsts_update_thy str qcinfo = QConstsData.map (Symtab.update (str, qcinfo)) |
195 fun qconsts_update_thy const qcinfo = QConstsData.map (Termtab.update (const, qcinfo)) |
196 fun qconsts_update_gen str qcinfo = Context.mapping (qconsts_update_thy str qcinfo) I |
196 fun qconsts_update_gen const qcinfo = Context.mapping (qconsts_update_thy const qcinfo) I |
197 |
197 |
198 fun qconsts_dest thy = |
198 fun qconsts_dest thy = |
199 map snd (Symtab.dest (QConstsData.get thy)) |
199 map snd (Termtab.dest (QConstsData.get thy)) |
200 |
200 |
201 (* FIXME / TODO : better implementation of the lookup datastructure *) |
201 (* FIXME / TODO : better implementation of the lookup datastructure *) |
202 (* for example symtabs to alist; or tables with string type key *) |
202 (* for example symtabs to alist; or tables with string type key *) |
203 fun qconsts_lookup thy t = |
203 fun qconsts_lookup thy t = |
204 let |
204 let |
205 val smt = Symtab.dest (QConstsData.get thy); |
205 val smt = Termtab.dest (QConstsData.get thy); |
206 val (name, qty) = dest_Const t |
206 val (name, qty) = dest_Const t |
207 fun matches (_, x) = |
207 fun matches (_, x) = |
208 let |
208 let |
209 val (name', qty') = dest_Const (#qconst x); |
209 val (name', qty') = dest_Const (#qconst x); |
210 in |
210 in |
225 Syntax.pretty_term ctxt rconst, |
225 Syntax.pretty_term ctxt rconst, |
226 Pretty.str "as", |
226 Pretty.str "as", |
227 Syntax.pretty_term ctxt (prop_of def)]) |
227 Syntax.pretty_term ctxt (prop_of def)]) |
228 in |
228 in |
229 QConstsData.get (ProofContext.theory_of ctxt) |
229 QConstsData.get (ProofContext.theory_of ctxt) |
230 |> Symtab.dest |
230 |> Termtab.dest |
231 |> map (prt_qconst o snd) |
231 |> map (prt_qconst o snd) |
232 |> Pretty.big_list "quotient constants:" |
232 |> Pretty.big_list "quotient constants:" |
233 |> Pretty.writeln |
233 |> Pretty.writeln |
234 end |
234 end |
235 |
235 |