11 val quotdata_lookup: Proof.context -> string -> quotient_info option |
11 val quotdata_lookup: Proof.context -> string -> quotient_info option |
12 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
12 val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory |
13 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
13 val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context |
14 val quotdata_dest: theory -> quotient_info list |
14 val quotdata_dest: theory -> quotient_info list |
15 |
15 |
16 type qconsts_info = {qconst: term, rconst: term} |
16 type qconsts_info = {qconst: term, rconst: term, def: thm} |
17 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
17 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
18 val qconsts_lookup: theory -> string -> qconsts_info option |
18 val qconsts_lookup: theory -> string -> qconsts_info option |
19 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
19 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
20 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
20 val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic |
21 val print_qconstinfo: Proof.context -> unit |
21 val print_qconstinfo: Proof.context -> unit |
116 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
116 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
117 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
117 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
118 |
118 |
119 |
119 |
120 (* info about quotient constants *) |
120 (* info about quotient constants *) |
121 type qconsts_info = {qconst: term, rconst: term} |
121 type qconsts_info = {qconst: term, rconst: term, def: thm} |
122 |
122 |
123 structure QConstsData = Theory_Data |
123 structure QConstsData = Theory_Data |
124 (type T = qconsts_info Symtab.table |
124 (type T = qconsts_info Symtab.table |
125 val empty = Symtab.empty |
125 val empty = Symtab.empty |
126 val extend = I |
126 val extend = I |
127 val merge = Symtab.merge (K true)) |
127 val merge = Symtab.merge (K true)) |
128 |
128 |
129 fun qconsts_transfer phi {qconst, rconst} = |
129 fun qconsts_transfer phi {qconst, rconst, def} = |
130 {qconst = Morphism.term phi qconst, |
130 {qconst = Morphism.term phi qconst, |
131 rconst = Morphism.term phi rconst} |
131 rconst = Morphism.term phi rconst, |
|
132 def = Morphism.thm phi def} |
132 |
133 |
133 val qconsts_lookup = Symtab.lookup o QConstsData.get |
134 val qconsts_lookup = Symtab.lookup o QConstsData.get |
134 |
135 |
135 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
136 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
136 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
137 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
137 |
138 |
|
139 (* We don't print the definition *) |
138 fun print_qconstinfo ctxt = |
140 fun print_qconstinfo ctxt = |
139 let |
141 let |
140 fun prt_qconst {qconst, rconst} = |
142 fun prt_qconst {qconst, rconst, def} = |
141 Pretty.block (separate (Pretty.brk 1) |
143 Pretty.block (separate (Pretty.brk 1) |
142 [Syntax.pretty_term ctxt qconst, |
144 [Syntax.pretty_term ctxt qconst, |
143 Pretty.str ":=", |
145 Pretty.str ":=", |
144 Syntax.pretty_term ctxt rconst]) |
146 Syntax.pretty_term ctxt rconst]) |
145 in |
147 in |