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 qconsts_dest: theory -> qconsts_info list |
21 val print_qconstinfo: Proof.context -> unit |
22 val print_qconstinfo: Proof.context -> unit |
22 |
23 |
23 val rsp_rules_get: Proof.context -> thm list |
24 val rsp_rules_get: Proof.context -> thm list |
24 val quotient_rules_get: Proof.context -> thm list |
25 val quotient_rules_get: Proof.context -> thm list |
25 val quotient_rules_add: attribute |
26 val quotient_rules_add: attribute |
118 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
119 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
119 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
120 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of))) |
120 |
121 |
121 |
122 |
122 (* info about quotient constants *) |
123 (* info about quotient constants *) |
123 type qconsts_info = {qconst: term, rconst: term} |
124 type qconsts_info = {qconst: term, rconst: term, def: thm} |
124 |
125 |
125 structure QConstsData = Theory_Data |
126 structure QConstsData = Theory_Data |
126 (type T = qconsts_info Symtab.table |
127 (type T = qconsts_info Symtab.table |
127 val empty = Symtab.empty |
128 val empty = Symtab.empty |
128 val extend = I |
129 val extend = I |
129 val merge = Symtab.merge (K true)) |
130 val merge = Symtab.merge (K true)) |
130 |
131 |
131 fun qconsts_transfer phi {qconst, rconst} = |
132 fun qconsts_transfer phi {qconst, rconst, def} = |
132 {qconst = Morphism.term phi qconst, |
133 {qconst = Morphism.term phi qconst, |
133 rconst = Morphism.term phi rconst} |
134 rconst = Morphism.term phi rconst, |
|
135 def = Morphism.thm phi def} |
134 |
136 |
135 val qconsts_lookup = Symtab.lookup o QConstsData.get |
137 val qconsts_lookup = Symtab.lookup o QConstsData.get |
136 |
138 |
137 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
139 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
138 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
140 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I |
139 |
141 |
|
142 fun qconsts_dest thy = |
|
143 map snd (Symtab.dest (QConstsData.get thy)) |
|
144 |
|
145 (* We don't print the definition *) |
140 fun print_qconstinfo ctxt = |
146 fun print_qconstinfo ctxt = |
141 let |
147 let |
142 fun prt_qconst {qconst, rconst} = |
148 fun prt_qconst {qconst, rconst, def} = |
143 Pretty.block (separate (Pretty.brk 1) |
149 Pretty.block (separate (Pretty.brk 1) |
144 [Syntax.pretty_term ctxt qconst, |
150 [Syntax.pretty_term ctxt qconst, |
145 Pretty.str ":=", |
151 Pretty.str ":=", |
146 Syntax.pretty_term ctxt rconst]) |
152 Syntax.pretty_term ctxt rconst]) |
147 in |
153 in |