15 type qenv = (typ * typ) list |
15 type qenv = (typ * typ) list |
16 val mk_qenv: Proof.context -> qenv |
16 val mk_qenv: Proof.context -> qenv |
17 val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option |
17 val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option |
18 |
18 |
19 type qconsts_info = {qconst: term, rconst: term} |
19 type qconsts_info = {qconst: term, rconst: term} |
|
20 val qconsts_transfer: morphism -> qconsts_info -> qconsts_info |
20 val qconsts_lookup: theory -> string -> qconsts_info option |
21 val qconsts_lookup: theory -> string -> qconsts_info option |
21 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
22 val qconsts_update_thy: string -> qconsts_info -> theory -> theory |
22 val qconsts_update: string -> qconsts_info -> Proof.context -> Proof.context |
23 val qconsts_update_generic: string -> qconsts_info -> Context.generic -> Context.generic |
23 val print_qconstinfo: Proof.context -> unit |
24 val print_qconstinfo: Proof.context -> unit |
24 end; |
25 end; |
25 |
26 |
26 structure Quotient_Info: QUOTIENT_INFO = |
27 structure Quotient_Info: QUOTIENT_INFO = |
27 struct |
28 struct |
135 (type T = qconsts_info Symtab.table |
136 (type T = qconsts_info Symtab.table |
136 val empty = Symtab.empty |
137 val empty = Symtab.empty |
137 val extend = I |
138 val extend = I |
138 val merge = Symtab.merge (K true)) |
139 val merge = Symtab.merge (K true)) |
139 |
140 |
|
141 fun qconsts_transfer phi {qconst, rconst} = |
|
142 {qconst = Morphism.term phi qconst, |
|
143 rconst = Morphism.term phi rconst} |
|
144 |
140 val qconsts_lookup = Symtab.lookup o QConstsData.get |
145 val qconsts_lookup = Symtab.lookup o QConstsData.get |
141 |
146 |
142 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
147 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo)) |
143 fun qconsts_update k qcinfo = ProofContext.theory (qconsts_update_thy k qcinfo) |
148 fun qconsts_update_generic k qcinfo = |
|
149 Context.mapping (qconsts_update_thy k qcinfo) I |
144 |
150 |
145 fun print_qconstinfo ctxt = |
151 fun print_qconstinfo ctxt = |
146 let |
152 let |
147 fun prt_qconst {qconst, rconst} = |
153 fun prt_qconst {qconst, rconst} = |
148 Pretty.block (Library.separate (Pretty.brk 2) |
154 Pretty.block (separate (Pretty.brk 1) |
149 [Syntax.pretty_term ctxt qconst, |
155 [Syntax.pretty_term ctxt qconst, |
150 Pretty.str (" := "), |
156 Pretty.str ":=", |
151 Syntax.pretty_term ctxt rconst]) |
157 Syntax.pretty_term ctxt rconst]) |
152 in |
158 in |
153 QConstsData.get (ProofContext.theory_of ctxt) |
159 QConstsData.get (ProofContext.theory_of ctxt) |
154 |> Symtab.dest |
160 |> Symtab.dest |
155 |> map (prt_qconst o snd) |
161 |> map (prt_qconst o snd) |